From 99ffc8c47c86c55cc912fe71697c35e05030afd5 Mon Sep 17 00:00:00 2001 From: armin Date: Sat, 7 Nov 2026 07:42:44 -0500 Subject: [PATCH] =?UTF-8?q?Refined=20recovery:=20second-order=20term=20dec?= =?UTF-8?q?ays=20at=204.0=20to=2014.8=20bits=20per=20stage=20(no=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit OPT(t) = 2^-104 13^(8t) (1+eps_t). Exact first moment of S over PR6660's I+V E frame family (psi_j uniform into the 100-dim complement R') gives eps_t <= (2^104-16) q^t + 14*13^(-4t) + 13^(-8t) for t>=29 (below the #6848 threshold); Jensen on the uniform weight distribution of chi o phi_j gives eps_t >= 2^104 13^(-4t) for all frames. Co-Authored-By: Claude Opus 5.5 --- research/refined-recovery-eps-rate/PROOF.md | 91 +++++++ research/refined-recovery-eps-rate/README.md | 84 ++++++ .../refined-recovery-eps-rate/RESULT.json | 44 ++++ .../refined-recovery-eps-rate/SOURCES.json | 24 ++ research/refined-recovery-eps-rate/TASK.json | 89 +++++++ .../refined-recovery-eps-rate/VERIFY.json | 36 +++ research/refined-recovery-eps-rate/verify.py | 246 ++++++++++++++++++ 7 files changed, 614 insertions(+) create mode 100644 research/refined-recovery-eps-rate/PROOF.md create mode 100644 research/refined-recovery-eps-rate/README.md create mode 100644 research/refined-recovery-eps-rate/RESULT.json create mode 100644 research/refined-recovery-eps-rate/SOURCES.json create mode 100644 research/refined-recovery-eps-rate/TASK.json create mode 100644 research/refined-recovery-eps-rate/VERIFY.json create mode 100644 research/refined-recovery-eps-rate/verify.py diff --git a/research/refined-recovery-eps-rate/PROOF.md b/research/refined-recovery-eps-rate/PROOF.md new file mode 100644 index 0000000000..dee541400d --- /dev/null +++ b/research/refined-recovery-eps-rate/PROOF.md @@ -0,0 +1,91 @@ +# The second-order term of the refined-recovery optimum decays at 4 to 14.8 bits per stage + +Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0. + +## Setting and premises + +The objects are those of Nick Petalas's +[PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660) (head +`b6de532e`). Let V = red₂(ker_ℤ Mᵀ) be the 104-dimensional space containing +every image N_j (PR6660 (c)), and let μ = M mod 2 on Q = F2^8/C. For a frame +sequence define + + S(U) = Σ_{χ ∈ V^, χ≠0} Π_j 13^(−wt h_j(χ)), h_j(χ) = χ∘φ_j ∈ C. + +By Poisson summation ([#6849](https://github.com/CrocSwap/integer-mult-bounds/pull/6849) §1), + + |fiber(0)| = 2^(−104) · 13^(8t) · (1 + S(U)) + +for every frame sequence. S < 1 forces rank 104, because a deficient rank adds +1 for each χ vanishing on the span. Then S equals the ε₀ of +[#6848](https://github.com/CrocSwap/integer-mult-bounds/pull/6848). Hence + + OPT(t) = 2^(−104) 13^(8t) (1 + ε_t), ε_t := min_U S(U), + +whenever some U has S(U) ≤ ε* ≈ 4.25·10⁻⁴. In that case #6848 gives +max_y = |fiber(0)| for that U. For every other U the max fiber is at least +|fiber(0)|. + +## Theorem + +Let q = 16F/13^8 / 16 = (1 + 14·13^(−4) + 13^(−8))/16. For every t ≥ 29, + + (2^104 − 1) · 13^(−4t·2^104/(2^104−1)) ≤ ε_t ≤ E_t := (2^104 − 16) q^t + 14·13^(−4t) + 13^(−8t). + +So −log₂ ε_t / t lies between 4 − log₂(16F/13^8) = 3.9993 and 4·log₂13 = 14.8018, +asymptotically. At t = 29, E_t = 2.48·10⁻⁴. #6850's periodic construction gives +a decay of 13^(−4/26) per stage, about 0.57 bits per stage; this improves it to +4 bits per stage. + +## Upper bound: random frames, exact first moment + +Use PR6660's frame family W_j = I + V_jE, where V_j has four integer columns +with MᵀV_j = 0 and E V_j = 0, and W_1 = I. Modulo 2 this gives +φ_j = μ + ψ_j with ψ_j = V_j ∘ η, where η = E M mod 2 is an isomorphism +Q → F2^4. The column space R′ (the mod-2 reductions of the integer kernel of +Mᵀ on rows ∉ E) has dimension 100, and V = im μ ⊕ R′. verify.py computes both +from the pinned M. So ψ_2, …, ψ_t range over **all** linear maps Q → R′. + +Draw them independently and uniformly, and write χ = (χ₁, χ₂) ∈ (im μ)^ × R′^. + +* **χ₂ ≠ 0.** h_j = χ₁∘μ + χ₂∘ψ_j is uniform on C and independent for j ≥ 2, + with E[13^(−wt h)] = q. Stage 1 contributes 13^(−wt χ₁∘μ). Summing over χ₁ + gives (2^100 − 1)·16q·q^(t−1). +* **χ₂ = 0, χ₁ ≠ 0.** h_j = χ₁∘μ for every j. These are the 15 nonzero words of C + (14 of weight 4, one of weight 8). + +Hence E[S] = E_t exactly, and some choice has S ≤ E_t. By Markov's inequality, +at least half of all choices have S ≤ 2E_t. + +verify.py checks the identity E[S] = formula exactly by full enumeration in toy +dimensions dim R′ ∈ {1, 2} and t ≤ 4, using the real code C and the real η. + +## Lower bound: Jensen, all frames + +For each j, χ ↦ h_j(χ) is a linear surjection V^ → C, since φ_j is injective. +So every word of C is hit 2^100 times, and + + Σ_χ Σ_j wt h_j(χ) = t · 2^100 · Σ_{h∈C} wt h = 4t · 2^104. + +Since x ↦ 13^(−x) is convex, Jensen over the 2^104 − 1 nonzero χ gives the +lower bound. verify.py checks the weight identity and the bound on random toy +instances. + +## Consequences + +* OPT(t) = 2^(−104) 13^(8t) (1 + ε_t) with ε_t ≤ 2.48·10⁻⁴·16^(−(t−29))·(1.0005)^(t−29). +* "Most" frames of the family are near-optimal: half of them are within 2E_t. +* Pinning the exact rate needs either better codes than random ones or a + linear-programming lower bound on S. + +## Scope + +The premises are cited and not replayed here: + +* PR6660's dimension cap and frame family; +* #6848's max-fiber theorem; +* #6849's Poisson identity. + +All three are open and unmerged. The package supplies no codec, physical tag, +caller or restoration cost. κ, the selected frontier and its five assumptions are +unchanged. No independent human or proof-kernel review is claimed. diff --git a/research/refined-recovery-eps-rate/README.md b/research/refined-recovery-eps-rate/README.md new file mode 100644 index 0000000000..0289bd37b2 --- /dev/null +++ b/research/refined-recovery-eps-rate/README.md @@ -0,0 +1,84 @@ +# How fast the refined-recovery optimum approaches 13^(8t)/2^104 + +Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0. + +**Scoped proof with exact finite corroboration; no κ.** This answers open +question 2 of [#6849](https://github.com/CrocSwap/integer-mult-bounds/pull/6849): +how fast the second-order term ε_t can go to 0, where + + OPT(t) = 2^(−104)·13^(8t)·(1 + ε_t) (t ≥ 29). + +**Theorem.** For every t ≥ 29, + + (2^104−1)·13^(−4t·2^104/(2^104−1)) ≤ ε_t ≤ (2^104−16)·q^t + 14·13^(−4t) + 13^(−8t), q = (1+14·13⁻⁴+13⁻⁸)/16, + +so ε_t decays at between **4.0** and **14.8 bits per stage**. At t = 29 the upper +bound is 2.48·10⁻⁴. [#6850](https://github.com/CrocSwap/integer-mult-bounds/pull/6850)'s +periodic frames give a decay of about 0.57 bits per stage; this bound gives 4. + +| t | 29 | 30 | 40 | 60 | +|---|---:|---:|---:|---:| +| log₂ upper bound on ε_t | −11.98 | −15.98 | −55.97 | −135.96 | +| log₂ lower bound on ε_t | −325.3 | −340.1 | −488.1 | −784.1 | + +**Why.** + +- *Upper bound.* In PR6660's frame family W_j = I + V_jE, the stage maps are + φ_j = μ + ψ_j. Here ψ_j ranges over all linear maps Q → R′, a 100-dimensional + complement of im μ in the 104-dimensional V. Averaging S = Σ_{χ≠0} Π_j 13^(−wt) + over uniformly random ψ_j gives exactly the formula above. So some frames, and + in fact at least half of them up to a factor 2, achieve it. Since this is below + #6848's threshold, their max fiber is their zero fiber. +- *Lower bound.* Every stage map is injective, so each χ ↦ χ∘φ_j hits every word + of C equally often. The average total weight is therefore 4t, and Jensen gives + the bound. + +See [PROOF.md](PROOF.md). + +## Reproduce + +From the repository root, CPython 3.12, standard library only: + +```sh +python3.12 -I -W error -B research/refined-recovery-eps-rate/verify.py +python3.12 -I -O -W error -B research/refined-recovery-eps-rate/verify.py +python3.12 -B scripts/research_package.py --package research/refined-recovery-eps-rate +``` + +Each run prints `PASS_REFINED_RECOVERY_EPS_RATE` in under a second. It checks: + +* that dim R′ = 100 and dim(im μ + R′) = 104, from the pinned M; +* that η maps onto C; +* the first-moment formula, by exact full enumeration in toy dimensions; +* the Jensen weight identity on random toys; +* that E_t < ε* for 29 ≤ t ≤ 60, with E_28 > ε* as a control; +* the decay rates. + +## Limitations + +The result cites PR6660 (dimension cap, frame family), #6848 (max-fiber theorem) +and #6849 (Poisson identity). These are open and unmerged, and are not replayed +here. + +The upper bound is existential. It comes from a first moment and supplies no +explicit frames beyond t = 27. The gap between 4.0 and 14.8 bits per stage +remains open. At t = 28 the first moment exceeds the threshold, and #6850 +covers that depth instead. + +The package supplies no codec, physical tag, caller or restoration cost. κ, the +selected frontier and its five assumptions are unchanged. No independent human or +proof-kernel review is claimed. + +## Open next questions + +1. **Exact rate.** Is the true decay rate 4 bits per stage? A Delsarte-style + linear-programming bound on S, or structured codes (the per-stage maps form an + F2-linear code over GF(16)-sized blocks), should decide it. +2. **Explicit frames.** Give explicit near-optimal frames for t ≥ 29, for example + with algebraic-geometry codes. + +## Credit + +Nick Petalas's PR6660 (frame family, dimension cap, the question); CubeJerry's +PR6327; zxv's #5444; #6848, #6849 and #6850. The first-moment and Jensen +arguments are classical. diff --git a/research/refined-recovery-eps-rate/RESULT.json b/research/refined-recovery-eps-rate/RESULT.json new file mode 100644 index 0000000000..e7d9a899c9 --- /dev/null +++ b/research/refined-recovery-eps-rate/RESULT.json @@ -0,0 +1,44 @@ +{ + "E_t_formula": "(2^104-16)((16F/13^8)/16)^t + 14*13^(-4t) + 13^(-8t)", + "E_28_over_eps_star": 9.324900540037063, + "E_29_float": 0.00024763506057637905, + "rate_bits_per_stage_upper_bound_side": 3.999293, + "rate_bits_per_stage_lower_bound_side": 14.801759, + "table": [ + { + "t": 29, + "log2_upper_eps": -11.979, + "log2_lower_eps": -325.251 + }, + { + "t": 30, + "log2_upper_eps": -15.979, + "log2_lower_eps": -340.053 + }, + { + "t": 31, + "log2_upper_eps": -19.978, + "log2_lower_eps": -354.855 + }, + { + "t": 32, + "log2_upper_eps": -23.977, + "log2_lower_eps": -369.656 + }, + { + "t": 40, + "log2_upper_eps": -55.972, + "log2_lower_eps": -488.07 + }, + { + "t": 50, + "log2_upper_eps": -95.965, + "log2_lower_eps": -636.088 + }, + { + "t": 60, + "log2_upper_eps": -135.958, + "log2_lower_eps": -784.106 + } + ] +} diff --git a/research/refined-recovery-eps-rate/SOURCES.json b/research/refined-recovery-eps-rate/SOURCES.json new file mode 100644 index 0000000000..ae5689199c --- /dev/null +++ b/research/refined-recovery-eps-rate/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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" + } + ] +} diff --git a/research/refined-recovery-eps-rate/TASK.json b/research/refined-recovery-eps-rate/TASK.json new file mode 100644 index 0000000000..3859e890c9 --- /dev/null +++ b/research/refined-recovery-eps-rate/TASK.json @@ -0,0 +1,89 @@ +{ + "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": "Second-order term of the refined-recovery optimum OPT(t)=2^-104 13^(8t)(1+eps_t): for t>=29, (2^104-1)13^(-4t 2^104/(2^104-1)) <= eps_t <= (2^104-16)q^t+14*13^(-4t)+13^(-8t), q=(1+14*13^-4+13^-8)/16; decay between 4.0 and 14.8 bits per stage. Upper bound by an exact first moment over PR6660's frame family, lower bound by Jensen over all frames.", + "scope_change_reason": "Answers #6849 open question 2 (rate of eps0 decay). Precision-state accounting in the analytic_recovery interface, not a caller-bound discharge of a selected assumption.", + "bottleneck_link": "Side result for exact history accounting in the inherited rounded interface; it changes no supplier invoice.", + "budget_minutes": 60, + "stop_rule": "Stop at the two-sided rate bounds; leave the exact rate and explicit frames open.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py (exact rational arithmetic, normal and optimized Python) writes/rechecks RESULT.json.", + "author": "apoursh", + "ai_assistance": "Anthropic Claude (Claude Code) found the argument, wrote the verifier and ran the checks under apoursh direction. Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the exact decay rate of eps_t 4 bits per stage?", + "why_it_matters": "Pins the second-order term of the optimum.", + "first_step": "Set up the Delsarte linear program for S over F2-linear block codes with inner code C.", + "blocked_by": "Nothing; standard but not yet done." + }, + { + "question": "Explicit near-optimal frames for t>=29?", + "why_it_matters": "The upper bound is existential.", + "first_step": "Choose psi_j from an algebraic-geometry code over GF(16) and evaluate S.", + "blocked_by": "Realizability is free (any psi_j), so only code construction remains." + } + ] +} diff --git a/research/refined-recovery-eps-rate/VERIFY.json b/research/refined-recovery-eps-rate/VERIFY.json new file mode 100644 index 0000000000..77ca0858ee --- /dev/null +++ b/research/refined-recovery-eps-rate/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 hash; C and coset sums from M; integer kernel of M^T off E: mod-2 rank 100, with im M mod 2 rank 104; eta onto C; first-moment formula by exact enumeration in toy dimensions; Jensen weight identity on random toys; E_t < eps* for 29<=t<=60 and E_28 > eps* control; decay rates; RESULT.json recomputation." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same explicit checks under optimized Python." + } + ] +} diff --git a/research/refined-recovery-eps-rate/verify.py b/research/refined-recovery-eps-rate/verify.py new file mode 100644 index 0000000000..37dad2d112 --- /dev/null +++ b/research/refined-recovery-eps-rate/verify.py @@ -0,0 +1,246 @@ +"""Exact checks for the rate of the second-order term of the refined-recovery optimum. + +Prints PASS_REFINED_RECOVERY_EPS_RATE on success (stdlib only). +""" +import hashlib +import itertools +import json +import math +import pathlib +import random +from fractions import Fraction + +HERE = pathlib.Path(__file__).resolve().parent +FIXTURE = HERE.parent / "precision-state-frontier" / "FIXTURE.json" +FIXTURE_SHA = "2ca4d7550fcae5b757ec500f87aee1d2ef9f64b59e4abe2bda93319521304af8" +RESULT = HERE / "RESULT.json" +N, MODES = 112, 8 +F = (13**8 + 14 * 13**4 + 1) // 16 +CAP = 104 # #6660 Theorem (c) +EPS_STAR = Fraction(1, 13) / (Fraction(23, 12) ** 8 - 1) # #6848 threshold + + +def fail(msg): + raise SystemExit("FAIL: " + msg) + + +def check(cond, msg): + if not cond: + fail(msg) + + +def wt(u): + return bin(u).count("1") + + +def load_rows(): + 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 code_from_rows(rows): + """C = {q in F2^8 : M q = 0 mod 2}, as 8-bit masks.""" + code = [q for q in range(256) + if all(sum(r[k] for k in range(MODES) if q >> k & 1) % 2 == 0 for r in rows)] + check(len(code) == 16, "|C| = 16") + check(all(wt(a & b) % 2 == 0 for a in code for b in code), "C self-orthogonal (so self-dual)") + check(sorted(wt(c) for c in code) == [0] + [4] * 14 + [8], "C is the [8,4,4] code") + return code + + +def weight(u): + return 7 ** (8 - wt(u)) * 6 ** wt(u) + + +def coset_data(code): + rep = lambda u: min(u ^ c for c in code) + reps = sorted({rep(u) for u in range(256)}) + S = {a: sum(weight(a ^ c) for c in code) for a in reps} + check(S[0] == F, "S(C) = F") + check({S[a] for a in reps if wt(a) % 2} == {50983170}, "odd coset sum") + check({S[a] for a in reps if a and wt(a) % 2 == 0} == {50979600}, "even coset sum") + for h in code: # Fourier transform of the [-6,6] box weight + check(sum(weight(u) * (-1) ** wt(h & u) for u in range(256)) == 13 ** (8 - wt(h)), + "hat w(h) = 13^(8 - wt h)") + return reps, S + + +def rank2(vecs): + basis = [] + for v in vecs: + for b in basis: + v = min(v, v ^ b) + if v: + basis.append(v) + return len(basis) + + +EIDX = (0, 1, 2, 4) # rows of E, as in PR6327 / PR6660 +RPRIME_DIM = 100 + + +def kernel_mod2_rank(rows): + """Integer kernel of M^T restricted to rows outside E; ranks of its mod-2 reduction + alone and together with the columns of M mod 2.""" + free = [i for i in range(N) if i not in EIDX] + A = [[rows[i][k] for i in free] for k in range(MODES)] + n = len(free) + U = [[int(i == j) for j in range(n)] for i in range(n)] + + def colop(c1, c2, f): + for r in A: + r[c1] -= f * r[c2] + for r in U: + r[c1] -= f * r[c2] + + def swap(c1, c2): + for r in A + U: + r[c1], r[c2] = r[c2], r[c1] + + piv = 0 + for k in range(MODES): + while True: + nz = [c for c in range(piv, n) if A[k][c] != 0] + if len(nz) <= 1: + break + c0 = min(nz, key=lambda c: abs(A[k][c])) + for c in nz: + if c != c0: + colop(c, c0, A[k][c] // A[k][c0]) + nz = [c for c in range(piv, n) if A[k][c] != 0] + if nz: + swap(piv, nz[0]) + piv += 1 + check(piv == MODES, "M^T has rank 8 on the free rows") + kern = [] + for c in range(MODES, n): + v = [0] * N + for i, x in zip(free, (U[r][c] for r in range(n))): + v[i] = x + check(all(sum(rows[i][k] * v[i] for i in range(N)) == 0 for k in range(MODES)), "M^T v = 0") + check(all(v[i] == 0 for i in EIDX), "E v = 0") + kern.append(sum((v[i] & 1) << i for i in range(N))) + mcols = [sum((rows[i][k] & 1) << i for i in range(N)) for k in range(MODES)] + return rank2(kern), rank2(kern + mcols), rank2(mcols) + + +def eta_rows(rows): + """eta(u)_b = mod 2, as 8-bit masks of the E rows.""" + return [sum((rows[i][k] & 1) << k for k in range(MODES)) for i in EIDX] + + +def h_of(func, er): + """The element h in C with h.u = func . eta(u) (func a 4-bit functional).""" + h = 0 + for b in range(4): + if func >> b & 1: + h ^= er[b] + return h + + +def toy_first_moment(code, er): + """Exact average of S over all psi (psi_1 = 0) for small R' (dim r'), t stages.""" + for rp, t in ((1, 2), (1, 3), (2, 2), (1, 4)): + maps = list(itertools.product(range(2 ** rp), repeat=4)) # images of eta-basis + total, count = Fraction(0), 0 + for psis in itertools.product(maps, repeat=t - 1): + psis = ((0, 0, 0, 0),) + psis + S = Fraction(0) + for chi1 in range(16): + for chi2 in range(2 ** rp): + if chi1 == 0 and chi2 == 0: + continue + w = 0 + for psi in psis: + f = chi1 + for b in range(4): # functional chi2 o psi on eta-basis + if wt(chi2 & psi[b]) & 1: + f ^= 1 << b + h = h_of(f, er) + check(h in code, "chi o phi_j is a word of C") + w += wt(h) + S += Fraction(1, 13 ** w) + total += S + count += 1 + avg = total / count + q = Fraction(16 * F, 13 ** 8) / 16 + formula = (2 ** (4 + rp) - 16) * q ** t + 14 * Fraction(1, 13 ** (4 * t)) \ + + Fraction(1, 13 ** (8 * t)) + check(avg == formula, "first moment formula (r'=%d, t=%d)" % (rp, t)) + + +def toy_jensen(code, er): + """Sum over chi of total weight is 4 t 2^r for injective stage maps (toy r = 6).""" + rng = random.Random(29) + for trial in range(10): + t, rp = rng.randint(2, 4), 2 + psis = [(0, 0, 0, 0)] + [tuple(rng.randrange(4) for _ in range(4)) for _ in range(t - 1)] + tot, S = 0, Fraction(0) + for chi in range(1, 2 ** (4 + rp)): + chi1, chi2 = chi & 15, chi >> 4 + w = 0 + for psi in psis: + f = chi1 + for b in range(4): + if wt(chi2 & psi[b]) & 1: + f ^= 1 << b + w += wt(h_of(f, er)) + tot += w + S += Fraction(1, 13 ** w) + R = 2 ** (4 + rp) + check(tot == 4 * t * R, "sum of weights = 4 t 2^r") + check(S >= (R - 1) * 13.0 ** (-4 * t * R / (R - 1)) * (1 - 1e-12), "Jensen lower bound") + + +def E_t(t): + q = Fraction(16 * F, 13 ** 8) / 16 + return (2 ** CAP - 16) * q ** t + 14 * Fraction(1, 13 ** (4 * t)) + Fraction(1, 13 ** (8 * t)) + + +def log2_frac(x): + return math.log2(x.numerator) - math.log2(x.denominator) + + +def main(): + rows = load_rows() + code = code_from_rows(rows) + reps, S = coset_data(code) + r_k, r_all, r_m = kernel_mod2_rank(rows) + check((r_k, r_all, r_m) == (RPRIME_DIM, CAP, 4), "R' has dim 100 and V = im mu + R' has dim 104") + er = eta_rows(rows) + check(sorted({h_of(f, er) for f in range(16)}) == sorted(code), "eta^T maps F2^4 onto C") + toy_first_moment(code, er) + toy_jensen(code, er) + + check(E_t(28) > EPS_STAR, "control: first moment does not reach the threshold at t = 28") + table = [] + for t in range(29, 61): + e = E_t(t) + check(e < EPS_STAR, "E_t below the #6848 threshold at t=%d" % t) + lo_log2 = math.log2(2 ** CAP - 1) - 4 * t * (2 ** CAP / (2 ** CAP - 1)) * math.log2(13) + table.append({"t": t, "log2_upper_eps": round(log2_frac(e), 3), "log2_lower_eps": round(lo_log2, 3)}) + rate_up = 4 - math.log2(16 * F / 13 ** 8) + rate_lo = 4 * math.log2(13) + check(abs((table[-1]["log2_upper_eps"] - table[-2]["log2_upper_eps"]) + rate_up) < 1e-3, "upper rate") + result = { + "E_t_formula": "(2^104-16)((16F/13^8)/16)^t + 14*13^(-4t) + 13^(-8t)", + "E_28_over_eps_star": float(E_t(28) / EPS_STAR), + "E_29_float": float(E_t(29)), + "rate_bits_per_stage_upper_bound_side": round(rate_up, 6), + "rate_bits_per_stage_lower_bound_side": round(rate_lo, 6), + "table": [row for row in table if row["t"] <= 32 or row["t"] % 10 == 0], + } + text = json.dumps(result, indent=1) + "\n" + if __debug__ and not RESULT.exists(): + RESULT.write_text(text) + check(RESULT.read_text() == text, "RESULT.json matches recomputation") + print("E_29 = %.4e < eps*; decay rates %.4f (upper) and %.4f (lower) bits per stage" + % (float(E_t(29)), rate_up, rate_lo)) + print("PASS_REFINED_RECOVERY_EPS_RATE") + + +if __name__ == "__main__": + main()