Prove sharp five-thirds bounds for two binary helper classes

research/binary-helper-five-thirds/PROOF.md

@@ -0,0 +1,189 @@
+# Two sharp binary bounds with different scopes
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+All vector spaces and matrices in this note are over F2. A matrix rank is an
+integer. A trace is an element of F2. The two theorems have different
+hypotheses. Neither theorem states a limit for every native controller.
+
+## A. Commuting supports of rank three
+
+Let E_1,...,E_f be pairwise commuting idempotents of rank three on a finite
+vector space V. For each i, assume
+
+    E_i R_i = R_i E_i = R_i,
+    R_i is similar to J_2(0) direct-sum [1] direct-sum 0.
+
+Here J_2(0) is the two-dimensional nilpotent Jordan block. Thus each R_i has
+rank two, trace one, and is not idempotent. Suppose
+
+    sum_i R_i = P,
+
+where P is an idempotent that commutes with every E_i. Then
+
+    rank(P) <= 5*f/3.                                      (A)
+
+In particular, if P=I_n, then n<=5*f/3. The statement permits zero target
+coordinates. It imposes no order on the calls and no prefix condition.
+
+### Common coordinates and components
+
+An idempotent has minimal polynomial dividing x(x+1). These two roots are
+distinct in F2. Commuting idempotents therefore have a common eigenbasis:
+split V into the kernel and image of one idempotent, then repeat the split
+on each invariant part. Include P in these splits.
+
+In this basis, E_i selects a three-element coordinate set S_i. The two-sided
+support condition confines every nonzero entry of R_i to S_i times S_i.
+Form a graph on the calls. Join i and j when |S_i intersect S_j|>=2.
+
+For one connected component C, put T_C=sum_{i in C} R_i. This matrix is
+diagonal. To see this, fix distinct coordinates a,b. Any call that contributes
+to entry (a,b) has both coordinates in its support. All such calls belong to
+one component. Their total is zero because P is diagonal. Thus the entry is
+zero in that component and is zero in all other components.
+
+A component with c calls has a support union of size at most c+2. Start at one
+vertex of a spanning tree. Its support has size three. Each next vertex
+shares at least two coordinates with a previous vertex and adds at most one.
+Hence, when c>=3,
+
+    rank(T_C) <= c+2 <= 5*c/3.                              (1)
+
+### Components with one or two calls
+
+A one-call component cannot occur: its sum would be R_i, which is diagonal
+and hence idempotent over F2. This contradicts the stated Jordan type.
+
+For two calls, the support union has size at most four. Its diagonal sum D
+has trace 1+1=0, so rank(D) is even. Rank four is impossible by the following
+rank-additivity fact.
+
+Suppose A+B=D, where D is an idempotent of rank four and A,B each have rank
+two. Since image(D) is contained in image(A)+image(B), equality of dimensions
+gives
+
+    image(D) = image(A) direct-sum image(B).
+
+For x in image(A), D x=x. The decomposition A x+B x=x into these two images is
+unique, so A x=x and B x=0. Thus A is identity on its image, and A^2=A.
+The same argument gives B^2=B. Apply this fact to the two R terms to obtain
+a contradiction. Therefore rank(T_C)<=2 for a two-call component, which is
+also at most 5*c/3.
+
+Finally, rank is subadditive. Sum the component bounds:
+
+    rank(P) = rank(sum_C T_C) <= sum_C rank(T_C) <= 5*f/3.
+
+This proves (A). Components can share one coordinate; the rank inequality
+does not assume that their diagonal supports are disjoint.
+
+### A sharp example
+
+Use coordinates a,b,c,d,e and let P_x denote the coordinate projector at x.
+Set
+
+    N_1 = (b+c)(b*+c*),       N_3 = (c+d)(c*+d*),
+    R_1 = P_a + N_1,
+    R_2 = P_b + P_c + P_d + N_1 + N_3,
+    R_3 = P_e + N_3.
+
+The supports are abc, bcd, cde. Each term has the required Jordan type and
+the sum is I_5. Thus three calls attain five outputs.
+
+This example also satisfies the stage order condition
+
+    [E_i, sum_{j<i} R_j] = 0.
+
+For independent commuting stage variables D_i and q^2=0, define
+
+    M_i = (I+(D_i+1)E_i)(I+q R_i).
+
+The exact product M_3 M_2 M_1 is diagonal. Its entries are
+
+    (1+q) D_1, (1+q) D_1 D_2, (1+q) D_1 D_2 D_3,
+    (1+q) D_2 D_3, (1+q) D_3.
+
+The verifier multiplies the polynomial matrices over F2 and checks every
+coefficient. This abstract binary identity is not a complex Laurent lift or
+a replay of a physical native caller.
+
+## B. A finite adaptive grammar
+
+This theorem permits an outside-support helper contribution, which theorem A
+does not permit. It limits the retained state instead. No implication from
+one theorem to the other is used.
+
+A state is a binary matrix on at most three live coordinates. An isolated
+coordinate has diagonal entry zero or one and no off-diagonal entry in its
+row or column. Remove every isolated coordinate at once. Charge one output
+for each removed diagonal one. A removed zero can represent a D-only output.
+Order the remaining coordinates by the lexicographically smallest matrix
+under coordinate permutations. No other change of basis is allowed.
+
+There are two operations.
+
+1. FULL: put the live coordinates first and add zero coordinates to reach
+   four. The first three coordinates form the source support E. Add
+
+       R = u v^T + h p^T,
+
+   where u,v,p are nonzero vectors in that support, v^T u=p^T u=0,
+   p is different from v, and h is any vector on all four coordinates.
+   Charge one FULL. The conditions make u v^T a rank-one nilpotent and make
+   p an independent helper input row. The source E contains the whole old
+   state, so E commutes with it. Apply the stated state reduction.
+2. THIN: add one zero coordinate, with total size at most four. Add any
+   rank-one matrix u v^T with u and v nonzero on those coordinates.
+   Charge one THIN, then apply the same state reduction.
+
+Reject a transition if more than three live coordinates remain. Removed
+coordinates cannot return as catalysts. A closed word starts and ends at the
+empty state. Write g for its output count, h for its THIN count, and f for its
+FULL count. Then
+
+    3*(g-h) <= 5*f.                                        (B)
+
+For f>0 the maximum ratio (g-h)/f is exactly 5/3.
+
+### Complete finite certificate
+
+The code enumerates every parameter tuple in the stated FULL alphabet and
+retains its matrix. There are 315 distinct matrices. It enumerates every
+nonzero u,v pair for each THIN support size. Breadth-first closure from the
+empty state reaches 94 canonical states and 20,020 legal raw transitions.
+
+For each source, target, and operation type, retaining only the largest gain
+leaves 10,035 transitions. A discarded smaller gain cannot improve the
+claimed bound. The verifier checks the potential on all raw transitions too.
+
+The certificate assigns an integer z(S) to each reachable state S. For every
+edge S->T with counts (g,h,f), it verifies
+
+    z(T)-z(S) >= 3*g-3*h-5*f.                              (2)
+
+Sum (2) along a closed word. The potentials cancel, proving (B). Each
+certificate transition is also checked against the declared matrix rule.
+The retained witness starts at the empty state, uses three FULL operations,
+and returns there with five outputs and no THIN. This proves sharpness.
+
+The mathematical implication from a valid potential to (B) is elementary.
+The finite enumeration and the retained potential are checked by the supplied
+program. This is a finite computational certificate, not proof-assistant
+acceptance or a claim about an unrestricted controller grammar.
+
+## Verification boundaries
+
+The verifier also checks all 84 three-dimensional matrices of the stated
+Jordan type and all 28,224 two-call embeddings into a four-coordinate union.
+The only diagonal sum ranks are zero and two. This finite check supports the
+written two-call argument; it does not replace the general proof above.
+
+Rejected controls include a lowered tight potential, a missing reachable
+state, an unpaid THIN query, a non-nilpotent native direction, and a changed
+motif coefficient. The identity on three coordinates is retained as a
+counterexample after the Jordan-type hypothesis is dropped.
+
+Neither theorem permits an unproved complex reduction modulo two. Neither
+proves native input access, helper restoration, supplier admission, complete
+pricing, or a multiplication exponent. Those obligations remain separate.

research/binary-helper-five-thirds/README.md

@@ -0,0 +1,105 @@
+# Sharp 5/3 bounds for two binary helper-controller classes
+
+This package gives a scoped negative result and a sharp binary construction.
+It proves two distinct bounds on Q outputs per FULL call. The complete kappa
+calculation does not improve.
+
+- **Global support theorem:** commuting rank-three stage projectors, with each
+  query term supported on its stage and of type `J_2(0) direct-sum [1]`, give
+  at most `5*f/3` Q outputs from f FULL terms. The proof also permits D-only
+  target coordinates and needs no call order.
+- **Finite adaptive theorem:** a grammar with at most three live coordinates
+  permits outside-support helper feedback and paid THIN queries. Its 94-state,
+  10,035-edge graph has exact maximum `(Q outputs - THIN calls)/FULL = 5/3`.
+
+Read [the proof and exact scope](PROOF.md),
+[the integer potential and attaining word](CERTIFICATE.json), and
+[the deterministic verification receipt](RESULT.json). The two theorems have
+different hypotheses. The finite graph is not an exhaustive model of native
+controllers. A three-FULL, five-output example attains both bounds; its full
+binary polynomial endpoint is checked.
+
+A later local-only
+[catalyst extension](https://github.com/CrocSwap/integer-mult-bounds/discussions/4930#discussioncomment-19156336)
+reports 188 states and 32,110 edges with the same 5/3 bound. It permits one
+completed Q coordinate to remain live and credits the released 94-state
+search. This package does not claim that broader result or that its own
+finite grammar is the largest checked class.
+
+## Reproduce
+
+Python 3.12 or later and its standard library are sufficient. No native source,
+network call, solver, or pending PR is a runtime dependency.
+
+```sh
+python3.12 -B scripts/research_package.py --package research/binary-helper-five-thirds
+python3.12 -O -B research/binary-helper-five-thirds/verify.py
+```
+
+The first command ends with:
+
+```text
+PASS_REGISTERED_RESEARCH_PACKAGE research/binary-helper-five-thirds outcome=negative-result
+```
+
+The direct verifier prints `PASS_BINARY_HELPER_FIVE_THIRDS` in its JSON result
+and compares the result with `RESULT.json`. It checks all 20,020 raw graph
+transitions, the integer potential, the sharp binary polynomial word, and
+28,224 two-term support cases. Meaningful perturbations must fail: a changed
+potential, omitted state, unpaid THIN query, invalid native direction, and
+wrong endpoint coefficient. Normal and optimized Python use explicit checks.
+
+For a trusted source export, run the same direct verifier after extraction.
+The registered runner needs Git history for the provenance pins. The direct
+verifier does not. `--write` regenerates the receipt and is an authoring option.
+
+## Scope and effect on kappa
+
+The current publication base is `32890bc5de034ab8fc93ac88ead7279a6a416d04`.
+The selected record and task card at that base are historical provenance in
+[SOURCES.json](SOURCES.json). The assigned task changed from caller design to
+publication of these scoped bounds; [TASK.json](TASK.json) records that change.
+
+There is no new recursive invoice or claimed kappa. The operation ratio is
+not a multiplication exponent. The source interface, fixed cover maps,
+owned state, complex phases, recursive pricing, and supplier admission are
+not checked here. No selected source or frontier file is changed. Earlier
+floating-point tariff screens are excluded from the proof and verifier.
+
+The original search also tested larger finite components, kernel packets,
+D-only Gram factors, and fresh-axis cuts. Those bounded records are retained
+in the coordinated closeout archive. They supply no general impossibility
+claim and are not dependencies of this package.
+
+## Open next questions
+
+The one-catalyst finite extension already has a local result at the link
+above; repeating that census is not the proposed next task. A useful next
+question is whether a source-compatible packet outside the global support
+hypothesis and outside both finite grammars can beat the bound. First give
+its exact binary matrices and full source obligations. A favorable matrix
+word would still need a signed complex identity and complete paid and target
+accounting. This package does not reserve that work.
+
+A separate review can check the component proof and the grammar-to-native
+boundary. The program certifies the finite graph, not the physical scope of
+all possible native words. These questions are also recorded in TASK.json.
+
+## Credit
+
+Cinna Davis / 1337isnot1337 supplied the earlier commuting-projector tangent
+reduction and support-pair obstruction in the
+[productive-controller proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/productive-controller-basis-search/GLOBAL-PROOF.md).
+The present rank-three component argument changes that two-coordinate
+support model. The earlier package retains credit for the controller, native,
+mixed-target, Clifford, and outer-recursion contributors.
+
+Dillon's [PR #5388](https://github.com/CrocSwap/integer-mult-bounds/pull/5388)
+motivated the early helper-observation interface. The physical source and
+wrapper work remain separate from this abstract binary certificate. The
+later catalyst extension is credited above as broader finite coverage.
+
+New proof, code, and certificate by Ali Romman, with substantial OpenAI Codex
+assistance. Parallel Codex workers checked the component argument and the
+separation from the rank-four simple-graph model. This is not independent
+human review. New work is under Apache-2.0.

research/binary-helper-five-thirds/RESULT.json

@@ -0,0 +1,45 @@
+{
+  "controls": {
+    "free_thin_query_rejected": true,
+    "identity_term_violates_bound_without_Jordan_condition": true,
+    "lowered_potential_rejected": true,
+    "missing_state_rejected": true,
+    "non_nilpotent_source_rejected": true,
+    "wrong_motif_endpoint_rejected": true
+  },
+  "graph": {
+    "cycle": {
+      "full": 3,
+      "gain": 5,
+      "thin": 0
+    },
+    "dominant_edges": 10035,
+    "exact_maximum": "5/3",
+    "full_matrices": 315,
+    "raw_edges": 20020,
+    "sha256": "314cc195731ca1ea933e6fab812107629ab087425e40c86e6018c2113b349e1f",
+    "states": 94
+  },
+  "scope": "Two separate binary classes; no complex lift, native admission, or kappa improvement.",
+  "sharp_motif": {
+    "exact_binary_polynomial_endpoint": true,
+    "full": 3,
+    "outputs": 5,
+    "stage_degrees": [
+      1,
+      2,
+      3,
+      2,
+      1
+    ]
+  },
+  "status": "PASS_BINARY_HELPER_FIVE_THIRDS",
+  "two_call_control": {
+    "diagonal_rank_counts": {
+      "0": 84,
+      "2": 81
+    },
+    "pairs": 28224,
+    "three_dimensional_terms": 84
+  }
+}

research/binary-helper-five-thirds/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/productive-controller-basis-search/GLOBAL-PROOF.md",
+      "usage": "provenance",
+      "git_blob": "74b67e22e6c063193a83825207cdec19a8fef7a4",
+      "sha256": "adc377b13924701bf5b0b50b091d8b69c90195d50ce0f6808f7fb4c7e0b16457"
+    }
+  ]
+}