Design: construct finite stopped-channel availability from primitive operations

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.

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.

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

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

verification/lean-mathlib/OIBridge.lean

@@ -1,3 +1,4 @@
+import OIBridge.BridgeFiniteProtocol
 /-
   OIBridge.lean — ROADMAP §A1/§A5, in the form the counting layer consumes.