Design: replace pair self-duality with maxCone and cone closure

.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_oimaxcone:
+    name: Numerical probes / OI pair maxCone
+    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 maxCone and cone controls
+        run: python3 -I -B verification/lean/oi_maxcone_check.py
+      - name: Native control mutation tests
+        run: python3 -I -B verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-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_oimaxcone, 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 }}
+          OIMAXCONE_RESULT: ${{ needs.probes_oimaxcone.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 "oimaxcone=${OIMAXCONE_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 "${OIMAXCONE_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,21 @@
       "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": "conditional pair-cone reconstruction using exact block generation, explicit cone closure and product-test positivity (round OI-PAIR-MAXCONE-1)",
+      "modules": [
+        "EqvK2Schema",
+        "EqvK2Converse",
+        "EqvK2Block",
+        "EqvK2Generation",
+        "BridgeDictionary",
+        "BridgeConverge",
+        "EqvK2MaxCone"
+      ],
+      "status": "kernel-only",
+      "manuscript": [],
+      "note": "Conditional pair-level infrastructure on W 3. EqvK2MaxCone.subset_Q3_of_maxCone_block uses maxCone and block invariance for the upper inclusion; Q3_subset_of_products_cone_block uses products, addition, nonnegative scaling and block invariance for the lower. pairCone_eq_Q3_of_drive_maxCone assembles equality using E19's exact CNOT/full-flow/cyclic generation. The two block and generator equivalences have separately named witnesses. pairCone_eq_Q3_of_sharp_available obtains the upper bound from product-test validity on an available family containing sharpFamily 3; it assumes neither full affine effect availability nor EffectsOn in that direction. Self-duality, closedness and assumed ReachPure are absent from the replacement headlines. The six auxiliary modules supply the measured dictionary, generation, reachability and conditional transfer identities. This family is carried by no manuscript. The state/test identification, products and cone structure, pair validity, CNOT invariance and the full-flow/cyclic invariance remain explicit premises; no bare OI source, arbitrary finite-carrier reconstruction or full-model independence is asserted. Record: verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/."
     }
   ]
 }

verification/lean-mathlib/OIBridge.lean

@@ -264,6 +264,7 @@ import OIBridge.RelcSelectParity
 import OIBridge.RelcSelectBlock
 import OIBridge.RelcSelectSqueeze
 import OIBridge.RelcSelectC5
+import OIBridge.EqvK2MaxCone
 
 namespace OIBridge
 

verification/lean-mathlib/OIBridge/BridgeConverge.lean

@@ -0,0 +1,209 @@
+/-
+  OIBridge/BridgeConverge.lean — conditional pair-cone infrastructure (OI-PAIR-MAXCONE-1).
+
+  Compatibility of the two dictionaries and the conditional transfer maps.
+
+  The hypotheses retain their stated scope. The physical realization of the pair carrier,
+  its product tests and its operation-preserving action has separate source obligations.
+  Proof bodies follow the measured E19 and MaxCone design sources.
+-/
+import OIBridge.BridgeDictionary
+import OIBridge.EqvK2Schema
+import OIBridge.SubstratumInterfaceAudit
+import OIBridge.SpectatorBridge
+
+namespace OIBridge
+namespace BridgeConverge
+
+open CompositeDimension MonoidalCompletion InterventionLocality StructuralClosure
+  SubstratumInterfaceAudit
+open scoped ComplexOrder Matrix
+
+/-! ### §A — one dictionary -/
+
+/-- **THE TWO THREADS' PAULI MATRICES ARE THE SAME.** -/
+theorem pauli_converge : BridgeDictionary.pauli = EqvK2Schema.pauli := rfl
+
+/-- **THE TWO THREADS' ONE-TOKEN MAPS ARE THE SAME.** -/
+theorem tokMat_converge : BridgeDictionary.tokMat = EqvK2Schema.tokMat := rfl
+
+/-- **THE TWO THREADS' DICTIONARIES ARE ONE MAP.** -/
+theorem dict_converge : BridgeDictionary.dict = EqvK2Schema.dict := rfl
+
+/-- The bridge's dictionary is injective (the equivalence thread's `dict_injective`). -/
+theorem dict_injective : Function.Injective BridgeDictionary.dict := by
+  rw [dict_converge]
+  exact EqvK2Schema.dict_injective
+
+/-- The bridge's dictionary takes Hermitian values. -/
+theorem dict_isHermitian (ω : W 3) : (BridgeDictionary.dict ω).IsHermitian := by
+  rw [dict_converge]
+  exact EqvK2Schema.dict_isHermitian ω
+
+/-- The bridge's dictionary is the equivalence thread's linear equivalence `dictEquiv` onto the
+Hermitian matrices. -/
+theorem dictEquiv_eq (ω : W 3) :
+    (EqvK2Schema.dictEquiv ω : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) =
+      BridgeDictionary.dict ω := by
+  rw [EqvK2Schema.dictEquiv_apply, dict_converge]
+
+/-! ### §B — the transfer clause in table form -/
+
+/-- **THE TRANSFERRED TABLE**: the table whose dictionary image is the conjugate of `dict ω` by the
+idle extension `1 ⊗ U` (read back through the equivalence thread's coordinates). -/
+noncomputable def transferMap (U : Matrix (Fin 2) (Fin 2) ℂ) (ω : W 3) : W 3 :=
+  EqvK2Schema.coordOf (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U * BridgeDictionary.dict ω *
+    (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U)ᴴ)
+
+/-- The dictionary image of the transferred table. -/
+theorem dict_transferMap (U : Matrix (Fin 2) (Fin 2) ℂ) (ω : W 3) :
+    BridgeDictionary.dict (transferMap U ω) =
+      tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U * BridgeDictionary.dict ω *
+        (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U)ᴴ := by
+  have hH := Matrix.isHermitian_mul_mul_conjTranspose
+    (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U) (dict_isHermitian ω)
+  unfold transferMap
+  rw [dict_converge] at hH ⊢
+  exact EqvK2Schema.dict_coordOf _ hH
+
+/-- **THE TRANSFER CLAUSE IN TABLE FORM**: it holds exactly when the pair cone is invariant under the
+transferred tables of every admissible unitary. -/
+theorem transferClause_iff (𝓘 : ImplementationClass) (K : Set (W 3)) :
+    BridgeDictionary.TransferClause 𝓘 K ↔
+      ∀ U : Matrix (Fin 2) (Fin 2) ℂ, 𝓘 (Fin 2) U → Uᴴ * U = 1 → ∀ ω ∈ K, transferMap U ω ∈ K := by
+  constructor
+  · intro hT U hU hu ω hω
+    obtain ⟨ω', hω', heq⟩ := hT U hU hu ω hω
+    have h' : ω' = transferMap U ω := dict_injective (heq.trans (dict_transferMap U ω).symm)
+    rw [← h']
+    exact hω'
+  · intro h U hU hu ω hω
+    exact ⟨transferMap U ω, h U hU hu ω hω, dict_transferMap U ω⟩
+
+/-- The clause is antitone in the class: a larger class gives a stronger clause. -/
+theorem transferClause_mono {𝓘 𝓙 : ImplementationClass}
+    (h𝓘 : ∀ (S : Type) [Fintype S] [DecidableEq S] (M : Matrix S S ℂ), 𝓘 S M → 𝓙 S M)
+    {K : Set (W 3)} (hT : BridgeDictionary.TransferClause 𝓙 K) :
+    BridgeDictionary.TransferClause 𝓘 K :=
+  fun U hU hu ω hω => hT U (h𝓘 (Fin 2) U hU) hu ω hω
+
+/-! ### §C — (b) for the phase circle, in table form -/
+
+/-- **(b) FOR THE PHASE CIRCLE, IN TABLE FORM**: on a pair cone satisfying the transfer clause for
+the monomial class, every target rotation about the third axis by a point of the unit circle maps
+the cone into itself. -/
+theorem transfer_phase_table {K : Set (W 3)}
+    (hT : BridgeDictionary.TransferClause substratumClass K) (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1)
+    {ω : W 3} (hω : ω ∈ K) : actT (BridgeDictionary.rotZ c s) ω ∈ K := by
+  obtain ⟨ω', hω', heq⟩ := BridgeDictionary.transfer_phase hT c s h hω
+  rw [← dict_injective heq]
+  exact hω'
+
+/-- The flow form: the kernel's rotation `rotLin t` on the target, for every `t`. -/
+theorem transfer_flow_table {K : Set (W 3)}
+    (hT : BridgeDictionary.TransferClause substratumClass K) (t : ℝ) {ω : W 3} (hω : ω ∈ K) :
+    actT (KInfFoundations.rotLin t) ω ∈ K := by
+  rw [← BridgeDictionary.rotZ_cos_sin t]
+  exact transfer_phase_table hT _ _ (Real.cos_sq_add_sin_sq (x := t)) hω
+
+/-- The 3-4-5 point: `R_z(θ₀)` on the target, `cos θ₀ = 3/5`. -/
+theorem transfer_345_table {K : Set (W 3)}
+    (hT : BridgeDictionary.TransferClause substratumClass K) {ω : W 3} (hω : ω ∈ K) :
+    actT (BridgeDictionary.rotZ (3 / 5) (4 / 5)) ω ∈ K :=
+  transfer_phase_table hT _ _ (by norm_num) hω
+
+/-- The bridge's `X` is the permutation matrix of the exchange. -/
+theorem pauli1_eq_perm :
+    BridgeDictionary.pauli 1 = CoherentLift.permMatrix (Equiv.swap (0 : Fin 2) 1) := by
+  ext i j
+  fin_cases i <;> fin_cases j <;>
+    first
+    | rfl
+    | simp [BridgeDictionary.pauli, CoherentLift.permMatrix]
+
+theorem pauli1_permClass : permClass (Fin 2) (BridgeDictionary.pauli 1) := by
+  rw [pauli1_eq_perm]
+  exact permClass_permMatrix _
+
+theorem pauli1_unitary : (BridgeDictionary.pauli 1)ᴴ * BridgeDictionary.pauli 1 = 1 := by
+  rw [pauli1_eq_perm]
+  exact SpectatorBridge.permMatrix_isometry _
+
+/-- **THE NOT FROM THE CLAUSE FOR THE STATED ACCESS**, in table form. -/
+theorem transfer_nflip_table {K : Set (W 3)}
+    (hT : BridgeDictionary.TransferClause permClass K) {ω : W 3} (hω : ω ∈ K) :
+    actT nflip ω ∈ K := by
+  obtain ⟨ω', hω', heq⟩ := hT (BridgeDictionary.pauli 1) pauli1_permClass pauli1_unitary ω hω
+  have h2 : BridgeDictionary.dict ω' = BridgeDictionary.dict (actT nflip ω) :=
+    heq.trans (BridgeDictionary.dict_actT_nflip ω).symm
+  rw [← dict_injective h2]
+  exact hω'
+
+/-- The NOT from the clause for the monomial class. -/
+theorem transfer_nflip_of_substratum {K : Set (W 3)}
+    (hT : BridgeDictionary.TransferClause substratumClass K) {ω : W 3} (hω : ω ∈ K) :
+    actT nflip ω ∈ K :=
+  transfer_nflip_table (transferClause_mono (fun _ _ _ M h => permClass_le_substratum M h) hT) hω
+
+/-! ### §D — controls -/
+
+/-- **POSITIVE CONTROL**: `Q3`, the tables with positive semidefinite dictionary image, satisfies the
+transfer clause for every class. -/
+theorem transferClause_Q3 (𝓘 : ImplementationClass) :
+    BridgeDictionary.TransferClause 𝓘 EqvK2Schema.Q3 := by
+  intro U _ _ ω hω
+  refine ⟨transferMap U ω, ?_, dict_transferMap U ω⟩
+  have hω' : (EqvK2Schema.dict ω).PosSemidef := hω
+  have key : (EqvK2Schema.dict (transferMap U ω)).PosSemidef := by
+    rw [← dict_converge, dict_transferMap, dict_converge]
+    exact hω'.mul_mul_conjTranspose_same _
+  exact key
+
+/-- The table form holds non-vacuously: `Q3` is invariant under every target rotation of the phase
+circle. -/
+theorem Q3_phase_invariant (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) {ω : W 3}
+    (hω : ω ∈ EqvK2Schema.Q3) : actT (BridgeDictionary.rotZ c s) ω ∈ EqvK2Schema.Q3 :=
+  transfer_phase_table (transferClause_Q3 substratumClass) c s h hω
+
+/-- The elementary table with a single `1` at `(0, 1)`. -/
+def e01 : W 3 := fun μ ν => if μ = 0 ∧ ν = 1 then 1 else 0
+
+/-- The quarter-turn of the target moves `e01`. -/
+theorem e01_moved : actT (BridgeDictionary.rotZ 0 1) e01 ≠ e01 := by
+  intro h
+  have h1 := congrFun (congrFun h 0) 1
+  rw [actT_apply, BridgeDictionary.homMap_rotZ_one] at h1
+  simp [e01] at h1
+
+/-- **COUNTERCONTROL**: the one-table set `{e01}` fails the conclusion of the table form, hence the
+clause; the hypothesis is load-bearing. -/
+theorem transfer_counter :
+    ¬ BridgeDictionary.TransferClause substratumClass ({e01} : Set (W 3)) := by
+  intro hT
+  exact e01_moved (Set.mem_singleton_iff.mp
+    (transfer_phase_table hT 0 1 (by norm_num) (Set.mem_singleton e01)))
+
+#print axioms pauli_converge
+#print axioms tokMat_converge
+#print axioms dict_converge
+#print axioms dict_injective
+#print axioms dict_isHermitian
+#print axioms dictEquiv_eq
+#print axioms dict_transferMap
+#print axioms transferClause_iff
+#print axioms transferClause_mono
+#print axioms transfer_phase_table
+#print axioms transfer_flow_table
+#print axioms transfer_345_table
+#print axioms pauli1_eq_perm
+#print axioms pauli1_permClass
+#print axioms pauli1_unitary
+#print axioms transfer_nflip_table
+#print axioms transfer_nflip_of_substratum
+#print axioms transferClause_Q3
+#print axioms Q3_phase_invariant
+#print axioms e01_moved
+#print axioms transfer_counter
+
+end BridgeConverge
+end OIBridge