diff --git a/research/refined-recovery-max-fiber/PROOF.md b/research/refined-recovery-max-fiber/PROOF.md
new file mode 100644
index 0000000000..745f436b4e
--- /dev/null
+++ b/research/refined-recovery-max-fiber/PROOF.md
@@ -0,0 +1,183 @@
+# The maximum fiber equals the zero fiber near the Fourier main term
+
+Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0.
+
+## Setting
+
+All objects are those of Nick Petalas's
+[PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660)
+(`research/refined-recovery-longer-chains`, head
+`b6de532eff668a7daf8f2f98668f97af5af41338`), built on CubeJerry's PR6327 and the
+112×8 matrix M of #5444. R is nearest-integer rounding with half ties away from
+zero, and Q(s) = {q : R((s+56q)/52) = q}. The chain is z_1 = K(2x),
+z_(j+1) = K(U_j z_j), with fixed frames U_j ∈ G, and W_j = (U_(j−1)⋯U_1)^(−1).
+C = ker_F2(M mod 2) is the self-dual [8,4,4] code.
+
+We use PR6660 §2 without re-proving it. With s = Mᵀy, the preimages of y are in
+bijection with integer chains
+
+    q_t ∈ Q(s),  q_(t−1) ∈ Q(s + 56 q_t),  …,  q_1 ∈ Q(s + 56(q_2+⋯+q_t)),   (1)
+
+taken per mode coordinate, that satisfy the parity condition
+
+    Σ_j (W_j M mod 2) q̄_j = W_t y  (mod 2).                                  (2)
+
+Let Φ(v) = Σ_j (W_j M mod 2) v_j on (F2^8)^t, and let H = ker Φ. Since every
+W_j M kills C modulo 2, H = {v : (v_j + C)_j ∈ D}, where D is the dependency space
+of [#6828](https://github.com/CrocSwap/integer-mult-bounds/pull/6828), and
+|H| = 2^(4t + dim D).
+
+**Definition.** Define ε₀ by
+
+    |fiber(0)| = 2^(dim D − 4t) · 13^(8t) · (1 + ε₀).
+
+The right side without ε₀ is the main Fourier term of §1. Section 1 shows ε₀ ≥ 0.
+
+## Theorem
+
+Let ε* = (1/13) / ((23/12)^8 − 1) = 429981696/1012453046605 ≈ 4.2469·10⁻⁴.
+For every depth t and every frame sequence in G with ε₀ ≤ ε*,
+
+    max_y |fiber(y)| = |fiber(0)|.
+
+**Corollary (depth 27).**
+
+    min_U max_y |fiber(y)| = (1 + 12ρ₂^25 + 3ρ₂^26) · F^27 ≈ 15.7897746 · F^27,
+
+that is, exactly 696 tag bits.
+
+*Proof of the corollary.* For every frame sequence, max_y ≥ |fiber(0)|. #6828
+proves that the minimum depth-27 zero fiber over all frame sequences is the stated
+value, and that its FRAMES27.json frames attain it with dim D = 4. For those
+frames ε₀ = 5.4537·10⁻⁶ < ε*/75. The theorem then gives max_y = |fiber(0)| for
+them, which matches the lower bound. verify.py computes ε₀ exactly from the
+closed form.
+
+## 1. Fourier form
+
+For one coordinate k, let c_k(π) be the number of per-coordinate chains (1)
+whose parity string (q_(t,k) mod 2, …, q_(1,k) mod 2) equals π ∈ F2^t. The
+interval at each stage depends only on that coordinate's own history, so the set
+of chains (1) is a product over the 8 coordinates.
+
+Let v* be any solution of (2). The fiber of y is then the sum over the coset
+v* + H:
+
+    |fiber(y)| = Σ_{v ∈ v*+H} Π_k c_k(v_{·,k}).
+
+Poisson summation gives
+
+    |fiber(y)| = 2^(dim D − 4t) · Σ_{h ∈ H^⊥} (−1)^(h·v*) · Π_k Z_k(h_{·,k}),
+
+where Z_k(b) = Σ_chains Π_j (−1)^(b_j q_j) for b ∈ F2^t. Here H^⊥ ⊆ C^t, by
+self-duality. verify.py checks this identity exactly on six random t = 2
+instances, with tie and non-tie coordinates and random D.
+
+For y = 0 every box is [−6,6] − 14W (PR6327), so Z_k(b) = 13^(zeros of b) with
+positive sign. Hence
+
+    |fiber(0)| = 2^(dim D − 4t) · 13^(8t) · (1 + ε₀),
+    ε₀ = Σ_{h ∈ H^⊥, h ≠ 0} 13^(−wt h) ≥ 0.
+
+## 2. Lemma 1: boxes
+
+For s ≢ 2 (mod 4) there are no ties, and Q(s) = {q : |s+4q| < 26}. Then
+Q(s + 56W) = Q(s) − 14W: the box is 13 consecutive integers, shifted by an even
+amount.
+
+For s = 4x + 2 we have r := q + x ∈ [−6,5]. In addition:
+
+* r = 6 is included iff x ≥ 7 (class U);
+* r = −7 is included iff x ≤ −8 (class L);
+* neither is included for −7 ≤ x ≤ 6 (class N, a 12-element box).
+
+*Proof.* (s + 56q)/52 − q = (s + 4q)/52. A tie occurs at s + 4q = ±26. At
+r = 6 the value is q + ½, which rounds to q iff q + ½ < 0, iff x ≥ 7. At r = −7
+the value is q − ½, which rounds to q iff q ≥ 1, iff x ≤ −8.
+
+Along a chain, s_j = s + 56W gives x_j = x + 14W. With W′ = W + q this gives
+
+    x_(j−1) = −13 x_j + 14 r.
+
+So x_j ≡ x (mod 2) at every stage, and q_j ≡ r_j + x (mod 2). verify.py checks
+the box description for |s| ≤ 3000.
+
+## 3. Lemma 2: per-coordinate signed chains
+
+* **Non-tie coordinates.** By Lemma 1 the boxes do not depend on the history,
+  so |Z(b)| = 13^(zeros b) exactly.
+* **Tie coordinates.** If |x| ≥ 8, then |x′| ≥ 20 and the class alternates
+  between U and L forever (§2 recursion). So for x ∉ [−8,7] the boxes are again
+  fixed 13-intervals up to even shifts, and |Z(b)| = 13^(zeros b).
+* **The sixteen states x ∈ [−8,7].** Z is a product of 10×10 transfer matrices,
+  one family per parity of x:
+
+      Z_x(b) = ± (T_(b_t) ⋯ T_(b_1) 𝟙)_x,
+
+  on {x ∈ [−8,7] of one parity} ∪ {U, L}. The entry T_b[x][y] is
+  Σ (−1)^(b r) over the r leading from x to class y. verify.py checks this
+  against direct chain recursion for all |s| ≤ 150 and depth ≤ 4.
+
+  Normalize the b = 0 steps by 13. Then the U and L entries stay ±1, and each
+  small state has at most one small successor. So the reachable set of
+  normalized vectors is described exactly by an interval for each small state,
+  given the pair (v_U, v_L).
+
+  verify.py exhibits a family of such intervals with endpoints on the 1/12
+  grid. The family contains the starting vector 𝟙 and is exactly closed under
+  T_0/13 and T_1. Hence, for **every** t and every b,
+
+      |Z_x(b)| ≤ c_x · 13^(zeros b),    c_x ≤ 23/12,
+
+  with c_x = 1 for x ∈ {−8, −7, 6, 7}. So c_x > 1 occurs only in class N.
+
+  The bound 23/12 is essentially attained: at depth 27 the supremum for x = −6
+  exceeds 1.9166.
+  It also shows the naive majorant fails: Z_(−22)(1,0,1) = 24 > 13.
+
+## 4. Lemma 3: chain counts
+
+Z_x(0…0) is the total number of chains. Every box has at most 13 elements, and
+class-N boxes have 12. So a coordinate in class N at stage t has
+Z(0) ≤ 12·13^(t−1), and every coordinate has Z(0) ≤ 13^t.
+
+## 5. Proof of the theorem
+
+Fix y. Bound the χ = 0 term of §1 exactly, and every other term by absolute
+values:
+
+    |fiber(y)| ≤ 2^(dim D − 4t) [ Π_k Z_k(0) + Σ_{h≠0} Π_k c_k 13^(zeros h_{·,k}) ]
+               ≤ 2^(dim D − 4t) 13^(8t) [ Π_k Z_k(0)/13^t + (Π_k c_k) ε₀ ].
+
+There are two cases:
+
+* **No coordinate has c_k > 1.** Then every c_k = 1, and the bracket is at
+  most 1 + ε₀. So |fiber(y)| ≤ |fiber(0)|.
+* **Some coordinate has c_k > 1.** By §3 that coordinate is in class N, so by
+  §4 the first product is at most 12/13. Also Π c_k ≤ (23/12)^8. The bracket is
+  therefore at most 12/13 + (23/12)^8 ε₀, which is ≤ 1 + ε₀ exactly when
+  ε₀ ≤ ε*.
+
+∎
+
+For direct sums at t = 26, ε₀ = (16F/13^8)^26 − 1 ≈ 0.0128 > ε*. Those are
+covered by PR6660's box lemma instead. verify.py records this as a control.
+
+## Scope
+
+Exact for the interface of PR6660:
+
+* fixed known frames in G;
+* one relative precision bit before the first call;
+* unbounded exact integers;
+* complete output access.
+
+The corollary uses two premises:
+
+* #6828's exact depth-27 minimum and its realization by FRAMES27.json;
+* PR6660's chain bijection.
+
+Both are open and unmerged, and this package does not replay them. It 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-max-fiber/README.md b/research/refined-recovery-max-fiber/README.md
new file mode 100644
index 0000000000..654c3c7d2c
--- /dev/null
+++ b/research/refined-recovery-max-fiber/README.md
@@ -0,0 +1,99 @@
+# Exact depth-27 optimum for refined recovery: max fiber = zero fiber
+
+Prepared for apoursh with substantial Anthropic Claude assistance. Apache-2.0.
+
+**Scoped proof with exact finite corroboration; no κ.** This addresses open
+question 1 of Nick Petalas's
+[PR6660](https://github.com/CrocSwap/integer-mult-bounds/pull/6660)
+(`research/refined-recovery-longer-chains`, head `b6de532e`), which asks for the
+exact optimum at t ≥ 27. It also answers open question 1 of
+[#6828](https://github.com/CrocSwap/integer-mult-bounds/pull/6828).
+
+**Theorem.** Suppose a frame sequence's zero fiber is within a relative 4.2·10⁻⁴
+of its Fourier main term 2^(dim D−4t)·13^(8t), that is, ε₀ ≤ ε*. Then no output
+has a larger fiber than 0:
+
+    max_y |fiber(y)| = |fiber(0)|.
+
+**Corollary.** At depth 27,
+
+    min_U max_y |fiber(y)| = (1 + 12ρ₂^25 + 3ρ₂^26) · F^27 ≈ 15.7897746 · F^27,
+
+that is, **696 tag bits**, exactly. This is the first exact value beyond PR6660's
+range t ≤ 26. The lower bound is #6828's exact minimum zero fiber. The upper bound
+comes from #6828's FRAMES27 frames, whose ε₀ = 5.45·10⁻⁶ is 78 times below the
+threshold.
+
+**Why it is not just the box lemma.** For y ≠ 0 the interval boxes of a chain can
+depend on its history, and the coupled stage cosets block PR6660's stage-by-stage
+count. The proof uses three facts:
+
+1. **Factorization.** The fiber expands over characters h ∈ H^⊥, and each term is
+   a product of eight one-coordinate signed chain sums Z_k. The interval at each
+   stage depends only on that coordinate's history.
+2. **Ties are the only adaptivity.** Without rounding ties, each box is a fixed
+   13-interval shifted by an even amount, so |Z_k| equals its value at y = 0.
+   With ties, s = 4x+2, and the state follows x ↦ −13x+14r. Only sixteen states
+   x ∈ [−8,7] can still meet a 12-element box.
+3. **A bound with a matching penalty.** A transfer-matrix analysis with an
+   exactly closed interval family on the 1/12 grid gives |Z_k| ≤ (23/12)·13^(zeros)
+   at every depth. The constant 23/12 is attained in the limit, and the naive bound
+   with constant 1 is false. Every coordinate whose ratio exceeds 1 starts with a
+   12-element box, which costs the main term a factor 12/13. That loss outweighs
+   (23/12)^8·ε₀ whenever ε₀ ≤ ε*.
+
+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-max-fiber/verify.py
+python3.12 -I -O -W error -B research/refined-recovery-max-fiber/verify.py
+python3.12 -B scripts/research_package.py --package research/refined-recovery-max-fiber
+```
+
+Each run prints `PASS_REFINED_RECOVERY_MAX_FIBER` in under a minute. It checks
+the following:
+
+* C and the coset sum ρ₂, derived from the pinned matrix;
+* the box lemma for |s| ≤ 3000;
+* the transfer matrices against direct chain recursion (|s| ≤ 150, depth ≤ 4);
+* the closed interval family (exact rationals), the caps per state, and the
+  near-attainment at depth 27;
+* the Poisson identity on six random t = 2 instances, with random D and tie
+  coordinates;
+* ε* and ε₀(t = 27) exactly, and the 696-bit count;
+* two controls: the failing naive majorant, and t = 26 direct sums lying outside
+  the threshold.
+
+## Limitations
+
+The corollary uses #6828's exact zero-fiber minimum and its FRAMES27.json
+realization. Both are open and unmerged, and this package does not replay them.
+Like #6828, it also cites PR6660's chain bijection (§2) and PR6327's box facts.
+Neither fork commit is reachable here, so SOURCES.json does not pin them.
+
+The theorem needs ε₀ ≤ ε*. It does not cover t ≤ 26 direct sums (ε₀ ≈ 0.0128),
+which PR6660 handles by its box lemma. Nor does it cover frames with heavy
+overlap. The exact optimum at t ≥ 28 remains open: #6828's floor is not known to
+be attained there. 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. **Depth 28 and beyond.** Find frames attaining (or approaching) #6828's floor at
+   t ≥ 28. If the attaining frames satisfy ε₀ ≤ ε*, this theorem gives the exact
+   optimum there too.
+2. **Sharper threshold.** Use the per-state caps (13/12 to 23/12) together with
+   the actual H^⊥ weight distribution to widen ε*. Then frames with heavier
+   overlap would be covered as well.
+
+## Credit
+
+Nick Petalas's PR6660 supplies the chain bijection, the depth law and the open
+question. CubeJerry's PR6327 supplies the chain model, F and the box facts. zxv's
+#5444 supplies M. #6828 supplies the exact depth-27 zero-fiber minimum and the
+FRAMES27 frames. Poisson summation and transfer matrices are classical.
diff --git a/research/refined-recovery-max-fiber/RESULT.json b/research/refined-recovery-max-fiber/RESULT.json
new file mode 100644
index 0000000000..322e2538c0
--- /dev/null
+++ b/research/refined-recovery-max-fiber/RESULT.json
@@ -0,0 +1,28 @@
+{
+ "per_coordinate_ratio_bound": "23/12",
+ "ratio_caps_by_tie_state": {
+  "-8": "1",
+  "-7": "1",
+  "-6": "23/12",
+  "-5": "7/4",
+  "-4": "19/12",
+  "-3": "17/12",
+  "-2": "5/4",
+  "-1": "13/12",
+  "0": "13/12",
+  "1": "5/4",
+  "2": "17/12",
+  "3": "19/12",
+  "4": "7/4",
+  "5": "23/12",
+  "6": "1",
+  "7": "1"
+ },
+ "sup_ratio_depth27_state_minus6": 1.9166666665802254,
+ "threshold_eps_star": "429981696/1012453046605",
+ "threshold_eps_star_float": 0.0004246929745945579,
+ "t27_value_over_F27": 15.789774623144325,
+ "t27_eps0_float": 5.453687310396066e-06,
+ "t27_exact_optimum_tag_bits": 696,
+ "t26_direct_sum_eps0_float": 0.012823080646547256
+}
diff --git a/research/refined-recovery-max-fiber/SOURCES.json b/research/refined-recovery-max-fiber/SOURCES.json
new file mode 100644
index 0000000000..ae5689199c
--- /dev/null
+++ b/research/refined-recovery-max-fiber/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-max-fiber/TASK.json b/research/refined-recovery-max-fiber/TASK.json
new file mode 100644
index 0000000000..10834d6686
--- /dev/null
+++ b/research/refined-recovery-max-fiber/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": "Maximum fiber of PR6660 refined chains: for every depth and every frame sequence in G whose zero fiber is within eps*=(1/13)/((23/12)^8-1)~4.25e-4 of its Fourier main term 2^(dim D-4t) 13^(8t), every output y has |fiber(y)|<=|fiber(0)|. With #6828's exact depth-27 zero-fiber minimum and FRAMES27 (eps0=5.45e-6), the exact depth-27 optimum is min_U max_y |fiber(y)| = (1+12rho2^25+3rho2^26)F^27, 696 tag bits.",
+  "scope_change_reason": "Answers PR6660 open question 1 at t=27 and #6828 open question 1 (max fiber of FRAMES27). Like its predecessors this is 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 max-fiber = zero-fiber theorem under the eps0 threshold and the exact depth-27 optimum; leave t>=28 attainment and a sharper threshold open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md; verify.py (exact rational arithmetic, normal and optimized Python) checks every lemma's finite certificate and 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 #6828's zero-fiber floor attained (or approached) by frames at t>=28?",
+      "why_it_matters": "If the attaining frames have eps0<=eps*, this theorem makes the floor the exact optimum there.",
+      "first_step": "Extend build_frames.py of #6828 to t=28 with an 8-dimensional E-valued dependency and compute eps0.",
+      "blocked_by": "Realizability of larger E-valued dependency spaces within the 104-dimensional cap."
+    },
+    {
+      "question": "Can the threshold eps* be widened using per-state ratio caps and the H^perp weight distribution?",
+      "why_it_matters": "It would cover frame sequences with heavier overlap.",
+      "first_step": "Replace (23/12)^8 by the product of per-state caps and bound the h!=0 sum by weight classes.",
+      "blocked_by": "Nothing; routine refinement."
+    }
+  ]
+}
diff --git a/research/refined-recovery-max-fiber/VERIFY.json b/research/refined-recovery-max-fiber/VERIFY.json
new file mode 100644
index 0000000000..bf3566514f
--- /dev/null
+++ b/research/refined-recovery-max-fiber/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": 300,
+      "checks": "Fixture hash; C=[8,4,4] self-dual from M and coset sum rho2; rounding-box lemma on |s|<=3000; tie transfer matrices against direct chain recursion (|s|<=150, depth<=4); exactly closed 1/12-grid interval family giving |Z|<=(23/12) 13^zeros at every depth, caps per state, near-attainment at depth 27; box-size row sums; Poisson identity on six random t=2 instances; eps* and eps0(t=27) exact, 696 bits; RESULT.json recomputation; controls."
+    },
+    {
+      "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/verify.py"],
+      "timeout_seconds": 300,
+      "checks": "The same explicit checks under optimized Python."
+    }
+  ]
+}
diff --git a/research/refined-recovery-max-fiber/verify.py b/research/refined-recovery-max-fiber/verify.py
new file mode 100644
index 0000000000..17b7e7f581
--- /dev/null
+++ b/research/refined-recovery-max-fiber/verify.py
@@ -0,0 +1,336 @@
+"""Exact checks for the maximum fiber of refined recovery chains (stdlib only).
+
+Prints PASS_REFINED_RECOVERY_MAX_FIBER on success.
+"""
+import hashlib
+import itertools
+import json
+import math
+import pathlib
+import random
+from fractions import Fraction
+from functools import lru_cache
+
+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
+SMALL = range(-8, 8)  # tie states that can still meet a 12-element box
+C_MAX = Fraction(23, 12)
+
+
+def fail(msg):
+    raise SystemExit("FAIL: " + msg)
+
+
+def check(cond, msg):
+    if not cond:
+        fail(msg)
+
+
+def wt(u):
+    return bin(u).count("1")
+
+
+# ---------------------------------------------------------------- source code C
+
+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 coset_sums(code):
+    w = lambda u: 7 ** (8 - wt(u)) * 6 ** wt(u)
+    S = {u: sum(w(u ^ c) for c in code) for u in range(256)}
+    check(S[0] == F, "S(C) = F")
+    check({S[u] for u in range(256) if wt(u) % 2} == {50983170}, "odd coset sum")
+    check({S[u] for u in range(256) if wt(u) % 2 == 0 and u not in code} == {50979600},
+          "even coset sum")
+    return Fraction(50979600, F)
+
+
+# ---------------------------------------------------------------- rounding boxes
+
+def rnd(x):
+    """Nearest integer, half ties away from zero."""
+    f = math.floor(x)
+    d = x - f
+    if d != Fraction(1, 2):
+        return f + (d > Fraction(1, 2))
+    return f + 1 if x > 0 else f
+
+
+@lru_cache(maxsize=None)
+def box(s):
+    """Q(s) = {q : R((s + 56 q)/52) = q}, as a sorted tuple."""
+    c = -s // 4
+    return tuple(q for q in range(c - 10, c + 11) if rnd(Fraction(s + 56 * q, 52)) == q)
+
+
+def tie_range(x):
+    """Box Q(4x+2) shifted by x (so r = q + x), by the class of x."""
+    if -7 <= x <= 6:
+        return range(-6, 6)
+    return range(-6, 7) if x >= 7 else range(-7, 6)
+
+
+def check_boxes():
+    """Lemma 1 on a window; PROOF.md section 2 proves it for every s."""
+    for s in range(-3000, 3001):
+        q = box(s)
+        if s % 4 != 2:
+            check(q == tuple(v for v in range(-s // 4 - 10, -s // 4 + 11) if abs(s + 4 * v) < 26),
+                  "non-tie box is {q : |s+4q| < 26}")
+            check(len(q) == 13, "non-tie box has 13 elements")
+            for w in (-3, -1, 1, 2, 5):
+                check(box(s + 56 * w) == tuple(v - 14 * w for v in q), "non-tie box shifts by 14w")
+        else:
+            x = (s - 2) // 4
+            check(tuple(v + x for v in q) == tuple(tie_range(x)), "tie box by class of x")
+
+
+# ---------------------------------------------------------------- per-coordinate chains
+
+@lru_cache(maxsize=None)
+def chains_direct(s, bits):
+    """Z_s(b) = sum over one coordinate's chains of prod_j (-1)^(b_j q_j), b_1 = stage t."""
+    if not bits:
+        return 1
+    b = bits[0]
+    return sum((-1 if b and q % 2 else 1) * chains_direct(s + 56 * q, bits[1:]) for q in box(s))
+
+
+def transfer(par):
+    """Transfer matrices on {x in SMALL of parity par} + {U, L}; signs (-1)^(b r)."""
+    states = [x for x in SMALL if x % 2 == par] + ["U", "L"]
+    idx = {s: i for i, s in enumerate(states)}
+    rep = {"U": 100 + par, "L": -100 + par}  # any |x| >= 8 outside SMALL behaves alike
+    cls = lambda y: y if y in SMALL else ("U" if y > 0 else "L")
+    n = len(states)
+    T = {b: [[0] * n for _ in range(n)] for b in (0, 1)}
+    for s in states:
+        x = rep.get(s, s)
+        for r in tie_range(x):
+            y = -13 * x + 14 * r
+            if s in ("U", "L"):
+                check(abs(y) >= 20 and (y > 0) == (s == "L"), "big states alternate U <-> L")
+            for b in (0, 1):
+                T[b][idx[s]][idx[cls(y)]] += -1 if b and r % 2 else 1
+    for x in range(-60, 61):  # closure: outside SMALL never re-enters SMALL
+        if x not in SMALL:
+            check(all(-13 * x + 14 * r not in SMALL for r in tie_range(x)), "SMALL is the reach set")
+    return states, idx, T
+
+
+def apply(T, b, v):
+    nm = 13 if b == 0 else 1
+    return [Fraction(sum(a * x for a, x in zip(row, v)), nm) for row in T[b]]
+
+
+def predicted(s, bits, cache):
+    """Z_s(b) from the transfer matrices (tie s) or the product formula (others)."""
+    zeros = bits.count(0)
+    if s % 4 != 2:
+        sign = 1
+        for j, b in enumerate(bits):  # majority parity of every 13-box is that of Q(s)'s lowest point
+            if b and box(s)[0] % 2:
+                sign = -sign
+        return sign * 13 ** zeros
+    x = (s - 2) // 4
+    par = x % 2
+    states, idx, T = cache[par]
+    v = [Fraction(1)] * len(states)
+    for b in reversed(bits):
+        v = apply(T, b, v)
+    key = x if x in SMALL else ("U" if x > 0 else "L")
+    return (-1) ** (x * sum(bits) % 2) * v[idx[key]] * 13 ** zeros
+
+
+def check_transfer(cache):
+    for L in range(1, 5):
+        for s in range(-150, 151):
+            for bits in itertools.product((0, 1), repeat=L):
+                check(chains_direct(s, bits) == predicted(s, bits, cache), "transfer = direct chains")
+
+
+def interval_step(D, T, n):
+    nS = n - 2
+    out = {}
+    for (u, l), iv in D.items():
+        for b in (0, 1):
+            nm = 13 if b == 0 else 1
+            key = (Fraction(T[b][n - 2][n - 2] * u + T[b][n - 2][n - 1] * l, nm),
+                   Fraction(T[b][n - 1][n - 2] * u + T[b][n - 1][n - 1] * l, nm))
+            check(abs(key[0]) == 1 and abs(key[1]) == 1, "big states keep |value| = 1")
+            new = []
+            for i in range(nS):
+                check(sum(1 for j in range(nS) if T[b][i][j]) <= 1, "one small successor")
+                lo = hi = Fraction(T[b][i][n - 2] * u + T[b][i][n - 1] * l)
+                for j in range(nS):
+                    a = T[b][i][j]
+                    lo, hi = (lo + a * iv[j][0], hi + a * iv[j][1]) if a > 0 else \
+                             (lo + a * iv[j][1], hi + a * iv[j][0]) if a < 0 else (lo, hi)
+                new.append((lo / nm, hi / nm))
+            out[key] = [(min(p[0], q[0]), max(p[1], q[1])) for p, q in zip(out[key], new)] \
+                if key in out else new
+    return out
+
+
+def ratio_bounds(cache):
+    """Lemma 2: an exactly closed interval family on the 1/12 grid."""
+    caps = {}
+    for par in (0, 1):
+        states, idx, T = cache[par]
+        n = len(states)
+        start = {(Fraction(1), Fraction(1)): [(Fraction(1), Fraction(1))] * (n - 2)}
+        D = start
+        for _ in range(40):
+            D = interval_step(D, T, n)
+        grid = {k: [(Fraction(math.floor(lo * 12), 12), Fraction(math.ceil(hi * 12), 12))
+                    for lo, hi in iv] for k, iv in D.items()}
+        for k, iv in start.items():
+            check(all(g[0] <= a[0] and a[1] <= g[1] for g, a in zip(grid[k], iv)), "start inside")
+        img = interval_step(grid, T, n)
+        check(set(img) <= set(grid), "keys closed")
+        check(all(grid[k][i][0] <= img[k][i][0] and img[k][i][1] <= grid[k][i][1]
+                  for k in img for i in range(n - 2)), "interval family closed under T_0/13, T_1")
+        for i, s in enumerate(states[:-2]):
+            caps[s] = max(max(abs(a), abs(b)) for iv in grid.values() for a, b in [iv[i]])
+    check(max(caps.values()) == C_MAX, "sup ratio bound 23/12")
+    one = [x for x, c in caps.items() if c <= 1]
+    check(sorted(one) == [-8, -7, 6, 7], "ratio <= 1 exactly at the boundary states")
+    check(all(-7 <= x <= 6 for x, c in caps.items() if c > 1), "ratio > 1 only in the 12-box class")
+    # tightness: depth 27 already exceeds 1.9166
+    par, x = 0, -6
+    states, idx, T = cache[par]
+    D = {(Fraction(1), Fraction(1)): [(Fraction(1), Fraction(1))] * (len(states) - 2)}
+    for _ in range(27):
+        D = interval_step(D, T, len(states))
+    sup27 = max(max(abs(a), abs(b)) for iv in D.values() for a, b in [iv[idx[x]]])
+    check(Fraction(19166, 10000) < sup27 <= C_MAX, "bound is essentially attained at depth 27")
+    return caps, sup27
+
+
+def check_counts(cache):
+    """Lemma 3: row sums of T_0 are <= 13, and = 12 on the 12-box class."""
+    for par in (0, 1):
+        states, idx, T = cache[par]
+        for i, s in enumerate(states):
+            tot = sum(T[0][i])
+            x = s if s in SMALL else None
+            check(tot == (12 if x is not None and -7 <= x <= 6 else 13), "box sizes")
+
+
+# ---------------------------------------------------------------- Poisson identity on a toy
+
+def toy_poisson(code):
+    """t = 2: sum over a coset of H of prod_k c_k equals the character formula."""
+    rng = random.Random(6660)
+    rep = lambda u: min(u ^ c for c in code)
+    reps = sorted({rep(u) for u in range(256)})
+    for trial in range(6):
+        t = 2
+        ss = [rng.choice([0, -22, -18, 30, 7, 13, 2, -26]) for _ in range(MODES)]
+        # per-coordinate parity-string counts
+        cnt = []
+        for s in ss:
+            c = [0] * 4
+            for q2 in box(s):
+                for q1 in box(s + 56 * q2):
+                    c[(q2 & 1) | (q1 & 1) << 1] += 1
+            cnt.append(c)
+        gens = [tuple(rng.choice(reps) for _ in range(t)) for _ in range(rng.randint(1, 3))]
+        Dset = {tuple([0] * t)}
+        for g in gens:
+            Dset |= {tuple(rep(a ^ b) for a, b in zip(d, g)) for d in Dset}
+        vstar = tuple(rng.randrange(256) for _ in range(t))
+        lhs = 0
+        for v in itertools.product(range(256), repeat=t):
+            if tuple(rep(a ^ b) for a, b in zip(v, vstar)) in Dset:
+                p = 1
+                for k in range(MODES):
+                    p *= cnt[k][(v[0] >> k & 1) | (v[1] >> k & 1) << 1]
+                lhs += p
+        Hperp = [h for h in itertools.product(code, repeat=t)
+                 if all(sum(wt(hj & dj) for hj, dj in zip(h, d)) % 2 == 0 for d in Dset)]
+        rhs = Fraction(0)
+        for h in Hperp:
+            term = (-1) ** (sum(wt(hj & vj) for hj, vj in zip(h, vstar)) % 2)
+            for k in range(MODES):
+                bits = tuple(h[j] >> k & 1 for j in range(t))  # bits[0] = stage t = v[0]
+                term *= sum(cnt[k][a] * (-1) ** sum(bits[j] * (a >> j & 1) for j in range(t))
+                            for a in range(4))
+            rhs += term
+        dimD = len(Dset).bit_length() - 1
+        rhs *= Fraction(2 ** dimD, 2 ** (4 * t))
+        check(lhs == rhs, "Poisson form of the fiber")
+        check(len(Hperp) == 2 ** (4 * t - dimD), "|H^perp| = 2^(4t - dim D)")
+
+
+# ---------------------------------------------------------------- main
+
+def main():
+    rows = load_rows()
+    code = code_from_rows(rows)
+    rho2 = coset_sums(code)
+    check_boxes()
+    cache = {par: transfer(par) for par in (0, 1)}
+    check_transfer(cache)
+    check_counts(cache)
+    caps, sup27 = ratio_bounds(cache)
+    toy_poisson(code)
+
+    # control: the naive per-coordinate Fourier majorant fails at a tie
+    z = chains_direct(-22, (1, 0, 1))
+    check(abs(z) == 24 and 24 > 13, "control: |Z| exceeds 13^zeros at s = -22")
+
+    # Theorem threshold
+    eps_star = Fraction(1, 13) / (C_MAX ** 8 - 1)
+    # Depth-27 corollary
+    t, dimD = 27, 4
+    V = (1 + 12 * rho2 ** 25 + 3 * rho2 ** 26) * F ** t
+    eps0 = V * 2 ** (4 * t - dimD) / 13 ** (8 * t) - 1
+    check(0 < eps0 < eps_star, "FRAMES27 zero fiber is within the threshold")
+    check(eps0 * 75 < eps_star, "with a factor 75 to spare")
+    bits = math.ceil(math.log2(V))
+    check(2 ** (bits - 1) < V <= 2 ** bits and bits == 696, "696 tag bits")
+    # control: a t = 26 direct sum is not covered (PR6660 handles it separately)
+    eps26 = Fraction(F ** 26 * 2 ** (4 * 26), 13 ** (8 * 26)) - 1
+    check(eps26 > eps_star, "control: direct sums at t=26 lie outside the threshold")
+
+    result = {
+        "per_coordinate_ratio_bound": str(C_MAX),
+        "ratio_caps_by_tie_state": {str(k): str(v) for k, v in sorted(caps.items())},
+        "sup_ratio_depth27_state_minus6": float(sup27),
+        "threshold_eps_star": str(eps_star),
+        "threshold_eps_star_float": float(eps_star),
+        "t27_value_over_F27": float(V / F ** t),
+        "t27_eps0_float": float(eps0),
+        "t27_exact_optimum_tag_bits": bits,
+        "t26_direct_sum_eps0_float": float(eps26),
+    }
+    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("eps* = %.6e, eps0(t=27) = %.6e, sup ratio = 23/12, bits = %d" % (eps_star, eps0, bits))
+    print("PASS_REFINED_RECOVERY_MAX_FIBER")
+
+
+if __name__ == "__main__":
+    main()