From 1e5406c51f536d0b243827788b71dff8ceefd191 Mon Sep 17 00:00:00 2001 From: armin Date: Sat, 7 Nov 2026 07:33:00 -0500 Subject: [PATCH] =?UTF-8?q?Refined=20recovery:=20optimum=20->=2013^(8t)/2^?= =?UTF-8?q?104,=20exact=20tag=20at=20every=20depth=20t>=3D27=20(no=20?= =?UTF-8?q?=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit FRAMES27 followed by cycled PR6660 direct-sum frames shrinks eps0 by 13^-4 per 26-stage cycle, so 1 <= OPT 2^104/13^(8t) <= 1+theta 13^(-4 floor((t-27)/26)). Tag = ceil(8t log2 13)-104 for every t>=27: big integers to t=1500, a 700-digit continued fraction to 10^200, Laurent-Mignotte-Nesterenko beyond. Co-Authored-By: Claude Opus 5.5 --- research/refined-recovery-asymptotic/PROOF.md | 86 +++++++ .../refined-recovery-asymptotic/README.md | 78 ++++++ .../refined-recovery-asymptotic/RESULT.json | 100 ++++++++ .../refined-recovery-asymptotic/SOURCES.json | 24 ++ .../refined-recovery-asymptotic/TASK.json | 89 +++++++ .../refined-recovery-asymptotic/VERIFY.json | 36 +++ .../refined-recovery-asymptotic/verify.py | 230 ++++++++++++++++++ 7 files changed, 643 insertions(+) create mode 100644 research/refined-recovery-asymptotic/PROOF.md create mode 100644 research/refined-recovery-asymptotic/README.md create mode 100644 research/refined-recovery-asymptotic/RESULT.json create mode 100644 research/refined-recovery-asymptotic/SOURCES.json create mode 100644 research/refined-recovery-asymptotic/TASK.json create mode 100644 research/refined-recovery-asymptotic/VERIFY.json create mode 100644 research/refined-recovery-asymptotic/verify.py diff --git a/research/refined-recovery-asymptotic/PROOF.md b/research/refined-recovery-asymptotic/PROOF.md new file mode 100644 index 0000000000..d8a60b56d4 --- /dev/null +++ b/research/refined-recovery-asymptotic/PROOF.md @@ -0,0 +1,86 @@ +# Refined recovery past depth 26: the optimum is asymptotically exact + +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`). OPT(t) = min_U max_y |fiber(y)|, and α = 8·log₂13. The following +premises are cited and not replayed: + +* **(P1) PR6660 (c).** All binary images N_j lie in one space V of dimension at + most 104. Its FRAMES.json gives 26 frames whose images form a direct sum, so + together they span all of V and dim V = 104. +* **(P2) [#6828](https://github.com/CrocSwap/integer-mult-bounds/pull/6828).** + FRAMES27 has rank 104, and its zero fiber equals (1+12ρ₂^25+3ρ₂^26)F^27. +* **(P3) [#6848](https://github.com/CrocSwap/integer-mult-bounds/pull/6848).** + If ε₀ ≤ ε* ≈ 4.25·10⁻⁴, then max_y |fiber(y)| = |fiber(0)|. +* **(P4) [#6849](https://github.com/CrocSwap/integer-mult-bounds/pull/6849).** + Every frame sequence has |fiber(0)| ≥ 13^(8t)/2^104. For rank 104, + |fiber(0)| = 2^(−104) 13^(8t) (1+ε₀) with ε₀ = Σ_{χ∈V^∖0} Π_j 13^(−wt h_j(χ)). + +## Theorem + +Let θ = ε₀(FRAMES27) = 5.4537·10⁻⁶. For every t ≥ 27, + + 1 ≤ OPT(t) · 2^104 / 13^(8t) ≤ 1 + θ · 13^(−4⌊(t−27)/26⌋). + +In particular, OPT(t)·2^104/13^(8t) → 1 exponentially fast. Moreover the +minimum tag is + + ⌈log₂ OPT(t)⌉ = ⌈8t·log₂13⌉ − 104 for every t ≥ 27. + +This removes every sparse exception left by #6849, including t = 584,977. + +## Proof + +**Frames.** Take FRAMES27 for stages 1–27. Then append #6660's 26 direct-sum +frames, cycled. Each U_j ∈ G, because G is a group containing every W_j. The +rank stays 104 by (P1). + +**Decay.** Fix χ ∈ V^∖0. In each complete cycle, χ is nonzero on some N_j, +because those images span V. There h_j(χ) is a nonzero word of C and has weight +at least 4. So every term of ε₀ gains a factor of at most 13^(−4) per complete +cycle, and no term grows. Hence ε₀(t) ≤ θ·13^(−4m) with m = ⌊(t−27)/26⌋. + +Since ε₀(t) ≤ θ < ε*, (P3) gives max_y = |fiber(0)|. Then (P4) gives both +bounds. verify.py checks the decay claim exactly on eight random small instances. + +**Tag bits.** The tag is undetermined only if 1 − {tα} < log₂(1+ε₀(t)) ≤ 2ε₀(t). + +* For 27 ≤ t ≤ 1500, verify.py decides this exactly with big integers. +* For t > 1500, 2ε₀(t) ≤ 10^(−254.8). + +The continued fraction of α = [29; 1, 1, 1, 1, 10, …] is computed to 700 +digits. It gives convergents with q_414 of 200 digits, q_415 ≥ 10^200 and +‖q_414 α‖ ≈ 10^(−202). By the best-approximation property, every 0 < t < q_415 +has ‖tα‖ ≥ ‖q_414 α‖ > 10^(−254.8). So no t in (1500, 10^200) is ambiguous. + +For t ≥ 10^200 we use Laurent–Mignotte–Nesterenko (J. Number Theory 55 +(1995) 285–321), Corollary 2. Here D = 1, α₁ = 2, α₂ = 13, log A₁ = 1 and +log A₂ = log 13. With b₁ = k and b₂ = 8t we have b′ = k/log 13 + 8t ≤ 20t. The +bound gives + + log|8t·log 13 − k·log 2| ≥ −24.34·(log(20t) + 0.14)²·log 13. + +At t = 10^200 the right side is about −1.34·10⁷. The window's logarithm is +≤ log(2θ) − 4·log 13·⌊(t−27)/26⌋ ≈ −4·10^199. That side falls linearly in t, while +the right side falls only polylogarithmically, so the window stays below ‖tα‖ +for every t ≥ 10^200. The margin is so large, a factor of 10^6 in the exponent +and far more, that any constant of this type would do. ∎ + +## Scope + +Exact for the PR6660 interface: + +* fixed known frames in G; +* one relative precision bit before the first call; +* unbounded exact integers; +* complete output access. + +Premises (P1)–(P4) are open and unmerged, and are not replayed here. For +t ≥ 10^200 the LMN bound is cited, not formalized; the margin is enormous. 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-asymptotic/README.md b/research/refined-recovery-asymptotic/README.md new file mode 100644 index 0000000000..38b77188bd --- /dev/null +++ b/research/refined-recovery-asymptotic/README.md @@ -0,0 +1,78 @@ +# Refined recovery past depth 26: optimum → 13^(8t)/2^104, exact tag at every depth + +Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0. + +**Scoped proof with exact finite corroboration; no κ.** This continues +[#6849](https://github.com/CrocSwap/integer-mult-bounds/pull/6849), which +answers [PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660)'s +open question 1 up to a fixed window 1+5.5·10⁻⁶. Here the window closes +exponentially: + + 1 ≤ OPT(t)·2^104/13^(8t) ≤ 1 + 5.46·10⁻⁶ · 13^(−4⌊(t−27)/26⌋) (t ≥ 27) + +So the optimal worst-case fiber is asymptotically exactly 13^(8t)/2^104. The +minimum tag is **⌈8t·log₂13⌉ − 104 bits for every t ≥ 27**, with no exceptions. +#6849 left sparse depths open, starting at t = 584,977. Together with PR6660 +(ceil(t·log₂F) for t ≤ 26), this completes the tag-size depth law for this +interface. + +**How.** + +- *Frames.* Run #6828's FRAMES27 first, then cycle PR6660's 26 direct-sum frames. +- *Decay.* Each cycle's images span the whole 104-dimensional space, so every + nonzero character picks up a codeword of weight at least 4. Each cycle therefore + multiplies ε₀ by at most 13^(−4). +- *Bound.* #6848 (max fiber = zero fiber) and #6849 (main-term lower bound) then + give the two-sided bound. +- *Tag sizes.* For 27 ≤ t ≤ 1500 the tag sizes are checked exactly with big + integers. Above that, a 700-digit continued fraction of 8·log₂13 shows + ‖t·8log₂13‖ ≥ 10^(−202) for all t < 10^200. That is far above the remaining + window of 10^(−254.8). For t ≥ 10^200, the explicit two-logarithm bound of + Laurent–Mignotte–Nesterenko (1995) decays only polylogarithmically, while the + window decays exponentially. + +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-asymptotic/verify.py +python3.12 -I -O -W error -B research/refined-recovery-asymptotic/verify.py +python3.12 -B scripts/research_package.py --package research/refined-recovery-asymptotic +``` + +Each run prints `PASS_REFINED_RECOVERY_ASYMPTOTIC` in about one second. + +## Limitations + +The result rests on four cited premises, which are not replayed here: + +* PR6660's dimension cap and its 26 direct-sum frames; +* #6828's FRAMES27; +* #6848's max-fiber theorem; +* #6849's main-term identity. + +All of these are open and unmerged. + +For t ≥ 10^200 the LMN (1995) Corollary 2 bound is cited, not formalized; the +margin is enormous. The exact value of OPT(t) for t ≥ 28 is still known only up +to the shrinking window. + +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 OPT(t) at t ≥ 28.** Minimize ε₀ over the 104-dimensional character + codes in C^t that frames can realize. The answer pins the second-order term. +2. **Other frame classes.** PR6660's open question 2: does the depth law change + for mode-changing frames, or for extra refinement between calls? + +## Credit + +Nick Petalas's PR6660 (direct-sum frames, dimension cap, the question); +CubeJerry's PR6327; zxv's #5444; #6828, #6848 and #6849. The two-logarithm bound is +Laurent–Mignotte–Nesterenko (1995). diff --git a/research/refined-recovery-asymptotic/RESULT.json b/research/refined-recovery-asymptotic/RESULT.json new file mode 100644 index 0000000000..1f89c8640b --- /dev/null +++ b/research/refined-recovery-asymptotic/RESULT.json @@ -0,0 +1,100 @@ +{ + "theta_t27_float": 5.453687310396066e-06, + "cycle_length": 26, + "exact_limit": 1500, + "best_approx_index": 414, + "q_n_digits": 200, + "q_n_plus_1_digits": 202, + "norm_q_n_alpha_log10": -202, + "window_after_exact_limit_log10": -254.8, + "lmn_log_lower_bound_at_1e200": -13421005.0, + "continued_fraction_first_30": [ + 29, + 1, + 1, + 1, + 1, + 10, + 1, + 3, + 2, + 1, + 2, + 1, + 4, + 3, + 1, + 17, + 1, + 30, + 3, + 1, + 2, + 11, + 6, + 6, + 1, + 2, + 3, + 1, + 45, + 1 + ], + "table": [ + { + "t": 27, + "opt_bits": 696, + "eps0_bound_log10": -5.26 + }, + { + "t": 28, + "opt_bits": 725, + "eps0_bound_log10": -5.26 + }, + { + "t": 29, + "opt_bits": 755, + "eps0_bound_log10": -5.26 + }, + { + "t": 30, + "opt_bits": 785, + "eps0_bound_log10": -5.26 + }, + { + "t": 40, + "opt_bits": 1081, + "eps0_bound_log10": -5.26 + }, + { + "t": 53, + "opt_bits": 1465, + "eps0_bound_log10": -9.72 + }, + { + "t": 79, + "opt_bits": 2235, + "eps0_bound_log10": -14.17 + }, + { + "t": 100, + "opt_bits": 2857, + "eps0_bound_log10": -14.17 + }, + { + "t": 500, + "opt_bits": 14698, + "eps0_bound_log10": -85.47 + }, + { + "t": 1000, + "opt_bits": 29500, + "eps0_bound_log10": -170.13 + }, + { + "t": 1500, + "opt_bits": 44302, + "eps0_bound_log10": -254.79 + } + ] +} diff --git a/research/refined-recovery-asymptotic/SOURCES.json b/research/refined-recovery-asymptotic/SOURCES.json new file mode 100644 index 0000000000..ae5689199c --- /dev/null +++ b/research/refined-recovery-asymptotic/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-asymptotic/TASK.json b/research/refined-recovery-asymptotic/TASK.json new file mode 100644 index 0000000000..d1ee64dd2a --- /dev/null +++ b/research/refined-recovery-asymptotic/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": "For every t>=27, 1 <= OPT(t) 2^104/13^(8t) <= 1+theta 13^(-4 floor((t-27)/26)) with theta=5.4537e-6, via FRAMES27 followed by cycled PR6660 direct-sum frames; minimum tag ceil(8t log2 13)-104 bits for every t>=27 (continued fraction below 10^200, Laurent-Mignotte-Nesterenko 1995 above).", + "scope_change_reason": "Closes the window of #6849 exponentially and removes its sparse tag ambiguities below 10^200. 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 exponentially shrinking window and the tag determination at every depth.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py (exact rational and big-integer arithmetic plus a 700-digit continued fraction; 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": "What is the exact OPT(t) at t>=28?", + "why_it_matters": "Only the main term and an exponentially small window are known.", + "first_step": "Minimize eps0 over realizable 104-dimensional character codes in C^t at t=28.", + "blocked_by": "Realizability constraints on the stage maps." + }, + { + "question": "Does the depth law change for mode-changing frames or extra refinement between calls?", + "why_it_matters": "Remaining frame classes of PR6660 open question 2.", + "first_step": "Derive the coupled quotient congruences for one mode-changing frame at depth two.", + "blocked_by": "The per-mode scalar recursion no longer separates." + } + ] +} diff --git a/research/refined-recovery-asymptotic/VERIFY.json b/research/refined-recovery-asymptotic/VERIFY.json new file mode 100644 index 0000000000..1e3af02146 --- /dev/null +++ b/research/refined-recovery-asymptotic/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; cycle decay of eps0 by 13^-4 on eight random small instances; theta exact below the #6848 threshold; exact tag bits with eps0 window for 27<=t<=1500 by big integers; 700-digit continued fraction of 8 log2 13 and best-approximation bound covering every t<10^200; Laurent-Mignotte-Nesterenko margin for t>=10^200; 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-asymptotic/verify.py b/research/refined-recovery-asymptotic/verify.py new file mode 100644 index 0000000000..03c6c26eb1 --- /dev/null +++ b/research/refined-recovery-asymptotic/verify.py @@ -0,0 +1,230 @@ +"""Exact checks for the asymptotically exact refined-recovery optimum (stdlib only). + +Prints PASS_REFINED_RECOVERY_ASYMPTOTIC on success. +""" +import hashlib +import itertools +import json +import math +import pathlib +import random +from decimal import Decimal, getcontext +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 +EXACT_LIMIT = 1500 + + +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) + + +CYCLE = 26 # #6660 direct-sum frames +DIGITS = 700 # working precision for the continued fraction of 8 log2 13 +Q_EXP = 200 # claim: exact tag bits for every 27 <= t < 10^Q_EXP + + +def eps_terms(H, r, stages): + """eps0 * 13^(8t) / 2^(r - rank)-normalized: sum over chi outside span^perp of 13^(-wt).""" + out = Fraction(0) + for chi in range(1, 2 ** r): + hs = [] + for j in stages: + h = 0 + for i in range(r): + if chi >> i & 1: + h ^= H[j][i] + hs.append(h) + if any(hs): + out += Fraction(1, 13 ** sum(wt(h) for h in hs)) + return out + + +def toy_cycle(code, reps): + """Appending a direct-sum cycle spanning V multiplies eps0 by at most 13^-4.""" + rng = random.Random(26) + r = 8 + for trial in range(8): + while True: # two stages whose images form a direct sum = V + cyc = [[rng.choice(code) for _ in range(r)] for _ in range(2)] + phi = lambda Hj, u: sum((wt(Hj[i] & u) & 1) << i for i in range(r)) + if rank2([phi(Hj, a) for Hj in cyc for a in reps]) == r: + break + pre = [[rng.choice(code) for _ in range(r)] for _ in range(rng.randint(1, 3))] + if rank2([phi(Hj, a) for Hj in pre for a in reps]) == 0: + continue + H = pre + cyc + cyc + e0 = eps_terms(H, r, range(len(pre))) + e1 = eps_terms(H, r, range(len(pre) + 2)) + e2 = eps_terms(H, r, range(len(pre) + 4)) + # restricted to the full span V (rank r), eps0 counts every chi != 0 + full0 = sum(Fraction(1, 13 ** sum(wt(sum_h(H, j, chi, r)) for j in range(len(pre)))) + for chi in range(1, 2 ** r)) + check(e1 <= full0 / 13 ** 4 and e2 <= full0 / 13 ** 8, "one cycle gains a factor 13^-4") + check(e2 <= e1 <= full0, "monotone") + + +def sum_h(H, j, chi, r): + h = 0 + for i in range(r): + if chi >> i & 1: + h ^= H[j][i] + return h + + +def bits(x): + """ceil(log2 x) for a positive Fraction.""" + k = x.numerator.bit_length() - x.denominator.bit_length() + 1 + while Fraction(2) ** k < x: + k += 1 + while Fraction(2) ** (k - 1) >= x: + k -= 1 + return k + + +def window(theta, t): + """Upper bound on eps0(t) for FRAMES27 followed by #6660 cycles.""" + return theta / Fraction(13) ** (4 * ((t - 27) // CYCLE)) + + +def main(): + rows = load_rows() + code = code_from_rows(rows) + reps, S = coset_data(code) + toy_cycle(code, reps) + rho2 = Fraction(50979600, F) + V27 = (1 + 12 * rho2 ** 25 + 3 * rho2 ** 26) * F ** 27 + theta = V27 * 2 ** CAP / 13 ** 216 - 1 + check(0 < theta < EPS_STAR / 75, "theta below the #6848 threshold") + + # Part 1: exact big-integer determination of the tag for 27 <= t <= EXACT_LIMIT + table = [] + for t in range(27, EXACT_LIMIT + 1): + lo = Fraction(13 ** (8 * t), 2 ** CAP) + b = bits(lo) + check(bits(lo * (1 + window(theta, t))) == b, "tag determined at t=%d" % t) + if t <= 30 or t in (40, 53, 79, 100, 584977) or t % 500 == 0: + table.append({"t": t, "opt_bits": b, + "eps0_bound_log10": round(math.log10(window(theta, t)), 2)}) + + # Part 2: continued fraction of alpha = 8 log2 13, best-approximation bound + getcontext().prec = DIGITS + alpha = 8 * (Decimal(13).ln() / Decimal(2).ln()) + x, cf = alpha, [] + p0, q0, p1, q1 = 0, 1, 1, 0 + qs = [] + while q1 <= 10 ** (Q_EXP + 5): + a = int(x) + cf.append(a) + p0, q0, p1, q1 = p1, q1, a * p1 + p0, a * q1 + q0 + qs.append(q1) + x = 1 / (x - a) + check(cf[:6] == [29, 1, 1, 1, 1, 10], "continued fraction start") + n = next(i for i in range(len(qs) - 1) if qs[i + 1] >= 10 ** Q_EXP) + qn, qn1 = qs[n], qs[n + 1] + dist = abs(qn * alpha - (qn * alpha).to_integral_value()) + check(Decimal(qn1) * Decimal(10) ** (6 - DIGITS) * 10 ** 6 < dist, "precision margin") + # for 0 < t < q_(n+1): ||t alpha|| >= ||q_n alpha|| = dist (best approximation) + # for t > EXACT_LIMIT: window <= log2(1 + w) <= 2 w <= 2 theta 13^(-4 m) < dist + w = window(theta, EXACT_LIMIT + 1) + check(Decimal(2 * w.numerator) / Decimal(w.denominator) < dist, "window below ||q_n alpha||") + check(qn1 >= 10 ** Q_EXP, "covers every t < 10^200") + + # Part 3: t >= 10^200 by Laurent-Mignotte-Nesterenko (1995), Corollary 2: + # log|b2 log 13 - b1 log 2| >= -24.34 (max(log b' + 0.14, 21, 1/2))^2 log A1 log A2, + # D = 1, log A1 = 1, log A2 = log 13, b' = b1/log A2 + b2/log A1 <= 20 t here. + # Both sides are monotone in t, so it suffices to compare at t0 = 10^200, in natural logs: + # log window <= log(2 theta) - 4 log(13) ((t-27)//26), linear in t; + # log ||t alpha|| >= LMN bound - log log 2, polylogarithmic in t. + t0 = 10 ** Q_EXP + log_window = math.log(2 * float(theta)) - 4 * math.log(13) * ((t0 - 27) // CYCLE) + logb = math.log(20) + Q_EXP * math.log(10) + lmn = -24.34 * max(logb + 0.14, 21.0, 0.5) ** 2 * 1.0 * math.log(13) - math.log(math.log(2)) + check(log_window < -1e199 and lmn > -2e7, "LMN margin at 10^200") + check(log_window < 10 ** 6 * lmn, "window far below the LMN bound (factor 10^6 in the exponent)") + + result = { + "theta_t27_float": float(theta), + "cycle_length": CYCLE, + "exact_limit": EXACT_LIMIT, + "best_approx_index": n, + "q_n_digits": len(str(qn)), + "q_n_plus_1_digits": len(str(qn1)), + "norm_q_n_alpha_log10": int(dist.adjusted()), + "window_after_exact_limit_log10": round(math.log10(w), 1), + "lmn_log_lower_bound_at_1e200": round(lmn, 1), + "continued_fraction_first_30": cf[:30], + "table": table, + } + 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("exact tags for all t >= 27 (cf < 10^%d, LMN above); ||q_n alpha|| ~ 1e%d; window after t=%d ~ 1e%.0f" + % (Q_EXP, dist.adjusted(), EXACT_LIMIT, math.log10(w))) + print("PASS_REFINED_RECOVERY_ASYMPTOTIC") + + +if __name__ == "__main__": + main()