diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 4cd48e87e..c2203af2f 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -410,6 +410,21 @@ jobs: - name: Audit control mutation tests run: python3 -I -B verification/programmes/oi-qm/reconstruction/round-oi-channel-1-audit/controls.py --self-test + probes_oifiniteprotocol1: + name: Numerical probes / OI finite protocol + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + - uses: actions/setup-python@v5 + with: + python-version: '3.11' + - name: Exact finite protocol controls + run: python3 -I -B verification/lean/oi_finite_protocol_check.py + - name: Adoption control mutation tests + run: python3 -I -B verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/controls.py --self-test + # Act 42. Two shards run on every event; the exclusion shards, about six CPU-hours between them, # run only on workflow_dispatch, which is how the exact-head attestations are taken (section A.39). # On any other event the matrix job is skipped and the aggregate below requires exactly that. @@ -505,7 +520,7 @@ jobs: probes: name: Numerical probes - needs: [probes_core_a, probes_core_b, probes_a36, probes_a38, probes_a40, probes_a41_production, probes_a41_independent, probes_a41_hulls, probes_a45, probes_nb1, probes_kinf2, probes_kt4prem1, probes_oichannel1, probes_a42_witness, probes_a42_census01, probes_a42_exclusion, probes_foundations] + needs: [probes_core_a, probes_core_b, probes_a36, probes_a38, probes_a40, probes_a41_production, probes_a41_independent, probes_a41_hulls, probes_a45, probes_nb1, probes_kinf2, probes_kt4prem1, probes_oichannel1, probes_oifiniteprotocol1, probes_a42_witness, probes_a42_census01, probes_a42_exclusion, probes_foundations] if: ${{ always() }} runs-on: ubuntu-latest steps: @@ -524,6 +539,7 @@ jobs: KINF2_RESULT: ${{ needs.probes_kinf2.result }} KT4PREM1_RESULT: ${{ needs.probes_kt4prem1.result }} OICHANNEL1_RESULT: ${{ needs.probes_oichannel1.result }} + OIFINITEPROTOCOL1_RESULT: ${{ needs.probes_oifiniteprotocol1.result }} A42W_RESULT: ${{ needs.probes_a42_witness.result }} A42C_RESULT: ${{ needs.probes_a42_census01.result }} A42X_RESULT: ${{ needs.probes_a42_exclusion.result }} @@ -542,6 +558,7 @@ jobs: echo "kinf2=${KINF2_RESULT}" echo "kt4prem1=${KT4PREM1_RESULT}" echo "oichannel1=${OICHANNEL1_RESULT}" + echo "oifiniteprotocol1=${OIFINITEPROTOCOL1_RESULT}" echo "a42_witness=${A42W_RESULT}" echo "a42_census01=${A42C_RESULT}" echo "a42_exclusion=${A42X_RESULT} (event ${GITHUB_EVENT_NAME})" @@ -559,6 +576,7 @@ jobs: test "${KINF2_RESULT}" = success test "${KT4PREM1_RESULT}" = success test "${OICHANNEL1_RESULT}" = success + test "${OIFINITEPROTOCOL1_RESULT}" = success test "${A42W_RESULT}" = success test "${A42C_RESULT}" = success if [ "${GITHUB_EVENT_NAME}" = workflow_dispatch ]; then diff --git a/verification/lean-manuscript-census.json b/verification/lean-manuscript-census.json index 1bc4d1f1c..88206432a 100644 --- a/verification/lean-manuscript-census.json +++ b/verification/lean-manuscript-census.json @@ -1457,6 +1457,15 @@ "status": "kernel-only", "manuscript": [], "note": "Round RELC-SELECT-1, a native round under AGENTS.md §A.39, executed under the frozen control plane programmes/oi-qm/reconstruction/round-relc-select-1/preregistration.md. Q-PAR: from IsNot (eball d) z N and the control relation alone, the two homogenized eigenspaces of N have equal dimension and d is not even (finrank_plus_eq_finrank_minus_relC, not_even_of_relC). Q-SEL: CtrlGate, NativeGate's frame, two positivity clauses and control relation without its target relation, gives d = 1 ∨ d = 3 with IsNot and d = 3 with Entangling (dim_of_ctrlGate, three_of_ctrlGate), through DIM-1's block reduction restated over CtrlGate with its one target-relation step replaced by actT_slice_ctrl. Q-POS: at d = 5 with PARITY-NOT-1's n5, the squeezed gate gSq has the frame, GateRel and forward positivity and fails inverse positivity, and its inverse has the frame, GateRel and inverse positivity and fails forward positivity (gSq_sep, gSqInv_sep). Q-REL: at d = 5 the witness NOT nC5 and NB-1's J/K map gC5 have the frame, the target relation and both positivity clauses and fail the control relation (c5_sep), so those clauses with IsNot do not give d = 1 ∨ d = 3 (relT_not_dimension_selecting). Carried by no manuscript. CtrlGate is the selector's hypothesis only; NativeGate and GateRel are unchanged and the target relation remains a field of both; the transfer of the control relation to an inverse reads the target relation; the frame is not audited." + }, + { + "name": "Finite stopped-channel protocols constructed from primitive resources (round OI-FINITE-PROTOCOL-1, reconstruction)", + "modules": [ + "BridgeFiniteProtocol" + ], + "status": "kernel-only", + "manuscript": [], + "note": "Conditional finite-depth availability through InstAvail readout, op, bind, coarse and discard. The actual uniformly attached ancilla is reset internally. From Architecture and explicit circuit/reset/correction memberships, finite_protocol_available constructs every finite depth; balanced_stopped_formula derives the O14 channel formula and balanced_finite_available combines availability with it. finite_protocol_spectator additionally requires ContextStable and LabelInvariant. No AvailableChannelApproximation sequence is a premise. Primitive memberships, convergence, availability of a limit, physical state/test identification, validity or preservation of an arbitrary pair cone, arbitrary finite-carrier reconstruction and unconditional OI reconstruction remain unestablished here. Carried by no manuscript." } ] } diff --git a/verification/lean-mathlib/OIBridge.lean b/verification/lean-mathlib/OIBridge.lean index f3b6b201c..03a29e2fd 100644 --- a/verification/lean-mathlib/OIBridge.lean +++ b/verification/lean-mathlib/OIBridge.lean @@ -139,6 +139,7 @@ import OIBridge.CompletedOI import OIBridge.CarrierGeneralOIPlus import OIBridge.EmbeddedObservation import OIBridge.ImplementationLocality +import OIBridge.BridgeFiniteProtocol import OIBridge.MicroscopicReversibility import OIBridge.LieRankSource import OIBridge.SubstratumSource diff --git a/verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean b/verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean new file mode 100644 index 000000000..baf7a6d42 --- /dev/null +++ b/verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean @@ -0,0 +1,296 @@ +/- + Conditional finite stopped protocols, constructed with InstAvail's five rules. + + Four-level readout and primitive circuit/reset/correction memberships remain explicit. + Ancillas start maximally mixed; readout and conditional permutations reset them internally. + Every finite depth is available from these primitive resources, rather than assumed as a + whole approximation sequence. Spectator extension assumes context and label stability. + + No limiting-channel availability, arbitrary pair-cone preservation, physical state/test + identification or unconditional OI reconstruction is established by these theorems. + Adopted infrastructure is registered kernel-only by round OI-FINITE-PROTOCOL-1. +-/ +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 diff --git a/verification/lean/oi_finite_protocol_check.py b/verification/lean/oi_finite_protocol_check.py new file mode 100644 index 000000000..ef104005b --- /dev/null +++ b/verification/lean/oi_finite_protocol_check.py @@ -0,0 +1,167 @@ +#!/usr/bin/env python3 +"""Exact controls for round OI-FINITE-PROTOCOL-1. 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/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/controls.py b/verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/controls.py new file mode 100644 index 000000000..104dfba2b --- /dev/null +++ b/verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/controls.py @@ -0,0 +1,245 @@ +#!/usr/bin/env python3 +"""Frozen adoption controls; no imports from the checker or Lean implementation.""" +import argparse +import hashlib +import json +from pathlib import Path +import re +import subprocess +import sys + +META = {'d': 'f2415108601a9c36bb985b3374c56f0eb34c2962', 'family': {'name': 'Finite stopped-channel protocols constructed from primitive resources (round OI-FINITE-PROTOCOL-1, reconstruction)', 'modules': ['BridgeFiniteProtocol'], 'status': 'kernel-only', 'manuscript': [], 'note': 'Conditional finite-depth availability through InstAvail readout, op, bind, coarse and discard. The actual uniformly attached ancilla is reset internally. From Architecture and explicit circuit/reset/correction memberships, finite_protocol_available constructs every finite depth; balanced_stopped_formula derives the O14 channel formula and balanced_finite_available combines availability with it. finite_protocol_spectator additionally requires ContextStable and LabelInvariant. No AvailableChannelApproximation sequence is a premise. Primitive memberships, convergence, availability of a limit, physical state/test identification, validity or preservation of an arbitrary pair cone, arbitrary finite-carrier reconstruction and unconditional OI reconstruction remain unestablished here. Carried by no manuscript.'}, 'workflow_splices': [[' # Act 42. Two shards run on every event;', " probes_oifiniteprotocol1:\n name: Numerical probes / OI finite protocol\n runs-on: ubuntu-latest\n steps:\n - uses: actions/checkout@v4\n with:\n fetch-depth: 0\n - uses: actions/setup-python@v5\n with:\n python-version: '3.11'\n - name: Exact finite protocol controls\n run: python3 -I -B verification/lean/oi_finite_protocol_check.py\n - name: Adoption control mutation tests\n run: python3 -I -B verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/controls.py --self-test\n\n # Act 42. Two shards run on every event;"], ['probes_oichannel1, probes_a42_witness', 'probes_oichannel1, probes_oifiniteprotocol1, probes_a42_witness'], [' OICHANNEL1_RESULT: ${{ needs.probes_oichannel1.result }}\n', ' OICHANNEL1_RESULT: ${{ needs.probes_oichannel1.result }}\n OIFINITEPROTOCOL1_RESULT: ${{ needs.probes_oifiniteprotocol1.result }}\n'], [' echo "oichannel1=${OICHANNEL1_RESULT}"\n', ' echo "oichannel1=${OICHANNEL1_RESULT}"\n echo "oifiniteprotocol1=${OIFINITEPROTOCOL1_RESULT}"\n'], [' test "${OICHANNEL1_RESULT}" = success\n', ' test "${OICHANNEL1_RESULT}" = success\n test "${OIFINITEPROTOCOL1_RESULT}" = success\n']], 'roadmap_splice': ['- **K3 — the operations. CONDITIONAL** on reaching complex matrix kinematics. A quantum\n architecture — an architecture that is context-, label- and dagger-stable and drives the\n elementary transitions (`DrivesElementary`) — generates a theory carrying every finite\n endomorphic quantum operation (`genTheory_qm_of_quantumArchitecture`), through composite unitary\n control (`control_of_lieRank`) and the full instruments (`fullInstruments_of_control`). The typed\n characterization covers the finite rectangular Kraus endpoint (`typed_determined_iff`).\n', '- **K3 — the operations. CONDITIONAL** on reaching complex matrix kinematics. A quantum\n architecture — an architecture that is context-, label- and dagger-stable and drives the\n elementary transitions (`DrivesElementary`) — generates a theory carrying every finite\n endomorphic quantum operation (`genTheory_qm_of_quantumArchitecture`), through composite unitary\n control (`control_of_lieRank`) and the full instruments (`fullInstruments_of_control`). The typed\n characterization covers the finite rectangular Kraus endpoint (`typed_determined_iff`). Round OI-FINITE-PROTOCOL-1 constructs every finite\n stopped-channel depth from an architecture and explicit circuit/reset/correction\n memberships (`finite_protocol_available`); its balanced circuit obeys the all-depth\n formula (`balanced_stopped_formula`) and yields conditional availability\n (`balanced_finite_available`). The ancilla starts uniformly mixed and is reset inside\n the protocol. Spectator extension additionally requires `ContextStable` and\n `LabelInvariant` (`finite_protocol_spectator`). Primitive memberships, convergence and\n availability of a limiting drive, physical state/test identification and preservation\n of an arbitrary pair cone remain separate obligations. K3 retains its conditional status.\n'], 'body_sha256': '016c8e724c73ae358fbcae3646c0b7e975beed3ddd8056d9197bf2f79a27b847', 'pins': {'verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean': {'sha256': 'd350d235b1b8b1379f9ea9dafcdb6be7a9f256f0eda96633ff119a7904c7cce4', 'blob': 'baf7a6d421597b115d588b824524e3bc38a946d6'}, 'verification/lean/oi_finite_protocol_check.py': {'sha256': '5a4f0862b953e4d07e201ecbe03291d0cfa6e6df615dd4b6f25f723052927839', 'blob': 'ef104005b47ef5323a2a937d5df3c7c993f972d4'}, 'verification/lean-mathlib/OIBridge.lean': {'sha256': 'db19e164d0843cddffa1e8a5f281911b0742e9f1b5dc794fc287333ddc75847a', 'blob': '03a29e2fd41634103d6a274f3fb36056ed5b6826'}, 'verification/lean-manuscript-census.json': {'sha256': '0803c812cafeffbbbd7b211e5d9420ab3372f29ac31fe35655ad471192423aa9', 'blob': '88206432a44074cbd1bfb46fff1847d2dcb425f4'}, '.github/workflows/verify.yml': {'sha256': '05020b877f667199f647ce50b00e446670e2e1fea37854e5a00972b879eb089d', 'blob': 'c2203af2f9f668442561f02e6a936c736378d362'}, 'verification/ROADMAP.md': {'sha256': '971b868db5e81ca7eaad17dd1d39c97558a4553f3ddad9e16162bd65312af615', 'blob': 'ba7b23d4f1b0a2b78722dbc15b3fc51193f147d8'}}, 'anchors': {'verification/lean-mathlib/OIBridge.lean': 'e5af9614009889dab616d7f02f75bb395f1ae1fb01307f46ef82d3b282b4c313', 'verification/lean-manuscript-census.json': 'cdadb02e0463366c036834f2ca58ae904ad70e05dfe981fd1f37d9bc928e0bbf', '.github/workflows/verify.yml': 'bd71bdc270753be8296c4a5c9723e23673c2f8acdaa9417fb70a6ddd6cbe2443', 'verification/ROADMAP.md': 'a64835c2107131530f2396311b3e8fa291bc690462ffbbde225f3479d89a2c2c', 'verification/lean-mathlib/OIBridge/ImplementationLocality.lean': '4e5b4b22298dfba7b0ee7ba26109ef3090eb48b23227734bb26bbf6834a545ac', 'verification/lean-mathlib/OIBridge/OperationalValidity.lean': 'ba316747d23820f75f4bbd25105d87a85febb3bd1d0eaa123913b629b34f05f0'}} +ROUND = 'verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/' +MODULE = 'verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean' +PROBE = 'verification/lean/oi_finite_protocol_check.py' +WORKFLOW = '.github/workflows/verify.yml' +AGGREGATE = 'verification/lean-mathlib/OIBridge.lean' +REGISTRY = 'verification/lean-manuscript-census.json' +ROADMAP = 'verification/ROADMAP.md' +OUTPUT_SHA = 'f33e3c97bd1baa7f4b583f798cf0ecdec185860d37f69523f31128e4131d35e1' +RESULT = '''# OI-FINITE-PROTOCOL-1 — finite stopped protocol from primitive resources + +Outcome: OI-FINITE-PROTOCOL-1-PROVED + +Every finite stopped-channel depth is InstAvail from Architecture and explicit circuit/reset/correction memberships, using the existing readout, op, bind, coarse and discard rules. The uniformly mixed ancilla is reset inside the protocol. The balanced circuit's corrected branches and all-depth stopped formula are proved for every input matrix. No available approximation sequence is a premise. + +Spectator availability additionally requires ContextStable and LabelInvariant. Primitive memberships, convergence, availability of a limiting drive, physical state/test identification and validity or preservation of an arbitrary pair cone remain separate obligations. K2 remains open, K3 remains conditional, and arbitrary finite-carrier reconstruction and the full operation/instrument correspondence retain their existing obligations. This package does not establish unconditional OI reconstruction or full-model independence. + +Exact controls: FINITE-PROTOCOL: PASS; 10 groups; 36 stopped matrix-unit cases +Arithmetic is in Q(i). Replay is byte-identical, stderr is empty and exit code is zero. Removing reset, removing correction and continuing after success each disagrees with the intended map on the 0,1 matrix unit. These finite controls do not prove the universal theorem. + +The adopted module is kernel-only and imports only existing main ImplementationLocality and Mathlib tactics. Its proof body is unchanged from the measured #810 design head 708153423ffb5ea4fe27663654431650b5a2e48a. Historical design measurements and new predictive evidence are recorded separately in the preregistration; neither is an F/E attestation. + +F: {F} +F workflow run: {F_RUN} +S1: {S1} +S1 workflow run: {S1_RUN} + +Successful Build and fourteen standard named axiom reports without sorryAx are required, alongside all-green exact-head host checks before E designation. Owner E designation and host attestations are recorded in the receipt. Local content controls do not certify host facts. +''' + + +def sha(data): + return hashlib.sha256(data).hexdigest() + + +def git(*args): + return subprocess.check_output(['git', *args]) + + +def originals(): + data = {p: git('show', META['d'] + ':' + p) for p in META['anchors']} + if any(sha(data[p]) != digest for p, digest in META['anchors'].items()): + raise ValueError('D anchor mismatch') + return data + + +def expected(original): + output = {} + aggregate = original[AGGREGATE] + anchor = b'import OIBridge.ImplementationLocality\n' + if aggregate.count(anchor) != 1: + raise ValueError('non-unique aggregate anchor') + output[AGGREGATE] = aggregate.replace(anchor, anchor + b'import OIBridge.BridgeFiniteProtocol\n') + registry = json.loads(original[REGISTRY]) + registry['families'].append(META['family']) + output[REGISTRY] = (json.dumps(registry, indent=2, ensure_ascii=False) + '\n').encode() + workflow = original[WORKFLOW].decode() + for old, new in META['workflow_splices']: + if workflow.count(old) != 1: + raise ValueError('non-unique workflow anchor') + workflow = workflow.replace(old, new) + output[WORKFLOW] = workflow.encode() + roadmap = original[ROADMAP].decode() + old, new = META['roadmap_splice'] + if roadmap.count(old) != 1: + raise ValueError('non-unique roadmap anchor') + output[ROADMAP] = roadmap.replace(old, new).encode() + return output + + +def result_ok(data, freeze_id, s1_id): + text = data.decode(errors='replace') + names = {} + for field, pattern in [('F', '[0-9a-f]{40}'), ('S1', '[0-9a-f]{40}'), + ('F_RUN', '[1-9][0-9]*'), ('S1_RUN', '[1-9][0-9]*')]: + label = {'F_RUN': 'F workflow run', 'S1_RUN': 'S1 workflow run'}.get(field, field) + match = re.search('^' + label + ': (' + pattern + ')$', text, re.M) + if not match: + return False + names[field] = match.group(1) + return (names['F'] == freeze_id and names['S1'] == s1_id + and text == RESULT.format(**names)) + + +def failures(files, original, freeze, output, stderr, rc, required, freeze_id, s1_id): + errors = [] + rebuilt = expected(original) + for path, pin in META['pins'].items(): + wanted = rebuilt[path] if path in rebuilt else None + pinned_sha = pin['sha256'] + if path == ROADMAP and not required: + wanted = original[path] + pinned_sha = META['anchors'][ROADMAP] + actual = files.get(path, b'') + if sha(actual) != pinned_sha: + errors.append('pin:' + path) + if wanted is not None: + if actual != wanted: + errors.append(path) + module = files.get(MODULE, b'') + body = module.split(b'-/', 1)[1] if b'-/' in module else b'' + if sha(body) != META['body_sha256']: + errors.append('body') + if files.get(ROUND + 'preregistration.md') != freeze: + errors.append('freeze') + control_hash = re.search(rb'^Controls SHA256: ([0-9a-f]{64})$', freeze, re.M) + if (not control_hash or sha(files.get(ROUND + 'controls.py', b'')).encode() != control_hash.group(1)): + errors.append('controls') + population = {p[len(ROUND):] for p in files if p.startswith(ROUND)} + if population != {'preregistration.md', 'controls.py'} | ({'result.md'} if required else set()): + errors.append('population') + if rc or stderr or sha(output) != OUTPUT_SHA: + errors.append('measurement') + if required and not result_ok(files.get(ROUND + 'result.md', b''), freeze_id, s1_id): + errors.append('result') + return errors + + +def self_test(probe): + original = originals() + # Immutable blobs reconstruct the original execution, so later changes to shared + # aggregator/workflow/registry/roadmap cannot invalidate this round's fixture. + rebuilt = expected(original) + files = {p: rebuilt[p] if p in rebuilt else git('cat-file', 'blob', pin['blob']) + for p, pin in META['pins'].items()} + source = Path(probe).read_bytes() + if sha(source) != META['pins'][PROBE]['sha256']: + raise ValueError('live owned checker mismatch') + proc = subprocess.run([sys.executable, '-I', '-B', probe], capture_output=True) + control_bytes = Path(__file__).read_bytes() + freeze = ('fixture\nControls SHA256: ' + sha(control_bytes) + '\n').encode() + f, s1 = '1' * 40, '2' * 40 + files.update({ROUND+'preregistration.md': freeze, ROUND+'controls.py': control_bytes, + ROUND+'result.md': RESULT.format(F=f, S1=s1, F_RUN='1', S1_RUN='2').encode()}) + def run(values, required=True, out=proc.stdout, err=proc.stderr, rc=proc.returncode, freeze_id=f): + return failures(values, original, freeze, out, err, rc, required, freeze_id, s1) + if run(files): + raise ValueError('S2 fixture failed ' + str(run(files))) + s1_files = dict(files) + del s1_files[ROUND+'result.md'] + s1_files[ROADMAP] = original[ROADMAP] + if run(s1_files, False): + raise ValueError('S1 fixture failed') + mutations = 0 + for path in META['pins']: + changed = dict(files); changed[path] += b'changed\n' + if not run(changed): + raise ValueError('file mutation missed ' + path) + mutations += 1 + for path, value in [(ROUND+'preregistration.md', b'changed'), + (ROUND+'controls.py', b'changed'), + (ROUND+'extra', b'new'), + (ROUND+'result.md', files[ROUND+'result.md'] + b'OI implies QM.\n')]: + changed = dict(files); changed[path] = value + if not run(changed): + raise ValueError('record mutation missed ' + path) + mutations += 1 + for out, err, rc in [(b'PASS', b'', 0), (proc.stdout, b'error', 0), (proc.stdout, b'', 1)]: + if 'measurement' not in run(files, out=out, err=err, rc=rc): + raise ValueError('measurement mutation missed') + mutations += 1 + if 'result' not in run(files, freeze_id='3'*40): + raise ValueError('wrong F missed') + mutations += 1 + # A self-consistent reconstruction must still fail if its declared immutable + # pin is stale. Exercise metadata corruption, restoring scope after each check. + for path in [AGGREGATE, REGISTRY, WORKFLOW, ROADMAP]: + original_pin = META['pins'][path]['sha256'] + try: + META['pins'][path]['sha256'] = '0' * 64 + if 'pin:' + path not in run(files): + raise ValueError('stale shared pin missed ' + path) + finally: + META['pins'][path]['sha256'] = original_pin + mutations += 1 + original_roadmap_anchor = META['anchors'][ROADMAP] + try: + META['anchors'][ROADMAP] = '0' * 64 + if 'pin:' + ROADMAP not in run(s1_files, False): + raise ValueError('stale S1 roadmap anchor pin missed') + finally: + META['anchors'][ROADMAP] = original_roadmap_anchor + mutations += 1 + print(f'controls self-test: PASS; S1/S2 fixtures and {mutations} rejected mutations') + + +def check(head, freeze_id): + original = originals() + if git('diff', '--name-only', META['d'], freeze_id).decode().splitlines() != [ROUND+'preregistration.md']: + raise ValueError('D-to-F delta is not preregistration alone') + git('merge-base', '--is-ancestor', freeze_id, head) + commits = git('rev-list', '--reverse', head, '^'+freeze_id).decode().splitlines() + if not commits: + raise ValueError('execution is empty') + prior = freeze_id + allowed = set(META['pins']) | {ROUND+'controls.py', ROUND+'result.md'} + for commit in commits: + parents = git('show', '-s', '--format=%P', commit).decode().split() + if parents != [prior]: + raise ValueError('execution not linear') + changed = set(git('diff', '--name-only', prior, commit).decode().splitlines()) + if not changed <= allowed: + raise ValueError('changed path outside execution scope') + prior = commit + names = git('ls-tree', '-r', '--name-only', head, '--', ROUND).decode().splitlines() + files = {p: git('show', head+':'+p) for p in set(META['pins']) | set(names)} + fixed = git('show', freeze_id+':'+ROUND+'preregistration.md') + if Path(PROBE).read_bytes() != files[PROBE] or Path(__file__).read_bytes() != files[ROUND+'controls.py']: + raise ValueError('running sources differ from checked object') + proc = subprocess.run([sys.executable, '-I', '-B', PROBE], capture_output=True) + errors = failures(files, original, fixed, proc.stdout, proc.stderr, proc.returncode, + ROUND+'result.md' in files, freeze_id, commits[0]) + if errors: + raise ValueError('controls failed: '+','.join(errors)) + print('controls: PASS') + print(proc.stdout.decode(), end='') + + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('head', nargs='?') + parser.add_argument('--freeze') + parser.add_argument('--self-test', action='store_true') + parser.add_argument('--probe', default=PROBE) + args = parser.parse_args() + try: + if args.self_test: + self_test(args.probe) + elif args.head and args.freeze: + check(args.head, args.freeze) + else: + parser.error('head and --freeze, or --self-test, required') + except (ValueError, subprocess.CalledProcessError) as exc: + print(str(exc), file=sys.stderr) + sys.exit(1) diff --git a/verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/preregistration.md b/verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/preregistration.md new file mode 100644 index 000000000..2c46aabae --- /dev/null +++ b/verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/preregistration.md @@ -0,0 +1,220 @@ +# OI-FINITE-PROTOCOL-1 — finite stopped protocol from primitive resources + +Status: prospective native V3 draft. The owner requested finishing the open pull requests +and parallel threads on 2026-10-12. This authorizes preparation; it is not an exact-object +F or E designation. Execution starts only after the exact-head checks and owner F designation. + +```v3-round +round OI-FINITE-PROTOCOL-1 +kind non-sealing +record-directory verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/ +``` + +```v3-governed-paths +record AM verification/programmes/oi-qm/reconstruction/round-oi-finite-protocol-1/ +record AM verification/receipts/OI-FINITE-PROTOCOL-1.json +execution A verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean +execution A verification/lean/oi_finite_protocol_check.py +execution M verification/lean-mathlib/OIBridge.lean +execution M verification/lean-manuscript-census.json +execution M .github/workflows/verify.yml +execution M verification/ROADMAP.md +``` + +D: f2415108601a9c36bb985b3374c56f0eb34c2962. +The D-to-F delta contains control-plane files only. No manuscripts, historical design +records, shared kernel modules or other rounds' records are authorized for execution. + +## Prospective preparation budget and decision rules + +The historical #810 design budget is exhausted. Its measured head +708153423ffb5ea4fe27663654431650b5a2e48a supplies fourteen standard axiom reports. +This newly prospective preparation permits one predictive fresh-head CI run on a disposable +design branch containing exactly the predicted S1 executable tree, with D's roadmap and no result +note. It is additional disclosed design evidence and never an F/E attestation. Local exact +checks, replay and controlled fixture mutations are preparation controls, recorded separately. +A failed predictive run stops preparation for reassessment; no second run is silently licensed. +The predictive tree and all control files are fixed before dispatch. + +The productivity test is all-depth InstAvail constructed from primitive memberships, rather +than assumed availability of a whole approximation sequence. Preserve every byte after the +original Lean header and all fourteen named axiom reports. Change only the header to describe +conditional infrastructure. Adopt BridgeFiniteProtocol alone: its sole OIBridge import is +main's ImplementationLocality. No #807 repair or other historical design module is needed. + +The independent Gaussian-rational checker evaluates the actual uniform attachment, reset, +finite circuit, readout/correction and stopped loop. All ten groups must pass, with the three +countercontrols rejecting removal of reset, removal of correction and continuation after +success on the named 0,1 matrix unit. No computational verdict prints after a failed group. +Finite depths 0–8 are controls for the kernel's universal finite-depth theorem, not a proof +of that theorem. The predicted adoption adds a truthful kernel-only registry family and an +independently reconstructed CI shard with required-success aggregation. + +Primitive circuit/reset/correction memberships and the architecture projector premise stay +explicit. Spectator availability additionally assumes ContextStable and LabelInvariant. +No channel-limit availability, convergence theorem, arbitrary pair-cone preservation, +state/test identification, K2 closure, K_n reconstruction or full OI reconstruction is earned. + +## Invariant checkpoints + +| Invariant | Checkpoint | +|---|---| +| Actual uniformly attached ancilla is reset internally | reset_uniformAttach; ACTUAL-UNIFORM-RESET | +| Every finite depth is constructed by InstAvail rules | instAvail_attempt; instAvail_stopped; finite_protocol_available | +| Correct branch and stopped-loop formulas | attempt_balanced_branch; balanced_stopped_formula; exact branch/depth groups | +| Failures continue and success stops | stopped definition; CONTROL-CONTINUE-SUCCESS | +| Reset and correction are load-bearing | CONTROL-REMOVE-RESET; CONTROL-REMOVE-CORRECTION | +| Primitive and spectator premises remain explicit | preserved proof body; finite_protocol_spectator named report | +| Module depends only on existing main infrastructure | preserved imports; dependency source anchors; CI Build | +| No extra design modules are adopted | exact output population; path allowlist; manuscript census | +| Only standard axioms, no sorryAx | successful CI Build and fourteen named reports | +| Shared workflow/import/registry changes are only declared splices | independent byte reconstruction; mutations | +| Existing statuses and unrelated roadmap rows remain | unique K3 paragraph splice; exact reconstruction | +| Frozen control plane remains unchanged | exact F bytes; controls checksum; native V3 receipt | +| No finite evidence or availability becomes physical reconstruction | exact conditional result template | +| Local evidence is distinguished from host certification | design run metadata; F/E dispatch records; receipt | + +## Frozen outputs and independent reconstruction + +S1 adds the module, checker and controls, and changes only the aggregate import, +registry family and workflow splices. The roadmap stays at D. S2 adds the exact result +note and replaces only the K3 paragraph. No K2 paragraph, P1 summary row, K∞, K1, K_n +or H-Bell status is changed. The K3 label remains CONDITIONAL. + +| File | SHA256 | Git blob | +|---|---|---| +| S1 verification/lean-mathlib/OIBridge/BridgeFiniteProtocol.lean | d350d235b1b8b1379f9ea9dafcdb6be7a9f256f0eda96633ff119a7904c7cce4 | baf7a6d421597b115d588b824524e3bc38a946d6 | +| S1 verification/lean/oi_finite_protocol_check.py | 5a4f0862b953e4d07e201ecbe03291d0cfa6e6df615dd4b6f25f723052927839 | ef104005b47ef5323a2a937d5df3c7c993f972d4 | +| S1 verification/lean-mathlib/OIBridge.lean | db19e164d0843cddffa1e8a5f281911b0742e9f1b5dc794fc287333ddc75847a | 03a29e2fd41634103d6a274f3fb36056ed5b6826 | +| S1 verification/lean-manuscript-census.json | 0803c812cafeffbbbd7b211e5d9420ab3372f29ac31fe35655ad471192423aa9 | 88206432a44074cbd1bfb46fff1847d2dcb425f4 | +| S1 .github/workflows/verify.yml | 05020b877f667199f647ce50b00e446670e2e1fea37854e5a00972b879eb089d | c2203af2f9f668442561f02e6a936c736378d362 | +| S2 verification/ROADMAP.md | 971b868db5e81ca7eaad17dd1d39c97558a4553f3ddad9e16162bd65312af615 | ba7b23d4f1b0a2b78722dbc15b3fc51193f147d8 | + +Controls SHA256: fe801c75b554b798acdefa9efc64c7f39df83e30dbf6edf41fde061da10ef38c + +Preserved body SHA256: 016c8e724c73ae358fbcae3646c0b7e975beed3ddd8056d9197bf2f79a27b847 + +The proof body means every byte after the first header-closing -/, including all imports, +statements, proofs and fourteen #print axioms commands. The checker differs from the +historical measured checker only in its opening provenance sentence. Its mathematical +code is unchanged. The independent controls import neither Lean nor the checker. They +reconstruct the workflow's five splices, the aggregate's one import insertion, the +registry's single family append and the roadmap's unique K3 paragraph replacement +from D. Each output's declared SHA256 is checked alongside the independent +reconstruction. At S1 the roadmap is compared to the declared D anchor SHA256; at S2 it uses +the declared execution SHA256. The kernel-only family has manuscript=[] and lists +only BridgeFiniteProtocol. +No family or supersession that D already carries is changed. + +The controls hold the six D anchors below, preserve the module body, reject extra changed +paths and extra record files, require exact F bytes and controls checksum, measure linear +F-to-head ancestry, and bind the exact checker output. CI self-test reconstructs its +historical virtual fixtures from immutable Git blobs rather than the live shared workflow, +registry, aggregate or roadmap. Later rounds may change those shared files without +invalidating this self-test. The owned checker remains a live regression input. + +| D anchor | SHA256 | +|---|---| +| verification/lean-mathlib/OIBridge.lean | e5af9614009889dab616d7f02f75bb395f1ae1fb01307f46ef82d3b282b4c313 | +| verification/lean-manuscript-census.json | cdadb02e0463366c036834f2ca58ae904ad70e05dfe981fd1f37d9bc928e0bbf | +| .github/workflows/verify.yml | bd71bdc270753be8296c4a5c9723e23673c2f8acdaa9417fb70a6ddd6cbe2443 | +| verification/ROADMAP.md | a64835c2107131530f2396311b3e8fa291bc690462ffbbde225f3479d89a2c2c | +| verification/lean-mathlib/OIBridge/ImplementationLocality.lean | 4e5b4b22298dfba7b0ee7ba26109ef3090eb48b23227734bb26bbf6834a545ac | +| verification/lean-mathlib/OIBridge/OperationalValidity.lean | ba316747d23820f75f4bbd25105d87a85febb3bd1d0eaa123913b629b34f05f0 | + +## Sources and scope + +The actual uniformly attached ancilla, rather than an assumed pure seed, enters the +protocol. Architecture supplies the four-level projector rule. hCircuit, hReset and +hCorrect are explicit memberships in the ImplementationClass; its balanced matrix's +isometry is proved. Availability at every finite depth is constructed by induction and +bind/coarse/discard from those resources. The primitive memberships are not derived +for MixR {pi/4} by this round. + +ContextStable and LabelInvariant are explicit premises of the existing spectator rule. +I4.38 validity_of_implementationLocality and I4.66 CompositeOperationalValidity concern +PSD matrices at their carrier; they do not identify an arbitrary physical pair cone or +establish preservation of it. Identification with the whole PSD cone would already assert +the reconstruction target K=Q3. This package supplies no such identification or transfer. +No limit is taken. A later channel-limit route requires its own convergence, closedness +and arbitrary-cone transfer premises. Removing closedness from the distinct full-flow +maxCone theorem does not remove it from that later limit route. + +The corpus search at D located no BridgeFiniteProtocol or finite_protocol_available +identifier in papers or book. The truthful kernel-only disposition requires no invented +manuscript anchor; the only public status addition is the conditional K3 paragraph. + +## Exact earned result + +The controls.py RESULT literal is the complete result template. F and S1 are lower-case +40-hex object IDs, equal to the actual freeze and first execution child; F_RUN and S1_RUN +are positive workflow IDs. These four fields alone vary. The exact template states +conditional finite availability, the full explicit resource and spectator premises, +the finite controls' scope and every remaining physical/limit obligation. Appending any +extra affirmative claim fails template equality. Host event/head/conclusion/job results +are checked separately and recorded as attestations; local equality does not prove them. + +```text +# OI-FINITE-PROTOCOL-1 — finite stopped protocol from primitive resources + +Outcome: OI-FINITE-PROTOCOL-1-PROVED + +Every finite stopped-channel depth is InstAvail from Architecture and explicit circuit/reset/correction memberships, using the existing readout, op, bind, coarse and discard rules. The uniformly mixed ancilla is reset inside the protocol. The balanced circuit's corrected branches and all-depth stopped formula are proved for every input matrix. No available approximation sequence is a premise. + +Spectator availability additionally requires ContextStable and LabelInvariant. Primitive memberships, convergence, availability of a limiting drive, physical state/test identification and validity or preservation of an arbitrary pair cone remain separate obligations. K2 remains open, K3 remains conditional, and arbitrary finite-carrier reconstruction and the full operation/instrument correspondence retain their existing obligations. This package does not establish unconditional OI reconstruction or full-model independence. + +Exact controls: FINITE-PROTOCOL: PASS; 10 groups; 36 stopped matrix-unit cases +Arithmetic is in Q(i). Replay is byte-identical, stderr is empty and exit code is zero. Removing reset, removing correction and continuing after success each disagrees with the intended map on the 0,1 matrix unit. These finite controls do not prove the universal theorem. + +The adopted module is kernel-only and imports only existing main ImplementationLocality and Mathlib tactics. Its proof body is unchanged from the measured #810 design head 708153423ffb5ea4fe27663654431650b5a2e48a. Historical design measurements and new predictive evidence are recorded separately in the preregistration; neither is an F/E attestation. + +F: {F} +F workflow run: {F_RUN} +S1: {S1} +S1 workflow run: {S1_RUN} + +Successful Build and fourteen standard named axiom reports without sorryAx are required, alongside all-green exact-head host checks before E designation. Owner E designation and host attestations are recorded in the receipt. Local content controls do not certify host facts. +``` + +## Design evidence and execution sequence + +Historical #810 measured design: head 708153423ffb5ea4fe27663654431650b5a2e48a, +Build succeeded and fourteen named axiom reports used only standard axioms, without +sorryAx. The historical census failure reflects unadopted design modules, not a native +adoption or a failed finite-availability theorem. Its earlier failed runs remain historical +and are not rewritten. This native successor adopts no unrelated historical module. + +The local preparation checkpoint 5152a959 carried the preregistration alone before the +new local checks. The published prospective control-plane checkpoint is +07a09570ff343aec73e12e1aae991b2290de840b, committed before the predictive CI run. +Neither checkpoint is an owner F designation. The exact checker must replay byte-for-byte to +SHA256 f33e3c97bd1baa7f4b583f798cf0ecdec185860d37f69523f31128e4131d35e1, +with empty stderr and exit zero. Its final line is: +FINITE-PROTOCOL: PASS; 10 groups; 36 stopped matrix-unit cases + +Local preparation: the independent controls pass S1/S2 fixtures and reject nineteen +mutations, including every output file, record files/population, result overclaim, wrong F, +altered stdout/stderr/exit, and stale declared SHA256 pins on all four shared +outputs and S1's D roadmap anchor pin. The stale-pin tests restore each original metadata +pin after probing it. Python compilation and artifact placement pass. The corpus +search reports zero occurrences of the five new kernel identifiers across papers and book. +Predictive CI results will be recorded here during drafting. +No predictive run or local check is an F/E attestation. + +1. Fix the predicted executable tree and controls, publish it only as disposable design, + and complete the one newly budgeted predictive CI run. Preserve the tested head, run, + actual Build result and all fourteen named axiom reports. A failed run stops preparation. +2. Hold the control-plane-only PR at its proposed F. Dispatch verify.yml on that exact + head; all jobs must be green before the owner designates F. +3. S1 is one single-parent child of F adding the frozen files and controls, with D's roadmap. + Run controls HEAD --freeze F, self-test and CI. Build must succeed with fourteen standard + named reports, no sorryAx, a passing manuscript census and passing complete release gate. +4. S2 adds only the exact result and roadmap splice. Run controls, hold the proposed E, + obtain its all-green exact-head workflow_dispatch run and owner E designation. +5. Reconcile after E under S9, resolving shared files by the merits and ownership of each + insertion or paragraph. Compare the landing to the execution's own diff. Build receipt-only + Q, require v3_verifier --verify-round Q to print VERDICT HOLDS, then complete ordinary + review and the owner's landing authorization. PR merge checks do not attest F or E. + +Any failed frozen checkpoint halts under S12; the immutable control plane is not repaired +in execution. A halted outcome still requires its result, reconciliation and valid receipt.