From 4ed8e8a9b587f98f25201758dcb1cf2cca0a40d8 Mon Sep 17 00:00:00 2001 From: joaqcoo Date: Tue, 13 Oct 2026 17:23:11 -0300 Subject: [PATCH 1/2] Research: nine-term complex E8 decoder normal form and residual class (seed 42, no new kappa) Theorem A gives the exact normal form of every m-term decoder (D = RA + N1, T = RB + N2 with AB^T = 2I, N1 B^T = 0, A N2^T = 0, N1 N2^T = 0). At m = 9 the kernel pairing forces junk onto at most one factor, so one-sided nine-term decoders are exactly overcomplete per-line representations. Merging reduces |supp z| <= 2 to the PR968/PR1077 eight-term floor. Ratio-class and P120 cost propositions bound the residual class; exact frame constructions and a bounded search find nothing below 4/7. Co-Authored-By: Claude Opus 5.5 --- .../CERTIFICATE.json | 270 ++++++++++ .../CLAIM.md | 26 + .../PROOF.md | 173 +++++++ .../README.md | 162 ++++++ .../SEARCH.json | 281 +++++++++++ .../SOURCES.json | 20 + .../e8lab.py | 265 ++++++++++ .../search.py | 91 ++++ .../verify.py | 467 ++++++++++++++++++ 9 files changed, 1755 insertions(+) create mode 100644 research/nine-term-decoder-normal-form-seed42/CERTIFICATE.json create mode 100644 research/nine-term-decoder-normal-form-seed42/CLAIM.md create mode 100644 research/nine-term-decoder-normal-form-seed42/PROOF.md create mode 100644 research/nine-term-decoder-normal-form-seed42/README.md create mode 100644 research/nine-term-decoder-normal-form-seed42/SEARCH.json create mode 100644 research/nine-term-decoder-normal-form-seed42/SOURCES.json create mode 100644 research/nine-term-decoder-normal-form-seed42/e8lab.py create mode 100644 research/nine-term-decoder-normal-form-seed42/search.py create mode 100644 research/nine-term-decoder-normal-form-seed42/verify.py diff --git a/research/nine-term-decoder-normal-form-seed42/CERTIFICATE.json b/research/nine-term-decoder-normal-form-seed42/CERTIFICATE.json new file mode 100644 index 0000000000..e7813adcca --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/CERTIFICATE.json @@ -0,0 +1,270 @@ +{ + "U1": 56, + "U2": 84, + "code_weights": { + "56": 255, + "64": 255, + "120": 1 + }, + "deficient_intersection_size_rank": { + "0,0": 255, + "28,7": 12960, + "32,7": 22680, + "36,6": 3360 + }, + "fails": [], + "frames": { + "A2 weights + E6 root basis": { + "P120_cost": 78, + "P120_term_costs": [ + 9, + 7, + 8, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "masked_terms": 3, + "row_support_sizes": [ + 30, + 28, + 29, + 57, + 106, + 106, + 106, + 106, + 106 + ], + "sparsity": { + "1": 6, + "2": 13, + "6": 65, + "7": 36 + } + }, + "A3 weights + D5 root basis": { + "P120_cost": 81, + "P120_term_costs": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "masked_terms": 4, + "row_support_sizes": [ + 39, + 19, + 39, + 39, + 78, + 78, + 104, + 104, + 104 + ], + "sparsity": { + "1": 5, + "2": 14, + "3": 4, + "4": 2, + "5": 19, + "6": 76 + } + }, + "A7 weights + A1 root": { + "P120_cost": 81, + "P120_term_costs": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "masked_terms": 8, + "row_support_sizes": [ + 42, + 22, + 42, + 42, + 40, + 40, + 40, + 40, + 57 + ], + "sparsity": { + "1": 1, + "2": 28, + "3": 56, + "4": 35 + } + }, + "A8 weights": { + "P120_cost": 81, + "P120_term_costs": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9 + ], + "masked_terms": 9, + "row_support_sizes": [ + 36, + 36, + 36, + 36, + 36, + 36, + 36, + 36, + 36 + ], + "sparsity": { + "2": 36, + "3": 84 + } + }, + "coordinate frame + root": { + "P120_cost": 76, + "P120_term_costs": [ + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 9, + 4 + ], + "masked_terms": 5, + "row_support_sizes": [ + 53, + 51, + 51, + 51, + 57, + 57, + 57, + 57, + 8 + ], + "sparsity": { + "1": 9, + "2": 4, + "3": 3, + "4": 104 + } + } + }, + "log": [ + "PASS A1 120 lines", + "PASS A2 label pairing F2 rank 9", + "PASS A3 pairing rows distinct", + "PASS A4 code weights {56:255, 64:255, 120:1} | {64: 255, 56: 255, 120: 1}", + "PASS B1 every nonzero codeword support spans R^8 | {8: 511}", + "PASS B2 U1 = 56 (largest set of label span <= 8 has 64 lines)", + "PASS B3 pairwise intersections: 130305 pairs, rank census {8:91050, 7:35640, 6:3360, 0:255} | {6: 3360, 8: 91050, 7: 35640, 0: 255}", + "PASS B4 deficient intersections have (size, rank) in {(0,0),(28,7),(32,7),(36,6)} | {(36, 6): 3360, (32, 7): 22680, (28, 7): 12960, (0, 0): 255}", + "PASS B5 U2 = 84 (largest set of label span <= 7 has 36 lines)", + "PASS C1 P120: random one-sided 9-term decoder (frame+root, random t_i) is exact | 14400", + "PASS C1 P120 A'B'^T = I/2 (doubled coordinates)", + "PASS C1 P120 R^T N1 = 0 and R^T N2 = 0", + "PASS C1 P120 N1 B'^T = 0, A' N2^T = 0, N1 N2^T = 0", + "PASS C1 P120 dim ker B' = dim ker A' = m-8 = 1", + "PASS C1 P120 ker A' x ker B' dot pairing nondegenerate", + "PASS C1 P120 Corollary B: at most one factor leaves the root code | N1 zero=False, N2 zero=True", + "PASS C1 P120: row factor leaves the root code, column factor does not", + "PASS C1 P112: random one-sided 9-term decoder (frame+root, random t_i) is exact | 12544", + "PASS C1 P112 A'B'^T = I/2 (doubled coordinates)", + "PASS C1 P112 R^T N1 = 0 and R^T N2 = 0", + "PASS C1 P112 N1 B'^T = 0, A' N2^T = 0, N1 N2^T = 0", + "PASS C1 P112 dim ker B' = dim ker A' = m-8 = 1", + "PASS C1 P112 ker A' x ker B' dot pairing nondegenerate", + "PASS C1 P112 Corollary B: at most one factor leaves the root code | N1 zero=False, N2 zero=True", + "PASS C1 P112: row factor leaves the root code, column factor does not", + "PASS C2 PR1180-shaped outside-code nine-term identity exact on all 12544 P112 pairs", + "PASS C2 A'B'^T = I/2 (doubled coordinates)", + "PASS C2 R^T N1 = 0 and R^T N2 = 0", + "PASS C2 N1 B'^T = 0, A' N2^T = 0, N1 N2^T = 0", + "PASS C2 dim ker B' = dim ker A' = m-8 = 1", + "PASS C2 ker A' x ker B' dot pairing nondegenerate", + "PASS C2 Corollary B: at most one factor leaves the root code | N1 zero=False, N2 zero=True", + "PASS C2 its outside-code part sits in D only", + "PASS C3 z.y != 0 at m = 9 | 5/4", + "PASS C3 one-sided junk n z^T alone keeps exactness (sampled pairs)", + "PASS C3 control: two-sided junk (n z^T, m y^T) at m = 9 is inexact | 5700 wrong entries", + "PASS C4 m = 10: found z in ker B', y in ker A' with z.y = 0, y != 0", + "PASS C4 m = 10 decoder with junk on both factors is exact on all 14400 pairs", + "PASS C4 A'B'^T = I/2 (doubled coordinates)", + "PASS C4 R^T N1 = 0 and R^T N2 = 0", + "PASS C4 N1 B'^T = 0, A' N2^T = 0, N1 N2^T = 0", + "PASS C4 dim ker B' = dim ker A' = m-8 = 2", + "PASS C4 ker A' x ker B' dot pairing nondegenerate", + "PASS C4 both factors leave the root code (Corollary B is specific to m = 9)", + "PASS D1 dependency support of a parallel pair is {0, 8} | [0, 8]", + "PASS D2 merged eight-term decoder is exact on all 14400 pairs", + "PASS D3 merging never increases cost (40 random one-sided decoders) | min saving 9", + "PASS E1 A8 weights: v_kk' != 0 for all 36 masked pairs", + "PASS E2 A8 weights: a line avoiding two masked terms is orthogonal to v_kk'", + "PASS E3 A8 weights: every option avoids exactly one ratio class of masked terms", + "PASS E1 A7 weights + A1 root: v_kk' != 0 for all 28 masked pairs", + "PASS E2 A7 weights + A1 root: a line avoiding two masked terms is orthogonal to v_kk'", + "PASS E3 A7 weights + A1 root: every option avoids exactly one ratio class of masked terms", + "PASS E1 A2 weights + E6 root basis: v_kk' != 0 for all 3 masked pairs", + "PASS E2 A2 weights + E6 root basis: a line avoiding two masked terms is orthogonal to v_kk'", + "PASS E3 A2 weights + E6 root basis: every option avoids exactly one ratio class of masked terms", + "PASS E1 A3 weights + D5 root basis: v_kk' != 0 for all 6 masked pairs", + "PASS E2 A3 weights + D5 root basis: a line avoiding two masked terms is orthogonal to v_kk'", + "PASS E3 A3 weights + D5 root basis: every option avoids exactly one ratio class of masked terms", + "PASS E1 coordinate frame + root: v_kk' != 0 for all 10 masked pairs", + "PASS E2 coordinate frame + root: a line avoiding two masked terms is orthogonal to v_kk'", + "PASS E3 coordinate frame + root: every option avoids exactly one ratio class of masked terms", + "PASS F1 A8 weights: sparsest-representation 9-term decoder exact on all 14400 pairs | 14400", + "PASS F2 A8 weights: P120 cost formula rho_k = dim V_Xk (all column supports span 9)", + "PASS F1 A7 weights + A1 root: sparsest-representation 9-term decoder exact on all 14400 pairs | 14400", + "PASS F2 A7 weights + A1 root: P120 cost formula rho_k = dim V_Xk (all column supports span 9)", + "PASS F1 A2 weights + E6 root basis: sparsest-representation 9-term decoder exact on all 14400 pairs | 14400", + "PASS F2 A2 weights + E6 root basis: P120 cost formula rho_k = dim V_Xk (all column supports span 9)", + "PASS F1 A3 weights + D5 root basis: sparsest-representation 9-term decoder exact on all 14400 pairs | 14400", + "PASS F2 A3 weights + D5 root basis: P120 cost formula rho_k = dim V_Xk (all column supports span 9)", + "PASS F1 coordinate frame + root: sparsest-representation 9-term decoder exact on all 14400 pairs | 14400", + "PASS F2 coordinate frame + root: P120 cost formula rho_k = dim V_Xk (all column supports span 9)", + "PASS F3 A8 frame: every line is 2- or 3-sparse (36 + 84)", + "PASS F4 A8 frame: every row support has 36 = 120 - U2 lines, yet label span 9; cost 81", + "PASS F5 no frame of section F beats the eight-term P120 floor 72 | {'A8 weights': 81, 'A7 weights + A1 root': 81, 'A2 weights + E6 root basis': 78, 'A3 weights + D5 root basis': 81, 'coordinate frame + root': 76}", + "PASS G1 control: perturbing one coefficient breaks exactness", + "PASS G2 control: deleting one support entry breaks exactness", + "PASS G3 control: a rank-deficient frame is rejected", + "PASS G4 control: a flipped label entry changes the pairing rank away from 9 | 10", + "PASS G5 control: label_dim of a single line is 1, of C(root) is 9" + ], + "pairwise_intersection_rank_census": { + "0": 255, + "6": 3360, + "7": 35640, + "8": 91050 + }, + "section_C": { + "C1_P112_random_cost": 73, + "C1_P120_random_cost": 81 + } +} diff --git a/research/nine-term-decoder-normal-form-seed42/CLAIM.md b/research/nine-term-decoder-normal-form-seed42/CLAIM.md new file mode 100644 index 0000000000..ce6c5b94ce --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/CLAIM.md @@ -0,0 +1,26 @@ +# Local sprint claim (no coordination post was made) + +- Recorded: 2026-10-13T19:40Z. Track 40-49, structural decoder research. Assignment seed **42**, + drawn once with `python -c "import secrets; print(secrets.randbelow(100))"` (OS randomness). +- Base commit: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` (main; selected PR1094, kappa 0.001672660197076918). +- Initial object: whole-decoder copy ratio of exact 8-term complex decoders for punctures p >= 25 + (beyond PR968's p <= 24; PR1020 settled only the single-term threshold). +- Candidates considered: (1) the p >= 25 ratio question; (2) n >= 9-term decoders (PR968 scope, PR717 + mixed-beta); (3) E-graph-only masked decoders (needs PR717 D1 spec). +- Pivot (one, evidence-driven): any complex-only gain beyond P104 is already capped by the PR589 bit + supplier (PR968 section G), so the p >= 25 ratio question has little practical value. While + pricing it, the n = 9 normal form (Corollaries B/C) emerged, and n >= 9 became the object. +- Method: exact linear algebra (written proofs) plus exact F2/rational census and constructions; + bounded annealing over frames (seeds 0-2, 3000 moves). + +## Result + +- Delivered as `research/nine-term-decoder-normal-form-seed42/` (research note / scoped structural + result, no kappa claim). +- Theorem A (normal form for any m), Corollary B (m = 9: at most one factor leaves the root code), + Corollary C (one-sided 9-term = overcomplete representation), Lemma D (|S| <= 2 reduces to 8 terms), + Propositions E-G (rigid unmasked terms, ratio classes, exact P120 cost 81 - sum delta_k and its + necessary conditions; 39,255 non-spanning support pairs). +- No 9-term construction or search run beat 72 (P120), 64/112 or 7/13; best ratio 0.6036. +- Overlap at submission: PR1180 (both factors root-linear, any m), PR1191 (masked identities), + PR1197 (P112 ten-term restricted cases): complementary, credited. diff --git a/research/nine-term-decoder-normal-form-seed42/PROOF.md b/research/nine-term-decoder-normal-form-seed42/PROOF.md new file mode 100644 index 0000000000..e510fd180a --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/PROOF.md @@ -0,0 +1,173 @@ +# Nine-term complex E8 decoders: normal form and reductions + +Finite facts cited as **(Bk)**, **(Ck)**, ... are checked by `verify.py` with exact integer, F2 and +rational arithmetic. Everything else is a written argument. No premise is imported from an +unreviewed pull request; where a result of an open PR is *combined* with the statements below, it is +named as such. + +## 1. Model + +This is the B14 decoder model of PR717 as used by PR968 §1 and PR1077. The 120 root lines of E8 have +norm-2 representatives r_i and Gram matrix G. A puncture P removes p lines, leaving the live set L. +Labels lie in a nine-dimensional F2 space Λ with nondegenerate pairing +S9(u_i, u_j) = (⟨r_i, r_j⟩ + 1) mod 2. For a set X of lines write V_X for the span of its labels. + +Let F be R or C (ordinary transpose, no conjugation). An **exact m-term decoder** is a pair +D, T ∈ F^{L×m} with D Tᵀ = 2G on all live pairs. Term k has row support X_k = {i : D_ik ≠ 0} and +column support Y_k = {j : T_jk ≠ 0}, and costs the PR446 Theorem C pairing rank +ρ_k = rank(S9 restricted to V_{X_k} × V_{Y_k}). The copy cost is cst = Σ_k ρ_k. Since the pairing is +symmetric, transposing a decoder (D ↔ T) preserves exactness and every term cost. + +R ∈ R^{L×8} is the live-root matrix. **Standing hypothesis:** rank R = 8. This holds whenever +p ≤ 56, because a real root-spanned hyperplane contains at most 63 lines. + +For a vector b let C(b) = {i ∈ L : ⟨r_i, b⟩ ≠ 0}. For complex b = u + iv, a real line is orthogonal +to b exactly when it is orthogonal to both u and v. + +## 2. Theorem A (normal form for any number of terms) + +Since RᵀR is real positive definite, it is invertible over F, and F^L = col(R) ⊕ ker(Rᵀ). (The +intersection is zero: R a ∈ ker Rᵀ gives RᵀR a = 0, so a = 0. The dimensions add up.) Write + + D = R A + N1, T = R B + N2, with Rᵀ N1 = Rᵀ N2 = 0, + +where A = (RᵀR)⁻¹RᵀD and B = (RᵀR)⁻¹RᵀT are 8×m. + +**Theorem A.** D Tᵀ = 2G holds if and only if + + (i) A Bᵀ = 2 I_8, (ii) N1 Bᵀ = 0, (iii) A N2ᵀ = 0, (iv) N1 N2ᵀ = 0. + +*Proof.* Here 2G = 2RRᵀ in true units. Expand + + D Tᵀ = R A Bᵀ Rᵀ + R A N2ᵀ + N1 Bᵀ Rᵀ + N1 N2ᵀ. + +Let L⁺ = (RᵀR)⁻¹Rᵀ and Π = I − R L⁺. Then L⁺R = I, L⁺N = 0, ΠR = 0 and ΠN = N for N in ker Rᵀ. +Applying L⁺(·)L⁺ᵀ, Π(·)L⁺ᵀ, L⁺(·)Πᵀ and Π(·)Πᵀ to both sides isolates the four summands. The right +side 2RRᵀ gives 2I, 0, 0 and 0 respectively. Conversely, (i)–(iv) make the expansion equal to +R(2I)Rᵀ. ∎ + +From (i), rank A = rank B = 8 and m ≥ 8. Let ker A and ker B be the right kernels in F^m; each has +dimension m − 8. Condition (ii) says every row of N1 lies in ker B, and (iii) says every row of N2 +lies in ker A. + +**Lemma A′.** The bilinear pairing ker A × ker B → F, (y, z) ↦ yᵀz, is nondegenerate. + +*Proof.* Let y ∈ ker A satisfy yᵀz = 0 for every z in ker B. The bilinear orthogonal complement of +ker B is the row space {Bᵀu} of B, because the row space is contained in it and both have dimension 8. +So y = Bᵀu, and 0 = A y = A Bᵀ u = 2u. Hence y = 0. The other side is symmetric. ∎ + +## 3. Corollary B (m = 9: at most one factor leaves the root code) + +For m = 9, ker A = span(y) and ker B = span(z), with yᵀz ≠ 0 by Lemma A′. Then N1 = n zᵀ and +N2 = n′ yᵀ for some n, n′ ∈ ker Rᵀ, and (iv) reads (zᵀy) n n′ᵀ = 0. So **n = 0 or n′ = 0**. At least +one of D, T has every column in col(R). (C3) checks that putting junk on both sides breaks +exactness. (C4) gives an exact 10-term decoder with junk on both factors, so this corollary is +specific to m = 9. (C1) and (C2) decompose explicit decoders: random one-sided ones, and the shape of +PR1180's outside-code identity. + +*Combination with concurrent work.* PR1180 (@woklerx, open, head `75b4086`) proves cst ≥ max(72 − p, 56) +for p ≤ 24 and any m, when **both** factors lie in col(R). With Corollary B, a 9-term decoder +outside PR1180's class therefore has *exactly one* factor outside the root code. This package does +not re-verify PR1180. + +## 4. Corollary C (one-sided nine-term decoders are overcomplete representations) + +Transpose if necessary so that N2 = 0. Write b_1..b_9 for the columns of B, so T_jk = ⟨r_j, b_k⟩. +They span F^8 and satisfy the single dependency Σ_k z_k b_k = 0. + +**Corollary C.** (D, T) is exact if and only if every row d_i of D satisfies Σ_k d_ik b_k = 2 r_i. + +*Proof.* (D Tᵀ)_ij = ⟨r_j, Σ_k d_ik b_k⟩. Since the live roots span R^8, this equals 2⟨r_j, r_i⟩ for +all live j exactly when Σ_k d_ik b_k = 2 r_i. ∎ + +So each live line independently picks any representation of 2r_i in the overcomplete frame {b_k}. +The representations of line i form the affine line c⁰_i + F·z, giving one free scalar t_i per line. +Row supports are the supports of the chosen representations, and the column supports are +Y_k = C(b_k). Every 8-term decoder is the case with no freedom. + +## 5. Lemma D (merging) and the residual class + +**Lemma D.** Suppose b_l = μ b_k for some l ≠ k. Replace the two terms by the single term with row +vector d_k + μ d_l and column normal b_k. This gives an exact decoder with one term fewer and no +larger cost. + +*Proof.* Exactness is linear. The new row support is contained in X_k ∪ X_l, and the column support +is unchanged. The pairing rank is monotone in the row set and subadditive over a union of row sets. ∎ + +A zero column normal contributes a vanishing term of cost 0 and can be dropped. Let S = supp(z). If +|S| ≤ 2, then some b_k = 0 or two normals are proportional, and dropping or merging yields an exact +8-term decoder with no larger cost. PR968 (real) and PR1077 (complex), both on main, then give +cst ≥ max(72 − p, 56) for p ≤ 24. Hence: + +> **For p ≤ 24, an exact nine-term decoder can beat the eight-term floor only if exactly one factor +> leaves the root code and its overcomplete frame has |S| ≥ 3 pairwise non-proportional normals in +> its dependency.** (The "exactly one factor" part uses the open PR1180 for the other case.) + +## 6. Proposition E (unmasked terms are rigid) + +For k ∉ S, b_k is not in the span of the other eight normals. Otherwise the unique dependency would +have z_k ≠ 0. So the coefficient of b_k is the same in every representation. It is given by a fixed +functional ã_k, and X_k = C(ã_k) is forced exactly as in an 8-term decoder. Only the |S| **masked** +terms have adjustable row supports. + +## 7. Proposition F (ratio classes) + +For k ∈ S we have d_ik = c⁰_ik + t_i z_k, which vanishes iff t_i = −c⁰_ik / z_k. Therefore the masked +terms avoided by line i are exactly one class of equal ratios. (E3) checks this on every frame. + +For k ≠ k′ in S, the quantity c_k z_{k′} − c_{k′} z_k does not depend on the choice of representation +c of 2x, because t cancels. It is linear in x, so it equals ⟨v_{kk′}, 2x⟩ for a unique vector +v_{kk′}. + +**Proposition F.** v_{kk′} ≠ 0, and every line avoiding both masked terms k and k′ satisfies +⟨v_{kk′}, r_i⟩ = 0. + +*Proof.* The vector 2e_k is a representation of 2b_k. For it, the quantity is 2z_{k′} ≠ 0. A line +avoiding both terms has c_k = c_{k′} = 0. ∎ + +(E1)–(E2) check this on five frames. For a deficiency functional (codeword) w of a row side, let +K(X) = {w : supp(w) ∩ X = ∅}, so that dim V_X = 9 − dim K(X). + +- **F1.** If w ∈ K(X_k) ∩ K(X_{k′}) with k ≠ k′ masked, then the live part of supp(w) lies in the + proper subspace v_{kk′}^⊥. +- **F2.** If w ∈ K(X_k) and w′ ∈ K(X_{k′}), then L ∩ supp(w) ∩ supp(w′) lies in v_{kk′}^⊥. + +## 8. Proposition G (the unpunctured unit P120) + +**(B1)** All 511 nonzero codeword supports span R^8. If C(b) ∩ supp(w) = ∅ for some b ≠ 0, then +supp(w) would lie in the proper subspace b^⊥ (real and imaginary parts), which is impossible. So +**every** C(b) on P120 has label span Λ. + +Consequently V_Y^⊥ = 0 for every column side, and ρ_k = dim V_{X_k} exactly. (F2) checks this +formula on every frame decoder. Unmasked row sides have full span as well. For a one-sided 9-term +decoder on P120 this gives + + cst = 81 − Σ_{k∈S} δ_k, δ_k = 9 − dim V_{X_k}. + +**G1.** cst < 72 requires Σ_{k∈S} δ_k ≥ 10. Since |S| ≤ 9, some masked row side must have δ_k ≥ 2. +By **(B5)**, U2 = 84, so that side has at most 36 lines and at least 84 lines avoid its term. In +particular, if every masked δ_k ≤ 1, then cst ≥ 72. + +**G2.** By F1 and B1, the deficiency spaces K(X_k), k ∈ S, intersect pairwise trivially. By F2, every +cross pair (w ∈ K(X_k), w′ ∈ K(X_{k′}), w ≠ w′) is one of the **39,255** pairs whose support +intersection does not span R^8 **(B3–B4)**: + +- 255 complementary pairs, with empty intersection; +- 35,640 pairs whose intersection of 28 or 32 lines has rank 7; +- 3,360 pairs whose 36-line intersection has rank 6. + +Moreover, the hyperplane in question must be v_{kk′}^⊥. Because so many non-spanning pairs exist, +the pairwise argument alone does **not** exclude a P120 counterexample. This is recorded as an open +case, not a theorem. + +## 9. What is and is not proved + +Proved here: Theorem A, Lemma A′, Corollaries B and C, Lemma D, and Propositions E, F and G (with the +finite facts B1–B5). Together with PR968/PR1077 these give the residual-class statement of §5. The +"exactly one factor" refinement additionally uses the open PR1180. + +Not proved: a copy-cost floor for one-sided 9-term decoders with |S| ≥ 3 (on P120, P112 or any p); +decoders with m ≥ 10 (two-sided junk is possible, see C4); masked-identity (E-graph only) decoders +(see #1191); punctures with p > 56; and any physical realization. The frames and annealing in +`verify.py` §F and `search.py` are finite evidence, not proofs. This is not a formal verification of +the multiplication theorem. diff --git a/research/nine-term-decoder-normal-form-seed42/README.md b/research/nine-term-decoder-normal-form-seed42/README.md new file mode 100644 index 0000000000..9b80020d0c --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/README.md @@ -0,0 +1,162 @@ +# Nine-term complex E8 decoders: normal form and residual class (no new κ) + +**Status:** research note / scoped structural result. No κ claim, no supplier word. +`certificates/selected-result.json` (PR1094, κ = 0.001672660197076918), `upstream/` and every +existing file are unchanged. + +PR968 and PR1077 proved the punctured complex E8 copy-cost floor for **exactly eight** terms. +Decoders with **n ≥ 9 terms** stayed open (PR968 §6, PR1071, PR1077, and PR717's open mixed-β +problem). This package finds the exact algebraic structure of every nine-term decoder and +reduces the open part to one explicit class. + +## Results + +The model is PR717 B14 / PR968 §1, with real or complex coefficients and ordinary transpose. Assume +the live roots span R^8, which is automatic for p ≤ 56. Proofs are in [PROOF.md](PROOF.md). + +1. **Theorem A (any m).** Every exact m-term decoder is D = RA + N1, T = RB + N2. Here R^T N1 = R^T N2 = 0 and + AB^T = 2I, N1 B^T = 0, A N2^T = 0, N1 N2^T = 0. The converse also holds. The pairing between + ker A and ker B is nondegenerate. +2. **Corollary B (m = 9).** At most one of D, T has columns outside the live root code: the two junk + parts satisfy (z·y) n n'^T = 0 with z·y ≠ 0. This is specific to nine terms. An exact ten-term + decoder with outside-code columns on both factors is checked in C4. +3. **Corollary C.** A one-sided nine-term decoder is the same thing as an **overcomplete + representation**. Pick nine column normals b_k with one dependency z, set T_jk = , and + let row i of D be *any* coefficient vector with Σ_k d_ik b_k = 2 r_i. Each line has exactly one + free scalar. +4. **Lemma D.** Proportional column normals can be merged without increasing cost. So a nine-term + decoder whose dependency has support |S| ≤ 2 is no cheaper than an eight-term one. PR968/PR1077 + then give cst ≥ max(72 − p, 56) for p ≤ 24. +5. **Propositions E, F.** Terms outside S have forced (unmaskable) row supports. A line skips + exactly one *ratio class* of masked terms. A line skipping two masked terms k, k' is orthogonal to + a canonical nonzero vector v_kk'. Hence one deficiency codeword cannot serve two masked row sides + if its live support spans R^8. +6. **Proposition G (P120).** All 511 codeword supports span R^8, so every column side has full + label span. A one-sided nine-term decoder on P120 therefore costs exactly 81 − Σ_{k∈S} δ_k, where + δ_k is the label deficiency of masked row side k. Beating 72 needs Σ δ_k ≥ 10. That forces a + masked row support of at most 36 lines (U2 = 84), and every cross pair of deficiency codewords must + be one of 39,255 non-spanning support pairs. Census: + - 255 complementary pairs; + - 35,640 pairs whose intersection has rank 7; + - 3,360 pairs whose intersection has rank 6. + + This census shows that the pairwise argument alone cannot close P120. + +**Residual class.** For p ≤ 24, the eight-term floor can fail at nine terms only for decoders with +exactly one factor outside the root code and |S| ≥ 3. The "exactly one" part uses PR1180 (open, +concurrent), which handles the case where both factors stay in the root code. Without PR1180 the +statement reads "at most one". + +## Constructions and bounded search (evidence, not proof) + +Exact nine-term decoders were built from weight frames of maximal subsystems. Every line is +represented sparsely; for example, in the **A8 weight frame** each E8 root is 2- or 3-sparse. +Each decoder is checked on all 14,400 pairs. + +| frame | masked terms | P120 cost | note | +|---|---|---|---| +| A8 weights | 9 | 81 | every row support has 36 = 120 − U2 lines, yet label span 9 | +| A7 weights + A1 root | 8 | 81 | | +| A2 weights + E6 root basis | 3 | 78 | | +| A3 weights + D5 root basis | 4 | 81 | | +| coordinate frame + one root | 5 | 76 | | + +`search.py` annealed over every per-line ratio-class choice. + +- **Domain:** the five frames, each on P120 and on its self-punctured live set. +- **Stopping rule:** seeds 0–2, 3,000 moves per run, 27 runs in total. +- **Result:** best ratio 67/111 = 0.6036. Nothing came below the shipped 64/112 = 0.5714 or PR968's + 56/104. + +Earlier exploratory annealing from the coordinate decoder with 2, 4 or 8 extra root normals +never left 72 (P120) or 64 (P112). Those scratch runs are not packaged. This is a failed search over +the stated domain, not an impossibility theorem. Because no candidate was found, there is nothing to +price. Any complex-only gain would in any case be capped by the PR589 bit supplier, as PR968 §G +shows. + +## Reproduce + +From the repository root, Python 3.10+, standard library only: + +```text +python3 -I -B research/nine-term-decoder-normal-form-seed42/verify.py +``` + +The run takes about 35 s. Expected final line: + +```text +PASS_NINE_TERM_NORMAL_FORM_S42 checks=80 pairs=130305 frames=5 A8_cost=81 +``` + +`--quick` skips the 130,305-pair census (B3–B5). `--out FILE` writes the full JSON certificate. The +bounded search (about 70 s) is: + +```text +python3 -I -B research/nine-term-decoder-normal-form-seed42/search.py --iters 3000 --seeds 3 +``` + +Its expected last line begins `SEARCH_DONE runs=27 best_ratio=0.6036`. The recorded run is +[SEARCH.json](SEARCH.json). + +What `verify.py` checks: + +- **A:** the model: 120 lines, a rank-9 pairing, code weights {56:255, 64:255, 120:1}. +- **B:** the spanning census: + - all supports span R^8; + - the rank of all 130,305 pairwise intersections; + - U1 = 56 and U2 = 84. +- **C:** Theorem A and Corollaries B and C on exact decoders: + - random one-sided decoders on P112 and P120; + - the PR1180-shaped outside-code identity; + - an inexact two-sided control at m = 9; + - an exact two-sided decoder at m = 10. +- **D:** merging. +- **E:** the ratio classes and v_kk' ≠ 0 on every frame. +- **F:** the frame decoders and the P120 cost formula. +- **G:** controls: + - a perturbed coefficient; + - a deleted support entry; + - a rank-deficient frame; + - a flipped label; + - label-span sanity checks. + +## Scope and inherited obligations + +- **Covered:** the structure of all exact nine-term decoders when the live roots span R^8; the + reduction of the n = 9 floor question to the residual class; the P120 necessary conditions. +- **Not covered:** + - a floor for the residual class; + - m ≥ 10 terms; + - E-graph-only (masked-identity) decoders, for which see PR1191; + - p > 56; + - any copy-tree realization, delivery, restoration, hosting or precision cost. +- **Cited, not recomputed:** PR968's real eight-term floor (including its F6 flat classification) + and PR1077's complex extension, both on main and pinned in `SOURCES.json`. PR1180's both-root-code + theorem is cited only for the optional "exactly one factor" refinement. It is open and is not + re-verified here. +- All inherited conditions of the selected record are unchanged: all-size/compiler, common-label + and mutable-source realization, whole-call hosting, precision/tape, analytic transfer, and the bit + supplier's H1–H5. Finite replay is not a formal proof of the multiplication theorem, and the + written proofs have had no independent human review. + +## Provenance, credit and overlap + +- **Base:** `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` (main). Sprint track 40–49 (structural + decoder research), OS-random seed **42**. See [CLAIM.md](CLAIM.md). The claim was recorded locally; + no coordination post was made. +- **DreamingOfClouds (PR717, PR595):** the B14 decoder model, the cost semantics and the open + n ≥ 9 / mixed-β question. +- **themilkman216 (PR968)** and **@woklerx (PR1077):** the eight-term floor this package extends the + reach of. +- **@woklerx (PR1180, open, concurrent):** the arbitrary-m floor when both factors stay in the root + code. It also gives the outside-code nine-term example that this package's Corollary B explains, + since that junk is necessarily one-sided. +- **@mightyOil (PR1191, PR1197, open, concurrent):** one-sided mask rigidity for masked identities, and + restricted P112 ten-term cases. These are adjacent scopes that neither contain nor are contained in + this one. +- **@3xcalibur-tech (PR1171):** the support-union hierarchy (U1, U2) is re-derived here independently. +- Also credited: PR620 (GamingPuzzled), PR446 Theorem C (DreamingOfClouds) and the selected supplier + lineage. All code here is independently written; nothing is vendored. +- **AI assistance and license:** prepared with substantial assistance from Claude Opus 5.5 + (Anthropic) via Claude Code, covering the research, proofs, implementation and write-up. Submitted + by @joaqcoo. Apache-2.0. diff --git a/research/nine-term-decoder-normal-form-seed42/SEARCH.json b/research/nine-term-decoder-normal-form-seed42/SEARCH.json new file mode 100644 index 0000000000..d171a6903a --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/SEARCH.json @@ -0,0 +1,281 @@ +{ + "domain": "verify.py section F frames x {P120, self-punctured}; per-line ratio-class options", + "stopping_rule": "3000 annealing moves per run, seeds 0..2", + "comparators": { + "P120 eight-term floor": 72, + "P112 shipped": "64/112", + "PR968 best ratio": "56/104" + }, + "runs": [ + { + "frame": "A8 weights", + "live": "P120", + "v": 120, + "seed": 0, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A8 weights", + "live": "P120", + "v": 120, + "seed": 1, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A8 weights", + "live": "P120", + "v": 120, + "seed": 2, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A7 weights + A1 root", + "live": "P120", + "v": 120, + "seed": 0, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A7 weights + A1 root", + "live": "P120", + "v": 120, + "seed": 1, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A7 weights + A1 root", + "live": "P120", + "v": 120, + "seed": 2, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A7 weights + A1 root", + "live": "self-punctured", + "v": 119, + "seed": 0, + "iters": 3000, + "start_cost": 80, + "best_cost": 80, + "best_ratio": "80/119" + }, + { + "frame": "A7 weights + A1 root", + "live": "self-punctured", + "v": 119, + "seed": 1, + "iters": 3000, + "start_cost": 80, + "best_cost": 80, + "best_ratio": "80/119" + }, + { + "frame": "A7 weights + A1 root", + "live": "self-punctured", + "v": 119, + "seed": 2, + "iters": 3000, + "start_cost": 80, + "best_cost": 80, + "best_ratio": "80/119" + }, + { + "frame": "A2 weights + E6 root basis", + "live": "P120", + "v": 120, + "seed": 0, + "iters": 3000, + "start_cost": 78, + "best_cost": 78, + "best_ratio": "78/120" + }, + { + "frame": "A2 weights + E6 root basis", + "live": "P120", + "v": 120, + "seed": 1, + "iters": 3000, + "start_cost": 78, + "best_cost": 78, + "best_ratio": "78/120" + }, + { + "frame": "A2 weights + E6 root basis", + "live": "P120", + "v": 120, + "seed": 2, + "iters": 3000, + "start_cost": 78, + "best_cost": 78, + "best_ratio": "78/120" + }, + { + "frame": "A2 weights + E6 root basis", + "live": "self-punctured", + "v": 114, + "seed": 0, + "iters": 3000, + "start_cost": 72, + "best_cost": 72, + "best_ratio": "72/114" + }, + { + "frame": "A2 weights + E6 root basis", + "live": "self-punctured", + "v": 114, + "seed": 1, + "iters": 3000, + "start_cost": 72, + "best_cost": 72, + "best_ratio": "72/114" + }, + { + "frame": "A2 weights + E6 root basis", + "live": "self-punctured", + "v": 114, + "seed": 2, + "iters": 3000, + "start_cost": 72, + "best_cost": 72, + "best_ratio": "72/114" + }, + { + "frame": "A3 weights + D5 root basis", + "live": "P120", + "v": 120, + "seed": 0, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A3 weights + D5 root basis", + "live": "P120", + "v": 120, + "seed": 1, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A3 weights + D5 root basis", + "live": "P120", + "v": 120, + "seed": 2, + "iters": 3000, + "start_cost": 81, + "best_cost": 81, + "best_ratio": "81/120" + }, + { + "frame": "A3 weights + D5 root basis", + "live": "self-punctured", + "v": 115, + "seed": 0, + "iters": 3000, + "start_cost": 76, + "best_cost": 76, + "best_ratio": "76/115" + }, + { + "frame": "A3 weights + D5 root basis", + "live": "self-punctured", + "v": 115, + "seed": 1, + "iters": 3000, + "start_cost": 76, + "best_cost": 76, + "best_ratio": "76/115" + }, + { + "frame": "A3 weights + D5 root basis", + "live": "self-punctured", + "v": 115, + "seed": 2, + "iters": 3000, + "start_cost": 76, + "best_cost": 76, + "best_ratio": "76/115" + }, + { + "frame": "coordinate frame + root", + "live": "P120", + "v": 120, + "seed": 0, + "iters": 3000, + "start_cost": 76, + "best_cost": 76, + "best_ratio": "76/120" + }, + { + "frame": "coordinate frame + root", + "live": "P120", + "v": 120, + "seed": 1, + "iters": 3000, + "start_cost": 76, + "best_cost": 76, + "best_ratio": "76/120" + }, + { + "frame": "coordinate frame + root", + "live": "P120", + "v": 120, + "seed": 2, + "iters": 3000, + "start_cost": 76, + "best_cost": 76, + "best_ratio": "76/120" + }, + { + "frame": "coordinate frame + root", + "live": "self-punctured", + "v": 111, + "seed": 0, + "iters": 3000, + "start_cost": 67, + "best_cost": 67, + "best_ratio": "67/111" + }, + { + "frame": "coordinate frame + root", + "live": "self-punctured", + "v": 111, + "seed": 1, + "iters": 3000, + "start_cost": 67, + "best_cost": 67, + "best_ratio": "67/111" + }, + { + "frame": "coordinate frame + root", + "live": "self-punctured", + "v": 111, + "seed": 2, + "iters": 3000, + "start_cost": 67, + "best_cost": 67, + "best_ratio": "67/111" + } + ] +} diff --git a/research/nine-term-decoder-normal-form-seed42/SOURCES.json b/research/nine-term-decoder-normal-form-seed42/SOURCES.json new file mode 100644 index 0000000000..2feace29b8 --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/SOURCES.json @@ -0,0 +1,20 @@ +{ + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "selected_record": { + "path": "certificates/selected-result.json", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "kappa": "836330098538459/500000000000000000" + }, + "cited_on_main": { + "research/complex-frame-pair-decoders/PROOF.md": {"pr": 968, "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74"}, + "research/complex-decoder-field-extension-seed44/README.md": {"pr": 1077, "sha256": "788a99eef3f187c2cbff6d490933fcc8f8e7fd15d1b685c188023605916887d4"} + }, + "cited_open_prs_not_imported": { + "1180": {"head": "75b408646d558147a4eb250fc407d1fbfcb8df4e", "file": "research/e8-factor-linear-overcomplete47/PROOF.md", "sha256": "98f9663c7340363debd239679cc45931e0db638f006e8742cdf0d876ea09a64a"}, + "1191": {"head": "640b43bb13d3d476a2d83b74ef0d33f14d1b5711"}, + "1197": {"head": "a0935afff6cc5540a582c5881bc8d5f98b587357"}, + "1171": {"head": "ab74c73b5b512f459b9be97680f41390d45a3bf3"} + }, + "vendored": {}, + "note": "All code in this package is written independently; no predecessor code is executed or vendored. Cited theorems are used only where stated in PROOF.md." +} diff --git a/research/nine-term-decoder-normal-form-seed42/e8lab.py b/research/nine-term-decoder-normal-form-seed42/e8lab.py new file mode 100644 index 0000000000..6aef95fc97 --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/e8lab.py @@ -0,0 +1,265 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Exact E8 / label / rational linear-algebra helpers for the nine-term normal-form package. + +Standard library only. Written independently of the PR968/PR1077/PR1180 checkers: the 120 E8 lines +are generated here, the binary label pairing is ( + 1) mod 2 (PR717 B14 / PR968 eq. (1)), +and every rank over Q is computed with exact Fractions. +""" +import itertools +from fractions import Fraction as Q + +# ------------------------------------------------------------------ E8 lines (doubled coordinates) + + +def _roots240(): + out = [] + for i, j in itertools.combinations(range(8), 2): + for si in (1, -1): + for sj in (1, -1): + v = [0] * 8 + v[i], v[j] = 2 * si, 2 * sj + out.append(tuple(v)) + for s in itertools.product((1, -1), repeat=8): + if s.count(-1) % 2 == 0: + out.append(tuple(s)) + return out + + +ROOTS240 = _roots240() + + +def _canon(v): + for a in v: + if a: + return tuple(v) if a > 0 else tuple(-x for x in v) + raise ValueError('zero vector') + + +LINES = sorted({_canon(v) for v in ROOTS240}, reverse=True) +N = len(LINES) +FULL = (1 << N) - 1 + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y)) + + +def gram(i, j): + """True inner product of the norm-2 representatives of lines i, j.""" + return dot(LINES[i], LINES[j]) // 4 + + +G = [[gram(i, j) for j in range(N)] for i in range(N)] +# label pairing rows as bitsets: bit j of M[i] is (G_ij + 1) mod 2 +M = [sum(((G[i][j] + 1) & 1) << j for j in range(N)) for i in range(N)] + + +def bits(mask): + i = 0 + while mask: + if mask & 1: + yield i + mask >>= 1 + i += 1 + + +def popcount(x): + return bin(x).count('1') + + +def f2_rank(rows): + piv = {} + r = 0 + for v in rows: + while v: + h = v.bit_length() - 1 + if h in piv: + v ^= piv[h] + else: + piv[h] = v + r += 1 + break + return r + + +def pairing_rank(X, Y): + """Theorem C cost of a term: F2 rank of the label pairing between line sets X and Y (bitmasks).""" + return f2_rank([M[i] & Y for i in bits(X)]) + + +def label_dim(X): + """dim of the label span V_X (= rank of the pairing rows of X against all lines).""" + return f2_rank([M[i] for i in bits(X)]) + + +def support(vec, live=FULL): + """Live lines not orthogonal to the (rational) vector vec.""" + m = 0 + for i in bits(live): + if sum(Q(a) * b for a, b in zip(LINES[i], vec)) != 0: + m |= 1 << i + return m + + +def code_words(): + """The 511 nonzero codewords (supports of nonzero label functionals) as bitmasks.""" + piv = {} + basis = [] + for v in M: + w = v + while w: + h = w.bit_length() - 1 + if h in piv: + w ^= piv[h] + else: + piv[h] = w + basis.append(v) + break + words = [] + for c in range(1, 1 << len(basis)): + w = 0 + for t in range(len(basis)): + if c >> t & 1: + w ^= basis[t] + words.append(w) + return basis, words + + +# ------------------------------------------------------------------ exact linear algebra over Q + + +def q_rank(rows): + rows = [[Q(x) for x in r] for r in rows] + if not rows: + return 0 + ncol = len(rows[0]) + r = 0 + for c in range(ncol): + p = next((i for i in range(r, len(rows)) if rows[i][c] != 0), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + pv = rows[r][c] + for i in range(len(rows)): + if i != r and rows[i][c] != 0: + f = rows[i][c] / pv + rows[i] = [x - f * y for x, y in zip(rows[i], rows[r])] + r += 1 + if r == len(rows): + break + return r + + +def line_rank(mask): + """Real rank of the root vectors of the lines in mask (integer elimination).""" + rows = [list(LINES[i]) for i in bits(mask)] + r = 0 + for c in range(8): + p = next((i for i in range(r, len(rows)) if rows[i][c] != 0), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + for i in range(len(rows)): + if i != r and rows[i][c] != 0: + a, b = rows[r][c], rows[i][c] + rows[i] = [a * x - b * y for x, y in zip(rows[i], rows[r])] + r += 1 + if r == 8: + break + return r + + +def q_inv(A): + n = len(A) + Mx = [[Q(x) for x in row] + [Q(int(i == j)) for j in range(n)] for i, row in enumerate(A)] + for c in range(n): + p = next(r for r in range(c, n) if Mx[r][c] != 0) + Mx[c], Mx[p] = Mx[p], Mx[c] + pv = Mx[c][c] + Mx[c] = [x / pv for x in Mx[c]] + for r in range(n): + if r != c and Mx[r][c] != 0: + f = Mx[r][c] + Mx[r] = [x - f * y for x, y in zip(Mx[r], Mx[c])] + return [row[n:] for row in Mx] + + +def q_nullspace(A, ncol): + """Basis of {x : A x = 0} for a list of rows A with ncol columns.""" + rows = [[Q(x) for x in r] for r in A] + pivots = [] + r = 0 + for c in range(ncol): + p = next((i for i in range(r, len(rows)) if rows[i][c] != 0), None) + if p is None: + continue + rows[r], rows[p] = rows[p], rows[r] + pv = rows[r][c] + rows[r] = [x / pv for x in rows[r]] + for i in range(len(rows)): + if i != r and rows[i][c] != 0: + f = rows[i][c] + rows[i] = [x - f * y for x, y in zip(rows[i], rows[r])] + pivots.append(c) + r += 1 + free = [c for c in range(ncol) if c not in pivots] + basis = [] + for f in free: + x = [Q(0)] * ncol + x[f] = Q(1) + for i, c in enumerate(pivots): + x[c] = -rows[i][f] + basis.append(x) + return basis + + +def matmul(A, B): + Bt = list(zip(*B)) + return [[sum((a * b for a, b in zip(row, col)), Q(0)) for col in Bt] for row in A] + + +def transpose(A): + return [list(r) for r in zip(*A)] + + +# ------------------------------------------------------------------ root subsystems and weight frames + + +def simple_chain(n, orth_to=()): + """Deterministic A_n simple-root chain (roots in doubled coords), orthogonal to the given vectors.""" + nb = {v: [w for w in ROOTS240 if dot(v, w) == -4] for v in ROOTS240} + for start in ROOTS240: + if any(dot(start, a) for a in orth_to): + continue + stack = [[start]] + while stack: + ch = stack.pop() + if len(ch) == n: + return ch + for w in nb[ch[-1]]: + if w not in ch and all(dot(w, u) == 0 for u in ch[:-1]) and all(dot(w, a) == 0 for a in orth_to): + stack.append(ch + [w]) + raise ValueError('no chain') + + +def an_weights(chain): + """The n+1 weights of the vector representation of A_n: w_1 - w_2 = a_1, ..., sum w = 0.""" + n = len(chain) + w1 = [Q(0)] * 8 + for t, a in enumerate(chain): + for c in range(8): + w1[c] += Q(n - t, n + 1) * a[c] + W = [tuple(w1)] + for a in chain: + W.append(tuple(x - y for x, y in zip(W[-1], a))) + return W + + +def root_basis_orthogonal_to(vecs, size): + out = [] + for v in ROOTS240: + if all(dot(v, u) == 0 for u in vecs) and q_rank(out + [list(v)]) > len(out): + out.append(list(v)) + if len(out) == size: + return [tuple(x) for x in out] + raise ValueError('basis not found') diff --git a/research/nine-term-decoder-normal-form-seed42/search.py b/research/nine-term-decoder-normal-form-seed42/search.py new file mode 100644 index 0000000000..89d02dcd7b --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/search.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Bounded heuristic search over one-sided nine-term decoders (Corollary C form). NOT a proof. + +Domain: the five frames of verify.py section F, each on P120 and on P120 minus the lines parallel to +frame normals ("self-punctured"); per-line options = every ratio class plus one generic t (exact). +Method: simulated annealing over per-line options, exact cost after every move. +Stopping rule: fixed iteration count per (frame, live set, seed); seeds 0..SEEDS-1. + + python3 -I -B research/nine-term-decoder-normal-form-seed42/search.py [--iters 3000] [--seeds 3] +""" +import argparse +import json +import math +import random +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import e8lab as E # noqa: E402 +import verify as V # noqa: E402 + + +def anneal(fr, live, iters, seed): + rng = random.Random(seed) + opts = {i: [c for t, c in fr.options(i)] for i in E.bits(live)} + Y = [E.support(b, live) for b in fr.F] + + def cost(ch): + X = [0] * 9 + for i, c in ch.items(): + for k, x in enumerate(c): + if x != 0: + X[k] |= 1 << i + return sum(E.pairing_rank(X[k], Y[k]) for k in range(9)) + ch = {i: min(o, key=lambda c: sum(1 for x in c if x != 0)) for i, o in opts.items()} + c = cost(ch) + start = best = c + temp = 1.5 + movable = [i for i in opts if len(opts[i]) > 1] + for _ in range(iters): + i = rng.choice(movable) + old = ch[i] + ch[i] = rng.choice(opts[i]) + c2 = cost(ch) + if c2 <= c or rng.random() < math.exp(-(c2 - c) / temp): + c = c2 + else: + ch[i] = old + best = min(best, c) + temp = max(0.05, temp * 0.9993) + return start, best + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--iters', type=int, default=3000) + ap.add_argument('--seeds', type=int, default=3) + ap.add_argument('--out') + a = ap.parse_args() + frames = V.build_frames() + rows = [] + for name, fr in frames.items(): + P = 0 + for b in fr.F: + for i, l in enumerate(E.LINES): + if E.q_rank([list(b), list(l)]) == 1: + P |= 1 << i + for lname, live in (('P120', E.FULL), ('self-punctured', E.FULL & ~P)): + if lname != 'P120' and P == 0: + continue + for s in range(a.seeds): + st, b = anneal(fr, live, a.iters, s) + v = E.popcount(live) + rows.append({'frame': name, 'live': lname, 'v': v, 'seed': s, 'iters': a.iters, + 'start_cost': st, 'best_cost': b, 'best_ratio': f'{b}/{v}'}) + print(f'{name:28s} {lname:15s} v={v:3d} seed={s} start={st} best={b} ratio={b / v:.4f}', flush=True) + rec = {'domain': 'verify.py section F frames x {P120, self-punctured}; per-line ratio-class options', + 'stopping_rule': f'{a.iters} annealing moves per run, seeds 0..{a.seeds - 1}', + 'comparators': {'P120 eight-term floor': 72, 'P112 shipped': '64/112', 'PR968 best ratio': '56/104'}, + 'runs': rows} + if a.out: + Path(a.out).write_text(json.dumps(rec, indent=1) + '\n') + best = min(r['best_cost'] / r['v'] for r in rows) + print(f'SEARCH_DONE runs={len(rows)} best_ratio={best:.4f} (7/13={7 / 13:.4f}, 4/7={4 / 7:.4f}); no candidate below 4/7' + if best >= 4 / 7 else f'SEARCH_DONE runs={len(rows)} best_ratio={best:.4f} CANDIDATE BELOW 4/7') + + +if __name__ == '__main__': + main() diff --git a/research/nine-term-decoder-normal-form-seed42/verify.py b/research/nine-term-decoder-normal-form-seed42/verify.py new file mode 100644 index 0000000000..994e429042 --- /dev/null +++ b/research/nine-term-decoder-normal-form-seed42/verify.py @@ -0,0 +1,467 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Nine-term complex E8 decoders: exact normal form, census facts and constructions (no new kappa). + +Standard library only, exact integer / F2 / rational arithmetic. Run from the repository root: + + python3 -I -B research/nine-term-decoder-normal-form-seed42/verify.py [--out FILE.json] + +Sections (each prints PASS/FAIL lines; exit status 1 on any FAIL): + A model: 120 lines, rank-9 label pairing, code weights + B spanning census: all 511 codeword supports span R^8 (=> every nonzero normal has full label span + on P120); all 130305 pairwise support intersections; U1 = 56, U2 = 84 + C Theorem A / Corollary B / Corollary C on explicit exact decoders (P112 and P120), the PR1180-shaped + outside-code example, a two-sided m=9 control (inexact) and an exact two-sided m=10 example + D Lemma D (merging parallel column normals) on explicit instances + E Proposition F (ratio classes, pairwise hyperplane) on every frame of section F + F weight frames of maximal subsystems (A8, A7+A1, A2+E6, A3+D5) and frame+root decoders: exact + identities on all live pairs, P120 cost formula, recorded costs + G negative controls +""" +import argparse +import hashlib +import json +import random +import sys +from collections import Counter +from fractions import Fraction as Q +from itertools import combinations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import e8lab as E # noqa: E402 + +FAILS, LOG, CERT = [], [], {} + + +def check(tag, cond, info=''): + line = ('PASS ' if cond else 'FAIL ') + tag + (' | ' + info if info else '') + print(line, flush=True) + LOG.append(line) + if not cond: + FAILS.append(tag) + + +# ============================================================================ A. model +def section_a(): + check('A1 120 lines', E.N == 120) + check('A2 label pairing F2 rank 9', E.f2_rank(E.M) == 9) + check('A3 pairing rows distinct', len(set(E.M)) == 120) + basis, words = E.code_words() + wt = Counter(E.popcount(w) for w in words) + check('A4 code weights {56:255, 64:255, 120:1}', dict(wt) == {56: 255, 64: 255, 120: 1}, str(dict(wt))) + CERT['code_weights'] = dict(wt) + return words + + +# ============================================================================ B. spanning census +def section_b(words, full_pairs=True): + ranks = Counter(E.line_rank(w) for w in words) + check('B1 every nonzero codeword support spans R^8', dict(ranks) == {8: 511}, str(dict(ranks))) + # consequence: for every nonzero normal b (real or complex), C(b) on P120 has label span 9 + # (dim V_X <= 8 iff X misses some support; C(b) misses supp(w) iff supp(w) lies in b-perp). + U1 = min(E.popcount(w) for w in words) + check('B2 U1 = 56 (largest set of label span <= 8 has 64 lines)', U1 == 56) + cnt, U2, sizes = Counter(), 120, Counter() + if full_pairs: + for a in range(len(words)): + wa = words[a] + for b in range(a + 1, len(words)): + inter = wa & words[b] + r = E.line_rank(inter) + cnt[r] += 1 + if r < 8: + sizes[(E.popcount(inter), r)] += 1 + U2 = min(U2, E.popcount(wa | words[b])) + check('B3 pairwise intersections: 130305 pairs, rank census {8:91050, 7:35640, 6:3360, 0:255}', + dict(cnt) == {8: 91050, 7: 35640, 6: 3360, 0: 255}, str(dict(cnt))) + check('B4 deficient intersections have (size, rank) in {(0,0),(28,7),(32,7),(36,6)}', + set(sizes) == {(0, 0), (28, 7), (32, 7), (36, 6)}, str(dict(sizes))) + check('B5 U2 = 84 (largest set of label span <= 7 has 36 lines)', U2 == 84) + CERT['pairwise_intersection_rank_census'] = {str(k): v for k, v in sorted(cnt.items())} + CERT['deficient_intersection_size_rank'] = {f'{s},{r}': v for (s, r), v in sorted(sizes.items())} + CERT['U1'], CERT['U2'] = U1, U2 if full_pairs else None + + +# ============================================================================ frames and representations +class Frame: + """Nine column normals b_0..b_8 (doubled coordinates, rational) spanning R^8 with one dependency z.""" + + def __init__(self, name, vecs): + self.name = name + self.F = [tuple(Q(x) for x in v) for v in vecs] + if len(self.F) != 9 or E.q_rank([list(v) for v in self.F]) != 8: + raise ValueError('a frame needs nine vectors spanning R^8') + for drop in range(9): + basis = [self.F[k] for k in range(9) if k != drop] + if E.q_rank([list(v) for v in basis]) == 8: + break + self.drop = drop + cols = [list(c) for c in zip(*basis)] # 8x8, columns = basis vectors + self.inv = E.q_inv(cols) + zb = self._solve(self.F[drop]) + self.z = self._lift(zb, Q(-1)) + if any(sum(self.z[k] * self.F[k][c] for k in range(9)) != 0 for c in range(8)): + raise ValueError('dependency check failed') + self.S = [k for k in range(9) if self.z[k] != 0] + + def _solve(self, v): + return [sum(self.inv[r][c] * v[c] for c in range(8)) for r in range(8)] + + def _lift(self, c8, at_drop): + out, j = [], 0 + for k in range(9): + if k == self.drop: + out.append(at_drop) + else: + out.append(c8[j]) + j += 1 + return out + + def base(self, i): + """One coefficient vector c with sum_k c_k b_k = 2 r_i.""" + return self._lift(self._solve([2 * Q(x) for x in E.LINES[i]]), Q(0)) + + def options(self, i): + """All supports of c0 + t z: critical t (one per ratio class) and one generic t.""" + c0 = self.base(i) + ts = sorted({-c0[k] / self.z[k] for k in self.S}) + generic = (ts[-1] + 1) if ts else Q(1) + out = [] + for t in ts + [generic]: + c = [c0[k] + t * self.z[k] for k in range(9)] + out.append((t, c)) + return out + + def sparsest(self, i): + return min(self.options(i), key=lambda tc: (sum(1 for x in tc[1] if x != 0), tc[0]))[1] + + +def T_entry(j, b): + return sum(Q(a) * x for a, x in zip(E.LINES[j], b)) / 4 # in true units + + +def exact_on_pairs(rows, F, live): + """D T^T = 2 G on all live pairs, where T_jk = .""" + idx = list(E.bits(live)) + Tm = {j: [T_entry(j, b) for b in F] for j in idx} + for i in idx: + d = rows[i] + for j in idx: + if sum(x * y for x, y in zip(d, Tm[j])) != 2 * E.G[i][j]: + return False, (i, j) + return True, len(idx) ** 2 + + +def decoder_cost(rows, F, live): + X = [0] * len(F) + for i in E.bits(live): + for k, x in enumerate(rows[i]): + if x != 0: + X[k] |= 1 << i + Y = [E.support(b, live) for b in F] + per = [E.pairing_rank(X[k], Y[k]) for k in range(len(F))] + return per, X, Y + + +def coordinate_frame(): + F0 = [] + for i in range(E.N): + if all(E.G[i][j] == 0 for j in F0): + F0.append(i) + if len(F0) == 8: + return F0 + + +# ============================================================================ C. normal form +def decompose(D, T, live): + """Theorem A decomposition D = R A' + N1, T = R B' + N2 with R^T N = 0 (exact).""" + idx = list(E.bits(live)) + R = [[Q(x) for x in E.LINES[i]] for i in idx] + Rt = E.transpose(R) + G0inv = E.q_inv(E.matmul(Rt, R)) + P = E.matmul(G0inv, Rt) # 8 x L left inverse + A = E.matmul(P, D) + B = E.matmul(P, T) + N1 = [[d - r for d, r in zip(drow, rrow)] for drow, rrow in zip(D, E.matmul(R, A))] + N2 = [[d - r for d, r in zip(drow, rrow)] for drow, rrow in zip(T, E.matmul(R, B))] + return R, A, B, N1, N2 + + +def is_zero(Mx): + return all(x == 0 for row in Mx for x in row) + + +def theorem_a_checks(tag, D, T, live, expect_one_sided=True): + R, A, B, N1, N2 = decompose(D, T, live) + Rt = E.transpose(R) + m = len(D[0]) + ABt = E.matmul(A, E.transpose(B)) + # doubled coordinates: R R^T = 4 G, so D T^T = 2G = R R^T / 2 gives A' B'^T = I/2 + check(f'{tag} A\'B\'^T = I/2 (doubled coordinates)', + all(ABt[r][c] == (Q(1, 2) if r == c else 0) for r in range(8) for c in range(8))) + check(f'{tag} R^T N1 = 0 and R^T N2 = 0', is_zero(E.matmul(Rt, N1)) and is_zero(E.matmul(Rt, N2))) + check(f'{tag} N1 B\'^T = 0, A\' N2^T = 0, N1 N2^T = 0', + is_zero(E.matmul(N1, E.transpose(B))) and is_zero(E.matmul(A, E.transpose(N2))) + and is_zero(E.matmul(N1, E.transpose(N2)))) + zs = E.q_nullspace(B, m) + ys = E.q_nullspace(A, m) + check(f'{tag} dim ker B\' = dim ker A\' = m-8 = {m - 8}', len(zs) == len(ys) == m - 8) + pair = [[sum(a * b for a, b in zip(y, z)) for z in zs] for y in ys] + check(f'{tag} ker A\' x ker B\' dot pairing nondegenerate', E.q_rank(pair) == m - 8) + n1z, n2z = is_zero(N1), is_zero(N2) + if m == 9 and expect_one_sided: + check(f'{tag} Corollary B: at most one factor leaves the root code', n1z or n2z, + f'N1 zero={n1z}, N2 zero={n2z}') + return n1z, n2z + + +def section_c(rng): + F0 = coordinate_frame() + P112 = E.FULL + for i in F0: + P112 &= ~(1 << i) + out = {} + # C1: coordinate frame + one extra root column normal, random rational t per line (Corollary C form) + extra = next(i for i in range(E.N) if i not in F0 and sum(1 for f in F0 if E.G[i][f]) == 4) + fr = Frame('coord+root', [E.LINES[f] for f in F0] + [E.LINES[extra]]) + for lname, live in (('P120', E.FULL), ('P112', P112)): + rows = {} + for i in E.bits(live): + c0 = fr.base(i) + t = Q(rng.randint(-7, 7), rng.randint(1, 5)) + rows[i] = [c0[k] + t * fr.z[k] for k in range(9)] + ok, info = exact_on_pairs(rows, fr.F, live) + check(f'C1 {lname}: random one-sided 9-term decoder (frame+root, random t_i) is exact', ok, str(info)) + idx = list(E.bits(live)) + D = [rows[i] for i in idx] + T = [[T_entry(j, b) for b in fr.F] for j in idx] + n1z, n2z = theorem_a_checks(f'C1 {lname}', D, T, live) + check(f'C1 {lname}: row factor leaves the root code, column factor does not', (not n1z) and n2z) + per, X, Y = decoder_cost(rows, fr.F, live) + out[f'C1_{lname}_random_cost'] = sum(per) + # C2: PR1180-shaped outside-code identity on P112: (R0+e)R0^T + sum_{j>=1} Rj Rj^T + (-e)R0^T + idx = list(E.bits(P112)) + ell = idx[0] + # columns R_j = (true units) for the coordinate frame lines f_j; an orthogonal frame of + # norm-2 roots has sum_j f_j f_j^T = 2I, so sum_j R_j R_j^T = 2G + cols = [[Q(E.dot(E.LINES[i], E.LINES[f]), 4) for i in idx] for f in F0] + D = [[cols[j][a] + (Q(1) if (j == 0 and idx[a] == ell) else 0) for j in range(8)] + + [Q(-1) if idx[a] == ell else Q(0)] for a in range(len(idx))] + T = [[cols[j][a] for j in range(8)] + [cols[0][a]] for a in range(len(idx))] + DT = E.matmul(D, E.transpose(T)) + ok = all(DT[a][b] == 2 * E.G[idx[a]][idx[b]] for a in range(len(idx)) for b in range(len(idx))) + check('C2 PR1180-shaped outside-code nine-term identity exact on all 12544 P112 pairs', ok) + n1z, n2z = theorem_a_checks('C2', D, T, P112) + check('C2 its outside-code part sits in D only', (not n1z) and n2z) + # C3: control -- two-sided junk at m = 9 is never exact + rows = {i: fr.sparsest(i) for i in E.bits(E.FULL)} + idx = list(E.bits(E.FULL)) + D = [rows[i] for i in idx] + T = [[T_entry(j, b) for b in fr.F] for j in idx] + R, A, B, N1, N2 = decompose(D, T, E.FULL) + z = E.q_nullspace(B, 9)[0] + y = E.q_nullspace(A, 9)[0] + zy = sum(a * b for a, b in zip(z, y)) + check('C3 z.y != 0 at m = 9', zy != 0, str(zy)) + # a vector n in ker R^T: n = e_l - R (R^T R)^-1 R^T e_l + Rt = E.transpose(R) + G0inv = E.q_inv(E.matmul(Rt, R)) + + def kernel_vec(a): + e = [[Q(int(b == a))] for b in range(len(idx))] + proj = E.matmul(R, E.matmul(G0inv, E.matmul(Rt, e))) + return [e[b][0] - proj[b][0] for b in range(len(idx))] + nvec, mvec = kernel_vec(3), kernel_vec(17) + D2 = [[D[a][k] + nvec[a] * z[k] for k in range(9)] for a in range(len(idx))] + T2 = [[T[a][k] + mvec[a] * y[k] for k in range(9)] for a in range(len(idx))] + D1ok = all(sum(x * w for x, w in zip(D2[a], T[b])) == 2 * E.G[idx[a]][idx[b]] + for a in range(0, 120, 7) for b in range(0, 120, 5)) + check('C3 one-sided junk n z^T alone keeps exactness (sampled pairs)', D1ok) + bad = sum(1 for a in range(len(idx)) for b in range(len(idx)) + if sum(x * w for x, w in zip(D2[a], T2[b])) != 2 * E.G[idx[a]][idx[b]]) + check('C3 control: two-sided junk (n z^T, m y^T) at m = 9 is inexact', bad > 0, f'{bad} wrong entries') + # C4: m = 10 admits exact two-sided junk (z1 . y = 0 possible) + b9 = next(i for i in range(E.N) if i not in F0 and i != extra and sum(1 for f in F0 if E.G[i][f]) == 4) + F10 = [tuple(Q(x) for x in E.LINES[f]) for f in F0] + [tuple(Q(x) for x in E.LINES[extra]), + tuple(Q(x) for x in E.LINES[b9])] + D10 = [fr.sparsest(i) + [Q(0)] for i in idx] + T10 = [[T_entry(j, b) for b in F10] for j in idx] + R, A, B, N1, N2 = decompose(D10, T10, E.FULL) + zs = E.q_nullspace(B, 10) + ys = E.q_nullspace(A, 10) + # choose z in ker B' and y in ker A' with z.y = 0 + z = zs[0] + a0 = sum(p * q for p, q in zip(ys[0], z)) + a1 = sum(p * q for p, q in zip(ys[1], z)) + y = [a1 * p - a0 * q for p, q in zip(ys[0], ys[1])] + check('C4 m = 10: found z in ker B\', y in ker A\' with z.y = 0, y != 0', + sum(p * q for p, q in zip(z, y)) == 0 and any(y)) + D3 = [[D10[a][k] + nvec[a] * z[k] for k in range(10)] for a in range(len(idx))] + T3 = [[T10[a][k] + mvec[a] * y[k] for k in range(10)] for a in range(len(idx))] + DT = E.matmul(D3, E.transpose(T3)) + ok = all(DT[a][b] == 2 * E.G[idx[a]][idx[b]] for a in range(len(idx)) for b in range(len(idx))) + check('C4 m = 10 decoder with junk on both factors is exact on all 14400 pairs', ok) + n1z, n2z = theorem_a_checks('C4', D3, T3, E.FULL, expect_one_sided=False) + check('C4 both factors leave the root code (Corollary B is specific to m = 9)', (not n1z) and (not n2z)) + CERT['section_C'] = out + + +# ============================================================================ D. merging lemma +def section_d(rng): + F0 = coordinate_frame() + # b_8 parallel to b_0: dependency support |S| = 2 + vecs = [E.LINES[f] for f in F0] + [tuple(2 * x for x in E.LINES[F0[0]])] + fr = Frame('parallel', vecs) + check('D1 dependency support of a parallel pair is {0, 8}', fr.S == [0, 8], str(fr.S)) + worst = None + for trial in range(40): + rows = {} + for i in E.bits(E.FULL): + c0 = fr.base(i) + t = Q(rng.randint(-5, 5), rng.randint(1, 3)) + rows[i] = [c0[k] + t * fr.z[k] for k in range(9)] + per, X, Y = decoder_cost(rows, fr.F, E.FULL) + # merge: column 8 = 2 * column 0 -> single term with row c_0 + 2 c_8 + merged = {i: [rows[i][0] + 2 * rows[i][8]] + rows[i][1:8] for i in rows} + mper, _, _ = decoder_cost(merged, fr.F[:8], E.FULL) + ok, _ = exact_on_pairs(merged, fr.F[:8], E.FULL) if trial == 0 else (True, 0) + if trial == 0: + check('D2 merged eight-term decoder is exact on all 14400 pairs', ok) + d = sum(per) - sum(mper) + worst = d if worst is None else min(worst, d) + check('D3 merging never increases cost (40 random one-sided decoders)', worst >= 0, f'min saving {worst}') + + +# ============================================================================ E/F. frames +def build_frames(): + frames = {} + frames['A8 weights'] = E.an_weights(E.simple_chain(8)) + a1 = E.ROOTS240[0] + frames['A7 weights + A1 root'] = E.an_weights(E.simple_chain(7, orth_to=(a1,))) + [a1] + ch2 = E.simple_chain(2) + frames['A2 weights + E6 root basis'] = E.an_weights(ch2) + E.root_basis_orthogonal_to(ch2, 6) + ch3 = E.simple_chain(3) + frames['A3 weights + D5 root basis'] = E.an_weights(ch3) + E.root_basis_orthogonal_to(ch3, 5) + F0 = coordinate_frame() + extra = next(i for i in range(E.N) if i not in F0 and sum(1 for f in F0 if E.G[i][f]) == 4) + frames['coordinate frame + root'] = [E.LINES[f] for f in F0] + [E.LINES[extra]] + return {k: Frame(k, v) for k, v in frames.items()} + + +def section_e(frames): + for name, fr in frames.items(): + # ratio-class vectors v_kk' = z_k' a_k - z_k a_k' where a_k = coefficient functional of base rep + # computed by the identity c0_k(i) = : test nonvanishing via lines + nonzero = True + hyper = True + for k, kk in combinations(fr.S, 2): + vals = [] + for i in range(E.N): + c0 = fr.base(i) + vals.append(fr.z[kk] * c0[k] - fr.z[k] * c0[kk]) # = + if all(v == 0 for v in vals): + nonzero = False + # lines with an option avoiding both k and kk have = 0 + for i in range(E.N): + for t, c in fr.options(i): + if c[k] == 0 and c[kk] == 0 and vals[i] != 0: + hyper = False + check(f'E1 {name}: v_kk\' != 0 for all {len(fr.S) * (len(fr.S) - 1) // 2} masked pairs', nonzero) + check(f'E2 {name}: a line avoiding two masked terms is orthogonal to v_kk\'', hyper) + # each option's avoided masked set is one ratio class + ok = True + for i in range(E.N): + c0 = fr.base(i) + for t, c in fr.options(i): + av = {k for k in fr.S if c[k] == 0} + if av != {k for k in fr.S if c0[k] / fr.z[k] == -t}: + ok = False + check(f'E3 {name}: every option avoids exactly one ratio class of masked terms', ok) + + +def section_f(frames): + res = {} + for name, fr in frames.items(): + rows = {i: fr.sparsest(i) for i in range(E.N)} + ok, info = exact_on_pairs(rows, fr.F, E.FULL) + check(f'F1 {name}: sparsest-representation 9-term decoder exact on all 14400 pairs', ok, str(info)) + per, X, Y = decoder_cost(rows, fr.F, E.FULL) + ydims = [E.label_dim(y) for y in Y] + xdims = [E.label_dim(x) for x in X] + check(f'F2 {name}: P120 cost formula rho_k = dim V_Xk (all column supports span 9)', + all(d == 9 for d in ydims) and per == xdims) + spars = Counter(sum(1 for x in rows[i] if x != 0) for i in range(E.N)) + res[name] = {'masked_terms': len(fr.S), 'P120_term_costs': per, 'P120_cost': sum(per), + 'row_support_sizes': [E.popcount(x) for x in X], 'sparsity': dict(sorted(spars.items()))} + print(f' {name}: |S|={len(fr.S)} cost={sum(per)} per-term={per} |X|={res[name]["row_support_sizes"]}') + a8 = res['A8 weights'] + check('F3 A8 frame: every line is 2- or 3-sparse (36 + 84)', a8['sparsity'] == {2: 36, 3: 84}) + check('F4 A8 frame: every row support has 36 = 120 - U2 lines, yet label span 9; cost 81', + a8['row_support_sizes'] == [36] * 9 and a8['P120_cost'] == 81) + check('F5 no frame of section F beats the eight-term P120 floor 72', + min(r['P120_cost'] for r in res.values()) >= 72, str({k: v['P120_cost'] for k, v in res.items()})) + CERT['frames'] = res + + +# ============================================================================ G. controls +def section_g(frames, rng): + fr = frames['A8 weights'] + rows = {i: fr.sparsest(i) for i in range(E.N)} + bad = dict(rows) + i0 = 5 + k0 = next(k for k in range(9) if bad[i0][k] != 0) + bad[i0] = list(bad[i0]) + bad[i0][k0] += Q(1, 3) + ok, _ = exact_on_pairs(bad, fr.F, E.FULL) + check('G1 control: perturbing one coefficient breaks exactness', not ok) + bad = dict(rows) + bad[i0] = [x if k != k0 else Q(0) for k, x in enumerate(rows[i0])] + ok, _ = exact_on_pairs(bad, fr.F, E.FULL) + check('G2 control: deleting one support entry breaks exactness', not ok) + try: + Frame('rank7', [E.LINES[0]] * 9) + check('G3 control: a rank-deficient frame is rejected', False) + except ValueError: + check('G3 control: a rank-deficient frame is rejected', True) + flipped = list(E.M) + flipped[0] ^= 1 << 7 + saved = E.M[:] + E.M[:] = flipped + r = E.f2_rank(E.M) + E.M[:] = saved + check('G4 control: a flipped label entry changes the pairing rank away from 9', r != 9, str(r)) + check('G5 control: label_dim of a single line is 1, of C(root) is 9', + E.label_dim(1) == 1 and E.label_dim(E.support(E.LINES[0])) == 9) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--out', help='write the JSON certificate here') + ap.add_argument('--quick', action='store_true', help='skip the 130305-pair census (section B3-B5)') + args = ap.parse_args() + rng = random.Random(42) + print('== A model'); words = section_a() + print('== B spanning census'); section_b(words, full_pairs=not args.quick) + print('== C normal form'); section_c(rng) + print('== D merging'); section_d(rng) + frames = build_frames() + print('== E ratio classes'); section_e(frames) + print('== F frames'); section_f(frames) + print('== G controls'); section_g(frames, rng) + CERT['log'] = LOG + CERT['fails'] = FAILS + if args.out: + Path(args.out).write_text(json.dumps(CERT, indent=1, sort_keys=True) + '\n') + npass = sum(1 for l in LOG if l.startswith('PASS')) + if FAILS: + print(f'FAIL_NINE_TERM_NORMAL_FORM_S42 failures={len(FAILS)}: {FAILS}') + sys.exit(1) + pairs = 'skipped' if args.quick else '130305' + print(f'PASS_NINE_TERM_NORMAL_FORM_S42 checks={npass} pairs={pairs} frames={len(frames)} ' + f'A8_cost={CERT["frames"]["A8 weights"]["P120_cost"]}') + + +if __name__ == '__main__': + main() From 00e6ed0810b8ebc7f6133e2c036d0f1c9a3a4162 Mon Sep 17 00:00:00 2001 From: joaqcoo Date: Tue, 13 Oct 2026 17:23:31 -0300 Subject: [PATCH 2/2] Record concurrent masked-decoder PRs 1212/1213 in overlap notes Co-Authored-By: Claude Opus 5.5 --- .../README.md | 4 +++ .../SOURCES.json | 34 +++++++++++++++---- 2 files changed, 32 insertions(+), 6 deletions(-) diff --git a/research/nine-term-decoder-normal-form-seed42/README.md b/research/nine-term-decoder-normal-form-seed42/README.md index 9b80020d0c..9cf8ecd3ed 100644 --- a/research/nine-term-decoder-normal-form-seed42/README.md +++ b/research/nine-term-decoder-normal-form-seed42/README.md @@ -154,6 +154,10 @@ What `verify.py` checks: - **@mightyOil (PR1191, PR1197, open, concurrent):** one-sided mask rigidity for masked identities, and restricted P112 ten-term cases. These are adjacent scopes that neither contain nor are contained in this one. +- **@burntout76 (PR1212)** and **@DavidAriasC (PR1213), open, concurrent:** rank-8 gauge rigidity and the + P112 connected component for *masked (E-graph-only) eight-term* decoders. Both list nine or more terms + as open, and both are disjoint from this all-pairs nine-term scope. The final overlap scan covered open + PRs through #1221. - **@3xcalibur-tech (PR1171):** the support-union hierarchy (U1, U2) is re-derived here independently. - Also credited: PR620 (GamingPuzzled), PR446 Theorem C (DreamingOfClouds) and the selected supplier lineage. All code here is independently written; nothing is vendored. diff --git a/research/nine-term-decoder-normal-form-seed42/SOURCES.json b/research/nine-term-decoder-normal-form-seed42/SOURCES.json index 2feace29b8..a36ca6604a 100644 --- a/research/nine-term-decoder-normal-form-seed42/SOURCES.json +++ b/research/nine-term-decoder-normal-form-seed42/SOURCES.json @@ -6,14 +6,36 @@ "kappa": "836330098538459/500000000000000000" }, "cited_on_main": { - "research/complex-frame-pair-decoders/PROOF.md": {"pr": 968, "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74"}, - "research/complex-decoder-field-extension-seed44/README.md": {"pr": 1077, "sha256": "788a99eef3f187c2cbff6d490933fcc8f8e7fd15d1b685c188023605916887d4"} + "research/complex-frame-pair-decoders/PROOF.md": { + "pr": 968, + "sha256": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74" + }, + "research/complex-decoder-field-extension-seed44/README.md": { + "pr": 1077, + "sha256": "788a99eef3f187c2cbff6d490933fcc8f8e7fd15d1b685c188023605916887d4" + } }, "cited_open_prs_not_imported": { - "1180": {"head": "75b408646d558147a4eb250fc407d1fbfcb8df4e", "file": "research/e8-factor-linear-overcomplete47/PROOF.md", "sha256": "98f9663c7340363debd239679cc45931e0db638f006e8742cdf0d876ea09a64a"}, - "1191": {"head": "640b43bb13d3d476a2d83b74ef0d33f14d1b5711"}, - "1197": {"head": "a0935afff6cc5540a582c5881bc8d5f98b587357"}, - "1171": {"head": "ab74c73b5b512f459b9be97680f41390d45a3bf3"} + "1180": { + "head": "75b408646d558147a4eb250fc407d1fbfcb8df4e", + "file": "research/e8-factor-linear-overcomplete47/PROOF.md", + "sha256": "98f9663c7340363debd239679cc45931e0db638f006e8742cdf0d876ea09a64a" + }, + "1191": { + "head": "640b43bb13d3d476a2d83b74ef0d33f14d1b5711" + }, + "1197": { + "head": "a0935afff6cc5540a582c5881bc8d5f98b587357" + }, + "1171": { + "head": "ab74c73b5b512f459b9be97680f41390d45a3bf3" + }, + "1212": { + "head": "072ae2f43d5c249a31e5d6ed266bfef3924417f3" + }, + "1213": { + "head": "8867cf20fbe0d3960f68bcffca118a5ac0624f7f" + } }, "vendored": {}, "note": "All code in this package is written independently; no predecessor code is executed or vendored. Cited theorems are used only where stated in PROOF.md."