Refined recovery: optimum → 13^(8t)/2^104 exponentially; exact tag ⌈8t·log₂13⌉−104 at every depth t≥27 (no κ)

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.

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).

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

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

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