From b6de532eff668a7daf8f2f98668f97af5af41338 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 15:17:23 +0000 Subject: [PATCH] feat(research): prove optimal recovery for longer mode-preserving chains Over all fixed mode-preserving integer frames on the #5444 matrix, the depth-t refined chain has optimal worst-case fiber exactly F^t for t <= 26, with a direct-sum criterion on the binary images, and strictly more for t >= 27. Answers open question 3 of PR6327. --- .../FRAMES.json | 1 + .../refined-recovery-longer-chains/PROOF.md | 148 +++++++++++ .../refined-recovery-longer-chains/README.md | 107 ++++++++ .../SOURCES.json | 42 +++ .../refined-recovery-longer-chains/TASK.json | 95 +++++++ .../VERIFY.json | 36 +++ .../build_frames.py | 130 +++++++++ .../refined-recovery-longer-chains/verify.py | 247 ++++++++++++++++++ 8 files changed, 806 insertions(+) create mode 100644 research/refined-recovery-longer-chains/FRAMES.json create mode 100644 research/refined-recovery-longer-chains/PROOF.md create mode 100644 research/refined-recovery-longer-chains/README.md create mode 100644 research/refined-recovery-longer-chains/SOURCES.json create mode 100644 research/refined-recovery-longer-chains/TASK.json create mode 100644 research/refined-recovery-longer-chains/VERIFY.json create mode 100644 research/refined-recovery-longer-chains/build_frames.py create mode 100644 research/refined-recovery-longer-chains/verify.py diff --git a/research/refined-recovery-longer-chains/FRAMES.json b/research/refined-recovery-longer-chains/FRAMES.json new file mode 100644 index 0000000000..ecc2011e2e --- /dev/null +++ b/research/refined-recovery-longer-chains/FRAMES.json @@ -0,0 +1 @@ +{"schema":"refined-recovery-longer-chains-frames-v1","E_coords":[0,1,2,4],"stages":26,"lattice_basis_rows":[3,5,6,7,8,9,10,31],"V_blocks":[[[[3,-1],[5,1],[9,-1],[11,1]],[[3,-2],[5,1],[6,-2],[7,1],[9,-3],[10,-1],[12,1],[31,2]],[[3,-2],[5,1],[6,-2],[7,1],[8,1],[9,-2],[10,-1],[13,1],[31,2]],[[3,-2],[5,1],[6,-2],[7,1],[8,1],[9,-3],[14,1],[31,2]]],[[[3,-1],[6,-2],[7,1],[8,1],[9,-2],[10,-1],[15,1],[31,2]],[[3,-2],[5,1],[6,-1],[7,2],[9,-3],[10,-1],[16,1],[31,2]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,2],[10,1],[17,1],[31,-2]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[18,1],[31,-2]]],[[[3,1],[6,1],[7,-2],[8,-1],[9,2],[10,1],[19,1],[31,-2]],[[3,-2],[5,1],[6,-1],[7,1],[9,-3],[20,1],[31,2]],[[3,-1],[6,-1],[7,1],[9,-2],[10,-1],[21,1],[31,2]],[[3,2],[5,-1],[6,1],[7,-1],[8,-1],[9,2],[22,1],[31,-2]]],[[[3,1],[6,1],[7,-1],[8,-1],[9,1],[10,1],[23,1],[31,-2]],[[3,1],[6,1],[7,-1],[8,-1],[9,2],[24,1],[31,-2]],[[3,4],[5,-2],[6,3],[7,-3],[8,-2],[9,6],[10,2],[25,1],[26,1],[31,-6]],[[3,4],[5,-2],[6,3],[7,-4],[8,-3],[9,6],[10,2],[25,1],[27,1],[31,-6]]],[[[3,4],[5,-2],[6,3],[7,-4],[8,-2],[9,7],[10,2],[25,1],[28,1],[31,-6]],[[3,4],[5,-2],[6,3],[7,-4],[8,-2],[9,6],[10,3],[25,1],[29,1],[31,-6]],[[3,5],[5,-3],[6,3],[7,-4],[8,-2],[9,7],[10,2],[25,1],[30,1],[31,-6]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[10,1],[25,1],[31,-3]]],[[[3,2],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,1],[25,1],[31,-4],[32,1]],[[3,2],[5,-1],[6,1],[7,-3],[8,-1],[9,3],[10,2],[25,1],[31,-4],[33,1]],[[3,3],[5,-2],[6,1],[7,-3],[8,-1],[9,4],[10,1],[25,1],[31,-4],[34,1]],[[3,2],[5,-1],[6,2],[7,-2],[8,-2],[9,3],[10,1],[25,1],[31,-4],[35,1]]],[[[3,2],[5,-1],[7,-2],[8,-1],[9,3],[25,1],[31,-2],[36,1]],[[3,1],[7,-2],[8,-1],[9,2],[10,1],[25,1],[31,-2],[37,1]],[[3,2],[5,-1],[6,2],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[38,1]],[[3,2],[5,-1],[6,2],[7,-3],[8,-2],[9,3],[10,2],[25,1],[31,-4],[39,1]]],[[[3,3],[5,-2],[6,2],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[40,1]],[[3,2],[5,-1],[7,-1],[8,-1],[9,2],[25,1],[31,-2],[41,1]],[[3,1],[7,-1],[8,-1],[9,1],[10,1],[25,1],[31,-2],[42,1]],[[3,1],[7,-1],[8,-1],[9,2],[25,1],[31,-2],[43,1]]],[[[3,3],[5,-1],[6,1],[7,-2],[8,-1],[9,4],[10,1],[25,1],[31,-4],[44,1]],[[3,3],[5,-1],[6,1],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[45,1]],[[3,3],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,2],[25,1],[31,-4],[46,1]],[[3,4],[5,-2],[6,1],[7,-3],[8,-1],[9,5],[10,1],[25,1],[31,-4],[47,1]]],[[[3,1],[5,-1],[7,-2],[8,-1],[9,1],[10,1],[25,1],[31,-2],[48,1]],[[3,1],[5,-1],[7,-2],[8,-1],[9,2],[25,1],[31,-2],[49,1]],[[7,-2],[8,-1],[9,1],[10,1],[25,1],[31,-2],[50,1]],[[3,1],[5,-1],[7,-1],[9,1],[10,1],[25,1],[31,-2],[51,1]]],[[[3,1],[5,-1],[7,-1],[9,2],[25,1],[31,-2],[52,1]],[[7,-1],[9,1],[10,1],[25,1],[31,-2],[53,1]],[[3,1],[5,-1],[7,-1],[8,-1],[9,1],[25,1],[31,-2],[54,1]],[[7,-1],[8,-1],[10,1],[25,1],[31,-2],[55,1]]],[[[7,-1],[8,-1],[9,1],[25,1],[31,-2],[56,1]],[[3,1],[7,-1],[8,-1],[9,1],[25,1],[31,-2],[57,1]],[[3,3],[5,-2],[6,2],[7,-3],[8,-2],[9,4],[10,2],[25,1],[31,-4],[58,1]],[[3,3],[5,-2],[6,2],[7,-3],[8,-2],[9,5],[10,1],[25,1],[31,-4],[59,1]]],[[[3,2],[5,-1],[6,2],[7,-3],[8,-2],[9,4],[10,2],[25,1],[31,-4],[60,1]],[[3,1],[7,-2],[8,-1],[9,2],[25,1],[31,-2],[61,1]],[[3,1],[7,-2],[8,-1],[9,1],[10,1],[25,1],[31,-2],[62,1]],[[3,2],[5,-1],[7,-2],[8,-1],[9,2],[25,1],[31,-2],[63,1]]],[[[3,3],[5,-2],[6,2],[7,-2],[8,-2],[9,4],[10,1],[25,1],[31,-4],[64,1]],[[3,2],[5,-1],[6,2],[7,-2],[8,-2],[9,3],[10,2],[25,1],[31,-4],[65,1]],[[3,2],[5,-1],[6,2],[7,-2],[8,-2],[9,4],[10,1],[25,1],[31,-4],[66,1]],[[3,3],[5,-2],[6,1],[7,-3],[8,-1],[9,4],[10,2],[25,1],[31,-4],[67,1]]],[[[3,3],[5,-2],[6,1],[7,-3],[8,-1],[9,5],[10,1],[25,1],[31,-4],[68,1]],[[3,2],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,2],[25,1],[31,-4],[69,1]],[[3,3],[5,-2],[6,1],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[70,1]],[[3,2],[5,-1],[6,1],[7,-3],[8,-2],[9,3],[10,2],[25,1],[31,-4],[71,1]]],[[[3,2],[5,-1],[6,1],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[72,1]],[[3,3],[5,-2],[6,1],[7,-2],[8,-1],[9,4],[10,1],[25,1],[31,-4],[73,1]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[10,2],[25,1],[31,-4],[74,1]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,4],[10,1],[25,1],[31,-4],[75,1]]],[[[3,2],[5,-1],[6,1],[7,-2],[8,-2],[9,3],[10,1],[25,1],[31,-4],[76,1]],[[3,4],[5,-2],[6,3],[7,-4],[8,-2],[9,6],[10,2],[25,1],[31,-6],[77,1]],[[3,-1],[6,-1],[9,-1],[25,1],[78,1]],[[3,3],[5,-1],[6,1],[7,-3],[8,-1],[9,4],[10,1],[25,1],[31,-4],[79,1]]],[[[3,1],[5,-1],[7,-2],[8,-1],[9,2],[10,1],[25,1],[31,-2],[80,1]],[[3,3],[5,-1],[6,2],[7,-3],[8,-2],[9,4],[10,1],[25,1],[31,-4],[81,1]],[[3,1],[5,-1],[7,-1],[8,-1],[9,1],[10,1],[25,1],[31,-2],[82,1]],[[3,1],[5,-1],[7,-1],[8,-1],[9,2],[25,1],[31,-2],[83,1]]],[[[7,-1],[8,-1],[9,1],[10,1],[25,1],[31,-2],[84,1]],[[3,-1],[9,-1],[85,1]],[[3,1],[5,-1],[6,2],[7,-1],[8,-1],[9,2],[10,1],[31,-2],[86,1]],[[3,1],[5,-1],[6,1],[7,-2],[8,-1],[9,2],[10,1],[31,-2],[87,1]]],[[[3,1],[5,-1],[6,1],[7,-1],[9,2],[10,1],[31,-2],[88,1]],[[3,1],[5,-1],[6,1],[7,-1],[8,-1],[9,1],[10,1],[31,-2],[89,1]],[[3,1],[5,-1],[6,1],[7,-1],[8,-1],[9,2],[31,-2],[90,1]],[[6,1],[7,-1],[8,-1],[9,1],[10,1],[31,-2],[91,1]]],[[[3,-2],[5,1],[6,-2],[7,1],[8,1],[9,-3],[10,-1],[31,2],[92,1]],[[3,2],[5,-1],[6,1],[7,-2],[8,-1],[9,3],[10,1],[31,-2],[93,1]],[[3,-2],[5,1],[6,-1],[7,1],[9,-3],[10,-1],[31,2],[94,1]],[[3,2],[5,-1],[6,1],[7,-1],[8,-1],[9,2],[10,1],[31,-2],[95,1]]],[[[3,2],[5,-1],[6,1],[7,-1],[8,-1],[9,3],[31,-2],[96,1]],[[3,1],[6,1],[7,-1],[8,-1],[9,2],[10,1],[31,-2],[97,1]],[[6,-1],[7,-1],[98,1]],[[6,-1],[8,1],[99,1]]],[[[6,-1],[9,-1],[100,1]],[[6,-1],[10,-1],[101,1]],[[3,-1],[5,1],[6,-1],[9,-1],[102,1]],[[7,-1],[8,-1],[103,1]]],[[[7,1],[9,-1],[104,1]],[[7,1],[10,-1],[105,1]],[[3,-1],[5,1],[7,1],[9,-1],[106,1]],[[8,-1],[9,-1],[107,1]]],[[[8,-1],[10,-1],[108,1]],[[3,-1],[5,1],[8,-1],[9,-1],[109,1]],[[9,-1],[10,1],[110,1]],[[3,1],[5,-1],[111,1]]]]} diff --git a/research/refined-recovery-longer-chains/PROOF.md b/research/refined-recovery-longer-chains/PROOF.md new file mode 100644 index 0000000000..34a5f56d60 --- /dev/null +++ b/research/refined-recovery-longer-chains/PROOF.md @@ -0,0 +1,148 @@ +# Longer refined chains over mode-preserving frames + +All objects are those of CubeJerry's PR6327 (`research/refined-native-recovery`), +for the literal 112×8 matrix M pinned from #5444 in +`research/precision-state-frontier/FIXTURE.json`. + +## 1. Statement + +R is nearest-integer rounding with half ties away from zero, and +K(z)=z−M R(Mᵀz/52). The source facts are MᵀM=56I, C=ker_F2(M mod 2) is the +self-dual [8,4,4] code, and F=W_C(13,1)/16=(13^8+14·13^4+1)/16=51,008,161. +Let G={U∈GL_112(Z): MᵀU=Mᵀ}. Fix t≥1 and U_1,…,U_(t−1)∈G with no parity +restriction. The chain is + + z_1=K(2x), z_(j+1)=K(U_j z_j), y=z_t. + +Write W_j=(U_(j−1)⋯U_1)^−1 (W_1=I) and N_j=im_F2(W_j M mod 2). + +**Theorem.** + +(a) Every frame sequence has |fiber(0)| ≥ F^t. Equality holds exactly when +N_1,…,N_t form a direct sum. + +(b) If N_1,…,N_t form a direct sum, every output has fiber at most F^t. +The maximum fiber is then exactly F^t. + +(c) For this M, every N_j lies in one fixed 104-dimensional subspace and has +dimension 4. A direct sum therefore needs t≤26. FRAMES.json gives an +explicit sequence for t=26, so every t≤26 is attained by a prefix. + +Consequently, over all mode-preserving frame sequences, + + min_U max_y |fiber(y)| = F^t for 1≤t≤26, + min_U max_y |fiber(y)| > F^t for t≥27. + +The minimum packed tag at depth t≤26 is ceil(t·log2 F) bits. That is 26, +52, 77, … and 666 bits at t=26, compared with ceil(log2 A_t) for the +parity-I class. At t=2 this recovers PR6327's 52-bit theorem and its +direct-sum criterion (2). + +## 2. Fiber parametrization + +Put m_j=Mᵀz_j. Since MᵀU_j=Mᵀ and MᵀM=56I, the j-th kernel call has quotient +q_j=R(Mᵀ(U_(j−1)z_(j−1))/52)=R(m_(j−1)/52), with m_0=2Mᵀx, and +m_j=m_(j−1)−56q_j. Going backward from s=Mᵀy, + + q_t∈Q(s), q_(t−1)∈Q(s+56q_t), …, q_1∈Q(s+56(q_2+⋯+q_t)), (1) + +per mode coordinate, where Q(s)={q: R((s+56q)/52)=q}. Reverse execution gives + + 2x = Σ_j W_j M q_j + W_t y. (2) + +Conversely every chain (1) with integral x in (2) is a preimage: forward +execution reproduces each m_j, and therefore each q_j. Forward execution is +deterministic and reproduces the chain of each preimage. The map from +preimages to chains (1) satisfying the parity condition + + Σ_j (W_j M) q̄_j ≡ W_t y (mod 2) (3) + +is therefore a bijection. verify.py replays (2) on random inputs at depth +3 and depth 26 for the constructed frames. + +PR6327's CHAIN_PROOF Section 2 proves that Q(s) is a nonempty interval of at +most 13 consecutive integers for every integer s, retaining ties. It also +proves Q(56w)=[−6,6]−14w. verify.py rechecks both on a finite window. The +general statement is the predecessor's. + +## 3. Box lemma + +Let B=I_1×⋯×I_8 with each I_k an interval of at most 13 integers, and let +c∈F2^8. Then #{q∈B: q̄∈c+C} ≤ F. + +Proof. C is self-dual with |C|=16, so 1[v∈c+C]=16^−1 Σ_(h∈C)(−1)^(h·(v+c)). +Summing over B factorizes per coordinate. The h_k=0 factor is |I_k|≤13. +The h_k=1 factor is a signed sum of consecutive ±1 values, so it has +absolute value at most 1. The triangle inequality gives the bound +16^−1 Σ_(h∈C) 13^(8−wt h)=W_C(13,1)/16=F. verify.py also checks the maximum +exhaustively at length 13, over every start parity and every coset. + +## 4. Proof of (b) + +Assume that N_1,…,N_t form a direct sum. The kernel of each W_j M mod 2 is +C, because W_j is invertible modulo 2. Equation (3) then has no solution, +or it fixes each component W_j M q̄_j uniquely. Hence there are fixed +cosets with q̄_j∈c_j+C for all j, and they depend only on y. Count the +chains (1) from stage t down to stage 1. Once q_t,…,q_(j+1) are fixed, +q_j ranges over a box of intervals of length at most 13 with parity in +c_j+C. By Section 3 there are at most F choices. The fiber therefore has +at most F^t points. This argument conditions stage by stage, so it avoids +PR6327's joint Fourier majorant, which that package shows fails for three +quotient parities. + +## 5. Proof of (a) + +At y=0, (1) with Q(56w)=[−6,6]−14w gives q_j=r_j−14q_(j+1) with free +r_j∈[−6,6]^8, so q̄_j=r̄_j. The zero fiber is therefore + + Σ_(u∈ker) Π_j 7^(8−wt u_j) 6^(wt u_j), + ker = {(u_1,…,u_t): Σ_j W_j M u_j ≡ 0 (mod 2)}. + +The kernel contains C^t, and that part contributes exactly +Π_j W_C(7,6)=F^t. Every term is positive. The kernel equals C^t exactly when +its dimension is 4t, that is, when dim(N_1+⋯+N_t)=4t, which is the direct +sum condition. Otherwise the zero fiber exceeds F^t. As a consistency +check, verify.py evaluates this formula with every N_j=im M for t=1,2,3 +and recovers PR6327's parity-I maximum A_t. + +## 6. Proof of (c) + +Let K=ker_Z(Mᵀ), a lattice of rank 104. For U∈G, Mᵀ(U^−1−I)=0, so +W_j M q ∈ Mq+K. Hence every N_j lies in im_F2(M mod 2)+red_2(K), where +red_2(K)=(K+2Z^112)/2Z^112 has dimension at most rank K=104. + +im_F2(M mod 2) lies inside red_2(K). The lattice MᵀZ^112 contains 2Z^8: +verify.py expresses each 2e_i through eight source rows recorded in +FRAMES.json. So 28q=Mᵀw for an integer w, and Mq−2w∈K reduces to Mq mod 2. +All N_j therefore lie in red_2(K), of dimension at most 104. Each N_j has +dimension 4, so a direct sum requires 4t≤104. + +Construction. E has rows e_0ᵀ,e_1ᵀ,e_2ᵀ,e_4ᵀ, as in PR6327, and E M mod 2 +has rank 4 with kernel C. FRAMES.json gives 25 integer blocks V_2,…,V_26 +of four columns each, with MᵀV_j=0 and E V_j=0 (zero on rows 0,1,2,4). +Put V_1=0 and + + W_j=I+V_jE, U_j=W_(j+1)^−1 W_j = I+(V_j−V_(j+1))E. + +Since E V=0, matrices of the form I+XE multiply by adding the X's. So +U_j∈GL_112(Z) with inverse I−(V_j−V_(j+1))E, MᵀU_j=Mᵀ, and +(U_(j−1)⋯U_1)^−1=W_j. verify.py checks MᵀV_j=0 and E V_j=0. It then forms +all 26 binary images of W_j M directly and finds total rank 104=4·26. Any +prefix of a direct sum is a direct sum, so this attains (b) for every t≤26. + +The blocks are lifts of an F2-basis of the kernel of the map +u↦Mᵀũ mod 2Λ on the 108 non-E coordinates, with Λ=MᵀZ^112. They are +chosen to be independent of im M. build_frames.py regenerates FRAMES.json +deterministically. verify.py does not trust that derivation; it checks the +stated properties of the committed integers. + +## 7. Scope + +This is a scoped proof with an exact finite certificate for one interface: +fixed known frames in G, one relative precision bit before the first call, +unbounded exact integers and complete output access. It does not cover +mode-changing frames, input-dependent frames, extra refinement between +calls, finite ranges or physical tags. It supplies no codec beyond the +count, no physical memory saving and no κ. The output function changes +with the frames, as PR6327 notes at t=2. For t≥27 only the strict +inequality is proved; the exact optimum there is open. diff --git a/research/refined-recovery-longer-chains/README.md b/research/refined-recovery-longer-chains/README.md new file mode 100644 index 0000000000..3fd64c60a0 --- /dev/null +++ b/research/refined-recovery-longer-chains/README.md @@ -0,0 +1,107 @@ +# Refined recovery over longer mode-preserving frame chains + +This package answers open question 3 of CubeJerry's +[PR6327](https://github.com/CrocSwap/integer-mult-bounds/pull/6327) +(`research/refined-native-recovery`) for every chain depth. That question +asked for the optimal recovery alphabet of longer parity-changing chains. + +The setting is PR6327's. M is the literal 112×8 matrix pinned from #5444. +K(z)=z−M R(Mᵀz/52) uses half-away rounding. The chain is z_1=K(2x), +z_(j+1)=K(U_j z_j), with one precision bit and fixed frames U_j∈GL_112(Z) +satisfying MᵀU_j=Mᵀ and no parity restriction. Put F=51,008,161, PR6327's +one-step maximum. + +## Result + +**Theorem** (scoped proof with an exact finite certificate): + +- For every depth t and every frame sequence, the zero output has at least + F^t preimages. Equality holds exactly when the t binary images of the + cumulative framed matrices W_jM form a direct sum. +- When they form a direct sum, every output has at most F^t preimages. +- For this M, all such images lie in one 104-dimensional binary subspace, + so a direct sum exists only for t≤26. An explicit 26-stage source frame + sequence attains it. + +Hence the optimal worst-case fiber over all mode-preserving frames is +**exactly F^t for 1≤t≤26** and **strictly larger than F^t for t≥27**. The +minimum packed tag is ceil(t·log₂F) bits for t≤26: 26, 52, 77, …, 666 bits. +At t=2 this reproduces PR6327's 52-bit theorem and its separation criterion. +For comparison, PR6327's parity-I chains need ceil(log₂A_t) bits, with +A_t=(13^(8t)+14·13^(4t)+1)/16. + +**The new step.** PR6327 shows that its joint Fourier majorant fails for +three quotient parities. The upper bound here does not use a joint majorant. +Under a direct sum, each stage's parity coset is fixed by the output alone. +Conditioning stage by stage then leaves a box of at most 13 values per mode, +and that box holds at most F points of one C-coset. The dimension cap comes +from 2Z^8⊂MᵀZ^112, which puts im(M mod 2) inside the reduction of +ker_Z Mᵀ, a space of dimension at most 104. + +[PROOF.md](PROOF.md) gives the argument. [FRAMES.json](FRAMES.json) holds +the 25 sparse integer blocks V_j. The frames are U_j=I+(V_j−V_(j+1))E, +with E the rows 0,1,2,4 of PR6327's construction. +[build_frames.py](build_frames.py) regenerates the blocks deterministically. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library only: + +```sh +python3.12 -I -W error -B research/refined-recovery-longer-chains/verify.py +python3.12 -I -W error -O -B research/refined-recovery-longer-chains/verify.py +python3.12 -B scripts/research_package.py --package research/refined-recovery-longer-chains +python3.12 -B research/refined-recovery-longer-chains/build_frames.py "$SCRATCH/FRAMES.json" +cmp "$SCRATCH/FRAMES.json" research/refined-recovery-longer-chains/FRAMES.json +``` + +Each verifier run prints `PASS_REFINED_RECOVERY_LONGER_CHAINS` in under a +second. It checks the following exactly: + +- the fixture hash, MᵀM=56I, the code C and F=W_C(13,1)/16; +- that Q(s) is an interval of at most 13 integers on s∈[−4000,4000]; +- the box-coset maximum F, over every start parity and coset; +- an integer expression of each 2e_i in source rows; +- the frame blocks: MᵀV_j=0, E V_j=0, and rank 104 of all 26 binary images; +- the inverse identity 2x=Σ W_jMq_j+W_t y on random inputs at depths 3 and 26; +- that the zero-fiber formula reproduces PR6327's A_t for parity-I chains at t=1,2,3. + +Controls confirm that a perturbed block breaks MᵀV=0 and a repeated frame +breaks the direct sum. + +## Limitations + +The all-depth statements are proved in PROOF.md. The finite checks cover the +source facts, the box lemma at maximal length and the explicit frames. The +predecessor's interval lemma (Q(s) has at most 13 elements for every s) is +cited from PR6327's CHAIN_PROOF and only rechecked on a window. For t≥27, +only the strict inequality is proved. The interface assumptions are PR6327's: +fixed known frames, unbounded exact integers and complete output access. The +output function changes with the frames. No codec, physical tag, caller or +restoration cost is supplied. **No κ change.** The selected frontier and its +five assumptions are unchanged. No independent human review or formal proof +kernel check has been done. + +## Open next questions + +1. **What is the exact optimum at t≥27?** The images must overlap there. The + zero-fiber kernel formula in PROOF.md Section 5 gives a lower bound for + each overlap pattern. First step: minimize that sum at t=27 over image + configurations in the 104-dimensional space. Blocker: with overlapping + images, stage cosets are coupled, so the stage-wise box bound no longer + applies as stated. +2. **Mode-changing frames or extra refinement between calls.** First step: + derive the coupled quotient congruences for one mode-changing frame at + depth two. Blocker: the per-mode scalar recursion no longer separates. +3. **A physical caller.** Can a caller accept the framed output and use the + t·log₂F tag at a favorable complete cost? Blocker: no accepting caller or + restoration invoice is known. + +## Credit + +This package was produced by Nick Petalas. CubeJerry's PR6327 supplies the +chain model, the scalar interval lemma, the t=2 theorem, the E rows and the +open question. zxv's #5444 supplies the matrix and the one-step code facts. +Ali Romman's #5323 and Brian's #5035 are credited for the same-grid counts +and the rounded kernel, as in PR6327. Character sums over self-dual codes +are classical. New work is Apache-2.0. diff --git a/research/refined-recovery-longer-chains/SOURCES.json b/research/refined-recovery-longer-chains/SOURCES.json new file mode 100644 index 0000000000..0ea1cc8565 --- /dev/null +++ b/research/refined-recovery-longer-chains/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/precision-state-frontier/FIXTURE.json", + "usage": "input", + "git_blob": "0aa9f7816378c3eb11ec2e3d63ed9e85cfaa893c", + "sha256": "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" + }, + { + "path": "research/refined-native-recovery/CHAIN_PROOF.md", + "usage": "provenance", + "git_blob": "e6af4bbcbb97daf0ccb4361337fd54e871a48553", + "sha256": "5b64a5a4a42f99ae8e094fdd20a9fbbcb54c2af4fbabfea8e58a351991a4e06a" + }, + { + "path": "research/refined-native-recovery/PROOF.md", + "usage": "provenance", + "git_blob": "26abf5db19ca6aff04cebd6d9847c37c1021fa6a", + "sha256": "d54eac2e7d464ff30f9eada02b049435ca48dfb335e37e74a3c1cc67871aedb9" + }, + { + "path": "research/refined-native-recovery/README.md", + "usage": "provenance", + "git_blob": "a5d15573e107cf814824c3377b1497ace81c90ce", + "sha256": "59bc2410dd267df849831eff8db65579f856ed40cdf77172c505d84c4b894df1" + } + ] +} diff --git a/research/refined-recovery-longer-chains/TASK.json b/research/refined-recovery-longer-chains/TASK.json new file mode 100644 index 0000000000..aef007fae6 --- /dev/null +++ b/research/refined-recovery-longer-chains/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Optimal worst-case recovery alphabet for depth-t refined chains over all fixed mode-preserving integer frames on the #5444 matrix: F^t exactly for t<=26 with a direct-sum criterion, strictly larger for t>=27; explicit 26-stage frame certificate.", + "scope_change_reason": "Answers open question 3 of PR6327 (longer parity-changing chains). It is a precision-state accounting theorem in the analytic_recovery interface, not a caller-bound discharge of a selected assumption.", + "bottleneck_link": "Side result for exact history accounting before reversible precision can be implemented; it fixes composition-state counts for the inherited rounded interface and does not change any supplier invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the sharp all-depth mode-preserving theorem with the explicit 26-stage source frame; leave t>=27 optima, mode-changing frames and physical tags open.", + "outcome": "completed", + "evidence": "PROOF.md; FRAMES.json regenerated by build_frames.py; verify.py in normal and optimized Python.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact optimal maximum fiber at depth t>=27, where the binary images must overlap?", + "why_it_matters": "It completes the depth law for this interface; the zero-fiber kernel formula gives the lower bound for any fixed overlap pattern.", + "first_step": "At t=27 minimise the zero-fiber kernel sum over admissible image configurations in the 104-dimensional space, then test whether the stage-by-stage box bound extends when one stage's coset depends on another's.", + "blocked_by": "With overlapping images the parity cosets of different stages are coupled, so the stage-wise box lemma no longer applies directly." + }, + { + "question": "Does the depth law change for mode-changing frames or extra refinement between calls?", + "why_it_matters": "Those are the remaining frame classes listed by PR6327.", + "first_step": "Derive the coupled quotient congruences for one mode-changing frame at depth two.", + "blocked_by": "The per-mode scalar recursion (1) no longer separates." + }, + { + "question": "Can an actual caller accept the changed output map and use the t*log2(F) tag at a favorable complete cost?", + "why_it_matters": "Only then would the count become a physical memory saving.", + "first_step": "Bind one caller and price restoration of the framed output.", + "blocked_by": "No accepting caller or restoration invoice is known." + } + ] +} diff --git a/research/refined-recovery-longer-chains/VERIFY.json b/research/refined-recovery-longer-chains/VERIFY.json new file mode 100644 index 0000000000..35f1b7c034 --- /dev/null +++ b/research/refined-recovery-longer-chains/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/precision-state-frontier/FIXTURE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fixture pin, MᵀM=56I and code C, scalar interval and box-coset lemma, 2Z^8 in MᵀZ^112, 26-stage frame certificate (MᵀV=0, EV=0, direct-sum rank 104), inverse-chain replay, parity-I A_t consistency and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fixture pin, MᵀM=56I and code C, scalar interval and box-coset lemma, 2Z^8 in MᵀZ^112, 26-stage frame certificate (MᵀV=0, EV=0, direct-sum rank 104), inverse-chain replay, parity-I A_t consistency and rejecting controls." + } + ] +} diff --git a/research/refined-recovery-longer-chains/build_frames.py b/research/refined-recovery-longer-chains/build_frames.py new file mode 100644 index 0000000000..fb43a28db8 --- /dev/null +++ b/research/refined-recovery-longer-chains/build_frames.py @@ -0,0 +1,130 @@ +"""Build the 26-stage frame certificate FRAMES.json (standard library only). + +Each frame block is an integer 112x4 matrix V_j with M^T V_j = 0 and V_j +zero on the coordinates E = (0, 1, 2, 4). The cumulative inverse frames are +W_j = I + V_j E (W_1 = I). Usage: build_frames.py OUTPUT.json +""" +import itertools +import json +import pathlib +import sys +from fractions import Fraction + +HERE = pathlib.Path(__file__).resolve().parent +FIXTURE = HERE.parent / "precision-state-frontier" / "FIXTURE.json" +E_COORDS = (0, 1, 2, 4) +N, MODES, STAGES = 112, 8, 26 + + +def load_rows(): + cols = json.loads(FIXTURE.read_text())["mode_columns"] + return [tuple(cols[j][i] for j in range(MODES)) for i in range(N)] + + +def det(rows): + a = [[Fraction(x) for x in r] for r in rows] + d = Fraction(1) + for c in range(len(a)): + p = next((r for r in range(c, len(a)) if a[r][c] != 0), None) + if p is None: + return Fraction(0) + if p != c: + a[c], a[p] = a[p], a[c] + d = -d + d *= a[c][c] + for r in range(c + 1, len(a)): + f = a[r][c] / a[c][c] + a[r] = [x - f * y for x, y in zip(a[r], a[c])] + return d + + +def solve(rows_t, rhs): + """Solve B c = rhs for square B given as list of columns' transpose rows.""" + n = len(rhs) + a = [[Fraction(rows_t[k][i]) for k in range(n)] + [Fraction(rhs[i])] for i in range(n)] + for c in range(n): + p = next(r for r in range(c, n) if a[r][c] != 0) + a[c], a[p] = a[p], a[c] + a[c] = [x / a[c][c] for x in a[c]] + for r in range(n): + if r != c and a[r][c] != 0: + f = a[r][c] + a[r] = [x - f * y for x, y in zip(a[r], a[c])] + return [a[i][n] for i in range(n)] + + +def main(out_path): + rho = load_rows() + free = [i for i in range(N) if i not in E_COORDS] + # Lattice Lambda = M^T Z^112 has index 16; find 8 free rows forming a basis. + basis = None + for combo in itertools.combinations(free[:40], MODES): + if abs(det([rho[i] for i in combo])) == 16: + basis = combo + break + assert basis is not None + brows = [rho[i] for i in basis] + + def coords(vec): + c = solve(brows, vec) + assert all(x.denominator == 1 for x in c) + return [int(x) for x in c] + + phi = {i: sum((coords(rho[i])[k] & 1) << k for k in range(MODES)) for i in free} + # F2 kernel of phi on free coordinates (red K restricted to free coords). + piv, kern = {}, [] + for i in free: + v, u = phi[i], 1 << i + while v: + p = v.bit_length() - 1 + if p not in piv: + piv[p] = (v, u) + break + v ^= piv[p][0] + u ^= piv[p][1] + if v == 0: + kern.append(u) + # Integer lifts supported on free coordinates. + lifts = [] + for u in kern: + supp = [i for i in range(N) if (u >> i) & 1] + tot = [sum(rho[i][k] for i in supp) for k in range(MODES)] + assert all(x % 2 == 0 for x in tot) + c = coords([x // 2 for x in tot]) + vec = {i: 1 for i in supp} + for k, i in enumerate(basis): + vec[i] = vec.get(i, 0) - 2 * c[k] + vec = {i: x for i, x in vec.items() if x} + assert all(sum(x * rho[i][m] for i, x in vec.items()) == 0 for m in range(MODES)) + lifts.append(vec) + # Keep lifts independent from im(M mod 2). + span = {} + + def add(x): + while x: + p = x.bit_length() - 1 + if p not in span: + span[p] = x + return True + x ^= span[p] + return False + + for j in range(MODES): + add(sum((rho[i][j] & 1) << i for i in range(N))) + chosen = [v for v in lifts if add(sum(1 << i for i, x in v.items() if x & 1))] + assert len(chosen) == 4 * (STAGES - 1), len(chosen) + blocks = [chosen[4 * b:4 * b + 4] for b in range(STAGES - 1)] + payload = { + "schema": "refined-recovery-longer-chains-frames-v1", + "E_coords": list(E_COORDS), + "stages": STAGES, + "lattice_basis_rows": list(basis), + "V_blocks": [[sorted([int(i), int(x)] for i, x in col.items()) for col in blk] for blk in blocks], + } + pathlib.Path(out_path).write_text(json.dumps(payload, separators=(",", ":")) + "\n") + + +if __name__ == "__main__": + if len(sys.argv) != 2: + raise SystemExit("usage: build_frames.py OUTPUT.json") + main(sys.argv[1]) diff --git a/research/refined-recovery-longer-chains/verify.py b/research/refined-recovery-longer-chains/verify.py new file mode 100644 index 0000000000..2e403bc1d8 --- /dev/null +++ b/research/refined-recovery-longer-chains/verify.py @@ -0,0 +1,247 @@ +"""Exact checks for the longer-chain refined recovery theorem (stdlib only). + +Prints PASS_REFINED_RECOVERY_LONGER_CHAINS on success. +""" +import hashlib +import itertools +import json +import pathlib +import random +import sys +from fractions import Fraction + +HERE = pathlib.Path(__file__).resolve().parent +FIXTURE = HERE.parent / "precision-state-frontier" / "FIXTURE.json" +FIXTURE_SHA = "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" +N, MODES = 112, 8 +F = (13**8 + 14 * 13**4 + 1) // 16 + + +def fail(msg): + raise SystemExit("FAIL: " + msg) + + +def check(cond, msg): + if not cond: + fail(msg) + + +def rnd(fr): + """Nearest integer, half ties away from zero.""" + n, d = fr.numerator, fr.denominator + q = (2 * abs(n) + d) // (2 * d) + return q if n >= 0 else -q + + +def quot(s): + lo, hi = -((26 + s) // 4) - 2, (26 - s) // 4 + 2 + return [q for q in range(lo, hi + 1) if rnd(Fraction(s + 56 * q, 52)) == q] + + +def f2_rank(vecs): + piv, r = {}, 0 + for v in vecs: + while v: + p = v.bit_length() - 1 + if p not in piv: + piv[p] = v + r += 1 + break + v ^= piv[p] + return r + + +def load(): + raw = FIXTURE.read_bytes() + check(hashlib.sha256(raw).hexdigest() == FIXTURE_SHA, "fixture hash") + cols = json.loads(raw)["mode_columns"] + check(len(cols) == MODES and all(len(c) == N for c in cols), "fixture shape") + return [tuple(cols[j][i] for j in range(MODES)) for i in range(N)] + + +def mt(rho, vec): + """M^T vec for an integer vector (dict index->value).""" + return tuple(sum(x * rho[i][m] for i, x in vec.items()) for m in range(MODES)) + + +def source_facts(rho): + for a in range(MODES): + for b in range(MODES): + check(sum(r[a] * r[b] for r in rho) == (56 if a == b else 0), "M^T M = 56 I") + colbits = [sum((rho[i][j] & 1) << i for i in range(N)) for j in range(MODES)] + code = [q for q in range(256) if not f2_xor(colbits, q)] + check(len(code) == 16, "|C| = 16") + weights = sorted(bin(c).count("1") for c in code) + check(weights == [0] + [4] * 14 + [8], "Hamming weight enumerator") + check(all(bin(a & b).count("1") % 2 == 0 for a in code for b in code), "C self-orthogonal") + check(f2_rank(colbits) == 4, "rank M mod 2 = 4") + check(sum(13 ** (8 - bin(c).count("1")) for c in code) == 16 * F, "F = W_C(13,1)/16") + return colbits, code + + +def f2_xor(colbits, q): + v = 0 + for j in range(MODES): + if (q >> j) & 1: + v ^= colbits[j] + return v + + +def scalar_and_box(code): + for s in range(-4000, 4001): + q = quot(s) + check(q and q == list(range(q[0], q[-1] + 1)) and len(q) <= 13, "Q(s) interval <= 13") + for m in range(-60, 61): + check(quot(56 * m) == list(range(-6 - 14 * m, 7 - 14 * m)), "Q(56m) translate") + # Box lemma at maximal lengths: every start parity per coordinate, every coset. + best = 0 + for starts in range(256): + counts = [((7, 6) if (starts >> k) & 1 == 0 else (6, 7)) for k in range(MODES)] + for c in range(256): + tot = 0 + for h in code: + p = c ^ h + v = 1 + for k in range(MODES): + v *= counts[k][(p >> k) & 1] + tot += v + best = max(best, tot) + check(best == F, "box coset maximum equals F") + # Fourier coefficient bound behind the lemma: |sum (-1)^x over an interval| <= 1. + check(all(abs(sum((-1) ** x for x in range(a, a + L))) <= 1 for a in range(-3, 3) for L in range(14)), "signed interval sum") + + +def two_e_witnesses(rho): + """Integer w_i with M^T w_i = 2 e_i, so 2 Z^8 lies in M^T Z^112.""" + basis = json.loads((HERE / "FRAMES.json").read_text())["lattice_basis_rows"] + check(len(basis) == MODES, "basis size") + for i in range(MODES): + a = [[Fraction(rho[b][r]) for b in basis] + [Fraction(2 if r == i else 0)] for r in range(MODES)] + for c in range(MODES): + p = next((r for r in range(c, MODES) if a[r][c] != 0), None) + check(p is not None, "lattice basis rows independent") + a[c], a[p] = a[p], a[c] + a[c] = [x / a[c][c] for x in a[c]] + for r in range(MODES): + if r != c and a[r][c] != 0: + f = a[r][c] + a[r] = [x - f * y for x, y in zip(a[r], a[c])] + coef = [a[r][MODES] for r in range(MODES)] + check(all(x.denominator == 1 for x in coef), "2e_i in M^T Z^112") + w = {b: int(x) for b, x in zip(basis, coef) if x} + check(mt(rho, w) == tuple(2 if k == i else 0 for k in range(MODES)), "2e_i witness value") + + +def frames(rho, colbits, code): + data = json.loads((HERE / "FRAMES.json").read_text()) + ecoords = tuple(data["E_coords"]) + t = data["stages"] + check(ecoords == (0, 1, 2, 4) and t == 26, "frame header") + blocks = [[{int(i): int(x) for i, x in col} for col in blk] for blk in data["V_blocks"]] + check(len(blocks) == t - 1 and all(len(b) == 4 for b in blocks), "block shape") + for blk in blocks: + for col in blk: + check(all(x != 0 for x in col.values()), "sparse nonzero") + check(mt(rho, col) == (0,) * MODES, "M^T V = 0") + check(not any(i in col for i in ecoords), "E V = 0") + # E M mod 2 has rank 4 and kernel C. + em = [sum((rho[e][j] & 1) << j for j in range(MODES)) for e in ecoords] + check(f2_rank(em) == 4, "rank EM = 4") + check(all(all(bin(r & c).count("1") % 2 == 0 for r in em) for c in code), "ker EM contains C") + # Binary images of W_j M = M + V_j (E M), j = 1..t (V_1 = 0). + images = [] + vlist = [None] + blocks + for j in range(t): + for col in range(MODES): + v = colbits[col] + if vlist[j] is not None: + for r, e in enumerate(ecoords): + if rho[e][col] & 1: + v ^= sum(1 << i for i, x in vlist[j][r].items() if x & 1) + images.append(v) + blockrank = [f2_rank(images[MODES * j:MODES * (j + 1)]) for j in range(t)] + check(blockrank == [4] * t, "each image has dimension 4") + check(f2_rank(images) == 4 * t == 104, "direct sum of 26 binary images") + return ecoords, blocks, images + + +def apply_w(vec, blk, ecoords, sign): + """(I + sign * V E) vec for a list vector.""" + out = list(vec) + if blk is None: + return out + for r, e in enumerate(ecoords): + if vec[e]: + for i, x in blk[r].items(): + out[i] += sign * x * vec[e] + return out + + +def chain_replay(rho, ecoords, blocks, depth, seed): + """Forward chain with U_j = I + (V_j - V_(j+1)) E, then check the inverse identity.""" + rng = random.Random(seed) + vlist = [None] + blocks + + def kernel(z): + m = [sum(z[i] * rho[i][k] for i in range(N)) for k in range(MODES)] + q = [rnd(Fraction(x, 52)) for x in m] + return [z[i] - sum(rho[i][k] * q[k] for k in range(MODES)) for i in range(N)], q + + for _ in range(3): + x = [rng.randint(-10**6, 10**6) for _ in range(N)] + z, q = kernel([2 * v for v in x]) + qs = [q] + for j in range(1, depth): + # U_j z = (I - V_(j+1) E)(I + V_j E) z + u = apply_w(apply_w(z, vlist[j - 1], ecoords, 1), vlist[j], ecoords, -1) + z, q = kernel(u) + qs.append(q) + y = z + # 2x = sum_j W_j M q_j + W_t y with W_j = I + V_j E. + acc = apply_w(y, vlist[depth - 1], ecoords, 1) + for j in range(depth): + mq = [sum(rho[i][k] * qs[j][k] for k in range(MODES)) for i in range(N)] + acc = [a + b for a, b in zip(acc, apply_w(mq, vlist[j], ecoords, 1))] + check(acc == [2 * v for v in x], "inverse chain identity") + + +def parity_i_zero_fiber(code, t): + """Zero fiber when every binary image equals im M: sum_j u_j in C.""" + cnt = [7 ** (8 - w) * 6 ** w for w in range(9)] + weight = [cnt[bin(u).count("1")] for u in range(256)] + dist = {0: 1} + for _ in range(t): + new = {} + for a, va in dist.items(): + for u in range(256): + new[a ^ u] = new.get(a ^ u, 0) + va * weight[u] + dist = new + return sum(dist.get(c, 0) for c in code) + + +def main(): + rho = load() + colbits, code = source_facts(rho) + scalar_and_box(code) + two_e_witnesses(rho) + ecoords, blocks, images = frames(rho, colbits, code) + for t in (1, 2, 3): + a_t = (13 ** (8 * t) + 14 * 13 ** (4 * t) + 1) // 16 + check(parity_i_zero_fiber(code, t) == a_t, "parity-I zero fiber equals A_t") + check(parity_i_zero_fiber(code, 2) > F**2, "overlapping images enlarge the zero fiber") + chain_replay(rho, ecoords, blocks, 3, 11) + chain_replay(rho, ecoords, blocks, 26, 12) + # Negative controls. + bad = json.loads((HERE / "FRAMES.json").read_text()) + col = bad["V_blocks"][0][0] + col[0][1] += 1 + try_col = {int(i): int(x) for i, x in col} + check(mt(rho, try_col) != (0,) * MODES, "control: perturbed V leaves M^T V = 0") + dup = images[:MODES * 25] + images[MODES:2 * MODES] + check(f2_rank(dup) < 104, "control: repeated frame keeps a direct sum") + print("depth, packed bits ceil(log2 F^t):", [(t, (F**t - 1).bit_length()) for t in (1, 2, 3, 26)]) + print("PASS_REFINED_RECOVERY_LONGER_CHAINS") + + +if __name__ == "__main__": + main()