diff --git a/research/finite-protocol/PROTOCOL.md b/research/finite-protocol/PROTOCOL.md
new file mode 100644
index 000000000..e29b68919
--- /dev/null
+++ b/research/finite-protocol/PROTOCOL.md
@@ -0,0 +1,59 @@
+# Finite channel protocol — prospective successor to the #807 design repair
+
+Owner authorization: ChatGPT, 2026-10-12T04:24:46Z, "Ok let's proceed as suggested";
+parallel work explicitly requested at 2026-10-12T05:10:00Z.
+Certified main base: f2415108601a9c36bb985b3374c56f0eb34c2962.
+Measured design parent: #807, 13ad14a1ba2973245354aea7790c021d946b1ff0.
+The existing #807 one-run preregistration and one-line diff remain the completed historical record.
+
+## Scope and decision rules, before the first new computation and CI
+
+Construct the stopped finite protocol with InstAvail's existing readout, op, bind, coarse and
+discard rules, including the maximally mixed ancilla and its internal pure reset. Prove every
+finite depth is available from primitive readout/reset/circuit/correction inputs. Derive the
+closed form from the constructed branches. No AvailableChannelApproximation witness is assumed.
+
+Every finite computation uses Gaussian rationals. Controls cover the actual uniformly attached
+ancilla, each reset branch, normalization, the gate circuit, the corrected outcome maps and the
+stopped loop. A failed control suppresses the computational verdict. Countercontrols remove the
+reset, remove the correction, and continue after success; each must disagree with the intended
+map on a named matrix unit. Finite computations establish only their checked cases.
+
+The Lean module counts as built design evidence only after Build succeeds and all fourteen
+declared axiom reports contain only propext, Classical.choice, Quot.sound. No sorryAx is allowed.
+The CI budget is at most three sequential fresh-head design runs. Retain each tested head,
+its errors and its actual result before correcting proofs and starting another run.
+The new PR targets the measured disposable #807 repair branch; it is neither a main landing
+nor a native F/E attestation. Its release gate is expected to stop at the manuscript census
+for thirteen unadopted design modules. Establish the actual scope from the logs.
+
+## Invariant checkpoints
+
+| Invariant | Checkpoint |
+|---|---|
+| The pure seed comes from uniformly attached ancilla | reset_uniformAttach and exact physical-reset calculation |
+| Availability is constructed, not supplied as an all-k witness | instAvail_attempt, instAvail_stopped, finite_protocol_available |
+| Failure continues and success stops | bind/coarse definition and stop countercontrol |
+| Exact O14 branch and all-k formulas | attempt_balanced_branch and balanced_stopped_formula |
+| Explicit finite primitive resources | hCircuit, hReset, hCorrect and architecture projector field |
+| Spectator extension names actual prerequisites | finite_protocol_spectator, ContextStable and LabelInvariant |
+| All named Lean statements are genuine proofs | actual Build plus fourteen standard axiom reports |
+| #807 and shared maxCone modules unchanged | prospective path allowlist and remote compare |
+| Pair-cone validity is not inferred from matrix positivity | source audit I4.38/I4.66 and result review |
+| Closedness enters only any later limit passage | no limit or availability closure theorem in this module |
+
+## Premise source audit
+
+I4.38 validity_of_implementationLocality and I4.66 CompositeOperationalValidity refer to
+positive semidefinite matrices at the matrix carrier. Their definitions do not assert
+preservation of an arbitrary identified pair cone. #807's channelTransfer_of_identified_stateSpace
+requires its pair-validity hypothesis separately; at the kernel's PSD space identification
+with that space is K = Q3. Applying that fact to an arbitrary K would assume the reconstruction
+target. Context stability I4.29 and label invariance I4.30 extend availability to a spectator;
+they do not identify the state cone or establish preservation of it.
+
+The primitive circuit is the O14 balanced Hadamard/Toffoli/quarter-phase circuit on the token
+and two ancilla qubits. Its rational table and exact isometry are checked. Class membership of
+that circuit, reset permutations and correction remains explicit. A theorem that derives all
+those memberships for MixR {pi/4}, and the channel convergence and arbitrary-cone transfer
+theorems, are further obligations; they are not claimed by this constructor package.
diff --git a/research/finite-protocol/RESULTS.md b/research/finite-protocol/RESULTS.md
new file mode 100644
index 000000000..898e6e69a
--- /dev/null
+++ b/research/finite-protocol/RESULTS.md
@@ -0,0 +1,74 @@
+# Finite protocol design results
+
+This is the successor to #807's completed one-line repair, not a change to that record.
+Its draft PR is #810 and its prospective rules are in PROTOCOL.md.
+
+## Exact protocol controls
+
+Gaussian-rational computation: ten of ten required groups pass, including the actual
+maximally mixed attachment, its readout/conditional-permutation reset, the circuit
+word/table identity, corrected branches, and 36 stopped matrix-unit cases at depths 0–8.
+Removing reset, removing failure correction or continuing after success each fails the
+intended channel identity on the 0,1 matrix unit. Two saved runs return exit zero,
+empty stderr and byte-identical stdout, SHA256
+f33e3c97bd1baa7f4b583f798cf0ecdec185860d37f69523f31128e4131d35e1.
+This is finite exact evidence [X], not a Lean proof of the general depth statement.
+
+## Design run 1
+
+Head: 5e57fb740496e6e851e1fcc0da13ef392016a9cf.
+Run: 38207454267, pull_request, attempt 1.
+Mathlib bridge job: 114673991060; Build failed, 05:20:07Z–05:23:01Z.
+Release gate skipped, so the forecast thirteen-module census failure was not tested.
+The initial head supplies no built design result.
+
+Reported causes: Matrix.diagonal_conjTranspose had been written in the wrong word order;
+tensorOf_apply had a wrong namespace; the closed form retained an if-True term; reset and
+the finite gate table needed further scalar/star-of-numeral simplification; the branch
+calculation exceeded the default 200000 heartbeats; the three-failure sum needed its
+linear-map scalar sum normalized before entrywise simplification. The constructor proofs
+elaborated, but this failed Build certifies no theorem. Failed source and logs remain at
+the immutable first head and job.
+
+## Prospective run-2 correction
+
+Proof corrections only: use the actual library lemma names, normalize numerals under
+conjugation, simplify the scalar sums and the pure-reset symmetry, and give the finite
+branch calculation 2000000 heartbeats. Statements, primitive availability inputs,
+protocol constructors, exact checker and its decision rules are unchanged.
+Require the original fourteen standard axiom reports and a successful Build. Only start
+this fresh-head run after the first complete workflow finishes. The budget remains three
+sequential design runs; none is a native F/E attestation.
+
+## Remaining sources
+
+Primitive memberships of the finite balanced circuit, reset permutations and corrections
+remain explicit. Their derivation in MixR {pi/4} is not claimed here. The constructed
+finite availability is distinct from an available limiting drive and from preservation
+of an arbitrary identified pair cone. A later channel-limit use on such a cone requires
+that cone's channel-transfer premise and closedness. The exact full-flow maxCone theorem
+does not need closedness; this approximation route has that separate obligation.
+
+## Design run 2
+
+Head: 6a2e9f0e2e3a5842491767a4ff2ff1b3652335bc.
+Run: 38208235321, pull_request, attempt 1.
+Mathlib bridge job: 114676391242; Build failed, 05:30:56Z–05:35:47Z.
+Release gate skipped. Eleven targets elaborate on standard axioms; the branch formula
+lemma and its two dependents remain unfinished. A failed Build establishes no built
+design result, including for the eleven elaborated targets.
+
+Two causes remain: the documentation comment was attached to a scoped set_option command
+instead of its theorem, and simp unfolded uniformAttach before applying the proved pure
+reset equation. The latter left resetChannel applied to the tensor table as an opaque
+variable in the matrix calculation. These are proof-script defects, not a failing physical
+control or a new mathematical premise.
+
+## Prospective run-3 correction
+
+Move the theorem documentation inside the scoped option, and use an explicit entrywise
+change followed by reset_uniformAttach_eq_pure before any matrix expansion. All fourteen
+statement and premise headers are unchanged from run 1. Constructors and the exact checker
+remain unchanged. Start the final budgeted design run only after run 2 fully completes.
+Require a successful Build and all fourteen standard axiom reports; make no stronger
+classification if either fails. No further run is authorized by this prospective budget.
diff --git a/research/finite-protocol/check.run1.out b/research/finite-protocol/check.run1.out
new file mode 100644
index 000000000..0942ada96
--- /dev/null
+++ b/research/finite-protocol/check.run1.out
@@ -0,0 +1,11 @@
+CIRCUIT-TABLE: PASS
+UNITARY: PASS
+RESET-ISOMETRIES: PASS
+PROJECTOR-RESOLUTION: PASS
+ACTUAL-UNIFORM-RESET: PASS
+ACTUAL-CORRECTED-BRANCHES: PASS
+STOPPED-DEPTHS-0-8: PASS
+CONTROL-REMOVE-RESET: PASS
+CONTROL-REMOVE-CORRECTION: PASS
+CONTROL-CONTINUE-SUCCESS: PASS
+FINITE-PROTOCOL: PASS; 10 groups; 36 stopped matrix-unit cases
diff --git a/research/finite-protocol/finite_protocol_check.py b/research/finite-protocol/finite_protocol_check.py
new file mode 100644
index 000000000..e86c6b927
--- /dev/null
+++ b/research/finite-protocol/finite_protocol_check.py
@@ -0,0 +1,167 @@
+#!/usr/bin/env python3
+"""Prospective controls: PROTOCOL.md. Exact physical reset, attempt and stopped-loop maps.
+
+Arithmetic is in Q(i). The actual circuit and uniformly attached ancilla are evaluated
+before branch maps and stopped-loop maps are compared with their stated formulas.
+"""
+from fractions import Fraction as R
+from dataclasses import dataclass
+from itertools import product
+import sys
+
+
+@dataclass(frozen=True)
+class C:
+    r: R = R(0)
+    i: R = R(0)
+
+    @classmethod
+    def cast(cls, x):
+        return x if isinstance(x, cls) else cls(R(x))
+
+    def __add__(self, other):
+        b = C.cast(other)
+        return C(self.r + b.r, self.i + b.i)
+
+    __radd__ = __add__
+
+    def __neg__(self):
+        return C(-self.r, -self.i)
+
+    def __sub__(self, other):
+        return self + -C.cast(other)
+
+    def __rsub__(self, other):
+        return C.cast(other) + -self
+
+    def __mul__(self, other):
+        b = C.cast(other)
+        return C(self.r*b.r-self.i*b.i, self.r*b.i+self.i*b.r)
+
+    __rmul__ = __mul__
+
+    def conj(self):
+        return C(self.r, -self.i)
+
+
+I = C(R(0), R(1))
+
+
+def tab(n, f):
+    return tuple(tuple(C.cast(f(a,b)) for b in range(n)) for a in range(n))
+
+
+def ident(n):
+    return tab(n, lambda a,b: int(a == b))
+
+
+def unit(n, a, b):
+    return tab(n, lambda x,y: int((x,y) == (a,b)))
+
+
+def scale(c, a):
+    return tuple(tuple(c*x for x in row) for row in a)
+
+
+def plus(a, b):
+    return tuple(tuple(x+y for x,y in zip(ra,rb)) for ra,rb in zip(a,b))
+
+
+def mm(a,b):
+    return tuple(tuple(sum((a[x][k]*b[k][y] for k in range(len(b))), C())
+                       for y in range(len(b[0]))) for x in range(len(a)))
+
+
+def dagger(a):
+    return tuple(tuple(a[y][x].conj() for y in range(len(a))) for x in range(len(a[0])))
+
+
+def apply(u,x):
+    return mm(mm(u,x),dagger(u))
+
+
+def tensor(a,b):
+    return tuple(tuple(a[s][t]*b[f][e] for t in range(len(a)) for e in range(len(b)))
+                 for s in range(len(a)) for f in range(len(b)))
+
+
+def total(xs,n):
+    out = scale(0,ident(n))
+    for x in xs:
+        out = plus(out,x)
+    return out
+
+
+def trace_anc(x):
+    return tab(2,lambda s,t: sum((x[4*s+f][4*t+f] for f in range(4)),C()))
+
+
+P = [tab(8,lambda x,y: int(x == y and x%4 == j)) for j in range(4)]
+reset = [tab(8,lambda x,y: int(x == 4*(y//4)+(0 if y%4 == j else j if y%4 == 0 else y%4)))
+         for j in range(4)]
+Z = tab(2,lambda s,t: (1 if s == 0 else -1) if s == t else 0)
+correct = [ident(8) if j == 0 else tensor(Z,ident(4)) for j in range(4)]
+D = tab(2,lambda s,t: (1 if s == 0 else C(R(3,5),R(4,5))) if s == t else 0)
+
+# Construct U from the permitted finite circuit, not from its desired channel formula.
+hraw = tab(2,lambda s,t: -1 if s == t == 1 else 1)
+hh = scale(R(1,2),tensor(ident(2),tensor(hraw,hraw)))
+tof = tab(8,lambda x,y: int(x == (y ^ 4 if y%4 == 3 else y)))
+phase = tab(8,lambda x,y: (1 if x//4 == 0 else I) if x == y else 0)
+U = mm(mm(mm(mm(hh,tof),phase),tof),hh)
+v = (1,-1,-1,1)
+Utable = tab(8,lambda x,y: 0 if x//4 != y//4 else
+    ((1 if x//4 == 0 else I) if x%4 == y%4 else 0) +
+    R(1,4)*(I-1 if x//4 == 0 else 1-I)*v[x%4]*v[y%4])
+
+
+def reset_state(x):
+    attached = tensor(x,scale(R(1,4),ident(4)))
+    return total((apply(reset[j],apply(P[j],attached)) for j in range(4)),8)
+
+
+def branches(x, do_reset=True, do_correct=True):
+    seed = reset_state(x) if do_reset else tensor(x,scale(R(1,4),ident(4)))
+    ran = apply(U,seed)
+    return tuple(trace_anc(apply(correct[j] if do_correct else ident(8),apply(P[j],ran)))
+                 for j in range(4))
+
+
+def stopped(k,x):
+    if k == 0:
+        return x
+    bs = branches(x)
+    return plus(bs[0],stopped(k-1,total(bs[1:],2)))
+
+
+def formula(k,x):
+    q = R(3,8)**k
+    return plus(scale(1-q,apply(D,x)),scale(q,x))
+
+
+checks = []
+
+
+def check(name, passed):
+    checks.append(bool(passed))
+    print(name + (': PASS' if passed else ': FAIL'))
+
+
+units = tuple(unit(2,a,b) for a,b in product(range(2),repeat=2))
+check('CIRCUIT-TABLE',U == Utable)
+check('UNITARY',mm(dagger(U),U) == ident(8) and mm(U,dagger(U)) == ident(8))
+check('RESET-ISOMETRIES',all(mm(dagger(r),r) == ident(8) for r in reset))
+check('PROJECTOR-RESOLUTION',total(P,8) == ident(8))
+check('ACTUAL-UNIFORM-RESET',all(reset_state(x) == tensor(x,unit(4,0,0)) for x in units))
+check('ACTUAL-CORRECTED-BRANCHES',all(
+    branches(x)[0] == scale(R(5,8),apply(D,x)) and
+    all(b == scale(R(1,8),x) for b in branches(x)[1:]) for x in units))
+check('STOPPED-DEPTHS-0-8',all(stopped(k,x) == formula(k,x) for k in range(9) for x in units))
+e01 = unit(2,0,1)
+check('CONTROL-REMOVE-RESET',total(branches(e01,do_reset=False),2) != formula(1,e01))
+check('CONTROL-REMOVE-CORRECTION',total(branches(e01,do_correct=False),2) != formula(1,e01))
+check('CONTROL-CONTINUE-SUCCESS',total(branches(total(branches(e01),2)),2) != formula(2,e01))
+if not all(checks):
+    print('NO VERDICT: a required control failed')
+    sys.exit(1)
+print('FINITE-PROTOCOL: PASS; 10 groups; 36 stopped matrix-unit cases')
diff --git a/verification/lean-mathlib/OIBridge.lean b/verification/lean-mathlib/OIBridge.lean
index 9dd9ce966..184357168 100644
--- a/verification/lean-mathlib/OIBridge.lean
+++ b/verification/lean-mathlib/OIBridge.lean
@@ -1,3 +1,4 @@
+import OIBridge.BridgeFiniteProtocol
 /-
   OIBridge.lean — ROADMAP §A1/§A5, in the form the counting layer consumes.
 
diff --git a/verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean b/verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean
new file mode 100644
index 000000000..ead35aa26
--- /dev/null
+++ b/verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean
@@ -0,0 +1,296 @@
+/-
+  Finite stopped protocols, constructed with the kernel's five InstAvail constructors.
+
+  The only operational inputs to the concrete attempt are the stated four-level readout,
+  the reset permutations, the eight-dimensional balanced circuit, its isometry, and the
+  conditional Z correction. Ancillas start maximally mixed, as InstAvail.discard requires;
+  readout and outcome-dependent permutations produce the pure seed inside the protocol.
+
+  Availability of a whole approximation sequence is not a premise. No claim is made that
+  available operations preserve an arbitrary pair cone, or that a channel limit is available.
+  This module is design evidence until adopted by a governed native round.
+-/
+import OIBridge.ImplementationLocality
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+import Mathlib.Tactic.Ring
+
+namespace OIBridge
+namespace BridgeFiniteProtocol
+
+open Matrix MonoidalCompletion CoherentExtension ReferenceExtension InterventionLocality
+  AncillaClosure CoherentLift SpectatorBridge OperationalAssembly
+
+noncomputable section
+
+abbrev Channel (T : Type) [Fintype T] [DecidableEq T] :=
+  Matrix T T ℂ →ₗ[ℂ] Matrix T T ℂ
+
+section Stopped
+
+variable {𝓘 : ImplementationClass} {T : Type} [Fintype T] [DecidableEq T]
+
+/-- Outcome zero is success. A failure runs the remaining stopped protocol. -/
+def stopped (F : Fin 4 → Channel T) : ℕ → Channel T
+  | 0 => LinearMap.id
+  | k + 1 => ∑ j : Fin 4, (if j = 0 then LinearMap.id else stopped F k).comp (F j)
+
+/-- The one-step continuation is an actual bind, followed by classical coarse-graining. -/
+theorem instAvail_stopped_step {F : Fin 4 → Channel T} {Φ : Channel T}
+    (hF : InstAvail 𝓘 T (Fin 4) F)
+    (hId : InstAvail 𝓘 T Unit (fun _ => LinearMap.id))
+    (hΦ : InstAvail 𝓘 T Unit (fun _ => Φ)) :
+    InstAvail 𝓘 T Unit (fun _ =>
+      ∑ j : Fin 4, (if j = 0 then LinearMap.id else Φ).comp (F j)) := by
+  have hc : ∀ j : Fin 4, InstAvail 𝓘 T Unit
+      (fun _ => if j = 0 then LinearMap.id else Φ) := by
+    intro j
+    by_cases hj : j = 0
+    · simpa only [hj, if_true] using hId
+    · simpa only [hj, if_false] using hΦ
+  have h := InstAvail.coarse (fun _ : Fin 4 × Unit => ()) (InstAvail.bind hF hc)
+  have he : (fun _ : Unit =>
+      ∑ j : Fin 4, (if j = 0 then LinearMap.id else Φ).comp (F j))
+      = fun a : Unit => ∑ c ∈ Finset.univ.filter (fun _ : Fin 4 × Unit => () = a),
+        (if c.1 = 0 then LinearMap.id else Φ).comp (F c.1) := by
+    funext a
+    cases a
+    simp [Fintype.sum_prod_type]
+  rw [← he] at h
+  exact h
+
+/-- Every finite depth is available, by induction using bind and coarse. -/
+theorem instAvail_stopped (arch : Architecture 𝓘) {F : Fin 4 → Channel T}
+    (hF : InstAvail 𝓘 T (Fin 4) F) (k : ℕ) :
+    InstAvail 𝓘 T Unit (fun _ => stopped F k) := by
+  induction k with
+  | zero => exact instAvail_id (arch.one T)
+  | succ k ih => exact instAvail_stopped_step hF (instAvail_id (arch.one T)) ih
+
+/-- Algebraic closed form, from the independently identified success and failure branches.
+    These equalities say nothing about availability; that is proved above. -/
+theorem stopped_closedForm (F : Fin 4 → Channel T) (D : Channel T) (q : ℂ)
+    (hS : F 0 = (1 - q) • D) (hF : ∑ j : Fin 3, F j.succ = q • LinearMap.id)
+    (k : ℕ) :
+    stopped F k = (1 - q ^ k) • D + q ^ k • LinearMap.id := by
+  induction k with
+  | zero => simp [stopped]
+  | succ k ih =>
+    rw [stopped, Fin.sum_univ_succ]
+    simp only [if_pos rfl, LinearMap.id_comp]
+    have hj : ∀ j : Fin 3, (j.succ : Fin 4) ≠ 0 := fun j => Fin.succ_ne_zero j
+    simp only [if_neg (hj _)]
+    have hm : (∑ j : Fin 3, (stopped F k).comp (F j.succ))
+        = (stopped F k).comp (q • LinearMap.id) := by
+      calc
+        _ = (stopped F k).comp (∑ j : Fin 3, F j.succ) := by
+          ext X s t
+          simp [LinearMap.comp_apply, map_sum]
+        _ = _ := by rw [hF]
+    rw [hm, hS, ih]
+    ext X s t
+    simp only [if_true, LinearMap.add_apply, LinearMap.smul_apply, LinearMap.comp_apply,
+      LinearMap.id_apply, map_smul, Matrix.add_apply, Matrix.smul_apply, smul_eq_mul]
+    rw [pow_succ]
+    ring
+
+end Stopped
+
+abbrev Token := Fin 2
+abbrev Work := Token × Fin 4
+
+/-- Reset register value j to zero by a reversible swap. -/
+def resetEquiv (j : Fin 4) : Work ≃ Work :=
+  (Equiv.refl Token).prodCongr (Equiv.swap j 0)
+
+def resetPerm (j : Fin 4) : Matrix Work Work ℂ := permMatrix (resetEquiv j)
+
+def resetChannel : Channel Work :=
+  ∑ j : Fin 4, (conjChannel (resetPerm j)).comp (conjChannel (InterventionLocality.readProj Token 4 j))
+
+theorem instAvail_reset {𝓘 : ImplementationClass} (arch : Architecture 𝓘)
+    (hReset : ∀ j, 𝓘 Work (resetPerm j)) :
+    InstAvail 𝓘 Work Unit (fun _ => resetChannel) := by
+  have hp : InstAvail 𝓘 Work (Fin 4) (fun j => conjChannel (InterventionLocality.readProj Token 4 j)) := by
+    have h := InstAvail.readout (𝓘 := 𝓘) (Equiv.refl Work) (fun j => arch.proj Token 4 j)
+    simpa only [Matrix.reindex_refl_refl] using h
+  have hr : ∀ j : Fin 4, InstAvail 𝓘 Work Unit (fun _ => conjChannel (resetPerm j)) :=
+    fun j => InstAvail.op _ (hReset j) (permMatrix_isometry (resetEquiv j))
+  have h := InstAvail.coarse (fun _ : Fin 4 × Unit => ()) (InstAvail.bind hp hr)
+  have he : (fun _ : Unit => resetChannel) =
+      fun a : Unit => ∑ c ∈ Finset.univ.filter (fun _ : Fin 4 × Unit => () = a),
+        (conjChannel (resetPerm c.1)).comp (conjChannel (InterventionLocality.readProj Token 4 c.1)) := by
+    funext a
+    cases a
+    simp [resetChannel, Fintype.sum_prod_type]
+  rw [← he] at h
+  exact h
+
+/-- The reset acts on the actual uniformly attached register, rather than assuming a pure
+    ancilla. This entrywise formula is valid for every input matrix. -/
+theorem reset_uniformAttach (X : Matrix Token Token ℂ) (s t : Token) (f e : Fin 4) :
+    resetChannel (uniformAttach 4 X) (s, f) (t, e) =
+      if f = 0 ∧ e = 0 then X s t else 0 := by
+  simp only [resetChannel, LinearMap.sum_apply, Matrix.sum_apply, LinearMap.comp_apply,
+    conjChannel_apply]
+  simp only [resetPerm, permMatrix_conj_apply, InterventionLocality.readProj,
+    Matrix.diagonal_conjTranspose, Matrix.diagonal_mul, Matrix.mul_diagonal,
+    Matrix.diagonal_apply_eq]
+  fin_cases f <;> fin_cases e <;>
+    simp [resetEquiv, uniformAttach, tensorOf_apply, Fin.sum_univ_four,
+      Matrix.smul_apply, Matrix.one_apply, Equiv.swap_apply_def] <;> norm_num <;> ring
+
+theorem reset_uniformAttach_eq_pure (X : Matrix Token Token ℂ) :
+    resetChannel (uniformAttach 4 X) = pureAttach 4 0 X := by
+  ext ⟨s, f⟩ ⟨t, e⟩
+  rw [reset_uniformAttach]
+  simp [pureAttach_apply, tensorOf_apply, Matrix.single_apply, eq_comm]
+
+/-- The exact rational eight-dimensional balanced circuit, in its computational basis.
+    v is the final column of the unnormalized two-ancilla Hadamard table. -/
+def v (a : Fin 4) : ℂ := if a = 1 ∨ a = 2 then -1 else 1
+
+def balancedCircuit : Matrix Work Work ℂ := fun r c =>
+  if r.1 = c.1 then
+    (if r.2 = c.2 then (if r.1 = 0 then 1 else Complex.I) else 0) +
+      ((if r.1 = 0 then Complex.I - 1 else 1 - Complex.I) / 4) * v r.2 * v c.2
+  else 0
+
+theorem balancedCircuit_isometry : balancedCircuitᴴ * balancedCircuit = 1 := by
+  ext ⟨s, a⟩ ⟨t, b⟩
+  fin_cases s <;> fin_cases t <;> fin_cases a <;> fin_cases b <;>
+    simp [Matrix.mul_apply, Matrix.conjTranspose_apply, Fintype.sum_prod_type,
+      Fin.sum_univ_two, Fin.sum_univ_four, balancedCircuit, v, Matrix.one_apply,
+      Complex.star_def, map_ofNat] <;> ring_nf <;>
+    simp [Complex.I_sq, Complex.I_pow_four, map_ofNat] <;> ring
+
+def drivePhase : Matrix Token Token ℂ :=
+  Matrix.diagonal fun s => if s = 0 then 1 else 3 / 5 + (4 / 5) * Complex.I
+
+def correction (j : Fin 4) : Matrix Work Work ℂ :=
+  Matrix.diagonal fun r => if j = 0 ∨ r.1 = 0 then 1 else -1
+
+theorem correction_isometry (j : Fin 4) : (correction j)ᴴ * correction j = 1 := by
+  ext r c
+  by_cases hrc : r = c
+  · subst c
+    by_cases hr : j = 0 ∨ r.1 = 0 <;>
+      simp [correction, Matrix.diagonal_conjTranspose, Matrix.diagonal_mul_diagonal, hr]
+  · simp [correction, Matrix.diagonal_conjTranspose, Matrix.diagonal_mul_diagonal, hrc]
+
+/-- Read the register and perform the Z correction on each failure branch. -/
+def correctedReadout (U : Matrix Work Work ℂ) (j : Fin 4) : Channel Work :=
+  (conjChannel (correction j)).comp
+    ((conjChannel (InterventionLocality.readProj Token 4 j)).comp (conjChannel U))
+
+/-- Reset first, then the stated circuit/readout/correction, and discard the same uniformly
+    attached ancilla. The readout outcome remains visible until the stopped loop consumes it. -/
+def attempt (U : Matrix Work Work ℂ) (j : Fin 4) : Channel Token :=
+  discardWith (A := Token) 4 (uniformAttach 4) ((correctedReadout U j).comp resetChannel)
+
+set_option maxHeartbeats 2000000 in
+/-- Exact identity for each branch of the constructed attempt, including the actual reset
+    from the uniformly attached register and its final partial trace. -/
+theorem attempt_balanced_branch (j : Fin 4) :
+    attempt balancedCircuit j = if j = 0 then (5 / 8 : ℂ) • conjChannel drivePhase
+      else (1 / 8 : ℂ) • LinearMap.id := by
+  ext X s t
+  change ptraceAnc 4 (conjChannel (correction j)
+    (conjChannel (InterventionLocality.readProj Token 4 j)
+      (conjChannel balancedCircuit (resetChannel (uniformAttach 4 X))))) s t = _
+  rw [reset_uniformAttach_eq_pure]
+  fin_cases s <;> fin_cases t <;> fin_cases j <;>
+    simp [attempt, discardWith, correctedReadout, LinearMap.comp_apply, ptraceAncL,
+      ptraceAnc_apply, reset_uniformAttach_eq_pure, pureAttach_apply,
+      conjChannel_apply, correction, InterventionLocality.readProj,
+      Matrix.diagonal_mul, Matrix.mul_diagonal, Matrix.diagonal_conjTranspose,
+      Matrix.mul_apply, Matrix.conjTranspose_apply, Fintype.sum_prod_type,
+      Fin.sum_univ_two, Fin.sum_univ_four, balancedCircuit, v, drivePhase,
+      Matrix.single_apply, tensorOf_apply, Complex.star_def, map_ofNat] <;>
+    ring_nf <;> simp [Complex.I_sq, Complex.I_pow_four, map_ofNat] <;> ring
+
+theorem instAvail_attempt {𝓘 : ImplementationClass} (arch : Architecture 𝓘)
+    (U : Matrix Work Work ℂ) (hU : 𝓘 Work U) (hIso : Uᴴ * U = 1)
+    (hReset : ∀ j, 𝓘 Work (resetPerm j))
+    (hCorrect : ∀ j, 𝓘 Work (correction j)) :
+    InstAvail 𝓘 Token (Fin 4) (attempt U) := by
+  have hp : InstAvail 𝓘 Work (Fin 4) (fun j => conjChannel (InterventionLocality.readProj Token 4 j)) := by
+    have h := InstAvail.readout (𝓘 := 𝓘) (Equiv.refl Work) (fun j => arch.proj Token 4 j)
+    simpa only [Matrix.reindex_refl_refl] using h
+  have hu := instAvail_comp_one hp (InstAvail.op U hU hIso)
+  have hc : ∀ j : Fin 4, InstAvail 𝓘 Work Unit (fun _ => conjChannel (correction j)) :=
+    fun j => InstAvail.op _ (hCorrect j) (correction_isometry j)
+  have hb := InstAvail.coarse (fun c : Fin 4 × Unit => c.1) (InstAvail.bind hu hc)
+  have he : correctedReadout U =
+      fun j => ∑ c ∈ Finset.univ.filter (fun c : Fin 4 × Unit => c.1 = j),
+        (conjChannel (correction c.1)).comp
+          ((conjChannel (InterventionLocality.readProj Token 4 c.1)).comp (conjChannel U)) := by
+    funext j
+    simp [correctedReadout, Finset.sum_filter, Fintype.sum_prod_type]
+  rw [← he] at hb
+  exact InstAvail.discard (by decide : 0 < 4)
+    (instAvail_comp_one hb (instAvail_reset arch hReset))
+
+/-- This closes the all-depth availability obligation from primitive operations, with no
+    available-channel sequence supplied as a hypothesis. -/
+theorem finite_protocol_available {𝓘 : ImplementationClass} (arch : Architecture 𝓘)
+    (U : Matrix Work Work ℂ) (hU : 𝓘 Work U) (hIso : Uᴴ * U = 1)
+    (hReset : ∀ j, 𝓘 Work (resetPerm j))
+    (hCorrect : ∀ j, 𝓘 Work (correction j)) (k : ℕ) :
+    InstAvail 𝓘 Token Unit (fun _ => stopped (attempt U) k) :=
+  instAvail_stopped arch (instAvail_attempt arch U hU hIso hReset hCorrect) k
+
+/-- The O14 stopped-loop formula at every finite depth, derived from the constructed
+    branch maps rather than posited as an available approximation. -/
+theorem balanced_stopped_formula (k : ℕ) :
+    stopped (attempt balancedCircuit) k =
+      (1 - (3 / 8 : ℂ) ^ k) • conjChannel drivePhase +
+        (3 / 8 : ℂ) ^ k • LinearMap.id := by
+  apply stopped_closedForm
+  · rw [attempt_balanced_branch]
+    norm_num
+  · simp only [attempt_balanced_branch, Fin.succ_ne_zero, if_false]
+    rw [← Finset.sum_smul]
+    norm_num [Fin.sum_univ_three]
+
+theorem balanced_finite_available {𝓘 : ImplementationClass} (arch : Architecture 𝓘)
+    (hCircuit : 𝓘 Work balancedCircuit)
+    (hReset : ∀ j, 𝓘 Work (resetPerm j))
+    (hCorrect : ∀ j, 𝓘 Work (correction j)) (k : ℕ) :
+    InstAvail 𝓘 Token Unit (fun _ =>
+      (1 - (3 / 8 : ℂ) ^ k) • conjChannel drivePhase +
+        (3 / 8 : ℂ) ^ k • LinearMap.id) := by
+  rw [← balanced_stopped_formula]
+  exact finite_protocol_available arch balancedCircuit hCircuit balancedCircuit_isometry
+    hReset hCorrect k
+
+/-- Availability also holds after adding a spectator, exactly through the existing kernel
+    rule. Context stability and label invariance remain explicit inventory hypotheses. -/
+theorem finite_protocol_spectator {𝓘 : ImplementationClass} (arch : Architecture 𝓘)
+    (hContext : ContextStable 𝓘) (hLabels : LabelInvariant 𝓘)
+    (R : Type) [Fintype R] [DecidableEq R]
+    (U : Matrix Work Work ℂ) (hU : 𝓘 Work U) (hIso : Uᴴ * U = 1)
+    (hReset : ∀ j, 𝓘 Work (resetPerm j))
+    (hCorrect : ∀ j, 𝓘 Work (correction j)) (k : ℕ) :
+    InstAvail 𝓘 (R × Token) Unit (fun _ => amplRefL R (stopped (attempt U) k)) :=
+  instAvail_spectator hContext hLabels R
+    (finite_protocol_available arch U hU hIso hReset hCorrect k)
+
+end
+end BridgeFiniteProtocol
+end OIBridge
+
+#print axioms OIBridge.BridgeFiniteProtocol.instAvail_stopped_step
+#print axioms OIBridge.BridgeFiniteProtocol.instAvail_stopped
+#print axioms OIBridge.BridgeFiniteProtocol.stopped_closedForm
+#print axioms OIBridge.BridgeFiniteProtocol.instAvail_reset
+#print axioms OIBridge.BridgeFiniteProtocol.reset_uniformAttach
+#print axioms OIBridge.BridgeFiniteProtocol.reset_uniformAttach_eq_pure
+#print axioms OIBridge.BridgeFiniteProtocol.balancedCircuit_isometry
+#print axioms OIBridge.BridgeFiniteProtocol.correction_isometry
+#print axioms OIBridge.BridgeFiniteProtocol.attempt_balanced_branch
+#print axioms OIBridge.BridgeFiniteProtocol.instAvail_attempt
+#print axioms OIBridge.BridgeFiniteProtocol.finite_protocol_available
+#print axioms OIBridge.BridgeFiniteProtocol.balanced_stopped_formula
+#print axioms OIBridge.BridgeFiniteProtocol.balanced_finite_available
+#print axioms OIBridge.BridgeFiniteProtocol.finite_protocol_spectator