From 29821d06678f9262f6fff6a341abc5c1d42c3604 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 11:35:49 +0000 Subject: [PATCH] feat(research): construct optimal affine recovery cycles --- .../refined-recovery-balanced-cycle/PROOF.md | 169 ++++++++++++++ .../refined-recovery-balanced-cycle/README.md | 101 +++++++++ .../SOURCES.json | 66 ++++++ .../refined-recovery-balanced-cycle/TASK.json | 100 +++++++++ .../VERIFY.json | 41 ++++ .../refined-recovery-balanced-cycle/cycle.py | 81 +++++++ .../refined-recovery-balanced-cycle/verify.py | 211 ++++++++++++++++++ 7 files changed, 769 insertions(+) create mode 100644 research/refined-recovery-balanced-cycle/PROOF.md create mode 100644 research/refined-recovery-balanced-cycle/README.md create mode 100644 research/refined-recovery-balanced-cycle/SOURCES.json create mode 100644 research/refined-recovery-balanced-cycle/TASK.json create mode 100644 research/refined-recovery-balanced-cycle/VERIFY.json create mode 100644 research/refined-recovery-balanced-cycle/cycle.py create mode 100644 research/refined-recovery-balanced-cycle/verify.py diff --git a/research/refined-recovery-balanced-cycle/PROOF.md b/research/refined-recovery-balanced-cycle/PROOF.md new file mode 100644 index 0000000000..c85dcef73c --- /dev/null +++ b/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. diff --git a/research/refined-recovery-balanced-cycle/README.md b/research/refined-recovery-balanced-cycle/README.md new file mode 100644 index 0000000000..1327975d37 --- /dev/null +++ b/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. diff --git a/research/refined-recovery-balanced-cycle/SOURCES.json b/research/refined-recovery-balanced-cycle/SOURCES.json new file mode 100644 index 0000000000..0c30db4616 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/refined-recovery-balanced-cycle/TASK.json b/research/refined-recovery-balanced-cycle/TASK.json new file mode 100644 index 0000000000..8177ea6826 --- /dev/null +++ b/research/refined-recovery-balanced-cycle/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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": "Explicit rank-one integer frame cycle attaining the sharp affine-family character-sum bound; exact equality-depth divisibility and full-cycle maximum-fiber formula.", + "scope_change_reason": "Answers structured-construction question 2 of apoursh PR6853 as a local analytic-recovery side result. It does not discharge analytic_recovery at an actual selected caller.", + "bottleneck_link": "Provides explicit precision-state counting frames with single-lift transitions. It leaves physical acquisition, restoration and the complete caller bill open.", + "budget_minutes": 60, + "stop_rule": "Stop after this one sharp scoped construction and bounded exact corroboration; do not search for shorter practical cycles.", + "outcome": "completed", + "evidence": "PROOF.md; cycle.py random-access integer frames; verify.py exact reduced-domain enumerations and literal integer actions.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a much shorter explicit near-balanced sequence give a useful finite-depth bound?", + "why_it_matters": "The exact equality cycle has 2^100 stages and does not improve the depth-28 to depth-30 constructions.", + "first_step": "Construct a small-bias multiset of kernel vectors and bound every character imbalance before generating integer frames.", + "blocked_by": "No short construction or favorable finite-depth bound is supplied here." + }, + { + "question": "What bound replaces B_100(t) outside the affine I+VE family?", + "why_it_matters": "The fixed fifteen characters and the equality divisibility obstruction were proved only for the affine family.", + "first_step": "Derive the character action of a mode-preserving frame that changes the fixed complement used here.", + "blocked_by": "This package supplies no classification or optimality statement for all mode-preserving frames." + } + ], + "question_source": { + "pr": 6853, + "author": "apoursh", + "question": 2 + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540684", + "environment": { + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "version": "CPython 3.12.15", + "dependencies": "standard library only" + } +} diff --git a/research/refined-recovery-balanced-cycle/VERIFY.json b/research/refined-recovery-balanced-cycle/VERIFY.json new file mode 100644 index 0000000000..8f6c3dd05e --- /dev/null +++ b/research/refined-recovery-balanced-cycle/VERIFY.json @@ -0,0 +1,41 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/precision-state-frontier/FIXTURE.json", + "research/refined-recovery-eps-exact-rate/PROOF.md", + "research/refined-recovery-eps-rate/PROOF.md", + "research/refined-recovery-explicit-frames/PROOF.md", + "research/refined-recovery-explicit-frames/README.md", + "research/refined-recovery-longer-chains/FRAMES.json", + "research/refined-recovery-longer-chains/PROOF.md", + "research/refined-recovery-max-fiber/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact balanced spectra in dimensions 1..8; arbitrary-map lower bounds and equality divisibility; Fourier occupancy inversion; random-access integer frames and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete finite coverage under optimized Python; checks remain enabled." + } + ] +} diff --git a/research/refined-recovery-balanced-cycle/cycle.py b/research/refined-recovery-balanced-cycle/cycle.py new file mode 100644 index 0000000000..cdb17c4291 --- /dev/null +++ b/research/refined-recovery-balanced-cycle/cycle.py @@ -0,0 +1,81 @@ +"""Random-access rank-one integer frames for the balanced recovery cycle.""" + +import argparse +import json +from pathlib import Path + +N = 112 +D = 100 +PERIOD = 1 << D +E = (0, 1, 2, 4) +LAMBDA = (1, 2, 4) +ROOT = Path(__file__).resolve().parents[2] + + +def load_basis(root=ROOT): + """Read the predecessor's integer lifts, without executing its verifier.""" + path = root / "research/refined-recovery-longer-chains/FRAMES.json" + spec = json.loads(path.read_text()) + blocks = spec["V_blocks"] + if len(blocks) != 25 or any(len(block) != 4 for block in blocks): + raise ValueError("expected 25 blocks of four integer lifts") + basis = [] + for block in blocks: + for sparse in block: + if len(sparse) > N: + raise ValueError("oversized sparse lift") + vector = [0] * N + seen = set() + for index, value in sparse: + if type(index) is not int or not 0 <= index < N or index in seen: + raise ValueError("invalid or repeated lift coordinate") + if type(value) is not int or abs(value) > 100: + raise ValueError("invalid lift coefficient") + seen.add(index) + vector[index] = value + basis.append(tuple(vector)) + return tuple(basis) + + +def frame_vector(index, basis): + """Return v_a in W_a = I + v_a lambda, using reflected Gray order.""" + if type(index) is not int or not 0 <= index < PERIOD: + raise ValueError("index must be an integer in [0, 2**100)") + if len(basis) != D or any(len(vector) != N for vector in basis): + raise ValueError("expected 100 integer vectors of length 112") + gray = index ^ (index >> 1) + return tuple(sum(basis[b][i] for b in range(D) if gray >> b & 1) + for i in range(N)) + + +def apply_frame(vector, state, sign=1): + """Apply W or its inverse; lambda has ones at owners 1, 2 and 4.""" + if len(vector) != N or len(state) != N or sign not in (-1, 1): + raise ValueError("invalid rank-one action") + if any(type(x) is not int or x.bit_length() > 4096 for x in vector + state): + raise ValueError("reference actions accept integers of at most 4096 bits") + coefficient = sign * sum(state[i] for i in LAMBDA) + return tuple(x + coefficient * v for x, v in zip(state, vector)) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--index", type=int, required=True) + args = parser.parse_args() + basis = load_basis() + try: + vector = frame_vector(args.index, basis) + following = frame_vector((args.index + 1) % PERIOD, basis) + except ValueError as error: + parser.error(str(error)) + difference = tuple(x - y for x, y in zip(vector, following)) + output = {"index": args.index, "period": PERIOD, + "meaning": "W=I+v*lambda; U_to_next=I+delta*lambda", + "lambda": [[i, 1] for i in LAMBDA], + "v": [[i, x] for i, x in enumerate(vector) if x], + "delta": [[i, x] for i, x in enumerate(difference) if x]} + print(json.dumps(output, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/refined-recovery-balanced-cycle/verify.py b/research/refined-recovery-balanced-cycle/verify.py new file mode 100644 index 0000000000..8d528c9e31 --- /dev/null +++ b/research/refined-recovery-balanced-cycle/verify.py @@ -0,0 +1,211 @@ +"""Exact finite corroboration of the balanced-cycle theorem, not its full cycle.""" + +import hashlib +import itertools +import json +from pathlib import Path + +from cycle import D, E, LAMBDA, N, PERIOD, apply_frame, frame_vector, load_basis + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def parity(value): + return value.bit_count() & 1 + + +def codeword(label): + """The [8,4,4] weight model, in an independent RM(1,3) chart.""" + return sum((parity((label >> 1) & point) ^ (label & 1)) << point + for point in range(8)) + + +def evaluate(cols, q): + value = 0 + for i in range(4): + if q >> i & 1: + value ^= cols[i] + return value + + +def rank(vectors): + pivots = [0] * 112 + for vector in vectors: + for bit in range(111, -1, -1): + if vector >> bit & 1: + if pivots[bit]: + vector ^= pivots[bit] + else: + pivots[bit] = vector + break + return sum(bool(pivot) for pivot in pivots) + + +def character_weights(maps, dimension): + """Literal adjoints for arbitrary Q -> R maps, including non-rank-one maps.""" + check(1 <= dimension <= 8 and 1 <= len(maps) <= 256, "toy domain") + check(all(len(cols) == 4 and all(0 <= x < 1 << dimension for x in cols) + for cols in maps), "toy map shape") + result = [] + weights = [codeword(c).bit_count() for c in range(16)] + for b in range(1 << dimension): + offsets = [sum(parity(b & col) << i for i, col in enumerate(cols)) + for cols in maps] + for c in range(16): + if b or c: + result.append(sum(weights[c ^ offset] for offset in offsets)) + return result + + +def scaled_gap(maps, dimension): + """13**(8t) times S minus the proposed lower bound; integer arithmetic.""" + t = len(maps) + values = character_weights(maps, dimension) + lhs = sum(13 ** (8 * t - weight) for weight in values) + rhs = ((1 << (dimension + 4)) - 2) * 13 ** (4 * t) + 1 + return lhs - rhs + + +def finite_cycles(): + cases = characters = 0 + for dimension in range(1, 9): + size = 1 << dimension + maps = [(a ^ (a >> 1), 0, 0, 0) for a in range(size)] + values = character_weights(maps, dimension) + check(values.count(4 * size) == (1 << (dimension + 4)) - 2, + "balanced spectrum at dimension " + str(dimension)) + check(values.count(8 * size) == 1, "unique weight-eight character") + check(scaled_gap(maps, dimension) == 0, "exact cycle lower bound") + if dimension <= 5: + check(scaled_gap(maps + maps, dimension) == 0, "repeated cycle") + mutant = maps.copy() + mutant[-1] = mutant[0] + check(scaled_gap(mutant, dimension) > 0, "omitted-vector control") + for q in range(1, 16, 2): + evaluations = [evaluate(cols, q) for cols in maps] + check(len(set(evaluations)) == size, "Fourier equality marginal") + characters += len(values) + cases += 1 + return cases, characters + + +def arbitrary_map_census(): + cases = equalities = 0 + for dimension, largest_t in ((1, 4), (2, 2)): + alphabet = tuple(itertools.product(range(1 << dimension), repeat=4)) + for t in range(1, largest_t + 1): + for suffix in itertools.product(alphabet, repeat=t - 1): + gap = scaled_gap(((0, 0, 0, 0),) + suffix, dimension) + check(gap >= 0, "affine lower bound") + if gap == 0: + check(t % (1 << dimension) == 0, "equality divisibility") + equalities += 1 + cases += 1 + return cases, equalities + + +def fourier_checks(): + cases = 0 + # Exhaust every occupancy vector of total at most six in dimensions 1..3. + for dimension in range(1, 4): + size = 1 << dimension + for total in range(1, 7): + for bars in itertools.combinations(range(total + size - 1), size - 1): + ends = (-1,) + bars + (total + size - 1,) + counts = tuple(ends[i + 1] - ends[i] - 1 for i in range(size)) + vanishes = all(sum(counts[a] * (-1) ** parity(a & b) + for a in range(size)) == 0 for b in range(1, size)) + check(vanishes == (len(set(counts)) == 1), "Fourier inversion") + if vanishes: + check(total % size == 0, "uniform multiset divisibility") + cases += 1 + return cases + + +def actual_frames(): + fixture = json.loads((ROOT / "research/precision-state-frontier/FIXTURE.json").read_text()) + columns = fixture["mode_columns"] + basis = load_basis(ROOT) + check(all(sum(columns[k][i] for i in LAMBDA) & 1 for k in range(8)), + "lambda M is the weight-eight codeword modulo two") + check(all(v[i] == 0 for v in basis for i in E), "E kills lifts") + indices = (0, 1, 2, 3, PERIOD - 1, PERIOD // 2) + tuple((1 << i) - 1 for i in range(D)) + samples = [] + for index in indices: + v = frame_vector(index, basis) + following = frame_vector((index + 1) % PERIOD, basis) + delta = tuple(x - y for x, y in zip(v, following)) + check(delta in basis or tuple(-x for x in delta) in basis, "one-lift transition") + state = tuple((17 * i + index) % 43 - 21 for i in range(N)) + changed = apply_frame(v, state) + check(apply_frame(v, changed, -1) == state, "integer frame inverse") + check(apply_frame(delta, changed) == apply_frame(v, apply_frame(following, changed, -1)), + "literal transition composition") + check(all(sum(columns[k][i] * v[i] for i in range(N)) == 0 for k in range(8)), + "mode preservation of constructed frame") + samples.append(sum((x & 1) << i for i, x in enumerate(v))) + mode_vectors = [sum((x & 1) << i for i, x in enumerate(col)) for col in columns] + check(rank(samples + mode_vectors) == 104, "rank-one cycle spans all 104 dimensions") + return len(indices) + + +def rejection_controls(): + basis = load_basis(ROOT) + rejected = 0 + for index in (-1, PERIOD, True, 0.5): + try: + frame_vector(index, basis) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid index accepted") + try: + frame_vector(0, basis[:-1]) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid basis accepted") + for state, sign in (((0,) * 111, 1), ((0,) * N, 0), ((1 << 4097,) * N, 1)): + try: + apply_frame((0,) * N, state, sign) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid action accepted") + return rejected + + +def main(): + sources = json.loads((HERE / "SOURCES.json").read_text())["files"] + check(len(sources) <= 16, "source inventory bound") + hashes = {} + for source in sources: + if source["usage"] == "input": + data = (ROOT / source["path"]).read_bytes() + digest = hashlib.sha256(data).hexdigest() + check(digest == source["sha256"], "source hash: " + source["path"]) + hashes[source["path"]] = digest + cycles, characters = finite_cycles() + maps, equalities = arbitrary_map_census() + output = {"cycles": cycles, "cycle_characters": characters, + "spectrum_rejection_controls": cycles, + "arbitrary_map_sequences": maps, "equality_sequences": equalities, + "fourier_multisets": fourier_checks(), "integer_frame_samples": actual_frames(), + "rejection_controls": rejection_controls(), "sha256": hashes} + entries = sorted(HERE.iterdir()) + check(len(entries) <= 16, "receipt inventory bound") + for path in entries: + if path.is_file(): + hashes[str(path.relative_to(ROOT))] = hashlib.sha256(path.read_bytes()).hexdigest() + print(json.dumps(output, sort_keys=True)) + print("PASS_REFINED_RECOVERY_BALANCED_CYCLE") + + +if __name__ == "__main__": + main()