diff --git a/research/one-sided-padding-lemma/LICENSE b/research/one-sided-padding-lemma/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/one-sided-padding-lemma/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/one-sided-padding-lemma/MANIFEST.sha256 b/research/one-sided-padding-lemma/MANIFEST.sha256 new file mode 100644 index 0000000000..91fc22b024 --- /dev/null +++ b/research/one-sided-padding-lemma/MANIFEST.sha256 @@ -0,0 +1,9 @@ +# sha256 of package files +b056475ca54f685a26ff1de6ad2986fd31c4d448e02bac428afd85b9cd2443d1 README.md +e86d8e5a057cfe111013d9ff499ba4898f88c4e40a775afbf3249fb3dedc9edd PROOF_MAP.md +1ea58e398f40239c0945d495a807b33bcadeb6d5dcd147a12bf71ff06a9ed7ec NOTICE.md +c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4 LICENSE +a9029fbebed80d5530d9a770340843cfd032aac6af297d237cc24b758537ea81 requirements.txt +daade0beeb1e35574b216b8c7ee60a51c633e46bad63503fb3232f2ab4b27778 checks/pad_audit.py +402a7ebf3913ef62da52a7b20e8f2f794a4e202b24fac10ebd8a29c5f6d45039 checks/pad.py +b84b5d55ae302ffdf40ee1323c15f3b57180b9e9624a857a5556e10a73b553b8 expected/pad_audit.out diff --git a/research/one-sided-padding-lemma/NOTICE.md b/research/one-sided-padding-lemma/NOTICE.md new file mode 100644 index 0000000000..c6f3494c2c --- /dev/null +++ b/research/one-sided-padding-lemma/NOTICE.md @@ -0,0 +1,3 @@ +# Notice + +Prepared by DreamingOfClouds with Claude Opus 5.5 (Anthropic), via Claude Code; Apache-2.0 (`LICENSE`, copied from the repository root). diff --git a/research/one-sided-padding-lemma/PROOF_MAP.md b/research/one-sided-padding-lemma/PROOF_MAP.md new file mode 100644 index 0000000000..5fb4401412 --- /dev/null +++ b/research/one-sided-padding-lemma/PROOF_MAP.md @@ -0,0 +1,12 @@ +# Proof map + +| Claim | Status | Proof / check | +|---|---|---| +| (1) Padding: one-sided P112 decoder of cost c gives one-sided P120 decoder of cost exactly c+8 | proved; checked | Exactness: rows of P112 unchanged, row f_i = (2/mu)(mu e_i) = 2e_i for i in I, row f_j = 2e_j for j not in I, so P_E Y_E^T = C_E and q_k = C_E y_k (one-sided). Cost (rank B[R_k,A_k] = dim U_k - dim(U_k cap l(A_k)^perp)): non-corrected term unchanged (A_k grows, perp shrinks, U_k cap perp = 0 already); corrected term +1 (A_k gains f_i, l(A_k) = W_i + z_i = F_2^9, beta(z_i,z_i)=1); unit term exactly 1. Total c + |I| + (8-|I|) = c+8. Merging corrected terms with the same i is required first (an unmerged second term would also lose its epsilon, +1) and never raises cost (#2816 section 3.1). Check: `checks/pad.py` (5 decoders), `checks/pad_audit.py` (12 decoders incl. a split-correction decoder that exercises merging); both assert exactness over Q and equality of two cost computations. | +| (2) Lift form cost_w(S+) <= cost_w(S) + 8 - |I| | proved | Minimal basis of S extended by 0 keeps supports and weights; p_h^{E8} - ext(p_h^{X_I}) lies in span of delta_{f_j} (j not in I), each of weight 1. | +| (3) L120 suffices for the one-sided P112 floor 64+|I| for all I, i.e. Delta >= n_nf for all Delta | proved (sufficiency only) | (2) with the #2816 section 7 identity; no P120 decoder cost model is used on this route. Reading the corollary as "one-sided P120 decoders cost >= 72" additionally uses the dense-beta P120 cost model (imported, not covered by the P112-only theorem). Chain: Delta >= n_nf <= L120 <= [Delta + D <= 7 implies rho_0 <= Delta]; converse not claimed. | +| (4) delta delta^T padding is two-sided | proved | delta_{f_i} not in C(E8): codewords have |Off| >= 53. q = C_E 2e_j stays in col C_E. | +| L120 | OPEN | Residue: 38 OPEN rows of the #3049 ledger; 7 prior-only rows; 7 E6-slack rows; d=0 sliver Z = ker rho cap S nonzero with D >= 1, kappa <= 6. | + +Checks cover the 12+ decoders: coordinate; root swaps k=1..4; basis changes; overcomplete m=11; shift decoders; split swap. +Related: #2816, #2826, #2862, #2985, #3049, #3029 (conditional only on L120 via this lemma). diff --git a/research/one-sided-padding-lemma/README.md b/research/one-sided-padding-lemma/README.md new file mode 100644 index 0000000000..9fca2bc389 --- /dev/null +++ b/research/one-sided-padding-lemma/README.md @@ -0,0 +1,17 @@ +# One-sided padding lemma: P112 to P120 (no kappa claim) + +Statement and a two-implementation check; nothing here claims a kappa improvement. + +**Lemma (padding).** Every one-sided P112 decoder (case (b)) of cost c becomes a one-sided P120 (E8) decoder of cost exactly c + 8: after merging corrected terms with proportional y, for each frame line f_j with j not in the corrected set I add the term (delta_{f_j}, y = 2e_j); for i in I the corrected term gets p_k(f_i) = 2/mu. The new q = C_E * 2e_j is the E8 frame codeword, so the decoder stays one-sided. + +**Lift form.** S containing the code of X_I gives S+ (extend by 0 on f_j, j not in I, plus the unit vectors delta_{f_j}) containing C(E8), with cost_w(S+) <= cost_w(S) + 8 - |I|. + +**Consequence (sufficiency only).** L120 (every lift S containing C(E8) has cost_w >= 72) suffices for the one-sided P112 floor 64 + |I| for every I, i.e. Delta >= n_nf for all Delta, using only the #2816 section 7 identity (corrected cost = cost(X_I) - |I|). The converse is not claimed. This makes the conditional in #3029 conditional on L120 alone. + +**Remark.** Padding with delta delta^T is two-sided: delta is not a codeword (codewords have |Off| >= 53), so it enlarges col Q. The earlier remark that the reduction "does not transfer" referred to that two-sided padding. + +**OPEN (L120).** Not proved. Residue: the 38 OPEN rows of the #3049 ledger (one d=4 [7^5,4]; one d=6 [7^7,6]; four d=7; 32 d=8), the 7 prior-only rows (killed only by prior arguments), the 7 E6-slack rows (E6-cover rows, conditional), and the d=0 sliver Z = ker(rho) intersect S nonzero with D >= 1, kappa <= 6. + +Cites: #2816, #2826, #2862, #2985, #3049, #3029. + +Run `bash verify.sh` (needs `sympy`; `PYTHON=/path/to/python`). Runtime about 2 s. `PROOF_MAP.md` maps each claim to its proof and check. diff --git a/research/one-sided-padding-lemma/checks/pad.py b/research/one-sided-padding-lemma/checks/pad.py new file mode 100644 index 0000000000..18e147d9c5 --- /dev/null +++ b/research/one-sided-padding-lemma/checks/pad.py @@ -0,0 +1,132 @@ +# EXCESS: one-sided padding P112 -> P120 (E8). For a one-sided P112 decoder (P, Y; P Y^T = C) with corrected set I, +# build the one-sided E8 decoder: rows f_i (i in I) get p_k(f_i)=2/y_k[i] on the corrected term; for j not in I add term (delta_{f_j}, y=2e_j). +# Check exactness P_E Y^T = C_E (C_E rows: c_t, and 2e_j for f_j) and cost_E = cost_P112 + 8, cost by two implementations: +# (A) rank_F2 of B[R_k, A_k], B_ts = 1 + mod 2 from the root vectors (no labels); +# (B) label formula dim U_k - eps_k (Lemma 3.1 form; eps only for y ∝ f_i with z_i in U and f_i not in A_k). +# AUDIT-PAD: independent re-implementation of the EXCESS padding lemma (own E8, own frame, own labels; no base.py). +# Cost (A): rank_F2 B[R,A], B_ts = 1 + mod 2 (integer inner products). +# Cost (B): dim U - dim(U ∩ span ℓ(A)^⊥β), labels ℓ=(1, simple-root coords mod 2), β = ab + n^T Cartan n' (mod 2): subspace algebra only. +import itertools, random +from fractions import Fraction as Fr +# E8 roots in doubled coords +R2=[] +for i,j in itertools.combinations(range(8),2): + for si in (2,-2): + for sj in (2,-2): + v=[0]*8; v[i]=si; v[j]=sj; R2.append(tuple(v)) +for s in itertools.product((1,-1),repeat=8): + if s.count(-1)%2==0: R2.append(s) +assert len(R2)==240 +ip=lambda a,b: sum(x*y for x,y in zip(a,b))//4 +lines=[];seen=set() +for v in R2: + w=tuple(-x for x in v) + if w in seen: continue + seen.add(v); lines.append(v) +assert len(lines)==120 +F=[(2,2,0,0,0,0,0,0),(2,-2,0,0,0,0,0,0),(0,0,2,2,0,0,0,0),(0,0,2,-2,0,0,0,0),(0,0,0,0,2,2,0,0),(0,0,0,0,2,-2,0,0),(0,0,0,0,0,0,2,2),(0,0,0,0,0,0,2,-2)] +assert all(ip(F[i],F[j])==2*(i==j) for i in range(8) for j in range(8)) +def canon(v): + w=tuple(-x for x in v); return v if v in seen else w +Fc=[canon(f) for f in F] +P112=[l for l in lines if l not in Fc]; assert len(P112)==112 +E=P112+Fc; n=112; N=120 +G=[[ip(a,f) for f in F] for a in E] # Gram realisation rows c_t (C_E); frame rows = 2e_j +for j in range(8): assert G[n+j]==[2*(i==j) for i in range(8)] +# simple roots of E8 (doubled coords), coords of each line in that basis (solve over Q) +S=[(1,-1,-1,-1,-1,-1,-1,1),(2,2,0,0,0,0,0,0),(-2,2,0,0,0,0,0,0),(0,-2,2,0,0,0,0,0),(0,0,-2,2,0,0,0,0),(0,0,0,-2,2,0,0,0),(0,0,0,0,-2,2,0,0),(0,0,0,0,0,-2,2,0)] +def solveQ(M,b): # M square list rows; solve M x = b + m=len(M); A=[[Fr(x) for x in M[i]]+[Fr(b[i])] for i in range(m)] + for c in range(m): + p=next(r for r in range(c,m) if A[r][c]!=0); A[c],A[p]=A[p],A[c] + for r in range(m): + if r!=c and A[r][c]!=0: + f=A[r][c]/A[c][c]; A[r]=[x-f*y for x,y in zip(A[r],A[c])] + return [A[i][m]/A[i][i] for i in range(m)] +ST=[[S[k][i] for k in range(8)] for i in range(8)] +coef=[solveQ(ST,v) for v in E] +assert all(all(x.denominator==1 for x in c) for c in coef) +Cart=[[ip(a,b)%2 for b in S] for a in S] +lab=[(1,)+tuple(int(x)%2 for x in c) for c in coef] +assert len(set(lab[:n]))==112 +def beta(a,b): return (a[0]*b[0]+sum(a[1+i]*Cart[i][j]*b[1+j] for i in range(8) for j in range(8)))%2 +for t in random.Random(0).sample(range(N),30): + for s in random.Random(t).sample(range(N),30): assert beta(lab[t],lab[s])==(1+ip(E[t],E[s]))%2 + +# --- adapter names used by the checks below (E8 data from the construction above) +L=P112; F0=Fc; dot=ip; FC=G[:n]; LAB=lab[:n]; Z=lab[n:]; LABE=lab +def toint(v): return int(''.join(map(str,v)),2) +def rk(vs): + b=[] + for x in vs: + for y in b: x=min(x,x^y) + if x: b.append(x) + return len(b) +def f2rank(vs): return rk([toint(v) for v in vs]) +import sympy as sp +C=[[int(x) for x in row] for row in FC] +ROOTS=[list(r) for r in L]+[list(f) for f in F0] # 120 lines: P112 then frame +CE=C+[[2 if i==j else 0 for i in range(8)] for j in range(8)] +assert all(sum(int(dot(ROOTS[n+j],F0[i])) for _ in [0])==CE[n+j][i] for j in range(8) for i in range(8)) +def gf2rank(rows): + rows=[int(''.join(map(str,r)),2) if r else 0 for r in rows]; r=0 + basis=[] + for x in rows: + for b in basis: x=min(x,x^b) + if x: basis.append(x) + return len(basis) +def costA(R,A,lines): + return gf2rank([[ (1+int(dot(lines[t],lines[s])))%2 for s in A] for t in R]) if R and A else 0 +def costB(R,y,lab,A): + U=[lab[t] for t in R]; w=f2rank(U); nz=[i for i in range(8) if y[i]!=0] + # label span of A is full unless y ∝ f_i and no line of A has label outside W_i (Lemma 3.1 + frame lines) + if len(nz)==1: + i=nz[0] + Alab=[lab[s] for s in A] + if f2rank(Alab)==8 and f2rank(U+[Z[i]])==w and f2rank(Alab+[Z[i]])==9: return w-1 + return w +def cost(Pcols,Y,lines,lab,N): + ca=cb=0 + for k,col in enumerate(Pcols): + y=list(Y[k]); R=[t for t in range(N) if col[t]!=0] + if not R or all(v==0 for v in y): continue + A=[s for s in range(N) if sum(sp.Rational(CE[s][i])*y[i] for i in range(8))!=0] + ca+=costA(R,A,lines); cb+=costB(R,y,lab,A) + return ca,cb +def solve(cols): + P=sp.Matrix(n,len(cols),lambda t,k: cols[k][t]); sol,par=P.gauss_jordan_solve(sp.Matrix(C)) + Y=sol.subs({s:0 for s in sol.free_symbols}); assert P*Y==sp.Matrix(C); return Y +def pad_and_check(cols,tag): + Y=solve(cols); Yl=[list(Y.row(k)) for k in range(len(cols))] + c112=cost(cols,Yl,ROOTS,LABE,n) + # corrected set + Ecols=[c+[0]*8 for c in cols]; EY=[y[:] for y in Yl]; I=[] + for k,y in enumerate(Yl): + nz=[i for i in range(8) if y[i]!=0]; R=[t for t in range(n) if cols[k][t]!=0] + if len(nz)==1 and f2rank([LAB[t] for t in R]+[Z[nz[0]]])==f2rank([LAB[t] for t in R]) and nz[0] not in I: + i=nz[0]; I.append(i); Ecols[k][n+i]=sp.Rational(2)/y[i] + for j in range(8): + if j not in I: + c=[0]*(n+8); c[n+j]=1; Ecols.append(c); EY.append([2 if i==j else 0 for i in range(8)]) + PE=sp.Matrix(n+8,len(Ecols),lambda t,k: Ecols[k][t]); YE=sp.Matrix(EY) + assert PE*YE==sp.Matrix(CE), 'exactness' + cE=cost(Ecols,EY,ROOTS,LABE,n+8) + print(tag,'I=',sorted(I),'P112 cost (A,B)=',c112,' E8 one-sided cost (A,B)=',cE, 'diff', cE[0]-c112[0]) + assert c112[0]==c112[1] and cE[0]==cE[1] and cE[0]==c112[0]+8 +# coordinate decoder +pad_and_check([[C[t][l] for t in range(n)] for l in range(8)],'coord') +def swap(J,roots): + cols=[[C[t][l] for t in range(n)] for l in range(8) if l not in J] + for r in roots: + pr=[sum(C[t][i]*C[r][i] for i in range(8)) for t in range(n)]; pr[r]=0; cols.append(pr) + d=[0]*n; d[r]=1; cols.append(d) + return cols +for k in (1,2,3,4): + for J in itertools.combinations(range(8),k): + rs=[] + for m in J: + cand=[t for t in range(n) if C[t][m]!=0 and all(C[t][j]==0 for j in J if j!=m) and t not in rs] + if not cand: break + rs.append(cand[0]) + else: pad_and_check(swap(list(J),rs),'swap k=%d J=%s'%(k,J)); break +print('PAD OK') diff --git a/research/one-sided-padding-lemma/checks/pad_audit.py b/research/one-sided-padding-lemma/checks/pad_audit.py new file mode 100644 index 0000000000..baf13a1122 --- /dev/null +++ b/research/one-sided-padding-lemma/checks/pad_audit.py @@ -0,0 +1,174 @@ +# AUDIT-PAD: independent re-implementation of the EXCESS padding lemma (own E8, own frame, own labels; no base.py). +# Cost (A): rank_F2 B[R,A], B_ts = 1 + mod 2 (integer inner products). +# Cost (B): dim U - dim(U ∩ span ℓ(A)^⊥β), labels ℓ=(1, simple-root coords mod 2), β = ab + n^T Cartan n' (mod 2): subspace algebra only. +import itertools, random +from fractions import Fraction as Fr +# E8 roots in doubled coords +R2=[] +for i,j in itertools.combinations(range(8),2): + for si in (2,-2): + for sj in (2,-2): + v=[0]*8; v[i]=si; v[j]=sj; R2.append(tuple(v)) +for s in itertools.product((1,-1),repeat=8): + if s.count(-1)%2==0: R2.append(s) +assert len(R2)==240 +ip=lambda a,b: sum(x*y for x,y in zip(a,b))//4 +lines=[];seen=set() +for v in R2: + w=tuple(-x for x in v) + if w in seen: continue + seen.add(v); lines.append(v) +assert len(lines)==120 +F=[(2,2,0,0,0,0,0,0),(2,-2,0,0,0,0,0,0),(0,0,2,2,0,0,0,0),(0,0,2,-2,0,0,0,0),(0,0,0,0,2,2,0,0),(0,0,0,0,2,-2,0,0),(0,0,0,0,0,0,2,2),(0,0,0,0,0,0,2,-2)] +assert all(ip(F[i],F[j])==2*(i==j) for i in range(8) for j in range(8)) +def canon(v): + w=tuple(-x for x in v); return v if v in seen else w +Fc=[canon(f) for f in F] +P112=[l for l in lines if l not in Fc]; assert len(P112)==112 +E=P112+Fc; n=112; N=120 +G=[[ip(a,f) for f in F] for a in E] # Gram realisation rows c_t (C_E); frame rows = 2e_j +for j in range(8): assert G[n+j]==[2*(i==j) for i in range(8)] +# simple roots of E8 (doubled coords), coords of each line in that basis (solve over Q) +S=[(1,-1,-1,-1,-1,-1,-1,1),(2,2,0,0,0,0,0,0),(-2,2,0,0,0,0,0,0),(0,-2,2,0,0,0,0,0),(0,0,-2,2,0,0,0,0),(0,0,0,-2,2,0,0,0),(0,0,0,0,-2,2,0,0),(0,0,0,0,0,-2,2,0)] +def solveQ(M,b): # M square list rows; solve M x = b + m=len(M); A=[[Fr(x) for x in M[i]]+[Fr(b[i])] for i in range(m)] + for c in range(m): + p=next(r for r in range(c,m) if A[r][c]!=0); A[c],A[p]=A[p],A[c] + for r in range(m): + if r!=c and A[r][c]!=0: + f=A[r][c]/A[c][c]; A[r]=[x-f*y for x,y in zip(A[r],A[c])] + return [A[i][m]/A[i][i] for i in range(m)] +ST=[[S[k][i] for k in range(8)] for i in range(8)] +coef=[solveQ(ST,v) for v in E] +assert all(all(x.denominator==1 for x in c) for c in coef) +Cart=[[ip(a,b)%2 for b in S] for a in S] +lab=[(1,)+tuple(int(x)%2 for x in c) for c in coef] +assert len(set(lab[:n]))==112 +def beta(a,b): return (a[0]*b[0]+sum(a[1+i]*Cart[i][j]*b[1+j] for i in range(8) for j in range(8)))%2 +for t in random.Random(0).sample(range(N),30): + for s in random.Random(t).sample(range(N),30): assert beta(lab[t],lab[s])==(1+ip(E[t],E[s]))%2 +def toint(v): return int(''.join(map(str,v)),2) +def basis(vs): + b=[] + for x in vs: + for y in b: x=min(x,x^y) + if x: b.append(x) + return b +def rk(vs): return len(basis(vs)) +def costA(Rr,Aa): return rk([toint([(1+ip(E[t],E[s]))%2 for s in Aa]) for t in Rr]) if Rr and Aa else 0 +def costB(Rr,Aa): + if not Rr or not Aa: return 0 + U=[lab[t] for t in Rr]; Al=[lab[s] for s in Aa] + # perp of span(Al): solve beta(x,a)=0 for all a, x in F2^9 (brute 512) + perp=[x for x in itertools.product((0,1),repeat=9) if all(beta(x,a)==0 for a in basis_vecs(Al))] + Ub=rk([toint(u) for u in U]); Pb=rk([toint(p) for p in perp]) + inter=Ub+Pb-rk([toint(u) for u in U]+[toint(p) for p in perp]) + return Ub-inter +def basis_vecs(vs): + out=[];b=[] + for v in vs: + x=toint(v) + for y in b: x=min(x,x^y) + if x: b.append(x); out.append(v) + return out +def decoder_cost(cols,Y,Nl): + ca=cb=0 + for col,y in zip(cols,Y): + Rr=[t for t in range(Nl) if col[t]!=0] + Aa=[s for s in range(Nl) if sum(G[s][i]*y[i] for i in range(8))!=0] + a=costA(Rr,Aa); b=costB(Rr,Aa); assert a==b,(a,b); ca+=a + return ca +def exact(cols,Y,Nl): + for t in range(Nl): + row=[sum(Fr(col[t])*Fr(y[i]) for col,y in zip(cols,Y)) for i in range(8)] + if row!=[Fr(x) for x in G[t]]: return False + return True +def corrected(col,y): + nz=[i for i in range(8) if y[i]!=0] + if len(nz)!=1: return None + i=nz[0]; Rr=[t for t in range(n) if col[t]!=0]; z=lab[n+i] + return i if rk([toint(lab[t]) for t in Rr]+[toint(z)])==rk([toint(lab[t]) for t in Rr]) else None +def merge(cols,Y): # merge corrected terms with proportional y (normalisation) + out=[];outY=[];seenI={} + for col,y in zip(cols,Y): + i=corrected(col,y) + if i is not None and i in seenI: + k=seenI[i]; mu=Fr(y[i])/Fr(outY[k][i]); out[k]=[a+mu*b for a,b in zip(out[k],col)] + else: + if i is not None: seenI[i]=len(out) + out.append(list(col)); outY.append(list(y)) + return out,outY +def pad(cols,Y,tag): + assert exact(cols,Y,n),'P112 exactness' + c0=decoder_cost(cols,Y,n); cols,Y=merge(cols,Y); assert exact(cols,Y,n) + c=decoder_cost(cols,Y,n); assert c<=c0 + Ec=[list(col)+[0]*8 for col in cols]; EY=[list(y) for y in Y]; I=[] + for k,(col,y) in enumerate(zip(cols,Y)): + i=corrected(col,y) + if i is not None: I.append(i); Ec[k][n+i]=Fr(2)/Fr(y[i]) + for j in range(8): + if j not in I: + u=[0]*N; u[n+j]=1; Ec.append(u); EY.append([2*(i==j) for i in range(8)]) + assert exact(Ec,EY,N),'E8 exactness' + # one-sidedness: q_k = C_E y_k by construction (Y given); also N = P_E (C_E Y)^T = C_E C_E^T follows from P_E Y^T = C_E + cE=decoder_cost(Ec,EY,N) + print(f"{tag:28s} terms={len(cols):2d} I={sorted(I)} P112={c} (raw {c0}) E8={cE} diff={cE-c} ok={cE==c+8}") + return cE-c +C=[G[t] for t in range(n)] +coordcols=lambda skip=(): [[C[t][j] for t in range(n)] for j in range(8) if j not in skip] +e=lambda j,s=1:[s*(i==j) for i in range(8)] +res=[] +# 1 coordinate decoder +res.append(pad(coordcols(),[e(j) for j in range(8)],'coord')) +# 2 root swaps (own search over all J up to size 4 that admit roots) +for k in (1,2,3,4): + for J in itertools.combinations(range(8),k): + rs=[] + for m in J: + cand=[t for t in range(n) if C[t][m]!=0 and all(C[t][j]==0 for j in J if j!=m) and t not in rs] + if not cand: break + rs.append(cand[0]) + else: break + else: continue + cols=coordcols(J); Y=[e(j) for j in range(8) if j not in J] + for m,r in zip(J,rs): + p=[sum(C[t][i]*C[r][i] for i in range(8)) for t in range(n)]; a=p[r]; p[r]=0 + # p_{r} with y = C_r-direction; express: term (p_r - a δ_r, y = c_r/|c_r|^2 ...) -> use y = e_m-proportional? build via h=c_r + cols.append(p); Y.append(None); cols.append([int(t==r) for t in range(n)]); Y.append(None) + # solve Y exactly: unknown y's for the swap terms; use generic solve P Y^T = C + import sympy as sp + Pm=sp.Matrix(n,len(cols),lambda t,kk: cols[kk][t]); sol,par=Pm.gauss_jordan_solve(sp.Matrix(C)); Ys=sol.subs({s:0 for s in sol.free_symbols}) + res.append(pad(cols,[[Fr(int(sp.fraction(x)[0]),int(sp.fraction(x)[1])) for x in Ys.row(kk)] for kk in range(len(cols))],f'rootswap k={k} J={J}')) +# 3 generic basis change: P = C A, Y^T = A^{-1} (no corrections expected) +import sympy as sp +rng=random.Random(7) +for trial in range(2): + A=sp.Matrix(8,8,lambda i,j: rng.choice([0,0,1,-1,2]) + (3 if i==j else 0)) + if A.det()==0: continue + Ai=A.inv(); cols=[[sum(C[t][i]*A[i,k] for i in range(8)) for t in range(n)] for k in range(8)] + Y=[[Fr(int(sp.fraction(Ai[k,i])[0]),int(sp.fraction(Ai[k,i])[1])) for i in range(8)] for k in range(8)] + res.append(pad(cols,Y,f'basis-change {trial}')) +# 4 overcomplete m=11 one-sided: P = C A (8x11), Y^T = right inverse of A, A contains e_i columns + sparse sums +A=sp.zeros(8,11) +for i in range(8): A[i,i]=1 +A[0,8]=1;A[1,8]=1; A[2,9]=1;A[3,9]=-1;A[4,9]=1; A[5,10]=2;A[6,10]=1;A[7,10]=1 +Yt=A.T*(A*A.T).inv() # right inverse (11x8): A*Yt = I +cols=[[sum(C[t][i]*A[i,k] for i in range(8)) for t in range(n)] for k in range(11)] +Y=[[Fr(int(sp.fraction(Yt[k,i])[0]),int(sp.fraction(Yt[k,i])[1])) for i in range(8)] for k in range(11)] +res.append(pad(cols,Y,'overcomplete m=11')) +# 5 shift decoder with unit term carrying two directions; and a split-correction decoder (exercises merge) +for t0 in (0,57,90): + cols=coordcols((0,1)); Y=[e(j) for j in range(2,8)] + c1=[C[t][0]+(t==t0) for t in range(n)]; c2=[C[t][1]+(t==t0) for t in range(n)] + cols+= [c1,c2,[int(t==t0) for t in range(n)]]; Y+=[e(0),e(1),[-1,-1,0,0,0,0,0,0]] + res.append(pad(cols,Y,f'shift t0={t0}')) +# 6 root swap split into two proportional corrected terms (tests merge): take first rootswap k=1 and split its swap column +J=(0,); r=[t for t in range(n) if C[t][0]!=0][0] +p=[sum(C[t][i]*C[r][i] for i in range(8)) for t in range(n)]; a=p[r]; p[r]=0 +cols=coordcols(J)+[p,[int(t==r) for t in range(n)]] +Pm=sp.Matrix(n,len(cols),lambda t,kk: cols[kk][t]); sol,_=Pm.gauss_jordan_solve(sp.Matrix(C)); Ys=sol.subs({s:0 for s in sol.free_symbols}) +Y=[[Fr(int(sp.fraction(x)[0]),int(sp.fraction(x)[1])) for x in Ys.row(kk)] for kk in range(len(cols))] +k=len(cols)-2; half=[Fr(1,2)*x for x in cols[k]] +cols2=cols[:k]+[half,half]+cols[k+1:]; Y2=Y[:k]+[Y[k],Y[k]]+Y[k+1:] +res.append(pad(cols2,Y2,'split swap (merge)')) +print('ALL diff==8:',all(d==8 for d in res), 'n=',len(res)) diff --git a/research/one-sided-padding-lemma/requirements.txt b/research/one-sided-padding-lemma/requirements.txt new file mode 100644 index 0000000000..31a0ac42e9 --- /dev/null +++ b/research/one-sided-padding-lemma/requirements.txt @@ -0,0 +1 @@ +sympy>=1.12 diff --git a/research/one-sided-padding-lemma/verify.sh b/research/one-sided-padding-lemma/verify.sh new file mode 100755 index 0000000000..bbdfd21b31 --- /dev/null +++ b/research/one-sided-padding-lemma/verify.sh @@ -0,0 +1,19 @@ +#!/usr/bin/env bash +# Verification of research/one-sided-padding-lemma (no kappa claim). usage: bash verify.sh PYTHON=/path/to/python (needs sympy) +set -uo pipefail +HERE=$(cd "$(dirname "$0")" && pwd); PY="${PYTHON:-python3}"; export PYTHONDONTWRITEBYTECODE=1 +fail=0; ok(){ echo "PASS $1"; }; bad(){ echo "FAIL $1"; fail=1; } +"$PY" -c "import sympy" 2>/dev/null || { echo "FAIL python needs sympy (PYTHON=...)"; exit 1; } +OUT=$(mktemp -d "${TMPDIR:-/tmp}/padver.XXXXXX") +echo "== 0. manifest" +(cd "$HERE" && grep -v '^#' MANIFEST.sha256 | shasum -a 256 -c - >"$OUT/m.out" 2>&1) && ok "MANIFEST.sha256 (all files match)" || { bad "manifest"; cat "$OUT/m.out"; } +echo "== 1. pad.py (implementation 1: root-vector rank_F2 vs label formula)" +timeout 1200 "$PY" -B "$HERE/checks/pad.py" >"$OUT/pad.log" 2>&1 || bad "pad.py exit" +[ "$(grep -c 'diff 8$' "$OUT/pad.log")" = 5 ] && grep -q '^PAD OK' "$OUT/pad.log" && ok "pad.py: 5 decoders (coordinate, root swaps k=1..4), exact over Q, cost(P120)=cost(P112)+8 by both costs" || bad "pad.py output" +grep -E 'cost \(A,B\)= \(([0-9]+), \1\)' "$OUT/pad.log" | wc -l | grep -q 5 && ok "pad.py: the two cost computations agree on every decoder" || bad "pad.py A=B" +echo "== 2. pad_audit.py (implementation 2: own E8, own labels, subspace algebra, with merging)" +timeout 1200 "$PY" -B "$HERE/checks/pad_audit.py" >"$OUT/aud.log" 2>&1 || bad "pad_audit.py exit" +[ "$(grep -c 'ok=True' "$OUT/aud.log")" = 12 ] && grep -q 'ALL diff==8: True n= 12' "$OUT/aud.log" && ok "pad_audit.py: 12 decoders, each exact over Q (P112 and E8), padded cost = normalised cost + 8" || bad "pad_audit.py output" +diff -q "$OUT/aud.log" "$HERE/expected/pad_audit.out" >/dev/null && ok "pad_audit.py output identical to expected/pad_audit.out" || bad "expected output differs" +rm -rf "$OUT" +[ $fail = 0 ] && echo "ALL PASS" || { echo "SOME FAILED"; exit 1; }