Refined recovery: the second-order term ε_t of the optimum decays at 4.0–14.8 bits per stage (no κ)

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.

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.

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
+  }
+ ]
+}

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}