Design: validate minimal OI-FINITE-PROTOCOL-1 adoption

.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

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."
     }
   ]
 }

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