Refined recovery: the second-order term ε_t decays at exactly 4·log₂13 ≈ 14.80 bits per stage (no κ)

research/refined-recovery-eps-exact-rate/PROOF.md

@@ -0,0 +1,86 @@
+# The second-order term of the refined-recovery optimum decays at exactly 4·log₂13 bits per stage
+
+Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0.
+
+## Setting
+
+We use the notation of [#6851](https://github.com/CrocSwap/integer-mult-bounds/pull/6851)
+and its predecessors. OPT(t) = 2^(−104)·13^(8t)·(1+ε_t), where ε_t = min_U S(U)
+and
+
+    S(U) = Σ_{χ ∈ V^, χ ≠ 0} 13^(−W(χ)),   W(χ) = Σ_j wt h_j(χ),   h_j(χ) = χ∘φ_j ∈ C.
+
+#6851 proved the following:
+
+* **Jensen.** ε_t ≥ (2^104−1)·13^(−4t·2^104/(2^104−1)) for every frame
+  sequence.
+* **First moment.** ε_t ≤ E_t, which decays at about 4 bits per stage.
+
+It left the exact rate open, somewhere between 4.0 and 14.8 bits per stage.
+
+## Theorem
+
+    lim_{t→∞} −log₂ ε_t / t = 4·log₂13 = 14.8018…
+
+Quantitatively, ε_t ≤ (2^104 − 1)·13^(−w_t) for the certified values w_t below.
+It is valid whenever w_t > 0.
+
+| t | 60 | 100 | 200 | 400 | 1000 |
+|---|---:|---:|---:|---:|---:|
+| w_t | 80 | 200 | 532 | 1236 | 3444 |
+| w_t / t | 1.33 | 2.00 | 2.66 | 3.09 | 3.44 |
+| log₂ upper bound on ε_t | −192 | −636 | −1865 | −4470 | −12640 |
+| log₂ Jensen lower bound | −784 | −1376 | −2856 | −5817 | −14698 |
+
+## Proof
+
+**The upper rate is at least 4·log₂13.** This uses PR6660's frame family, as in
+#6851: φ_j = μ + ψ_j with ψ_1 = 0 and ψ_2, …, ψ_t uniform and independent.
+
+* **χ with a nonzero R′-component** (2^104 − 16 of them). Here h_2, …, h_t are
+  independent and uniform on C. Write X for the weight of a uniform word of C:
+  it is 0 with probability 1/16, 4 with probability 14/16 and 8 with
+  probability 1/16. For 0 < r ≤ 1, Markov's inequality applied to r^W gives
+
+      P(W(χ) < w) ≤ r^(−w) · m(r)^(t−1),   m(r) = E[r^X] = (1 + 14r⁴ + r⁸)/16.
+
+* **The other 15 χ.** Their W is 4t or 8t, which is at least w whenever w ≤ 4t.
+
+If (2^104 − 16)·r^(−w)·m(r)^(t−1) < 1, a union bound shows that some choice of
+the ψ_j has W(χ) ≥ w for every χ ≠ 0. That choice has S ≤ (2^104 − 1)·13^(−w).
+verify.py certifies the largest such w (a multiple of 4) with exact rational r
+for each tabulated t.
+
+For the limit, fix c < 4. Then f(λ) = λc + log m(e^(−λ)) has f(0) = 0 and
+f′(0) = c − E[X] = c − 4 < 0. So some r = e^(−λ) < 1 gives r^(−c)·m(r) < 1. Then
+(2^104−16)·r^(−ct)·m(r)^(t−1) → 0, so w = 4⌊ct/4⌋ is admissible for all large t,
+and liminf −log₂ε_t/t ≥ c·log₂13. verify.py exhibits exact certificates r for
+c = 3, 3.5, 3.9 and 3.99. As a control, no r works at c = 4, because
+r^(−4)·m(r) ≥ 1 by AM–GM.
+
+**The lower rate is at most 4·log₂13.** This is #6851's Jensen bound.
+
+Each frame sequence in the table has S below #6848's threshold, so its max fiber
+equals its zero fiber. The bound therefore controls OPT(t) itself. ∎
+
+## Interpretation
+
+Every nonzero character must accumulate total weight close to the average 4t.
+A random member of PR6660's frame family achieves this, because W(χ) is a sum of
+independent weights. #6851's first-moment rate of 4 bits per stage came from
+rare characters with W ≈ 0. Rare means probability about 16^(−t) each; the union
+bound removes them once t is large enough. The convergence of w_t/t to 4 is slow:
+it is 3.44 at t = 1000.
+
+## Scope
+
+The premises are cited and not replayed here:
+
+* PR6660's frame family and dimension cap;
+* #6848's max-fiber theorem;
+* #6849's and #6851's Poisson and Jensen statements.
+
+All of these are open and unmerged. The upper bound is existential. 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.

research/refined-recovery-eps-exact-rate/README.md

@@ -0,0 +1,77 @@
+# Refined recovery: ε_t decays at exactly 4·log₂13 bits per stage
+
+Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0.
+
+**Scoped proof with exact finite corroboration; no κ.** This answers open
+question 1 of [#6851](https://github.com/CrocSwap/integer-mult-bounds/pull/6851).
+That PR showed the second-order term ε_t of
+
+    OPT(t) = 2^(−104)·13^(8t)·(1 + ε_t)
+
+decays at between 4.0 and 14.8 bits per stage. Here:
+
+    lim_{t→∞} −log₂ ε_t / t = 4·log₂13 ≈ 14.8018
+
+So the Jensen lower bound of #6851 gives the true rate.
+
+**How.**
+
+- *#6851's gap.* The first-moment bound there was dominated by rare characters χ
+  whose total weight W(χ) is near 0.
+- *Concentration.* In PR6660's frame family with random ψ_j, each W(χ) is a sum of
+  t − 1 independent weights of uniform words of C, with mean 4.
+- *Union bound.* A Chernoff bound P(W < w) ≤ r^(−w)·m(r)^(t−1), with
+  m(r) = (1+14r⁴+r⁸)/16, combined with a union bound over the 2^104 characters,
+  yields frames in which every χ has W(χ) ≥ w_t. Then S ≤ (2^104−1)·13^(−w_t).
+- *Limit.* Cramér's theorem gives w_t/t → 4.
+
+| t | 60 | 100 | 200 | 400 | 1000 |
+|---|---:|---:|---:|---:|---:|
+| w_t / t | 1.33 | 2.00 | 2.66 | 3.09 | 3.44 |
+| log₂ ε_t ≤ | −192 | −636 | −1865 | −4470 | −12640 |
+| log₂ ε_t ≥ (Jensen) | −784 | −1376 | −2856 | −5817 | −14698 |
+
+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-exact-rate/verify.py
+python3.12 -I -O -W error -B research/refined-recovery-eps-exact-rate/verify.py
+python3.12 -B scripts/research_package.py --package research/refined-recovery-eps-exact-rate
+```
+
+Each run prints `PASS_REFINED_RECOVERY_EPS_EXACT_RATE` in about 30 s. It checks:
+
+* the weights of C, and that m(1/13) equals #6851's q;
+* the exact rational Chernoff certificates for every tabulated t, with the
+  largest admissible w_t;
+* the Cramér certificates for slopes 3, 3.5, 3.9 and 3.99;
+* the control that no certificate exists at slope 4.
+
+## Limitations
+
+The result cites PR6660's frame family, #6848's max-fiber theorem, and the
+Poisson identity and Jensen bound of #6849 and #6851. All are unmerged, and none
+is replayed here.
+
+The upper bound is existential, from a union bound, and the convergence of the
+rate is slow. For t < 60 the bound of #6851 is better.
+
+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. **Second-order constant.** Determine lim (−log₂ε_t − 4t·log₂13), or at least
+   the √t-order correction from the Chernoff gap.
+2. **Explicit frames.** Find explicit near-constant-weight character codes, for
+   example from a Singer cycle of GF(2^104) restricted to a subgroup orbit.
+
+## Credit
+
+Nick Petalas's PR6660; CubeJerry's PR6327; zxv's #5444; #6848, #6849 and #6851.
+Chernoff and Cramér bounds are classical.

research/refined-recovery-eps-exact-rate/RESULT.json

@@ -0,0 +1,59 @@
+{
+ "rate_bits_per_stage": 14.801759,
+ "cramer_certificates_slope_to_r": {
+  "3": "999/1000",
+  "7/2": "999/1000",
+  "39/10": "999/1000",
+  "399/100": "999/1000"
+ },
+ "table": [
+  {
+   "t": 40,
+   "w_t": 24,
+   "r": "6/25",
+   "w_over_t": 0.6,
+   "log2_eps_upper": 15.2,
+   "log2_eps_lower": -488.1
+  },
+  {
+   "t": 60,
+   "w_t": 80,
+   "r": "2/5",
+   "w_over_t": 1.3333,
+   "log2_eps_upper": -192.0,
+   "log2_eps_lower": -784.1
+  },
+  {
+   "t": 100,
+   "w_t": 200,
+   "r": "12/25",
+   "w_over_t": 2.0,
+   "log2_eps_upper": -636.1,
+   "log2_eps_lower": -1376.2
+  },
+  {
+   "t": 200,
+   "w_t": 532,
+   "r": "59/100",
+   "w_over_t": 2.66,
+   "log2_eps_upper": -1864.6,
+   "log2_eps_lower": -2856.4
+  },
+  {
+   "t": 400,
+   "w_t": 1236,
+   "r": "67/100",
+   "w_over_t": 3.09,
+   "log2_eps_upper": -4469.7,
+   "log2_eps_lower": -5816.7
+  },
+  {
+   "t": 1000,
+   "w_t": 3444,
+   "r": "77/100",
+   "w_over_t": 3.444,
+   "log2_eps_upper": -12640.3,
+   "log2_eps_lower": -14697.8
+  }
+ ]
+}

research/refined-recovery-eps-exact-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"
+    }
+  ]
+}

research/refined-recovery-eps-exact-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": "lim -log2(eps_t)/t = 4 log2 13 for the second-order term of OPT(t)=2^-104 13^(8t)(1+eps_t): Chernoff plus union bound over PR6660's random I+VE frames gives eps_t <= (2^104-1)13^(-w_t) with certified w_t (w_t/t = 3.44 at t=1000), Cramer gives w_t/t -> 4, Jensen (#6851) gives the matching lower rate.",
+  "scope_change_reason": "Answers #6851 open question 1 (exact decay rate). 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 exact exponential rate; leave the subexponential correction 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": "What is the subexponential correction to -log2 eps_t - 4t log2 13?",
+      "why_it_matters": "Sharpens OPT(t) beyond the exponential rate.",
+      "first_step": "Combine the Chernoff tail with a second-moment lower bound on the minimum character weight.",
+      "blocked_by": "Nothing; routine."
+    },
+    {
+      "question": "Explicit near-constant-weight frames?",
+      "why_it_matters": "The upper bound is existential.",
+      "first_step": "Use Singer-cycle orbits in GF(2^104) to build psi_j with nearly equal W(chi).",
+      "blocked_by": "Code construction."
+    }
+  ]
+}

research/refined-recovery-eps-exact-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 weights and m(1/13)=q; exact rational Chernoff certificates and maximal w_t for t in 40,60,100,200,400,1000; Cramer certificates for slopes 3, 3.5, 3.9, 3.99 and none at 4; RESULT.json recomputation."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same explicit checks under optimized Python."
+    }
+  ]
+}