From 1fa430647d32f71a7ad20e1b2c27c1c6190abd3c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 12:06:20 +0100 Subject: [PATCH] feat(research): bound binary E8 factor ranks at every term count --- research/e8-one-extra-direction/PROOF.md | 105 +++++++++ research/e8-one-extra-direction/README.md | 99 ++++++++ research/e8-one-extra-direction/SOURCES.json | 42 ++++ research/e8-one-extra-direction/TASK.json | 90 ++++++++ research/e8-one-extra-direction/VERIFY.json | 34 +++ research/e8-one-extra-direction/verify.py | 230 +++++++++++++++++++ 6 files changed, 600 insertions(+) create mode 100644 research/e8-one-extra-direction/PROOF.md create mode 100644 research/e8-one-extra-direction/README.md create mode 100644 research/e8-one-extra-direction/SOURCES.json create mode 100644 research/e8-one-extra-direction/TASK.json create mode 100644 research/e8-one-extra-direction/VERIFY.json create mode 100644 research/e8-one-extra-direction/verify.py diff --git a/research/e8-one-extra-direction/PROOF.md b/research/e8-one-extra-direction/PROOF.md new file mode 100644 index 0000000000..0dc5a54955 --- /dev/null +++ b/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. diff --git a/research/e8-one-extra-direction/README.md b/research/e8-one-extra-direction/README.md new file mode 100644 index 0000000000..8f55b1f312 --- /dev/null +++ b/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. diff --git a/research/e8-one-extra-direction/SOURCES.json b/research/e8-one-extra-direction/SOURCES.json new file mode 100644 index 0000000000..57d972a069 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/e8-one-extra-direction/TASK.json b/research/e8-one-extra-direction/TASK.json new file mode 100644 index 0000000000..9997b67966 --- /dev/null +++ b/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" + } +} diff --git a/research/e8-one-extra-direction/VERIFY.json b/research/e8-one-extra-direction/VERIFY.json new file mode 100644 index 0000000000..571858f949 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/e8-one-extra-direction/verify.py b/research/e8-one-extra-direction/verify.py new file mode 100644 index 0000000000..28458f099b --- /dev/null +++ b/research/e8-one-extra-direction/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Check the new algebraic steps without replaying the cited E8 premises.""" + +from __future__ import annotations + +from fractions import Fraction +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def rank(rows: list[list[int]]) -> int: + """Exact rational elimination on fixtures of at most six rows/columns.""" + if not rows: + return 0 + require(len(rows) <= 6 and len(rows[0]) <= 6, "matrix capacity") + width = len(rows[0]) + require(all(len(row) == width for row in rows), "ragged matrix") + work = [[Fraction(value) for value in row] for row in rows] + pivot = 0 + for column in range(width): + candidates = [i for i in range(pivot, len(work)) if work[i][column]] + if not candidates: + continue + chosen = candidates[0] + work[pivot], work[chosen] = work[chosen], work[pivot] + scale = work[pivot][column] + work[pivot] = [value / scale for value in work[pivot]] + for i in range(pivot + 1, len(work)): + scale = work[i][column] + work[i] = [a - scale * b for a, b in zip(work[i], work[pivot])] + pivot += 1 + if pivot == len(work): + break + return pivot + + +def pairing_table() -> tuple[list[list[int]], list[int]]: + # A separate six-line rational configuration, not the E8 roots. + labels = [(1, 0, 0), (0, 1, 0), (0, 0, 1), + (1, 1, 0), (1, 0, 1), (0, 1, 1)] + supports = [[v for i, v in enumerate(labels) if mask & (1 << i)] + for mask in range(64)] + dimensions = [rank([list(v) for v in support]) for support in supports] + costs = [[rank([[sum(x * y for x, y in zip(a, b)) for b in right] + for a in left]) if left and right else 0 + for right in supports] for left in supports] + return costs, dimensions + + +def outer(a: int, b: int) -> int: + require(0 <= a < 64 and 0 <= b < 64, "support capacity") + return sum(b << (6 * i) for i in range(6) if a & (1 << i)) + + +def operator(terms: list[tuple[int, int]]) -> int: + result = 0 + for a, b in terms: + result ^= outer(a, b) + return result + + +def price(terms: list[tuple[int, int]], costs: list[list[int]]) -> int: + return sum(costs[a][b] for a, b in terms) + + +def binary_rank(masks: list[int]) -> int: + require(len(masks) <= 16, "binary rank capacity") + basis = [0] * 6 + for mask in masks: + require(0 <= mask < 64, "binary vector capacity") + remainder = mask + for bit in range(5, -1, -1): + if not remainder & (1 << bit): + continue + if basis[bit]: + remainder ^= basis[bit] + else: + basis[bit] = remainder + break + return sum(bool(row) for row in basis) + + +def normalize(terms: list[tuple[int, int]]) -> list[tuple[int, int]]: + """Delete zeros and merge one equal-column pair per bounded pass.""" + require(len(terms) <= 16, "normalization capacity") + current = list(terms) + for _ in range(len(terms) + 1): + current = [(a, b) for a, b in current if a and b] + replacement = None + for i, (a, b) in enumerate(current): + for j in range(i + 1, len(current)): + c, d = current[j] + if a == c: + replacement = (i, j, (a, b ^ d)) + break + if b == d: + replacement = (i, j, (a ^ c, b)) + break + if replacement is not None: + break + if replacement is None: + return current + i, j, merged = replacement + current = [term for k, term in enumerate(current) if k not in (i, j)] + current.append(merged) + raise ValueError("normalization did not decrease term count") + + +def check_pairings(costs: list[list[int]], dimensions: list[int]) -> dict: + merge_cases = 0 + for a, b, c in product(range(64), repeat=3): + require(costs[a][b ^ c] <= costs[a][b] + costs[a][c], "merge rank") + merge_cases += 1 + pairing_cases = 0 + for a, b in product(range(64), repeat=2): + require(costs[a][b] == costs[b][a], "transpose") + require(costs[a][b] >= dimensions[a] + dimensions[b] - 3, + "nondegenerate pairing bound") + pairing_cases += 1 + return {"merge_inequalities": merge_cases, "pairing_inequalities": pairing_cases} + + +def check_normalization(costs: list[list[int]]) -> int: + count = 0 + for alphabet, length in ((8, 2), (4, 3)): + for flat in product(range(alphabet), repeat=2 * length): + terms = list(zip(flat[::2], flat[1::2])) + reduced = normalize(terms) + require(operator(terms) == operator(reduced), "changed binary product") + require(price(reduced, costs) <= price(terms, costs), "increased price") + require(len({a for a, _ in reduced}) == len(reduced), "left repeats") + require(len({b for _, b in reduced}) == len(reduced), "right repeats") + require(all(a and b for a, b in reduced), "zero retained") + for side in (0, 1): + require(binary_rank([term[side] for term in reduced]) <= + binary_rank([term[side] for term in terms]), "rank increased") + r_left = binary_rank([a for a, _ in terms]) + r_right = binary_rank([b for _, b in terms]) + rows = [(operator(terms) >> (6 * i)) & 63 for i in range(6)] + require(binary_rank(rows) >= r_left + r_right - length, + "binary product-rank inequality") + count += 1 + return count + + +def floor_from_budgets(left_excess: int, right_excess: int, count: int) -> int: + require(left_excess in (0, 1) and right_excess in (0, 1), "excess scope") + require(count >= 9 + left_excess + right_excess, "product rank") + return 8 * count - 8 * left_excess - 8 * right_excess + + +def check_arithmetic() -> dict: + cases = 0 + for left_excess, right_excess in product(range(2), repeat=2): + start = 9 + left_excess + right_excess + require(floor_from_budgets(left_excess, right_excess, start) == 72, + "sharp arithmetic endpoint") + for count in range(start, 33): + require(floor_from_budgets(left_excess, right_excess, count) >= 72, + "rank-pair floor") + cases += 1 + require(floor_from_budgets(1, 1, 12) == 80, "twelve-term rank-(10,10)") + one_sided = 0 + for other_rank in (9, 10, 11): + for count in range(other_rank, 33): + require(72 + count - other_rank >= 72, "basis selection") + one_sided += 1 + return {"arithmetic_cases": cases, "one_sided_cases": one_sided} + + +def expect_rejected(action, name: str) -> None: + try: + action() + except ValueError: + return + raise ValueError("control was accepted: " + name) + + +def check_controls(costs: list[list[int]]) -> int: + invalid = [ + (lambda: floor_from_budgets(2, 0, 11), "two extra directions"), + (lambda: floor_from_budgets(1, 1, 10), "missing product rank"), + (lambda: normalize([(1, 1)] * 17), "unbounded fixture"), + (lambda: outer(64, 1), "oversize support"), + (lambda: rank([[1], [1, 2]]), "ragged matrix"), + (lambda: binary_rank([1] * 17), "binary rank capacity"), + (lambda: binary_rank([64]), "binary vector capacity"), + ] + count = 0 + for action, name in invalid: + expect_rejected(action, name) + count += 1 + counterexamples = [ + (operator([(1, 1), (1, 1)]) != operator([(1, 1 | 1)]), "OR mutant"), + (price([(1, 1), (1, 1)], costs) > price([], costs), "zero cost mutant"), + (floor_from_budgets(1, 1, 11) < 80, "overstated eighty floor"), + (2 * (8 - 1) > 8 and normalize([(1, 1), (1, 1)]) == [], "distinctness"), + ] + for condition, name in counterexamples: + require(condition, name) + count += 1 + return count + + +def main() -> None: + costs, dimensions = pairing_table() + receipt = check_pairings(costs, dimensions) + receipt["normalization_cases"] = check_normalization(costs) + receipt.update(check_arithmetic()) + receipt["controls"] = check_controls(costs) + receipt["claim_type"] = "scoped proof from cited E8 premises" + receipt["predecessor_geometry_replayed"] = False + package = Path(__file__).resolve().parent + receipt["source_sha256"] = { + name: sha256((package / name).read_bytes()).hexdigest() + for name in ("verify.py", "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json") + } + print(json.dumps(receipt, sort_keys=True)) + print("PASS_E8_ONE_EXTRA_DIRECTION factor_rank_sum<=20 pairing_floor=72") + + +if __name__ == "__main__": + main()