diff --git a/research/refined-recovery-all-depths/PROOF.md b/research/refined-recovery-all-depths/PROOF.md
new file mode 100644
index 0000000000..ee92cf8dca
--- /dev/null
+++ b/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.
diff --git a/research/refined-recovery-all-depths/README.md b/research/refined-recovery-all-depths/README.md
new file mode 100644
index 0000000000..d3a8ecb533
--- /dev/null
+++ b/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.
diff --git a/research/refined-recovery-all-depths/RESULT.json b/research/refined-recovery-all-depths/RESULT.json
new file mode 100644
index 0000000000..617dcf35bf
--- /dev/null
+++ b/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
+  }
+ ]
+}
diff --git a/research/refined-recovery-all-depths/SOURCES.json b/research/refined-recovery-all-depths/SOURCES.json
new file mode 100644
index 0000000000..ae5689199c
--- /dev/null
+++ b/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"
+    }
+  ]
+}
diff --git a/research/refined-recovery-all-depths/TASK.json b/research/refined-recovery-all-depths/TASK.json
new file mode 100644
index 0000000000..b32c67226c
--- /dev/null
+++ b/research/refined-recovery-all-depths/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": "Optimal worst-case fiber of PR6660 refined chains at every depth t>=27: 13^(8t)/2^104 <= min_U max_y |fiber(y)| <= (1+theta) 13^(8t)/2^104 with theta=5.4537e-6, so the minimum tag is ceil(8t log2 13)-104 bits (696, 725, 755, 785, ...) except possibly at sparse depths, the first being t=584977; exactly 100 bits below identity frames for 27<=t<=400.",
+  "scope_change_reason": "Answers PR6660 open question 1 (optimum at t>=27) up to a 5.5e-6 relative window, using the main Fourier term as a universal lower bound and #6828/#6848 for the upper bound. 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 bound and the tag-bit determination; leave the exact value of eps0-minimization at t>=28 open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; verify.py (exact rational and big-integer arithmetic plus a 60-digit decimal scan; 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 optimum at t>=28, i.e. the minimum eps0 over realizable 104-dimensional character codes in C^t?",
+      "why_it_matters": "Pins OPT(t) exactly instead of to a 5.5e-6 relative window.",
+      "first_step": "Compute the weight enumerator of the FRAMES27 character code extended by well-chosen extra stages and compare with a code-theoretic lower bound.",
+      "blocked_by": "Realizability constraints on the stage maps phi_j = mu + psi_j."
+    },
+    {
+      "question": "How fast can eps0(t) tend to zero?",
+      "why_it_matters": "Determines how quickly OPT(t) approaches 13^(8t)/2^104.",
+      "first_step": "Random-code heuristic 2^(104-4t)(16F/13^8)^t; test with random psi_j frames at t=28..32.",
+      "blocked_by": "Nothing; routine."
+    }
+  ]
+}
diff --git a/research/refined-recovery-all-depths/VERIFY.json b/research/refined-recovery-all-depths/VERIFY.json
new file mode 100644
index 0000000000..7b8188fa8a
--- /dev/null
+++ b/research/refined-recovery-all-depths/VERIFY.json
@@ -0,0 +1,21 @@
+{
+  "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=[8,4,4] self-dual and coset sums from M; hat w(h)=13^(8-wt h) on C; Poisson identity, zero fiber >= 13^(8t)/2^rank and eps0 monotonicity on twelve random small instances; theta=eps0(FRAMES27) exact and below the #6848 threshold; exact tag bits and 100-bit saving vs identity frames for 27<=t<=400; first possibly ambiguous depth 584977 by 60-digit scan; 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-all-depths/verify.py b/research/refined-recovery-all-depths/verify.py
new file mode 100644
index 0000000000..f1b54a8859
--- /dev/null
+++ b/research/refined-recovery-all-depths/verify.py
@@ -0,0 +1,199 @@
+"""Exact checks for the optimal refined-recovery fiber at every depth t >= 27 (stdlib only).
+
+Prints PASS_REFINED_RECOVERY_ALL_DEPTHS 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_TABLE = range(27, 401)
+SCAN_LIMIT = 600000
+
+
+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)
+
+
+def toy_checks(code, reps, S):
+    """Section 1 on random small instances: coset form = character form, the main-term
+    lower bound, and monotonicity of eps0 under appending a stage inside the span."""
+    rng = random.Random(27)
+    for trial in range(12):
+        t = rng.choice((2, 3))
+        r = rng.randint(3, 9)
+        # phi_j(u)_i = h_{j,i} . u with h_{j,i} in C = C^perp (so phi_j kills C)
+        H = [[rng.choice(code) for _ in range(r)] for _ in range(t)]
+        phi = lambda j, u: sum((wt(H[j][i] & u) & 1) << i for i in range(r))
+        lhs = 0
+        for a in itertools.product(reps, repeat=t):
+            acc = 0
+            for j in range(t):
+                acc ^= phi(j, a[j])
+            if acc == 0:
+                p = 1
+                for j in range(t):
+                    p *= S[a[j]]
+                lhs += p
+        def hj(j, chi):
+            h = 0
+            for i in range(r):
+                if chi >> i & 1:
+                    h ^= H[j][i]
+            return h
+        def terms(tt):
+            return [math.prod(13 ** (8 - wt(hj(j, chi))) for j in range(tt)) for chi in range(2 ** r)]
+        rhs = Fraction(sum(terms(t)), 2 ** r)
+        check(lhs == rhs, "zero fiber = 2^-r sum_chi prod_j 13^(8-wt h_j)")
+        images = [phi(j, a) for j in range(t) for a in reps]
+        rk = rank2(images)
+        main = Fraction(13 ** (8 * t), 2 ** rk)
+        check(lhs >= main, "zero fiber >= 13^(8t) / 2^rank")
+        # appending a stage that repeats stage 0 keeps the rank and the main term
+        H.append(list(H[0]))
+        lhs2 = Fraction(sum(terms(t + 1)), 2 ** r)
+        eps = lhs / main - 1
+        eps2 = lhs2 / Fraction(13 ** (8 * (t + 1)), 2 ** rk) - 1
+        check(0 <= eps2 <= eps, "eps0 is non-increasing when a stage is appended")
+        H.pop()
+
+
+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 main():
+    rows = load_rows()
+    code = code_from_rows(rows)
+    reps, S = coset_data(code)
+    toy_checks(code, reps, S)
+    rho2 = Fraction(50979600, F)
+
+    # depth 27: #6828 exact minimum, FRAMES27 has dim D = 4 (rank 104)
+    V27 = (1 + 12 * rho2 ** 25 + 3 * rho2 ** 26) * F ** 27
+    theta = V27 * 2 ** CAP / 13 ** 216 - 1
+    check(0 < theta < EPS_STAR, "FRAMES27 eps0 below the #6848 threshold")
+    check(theta < Fraction(546, 10 ** 8), "theta < 5.46e-6")
+
+    # exact table: lower main term and upper main term * (1 + theta)
+    table = []
+    for t in EXACT_TABLE:
+        lo = Fraction(13 ** (8 * t), 2 ** CAP)
+        hi = lo * (1 + theta)
+        b = bits(lo)
+        check(bits(hi) == b, "tag bits determined at t=%d" % t)
+        check(b == math.ceil(8 * t * math.log2(13) - CAP - 1e-9), "closed form")
+        A = Fraction(13 ** (8 * t) + 14 * 13 ** (4 * t) + 1, 16)
+        ident = bits(A)
+        table.append({"t": t, "opt_bits": b, "identity_bits": ident, "saving": ident - b})
+    check(table[0]["opt_bits"] == 696 and table[1]["opt_bits"] == 725, "t=27,28 bits")
+    check({row["saving"] for row in table} == {100}, "exactly 100 bits saved vs identity frames")
+    # main term beats the #6828 AM-GM floor from t = 28 on (that floor at t = 28 is < 252.51123)
+    check(Fraction(13 ** 224, 2 ** CAP) / F ** 28 > Fraction(25251123, 10 ** 5), "beats d=8 floor at t=28")
+    # at t = 27 the exact value is above the main term by theta
+    check(V27 > Fraction(13 ** 216, 2 ** CAP), "t=27 exact value above main term")
+
+    # scan for depths where the window (1+theta) could straddle a power of two
+    getcontext().prec = 60
+    alpha = 8 * (Decimal(13).ln() / Decimal(2).ln())
+    width = Decimal(math.log2(1 + float(theta))) * Decimal("1.000001")
+    first = None
+    for t in range(27, SCAN_LIMIT):
+        f = (alpha * t) % 1
+        if f > 1 - width:
+            first = t
+            break
+    check(first == 584977, "first ambiguous depth")
+    for t in (584977,):  # confirm with exact-enough decimal margin
+        f = (alpha * t) % 1
+        check(Decimal("7.8e-6") < 1 - f < Decimal("7.9e-6"), "ambiguous depth margin")
+
+    result = {
+        "theta_t27_float": float(theta),
+        "eps_star_float": float(EPS_STAR),
+        "first_possibly_ambiguous_depth": first,
+        "table": [row for row in table if row["t"] <= 40 or row["t"] % 50 == 0],
+    }
+    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("theta = %.6e; bits t=27..30: %s; first ambiguous depth %d"
+          % (theta, [r["opt_bits"] for r in table[:4]], first))
+    print("PASS_REFINED_RECOVERY_ALL_DEPTHS")
+
+
+if __name__ == "__main__":
+    main()