From 5950e7896b8825a2c167ee63836251b3096060f8 Mon Sep 17 00:00:00 2001 From: Jose Manuel <118126596+jmbarrancoml@users.noreply.github.com> Date: Wed, 14 Oct 2026 19:12:16 +0200 Subject: [PATCH] Prove sharp pairing cost for Eisenstein binary decoders --- .../eisenstein-reduction-copy-floor/README.md | 274 +++++++++++++++ .../SOURCES.json | 22 ++ .../eisenstein-reduction-copy-floor/TASK.json | 35 ++ .../VERIFY.json | 14 + .../eisenstein-reduction-copy-floor/verify.py | 318 ++++++++++++++++++ 5 files changed, 663 insertions(+) create mode 100644 research/eisenstein-reduction-copy-floor/README.md create mode 100644 research/eisenstein-reduction-copy-floor/SOURCES.json create mode 100644 research/eisenstein-reduction-copy-floor/TASK.json create mode 100644 research/eisenstein-reduction-copy-floor/VERIFY.json create mode 100644 research/eisenstein-reduction-copy-floor/verify.py diff --git a/research/eisenstein-reduction-copy-floor/README.md b/research/eisenstein-reduction-copy-floor/README.md new file mode 100644 index 0000000000..ebf030c259 --- /dev/null +++ b/research/eisenstein-reduction-copy-floor/README.md @@ -0,0 +1,274 @@ +# Sharp pairing cost for binary decoders on the 40 Eisenstein lines + +We prove **C >= 40** for the scalar rectangle model in Jonathan Lam's +[PR #798](https://github.com/CrocSwap/integer-mult-bounds/pull/798), and use +his row-star construction to attain equality. We allow arbitrary supports, +asymmetric readers and sources, any finite number of terms, and XOR +cancellations. We do not require clean rectangles or a minimum-rank decoder. + +We obtain the lower bound by reducing a normalized Hermitian Gram matrix +modulo 2 and applying rank subadditivity to a Hadamard product. DreamingOfClouds +used the same-field rank argument in Lemma B of +[PR #1590](https://github.com/CrocSwap/integer-mult-bounds/pull/1590). +We add the good-reduction certificate and pairing-rank comparison for this +Eisenstein geometry. With these steps, we close +the scalar cost interval left by the floor 22 in #798, the floor 23 in +[PR #1977](https://github.com/CrocSwap/integer-mult-bounds/pull/1977), and +the non-clean cost screen in +[PR #1794](https://github.com/CrocSwap/integer-mult-bounds/pull/1794). +We retain the selected multiplication exponent. + +## Exact model + +Use the 240 doubled E8 roots and the order-three orthogonal action J from +Joel Pulikkan / GamingPuzzled's PR #620, as reconstructed by Jonathan Lam +in `research/eisenstein-clique-copy-bound/geometry.py`. We pin that file in +`SOURCES.json`. Its six-root orbits under +/-J give 40 lines over +K = Q(omega), where omega^2 + omega + 1 = 0 and multiplication by omega +acts as J. Write r_i for a representative of line i. + +For a set S of lines, write X_S for the rational span of r_i and Jr_i. +For any rational row bases V_R and V_A of X_R and X_A, define + + c(R,A) = rank_Q(V_R V_A^T)/2. + +Choose any binary matrix B satisfying + + B_ii = 1; + B_ij = 0 when i != j and lines i,j are nonorthogonal. + +The entries at orthogonal pairs may differ in the two directions. Choose +any finite decomposition over F2, + + B = sum_j 1_Rj 1_Aj^T, + C = sum_j c(R_j,A_j). + +**Theorem.** For every such B and decomposition, C >= 40. For each fitting +B, a row-star decomposition has C = 40. Thus each fitting B has minimum +abstract cost 40, regardless of its binary rank. + +We prove a finite algebraic statement. A researcher who interprets C as a +physical COPY charge must establish the corresponding implementation +premise. We do not establish the unreviewed physical premise that earlier +authors traced to PR #446. + +## Proof + +### 1. An integral Hermitian Gram matrix at the prime 2 + +For x,y in Q^8, put d0 = x dot y and d1 = x dot Jy. Define + + h(x,y) = (d0 - d1 - omega*(d0 + 2*d1))/12. + +Using J^2+J+I = 0 and orthogonality of J, we obtain + + h(x,Jy) = omega*h(x,y), + h(Jx,y) = conjugate(omega)*h(x,y), + h(y,x) = conjugate(h(x,y)), + x dot y = 4*Tr_(K/Q)(h(x,y)). + +Thus we may regard h as a Hermitian form on the four-dimensional K-space. +For a root r, we have r dot r = 8 and r dot Jr = -4, hence h(r,r) = 1. +Two lines are orthogonal exactly when both d0 and d1 vanish, which is +equivalent to h(r_i,r_j) = 0. + +Write H_ij = h(r_i,r_j). The doubled-root inner products d0 and d1 are +multiples of 4, including after J permutes the roots. Therefore + + H_ij in S = Z[omega,1/3]. + +We can reduce S modulo 2. Since t^2+t+1 is irreducible over F2, we obtain +S/(2) = F4. Write Hbar for the entrywise reduction. We retain the diagonal +ones and the zeros at orthogonal pairs. We do not need to assume that a +nonzero off-diagonal entry stays nonzero, although the finite replay also +checks that property for this geometry. + +We reduce this fixed Gram matrix. We never reduce an arbitrary rational +row basis, whose denominators might include 2. + +### 2. Pairing cost bounds the reduced submatrix rank + +We first identify + + rank_K H[R,A] = c(R,A). + +The representatives r_i span X_R and X_A over K. A vector x in X_R +annihilates the rational pairing with X_A exactly when h(x,y) = 0 for +all y in X_A. Indeed, rational annihilation gives both +Tr(h(x,y)) = 0 and Tr(omega*h(x,y)) = 0, because Jy also lies in X_A. +For z=a+b*omega these two traces are 2a-b and -a-b; over Q their joint +vanishing forces a=b=0. The converse follows from the trace formula. +We have therefore identified the two radicals. Their K-dimensions are +half their rational dimensions, proving the rank equality. + +Next, if rank_K H[R,A] = c, every (c+1)-minor vanishes in K. Each minor +lies in S, a subring of K, so it vanishes in S and after reduction to F4. +Consequently + + rank_F4 Hbar[R,A] <= rank_K H[R,A] = c(R,A). (1) + +This proof covers arbitrary line subsets, including empty sets. We do not +need to enumerate flats or assume nonsingular restricted spans. + +### 3. The fitting identity forces total rank 40 + +Embed B and its binary decomposition in F4. Denote the entrywise product +by "o". The fitting conditions and the Gram zeros give + + Hbar o B = I_40. + +Distributing over the rectangle sum gives + + I_40 = sum_j diag(1_Rj) Hbar diag(1_Aj). + +The j-th summand has rank rank_F4 Hbar[R_j,A_j]. Rank subadditivity and +(1) imply + + 40 <= sum_j rank_F4 Hbar[R_j,A_j] <= C. + +The equality before the rank estimate holds in characteristic two, so we +have included overlapping supports and XOR cancellations. + +For the matching upper bound, decompose B by rows. In row i choose +R_i={i} and A_i={j:B_ij=1}. The set A_i contains i and otherwise contains +only lines orthogonal to i. Hence H[{i},A_i] has one nonzero entry and +rank one. The 40 rows give C=40. This construction and its cost already +appear in #798; our contribution is the matching lower bound. + +### 4. Binary minrank and minimum-rank support rigidity + +We also recover the known binary minrank 10 without a SAT premise. If B +has binary rank h, factor it into h binary rank-one matrices. Each support +pair costs at most four, since K has ambient dimension four. The theorem +gives 40 <= 4h, hence h >= 10. The known partition into ten orthogonal +four-frames attains h=10: put an all-ones block on each frame. We replay a +literal partition and verify its fitting conditions and rank. + +If B has rank 10, every nonzero vector in its row space and every nonzero +vector in its column space has support spanning the full four-dimensional +K-space. For example, suppose a row-space vector had support of K-rank +at most three. Extend it to a binary row-space basis. The resulting +ten-term factorization would cost at most 3+9*4=39, a contradiction. +Use a column-space basis for the other assertion. Thus a researcher +cannot build a rank-10 decoder from even one hyperplane-supported basis +vector, regardless of the other nine basis vectors. + +## Fixed-support block-linear corollary + +Suppose port t holds an independent b_t-bit vector. Message j consists of +q_j fixed binary linear forms in the inputs at A_j, and each receiver in +R_j receives that message. Receiver t also knows the full inputs at ports +orthogonal to t. Assume exact recovery on every input and the additive +pricing premise + + C = sum_j q_j*c(R_j,A_j). + +Then **C >= sum_t b_t**, with equality from direct messages. In particular, +block-linear coding at equal demand b costs at least 40b. + +To prove this, choose a linear recovery map for each demanded bit. Such a +map exists even if the declared decoder was nonlinear: exact recovery of +a linear coordinate from linear observations means that the observation +kernel lies in the coordinate kernel. The coordinate therefore belongs +to the observation row space. + +Stacking these maps gives a block matrix B=sum_j D_j E_j over F2, with +diagonal blocks I_(b_t) and zero blocks at distinct nonorthogonal ports. +Here D_j has q_j columns, E_j has q_j rows, and their nonzero port blocks +lie in R_j and A_j. Lift Hbar by replacing Hbar_st with the constant +b_s by b_t block of that value. Call the resulting matrix G. Then + + G o B = I_(sum_t b_t). + +Expand D_j E_j into its q_j rank-one terms. Each term after entrywise +multiplication has rank at most rank_F4 Hbar[R_j,A_j]: repeating rows and +columns to form G does not increase rank, and diagonal weighting cannot +increase it. Sum these bounds and apply (1). + +We have not extended this argument to nonlinear encoders. The earlier +Michael Fischler's `eisenstein-message-copy-bound` package treats a broader nonlinear message +model and proves a different lower bound. We leave its nonlinear claims +and their attribution unchanged. Adaptive supports and pricing shared +physical work below the declared additive charge also remain outside our +theorem. + +## Consequences and limits + +Under the specific accounting in Maximooch's #1794 screen, a supplier +that beats the selected construction would need C <= 31, or C <= 29 at +window h=10. Our lower bound excludes those costs for the stated scalar +model. We do not rerun that screen here; we pin its incorporated receipt +as provenance and state this consequence conditional on its accounting. +The proof C=40 does not depend on the screen or the selected exponent. + +The ten-source proposal that motivated this check also fails. If each +source lies in one orthogonal 12-line hyperplane, each term costs at most +three. Ten such terms would cost at most 30, contradicting the theorem, +even with unrestricted asymmetric reader sets. + +Researchers can still change the geometry, scalar field, support model, +message nonlinearity, or physical pricing premise. We have not proved a +barrier for arbitrary integer multiplication algorithms or for the native +paired-log constructions that motivated our separate investigation. + +## Reproduction and evidence + +Run from the repository root with Python 3.12 and its standard library: + +```sh +python3.12 scripts/research_package.py --package research/eisenstein-reduction-copy-floor +``` + +For a direct replay under an optimized interpreter: + +```sh +python3 -I -O -B research/eisenstein-reduction-copy-floor/verify.py +``` + +We reconstruct the pinned geometry, check all 1,600 Hermitian entries, +6,400 rational trace identities, the quotient-field arithmetic, and all +Gram-value reduction identities. We also compare rational, K and F4 +ranks on 209 boundary or deterministic sample blocks, check 40 hyperplane +column ranks, and replay two cost-40 row-star witnesses plus a non-clean +cost-48 cancellation witness. We verify the rank-10 frame partition, a +two-bit sharp frame code and 16 mixed-bit block estimates. Seven corruption +controls exercise diagonal, orthogonality, fitting, demand, denominator +and per-bit pricing assumptions. Acceptance +checks use explicit exceptions and remain active under `-O`. + +The sample rank comparisons corroborate the proof in Section 2. We use +the radical and minor arguments there to cover arbitrary supports; we do +not infer that universal statement from samples. We claim a written proof +with exact finite checks, without proof-assistant formalization. + +## Open next questions + +- Can nonlinear encoding lower cost below 40b under the fixed-support, + per-bit pairing charge? A researcher can start with one orthogonal + frame and one non-clean message, then test exact decoding and compare + with the existing nonlinear floor. The Schur-rank proof requires linear + encoders, so it leaves this question open. +- Can a native supplier share physical work across messages and escape + the additive pairing charge? A researcher must specify a complete + source/reader/frame contract and price one small instance. We do not + have such a contract, and a cheaper abstract rectangle search within + the present model cannot supply one. + +## Attribution + +Jose Manuel (@jmbarrancoml), with substantial OpenAI Codex assistance in +the proof, implementation and prose. A read-only mathematical agent +identified the reduction argument during a ten-source construction +search; the primary agent derived the trace/rank proof and implemented +the replay. We have not obtained independent human review. + +Joel Pulikkan / GamingPuzzled (#620) supplied the Eisenstein geometry. +Jonathan Lam (#798) supplied the exact pairing-cost model, geometry code, +floor 22 and row-star upper bound. Josie Elliston (#1977) obtained floor +23 by principal-submatrix minrank, and Maximooch (#1794) derived the +cost screen and the clean-class floor. DreamingOfClouds (#1590, Lemma B) +gave the same-field Hadamard rank argument for another decoder model. +Michael Fischler (@shiftybitshiftr) treated fixed-support nonlinear messages +in `eisenstein-message-copy-bound`. We use standard specialization and +trace-pairing arguments with the Hadamard bound to obtain the sharp cost. +We preserve their packages and licenses. See `SOURCES.json` for exact pins. diff --git a/research/eisenstein-reduction-copy-floor/SOURCES.json b/research/eisenstein-reduction-copy-floor/SOURCES.json new file mode 100644 index 0000000000..8d82a50d1a --- /dev/null +++ b/research/eisenstein-reduction-copy-floor/SOURCES.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "base_commit": "ec8707299e2f40918f5f96cdab99ee49cdbabcf0", + "files": [ + {"path": "docs/research/agent-task-catalog.json", "usage": "provenance", "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075"}, + {"path": "certificates/selected-result.json", "usage": "provenance", "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"}, + {"path": "research/eisenstein-clique-copy-bound/geometry.py", "usage": "input", "git_blob": "a92c16295d6fcf2a7ffeb7d38444613f939db6cb", "sha256": "248df3fb820b5165ca485ad4d43f0271043498c45a59ac1edc310a124073644c"}, + {"path": "research/eisenstein-clique-copy-bound/PROOF.md", "usage": "provenance", "git_blob": "5c5fd2f87ce3c4e61ed782ceaa623edd80811349", "sha256": "b75539c196ed45f23cf238413da9684dcba503f6630ad68a9648ecacf6aada3f"}, + {"path": "research/root-unit-decoder-lemmas/README.md", "usage": "provenance", "git_blob": "de305484c78226a3f8da5f3277ced78974116fbb", "sha256": "e3c856bc361a57cc2424c829001dba94e8f3a1bc8f6616f9c2f740e9665506a9"}, + {"path": "research/eisenstein-message-copy-bound/PROOF.md", "usage": "provenance", "git_blob": "86d6e25ed60488646c0316a2c930e1f9e3ade99a", "sha256": "dd8c7890d661ae87167d038d12356845470a2822733c45bd9ab4c9208e381311"}, + {"path": "research/community-efficient800-audit/packets/1794.json", "usage": "provenance", "git_blob": "b2adeb6260dee3d54f4443e2c652afc5a26298f6", "sha256": "3d621a1676fd13d893e1e9033a1aff7c131fb85a598ac8891d1018d4be03dccb"} + ], + "predecessors": [ + {"author": "Joel Pulikkan / GamingPuzzled", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/620", "source_head": "419c7374c3bf5f2eee28f08b1e50c1d57934081c", "scope": "Eisenstein E8 geometry and the prior ten-frame construction; this archived source head is identified in PR798's SOURCES.json."}, + {"author": "Jonathan Lam (@jonathanlam)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/798", "head": "0aea3382e49abd9a59d3cb6676cdb26fd15b04e5", "scope": "Exact pairing-cost model, imported geometry code, clique floor 22 and matching row-star upper bound 40."}, + {"author": "DreamingOfClouds", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1590", "head": "08e134b4a0c7f04869dae703f2a2e688e53c44f0", "scope": "Lemma B: same-field Hadamard-product rank argument for another decoder model. We add the Eisenstein good-reduction and pairing-rank bridge."}, + {"author": "Maximooch", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1794", "head": "148762722bb39c7ce2fd3fd0d42ef25d945aae4d", "scope": "Certified necessary cost screen and clean-class cost 40; contextual consequence only, not executed or required for the sharp theorem."}, + {"author": "Josie Elliston (@JosieElliston)", "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1977", "head": "ea021c002e61fea7f2f9cd1b613f65b88f7eb7e9", "readme_git_blob": "1c4f3f947f3bf4047215ca1b14a3fc84f3e72d49", "readme_sha256": "63324a1bda6445fad12e5d68a0a34a88729980cca3cd8f87f44bfb19d7a6f19f", "scope": "Principal-submatrix floor 23 and the remaining non-clean interval; no code imported."}, + {"author": "Michael Fischler (@shiftybitshiftr)", "path": "research/eisenstein-message-copy-bound/PROOF.md", "scope": "Fixed-support nonlinear message model and per-bit pairing pricing. Our block-linear corollary leaves nonlinear encoders open."} + ], + "attribution": "The new result is the sharp cost bound from the normalized Eisenstein Gram matrix, its good reduction at 2 and the pairing-rank conversion. Rank subadditivity, minor specialization and trace-pairing arguments are standard. We retain predecessor files and notices unchanged." +} diff --git a/research/eisenstein-reduction-copy-floor/TASK.json b/research/eisenstein-reduction-copy-floor/TASK.json new file mode 100644 index 0000000000..1637f53210 --- /dev/null +++ b/research/eisenstein-reduction-copy-floor/TASK.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 3, + "base_commit": "ec8707299e2f40918f5f96cdab99ee49cdbabcf0", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": ["research/complex-local-word-ceiling/README.md", "research/heterogeneous-owner-assembly/README.md", "certificates/selected-result.json"], + "methods": ["Propose a changed helper inventory and derive an optimistic exact moment.", "Design a small completed instance and independently verify its endpoint and rank bill."], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model.", + "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.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": ["Narrow to one changed boundary or helper type with explicit counts.", "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": ["Mixing only providers already inside the pinned catalogue."], + "overlap_terms": ["helper inventory", "heterogeneous-owner", "mutable leaver"] + }, + "scope_status": "changed", + "actual_scope": "Sharp abstract cost 40 for all binary scalar rectangle decoders on the 40 Eisenstein lines, with a fixed-support block-linear corollary.", + "scope_change_reason": "We investigated ten source-basis vectors supported in orthogonal hyperplanes, which would have cost at most 30. A good-reduction rank argument excludes that candidate and proves the stronger sharp floor for arbitrary supports. This is a scoped obstruction rather than a positive native supplier.", + "bottleneck_link": "The inherited Eisenstein screen needs cost at most 31 to beat the selected supplier. The theorem excludes that interval under its scalar pairing charge and identifies hypotheses a successor must change.", + "budget_minutes": 120, + "stop_rule": "Finish the sharp proof, exact arithmetic replay, predecessor pins and focused PR; retain the broader constructive research goal.", + "outcome": "negative-result", + "evidence": "Good reduction of the normalized Hermitian Gram matrix to F4; universal minor and Hadamard-rank proof; matching row-star upper bound; binary minrank-10 witness; block-linear corollary; explicit corruption controls.", + "author": "Jose Manuel (@jmbarrancoml)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, implementation and prose. A read-only mathematical agent identified the good-reduction argument; the primary agent derived the trace/rank proof and implemented the replay. No independent human review.", + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18930017", + "overlap": "Live refresh at 2026-10-14 17:05:32 UTC covered 381 open PRs, 646 Discussion records and 1381 local records, with complete remote pagination and no warnings. We inspected current PRs 1794 and 1977 and credited the same-field Hadamard argument from PR1590. Search coverage does not establish novelty.", + "open_questions": [ + {"question": "Can nonlinear encoding beat 40b under fixed-support per-bit pairing charges?", "why_it_matters": "The proof strengthens the linear subclass but does not settle the broader nonlinear message model.", "first_step": "Test an exact code on one orthogonal frame plus one non-clean message against the existing nonlinear lower bound.", "blocked_by": "The Hadamard factorization requires linear message encoders."}, + {"question": "Can a native supplier share physical work below the additive pairing charge?", "why_it_matters": "The theorem concerns an abstract price; a different physical contract could escape its hypotheses.", "first_step": "Specify and price a small complete source, reader and frame contract with dirty-state restoration.", "blocked_by": "No such native contract follows from this proof."} + ] +} diff --git a/research/eisenstein-reduction-copy-floor/VERIFY.json b/research/eisenstein-reduction-copy-floor/VERIFY.json new file mode 100644 index 0000000000..0a486b4d55 --- /dev/null +++ b/research/eisenstein-reduction-copy-floor/VERIFY.json @@ -0,0 +1,14 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": ["research/eisenstein-clique-copy-bound/geometry.py"], + "commands": [ + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Pinned geometry; 1600 Hermitian entries; 6400 trace identities; reduction homomorphism; rational/K/F4 rank comparisons; matching scalar and block-linear witnesses; minrank-10 partition; seven rejected assumption corruptions. Universal coverage follows from the written radical, minor and Hadamard-rank proof." + } + ] +} diff --git a/research/eisenstein-reduction-copy-floor/verify.py b/research/eisenstein-reduction-copy-floor/verify.py new file mode 100644 index 0000000000..25e47be9a6 --- /dev/null +++ b/research/eisenstein-reduction-copy-floor/verify.py @@ -0,0 +1,318 @@ +"""Exact good-reduction premises for the Eisenstein scalar copy-cost theorem. + +Jose Manuel (@jmbarrancoml), with substantial OpenAI Codex assistance. +Apache-2.0. Geometry: Jonathan Lam, following Joel Pulikkan / GamingPuzzled. +""" + +from fractions import Fraction as F +from hashlib import sha256 +import importlib.util +from itertools import combinations +import json +from pathlib import Path +from random import Random + + +ROOT = Path(__file__).resolve().parents[2] +GEOMETRY = ROOT / "research/eisenstein-clique-copy-bound/geometry.py" +GEOMETRY_SHA = "248df3fb820b5165ca485ad4d43f0271043498c45a59ac1edc310a124073644c" +ZERO = (F(0), F(0)) +ONE = (F(1), F(0)) +OMEGA = (F(0), F(1)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def add(x, y): + return x[0] + y[0], x[1] + y[1] + + +def neg(x): + return -x[0], -x[1] + + +def mul(x, y): + a, b = x + c, d = y + return a * c - b * d, a * d + b * c - b * d + + +def conjugate(x): + return x[0] - x[1], -x[1] + + +def inverse(x): + a, b = x + norm = a * a - a * b + b * b + require(norm != 0, "inverse of zero") + c, d = conjugate(x) + return c / norm, d / norm + + +def trace(x): + return 2 * x[0] - x[1] + + +def fmul(x, y): + a, b, c, d = x & 1, x >> 1, y & 1, y >> 1 + return (a * c ^ b * d) | ((a * d ^ b * c ^ b * d) << 1) + + +def reduce_mod2(x): + require(all(t.denominator % 2 for t in x), "even denominator") + return (x[0].numerator & 1) | ((x[1].numerator & 1) << 1) + + +def rank(matrix, field="K"): + """Elimination over K, F4, or Q; no numerical tolerance.""" + if not matrix or not matrix[0]: + return 0 + if field == "K": + zero, plus, times, minus, inv = ZERO, add, mul, neg, inverse + elif field == "F4": + zero, plus, times, minus = 0, lambda a, b: a ^ b, fmul, lambda a: a + inv = lambda a: fmul(a, a) + else: + zero, plus = F(0), lambda a, b: a + b + times, minus, inv = lambda a, b: a * b, lambda a: -a, lambda a: 1 / a + rows = [list(row) for row in matrix] + pivot = 0 + for col in range(len(rows[0])): + found = next((i for i in range(pivot, len(rows)) if rows[i][col] != zero), None) + if found is None: + continue + rows[pivot], rows[found] = rows[found], rows[pivot] + scale = inv(rows[pivot][col]) + rows[pivot] = [times(x, scale) for x in rows[pivot]] + for i in range(pivot + 1, len(rows)): + factor = rows[i][col] + if factor != zero: + rows[i] = [plus(x, minus(times(factor, y))) + for x, y in zip(rows[i], rows[pivot])] + pivot += 1 + if pivot == len(rows): + break + return pivot + + +def gram(x, y, jy): + d0 = sum(a * b for a, b in zip(x, y)) + d1 = sum(a * b for a, b in zip(x, jy)) + require(d0 % 4 == d1 % 4 == 0, "root dot divisibility") + return F(d0 - d1, 12), F(-d0 - 2 * d1, 12) + + +def submatrix(matrix, rows, cols): + return [[matrix[i][j] for j in cols] for i in rows] + + +def check_witness(matrix, adjacent): + n = len(matrix) + for i in range(n): + require(matrix[i][i] == 1, "fitting diagonal") + for j in range(n): + require(matrix[i][j] in (0, 1), "binary fitting entry") + require(not ((adjacent[i] >> j) & 1) or matrix[i][j] == 0, + "forbidden nonorthogonal entry") + + +def check_hadamard(hbar, matrix): + require(all(fmul(hbar[i][j], matrix[i][j]) == int(i == j) + for i in range(len(matrix)) for j in range(len(matrix))), + "Hadamard identity") + + +def expect_rejection(call, label): + try: + call() + except ValueError: + return label + raise ValueError("negative control accepted: " + label) + + +def main(): + require(sha256(GEOMETRY.read_bytes()).hexdigest() == GEOMETRY_SHA, "geometry pin") + spec = importlib.util.spec_from_file_location("pinned_eisenstein_geometry", GEOMETRY) + geometry = importlib.util.module_from_spec(spec) + spec.loader.exec_module(geometry) + reps, images, adjacent, pairs, orbits = geometry.geometry() + n = len(reps) + require(n == 40, "line count") + h = [[gram(x, y, jy) for y, jy in zip(reps, images)] for x in reps] + hbar = [[reduce_mod2(x) for x in row] for row in h] + # Check the complete rational trace realization, including the J rows. + trace_entries = 0 + for i in range(n): + for j in range(n): + value = h[i][j] + require(all(t.denominator in (1, 3) for t in value), "localized Gram") + require(h[j][i] == conjugate(value), "Hermitian symmetry") + require((value == ZERO) == (i != j and not ((adjacent[i] >> j) & 1)), + "Gram orthogonality pattern") + require(hbar[i][j] != 0 if i == j or ((adjacent[i] >> j) & 1) else hbar[i][j] == 0, + "reduced orthogonality pattern") + for a, x in enumerate((reps[i], images[i])): + for b, y in enumerate((reps[j], images[j])): + factor = ONE + if a: + factor = mul(factor, conjugate(OMEGA)) + if b: + factor = mul(factor, OMEGA) + require(4 * trace(mul(factor, value)) == geometry.dot(x, y), + "trace pairing realization") + trace_entries += 1 + require(h[i][i] == ONE and hbar[i][i] == 1, "unit diagonal") + require(rank(h) == rank(hbar, "F4") == 4, "full Hermitian rank") + # Check the quotient field and the reduction homomorphism on all Gram values. + for a in range(4): + if a: + require(fmul(a, fmul(a, a)) == 1, "F4 inverse") + for b in range(4): + for c in range(4): + require(fmul(fmul(a, b), c) == fmul(a, fmul(b, c)), "F4 associativity") + require(fmul(a, b ^ c) == (fmul(a, b) ^ fmul(a, c)), "F4 distributivity") + values = set(x for row in h for x in row) + for x in values: + for y in values: + require(reduce_mod2(add(x, y)) == reduce_mod2(x) ^ reduce_mod2(y), "reduction sum") + require(reduce_mod2(mul(x, y)) == fmul(reduce_mod2(x), reduce_mod2(y)), "reduction product") + + # These samples corroborate the universal radical/minor argument in README. + # Neither finite sampling nor a flat census replaces that argument. + rng = Random(20261014) + supports = [[], [0], list(range(n))] + supports += [[j for j in range(n) if j != i and not ((adjacent[i] >> j) & 1)] + for i in range(n)] + require(all(len(s) == 12 for s in supports[3:]), "orthogonal hyperplanes") + for support in supports[3:]: + require(rank(submatrix(hbar, list(range(n)), support), "F4") == 3, + "hyperplane column rank") + pairs_to_check = [(supports[i], supports[j]) for i in range(3) for j in range(len(supports))] + pairs_to_check += [(rng.sample(range(n), rng.randrange(1, 13)), + rng.sample(range(n), rng.randrange(1, 13))) for _ in range(80)] + for r, a in pairs_to_check: + kernel_rank = rank(submatrix(h, r, a)) + residue_rank = rank(submatrix(hbar, r, a), "F4") + vr = [x for i in r for x in (reps[i], images[i])] + va = [x for i in a for x in (reps[i], images[i])] + rational_gram = [[F(geometry.dot(x, y)) for y in va] for x in vr] + require(rank(rational_gram, "Q") == 2 * kernel_rank, "pairing rank conversion") + require(residue_rank <= kernel_rank, "minor specialization rank") + + # Two fitting matrices: identity and the dense directed orthogonal pattern. + identity = [[int(i == j) for j in range(n)] for i in range(n)] + fitting = [[int(i == j or not ((adjacent[i] >> j) & 1)) for j in range(n)] + for i in range(n)] + for matrix in (identity, fitting): + check_witness(matrix, adjacent) + check_hadamard(hbar, matrix) + cost = 0 + for i, row in enumerate(matrix): + source = [j for j, value in enumerate(row) if value] + cost += rank(submatrix(h, [i], source)) + require(cost == 40, "row-star upper bound") + # Cancelling full rectangles exercise non-clean decompositions and parity. + rectangles = [([i], [j for j, x in enumerate(row) if x]) for i, row in enumerate(fitting)] + rectangles += [(list(range(n)), list(range(n)))] * 2 + reconstructed = [[0] * n for _ in range(n)] + schur_sum = [[0] * n for _ in range(n)] + cost = residue_cost = 0 + for r, a in rectangles: + cost += rank(submatrix(h, r, a)) + residue_cost += rank(submatrix(hbar, r, a), "F4") + for i in r: + for j in a: + reconstructed[i][j] ^= 1 + schur_sum[i][j] ^= hbar[i][j] + require(reconstructed == fitting and schur_sum == identity, "XOR rectangle identity") + require(cost == residue_cost == 48, "non-clean cancellation cost") + + # The known ten-frame construction attains binary rank ten and cost forty. + partition = [(0, 28, 29, 39), (1, 22, 23, 38), (2, 16, 17, 37), + (9, 10, 11, 36), (3, 15, 26, 32), (5, 12, 24, 35), + (7, 14, 21, 34), (4, 18, 25, 31), (6, 19, 20, 33), + (8, 13, 27, 30)] + require(sorted(i for frame in partition for i in frame) == list(range(n)), "frame partition") + frame_b = [[0] * n for _ in range(n)] + for frame in partition: + require(all(not ((adjacent[i] >> j) & 1) for i, j in combinations(frame, 2)), + "orthogonal frame") + require(rank(submatrix(h, frame, frame)) == 4, "frame rank") + for i in frame: + for j in frame: + frame_b[i][j] = 1 + check_witness(frame_b, adjacent) + check_hadamard(hbar, frame_b) + # Field extension preserves the rank of a binary matrix, so F4 suffices. + require(rank(frame_b, "F4") == 10, "minrank upper witness") + + # A two-bit message on an orthogonal frame attains the block-linear bound. + # Mix its two parity channels, then undo that mix at each receiver. + frame = next(s for s in combinations(range(n), 4) + if all(not ((adjacent[i] >> j) & 1) for i, j in combinations(s, 2))) + frame_cost = rank(submatrix(h, frame, frame)) + require(frame_cost == 4, "orthogonal frame cost") + encoder = [[int(k % 2 == 0) for k in range(8)], [1] * 8] + decoder = [[1, 0] if k % 2 == 0 else [1, 1] for k in range(8)] + block_b = [[sum(decoder[i][a] * encoder[a][j] for a in range(2)) % 2 + for j in range(8)] for i in range(8)] + lifted = [[hbar[frame[i // 2]][frame[j // 2]] for j in range(8)] for i in range(8)] + product = [[fmul(lifted[i][j], block_b[i][j]) for j in range(8)] for i in range(8)] + require(product == [[int(i == j) for j in range(8)] for i in range(8)], + "block-linear recovery identity") + require(rank(product, "F4") == 2 * frame_cost == 8, "block-linear sharp cost") + # Test the q*c estimate on asymmetric, overlapping, mixed-bit block maps. + block_samples = 16 + for _ in range(block_samples): + r, a = rng.sample(range(n), 8), rng.sample(range(n), 9) + rows = [i for i in r for _ in range(rng.randrange(1, 4))] + cols = [j for j in a for _ in range(rng.randrange(1, 4))] + q = rng.randrange(1, 4) + d = [[rng.randrange(2) for _ in range(q)] for _ in rows] + e = [[rng.randrange(2) for _ in cols] for _ in range(q)] + b = [[sum(d[i][k] * e[k][j] for k in range(q)) % 2 + for j in range(len(cols))] for i in range(len(rows))] + masked = [[fmul(hbar[s][t], b[i][j]) for j, t in enumerate(cols)] + for i, s in enumerate(rows)] + require(rank(masked, "F4") <= q * rank(submatrix(h, r, a)), + "block-linear message rank estimate") + + bad_diagonal = [row[:] for row in hbar] + bad_diagonal[0][0] = 0 + bad_zero = [row[:] for row in hbar] + orthogonal = next(j for j in range(1, n) if not ((adjacent[0] >> j) & 1)) + bad_zero[0][orthogonal] = 1 + illegal = [row[:] for row in identity] + nonorthogonal = next(j for j in range(1, n) if (adjacent[0] >> j) & 1) + illegal[0][nonorthogonal] = 1 + missing = [row[:] for row in fitting] + missing[0][0] = 0 + controls = [ + expect_rejection(lambda: check_hadamard(bad_diagonal, fitting), "lost unit diagonal"), + expect_rejection(lambda: check_hadamard(bad_zero, fitting), "corrupted orthogonal zero"), + expect_rejection(lambda: check_witness(illegal, adjacent), "illegal side information"), + expect_rejection(lambda: check_hadamard(hbar, illegal), "non-fitting Schur product"), + expect_rejection(lambda: check_witness(missing, adjacent), "omitted demanded coordinate"), + expect_rejection(lambda: reduce_mod2((F(1, 2), F(0))), "bad reduction denominator"), + expect_rejection(lambda: require(frame_cost >= rank(product, "F4"), "underpriced width"), + "charging a two-bit message once"), + ] + receipt = { + "lines": n, "gram_entries": n * n, "trace_entries": trace_entries, + "gram_values": len(values), "rank_K": 4, "rank_F4": 4, + "rank_conversion_samples": len(pairs_to_check), + "hyperplanes": 40, "row_star_cost": 40, + "binary_minrank_witness": 10, + "non_clean_control_cost": cost, "negative_controls": controls, + "block_linear_samples": block_samples, "block_linear_sharp_cost": 8, + "proof_scope": "all finite scalar binary rectangle decompositions; see README for proof", + } + print(json.dumps(receipt, indent=2, sort_keys=True)) + print("PASS_EISENSTEIN_REDUCTION_COPY_FLOOR: sharp abstract scalar cost 40") + + +if __name__ == "__main__": + main()