Prove a complete funding obstruction for two-owner native multigraphs

research/bit-multigraph-funding-obstruction/PROOF.md

@@ -0,0 +1,204 @@
+# Parallel supports cannot fund the two-early-helper BIT controller
+
+## 1. Model, theorem and source boundary
+
+We use the explicit relaxed model of PR5456, now allowing arbitrary parallel
+edges and arbitrary diagonal Q/D flags. Work over F2 with q²=0 and independent
+commuting involutions D_i, i=0,...,c-1. Call i has a coordinate support C_i of
+size four; every field belongs to exactly one or two supports. Let T_i apply
+D_i on C_i and identity elsewhere. The chronological word is
+
+    F_(c-1)...F_0,       F_i=T_i(I+qR_i).
+
+Columns of R_i outside C_i vanish; rows outside C_i are allowed. There are
+u_i,w_i supported on C_i with u_i!=0, R_i u_i=0 and R_i w_i=u_i. Completing
+this chain to a four-role basis leaves two arbitrary helper columns. These
+are the same favorable native-main/early-helper hypotheses as PR5456, not a
+new physical assertion about every permitted matrix.
+
+The required endpoint is diagonal, with entry
+
+    (product_(i:a in C_i) D_i)(1+t_a q),        t_a in {0,1}.
+
+Let Qcount=sum_a t_a. **Theorem: Qcount<=2c.** This covers every order, any
+finite number of calls, private fields, arbitrary parallel intersections,
+D-only targets and arbitrary helper writes outside the support. It needs
+independent D symbols, coordinate four-supports, at most two owners and the
+native length-two zero Jordan chain. It does not cover extra thin calls,
+non-coordinate projectors, three owners or dependent D symbols.
+
+For the retained actual FULL invoice, the theorem implies target rank minus
+paid rank <=-63c, and strictly negative target-minus-paid moment for every
+r^s tariff with 0<s<=1. Thus parallel edges cannot fund this entire class.
+No selected frontier, native implementation, supplier or kappa is changed.
+
+## 2. Exact labels and a triangular restriction for every call
+
+Write h_i(a) for the incidence bit vector of calls j<i containing a. Factoring
+all commuting T_i to the left shows that coefficient R_i(a,b) has group label
+h_i(a)+h_i(b). Because q²=0 there are no higher R products. At each off-diagonal
+matrix entry, coefficients with each independent group label cancel.
+
+Fix i and restrict R_i to its four support rows/columns; call this A_i.
+Partition C_i into private singleton fields and common-support classes
+E_ij=C_i intersect C_j. Every E_ij has one partner j, since ownership<=2.
+For distinct a,b in C_i:
+
+- If b is private, its sole contributing call is i, so R_i(a,b)=0.
+- If b in E_ij with j<i and a not in E_ij, the label at call i has bit j=1
+  (b in C_j, a not); the label at call j has bit j=0. Thus R_i(a,b)=0.
+- If b in E_ij with j>i and a in E_ik with i<k<j, the label at call j has
+  bit k=1 and the label at call i has bit k=0. Thus R_i(a,b)=0.
+
+Only calls i,j can contribute column b, so these unequal-label arguments
+remain valid with completely arbitrary rows outside either support.
+Order the blocks of C_i as future partners j>i in increasing j, then all past
+partners, then private singletons. A column in a future block may write only
+to its own or later blocks; a past block column writes only within that block;
+private columns are diagonal. Therefore A_i is block lower triangular.
+No claim is made that the full R_i is block triangular.
+
+For each shared class E_ij, the two endpoint diagonal blocks satisfy
+
+    A_ij+A_ji = diag(t_a : a in E_ij).                              (1)
+
+Indeed, fields within this class have identical membership histories, hence
+both group labels are zero, and only i,j contribute their columns. A private
+diagonal block is the scalar t_a. These facts are valid in every chronology.
+
+Let z(B) denote the algebraic multiplicity of eigenvalue zero in B; equivalently
+z(B)=dim ker B^r for an r-by-r matrix. Block triangularity makes z(A_i) the sum
+of the block z values. Restricting the actual native chain equations gives
+A_i u_i=0, A_i w_i=u_i!=0, so z(A_i)>=2. This uses a genuine length-two chain,
+not just singularity or a trace condition.
+
+## 3. Local spectral lemma, including the exceptional triple
+
+Let A,B be r-by-r binary matrices, A+B=diag(t), and let k=sum t be the integer
+number of ones. For r<=3,
+
+    z(A)+z(B) <= 2r-k,                                             (2)
+
+except possibly r=3,k=2. In that case either the same bound4 holds, or
+z(A)=z(B)=3 and the sum is6. The latter is the only exceptional case.
+
+Proof: for k=0 the dimension bound suffices. For k=r, B=I+A, so z(B) is the
+multiplicity of eigenvalue one in A. Distinct factors x and x+1 in its degree-r
+characteristic polynomial give z(A)+z(B)<=r. The remaining cases for r<=3
+have k=1 or r=3,k=2. When k=1, trace(A)+trace(B)=1, so A,B cannot both be
+nilpotent; at least one has z<=r-1, proving the bound2r-1. For r=3,k=2,
+trace(A)=trace(B). A sum greater than4 is5 or6. Sum5 would require multiplicities
+3 and2: the former matrix is nilpotent with trace0, while the latter has
+characteristic polynomial x²(x+1) over F2, hence trace1. This is impossible.
+Sum6 means both multiplicities are3, as claimed.
+
+The exception is real. In column-bit notation,
+A=(2,7,5), B=(3,5,5) are nilpotent3 and A+B=diag(1,1,0).
+The verifier checks their characteristic polynomials, powers and exact diagonal
+sum using independent representations. Ignoring this exception would give a
+false proof for mixed Q/D targets.
+
+## 4. The exceptional cost cancels globally
+
+First remove any class E_ij of size four. It exhausts both C_i,C_j, so those
+two calls share no field with any other call. Their component has at most four
+Q targets, exactly the required upper bound2×2, regardless of helper writes
+outside its support. We may account for these vertices separately. The
+remaining calls and field incidences have all shared classes of size<=3;
+Section2 still applies to their restrictions and unchanged exact coefficient
+conditions. No new subword endpoint is assumed by this bookkeeping removal.
+
+Write c for the remaining number of calls, E for the number of shared fields
+(counting multiplicity), P for the number of private fields, and Z for the
+number of D-only fields (t_a=0). Then
+
+    4c=2E+P,       Qcount=E+P-Z=4c-E-Z.                             (3)
+
+Let b be the number of exceptional triple classes from Section3 for the
+actual matrices. Their endpoint call pairs are disjoint: a four-support call
+cannot contain two distinct size-three classes. Each exceptional endpoint has
+z(A_i)>=3, since one of its diagonal blocks already has z=3. Every other call
+has z(A_i)>=2. Therefore
+
+    sum_i z(A_i) >= 2c+2b.                                        (4)
+
+On the other hand, sum (2) over shared classes, allowing +2 at exactly the b
+exceptions. A private field contributes1 precisely when it is D-only. Writing
+Z_E,Z_P for the two kinds of D-only field, we obtain
+
+    sum_i z(A_i) <= sum_shared(2|E_ij|-#Qflags)+Z_P+2b
+                 = E+Z_E+Z_P+2b = E+Z+2b.                         (5)
+
+The exceptional +2 terms cancel between (4) and (5). Hence E+Z>=2c, and (3)
+gives Qcount<=2c. Adding back the four-edge components proves the theorem.
+The proof is a global multiplicity/ownership argument, not repeated last-call
+elimination and not a finite UNSAT claim.
+
+In the all-Q subcase Z=0, equality in 2c<=E<=2c forces P=0 and E=2c. Thus a
+completed all-Q word has no private fields. For example, the three-call doubled
+path with supports {0,1,4,5},{0,1,2,3},{2,3,6,7} cannot close all eight Q flags.
+Those eight flags would give a positive rank surplus33, but the theorem limits
+it to six. The mixed triple counterexample does not repair that funding gap.
+
+## 5. Complete actual signed invoice
+
+The live source WORD has111 ports and439 original helpers. Giving each port two
+early helper roles uses222 **distinct original helper owners** and leaves217
+untouched H8 jobs per FULL. A helper is selected only at its unique first
+departure from frame zero, which belongs to one port. The verifier scans the
+actual D/A/B/C source sections:439 helper first departures,286 rank-one first
+departures distributed over111 ports with at least two each, no helper write
+before departure, and222 distinct owners when choosing two per port. Repeated
+observations of one helper are not credited as new jobs. Reusing one owner at
+multiple ports is outside this invoice premise. The retained complete paid profile per FULL is
+
+    1323H1+1342H2+79H3+44H4+102H5+11H6+19H7,
+
+of total rank5129. It includes the retained source's owned center-query charges;
+none are removed. The independently authenticated source receipt and WORD
+supply these quantities; the verifier checks them directly.
+
+At a port, each call contributes four rank-seven D incidences. Independent
+fresh D axes give rank7 for a private D factor and rank14 for a shared pair;
+a Q flag adds one. Across c FULLs and111 ports, even permitting different
+support multigraphs at different ports, target rank is at most
+
+    217*8*c + 111*(28c+2c) = 5066c.
+
+Thus the complete target-minus-paid rank is <=-63c. Before applying the
+structural theorem its exact expression is111Qcount-285c for a uniform port
+pattern, with the obvious sum over port-specific Q counts otherwise.
+Selected helpers are included in these active target fields, not credited
+again among the217 untouched helpers. Dirty input independence and all
+retained helper targets remain charged. Adding physical prologue, chart,
+movement, cleanup and storage costs cannot improve this already-negative
+favorable native-only bill; those costs are not claimed implemented here.
+
+All paid ranks are<=7, and every credited target rank is>=7. For 0<s<=1 the
+function r^(s-1) is nonincreasing. Thus
+
+    sum_targets r^s - sum_paid r^s
+      <= 7^(s-1) (sum_targets r - sum_paid r)
+      <= -63c * 7^(s-1) < 0       (c>0).
+
+This proves the signed concave-moment gate, not merely the t=1 test. It uses
+independent D axes and the specific actual helper debit. Dependent D symbols,
+changed axis overlaps, a different retained source, three owners, extra thin
+calls or non-coordinate supports require a new proof and full invoice.
+
+## Evidence and attribution
+
+The written argument is the quantified result. Exact finite tests corroborate
+local spectral cases, chronology/label block ordering, native chains, complete
+positive endpoints and signed counts. They are not a controller search or a
+proof certificate for PR5456's saved solver outcomes. No solver is invoked.
+
+PR5456 at0d64d4d5d73f370182ada9825a611c86cfbf0049 supplies the model, simple-graph
+last-call argument and complementary-word control. This proof restates all
+needed hypotheses and proves its new global lemma without importing that
+pending package. Its immutable proof SHA256 is
+8f8f3ef5682adb154ccacd8b533b6733ff08a00dd47a38363587ef816fe59e62.
+PR5452/5388 motivate early helper observations; the actual retained PR589/555
+source and its eumemic/Anthropic-assisted lineage are pinned locally.
+Prepared by JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0.
+No independent human or proof-kernel acceptance is claimed.

research/bit-multigraph-funding-obstruction/README.md

@@ -0,0 +1,53 @@
+# Parallel-support funding obstruction for early BIT helpers
+
+Every completed two-owner coordinate four-support controller in the stated
+native-chain model has at most two Q targets per FULL call, even with arbitrary
+parallel edges, D-only target flags and helper writes outside supports.
+The complete retained invoice consequently loses at least63 ranks per FULL,
+and loses for every concave rank-power tariff r^s,0<s<=1.
+
+[PROOF.md](PROOF.md) gives the uniform argument. Exact coefficient labels make
+each call restriction block triangular. Native chains require zero algebraic
+multiplicity>=2. The only small-block spectral exception is a mixed-flag
+nilpotent triple; its disjoint endpoint calls require extra multiplicity that
+exactly cancels the exception. Four-shared-field pairs are accounted separately.
+This is a global theorem, not another finite support-graph UNSAT receipt.
+
+The actual source scan identifies222 distinct original helper owners at111
+ports, leaving217 untouched H8 jobs per FULL. No repeated observation earns
+an independent output job. Paid rank5129 versus target rank<=5066 gives the
+signed deficit. Extra physical preparation/movement costs cannot rescue it;
+no physical implementation or new kappa is claimed.
+
+## Reproduce
+
+```sh
+python3.12 -I -W error -B research/bit-multigraph-funding-obstruction/verify.py
+python3.12 -I -O -W error -B research/bit-multigraph-funding-obstruction/verify.py
+python3.12 -B scripts/research_package.py --package research/bit-multigraph-funding-obstruction
+```
+
+Expected `PASS_MULTIGRAPH_FUNDING_OBSTRUCTION`. Standard library only; no solver.
+The verifier compares independent characteristic-polynomial and matrix-power
+multiplicities on4164 local cases, exact chronology restrictions, full positive
+group-ring words, and actual source/owner/invoice quantities. Finite checks
+corroborate the written theorem; they are not proof-kernel acceptance.
+
+SOURCES.json declares only actual main-history inputs. Pending PR5456's model
+and simple-graph result are credited at immutable head
+0d64d4d5d73f370182ada9825a611c86cfbf0049; the new proof restates and derives all
+needed mathematics rather than importing that package or its solver receipts.
+
+## Open next questions
+
+A useful next caller must change coordinate supports, independent D symbols,
+at-most-two-owner fields or the native main-chain premise. Supply an exact
+completed word and full distinct-owner/paid invoice before a larger search.
+Additional physical routing/backing and native admission remain unproved.
+
+## Credit
+
+PR5456 supplies the model and simple-graph boundary; PR5452/5388 motivate the
+early helper interface. Retained PR589/555 source and eumemic/Anthropic-assisted
+lineage remain unchanged. JoyboyBrian, with substantial OpenAI Codex assistance;
+Apache-2.0. Independent peer review is AI-assisted, not human/formal acceptance.

research/bit-multigraph-funding-obstruction/RESULT.json

@@ -0,0 +1,17 @@
+{
+  "all_flags_covered": true,
+  "chronologies": 616,
+  "distinct_selected_helper_owners": 222,
+  "exceptional_cases": 18,
+  "graph_fixtures": 103,
+  "literal_positive_words": 3,
+  "local_spectral_cases": 4164,
+  "new_kappa": false,
+  "paid_rank_per_FULL": 5129,
+  "rank_deficit_per_FULL": 63,
+  "rejecting_controls": 4,
+  "restricted_entry_checks": 31296,
+  "solver_run": false,
+  "status": "PASS_MULTIGRAPH_FUNDING_OBSTRUCTION",
+  "untouched_helpers_per_FULL": 217
+}

research/bit-multigraph-funding-obstruction/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/PR589-STATE-SHARING-PROBE.json",
+      "usage": "input",
+      "git_blob": "cb4a5da1cd0455b754f7607d6511c5b40421fab2",
+      "sha256": "70c385ac83dc73ea977c7c60ab23041261929de9b17ccaa4874b85ab0891b663"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+    }
+  ]
+}

research/bit-multigraph-funding-obstruction/TASK.json

@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Uniform funding obstruction for all two-owner coordinate-support multigraphs with arbitrary Q/D flags and the native zero Jordan chain.",
+  "scope_change_reason": "Fresh PR5456 excludes only simple graphs. Global spectral compensation handles arbitrary parallel classes and proves the complete retained invoice nonpositive.",
+  "bottleneck_link": "Closes the parallel-support escape of the actual two-early-helper controller without a larger finite search.",
+  "budget_minutes": 60,
+  "stop_rule": "Require a uniform graph/funding argument or exact funded counterexample; no repeated solver census or simple last-call lemma.",
+  "outcome": "negative-result",
+  "evidence": "PROOF.md;4164 exact local cases;chronology checks;literal endpoint controls;distinct actual helper-owner/source invoice binding.",
+  "author": "JoyboyBrian, with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, source analysis and writing; independent AI peer review.",
+  "open_questions": [
+    {
+      "question": "Can non-coordinate supports, dependent D factors or three-owner fields fund an actual caller?",
+      "why_it_matters": "Each changes an essential hypothesis of the global block/multiplicity proof.",
+      "first_step": "Give one exact completed word and its distinct helper-owner debit before evaluating the full signed moment.",
+      "blocked_by": "No funded physical word or ordinary routing/cleanup tariff is supplied."
+    }
+  ]
+}