Prove binary E8 factor-rank-sum barrier 21 at every term count

research/e8-one-extra-direction/PROOF.md

@@ -0,0 +1,105 @@
+# An unbounded-term factor-rank obstruction
+
+## Model and cited premises
+
+Let Q be the full 120 E8 root lines used by Ali Romman in
+`research/e8-small-redundancy`. Their displayed representatives have squared
+length four. Set `K(q,r)=1+(q dot r)/2 mod 2` and
+`C=col_F2(K)=row_F2(K)`. For a binary word w on Q, let rho(w) be the
+rational dimension of the root vectors in its support.
+
+For `K=A B^T` over F2, the cost of column pair (a,b) is the rational rank
+of `(q dot r)_{q in supp(a), r in supp(b)}`. Write this as c(a,b) and add
+over all columns. Multiplying the displayed pairing by one half does not
+change its rational rank. Let r_A and r_B be the actual binary ranks.
+
+The following are cited premises from Ali Romman's #4967, retained at the
+base commit pinned in SOURCES.json. This package does not replay them.
+
+1. C has dimension nine, and every nonzero c in C has rho(c)=8.
+2. For every coset v+C other than C,
+   `sum_{w in v+C} (8-rho(w)) <= 8`.
+   This is equation (1) of TEN-PROOF.md, including all words in that coset.
+3. Every basis of a binary space U containing C, with dimension nine,
+   ten or eleven, has sum of support ranks at least 72.
+   The dimension-ten case is in TEN-PROOF.md and the dimension-eleven case
+   is the main basis theorem of ELEVEN-PROOF.md. Dimension nine is premise 1.
+
+These are the only E8-specific premises. The binary expression defining K
+and the rational inner product defining the cost are separate operations.
+
+## Normalization does not raise cost or factor ranks
+
+Delete any term with a zero factor. When two left columns agree, replace
+`a b_1^T + a b_2^T` with `a (b_1+b_2)^T`, using binary addition. The new
+right support is contained in the union of the two old right supports.
+For fixed left support, the rank of its rational pairing with that union
+is at most the sum of the old pairing ranks. Restricting to the new support
+cannot increase rank. Thus the merge does not increase total cost.
+The transposed operation handles equal right columns.
+
+Each deletion or merge strictly decreases the finite number of terms.
+After finitely many operations there are no zero columns and the columns
+are distinct on each side. The product remains K. Each new column is a
+binary combination of old columns on its own side, so neither factor space
+nor its rank increases. Recompute actual ranks after normalization.
+There is no assumption that rank stays constant or that cost-zero nonzero
+terms may be discarded.
+
+Every factorization of K satisfies `C subset col(A)` and
+`C subset col(B)`, since K is symmetric. Hence r_A,r_B are at least nine.
+
+## Two spaces with at most one extra direction
+
+Consider a normalized factorization with m terms and
+`r_A=9+s`, `r_B=9+t`, where s,t are in {0,1}.
+If s=0 every left word is a nonzero member of C and has support rank eight.
+If s=1, the left space consists of C and exactly one other coset. Its
+columns are distinct, so premise 2, with nonnegative defects, gives
+
+`sum_j (8-rho(a_j)) <= 8s`.
+
+The same argument on the right gives defect sum at most 8t.
+For rational subspaces U,V in the nondegenerate eight-dimensional root
+space, the rank of the restricted pairing is at least
+`dim U + dim V - 8`. Therefore
+
+`cost >= sum_j (rho(a_j)+rho(b_j)-8) >= 8m-8s-8t`.
+
+Sylvester's binary product-rank inequality gives
+`9=rank(K) >= r_A+r_B-m`, so `m >= 9+s+t`. Substitution yields
+`cost >= 72`. The inequalities apply to the normalized factorization;
+the original cost was at least as large. This proves the all-term-count
+floor when both original factor ranks are at most ten.
+
+For a normalized rank-(10,10) factorization, the intermediate inequality
+is `cost >= 8m-16`. At twelve terms this is 80. This stronger expression
+uses the reduced term count; arbitrarily padding an unreduced factorization
+does not justify substituting its larger term count.
+
+## The rank-nine / rank-eleven boundary
+
+Suppose one original factor has rank nine and the other rank at most
+eleven. Delete zero terms. The rank-nine factor's nonzero columns lie in
+C and span the full rational root space individually, by premise 1.
+Consequently each term costs exactly the support rank of the opposite
+column. Select a basis from the opposite factor's columns. Its column
+space contains C and has dimension between nine and eleven, so premise 3
+prices that basis at least 72. All remaining terms have nonnegative cost.
+The total is at least 72. In fact, with m nonzero terms and opposite rank
+r, it is at least `72+(m-r)`, because each unselected nonzero word has
+support rank at least one. Duplicate merging is not needed in this case.
+
+## Rank-sum consequence and the twelve-term boundary
+
+If r_A+r_B is at most 20, both ranks are at least nine. The only cases are
+(9,9), (9,10), (10,9), (10,10), (9,11), and (11,9). The preceding two
+arguments cover all of them, for every finite number of terms.
+Thus any cost below 72 requires `r_A+r_B >= 21`.
+
+For twelve terms, Sylvester also gives `r_A+r_B <= 21`, and neither factor
+rank exceeds twelve. A cost below 72 can therefore occur only at
+(9,12), (10,11), (11,10), or (12,9). The theorem does not decide any of
+these four pairs. This is a necessary-condition result for the fixed binary
+factorization and its separate rational pairing cost. It does not imply a
+lower bound for every physical decoder or multiplication algorithm.

research/e8-one-extra-direction/README.md

@@ -0,0 +1,99 @@
+# Binary E8 pairing savings require factor-rank sum at least 21
+
+Scoped proof from cited geometric premises. No new kappa or physical decoder.
+
+For the fixed 120-line binary E8 matrix
+`K(q,r) = 1 + (q dot r)/2 mod 2`, every finite binary factorization
+`K = A B^T` whose actual binary factor ranks sum to at most 20 has rational
+source-reader pairing-rank cost at least **72**, regardless of term count.
+In particular, adding arbitrarily many terms cannot help when both factor
+spaces add at most one direction beyond the rank-nine code.
+
+The reduced rank-(10,10) case has the stronger bound `cost >= 8m - 16`,
+where `m` is its term count after zero deletion and duplicate merging.
+Thus a reduced twelve-term factorization of that rank pair costs at least 80.
+The other boundary follows by choosing a basis from the rank-eleven
+factor when the opposite factor has rank nine.
+
+Ali Romman's [#4967](https://github.com/CrocSwap/integer-mult-bounds/pull/4967)
+already proves the 72 floor for every factorization with at most eleven
+terms. This result removes the term-count restriction for the stated factor
+ranks. It does not settle the general twelve-term question. The
+[proof](PROOF.md) cites the existing one-coset defect theorem and
+minimum-basis theorem for dimensions nine through eleven. Neither
+predecessor geometry nor its finite census is rerun as this contribution.
+
+## Evidence and reproduction
+
+From the repository root, using CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/e8-one-extra-direction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B research/e8-one-extra-direction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/e8-one-extra-direction --check-source-history
+```
+
+The written proof supplies the unbounded-term quantifier. The standalone
+verifier corroborates the new algebra steps on a separate six-line rational
+configuration. It enumerates 262,144 merge inequalities, 4,096 pairing
+inequalities and 8,192 complete normalization fixtures. It checks 92 two-sided
+arithmetic cases, 69 one-sided cases and eleven controls. It prints
+an automatically generated receipt bound to the package source hashes and
+writes no files. Those finite checks do not instantiate or re-prove the
+cited E8 geometry.
+
+`SOURCES.json` pins all mathematical predecessors as historical provenance
+at canonical main `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7.
+There are no runtime dependencies on predecessor code or data. The current
+selected source-binding orientation passed; it is not a scientific replay.
+
+## Limits
+
+The cost is the sum of rational ranks of root-pairing submatrices, with the
+binary scalar factorization taken over F2. These are different fields and
+must not be interchanged. The theorem uses the full fixed 120-line matrix,
+not a punctured or masked matrix or an odd-characteristic factorization.
+The geometric premises retain their original author-checked status.
+Independent human and formal proof-kernel review are unclaimed.
+
+No shared physical delivery, dirty restoration, native caller, recursive
+invoice, supplier admission or complete multiplication theorem is supplied.
+The selected frontier is unchanged. No performance number is claimed.
+
+## Open next questions
+
+1. Can factor ranks (10,11) or (11,10) lower the cost at twelve reduced
+   terms? These are the smallest two-sided rank pairs outside the new floor.
+   Start with the three nonzero quotient cosets of the rank-eleven factor
+   and couple their deficits to the opposite factor's single-coset budget.
+   The available one-coset budget alone is insufficient.
+2. Can the rank-(9,12) case lower the cost? Start with a dimension-twelve
+   extension of the rank-nine binary code and its minimum basis support
+   cost. The cited eleven-dimensional basis theorem stops one dimension
+   short. Neither question is reserved by this package.
+
+## Credit and verification design
+
+This result was produced by Nick Petalas. Ali Romman supplies the fixed binary
+matrix, the geometric one-coset defect budget, the eleven-dimensional basis
+theorem and the open twelve-term question in #4967. conorholds' #3755 is a
+method antecedent for combining two deficiency budgets with product rank,
+over a different scalar field and with different code dimensions and prices.
+Its theorem is not substituted for the binary geometric premise.
+Joel Pulikkan / GamingPuzzled #620, DreamingOfClouds #446 and the retained
+E8, scalar-copy and root-code contributors keep their predecessor credit.
+Standard rank inequalities and merging are not claimed as new mathematics.
+
+The build-the-lever principle led to an executable normalization checker.
+The prove-it-works principle led to full operator and cost comparisons for
+each fixture, including optimized Python. Power-of-ten inspection found no
+recursion; fixture sizes bound every loop and every function is under 60
+lines. Python's managed rational/list allocation and the fixed callbacks
+used by rejection controls are deviations from rules 3 and 9. They remain
+confined to the six-line, at-most-six-by-six fixtures and the sixteen-term
+normalizer. A runtime deployment would require a separately bounded storage
+implementation. Normal and optimized replays use explicit exceptions, so
+checks are not disabled by `-O`. Warnings-as-errors is registered. No static
+type analyzer or proof-assistant build is claimed.
+
+New work is Apache-2.0.

research/e8-one-extra-direction/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/e8-small-redundancy/README.md",
+      "usage": "provenance",
+      "git_blob": "bdf0715d2b9bb15fdf48b10cbfa774360a3179f6",
+      "sha256": "ba9d62c9fcf2a9913edd7c8985d4a6aae365e4c4762551ba9d84cd06dc8c0818"
+    },
+    {
+      "path": "research/e8-small-redundancy/TEN-PROOF.md",
+      "usage": "provenance",
+      "git_blob": "d61866bfe7f7671fc656732bdee9af17ec05f425",
+      "sha256": "f3bab259f11cc14415b0d1a242e76ca8371094d7814686e7251ff5b1579fb572"
+    },
+    {
+      "path": "research/e8-small-redundancy/ELEVEN-PROOF.md",
+      "usage": "provenance",
+      "git_blob": "2a0005908b68da3e686791ae63ff6a99feb77b8c",
+      "sha256": "afa044fce728f8b5a17217a26cd51aa5261afde3065f0cd4e8c8b5c9121de302"
+    },
+    {
+      "path": "research/e8-one-coset-deficiency/README.md",
+      "usage": "provenance",
+      "git_blob": "b8d0bcd485cdcd1fd6528fc536bc2486c7ce5a2e",
+      "sha256": "3f20bd9b8dc51f7d3d05fc87398ae4a1612d5a10123a721ae2fa033f1b7838be"
+    }
+  ]
+}

research/e8-one-extra-direction/TASK.json

@@ -0,0 +1,90 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "For the fixed 120-line binary E8 matrix, prove rational pairing-rank cost at least 72 for any finite binary factorization whose actual factor-rank sum is at most 20.",
+  "scope_change_reason": "The live open twelve-term question in Ali Romman PR4967 provides a narrow structural side result. This changes the generic block-child profile task to an all-term-count algebraic obstruction; no physical supplier gain is claimed.",
+  "bottleneck_link": "A pairing-rank saving in this fixed binary factorization must add at least three total factor-space dimensions beyond the two rank-nine codes. Extra terms alone in the excluded rank classes cannot lower this algebraic cost.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first rank-based extension. Do not search the remaining rank pairs or replay predecessor geometry.",
+  "outcome": "completed",
+  "evidence": "PROOF.md, standalone exact algebra verifier, generated source-hash receipt on stdout, normal and optimized registered checks.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can twelve reduced terms at factor ranks (10,11) or (11,10) cost below 72?",
+      "why_it_matters": "These are the first two-sided factor-rank pairs beyond this theorem.",
+      "first_step": "Couple the rank-eleven quotient-coset deficits to the opposite single-coset budget.",
+      "blocked_by": "The available one-coset bound does not control their coupled costs."
+    },
+    {
+      "question": "Can a dimension-twelve binary extension of C have basis support-rank sum below 72?",
+      "why_it_matters": "This would decide the one-sided rank-(9,12) branch.",
+      "first_step": "Classify low-rank words across a three-dimensional quotient.",
+      "blocked_by": "The cited basis theorem covers dimensions at most eleven."
+    }
+  ],
+  "claim_type": "scoped proof from cited geometric premises",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144298",
+  "upstream_checkpoint": {
+    "commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+    "priority_revision": 7,
+    "checked_at_utc": "2026-10-23T11:02:40.410645+00:00"
+  },
+  "preserved_checkout": {
+    "branch": null,
+    "state": "detached HEAD",
+    "commit": "20a1e31bc6009b9b3f4d084bbaadc6350e34fcba"
+  }
+}

research/e8-one-extra-direction/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact merge and pairing rank inequalities on all supports of a six-line rational configuration; complete bounded normalization fixtures; rank-budget arithmetic and rejecting controls. Cited E8 geometry is not replayed."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Same algebra checks with assertions disabled; explicit exception-based gates remain active."
+    }
+  ]
+}