Refined recovery at every depth t≥27: optimum = 13^(8t)/2^104 within 5.5·10⁻⁶; exact tag ⌈8t·log₂13⌉−104 bits (no κ)

research/refined-recovery-all-depths/PROOF.md

@@ -0,0 +1,116 @@
+# The optimal refined-recovery fiber at every depth t ≥ 27
+
+Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0.
+
+## Setting
+
+Objects are those of Nick Petalas's
+[PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660)
+(head `b6de532e`), built on CubeJerry's PR6327 and the matrix M of #5444.
+Frames U_j ∈ G = {U ∈ GL_112(ℤ) : MᵀU = Mᵀ}. Let W_j = (U_(j−1)⋯U_1)^(−1),
+let φ_j : Q = F2^8/C → F2^112 be the map induced by W_j M mod 2, and let
+ρ = dim(N_1+⋯+N_t) be the rank of the frame sequence. By PR6660 (c), ρ ≤ 104.
+
+Write OPT(t) = min_U max_y |fiber(y)|. PR6660 proves OPT(t) = F^t for t ≤ 26.
+
+## Theorem
+
+For every t ≥ 27,
+
+    13^(8t) / 2^104  ≤  OPT(t)  ≤  (1 + θ) · 13^(8t) / 2^104,
+    θ = 5.4537·10⁻⁶ (the exact rational is computed by verify.py).
+
+Consequently, the minimum packed tag at depth t is
+
+    ⌈log₂ OPT(t)⌉ = ⌈8t·log₂13⌉ − 104
+
+for every t ≥ 27 except possibly a sparse set of depths. At those depths
+{8t·log₂13} lies within log₂(1+θ) < 7.9·10⁻⁶ of 1. The first such depth is
+t = 584,977. The values are 696, 725, 755, 785, … bits. For 27 ≤ t ≤ 400 this
+is exactly 100 bits below the identity-frame tag ⌈log₂ A_t⌉ of PR6327.
+
+In words: past depth 26, mode-preserving frames save exactly the 104 parity bits
+of the dimension cap against the trivial count 13^(8t). Up to a 5.5·10⁻⁶ relative
+factor, they save nothing more.
+
+## 1. Lower bound: the main Fourier term (all frames)
+
+PR6660 §5 gives the zero fiber as Σ over (u_j) with Σ_j W_j M u_j ≡ 0 of
+Π_j w(u_j), where w(u) = 7^(8−wt u) 6^(wt u). Write each φ_j through
+χ ∈ F2^r on an ambient F2^r containing all images. For each χ, χ∘φ_j is the
+character u ↦ (−1)^(h_j(χ)·u), with h_j(χ) ∈ C^⊥ = C. Poisson summation gives
+
+    |fiber(0)| = 2^(−r) Σ_{χ ∈ F2^r} Π_j ŵ(h_j(χ)),   ŵ(h) = Σ_u w(u)(−1)^(h·u) = 13^(8 − wt h).
+
+Every term is positive. The χ with all h_j(χ) = 0 are those orthogonal to the
+span N_1+⋯+N_t, and there are 2^(r−ρ) of them, each contributing 13^(8t). Hence
+
+    |fiber(0)| = 2^(−ρ) 13^(8t) (1 + ε₀),
+    ε₀ = 2^(ρ−r) Σ_{χ: some h_j(χ) ≠ 0} Π_j 13^(−wt h_j(χ)) ≥ 0.
+
+Since
+ρ ≤ 104, every frame sequence has max_y |fiber(y)| ≥ |fiber(0)| ≥ 13^(8t)/2^104.
+
+This is the statement that the zero target gets at least the average share of
+all 13^(8t) chains among the 2^ρ parity targets. The positivity of ŵ is what
+makes that true.
+
+verify.py checks the identity, the bound and the next paragraph's monotonicity
+exactly on twelve random small instances (t ∈ {2,3}, r ≤ 9).
+
+**Monotonicity.** Suppose the new stage's image lies in the existing span, so ρ
+is unchanged. Appending the stage multiplies each χ-term by 13^(−wt h_(t+1)(χ)),
+which is at most 1. So ε₀ cannot increase.
+
+## 2. Upper bound: FRAMES27, then repeat the last frame
+
+[#6828](https://github.com/CrocSwap/integer-mult-bounds/pull/6828) gives explicit
+frames FRAMES27 with ρ = 104 (dim D = 4). Their zero fiber is
+(1+12ρ₂^25+3ρ₂^26) F^27, so
+
+    θ := ε₀(FRAMES27) = (1+12ρ₂^25+3ρ₂^26) F^27 · 2^104 / 13^216 − 1 = 5.4537·10⁻⁶.
+
+For t > 27 append U_j = I. The identity is in G, so W_j = W_27 for j > 27, ρ
+stays 104, and by monotonicity ε₀(t) ≤ θ.
+
+[#6848](https://github.com/CrocSwap/integer-mult-bounds/pull/6848) proves that
+any frame sequence with ε₀ ≤ ε* = (1/13)/((23/12)^8 − 1) ≈ 4.25·10⁻⁴ has
+max_y |fiber(y)| = |fiber(0)|. Since θ < ε*/75,
+
+    OPT(t) ≤ |fiber(0)| = 2^(−104) 13^(8t) (1 + ε₀(t)) ≤ (1+θ) 13^(8t)/2^104.   ∎
+
+## 3. Tag bits
+
+⌈log₂ OPT(t)⌉ is determined whenever [log₂ lo, log₂ lo + log₂(1+θ)] contains no
+integer, where lo = 13^(8t)/2^104. verify.py checks this exactly with big
+integers for 27 ≤ t ≤ 400, together with the comparison against ⌈log₂ A_t⌉. It
+then scans {8t·log₂13} at 60-digit precision for t < 600,000. The first depth
+whose window could straddle a power of two is t = 584,977, with
+1 − {8t·log₂13} ≈ 7.83·10⁻⁶.
+
+## Relation to #6828's floor
+
+The main term 13^(8t)/2^104 is below #6828's exact depth-27 value; it falls short
+by the factor 1+θ. For t ≥ 28 it is above #6828's AM–GM floor. For example, at
+t = 28 it is 252.51124·F^28 against 252.51122·F^28. #6828's balanced E-valued
+patterns would fall *below* the main term at t ≥ 28, so they are not realizable
+there.
+
+## 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.
+
+The premises are cited and not replayed here:
+
+* PR6660's chain bijection and dimension cap;
+* #6828's FRAMES27 value and rank;
+* #6848's max-fiber theorem.
+
+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-all-depths/README.md

@@ -0,0 +1,95 @@
+# Optimal refined-recovery fiber at every depth t ≥ 27
+
+Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0.
+
+**Scoped proof with exact finite corroboration; no κ.** This answers open
+question 1 of Nick Petalas's
+[PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660)
+(`research/refined-recovery-longer-chains`, head `b6de532e`): the optimum at
+t ≥ 27, which that PR leaves at "strictly larger than F^t". The answer holds
+up to a relative factor of 5.5·10⁻⁶, and it fixes the exact tag size.
+
+    13^(8t) / 2^104  ≤  min_U max_y |fiber(y)|  ≤  (1 + 5.46·10⁻⁶) · 13^(8t) / 2^104     (t ≥ 27)
+
+| depth t | 27 | 28 | 29 | 30 | 40 | 100 |
+|---|---:|---:|---:|---:|---:|---:|
+| optimal tag bits ⌈log₂ OPT⌉ | **696** | **725** | **755** | **785** | **1081** | **2857** |
+| identity frames ⌈log₂ A_t⌉ | 796 | 825 | 855 | 885 | 1181 | 2957 |
+
+The optimal tag is ⌈8t·log₂13⌉ − 104 bits for every t ≥ 27. The only possible
+exceptions are depths where {8t·log₂13} lies within 7.9·10⁻⁶ of 1; the first such
+depth is t = 584,977. Past depth 26, the best mode-preserving frames save exactly
+the 104 parity bits of PR6660's dimension cap against the trivial chain count
+13^(8t), and essentially nothing more. That is exactly 100 bits better than
+identity frames (checked for 27 ≤ t ≤ 400).
+
+**Proof in two lines.**
+
+- *Lower bound, for every frame sequence.* Poisson summation writes the zero
+  fiber as a sum of positive terms Π_j 13^(8 − wt h_j). The 2^(r−ρ) characters
+  that vanish on the span each contribute 13^(8t), so |fiber(0)| ≥ 13^(8t)/2^ρ
+  ≥ 13^(8t)/2^104. Informally, the zero target receives at least its average
+  share of all chains.
+- *Upper bound.* Take #6828's FRAMES27 (rank 104, ε₀ = 5.45·10⁻⁶) and repeat the
+  last frame (U_j = I). Appending stages inside the span can only lower ε₀. Then
+  #6848's theorem (max fiber = zero fiber when ε₀ ≤ 4.2·10⁻⁴) gives
+  max_y = |fiber(0)| ≤ (1+5.46·10⁻⁶)·13^(8t)/2^104.
+
+**What this implies for #6828.** The main term beats #6828's AM–GM floors for
+t ≥ 28. Its balanced E-valued patterns would give zero fibers *below* 13^(8t)/2^104
+there, so they are not realizable.
+
+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-all-depths/verify.py
+python3.12 -I -O -W error -B research/refined-recovery-all-depths/verify.py
+python3.12 -B scripts/research_package.py --package research/refined-recovery-all-depths
+```
+
+Each run prints `PASS_REFINED_RECOVERY_ALL_DEPTHS` in about one second. It
+checks:
+
+* C and the coset sums from the pinned matrix, and ŵ(h) = 13^(8 − wt h) for all
+  h ∈ C;
+* the Poisson identity, the main-term bound and monotonicity of ε₀, exactly, on
+  twelve random small instances;
+* θ exactly, and θ < ε*/75;
+* the exact tag bits and the 100-bit saving with big integers for 27 ≤ t ≤ 400;
+* the first possibly ambiguous depth, by a 60-digit scan up to 600,000;
+* RESULT.json.
+
+## Limitations
+
+The upper bound relies on two packages that are open and unmerged, and does not
+replay either:
+
+* #6828, for the FRAMES27 value and rank;
+* #6848, for the max-fiber theorem.
+
+Like those packages, it also cites PR6660's chain bijection and dimension cap,
+and PR6327's box facts. Neither fork commit is reachable here, so SOURCES.json
+does not pin them. The exact value of OPT(t) for t ≥ 28 is pinned only to the
+relative window 5.46·10⁻⁶, not exactly. The tag size is ambiguous at sparse
+depths, the first being t = 584,977. 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 ε₀ = Σ 13^(−wt) over the 104-dimensional
+   character codes realizable by frames. This is a weight-enumerator problem for
+   a code inside C^t.
+2. **Faster convergence.** Since ε₀(t) is non-increasing, how fast can it go to
+   0? A random-code heuristic suggests 2^(104−4t)·(16F/13^8)^t.
+
+## Credit
+
+Nick Petalas's PR6660 supplies the chain bijection, the dimension cap and the open
+question. CubeJerry's PR6327 supplies the chain model, F and A_t. zxv's #5444
+supplies M. #6828 supplies FRAMES27 and #6848 the max-fiber theorem. Poisson
+summation is classical.

research/refined-recovery-all-depths/RESULT.json

@@ -0,0 +1,139 @@
+{
+ "theta_t27_float": 5.453687310396066e-06,
+ "eps_star_float": 0.0004246929745945579,
+ "first_possibly_ambiguous_depth": 584977,
+ "table": [
+  {
+   "t": 27,
+   "opt_bits": 696,
+   "identity_bits": 796,
+   "saving": 100
+  },
+  {
+   "t": 28,
+   "opt_bits": 725,
+   "identity_bits": 825,
+   "saving": 100
+  },
+  {
+   "t": 29,
+   "opt_bits": 755,
+   "identity_bits": 855,
+   "saving": 100
+  },
+  {
+   "t": 30,
+   "opt_bits": 785,
+   "identity_bits": 885,
+   "saving": 100
+  },
+  {
+   "t": 31,
+   "opt_bits": 814,
+   "identity_bits": 914,
+   "saving": 100
+  },
+  {
+   "t": 32,
+   "opt_bits": 844,
+   "identity_bits": 944,
+   "saving": 100
+  },
+  {
+   "t": 33,
+   "opt_bits": 873,
+   "identity_bits": 973,
+   "saving": 100
+  },
+  {
+   "t": 34,
+   "opt_bits": 903,
+   "identity_bits": 1003,
+   "saving": 100
+  },
+  {
+   "t": 35,
+   "opt_bits": 933,
+   "identity_bits": 1033,
+   "saving": 100
+  },
+  {
+   "t": 36,
+   "opt_bits": 962,
+   "identity_bits": 1062,
+   "saving": 100
+  },
+  {
+   "t": 37,
+   "opt_bits": 992,
+   "identity_bits": 1092,
+   "saving": 100
+  },
+  {
+   "t": 38,
+   "opt_bits": 1021,
+   "identity_bits": 1121,
+   "saving": 100
+  },
+  {
+   "t": 39,
+   "opt_bits": 1051,
+   "identity_bits": 1151,
+   "saving": 100
+  },
+  {
+   "t": 40,
+   "opt_bits": 1081,
+   "identity_bits": 1181,
+   "saving": 100
+  },
+  {
+   "t": 50,
+   "opt_bits": 1377,
+   "identity_bits": 1477,
+   "saving": 100
+  },
+  {
+   "t": 100,
+   "opt_bits": 2857,
+   "identity_bits": 2957,
+   "saving": 100
+  },
+  {
+   "t": 150,
+   "opt_bits": 4337,
+   "identity_bits": 4437,
+   "saving": 100
+  },
+  {
+   "t": 200,
+   "opt_bits": 5817,
+   "identity_bits": 5917,
+   "saving": 100
+  },
+  {
+   "t": 250,
+   "opt_bits": 7297,
+   "identity_bits": 7397,
+   "saving": 100
+  },
+  {
+   "t": 300,
+   "opt_bits": 8778,
+   "identity_bits": 8878,
+   "saving": 100
+  },
+  {
+   "t": 350,
+   "opt_bits": 10258,
+   "identity_bits": 10358,
+   "saving": 100
+  },
+  {
+   "t": 400,
+   "opt_bits": 11738,
+   "identity_bits": 11838,
+   "saving": 100
+  }
+ ]
+}

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