Construct sharp balanced rank-one recovery cycles (no κ)

research/refined-recovery-balanced-cycle/PROOF.md

@@ -0,0 +1,169 @@
+# A sharp balanced rank-one cycle for refined recovery
+
+This scoped proof and construction were produced by Nick Petalas. Apache-2.0.
+
+## Premises and exact scope
+
+Armin Pourshafeie / apoursh's #6853 asks for a structured frame construction
+matching #6852's existential asymptotic rate. We use the affine family in
+#6851, derived from Nick Petalas's #6660 integer frames. CubeJerry's #6327
+and zxv's #5444 supply the retained rounded-native interface and matrix.
+These predecessor theorems are premises, not results proved again here.
+
+Let C be the binary self-dual [8,4,4] code. Its unique weight-eight word is
+omega = (1,...,1); its other fourteen nonzero words have weight four. Put
+Q = F2^8/C, so C = Q*. The predecessor's binary space decomposes as
+
+    V = im(mu) direct-sum R,    dim Q = 4,    dim R = d = 100.
+
+In the affine family, every stage has phi_j(q) = mu(q) + psi_j(q), with
+arbitrary binary linear psi_j: Q -> R and psi_1 = 0. Characters are pairs
+(c,b) in C x R*. Their codewords and total weights are
+
+    h_j(c,b) = c + psi_j* b,
+    W(c,b) = sum_j wt(h_j(c,b)).
+
+The Fourier error term from #6851 is
+
+    S = sum_{(c,b) != (0,0)} 13^(-W(c,b)).
+
+We prove a new sharp lower bound and an explicit equality construction
+within this family. All claims about arbitrary other mode-preserving frames
+are excluded. The combinatorial proof below works for every d >= 1; the
+integer construction specializes it to the actual d = 100.
+
+## Theorem
+
+Write L = 2^d and N = 16L. At every positive depth t,
+
+    S >= B_d(t) := (N-2) 13^(-4t) + 13^(-8t).
+
+Equality is attainable if and only if L divides t. At every positive
+multiple of L, the rank-one maps
+
+    psi_v(q) = omega(q) v,    v ranging once over R per cycle,
+
+attain equality. One can start with v = 0, so psi_1 = 0.
+
+For the actual d = 100, this gives the exact minimum of S at every positive
+multiple of 2^100. Using the predecessor's zero-fiber formula and small-error
+max-fiber theorem, the exact minimum maximum fiber in this affine family is
+
+    [13^(8t) + (2^104-2) 13^(4t) + 1] / 2^104,
+    t a positive multiple of 2^100.
+
+This is an exact symbolic formula, not an enumeration of that depth.
+The same explicit infinite periodic sequence has error exponent
+
+    lim_{t -> infinity} -log2(S(t))/t = 4 log2(13).
+
+Thus it answers #6853's structured-construction question, with an enormous
+period. It does not improve the practical depth-28 to depth-30 certificates.
+
+## Lower bound
+
+For b = 0 the contribution is exactly 14*13^(-4t) + 13^(-8t).
+Fix b != 0. At every stage, c -> c + psi_j* b permutes C. Consequently
+
+    sum_{c in C} W(c,b) = t sum_{c in C} wt(c) = 64t.
+
+Strict convexity of x -> 13^(-x) gives
+
+    sum_{c in C} 13^(-W(c,b)) >= 16*13^(-4t),
+
+with equality exactly when W(c,b) = 4t for every c. Sum over the L-1 nonzero
+b and add the fixed b = 0 contribution. This gives B_d(t), with equality
+exactly when all W(c,b) equal 4t for b != 0.
+
+## Rank-one equality construction
+
+For psi_v(q) = omega(q) v, its adjoint sends b to b(v) omega.
+For each b != 0, exactly half of R has b(v) = 0 and half has b(v) = 1.
+Complementary codewords obey
+
+    wt(c) + wt(c + omega) = 8.
+
+One cycle therefore gives W(c,b) = (L/2)*8 = 4L for every c and b != 0.
+Repeat the cycle to attain the bound at t = mL. The sole b = 0 character
+of weight eight has total weight 8t. Every other nonzero character has
+weight 4t. There are N-2 of the latter, proving the asserted spectrum.
+
+## No shorter equality length
+
+This argument permits arbitrary maps psi_j, not merely rank-one maps.
+For fixed b != 0 let n_b(a) count the j for which psi_j* b = a in C.
+Since wt(a) = 4 - 4*1[a=0] + 4*1[a=omega],
+
+    W(c,b) = 4t - 4 n_b(c) + 4 n_b(c+omega).
+
+Equality in the lower bound forces n_b(c) = n_b(c+omega) for every c.
+Choose any q in Q with omega(q) = 1. Pairing c with c+omega then gives
+
+    0 = sum_c n_b(c) (-1)^(c(q))
+      = sum_j (-1)^(b(psi_j(q)))        for every b != 0.
+
+Let m(v) count the occurrences of v in the multiset {psi_j(q)} in R.
+Every nontrivial Fourier coefficient of m vanishes, while its trivial
+coefficient is t. Fourier inversion on R gives m(v) = t/L for every v.
+These are integer multiplicities, so L divides t. In particular 2^100
+is the least positive equality depth for the actual affine family.
+
+## Integer realization and random access
+
+Use E selecting owners 0,1,2,4 and the 100 integer lifts k_i retained in
+#6660's FRAMES.json. They satisfy M^T k_i = 0 and E k_i = 0; their binary
+reductions form a basis of R. Define the integer row
+
+    lambda = e_1^T + e_2^T + e_4^T.
+
+For the literal source M, lambda M mod 2 = omega. For 0 <= a < 2^100,
+let g(a) = a XOR (a >> 1), the reflected Gray index, and put
+
+    v_a = sum_i bit_i(g(a)) k_i,
+    W_a = I + v_a lambda.
+
+Then lambda v_a = 0, so W_a^(-1) = I - v_a lambda over the integers.
+Also M^T W_a = M^T. Its binary action on M is exactly
+mu(q) + omega(q) red2(v_a), as required. In particular W_0 = I.
+The Gray map permutes all d-bit indices. Adjacent cyclic indices differ
+in one Gray bit, including the last-to-first transition. Thus
+
+    U_a = W_(a+1)^(-1) W_a = I + (v_a-v_(a+1)) lambda
+
+uses a signed single lift k_i. Both each frame change and every transition
+have rank at most one relative to I. The constructor computes any frame
+using at most 100 retained lifts; it never materializes the whole period.
+No physical instruction price for these integer maps is asserted.
+
+## Maximum fibers and the infinite sequence
+
+At t = m*2^100, B_100(t) < 2^104*2^(-4t) < 2^(-296), since t >= 100
+and 13 > 2. The inherited threshold epsilon* from #6848 is larger than
+2^(-296). For example (23/12)^8 < 256 gives
+epsilon* = 1/[13*((23/12)^8-1)] > 1/3315 > 2^(-12).
+Thus the predecessor's theorem makes the maximum fiber the zero fiber
+for this construction. Every competing affine sequence has maximum fiber
+at least its zero fiber. The Poisson formula and the sharp S bound prove
+the claimed exact optimum. The formula is integral: writing A=13^(4t),
+its value is A+(A-1)^2/2^104; 2^104 divides A-1 because
+v2(13^(4t)-1) = 4+v2(t) >= 104.
+
+For arbitrary t, a partial cycle adds only nonnegative weights, so
+
+    B_100(t) <= S(t) <= (2^104-1) 13^(-4L floor(t/L)).
+
+With the fixed constant L = 2^100, taking logarithms and dividing by t
+proves the explicit sequence's exponent. This limit does not promise useful
+convergence before a complete period.
+
+## Evidence and remaining obligations
+
+The universal statements rest on this written proof and the cited premises.
+The verifier exhausts reduced dimensions, arbitrary-map small cases and small
+Fourier occupancy multisets, and checks random-access frames against the
+actual integer matrix. Its generated hash-bound receipt states exact coverage.
+It neither enumerates the 2^100-stage period nor replays a predecessor's
+scientific verifier. No codec, physical tag acquisition, caller acceptance,
+restoration price, supplier invoice, new kappa, selected-frontier change or
+complete multiplication theorem is supplied. Independent human and formal
+proof-kernel review are unclaimed.

research/refined-recovery-balanced-cycle/README.md

@@ -0,0 +1,101 @@
+# Sharp balanced rank-one frames for refined recovery
+
+Scoped written proof with exact finite corroboration. This package was produced
+by Nick Petalas. Apache-2.0.
+
+The new explicit cycle answers structured-construction question 2 of Armin
+Pourshafeie / apoursh's [#6853](https://github.com/CrocSwap/integer-mult-bounds/pull/6853).
+Within the affine frame family of #6851, at every positive depth t,
+
+    S >= (2^104-2) 13^(-4t) + 13^(-8t).
+
+Equality is attainable exactly when 2^100 divides t. The construction enumerates
+kernel vectors in Gray order and uses only rank-one changes from the identity.
+Every transition uses one signed retained integer lift. At positive complete
+cycles the exact minimum maximum fiber within this family is
+
+    [13^(8t) + (2^104-2) 13^(4t) + 1] / 2^104.
+
+The fixed infinite sequence attains #6852's asymptotic exponent 4 log2(13)
+explicitly. Its enormous period gives no practical improvement at depths 28–30.
+The bound, construction, shortest equality depth and specialization are proved
+in [PROOF.md](PROOF.md). The full 2^100-stage period is not enumerated.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/refined-recovery-balanced-cycle
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/refined-recovery-balanced-cycle/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/refined-recovery-balanced-cycle/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/refined-recovery-balanced-cycle/cycle.py --index 7
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/refined-recovery-balanced-cycle --check-source-history
+```
+
+The scientific marker is PASS_REFINED_RECOVERY_BALANCED_CYCLE. The constructor
+prints sparse factors for W=I+v*lambda and U_to_next=I+delta*lambda, with zero-based
+owner and cycle indices. It computes any index below 2^100 without expanding the
+period. Sparse checkouts must first materialize this package and the declared
+VERIFY.json inputs. Direct verification is Git-free once those files are present.
+
+The generated stdout receipt binds every package file and live input by SHA256.
+It reports eight reduced-dimension cycles, 8,152 nonzero cycle characters,
+4,626 complete arbitrary-map sequences with 46 equality cases, 3,238 complete
+Fourier occupancy multisets, 106 integer frame sample invocations, eight
+omitted-vector spectrum controls and eight rejected API inputs. The arbitrary-map
+census fixes the first map at zero and covers d=1, t=1..4 and d=2, t=1..2.
+The occupancy census covers dimensions 1..3 and totals 1..6. The sample indices
+include all 100 individual Gray basis vectors and the cyclic wrap. These are
+finite corroborations; the universal proof is not a finite census.
+
+## Premises, credit and scope
+
+Credit apoursh #6853 for the question and finite-depth construction, #6851 for
+the affine character model and #6852 for the existential optimal rate; Nick
+Petalas #6660 for the integer frame family and retained lifts; CubeJerry #6327
+and zxv #5444 for the rounded-native interface and literal matrix. The inherited
+Poisson and small-error maximum-fiber implications are premises. Their exact
+source bytes are pinned in SOURCES.json. No predecessor scientific executable
+is imported or replayed. Their attribution and notices remain unchanged.
+
+This changes uniform-transfer-audit to a local analytic-recovery construction.
+It does not discharge a selected framework assumption. Optimality and the
+2^100 divisibility obstruction apply only to the affine family. Nonmultiples
+have a strict lower bound here, with no exact optimum supplied. The constructor
+uses the unbounded integer model in the proof; its reference action API limits
+operands to 4,096 bits. No full-cycle execution, codec, physical tag acquisition,
+restoration cost, accepting caller, supplier admission, new kappa or selected
+cold replay is claimed. Independent human and formal proof-kernel review are
+unclaimed. Lean and Docker were not run.
+
+## Implementation bounds
+
+The two new Python files use bounded loops and no recursion, dynamic evaluation
+or callback dispatch. A frame uses 100 lifts of 112 coordinates. The source
+parser accepts 25 blocks of four lifts, each with at most 112 entries and
+coefficients of magnitude at most 100. Functions are below 60 physical lines.
+Checks raise exceptions and remain active under -O. The CLI rejects out-of-range
+indices. Integer action, inverse, mode preservation and transition composition
+are checked against the actual matrix.
+
+Power-of-Ten rule 3 has a managed-runtime deviation in both files. Python and
+its JSON and integer libraries allocate dynamically. The fixed source dimensions,
+4,096-bit action limit, at most 256 stages and 4,096 characters in a toy case,
+and explicitly bounded census domains bound live data. Source JSON is trusted
+only after hash authentication in the verifier. No live service or retained
+resource is introduced. Warning-strict normal and optimized replay, source
+compilation and CLI checks are the available diagnostics; no static type checker
+is configured for this isolated Python package. A physical implementation would
+need fixed-capacity storage and its own resource proof.
+
+## Open next questions
+
+1. Can a much shorter explicit near-balanced sequence give a useful finite-depth
+   bound? Start with a small-bias kernel multiset and prove every character
+   imbalance bound. No short construction is supplied.
+2. What bound replaces this one outside the affine family? First derive the
+   character action of a frame that changes its fixed complement. This package
+   gives no global frame classification.
+
+The relevance and blockers are also recorded in TASK.json.

research/refined-recovery-balanced-cycle/SOURCES.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "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-recovery-eps-exact-rate/PROOF.md",
+      "usage": "input",
+      "git_blob": "56342cf9dfd6283a3f599e2845bd10f188f9ef1f",
+      "sha256": "86ec5cc2323a14f986fc6502ae8cdfbc518285959b4ffeb1e2ce69640fc06fd0"
+    },
+    {
+      "path": "research/refined-recovery-eps-rate/PROOF.md",
+      "usage": "input",
+      "git_blob": "dee541400d4c47fb57aa42aa30aa50ede679fda9",
+      "sha256": "5821b8cb0c97ac7037ec6d47f239217c33e876df5cdd9ab195de01db97d54d9d"
+    },
+    {
+      "path": "research/refined-recovery-explicit-frames/PROOF.md",
+      "usage": "input",
+      "git_blob": "7e7f355d37abf888f7eea0ef89416081756ce4c1",
+      "sha256": "0cecaf9ccda48f52032fe53ef3ec38aea027bff46705422335e63d48df1684b4"
+    },
+    {
+      "path": "research/refined-recovery-longer-chains/FRAMES.json",
+      "usage": "input",
+      "git_blob": "ecc2011e2ec451fda8e2ee0d6a7883f79c03db96",
+      "sha256": "9efe341a2e6e33088543a3fa689c183a15e4c6a9840ebc2515a1fdcc1d605981"
+    },
+    {
+      "path": "research/refined-recovery-max-fiber/PROOF.md",
+      "usage": "input",
+      "git_blob": "745f436b4e354b8bce446762a3293f8657458a8c",
+      "sha256": "8f0a35ed5d81d1e7dbac769e6c2fcec4a16d298924ff350c54d67bab660474a5"
+    },
+    {
+      "path": "research/refined-recovery-longer-chains/PROOF.md",
+      "usage": "input",
+      "git_blob": "34a5f56d608c17dec7acca938fb01d17a74c25c3",
+      "sha256": "9c67877b06dcdf24211f2d2ff23553fa07d54f476598382af0527f6b4ba2c9e9"
+    },
+    {
+      "path": "research/refined-recovery-explicit-frames/README.md",
+      "usage": "input",
+      "git_blob": "75b6e712c2020ea9b8586ae407ee865371d323c2",
+      "sha256": "c189114d63f5c0c3233ad70ee9a0da7ad94544864d77164c5b4eb24a4b0955ac"
+    }
+  ]
+}