diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index 4cd48e87e..7c85970db 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_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 diff --git a/verification/lean-manuscript-census.json b/verification/lean-manuscript-census.json index 1bc4d1f1c..dd59b8938 100644 --- a/verification/lean-manuscript-census.json +++ b/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/." } ] } diff --git a/verification/lean-mathlib/OIBridge.lean b/verification/lean-mathlib/OIBridge.lean index f3b6b201c..281b6a524 100644 --- a/verification/lean-mathlib/OIBridge.lean +++ b/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 diff --git a/verification/lean-mathlib/OIBridge/BridgeConverge.lean b/verification/lean-mathlib/OIBridge/BridgeConverge.lean new file mode 100644 index 000000000..e1647b1dc --- /dev/null +++ b/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 diff --git a/verification/lean-mathlib/OIBridge/BridgeDictionary.lean b/verification/lean-mathlib/OIBridge/BridgeDictionary.lean new file mode 100644 index 000000000..f997b33ec --- /dev/null +++ b/verification/lean-mathlib/OIBridge/BridgeDictionary.lean @@ -0,0 +1,386 @@ +/- + OIBridge/BridgeDictionary.lean — conditional pair-cone infrastructure (OI-PAIR-MAXCONE-1). + + Dictionary identities and explicitly introduced operation-transfer interfaces. + + 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.CompositeDimension +import OIBridge.MonoidalCompletion +import OIBridge.ImplementationLocality +import OIBridge.StructuralClosure +import Mathlib.LinearAlgebra.Matrix.Kronecker +import Mathlib.Tactic.LinearCombination +import Mathlib.Tactic.Module + +namespace OIBridge +namespace BridgeDictionary + +open CompositeDimension MonoidalCompletion InterventionLocality StructuralClosure KInfFoundations +open SubstratumInterface Matrix +open scoped Kronecker + +/-! ### The dictionary -/ + +/-- The Pauli matrices `σ₀ = 1, σ₁ = X, σ₂ = Y, σ₃ = Z`. -/ +noncomputable def pauli : Fin 4 → Matrix (Fin 2) (Fin 2) ℂ := + ![1, !![0, 1; 1, 0], !![0, -Complex.I; Complex.I, 0], !![1, 0; 0, -1]] + +/-- One token's homogenized vector as a 2 × 2 complex matrix: `v ↦ ½ Σ v_μ σ_μ`. -/ +noncomputable def tokMat (v : HVec 3) : Matrix (Fin 2) (Fin 2) ℂ := + ∑ μ : Fin 4, ((v μ : ℂ) / 2) • pauli μ + +/-- The two-token dictionary: `ω ↦ ¼ Σ ω_μν σ_μ ⊗ σ_ν`. -/ +noncomputable def dict (ω : W 3) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ := + ∑ μ : Fin 4, ∑ ν : Fin 4, ((ω μ ν : ℂ) / 4) • tensorOf (pauli μ) (pauli ν) + +/-- The kernel's tensor is Mathlib's Kronecker product. -/ +theorem tensorOf_eq_kron (XA XB : Matrix (Fin 2) (Fin 2) ℂ) : tensorOf XA XB = XA ⊗ₖ XB := rfl + +/-! ### §A — (D1) the product law -/ + +/-- **The product law of the dictionary.** -/ +theorem dict_tens (X Y : HVec 3) : dict (tens X Y) = tensorOf (tokMat X) (tokMat Y) := by + ext ⟨i, j⟩ ⟨k, l⟩ + simp only [dict, tokMat, tens_apply, Matrix.sum_apply, Matrix.smul_apply, tensorOf_apply, + smul_eq_mul, Complex.ofReal_mul] + simp only [Fin.sum_univ_four] + ring + +/-- The product states of the ball go to Kronecker products of one-token matrices. -/ +theorem dict_prodState (x y : Fin 3 → ℝ) : + dict (prodState x y) = tensorOf (tokMat (hom x)) (tokMat (hom y)) := + dict_tens (hom x) (hom y) + +/-! ### §B — (D2) the gate -/ + +/-- The projector `|0⟩⟨0|`. -/ +noncomputable def projZero : Matrix (Fin 2) (Fin 2) ℂ := Matrix.diagonal ![1, 0] + +/-- The projector `|1⟩⟨1|`. -/ +noncomputable def projOne : Matrix (Fin 2) (Fin 2) ℂ := Matrix.diagonal ![0, 1] + +/-- The controlled NOT on `ℂ² ⊗ ℂ²`, control first: `|0⟩⟨0| ⊗ 1 + |1⟩⟨1| ⊗ X`. -/ +noncomputable def cnotMat : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ := + tensorOf projZero 1 + tensorOf projOne (pauli 1) + +set_option maxHeartbeats 8000000 in +/-- **(D2), the gate.** The kernel's `d = 3` gate is conjugation by the controlled NOT. -/ +theorem dict_cnot (ω : W 3) : dict (cnot ω) = cnotMat * dict ω * cnotMat := by + ext ⟨i, j⟩ ⟨k, l⟩ + fin_cases i <;> fin_cases j <;> fin_cases k <;> fin_cases l <;> + simp only [dict, cnotMat, Matrix.mul_apply, Fintype.sum_prod_type, Fin.sum_univ_two, + Fin.sum_univ_four, Matrix.sum_apply, Matrix.add_apply, Matrix.smul_apply, smul_eq_mul, + tensorOf_apply] <;> + simp +decide [cnot_apply, cnotFun, cnotFun_apply, sgn, pc, pt, pauli, projZero, projOne, + Matrix.one_apply, Matrix.diagonal_apply] <;> + ring + +/-! ### §C — (D2) the monomial images -/ + +/-- The rotation of the ball by `(c, s)` about the third axis. -/ +def rotZ (c s : ℝ) : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ) where + toFun x := ![c * x 0 - s * x 1, s * x 0 + c * x 1, x 2] + map_add' x y := by + first + | (apply vec3_ext <;> simp <;> ring1) + | (funext m; fin_cases m <;> simp <;> ring1) + map_smul' r x := by + first + | (apply vec3_ext <;> simp <;> ring1) + | (funext m; fin_cases m <;> simp <;> ring1) + +/-- At `(cos t, sin t)` it is the kernel's rotation `rotLin t` (the flow of `ball3Drive`). -/ +theorem rotZ_cos_sin (t : ℝ) : rotZ (Real.cos t) (Real.sin t) = rotLin t := by + apply LinearMap.ext + intro x + apply vec3_ext <;> first | rfl | simp [rotZ, rotLin, rotFun] + +theorem homMap_rotZ_zero (c s : ℝ) (v : HVec 3) : + homMap (rotZ c s) v (0 : Fin 4) = v (0 : Fin 4) := by + first | rfl | simp [homMap, rotZ] + +theorem homMap_rotZ_one (c s : ℝ) (v : HVec 3) : + homMap (rotZ c s) v (1 : Fin 4) = c * v (1 : Fin 4) - s * v (2 : Fin 4) := by + first | rfl | (simp [homMap, rotZ, Matrix.vecTail] <;> ring1) + +theorem homMap_rotZ_two (c s : ℝ) (v : HVec 3) : + homMap (rotZ c s) v (2 : Fin 4) = s * v (1 : Fin 4) + c * v (2 : Fin 4) := by + first | rfl | (simp [homMap, rotZ, Matrix.vecTail] <;> ring1) + +theorem homMap_rotZ_three (c s : ℝ) (v : HVec 3) : + homMap (rotZ c s) v (3 : Fin 4) = v (3 : Fin 4) := by + first | rfl | simp [homMap, rotZ, Matrix.vecTail] + +theorem homMap_nflip_zero' (v : HVec 3) : homMap nflip v (0 : Fin 4) = v (0 : Fin 4) := by + first | rfl | exact homMap_nflip_zero v + +theorem homMap_nflip_one' (v : HVec 3) : homMap nflip v (1 : Fin 4) = v (1 : Fin 4) := by + first | exact homMap_nflip_one v | (show 1 * v 1 = v 1; ring1) + +theorem homMap_nflip_two' (v : HVec 3) : homMap nflip v (2 : Fin 4) = -v (2 : Fin 4) := by + first | exact homMap_nflip_two v | (show -1 * v 2 = -v 2; ring1) + +theorem homMap_nflip_three' (v : HVec 3) : homMap nflip v (3 : Fin 4) = -v (3 : Fin 4) := by + first | exact homMap_nflip_three v | (show -1 * v 3 = -v 3; ring1) + +/-- The phase `diag(1, c + i s)`: a monomial one-token operator, unitary on the unit circle. -/ +noncomputable def zPhase (c s : ℝ) : Matrix (Fin 2) (Fin 2) ℂ := + Matrix.diagonal ![1, (c : ℂ) + (s : ℂ) * Complex.I] + +/-- The adjoint of `zPhase c s`, written out. -/ +noncomputable def zPhaseD (c s : ℝ) : Matrix (Fin 2) (Fin 2) ℂ := + Matrix.diagonal ![1, (c : ℂ) - (s : ℂ) * Complex.I] + +theorem zPhase_conjTranspose (c s : ℝ) : (zPhase c s)ᴴ = zPhaseD c s := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [zPhase, zPhaseD, Matrix.conjTranspose_apply, Matrix.diagonal_apply] <;> ring1 + +/-- `σ₀` under the phase: fixed exactly on the unit circle. -/ +theorem zPhase_pauli0 (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) : + zPhase c s * pauli 0 * (zPhase c s)ᴴ = pauli 0 := by + have hc : (c : ℂ) ^ 2 + (s : ℂ) ^ 2 = 1 := by exact_mod_cast h + rw [zPhase_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [zPhase, zPhaseD, pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.diagonal_apply, + Matrix.one_apply] <;> + first + | ring1 + | linear_combination hc - (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination -hc + (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination hc + | linear_combination -hc + | linear_combination hc + (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination -hc - (s : ℂ) ^ 2 * Complex.I_sq + +/-- `σ₁` under the phase: `c σ₁ + s σ₂` (no circle needed). -/ +theorem zPhase_pauli1 (c s : ℝ) : + zPhase c s * pauli 1 * (zPhase c s)ᴴ = (c : ℂ) • pauli 1 + (s : ℂ) • pauli 2 := by + rw [zPhase_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [zPhase, zPhaseD, pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.diagonal_apply] <;> + first + | ring1 + | linear_combination (s : ℂ) * Complex.I_sq + | linear_combination -(s : ℂ) * Complex.I_sq + | linear_combination (c : ℂ) * Complex.I_sq + | linear_combination -(c : ℂ) * Complex.I_sq + +/-- `σ₂` under the phase: `−s σ₁ + c σ₂` (no circle needed). -/ +theorem zPhase_pauli2 (c s : ℝ) : + zPhase c s * pauli 2 * (zPhase c s)ᴴ = (-(s : ℂ)) • pauli 1 + (c : ℂ) • pauli 2 := by + rw [zPhase_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [zPhase, zPhaseD, pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.diagonal_apply] <;> + first + | ring1 + | linear_combination (s : ℂ) * Complex.I_sq + | linear_combination -(s : ℂ) * Complex.I_sq + | linear_combination (c : ℂ) * Complex.I_sq + | linear_combination -(c : ℂ) * Complex.I_sq + +/-- `σ₃` under the phase: fixed exactly on the unit circle. -/ +theorem zPhase_pauli3 (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) : + zPhase c s * pauli 3 * (zPhase c s)ᴴ = pauli 3 := by + have hc : (c : ℂ) ^ 2 + (s : ℂ) ^ 2 = 1 := by exact_mod_cast h + rw [zPhase_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [zPhase, zPhaseD, pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.diagonal_apply] <;> + first + | ring1 + | linear_combination hc - (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination -hc + (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination hc + | linear_combination -hc + | linear_combination hc + (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination -hc - (s : ℂ) ^ 2 * Complex.I_sq + +/-- The NOT `X = σ₁` on the four Pauli matrices: `σ₀, σ₁` fixed, `σ₂, σ₃` negated. -/ +theorem x_pauli0 : pauli 1 * pauli 0 * (pauli 1)ᴴ = pauli 0 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.conjTranspose_apply, + Matrix.one_apply] <;> first | rfl | ring1 + +theorem x_pauli1 : pauli 1 * pauli 1 * (pauli 1)ᴴ = pauli 1 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.conjTranspose_apply] <;> + first | rfl | ring1 + +theorem x_pauli2 : pauli 1 * pauli 2 * (pauli 1)ᴴ = (-1 : ℂ) • pauli 2 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.conjTranspose_apply] <;> + first | rfl | ring1 + +theorem x_pauli3 : pauli 1 * pauli 3 * (pauli 1)ᴴ = (-1 : ℂ) • pauli 3 := by + ext i j + fin_cases i <;> fin_cases j <;> + simp [pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.conjTranspose_apply] <;> + first | rfl | ring1 + +/-- **Conjugation by an idle extension on the target, term by term.** -/ +theorem conj_dict_right (U : Matrix (Fin 2) (Fin 2) ℂ) (ω : W 3) : + tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U * dict ω * + (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U)ᴴ = + ∑ μ : Fin 4, ∑ ν : Fin 4, ((ω μ ν : ℂ) / 4) • tensorOf (pauli μ) (U * pauli ν * Uᴴ) := by + simp only [dict, tensorOf_eq_kron, Finset.mul_sum, Finset.sum_mul, Matrix.mul_smul, + Matrix.smul_mul, Matrix.conjTranspose_kronecker, Matrix.conjTranspose_one, + ← Matrix.mul_kronecker_mul, Matrix.one_mul, Matrix.mul_one] + +/-- **Conjugation by an idle extension on the control, term by term.** -/ +theorem conj_dict_left (U : Matrix (Fin 2) (Fin 2) ℂ) (ω : W 3) : + tensorOf U (1 : Matrix (Fin 2) (Fin 2) ℂ) * dict ω * + (tensorOf U (1 : Matrix (Fin 2) (Fin 2) ℂ))ᴴ = + ∑ μ : Fin 4, ∑ ν : Fin 4, ((ω μ ν : ℂ) / 4) • tensorOf (U * pauli μ * Uᴴ) (pauli ν) := by + simp only [dict, tensorOf_eq_kron, Finset.mul_sum, Finset.sum_mul, Matrix.mul_smul, + Matrix.smul_mul, Matrix.conjTranspose_kronecker, Matrix.conjTranspose_one, + ← Matrix.mul_kronecker_mul, Matrix.one_mul, Matrix.mul_one] + +set_option maxHeartbeats 4000000 in +/-- **(D2), the phase rotation on the target.** On the unit circle, the target action of the +rotation about the third axis is conjugation by the idle extension `1 ⊗ diag(1, c + i s)`. -/ +theorem dict_actT_rotZ (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) (ω : W 3) : + dict (actT (rotZ c s) ω) = + tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) (zPhase c s) * dict ω * + (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) (zPhase c s))ᴴ := by + rw [conj_dict_right] + simp only [dict, Fin.sum_univ_four, actT, homMap_rotZ_zero, homMap_rotZ_one, homMap_rotZ_two, + homMap_rotZ_three, zPhase_pauli0 c s h, zPhase_pauli1, zPhase_pauli2, zPhase_pauli3 c s h, + tensorOf_eq_kron, Matrix.kronecker_add, Matrix.kronecker_smul, Complex.ofReal_sub, + Complex.ofReal_add, Complex.ofReal_mul] + module + +set_option maxHeartbeats 4000000 in +/-- **(D2), the phase rotation on the control.** -/ +theorem dict_actC_rotZ (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) (ω : W 3) : + dict (actC (rotZ c s) ω) = + tensorOf (zPhase c s) (1 : Matrix (Fin 2) (Fin 2) ℂ) * dict ω * + (tensorOf (zPhase c s) (1 : Matrix (Fin 2) (Fin 2) ℂ))ᴴ := by + rw [conj_dict_left] + simp only [dict, Fin.sum_univ_four, actC, homMap_rotZ_zero, homMap_rotZ_one, homMap_rotZ_two, + homMap_rotZ_three, zPhase_pauli0 c s h, zPhase_pauli1, zPhase_pauli2, zPhase_pauli3 c s h, + tensorOf_eq_kron, Matrix.add_kronecker, Matrix.smul_kronecker, Complex.ofReal_sub, + Complex.ofReal_add, Complex.ofReal_mul] + module + +set_option maxHeartbeats 4000000 in +/-- **(D2), the NOT on the target.** -/ +theorem dict_actT_nflip (ω : W 3) : + dict (actT nflip ω) = + tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) (pauli 1) * dict ω * + (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) (pauli 1))ᴴ := by + rw [conj_dict_right] + simp only [dict, Fin.sum_univ_four, actT, homMap_nflip_zero', homMap_nflip_one', + homMap_nflip_two', homMap_nflip_three', x_pauli0, x_pauli1, x_pauli2, x_pauli3, + tensorOf_eq_kron, Matrix.kronecker_smul, Complex.ofReal_neg] + module + +set_option maxHeartbeats 4000000 in +/-- **(D2), the NOT on the control.** -/ +theorem dict_actC_nflip (ω : W 3) : + dict (actC nflip ω) = + tensorOf (pauli 1) (1 : Matrix (Fin 2) (Fin 2) ℂ) * dict ω * + (tensorOf (pauli 1) (1 : Matrix (Fin 2) (Fin 2) ℂ))ᴴ := by + rw [conj_dict_left] + simp only [dict, Fin.sum_univ_four, actC, homMap_nflip_zero', homMap_nflip_one', + homMap_nflip_two', homMap_nflip_three', x_pauli0, x_pauli1, x_pauli2, x_pauli3, + tensorOf_eq_kron, Matrix.smul_kronecker, Complex.ofReal_neg] + module + +/-! ### §D — the certified context stability at the pair carrier, and the transfer clause -/ + +/-- **The certified spectator theorem at the pair carrier**: the idle extension of a monomial +one-token operator is admissible on `Fin 2 × Fin 2` (`substratumClass_contextStable`). -/ +theorem monomial_extension_admissible (U : Matrix (Fin 2) (Fin 2) ℂ) + (hU : substratumClass (Fin 2) U) : + substratumClass (Fin 2 × Fin 2) (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U) := + substratumClass_contextStable (Fin 2) (Fin 2) U hU + +/-- **The M→P transfer clause** (a design statement, not a premise of anything here): for every +admissible unitary `U` on one token and every `ω ∈ K`, conjugation of `dict ω` by the idle +extension `tensorOf 1 U` is the dictionary image of a member of `K`. -/ +def TransferClause (𝓘 : ImplementationClass) (K : Set (W 3)) : Prop := + ∀ U : Matrix (Fin 2) (Fin 2) ℂ, 𝓘 (Fin 2) U → Uᴴ * U = 1 → + ∀ ω ∈ K, ∃ ω' ∈ K, + dict ω' = tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U * dict ω * + (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U)ᴴ + +/-- The phase is in the substratum class (a diagonal operator is monomial). -/ +theorem zPhase_monomial (c s : ℝ) : substratumClass (Fin 2) (zPhase c s) := by + first + | exact monomial_diagonal _ + | (show IsMonomial (zPhase c s); exact monomial_diagonal _) + +/-- The phase is unitary on the unit circle. -/ +theorem zPhase_unitary (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) : (zPhase c s)ᴴ * zPhase c s = 1 := by + have hc : (c : ℂ) ^ 2 + (s : ℂ) ^ 2 = 1 := by exact_mod_cast h + rw [zPhase_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [zPhase, zPhaseD, Matrix.mul_apply, Fin.sum_univ_two, Matrix.diagonal_apply, + Matrix.one_apply] <;> + first + | ring1 + | linear_combination hc - (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination -hc + (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination hc + | linear_combination -hc + +/-- **The transfer clause pulls back to the phase rotations.** On a pair cone satisfying the clause +for the substratum class, every table rotated on the target by a point of the unit circle has the +dictionary image of a member of the cone. -/ +theorem transfer_phase {K : Set (W 3)} (hT : TransferClause substratumClass K) (c s : ℝ) + (h : c ^ 2 + s ^ 2 = 1) {ω : W 3} (hω : ω ∈ K) : + ∃ ω' ∈ K, dict ω' = dict (actT (rotZ c s) ω) := by + obtain ⟨ω', hω', heq⟩ := hT (zPhase c s) (zPhase_monomial c s) (zPhase_unitary c s h) ω hω + exact ⟨ω', hω', heq.trans (dict_actT_rotZ c s h ω).symm⟩ + +/-! ### §E — controls -/ + +/-- **Positive control**: the circle hypothesis holds at the rational point `(3/5, 4/5)`. -/ +theorem dict_actT_rotZ_345 (ω : W 3) : + dict (actT (rotZ (3 / 5) (4 / 5)) ω) = + tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) (zPhase (3 / 5) (4 / 5)) * dict ω * + (tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) (zPhase (3 / 5) (4 / 5)))ᴴ := + dict_actT_rotZ (3 / 5) (4 / 5) (by norm_num) ω + +/-- **Countercontrol**: off the unit circle the phase conjugation does not fix `σ₀`, so the circle +hypothesis of `zPhase_pauli0` (and of the intertwinings) is load-bearing. -/ +theorem zPhase_pauli0_counter : zPhase 0 0 * pauli 0 * (zPhase 0 0)ᴴ ≠ pauli 0 := by + intro heq + have h11 := congrFun (congrFun heq 1) 1 + simp [zPhase, pauli, Matrix.mul_apply, Fin.sum_univ_two, Matrix.diagonal_apply, + Matrix.conjTranspose_apply, Matrix.one_apply] at h11 + +#print axioms dict_tens +#print axioms dict_prodState +#print axioms dict_cnot +#print axioms rotZ_cos_sin +#print axioms zPhase_conjTranspose +#print axioms zPhase_pauli0 +#print axioms zPhase_pauli1 +#print axioms zPhase_pauli2 +#print axioms zPhase_pauli3 +#print axioms conj_dict_right +#print axioms conj_dict_left +#print axioms dict_actT_rotZ +#print axioms dict_actC_rotZ +#print axioms dict_actT_nflip +#print axioms dict_actC_nflip +#print axioms monomial_extension_admissible +#print axioms zPhase_unitary +#print axioms transfer_phase +#print axioms dict_actT_rotZ_345 +#print axioms zPhase_pauli0_counter + +end BridgeDictionary +end OIBridge diff --git a/verification/lean-mathlib/OIBridge/EqvK2Block.lean b/verification/lean-mathlib/OIBridge/EqvK2Block.lean new file mode 100644 index 000000000..23c741440 --- /dev/null +++ b/verification/lean-mathlib/OIBridge/EqvK2Block.lean @@ -0,0 +1,522 @@ +/- + OIBridge/EqvK2Block.lean — conditional pair-cone infrastructure (OI-PAIR-MAXCONE-1). + + Special-unitary block actions and the constructive rank-one product-state reduction. + + 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.EqvK2Converse + +namespace OIBridge +namespace EqvK2Block + +open Matrix CompositeDimension MonoidalCompletion EqvK2Schema EqvK2Converse +open scoped ComplexOrder + +noncomputable section + +/-! ### §H.1 — the block group and its action on tables -/ + +/-- The projector `|0⟩⟨0|` of the control. -/ +def P0 : Matrix (Fin 2) (Fin 2) ℂ := !![1, 0; 0, 0] + +/-- The projector `|1⟩⟨1|` of the control. -/ +def P1 : Matrix (Fin 2) (Fin 2) ℂ := !![0, 0; 0, 1] + +/-- The block-diagonal matrix `P₀ ⊗ U₀ + P₁ ⊗ U₁`. -/ +def blockMat (U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ := + tensorOf P0 U₀ + tensorOf P1 U₁ + +/-- The table carried by a block-diagonal conjugation, read back through the coordinates. -/ +def blockAct (U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ) (ω : W 3) : W 3 := + coordOf (blockMat U₀ U₁ * dict ω * (blockMat U₀ U₁)ᴴ) + +/-- A special unitary: a unitary matrix of determinant one. -/ +def IsSU (U : Matrix (Fin 2) (Fin 2) ℂ) : Prop := U ∈ Matrix.unitaryGroup (Fin 2) ℂ ∧ U.det = 1 + +/-- **Block invariance**: `K` is carried into itself by every pair of special unitaries acting +blockwise — the (b)-instances for the operations of the group `H = SU(2) × SU(2)` of HO-31 item 1. -/ +def BlockInvariant (K : Set (W 3)) : Prop := + ∀ U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ, IsSU U₀ → IsSU U₁ → ∀ ω ∈ K, blockAct U₀ U₁ ω ∈ K + +/-- The dictionary image of the carried table is the conjugate. -/ +theorem dict_blockAct (U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ) (ω : W 3) : + dict (blockAct U₀ U₁ ω) = blockMat U₀ U₁ * dict ω * (blockMat U₀ U₁)ᴴ := + dict_coordOf _ (Matrix.isHermitian_mul_mul_conjTranspose _ (dict_isHermitian ω)) + +/-- A pair vector from its two control blocks. -/ +def blockVec (u v : Fin 2 → ℂ) : Fin 2 × Fin 2 → ℂ := fun p => ![u, v] p.1 p.2 + +theorem blockVec_eq (x : Fin 2 × Fin 2 → ℂ) : + blockVec (fun j => x (0, j)) (fun j => x (1, j)) = x := by + funext p + obtain ⟨i, j⟩ := p + fin_cases i <;> rfl + +/-- The block matrix acts blockwise on block vectors. -/ +theorem blockMat_mulVec (U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ) (u v : Fin 2 → ℂ) : + blockMat U₀ U₁ *ᵥ blockVec u v = blockVec (U₀ *ᵥ u) (U₁ *ᵥ v) := by + funext p + obtain ⟨i, j⟩ := p + fin_cases i <;> fin_cases j <;> + simp [blockMat, blockVec, P0, P1, Matrix.mulVec, dotProduct, Fintype.sum_prod_type, + Fin.sum_univ_two, Matrix.add_apply, tensorOf_apply] <;> ring + +/-- Conjugating a rank-one matrix. -/ +theorem conj_vecMulVec (B : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (y : Fin 2 × Fin 2 → ℂ) : + B * Matrix.vecMulVec y (star y) * Bᴴ = Matrix.vecMulVec (B *ᵥ y) (star (B *ᵥ y)) := by + rw [Matrix.mul_vecMulVec, Matrix.vecMulVec_mul, Matrix.star_mulVec] + +/-! ### §H.2 — one token: a special unitary to the north pole -/ + +/-- The squared norm of a one-token vector. -/ +def nrm2 (a : Fin 2 → ℂ) : ℝ := Complex.normSq (a 0) + Complex.normSq (a 1) + +theorem nrm2_nonneg (a : Fin 2 → ℂ) : 0 ≤ nrm2 a := + add_nonneg (Complex.normSq_nonneg _) (Complex.normSq_nonneg _) + +/-- The norm. -/ +def nrm (a : Fin 2 → ℂ) : ℝ := Real.sqrt (nrm2 a) + +theorem nrm_sq (a : Fin 2 → ℂ) : nrm a ^ 2 = nrm2 a := Real.sq_sqrt (nrm2_nonneg a) + +theorem nrm_nonneg (a : Fin 2 → ℂ) : 0 ≤ nrm a := Real.sqrt_nonneg _ + +theorem nrm2_eq_conj (a : Fin 2 → ℂ) : + ((nrm2 a : ℝ) : ℂ) = star (a 0) * a 0 + star (a 1) * a 1 := by + simp only [nrm2, Complex.ofReal_add, Complex.normSq_eq_conj_mul_self, Complex.star_def] + +theorem eq_zero_of_nrm_eq_zero {a : Fin 2 → ℂ} (h : nrm a = 0) : a = 0 := by + have h2 : nrm2 a = 0 := by rw [← nrm_sq a, h]; ring + have h0 : Complex.normSq (a 0) = 0 := by + have := Complex.normSq_nonneg (a 0) + have := Complex.normSq_nonneg (a 1) + unfold nrm2 at h2 + linarith + have h1 : Complex.normSq (a 1) = 0 := by + have := Complex.normSq_nonneg (a 0) + have := Complex.normSq_nonneg (a 1) + unfold nrm2 at h2 + linarith + funext i + fin_cases i + · simpa using Complex.normSq_eq_zero.mp h0 + · simpa using Complex.normSq_eq_zero.mp h1 + +/-- The unnormalised rotation `[[ā₀, ā₁], [−a₁, a₀]]`. -/ +def rotTo (a : Fin 2 → ℂ) : Matrix (Fin 2) (Fin 2) ℂ := !![star (a 0), star (a 1); -(a 1), a 0] + +theorem rotTo_mulVec (a : Fin 2 → ℂ) : rotTo a *ᵥ a = ![((nrm2 a : ℝ) : ℂ), 0] := by + rw [nrm2_eq_conj] + funext i + fin_cases i <;> + simp [rotTo, Matrix.mulVec, dotProduct, Fin.sum_univ_two] <;> ring + +theorem rotTo_mul_star (a : Fin 2 → ℂ) : + rotTo a * star (rotTo a) = ((nrm2 a : ℝ) : ℂ) • (1 : Matrix (Fin 2) (Fin 2) ℂ) := by + rw [nrm2_eq_conj, Matrix.star_eq_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [rotTo, Matrix.mul_apply, Fin.sum_univ_two, Matrix.conjTranspose_apply, Matrix.one_apply] <;> + ring + +theorem rotTo_det (a : Fin 2 → ℂ) : (rotTo a).det = ((nrm2 a : ℝ) : ℂ) := by + rw [nrm2_eq_conj, Matrix.det_fin_two] + first + | (simp [rotTo]; ring) + | (simp [rotTo]; done) + | (simp only [rotTo, Matrix.of_apply, Matrix.cons_val', Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.head_cons, Matrix.empty_val', Matrix.cons_val_fin_one]; ring) + +/-- The special unitary carrying `a` to `(‖a‖, 0)`: the normalised rotation, or `1` when `a = 0`. -/ +def suTo (a : Fin 2 → ℂ) : Matrix (Fin 2) (Fin 2) ℂ := + if nrm a = 0 then 1 else ((nrm a : ℂ)⁻¹) • rotTo a + +theorem star_inv_ofReal (r : ℝ) : star ((r : ℂ)⁻¹) = (r : ℂ)⁻¹ := by + first + | (rw [star_inv₀, Complex.star_def, Complex.conj_ofReal]) + | (simp [Complex.star_def]) + +theorem suTo_isSU (a : Fin 2 → ℂ) : IsSU (suTo a) := by + unfold suTo + split_ifs with h + · exact ⟨Matrix.mem_unitaryGroup_iff.mpr (by simp), Matrix.det_one⟩ + · have hr : (nrm a : ℂ) ≠ 0 := by exact_mod_cast h + have hr2 : (nrm a : ℂ) ^ 2 = ((nrm2 a : ℝ) : ℂ) := by exact_mod_cast nrm_sq a + constructor + · rw [Matrix.mem_unitaryGroup_iff, star_smul, star_inv_ofReal, Matrix.smul_mul, Matrix.mul_smul, + rotTo_mul_star, smul_smul, smul_smul, ← hr2] + have hone : (nrm a : ℂ)⁻¹ * (nrm a : ℂ)⁻¹ * (nrm a : ℂ) ^ 2 = 1 := by + field_simp + first + | (rw [hone, one_smul]) + | (rw [show (nrm a : ℂ)⁻¹ * ((nrm a : ℂ)⁻¹ * (nrm a : ℂ) ^ 2) = 1 by field_simp, one_smul]) + | (simp only [smul_smul]; rw [show (nrm a : ℂ)⁻¹ * (nrm a : ℂ)⁻¹ * (nrm a : ℂ) ^ 2 = 1 by + field_simp, one_smul]) + · rw [Matrix.det_smul, rotTo_det, Fintype.card_fin, ← hr2] + field_simp + +theorem suTo_mulVec (a : Fin 2 → ℂ) : suTo a *ᵥ a = ![(nrm a : ℂ), 0] := by + unfold suTo + split_ifs with h + · have ha := eq_zero_of_nrm_eq_zero h + rw [h, ha, Matrix.mulVec_zero] + funext i + fin_cases i <;> simp + · have hr : (nrm a : ℂ) ≠ 0 := by exact_mod_cast h + have hr2 : (nrm a : ℂ) ^ 2 = ((nrm2 a : ℝ) : ℂ) := by exact_mod_cast nrm_sq a + rw [Matrix.smul_mulVec, rotTo_mulVec, ← hr2] + funext i + fin_cases i + · first + | (simp; field_simp; ring) + | (simp; field_simp) + | (simp; done) + | (simp [pow_two]; field_simp; ring) + · simp + +/-- The conjugate transpose of a special unitary is a special unitary. -/ +theorem isSU_conjTranspose {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : IsSU U) : IsSU Uᴴ := by + refine ⟨?_, ?_⟩ + · rw [← Matrix.star_eq_conjTranspose, Matrix.mem_unitaryGroup_iff, star_star] + exact Matrix.mem_unitaryGroup_iff'.mp hU.1 + · rw [Matrix.det_conjTranspose, hU.2, star_one] + +/-! ### §H.3 — reachability: C19-1 (a) in dictionary form -/ + +/-- The ball state with Bloch vector `(2αβ, 0, α² − β²)/(α² + β²)` (the zero vector when `α = β = 0`). -/ +def bloch (α β : ℝ) : Fin 3 → ℝ := + ![2 * α * β / (α ^ 2 + β ^ 2), 0, (α ^ 2 - β ^ 2) / (α ^ 2 + β ^ 2)] + +theorem bloch_mem_eball (α β : ℝ) : bloch α β ∈ TransitiveBody.eball 3 := by + rw [TransitiveBody.mem_eball, Fin.sum_univ_three] + have e0 : bloch α β 0 = 2 * α * β / (α ^ 2 + β ^ 2) := rfl + have e1 : bloch α β 1 = 0 := rfl + have e2 : bloch α β 2 = (α ^ 2 - β ^ 2) / (α ^ 2 + β ^ 2) := rfl + rw [e0, e1, e2] + by_cases h : α ^ 2 + β ^ 2 = 0 + · simp [h] + · have key : (2 * α * β / (α ^ 2 + β ^ 2)) ^ 2 + (0 : ℝ) ^ 2 + ((α ^ 2 - β ^ 2) / (α ^ 2 + β ^ 2)) ^ 2 + = 1 := by + field_simp + ring + rw [key] + +theorem z3_mem_eball : z3 ∈ TransitiveBody.eball 3 := by + rw [TransitiveBody.mem_eball, Fin.sum_univ_three] + simp [z3] + +/-- The Kronecker vector of two one-token vectors. -/ +def tensVec (u v : Fin 2 → ℂ) : Fin 2 × Fin 2 → ℂ := fun p => u p.1 * v p.2 + +theorem tensVec_eq_blockVec (α β : ℝ) : + tensVec ![(α : ℂ), (β : ℂ)] ![1, 0] = blockVec ![(α : ℂ), 0] ![(β : ℂ), 0] := by + funext p + obtain ⟨i, j⟩ := p + fin_cases i <;> fin_cases j <;> simp [tensVec, blockVec] + +/-- The Kronecker product of two rank-one matrices is the rank-one matrix of the Kronecker vector. -/ +theorem tensorOf_vecMulVec (u v : Fin 2 → ℂ) : + tensorOf (Matrix.vecMulVec u (star u)) (Matrix.vecMulVec v (star v)) = + Matrix.vecMulVec (tensVec u v) (star (tensVec u v)) := by + ext ⟨i, j⟩ ⟨k, l⟩ + simp only [tensorOf_apply, Matrix.vecMulVec_apply, tensVec, Pi.star_apply, star_mul'] + ring + +theorem tensorOf_smul_left (c : ℂ) (A B : Matrix (Fin 2) (Fin 2) ℂ) : + tensorOf (c • A) B = c • tensorOf A B := by + ext ⟨i, j⟩ ⟨k, l⟩ + simp only [tensorOf_apply, Matrix.smul_apply, smul_eq_mul] + ring + +theorem tensorOf_smul_right (c : ℂ) (A B : Matrix (Fin 2) (Fin 2) ℂ) : + tensorOf A (c • B) = c • tensorOf A B := by + ext ⟨i, j⟩ ⟨k, l⟩ + simp only [tensorOf_apply, Matrix.smul_apply, smul_eq_mul] + ring + +/-- The one-token matrix of the north pole is `|0⟩⟨0|`. -/ +theorem tokMat_hom_z3 : tokMat (hom z3) = Matrix.vecMulVec ![(1 : ℂ), 0] (star ![(1 : ℂ), 0]) := by + rw [tokMat_eq] + ext i j + fin_cases i <;> fin_cases j <;> simp [Matrix.vecMulVec_apply, z3] + +/-- The one-token matrix of the Bloch state is the normalised rank-one matrix of `(α, β)`. -/ +theorem tokMat_hom_bloch (α β : ℝ) (h : α ^ 2 + β ^ 2 ≠ 0) : + tokMat (hom (bloch α β)) = + (((α ^ 2 + β ^ 2 : ℝ) : ℂ)⁻¹) • Matrix.vecMulVec ![(α : ℂ), (β : ℂ)] (star ![(α : ℂ), (β : ℂ)]) := by + have hc' : (α : ℂ) ^ 2 + (β : ℂ) ^ 2 ≠ 0 := by exact_mod_cast h + have h0 : hom (bloch α β) 0 = 1 := rfl + have h1 : hom (bloch α β) 1 = 2 * α * β / (α ^ 2 + β ^ 2) := rfl + have h2 : hom (bloch α β) 2 = 0 := rfl + have h3 : hom (bloch α β) 3 = (α ^ 2 - β ^ 2) / (α ^ 2 + β ^ 2) := rfl + rw [tokMat_eq, h0, h1, h2, h3] + ext i j + -- the scalar and the rank-one matrix are applied before any `simp` (which would otherwise unfold + -- `vecMulVec` of a literal into rows by `cons_vecMulVec` and leave the scalar unapplied) + rw [Matrix.smul_apply, Matrix.vecMulVec_apply, smul_eq_mul] + fin_cases i <;> fin_cases j <;> + simp <;> + first + | (field_simp; ring1) + | (field_simp; done) + | ring1 + | (field_simp [hc']; ring1) + | (field_simp [hc']; done) + +/-- The dictionary image of the scaled product state is the rank-one matrix of the block vector. -/ +theorem dict_prod_bloch (α β : ℝ) : + dict ((α ^ 2 + β ^ 2) • prodState (bloch α β) z3) = + Matrix.vecMulVec (blockVec ![(α : ℂ), 0] ![(β : ℂ), 0]) + (star (blockVec ![(α : ℂ), 0] ![(β : ℂ), 0])) := by + rw [← tensVec_eq_blockVec, ← tensorOf_vecMulVec, dict_smul, dict_prodState, tokMat_hom_z3] + by_cases h : α ^ 2 + β ^ 2 = 0 + · have hα : α = 0 := by nlinarith [sq_nonneg α, sq_nonneg β] + have hβ : β = 0 := by nlinarith [sq_nonneg α, sq_nonneg β] + subst hα + subst hβ + have hz : ∀ i : Fin 2, (![((0 : ℝ) : ℂ), ((0 : ℝ) : ℂ)] : Fin 2 → ℂ) i = 0 := by + intro i + fin_cases i <;> simp + ext ⟨i, j⟩ ⟨k, l⟩ + -- the entries are applied before any `simp` (as in `tensorOf_vecMulVec`) + simp only [Matrix.smul_apply, tensorOf_apply, Matrix.vecMulVec_apply, Complex.real_smul, hz] + simp + · rw [tokMat_hom_bloch α β h, tensorOf_smul_left] + have hc : ((α ^ 2 + β ^ 2 : ℝ) : ℂ) ≠ 0 := by exact_mod_cast h + have hone : ((α ^ 2 + β ^ 2 : ℝ) : ℂ) * ((α ^ 2 + β ^ 2 : ℝ) : ℂ)⁻¹ = 1 := mul_inv_cancel₀ hc + ext p q + simp only [Matrix.smul_apply, Complex.real_smul, smul_eq_mul] + first + | (rw [← mul_assoc, hone, one_mul]) + | (field_simp) + | (rw [← mul_assoc, mul_inv_cancel₀ hc, one_mul]) + +/-- **Reachability (C19-1 (a)) in dictionary form.** Every rank-one positive matrix is a block +conjugate, by a pair of special unitaries, of the dictionary image of a nonnegative multiple of a +product state of the ball. -/ +theorem reach_block (x : Fin 2 × Fin 2 → ℂ) : + ∃ U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ, IsSU U₀ ∧ IsSU U₁ ∧ + ∃ x₀ ∈ TransitiveBody.eball 3, ∃ c : ℝ, 0 ≤ c ∧ + blockMat U₀ U₁ * dict (c • prodState x₀ z3) * (blockMat U₀ U₁)ᴴ = + Matrix.vecMulVec x (star x) := by + set a : Fin 2 → ℂ := fun j => x (0, j) with ha + set b : Fin 2 → ℂ := fun j => x (1, j) with hb + refine ⟨(suTo a)ᴴ, (suTo b)ᴴ, isSU_conjTranspose (suTo_isSU a), isSU_conjTranspose (suTo_isSU b), + bloch (nrm a) (nrm b), bloch_mem_eball _ _, nrm a ^ 2 + nrm b ^ 2, by positivity, ?_⟩ + rw [dict_prod_bloch, conj_vecMulVec] + have hx : blockMat (suTo a)ᴴ (suTo b)ᴴ *ᵥ blockVec ![(nrm a : ℂ), 0] ![(nrm b : ℂ), 0] = x := by + rw [blockMat_mulVec, ← suTo_mulVec a, ← suTo_mulVec b, Matrix.mulVec_mulVec, Matrix.mulVec_mulVec] + have hu : (suTo a)ᴴ * suTo a = 1 := by + rw [← Matrix.star_eq_conjTranspose] + exact Matrix.mem_unitaryGroup_iff'.mp (suTo_isSU a).1 + have hv : (suTo b)ᴴ * suTo b = 1 := by + rw [← Matrix.star_eq_conjTranspose] + exact Matrix.mem_unitaryGroup_iff'.mp (suTo_isSU b).1 + rw [hu, hv, Matrix.one_mulVec, Matrix.one_mulVec] + exact blockVec_eq x + rw [hx] + +/-! ### §H.4 — the forcing: C19-1 (b) in the schema's vocabulary -/ + +/-- **Theorem C19-1 (b) in the schema's vocabulary.** Products of ball states (H1), self-duality (H3) +and block invariance force the pair cone to be `Q3` — with no reachability hypothesis and no gate +hypothesis. -/ +theorem pairCone_eq_Q3_of_block {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hH3 : K = dualW K) (hB : BlockInvariant K) : K = Q3 := by + have hK : ∀ ω, ω ∈ K ↔ ω ∈ dualW K := fun ω => Set.ext_iff.mp hH3 ω + have hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K := by + intro c hc ω hω + rw [hK] at hω ⊢ + rw [mem_dualW] at hω ⊢ + intro η hη + rw [ipW_smul_right] + exact mul_nonneg hc (hω η hη) + have hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K := by + intro ω hω η hη + rw [hK] at hω hη ⊢ + rw [mem_dualW] at hω hη ⊢ + intro ζ hζ + rw [ipW_add_right] + exact add_nonneg (hω ζ hζ) (hη ζ hζ) + have hpure : ∀ x : Fin 2 × Fin 2 → ℂ, ∃ ω ∈ K, dict ω = Matrix.vecMulVec x (star x) := by + intro x + obtain ⟨U₀, U₁, hU₀, hU₁, x₀, hx₀, c, hc, h⟩ := reach_block x + refine ⟨blockAct U₀ U₁ (c • prodState x₀ z3), + hB U₀ U₁ hU₀ hU₁ _ (hsmul c hc _ (hH1 x₀ hx₀ z3 z3_mem_eball)), ?_⟩ + rw [dict_blockAct, h] + apply Set.Subset.antisymm + · exact subset_Q3_of_pure_dual hpure fun ω hω => (hK ω).mp hω + · exact Q3_subset_of_pure hadd hpure + +/-- **`Q3` is block-invariant** (the necessity direction in the block form: invariance only). -/ +theorem Q3_blockInvariant : BlockInvariant Q3 := by + intro U₀ U₁ _ _ ω hω + have hω' : (dict ω).PosSemidef := hω + show (dict (blockAct U₀ U₁ ω)).PosSemidef + rw [dict_blockAct] + exact hω'.mul_mul_conjTranspose_same _ + +/-- **The block form as an equivalence.** Given H1 and H3, the pair cone is `Q3` exactly when it is +block-invariant. The direction `→` is `Q3_blockInvariant`; the direction `←` is +`pairCone_eq_Q3_of_block`. -/ +theorem pairCone_eq_Q3_iff_block {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hH3 : K = dualW K) : K = Q3 ↔ BlockInvariant K := by + constructor + · rintro rfl + exact Q3_blockInvariant + · intro hB + exact pairCone_eq_Q3_of_block hH1 hH3 hB + +/-! ### §H.5 — block invariance gives the full-flow form of A_miss -/ + +/-- The diagonal block pair is the idle extension. -/ +theorem blockMat_same (U : Matrix (Fin 2) (Fin 2) ℂ) : + blockMat U U = tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) U := by + ext ⟨i, j⟩ ⟨k, l⟩ + fin_cases i <;> fin_cases k <;> + simp [blockMat, P0, P1, tensorOf_apply, Matrix.add_apply, Matrix.one_apply] + +/-- A common unit scalar does not change the conjugation. -/ +theorem conj_smul (z : ℂ) (hz : star z * z = 1) (A M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : + (z • A) * M * (z • A)ᴴ = A * M * Aᴴ := by + rw [Matrix.conjTranspose_smul, Matrix.smul_mul, Matrix.mul_smul, Matrix.smul_mul, smul_smul, hz, + one_smul] + +/-- The diagonal phase pair `diag(c − i s, c + i s)`, for real `c`, `s` (kept opaque, so that no +`simp` lemma about the cosine or the sine of a real number can rewrite them). -/ +def dphase (c s : ℝ) : Matrix (Fin 2) (Fin 2) ℂ := + !![(c : ℂ) - (s : ℂ) * Complex.I, 0; 0, (c : ℂ) + (s : ℂ) * Complex.I] + +theorem dphase_isSU (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) : IsSU (dphase c s) := by + have hC : (c : ℂ) ^ 2 + (s : ℂ) ^ 2 = 1 := by exact_mod_cast h + constructor + · rw [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [dphase, Matrix.mul_apply, Fin.sum_univ_two, Matrix.conjTranspose_apply, + Matrix.one_apply] <;> + first + | ring1 + | linear_combination hC - (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination hC + (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination hC + | (apply Complex.ext <;> simp <;> nlinarith [h]) + · rw [dphase, Matrix.det_fin_two_of] + first + | linear_combination hC - (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination hC + (s : ℂ) ^ 2 * Complex.I_sq + | (apply Complex.ext <;> simp <;> nlinarith [h]) + +/-- The diagonal phase pair is a unit multiple of `phaseMat c s` when `(c₂, s₂)` is the half angle of +`(c, s)`, stated through the two subtraction identities. -/ +theorem dphase_eq (c₂ s₂ c s : ℝ) (hc : c₂ = c * c₂ + s * s₂) (hs : s₂ = s * c₂ - c * s₂) : + dphase c₂ s₂ = ((c₂ : ℂ) - (s₂ : ℂ) * Complex.I) • phaseMat c s := by + have hcC : (c₂ : ℂ) = (c : ℂ) * c₂ + (s : ℂ) * s₂ := by exact_mod_cast hc + have hsC : (s₂ : ℂ) = (s : ℂ) * c₂ - (c : ℂ) * s₂ := by exact_mod_cast hs + ext i j + fin_cases i <;> fin_cases j <;> + simp [dphase, phaseMat] <;> + first + | ring1 + | linear_combination hcC + Complex.I * hsC + ((s₂ : ℂ) * (s : ℂ)) * Complex.I_sq + | linear_combination (-1 : ℂ) * hcC - Complex.I * hsC - ((s₂ : ℂ) * (s : ℂ)) * Complex.I_sq + | (apply Complex.ext <;> simp <;> nlinarith [hc, hs]) + +theorem dphase_unit (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) : + star ((c : ℂ) - (s : ℂ) * Complex.I) * ((c : ℂ) - (s : ℂ) * Complex.I) = 1 := by + have hC : (c : ℂ) ^ 2 + (s : ℂ) ^ 2 = 1 := by exact_mod_cast h + simp only [Complex.star_def, map_sub, map_mul, Complex.conj_ofReal, Complex.conj_I] + first + | linear_combination hC - (s : ℂ) ^ 2 * Complex.I_sq + | linear_combination hC + (s : ℂ) ^ 2 * Complex.I_sq + | (apply Complex.ext <;> simp <;> nlinarith [h]) + +/-- The half-angle phase `diag(e^{−it/2}, e^{it/2})`. -/ +def hphase (t : ℝ) : Matrix (Fin 2) (Fin 2) ℂ := dphase (Real.cos (t / 2)) (Real.sin (t / 2)) + +theorem hphase_isSU (t : ℝ) : IsSU (hphase t) := + dphase_isSU _ _ (Real.cos_sq_add_sin_sq _) + +/-- The half-angle phase is a unit multiple of the phase matrix of the flow. -/ +theorem hphase_eq (t : ℝ) : + hphase t = ((Real.cos (t / 2) : ℂ) - (Real.sin (t / 2) : ℂ) * Complex.I) • + phaseMat (Real.cos t) (Real.sin t) := by + have hc : Real.cos (t / 2) = Real.cos t * Real.cos (t / 2) + Real.sin t * Real.sin (t / 2) := by + rw [← Real.cos_sub] + congr 1 + ring + have hs : Real.sin (t / 2) = Real.sin t * Real.cos (t / 2) - Real.cos t * Real.sin (t / 2) := by + rw [← Real.sin_sub] + congr 1 + ring + exact dphase_eq _ _ _ _ hc hs + +theorem hphase_unit (t : ℝ) : + star ((Real.cos (t / 2) : ℂ) - (Real.sin (t / 2) : ℂ) * Complex.I) * + ((Real.cos (t / 2) : ℂ) - (Real.sin (t / 2) : ℂ) * Complex.I) = 1 := + dphase_unit _ _ (Real.cos_sq_add_sin_sq _) + +/-- The cyclic permutation's lift is a special unitary. -/ +theorem cycMat_isSU : IsSU cycMat := by + constructor + · rw [Matrix.mem_unitaryGroup_iff, Matrix.star_eq_conjTranspose, cycMat_conjTranspose] + ext i j + fin_cases i <;> fin_cases j <;> + simp [cycMat, cycMatH, Matrix.mul_apply, Fin.sum_univ_two, Matrix.one_apply] <;> + first + | ring1 + | linear_combination (-1 / 2 : ℂ) * Complex.I_sq + | linear_combination (1 / 2 : ℂ) * Complex.I_sq + | linear_combination (-1 / 4 : ℂ) * Complex.I_sq + | linear_combination (1 / 4 : ℂ) * Complex.I_sq + | (apply Complex.ext <;> simp <;> norm_num) + · rw [cycMat, Matrix.det_fin_two_of] + first + | ring1 + | linear_combination (-1 / 2 : ℂ) * Complex.I_sq + | linear_combination (1 / 2 : ℂ) * Complex.I_sq + | (apply Complex.ext <;> simp <;> norm_num) + +/-- **Block invariance gives the full-flow form of A_miss** (the flow and the cyclic permutation on +one token are block pairs of special unitaries). -/ +theorem aMiss_of_blockInvariant {K : Set (W 3)} (hB : BlockInvariant K) : + ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K := by + intro t ω hω + refine ⟨?_, ?_⟩ + · have h := hB (hphase t) (hphase t) (hphase_isSU t) (hphase_isSU t) ω hω + have heq : blockAct (hphase t) (hphase t) ω = actT (KInfFoundations.rotLin t) ω := by + apply dict_injective + rw [dict_blockAct, blockMat_same, dict_actT_rotLin, hphase_eq, tensorOf_smul_right, + conj_smul _ (hphase_unit t)] + rw [heq] at h + exact h + · have h := hB cycMat cycMat cycMat_isSU cycMat_isSU ω hω + have heq : blockAct cycMat cycMat ω = + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω := by + apply dict_injective + rw [dict_blockAct, blockMat_same, dict_actT_cyc] + rw [heq] at h + exact h + +end + +end EqvK2Block +end OIBridge + +#print axioms OIBridge.EqvK2Block.dict_blockAct +#print axioms OIBridge.EqvK2Block.blockMat_mulVec +#print axioms OIBridge.EqvK2Block.conj_vecMulVec +#print axioms OIBridge.EqvK2Block.suTo_isSU +#print axioms OIBridge.EqvK2Block.suTo_mulVec +#print axioms OIBridge.EqvK2Block.dict_prod_bloch +#print axioms OIBridge.EqvK2Block.reach_block +#print axioms OIBridge.EqvK2Block.pairCone_eq_Q3_of_block +#print axioms OIBridge.EqvK2Block.Q3_blockInvariant +#print axioms OIBridge.EqvK2Block.pairCone_eq_Q3_iff_block +#print axioms OIBridge.EqvK2Block.aMiss_of_blockInvariant diff --git a/verification/lean-mathlib/OIBridge/EqvK2Converse.lean b/verification/lean-mathlib/OIBridge/EqvK2Converse.lean new file mode 100644 index 000000000..f01fc607e --- /dev/null +++ b/verification/lean-mathlib/OIBridge/EqvK2Converse.lean @@ -0,0 +1,220 @@ +/- + OIBridge/EqvK2Converse.lean — conditional pair-cone infrastructure (OI-PAIR-MAXCONE-1). + + Exact one-token rotation and cyclic actions through the dictionary, with the quantum invariance witnesses. + + 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.EqvK2Schema + +namespace OIBridge +namespace EqvK2Converse + +open Matrix CompositeDimension MonoidalCompletion EqvK2Schema +open scoped ComplexOrder + +noncomputable section + +/-! ### §G.1 — the dictionary along the control index -/ + +/-- The dictionary split along the control index. -/ +theorem dict_eq_sum_tensorOf (ω : W 3) : + dict ω = ∑ μ : Fin 4, tensorOf (((1 : ℂ) / 2) • pauli μ) (tokMat (ω μ)) := by + ext ⟨i, j⟩ ⟨k, l⟩ + simp only [dict, tokMat, Matrix.sum_apply, Matrix.add_apply, Matrix.smul_apply, tensorOf_apply, + smul_eq_mul, Fin.sum_univ_four] + ring + +/-- The dictionary of a target action, through the split. -/ +theorem dict_actT (N : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) (ω : W 3) : + dict (actT N ω) = + ∑ μ : Fin 4, tensorOf (((1 : ℂ) / 2) • pauli μ) (tokMat (homMap N (ω μ))) := + dict_eq_sum_tensorOf (actT N ω) + +/-- Conjugating the target factor of a Kronecker product. -/ +theorem tensorOf_conj (A B U : Matrix (Fin 2) (Fin 2) ℂ) : + tensorOf A (U * B * Uᴴ) = tensorOf 1 U * tensorOf A B * (tensorOf 1 U)ᴴ := by + rw [tensorOf_conjTranspose, Matrix.conjTranspose_one, tensorOf_mul, tensorOf_mul, one_mul, + mul_one] + +/-! ### §G.2 — one token -/ + +/-- One token's matrix, entrywise. -/ +theorem tokMat_eq (v : HVec 3) : tokMat v = + !![((v 0 : ℂ) + (v 3 : ℂ)) / 2, ((v 1 : ℂ) - (v 2 : ℂ) * Complex.I) / 2; + ((v 1 : ℂ) + (v 2 : ℂ) * Complex.I) / 2, ((v 0 : ℂ) - (v 3 : ℂ)) / 2] := by + ext i j + fin_cases i <;> fin_cases j <;> + first + | (simp [tokMat, pauli, Matrix.sum_apply, Matrix.smul_apply, Fin.sum_univ_four, + Matrix.one_apply]; done) + | (simp [tokMat, pauli, Matrix.sum_apply, Matrix.smul_apply, Fin.sum_univ_four, + Matrix.one_apply]; ring) + | (apply Complex.ext <;> + simp [tokMat, pauli, Matrix.sum_apply, Matrix.smul_apply, Fin.sum_univ_four, + Matrix.one_apply] <;> ring) + +/-- Two `2 × 2` literals agree when their entries do. -/ +theorem mat2_ext {a b c d e f g h : ℂ} (h1 : a = e) (h2 : b = f) (h3 : c = g) (h4 : d = h) : + !![a, b; c, d] = !![e, f; g, h] := by + rw [h1, h2, h3, h4] + +/-- The phase matrix `diag(1, c + i s)`. -/ +def phaseMat (c s : ℝ) : Matrix (Fin 2) (Fin 2) ℂ := + !![1, 0; 0, (c : ℂ) + (s : ℂ) * Complex.I] + +theorem phaseMat_conjTranspose (c s : ℝ) : (phaseMat c s)ᴴ = phaseMat c (-s) := by + ext i j + fin_cases i <;> fin_cases j <;> + first + | (simp [phaseMat, Matrix.conjTranspose_apply]; done) + | (simp [phaseMat, Matrix.conjTranspose_apply]; ring) + | (simp [phaseMat, Matrix.conjTranspose_apply, Complex.star_def]; done) + | (simp [phaseMat, Matrix.conjTranspose_apply, Complex.star_def]; ring) + | (simp [phaseMat, Matrix.conjTranspose_apply]; apply Complex.ext <;> simp [Complex.star_def]) + +/-- The homogenized rotation about the third axis, coordinatewise. -/ +theorem homMap_rotLin (t : ℝ) (v : HVec 3) : + homMap (KInfFoundations.rotLin t) v 0 = v 0 ∧ + homMap (KInfFoundations.rotLin t) v 1 = Real.cos t * v 1 - Real.sin t * v 2 ∧ + homMap (KInfFoundations.rotLin t) v 2 = Real.sin t * v 1 + Real.cos t * v 2 ∧ + homMap (KInfFoundations.rotLin t) v 3 = v 3 := + ⟨rfl, rfl, rfl, rfl⟩ + +/-- **One token, rotation**: conjugation by `diag(1, cos t + i sin t)`. -/ +theorem tokMat_rot (t : ℝ) (v : HVec 3) : + tokMat (homMap (KInfFoundations.rotLin t) v) = + phaseMat (Real.cos t) (Real.sin t) * tokMat v * (phaseMat (Real.cos t) (Real.sin t))ᴴ := by + obtain ⟨h0, h1, h2, h3⟩ := homMap_rotLin t v + have hcs := Real.sin_sq_add_cos_sq t + have e0 : (Real.sin t ^ 2 + Real.cos t ^ 2) * v 0 = v 0 := by rw [hcs, one_mul] + have e3 : (Real.sin t ^ 2 + Real.cos t ^ 2) * v 3 = v 3 := by rw [hcs, one_mul] + rw [phaseMat_conjTranspose, tokMat_eq (homMap (KInfFoundations.rotLin t) v), tokMat_eq v, + h0, h1, h2, h3] + simp only [phaseMat] + rw [Matrix.mul_fin_two, Matrix.mul_fin_two] + refine mat2_ext ?_ ?_ ?_ ?_ <;> apply Complex.ext <;> + simp only [Complex.add_re, Complex.add_im, Complex.sub_re, Complex.sub_im, Complex.mul_re, + Complex.mul_im, Complex.neg_re, Complex.neg_im, Complex.ofReal_re, Complex.ofReal_im, + Complex.I_re, Complex.I_im, Complex.one_re, Complex.one_im, Complex.zero_re, Complex.zero_im, + Complex.div_ofNat_re, Complex.div_ofNat_im] <;> + linarith [e0, e3] + +/-- The matrix `(I − i(X + Y + Z))/2`. -/ +def cycMat : Matrix (Fin 2) (Fin 2) ℂ := + !![(1 - Complex.I) / 2, (-1 - Complex.I) / 2; (1 - Complex.I) / 2, (1 + Complex.I) / 2] + +/-- Its conjugate transpose. -/ +def cycMatH : Matrix (Fin 2) (Fin 2) ℂ := + !![(1 + Complex.I) / 2, (1 + Complex.I) / 2; (-1 + Complex.I) / 2, (1 - Complex.I) / 2] + +theorem cycMat_conjTranspose : cycMatᴴ = cycMatH := by + ext i j + fin_cases i <;> fin_cases j <;> + first + | (simp [cycMat, cycMatH, Matrix.conjTranspose_apply]; done) + | (simp [cycMat, cycMatH, Matrix.conjTranspose_apply]; ring) + | (simp [cycMat, cycMatH, Matrix.conjTranspose_apply, Complex.star_def]; done) + | (simp [cycMat, cycMatH, Matrix.conjTranspose_apply, Complex.star_def]; ring) + | (simp [cycMat, cycMatH, Matrix.conjTranspose_apply]; apply Complex.ext <;> + simp [Complex.star_def] <;> ring) + +/-- The homogenized cyclic permutation, coordinatewise: `(v₀, v₁, v₂, v₃) ↦ (v₀, v₃, v₁, v₂)`. -/ +theorem homMap_cyc (v : HVec 3) : + homMap (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) v 0 = v 0 ∧ + homMap (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) v 1 = v 3 ∧ + homMap (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) v 2 = v 1 ∧ + homMap (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) v 3 = v 2 := + ⟨rfl, rfl, rfl, rfl⟩ + +/-- **One token, cyclic permutation**: conjugation by `(I − i(X + Y + Z))/2`. -/ +theorem tokMat_cyc (v : HVec 3) : + tokMat (homMap (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) v) = + cycMat * tokMat v * cycMatᴴ := by + obtain ⟨h0, h1, h2, h3⟩ := homMap_cyc v + rw [cycMat_conjTranspose, + tokMat_eq (homMap (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) v), tokMat_eq v, + h0, h1, h2, h3] + simp only [cycMat, cycMatH] + rw [Matrix.mul_fin_two, Matrix.mul_fin_two] + refine mat2_ext ?_ ?_ ?_ ?_ <;> apply Complex.ext <;> + simp only [Complex.add_re, Complex.add_im, Complex.sub_re, Complex.sub_im, Complex.mul_re, + Complex.mul_im, Complex.neg_re, Complex.neg_im, Complex.ofReal_re, Complex.ofReal_im, + Complex.I_re, Complex.I_im, Complex.one_re, Complex.one_im, Complex.zero_re, Complex.zero_im, + Complex.div_ofNat_re, Complex.div_ofNat_im] <;> + linarith + +/-! ### §G.3 — the two intertwining lemmas -/ + +/-- **Intertwining, rotation**: the dictionary carries `actT (rotLin t)` to conjugation by +`1 ⊗ diag(1, cos t + i sin t)`. -/ +theorem dict_actT_rotLin (t : ℝ) (ω : W 3) : + dict (actT (KInfFoundations.rotLin t) ω) = + tensorOf 1 (phaseMat (Real.cos t) (Real.sin t)) * dict ω * + (tensorOf 1 (phaseMat (Real.cos t) (Real.sin t)))ᴴ := by + rw [dict_actT, dict_eq_sum_tensorOf ω, Finset.mul_sum, Finset.sum_mul] + refine Finset.sum_congr rfl fun μ _ => ?_ + rw [tokMat_rot, tensorOf_conj] + +/-- **Intertwining, cyclic permutation**: the dictionary carries `actT cycEquiv` to conjugation by +`1 ⊗ (I − i(X + Y + Z))/2`. -/ +theorem dict_actT_cyc (ω : W 3) : + dict (actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω) = + tensorOf 1 cycMat * dict ω * (tensorOf 1 cycMat)ᴴ := by + rw [dict_actT, dict_eq_sum_tensorOf ω, Finset.mul_sum, Finset.sum_mul] + refine Finset.sum_congr rfl fun μ _ => ?_ + rw [tokMat_cyc, tensorOf_conj] + +/-! ### §G.4 — the necessity direction and the equivalence -/ + +/-- **`Q3` is invariant under one token's rotations about the third axis and its cyclic +permutation** (the necessity direction: the full-flow form of A_miss holds for `Q3`). -/ +theorem Q3_aMiss : ∀ t : ℝ, ∀ ω ∈ Q3, actT (KInfFoundations.rotLin t) ω ∈ Q3 ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ Q3 := by + intro t ω hω + have hω' : (dict ω).PosSemidef := hω + refine ⟨?_, ?_⟩ + · show (dict (actT (KInfFoundations.rotLin t) ω)).PosSemidef + rw [dict_actT_rotLin] + first + | exact hω'.mul_mul_conjTranspose_same _ + | simpa using hω'.conjTranspose_mul_mul_same + (tensorOf 1 (phaseMat (Real.cos t) (Real.sin t)))ᴴ + · show (dict (actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω)).PosSemidef + rw [dict_actT_cyc] + first + | exact hω'.mul_mul_conjTranspose_same _ + | simpa using hω'.conjTranspose_mul_mul_same (tensorOf 1 cycMat)ᴴ + +/-- **The pair-level K2 schema as an equivalence.** Given products of ball states (H1), +`cnot`-invariance (H2), self-duality (H3) and the reachability statement `ReachPure`, the pair cone is +`Q3` exactly when it is invariant under one token's rotations about the third axis and its cyclic +permutation (A_miss). The direction `→` is `Q3_aMiss`; the direction `←` is +`EqvK2Schema.pairCone_eq_Q3_of_drive`. -/ +theorem pairCone_eq_Q3_iff_drive {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hH2 : ∀ ω ∈ K, cnot ω ∈ K) (hH3 : K = dualW K) (hreach : ReachPure) : + K = Q3 ↔ ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K := by + constructor + · rintro rfl + exact Q3_aMiss + · intro hA + exact pairCone_eq_Q3_of_drive hH1 hH2 hH3 hA hreach + +end + +end EqvK2Converse +end OIBridge + +#print axioms OIBridge.EqvK2Converse.dict_eq_sum_tensorOf +#print axioms OIBridge.EqvK2Converse.tensorOf_conj +#print axioms OIBridge.EqvK2Converse.tokMat_eq +#print axioms OIBridge.EqvK2Converse.tokMat_rot +#print axioms OIBridge.EqvK2Converse.tokMat_cyc +#print axioms OIBridge.EqvK2Converse.dict_actT_rotLin +#print axioms OIBridge.EqvK2Converse.dict_actT_cyc +#print axioms OIBridge.EqvK2Converse.Q3_aMiss +#print axioms OIBridge.EqvK2Converse.pairCone_eq_Q3_iff_drive diff --git a/verification/lean-mathlib/OIBridge/EqvK2Generation.lean b/verification/lean-mathlib/OIBridge/EqvK2Generation.lean new file mode 100644 index 000000000..1251afd7a --- /dev/null +++ b/verification/lean-mathlib/OIBridge/EqvK2Generation.lean @@ -0,0 +1,540 @@ +/- + OIBridge/EqvK2Generation.lean — conditional pair-cone infrastructure (OI-PAIR-MAXCONE-1). + + Exact generation of the SU(2) block subgroup by CNOT, the full rotation flow and the cyclic datum. + + 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.EqvK2Block +import OIBridge.BridgeConverge +import Mathlib.Analysis.SpecialFunctions.Complex.Arg +import Mathlib.Analysis.SpecialFunctions.Pow.Complex + +namespace OIBridge +namespace EqvK2Generation + +open Matrix CompositeDimension MonoidalCompletion EqvK2Schema EqvK2Converse EqvK2Block +open scoped ComplexOrder + +noncomputable section + +/-! ### §I.1 — conjugation invariance and the block product law -/ + +/-- `K` is carried into itself by conjugation with `M`, read back through the coordinates. -/ +def ConjInv (K : Set (W 3)) (M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : Prop := + ∀ ω ∈ K, coordOf (M * dict ω * Mᴴ) ∈ K + +theorem dict_coordOf_conj (M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (ω : W 3) : + dict (coordOf (M * dict ω * Mᴴ)) = M * dict ω * Mᴴ := + dict_coordOf _ (Matrix.isHermitian_mul_mul_conjTranspose _ (dict_isHermitian ω)) + +theorem conjInv_mul {K : Set (W 3)} {A B : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ} + (hA : ConjInv K A) (hB : ConjInv K B) : ConjInv K (A * B) := by + intro ω hω + have h := hA _ (hB ω hω) + rw [dict_coordOf_conj] at h + have e : A * (B * dict ω * Bᴴ) * Aᴴ = A * B * dict ω * (A * B)ᴴ := by + rw [Matrix.conjTranspose_mul] + simp only [Matrix.mul_assoc] + rwa [e] at h + +theorem conjInv_smul {K : Set (W 3)} {A : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ} (z : ℂ) + (hz : star z * z = 1) (hA : ConjInv K A) : ConjInv K (z • A) := by + intro ω hω + rw [conj_smul z hz] + exact hA ω hω + +theorem P0_mul_P0 : P0 * P0 = P0 := by + first + | (ext i j; fin_cases i <;> fin_cases j <;> simp [P0, Matrix.mul_apply, Fin.sum_univ_two]; done) + | (simp only [P0, Matrix.mul_fin_two]; ext i j; fin_cases i <;> fin_cases j <;> simp; done) + +theorem P0_mul_P1 : P0 * P1 = 0 := by + first + | (ext i j; fin_cases i <;> fin_cases j <;> simp [P0, P1, Matrix.mul_apply, Fin.sum_univ_two]; done) + | (simp only [P0, P1, Matrix.mul_fin_two]; ext i j; fin_cases i <;> fin_cases j <;> simp; done) + +theorem P1_mul_P0 : P1 * P0 = 0 := by + first + | (ext i j; fin_cases i <;> fin_cases j <;> simp [P0, P1, Matrix.mul_apply, Fin.sum_univ_two]; done) + | (simp only [P0, P1, Matrix.mul_fin_two]; ext i j; fin_cases i <;> fin_cases j <;> simp; done) + +theorem P1_mul_P1 : P1 * P1 = P1 := by + first + | (ext i j; fin_cases i <;> fin_cases j <;> simp [P1, Matrix.mul_apply, Fin.sum_univ_two]; done) + | (simp only [P1, Matrix.mul_fin_two]; ext i j; fin_cases i <;> fin_cases j <;> simp; done) + +theorem tensorOf_zero_left (B : Matrix (Fin 2) (Fin 2) ℂ) : + tensorOf (0 : Matrix (Fin 2) (Fin 2) ℂ) B = 0 := by + ext p q + simp [tensorOf_apply] + +/-- **The block product law.** -/ +theorem blockMat_mul (A B C D : Matrix (Fin 2) (Fin 2) ℂ) : + blockMat A B * blockMat C D = blockMat (A * C) (B * D) := by + simp only [blockMat, Matrix.add_mul, Matrix.mul_add, tensorOf_mul, P0_mul_P0, P0_mul_P1, + P1_mul_P0, P1_mul_P1, tensorOf_zero_left, add_zero, zero_add] + +theorem tensorOf_one_mul (A B : Matrix (Fin 2) (Fin 2) ℂ) : + tensorOf (1 : Matrix (Fin 2) (Fin 2) ℂ) (A * B) = tensorOf 1 A * tensorOf 1 B := by + rw [tensorOf_mul, Matrix.one_mul] + +theorem isSU_mul {A B : Matrix (Fin 2) (Fin 2) ℂ} (hA : IsSU A) (hB : IsSU B) : IsSU (A * B) := + ⟨Submonoid.mul_mem _ hA.1 hB.1, by rw [Matrix.det_mul, hA.2, hB.2, one_mul]⟩ + +theorem isSU_unitary {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : IsSU U) : Uᴴ * U = 1 := by + rw [← Matrix.star_eq_conjTranspose] + exact Matrix.mem_unitaryGroup_iff'.mp hU.1 + +/-! ### §I.2 — the generators -/ + +/-- Every point of the unit circle is `(cos t, sin t)` for some `t`. -/ +theorem exists_angle (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) : + ∃ t : ℝ, Real.cos t = c ∧ Real.sin t = s := by + have hre : (Complex.mk c s).re = c := rfl + have him : (Complex.mk c s).im = s := rfl + have hsq : ‖Complex.mk c s‖ ^ 2 = 1 := by + rw [← Complex.normSq_eq_norm_sq] + first + | (rw [Complex.normSq_apply, hre, him]; nlinarith [h]) + | (rw [Complex.normSq_mk]; nlinarith [h]) + | (simp [Complex.normSq_apply]; nlinarith [h]) + have hn : ‖Complex.mk c s‖ = 1 := by + have h0 := norm_nonneg (Complex.mk c s) + nlinarith [hsq, h0] + have hz0 : Complex.mk c s ≠ 0 := by + intro h0 + rw [h0, norm_zero] at hn + exact zero_ne_one hn + refine ⟨Complex.arg (Complex.mk c s), ?_, ?_⟩ + · simp only [Complex.cos_arg hz0, hn, div_one, hre] + · simp only [Complex.sin_arg, hn, div_one, him] + +/-- The flow at one angle. -/ +theorem conjInv_phase {K : Set (W 3)} + (hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K) (t : ℝ) : + ConjInv K (tensorOf 1 (phaseMat (Real.cos t) (Real.sin t))) := by + intro ω hω + rw [← dict_actT_rotLin, coordOf_dict] + exact hflow t ω hω + +/-- The flow at every point of the unit circle. -/ +theorem conjInv_phase_circle {K : Set (W 3)} + (hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K) (c s : ℝ) + (h : c ^ 2 + s ^ 2 = 1) : ConjInv K (tensorOf 1 (phaseMat c s)) := by + obtain ⟨t, hc, hs⟩ := exists_angle c s h + rw [← hc, ← hs] + exact conjInv_phase hflow t + +/-- The diagonal special unitary `diag(z, z̄)` (special unitary when `|z| = 1`). -/ +def dUnit (z : ℂ) : Matrix (Fin 2) (Fin 2) ℂ := !![z, 0; 0, star z] + +theorem dUnit_eq_smul (z : ℂ) (hz : star z * z = 1) : + dUnit z = z • phaseMat (star z ^ 2).re (star z ^ 2).im := by + have hre : (((star z ^ 2).re : ℝ) : ℂ) + (((star z ^ 2).im : ℝ) : ℂ) * Complex.I = star z ^ 2 := + Complex.re_add_im _ + have key : z * star z ^ 2 = star z := by linear_combination (star z) * hz + rw [Matrix.eta_fin_two (z • phaseMat (star z ^ 2).re (star z ^ 2).im)] + simp only [dUnit, phaseMat, Matrix.smul_apply, Matrix.of_apply, Matrix.cons_val_zero, + Matrix.cons_val_one, smul_eq_mul, mul_one, mul_zero, hre, key] + +/-- The diagonal unit pairs, from the flow. -/ +theorem conjInv_dUnit {K : Set (W 3)} + (hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K) (z : ℂ) + (hz : star z * z = 1) : ConjInv K (tensorOf 1 (dUnit z)) := by + have hw : (star z ^ 2).re ^ 2 + (star z ^ 2).im ^ 2 = 1 := by + have h1 : star (star z ^ 2) * star z ^ 2 = 1 := by + rw [star_pow, star_star] + linear_combination (star z * z + 1) * hz + have h2 : ((Complex.normSq (star z ^ 2) : ℝ) : ℂ) = 1 := by + rw [Complex.normSq_eq_conj_mul_self, ← Complex.star_def] + exact h1 + have h3 : Complex.normSq (star z ^ 2) = 1 := by exact_mod_cast h2 + rw [Complex.normSq_apply] at h3 + nlinarith [h3] + rw [dUnit_eq_smul z hz, tensorOf_smul_right] + exact conjInv_smul z hz (conjInv_phase_circle hflow _ _ hw) + +/-- The cyclic lift. -/ +theorem conjInv_cyc {K : Set (W 3)} + (hcyc : ∀ ω ∈ K, actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) : + ConjInv K (tensorOf 1 cycMat) := by + intro ω hω + rw [← dict_actT_cyc, coordOf_dict] + exact hcyc ω hω + +/-- The cyclic lift has order three up to sign: `cycMatᴴ = −cycMat²`. -/ +theorem cycMat_conjTranspose_eq : cycMatᴴ = (-1 : ℂ) • (cycMat * cycMat) := by + rw [cycMat_conjTranspose, Matrix.eta_fin_two ((-1 : ℂ) • (cycMat * cycMat))] + simp only [cycMatH, cycMat, Matrix.mul_fin_two, Matrix.smul_apply, Matrix.of_apply, + Matrix.cons_val_zero, Matrix.cons_val_one, smul_eq_mul] + refine mat2_ext ?_ ?_ ?_ ?_ <;> + first + | ring1 + | linear_combination (1 / 2 : ℂ) * Complex.I_sq + | linear_combination (-1 / 2 : ℂ) * Complex.I_sq + +/-- The inverse of the cyclic lift, as the square of the lift up to sign. -/ +theorem conjInv_cycH {K : Set (W 3)} + (hcyc : ∀ ω ∈ K, actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) : + ConjInv K (tensorOf 1 cycMatᴴ) := by + rw [cycMat_conjTranspose_eq, tensorOf_smul_right, tensorOf_one_mul] + exact conjInv_smul (-1) (by simp) (conjInv_mul (conjInv_cyc hcyc) (conjInv_cyc hcyc)) + +/-- The flip `X`. -/ +def Xm : Matrix (Fin 2) (Fin 2) ℂ := !![0, 1; 1, 0] + +/-- The bridge's controlled NOT is the block pair `(1, X)`. -/ +theorem cnotMat_eq : BridgeDictionary.cnotMat = blockMat 1 Xm := by + ext ⟨i, j⟩ ⟨k, l⟩ + fin_cases i <;> fin_cases j <;> fin_cases k <;> fin_cases l <;> + simp [BridgeDictionary.cnotMat, BridgeDictionary.projZero, BridgeDictionary.projOne, + BridgeDictionary.pauli, blockMat, P0, P1, Xm, tensorOf_apply, Matrix.add_apply, + Matrix.diagonal_apply, Matrix.one_apply] + +theorem cnotMat_conjTranspose : (blockMat 1 Xm)ᴴ = blockMat 1 Xm := by + ext ⟨i, j⟩ ⟨k, l⟩ + fin_cases i <;> fin_cases j <;> fin_cases k <;> fin_cases l <;> + simp [blockMat, P0, P1, Xm, tensorOf_apply, Matrix.add_apply, Matrix.conjTranspose_apply, + Matrix.one_apply] + +/-- The gate, through the bridge's `dict_cnot` on the one dictionary. -/ +theorem dict_cnot_block (ω : W 3) : + dict (cnot ω) = blockMat 1 Xm * dict ω * (blockMat 1 Xm)ᴴ := by + rw [cnotMat_conjTranspose, ← cnotMat_eq, ← BridgeConverge.dict_converge, + BridgeDictionary.dict_cnot] + +theorem conjInv_cnot {K : Set (W 3)} (hH2 : ∀ ω ∈ K, cnot ω ∈ K) : + ConjInv K (blockMat 1 Xm) := by + intro ω hω + rw [← dict_cnot_block, coordOf_dict] + exact hH2 ω hω + +/-! ### §I.3 — one token: Euler factors and idle invariance -/ + +/-- The real rotation `[[c, −s], [s, c]]`. -/ +def rotRe (c s : ℝ) : Matrix (Fin 2) (Fin 2) ℂ := !![(c : ℂ), -(s : ℂ); (s : ℂ), (c : ℂ)] + +/-- The real rotation is the inverse cyclic conjugate of a diagonal unit pair. -/ +theorem rotRe_eq (c s : ℝ) : + rotRe c s = cycMatᴴ * dUnit ((c : ℂ) - (s : ℂ) * Complex.I) * cycMat := by + have hst : star ((c : ℂ) - (s : ℂ) * Complex.I) = (c : ℂ) + (s : ℂ) * Complex.I := by + first + | (simp; done) + | (rw [Complex.star_def, map_sub, map_mul, Complex.conj_ofReal, Complex.conj_ofReal, + Complex.conj_I]; ring1) + rw [cycMat_conjTranspose] + simp only [rotRe, dUnit, hst, cycMatH, cycMat, Matrix.mul_fin_two] + refine mat2_ext ?_ ?_ ?_ ?_ + · linear_combination ((c : ℂ) / 2) * Complex.I_sq + · linear_combination (-(s : ℂ) * (Complex.I + 2) / 2) * Complex.I_sq + · linear_combination (-(s : ℂ) * (Complex.I - 2) / 2) * Complex.I_sq + · linear_combination ((c : ℂ) / 2) * Complex.I_sq + +/-- A special unitary of `ℂ²`: `[[p, −q̄], [q, p̄]]` with `|p|² + |q|² = 1`. -/ +theorem su_form {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : IsSU U) : + U = !![U 0 0, -star (U 1 0); U 1 0, star (U 0 0)] ∧ + star (U 0 0) * U 0 0 + star (U 1 0) * U 1 0 = 1 := by + have hu : star U * U = 1 := Matrix.mem_unitaryGroup_iff'.mp hU.1 + have h1 : U * Matrix.adjugate U = 1 := by rw [Matrix.mul_adjugate, hU.2, one_smul] + have hadj : star U = Matrix.adjugate U := by + calc star U = star U * (U * Matrix.adjugate U) := by rw [h1, Matrix.mul_one] + _ = star U * U * Matrix.adjugate U := by rw [Matrix.mul_assoc] + _ = Matrix.adjugate U := by rw [hu, Matrix.one_mul] + rw [Matrix.adjugate_fin_two] at hadj + have e00 : star (U 0 0) = U 1 1 := by + have h := congrFun (congrFun hadj 0) 0 + simpa [Matrix.star_apply] using h + have e10 : star (U 0 1) = -U 1 0 := by + have h := congrFun (congrFun hadj 1) 0 + simpa [Matrix.star_apply] using h + have e01 : U 0 1 = -star (U 1 0) := by + have h := congrArg star e10 + rwa [star_star, star_neg] at h + refine ⟨?_, ?_⟩ + · conv_lhs => rw [Matrix.eta_fin_two U] + rw [e01, ← e00] + · have h := congrFun (congrFun hu 0) 0 + simpa [Matrix.mul_apply, Fin.sum_univ_two, Matrix.star_apply] using h + +/-- Polar form. -/ +theorem polar_unit (p : ℂ) : ∃ u : ℂ, star u * u = 1 ∧ p = ((‖p‖ : ℝ) : ℂ) * u := by + by_cases hp : p = 0 + · exact ⟨1, by simp, by simp [hp]⟩ + · have hn : ((‖p‖ : ℝ) : ℂ) ≠ 0 := by + rw [Complex.ofReal_ne_zero] + exact norm_ne_zero_iff.mpr hp + refine ⟨p / ((‖p‖ : ℝ) : ℂ), ?_, (mul_div_cancel₀ p hn).symm⟩ + have h1 : star p * p = ((‖p‖ : ℝ) : ℂ) ^ 2 := by + rw [Complex.star_def] + exact_mod_cast Complex.conj_mul' p + have h2 : star (p / ((‖p‖ : ℝ) : ℂ)) = star p / ((‖p‖ : ℝ) : ℂ) := by + rw [star_div₀] + congr 1 + rw [Complex.star_def, Complex.conj_ofReal] + rw [h2, div_mul_div_comm, h1, sq, div_self (mul_ne_zero hn hn)] + +/-- A square root of a unit complex number is a unit. -/ +theorem exists_unit_sqrt {w : ℂ} (hw : star w * w = 1) : ∃ b : ℂ, star b * b = 1 ∧ b ^ 2 = w := by + obtain ⟨b, hb⟩ : ∃ b : ℂ, b ^ 2 = w := + ⟨w ^ (((2 : ℕ) : ℂ)⁻¹), Complex.cpow_nat_inv_pow w (by norm_num)⟩ + have hw' : (starRingEnd ℂ) w * w = 1 := by + rw [← Complex.star_def] + exact hw + have hn : Complex.normSq b = 1 := by + have h2 : ((Complex.normSq b : ℝ) : ℂ) ^ 2 = 1 := by + rw [Complex.normSq_eq_conj_mul_self, mul_pow, ← map_pow, hb] + exact hw' + have h2' : Complex.normSq b ^ 2 = 1 := by exact_mod_cast h2 + have hnn := Complex.normSq_nonneg b + nlinarith [h2', hnn] + refine ⟨b, ?_, hb⟩ + rw [Complex.star_def, ← Complex.normSq_eq_conj_mul_self, hn, Complex.ofReal_one] + +/-- The Euler factorisation, as an identity of `2 × 2` literals. -/ +theorem euler_core (p q u₁ u₂ b : ℂ) (c s : ℝ) + (hp : p = (c : ℂ) * u₁) (hq : q = (s : ℂ) * u₂) (hb : star b * b = 1) + (hb2 : b ^ 2 = u₁ * u₂) (hu₁ : star u₁ * u₁ = 1) : + !![p, -star q; q, star p] = dUnit (u₁ * star b) * rotRe c s * dUnit b := by + have hps : star p = (c : ℂ) * star u₁ := by + rw [hp] + first + | (simp; done) + | (rw [star_mul', Complex.star_def, Complex.conj_ofReal]) + have hqs : star q = (s : ℂ) * star u₂ := by + rw [hq] + first + | (simp; done) + | (rw [star_mul', Complex.star_def, Complex.conj_ofReal]) + have ha' : star (u₁ * star b) = star u₁ * b := by rw [star_mul', star_star] + have hb2s : star b ^ 2 = star u₁ * star u₂ := by + rw [← star_pow, hb2, star_mul'] + simp only [dUnit, rotRe, Matrix.mul_fin_two, ha'] + refine mat2_ext ?_ ?_ ?_ ?_ + · linear_combination hp - ((c : ℂ) * u₁) * hb + · linear_combination (-1 : ℂ) * hqs + ((s : ℂ) * u₁) * hb2s + ((s : ℂ) * star u₂) * hu₁ + · linear_combination hq - ((s : ℂ) * star u₁) * hb2 - ((s : ℂ) * u₂) * hu₁ + · linear_combination hps - ((c : ℂ) * star u₁) * hb + +/-- **Every special unitary of `ℂ²` is a product of a diagonal unit pair, a real rotation and a +diagonal unit pair** (exact, no angle beyond the polar forms and one square root). -/ +theorem su_euler {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : IsSU U) : + ∃ a b : ℂ, star a * a = 1 ∧ star b * b = 1 ∧ ∃ c s : ℝ, c ^ 2 + s ^ 2 = 1 ∧ + U = dUnit a * rotRe c s * dUnit b := by + obtain ⟨hform, hnorm⟩ := su_form hU + obtain ⟨u₁, hu₁, hp⟩ := polar_unit (U 0 0) + obtain ⟨u₂, hu₂, hq⟩ := polar_unit (U 1 0) + have hw : star (u₁ * u₂) * (u₁ * u₂) = 1 := by + rw [star_mul'] + linear_combination (star u₂ * u₂) * hu₁ + hu₂ + obtain ⟨b, hb, hb2⟩ := exists_unit_sqrt hw + refine ⟨u₁ * star b, b, ?_, hb, ‖U 0 0‖, ‖U 1 0‖, ?_, ?_⟩ + · rw [star_mul', star_star] + linear_combination (b * star b) * hu₁ + hb + · have h1 : star (U 0 0) * U 0 0 = ((‖U 0 0‖ : ℝ) : ℂ) ^ 2 := by + rw [Complex.star_def] + exact_mod_cast Complex.conj_mul' (U 0 0) + have h2 : star (U 1 0) * U 1 0 = ((‖U 1 0‖ : ℝ) : ℂ) ^ 2 := by + rw [Complex.star_def] + exact_mod_cast Complex.conj_mul' (U 1 0) + rw [h1, h2] at hnorm + exact_mod_cast hnorm + · exact hform.trans (euler_core (U 0 0) (U 1 0) u₁ u₂ b ‖U 0 0‖ ‖U 1 0‖ hp hq hb hb2 hu₁) + +/-- **Idle invariance under every special unitary**, from the flow and the cyclic lift. -/ +theorem conjInv_idle {K : Set (W 3)} + (hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K) + (hcyc : ∀ ω ∈ K, actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) + {U : Matrix (Fin 2) (Fin 2) ℂ} (hU : IsSU U) : ConjInv K (tensorOf 1 U) := by + obtain ⟨a, b, ha, hb, c, s, hcs, hUe⟩ := su_euler hU + rw [hUe, tensorOf_one_mul, tensorOf_one_mul, rotRe_eq, tensorOf_one_mul, tensorOf_one_mul] + exact conjInv_mul (conjInv_mul (conjInv_dUnit hflow a ha) + (conjInv_mul (conjInv_mul (conjInv_cycH hcyc) (conjInv_dUnit hflow _ (dphase_unit c s hcs))) + (conjInv_cyc hcyc))) (conjInv_dUnit hflow b hb) + +/-! ### §I.4 — the controlled half -/ + +/-- **The controlled phase as a word in the gate and the flow.** -/ +theorem rtrick (r : ℂ) (hr : star r * r = 1) : + blockMat 1 Xm * blockMat (dUnit r) (dUnit r) * blockMat 1 Xm * + blockMat (dUnit (star r)) (dUnit (star r)) = blockMat 1 (dUnit (star r ^ 2)) := by + rw [blockMat_mul, blockMat_mul, blockMat_mul] + congr 1 + · simp only [Matrix.one_mul, Matrix.mul_one, dUnit, Matrix.mul_fin_two, star_star, + Matrix.one_fin_two] + refine mat2_ext ?_ ?_ ?_ ?_ <;> + first + | ring1 + | linear_combination hr + · simp only [dUnit, Xm, Matrix.mul_fin_two, star_star, star_pow] + refine mat2_ext ?_ ?_ ?_ ?_ <;> ring1 + +/-- The controlled diagonal unit pairs. -/ +theorem conjInv_ctrl_dUnit {K : Set (W 3)} (hc : ConjInv K (blockMat 1 Xm)) + (hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K) (a : ℂ) + (ha : star a * a = 1) : ConjInv K (blockMat 1 (dUnit a)) := by + have hw : star (star a) * star a = 1 := by + rw [star_star] + linear_combination ha + obtain ⟨r, hr, hr2⟩ := exists_unit_sqrt hw + have e : dUnit a = dUnit (star r ^ 2) := by + rw [← star_pow, hr2, star_star] + have hsr : star (star r) * star r = 1 := by + rw [star_star] + linear_combination hr + rw [e, ← rtrick r hr] + refine conjInv_mul (conjInv_mul (conjInv_mul hc ?_) hc) ?_ + · rw [blockMat_same] + exact conjInv_dUnit hflow r hr + · rw [blockMat_same] + exact conjInv_dUnit hflow (star r) hsr + +/-- The controlled real rotations, conjugates of controlled diagonal pairs by idle cyclic lifts. -/ +theorem conjInv_ctrl_rotRe {K : Set (W 3)} (hc : ConjInv K (blockMat 1 Xm)) + (hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K) + (hcyc : ∀ ω ∈ K, actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) + (c s : ℝ) (h : c ^ 2 + s ^ 2 = 1) : ConjInv K (blockMat 1 (rotRe c s)) := by + have hCu : cycMatᴴ * cycMat = 1 := isSU_unitary cycMat_isSU + have e : blockMat 1 (rotRe c s) = blockMat cycMatᴴ cycMatᴴ * + blockMat 1 (dUnit ((c : ℂ) - (s : ℂ) * Complex.I)) * blockMat cycMat cycMat := by + rw [blockMat_mul, blockMat_mul, Matrix.mul_one, hCu, ← rotRe_eq] + rw [e] + refine conjInv_mul (conjInv_mul ?_ (conjInv_ctrl_dUnit hc hflow _ (dphase_unit c s h))) ?_ + · rw [blockMat_same] + exact conjInv_cycH hcyc + · rw [blockMat_same] + exact conjInv_cyc hcyc + +/-- **Controlled invariance under every special unitary.** -/ +theorem conjInv_ctrl {K : Set (W 3)} (hc : ConjInv K (blockMat 1 Xm)) + (hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K) + (hcyc : ∀ ω ∈ K, actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) + {V : Matrix (Fin 2) (Fin 2) ℂ} (hV : IsSU V) : ConjInv K (blockMat 1 V) := by + obtain ⟨a, b, ha, hb, c, s, hcs, hVe⟩ := su_euler hV + have e : blockMat 1 V = blockMat 1 (dUnit a) * blockMat 1 (rotRe c s) * blockMat 1 (dUnit b) := by + rw [blockMat_mul, blockMat_mul, Matrix.one_mul, Matrix.one_mul, ← hVe] + rw [e] + exact conjInv_mul (conjInv_mul (conjInv_ctrl_dUnit hc hflow a ha) + (conjInv_ctrl_rotRe hc hflow hcyc c s hcs)) (conjInv_ctrl_dUnit hc hflow b hb) + +/-! ### §I.5 — block invariance, `ReachPure`, and the schema without it -/ + +/-- **Block invariance from the gate and the clause's two operations at every angle** — exact finite +words, no closure. -/ +theorem blockInvariant_of_drive {K : Set (W 3)} (hH2 : ∀ ω ∈ K, cnot ω ∈ K) + (hA : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) : + BlockInvariant K := by + have hflow : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K := + fun t ω hω => (hA t ω hω).1 + have hcyc : ∀ ω ∈ K, actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K := + fun ω hω => (hA 0 ω hω).2 + have hc : ConjInv K (blockMat 1 Xm) := conjInv_cnot hH2 + intro U₀ U₁ hU₀ hU₁ ω hω + have hu : U₀ᴴ * U₀ = 1 := isSU_unitary hU₀ + have e : blockMat U₀ U₁ = blockMat 1 (U₁ * U₀ᴴ) * blockMat U₀ U₀ := by + rw [blockMat_mul, Matrix.one_mul, Matrix.mul_assoc, hu, Matrix.mul_one] + have hW : IsSU (U₁ * U₀ᴴ) := isSU_mul hU₁ (isSU_conjTranspose hU₀) + have hI : ConjInv K (blockMat U₀ U₀) := by + rw [blockMat_same] + exact conjInv_idle hflow hcyc hU₀ + show coordOf (blockMat U₀ U₁ * dict ω * (blockMat U₀ U₁)ᴴ) ∈ K + rw [e] + exact conjInv_mul (conjInv_ctrl hc hflow hcyc hW) hI ω hω + +theorem cnot_mem_driveWords : (cnot : W 3 →ₗ[ℝ] W 3) ∈ driveWords := by + first + | exact Submonoid.subset_closure (Set.mem_union_left _ (Set.mem_union_left _ (Set.mem_singleton _))) + | (apply Submonoid.subset_closure; simp [driveGens]) + +theorem rot_mem_driveWords (t : ℝ) : actTLin (KInfFoundations.rotLin t) ∈ driveWords := by + first + | exact Submonoid.subset_closure + (Set.mem_union_left _ (Set.mem_union_right _ (Set.mem_range_self t))) + | (apply Submonoid.subset_closure; simp [driveGens]) + +theorem cyc_mem_driveWords : + actTLin (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ∈ driveWords := by + first + | exact Submonoid.subset_closure (Set.mem_union_right _ (Set.mem_singleton _)) + | (apply Submonoid.subset_closure; simp [driveGens]) + +/-- The scaled drive images of product states of the ball. -/ +def driveOrbit : Set (W 3) := + {ω | ∃ g ∈ driveWords, ∃ x₀ ∈ TransitiveBody.eball 3, ∃ y₀ ∈ TransitiveBody.eball 3, + ∃ c : ℝ, 0 ≤ c ∧ ω = c • g (prodState x₀ y₀)} + +theorem driveOrbit_gen {g' : Module.End ℝ (W 3)} (hg' : g' ∈ driveWords) : + ∀ ω ∈ driveOrbit, g' ω ∈ driveOrbit := by + rintro ω ⟨g, hg, x₀, hx₀, y₀, hy₀, c, hc, rfl⟩ + exact ⟨g' * g, driveWords.mul_mem hg' hg, x₀, hx₀, y₀, hy₀, c, hc, by + rw [map_smul, Module.End.mul_apply]⟩ + +/-- **`ReachPure` is a theorem**: every pure two-token state is, up to a nonnegative scale, a drive +word applied to a product state of the ball (S6's lemma L4, no longer a hypothesis). -/ +theorem reachPure : ReachPure := by + intro x + have hH2 : ∀ ω ∈ driveOrbit, cnot ω ∈ driveOrbit := + fun ω hω => driveOrbit_gen cnot_mem_driveWords ω hω + have hA : ∀ t : ℝ, ∀ ω ∈ driveOrbit, actT (KInfFoundations.rotLin t) ω ∈ driveOrbit ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ driveOrbit := + fun t ω hω => ⟨driveOrbit_gen (rot_mem_driveWords t) ω hω, + driveOrbit_gen cyc_mem_driveWords ω hω⟩ + have hB : BlockInvariant driveOrbit := blockInvariant_of_drive hH2 hA + obtain ⟨U₀, U₁, hU₀, hU₁, x₀, hx₀, c, hc, h⟩ := reach_block x + have hmem : c • prodState x₀ z3 ∈ driveOrbit := + ⟨1, driveWords.one_mem, x₀, hx₀, z3, z3_mem_eball, c, hc, rfl⟩ + obtain ⟨g, hg, x₁, hx₁, y₁, hy₁, c₁, hc₁, he⟩ := hB U₀ U₁ hU₀ hU₁ _ hmem + refine ⟨g, hg, x₁, hx₁, y₁, hy₁, c₁, hc₁, ?_⟩ + rw [← he, dict_blockAct, h] + +/-- **The pair-level K2 schema without `ReachPure`**: products (H1), the gate (H2), self-duality +(H3) and the clause's two operations at every angle (A_miss) force `K = Q3`. -/ +theorem pairCone_eq_Q3_of_drive_exact {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hH2 : ∀ ω ∈ K, cnot ω ∈ K) (hH3 : K = dualW K) + (hA : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) : K = Q3 := + pairCone_eq_Q3_of_block hH1 hH3 (blockInvariant_of_drive hH2 hA) + +/-- **`Q3` is invariant under the gate** (the necessity of H2, invariance only). -/ +theorem Q3_cnot : ∀ ω ∈ Q3, cnot ω ∈ Q3 := by + intro ω hω + have hω' : (dict ω).PosSemidef := hω + show (dict (cnot ω)).PosSemidef + rw [dict_cnot_block] + exact hω'.mul_mul_conjTranspose_same _ + +/-- **The full-flow form as an equivalence.** Given H1 and H3, the pair cone is `Q3` exactly when it +is invariant under the gate and under the clause's two operations at every angle. The direction `→` +is `Q3_cnot` with `Q3_aMiss`; the direction `←` is `pairCone_eq_Q3_of_drive_exact`. -/ +theorem pairCone_eq_Q3_iff_drive_exact {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hH3 : K = dualW K) : + K = Q3 ↔ ((∀ ω ∈ K, cnot ω ∈ K) ∧ ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) := by + constructor + · rintro rfl + exact ⟨Q3_cnot, Q3_aMiss⟩ + · rintro ⟨hH2, hA⟩ + exact pairCone_eq_Q3_of_drive_exact hH1 hH2 hH3 hA + +end + +end EqvK2Generation +end OIBridge + +#print axioms OIBridge.EqvK2Generation.blockMat_mul +#print axioms OIBridge.EqvK2Generation.cycMat_conjTranspose_eq +#print axioms OIBridge.EqvK2Generation.rotRe_eq +#print axioms OIBridge.EqvK2Generation.su_euler +#print axioms OIBridge.EqvK2Generation.conjInv_idle +#print axioms OIBridge.EqvK2Generation.rtrick +#print axioms OIBridge.EqvK2Generation.conjInv_ctrl +#print axioms OIBridge.EqvK2Generation.blockInvariant_of_drive +#print axioms OIBridge.EqvK2Generation.reachPure +#print axioms OIBridge.EqvK2Generation.pairCone_eq_Q3_of_drive_exact +#print axioms OIBridge.EqvK2Generation.Q3_cnot +#print axioms OIBridge.EqvK2Generation.pairCone_eq_Q3_iff_drive_exact diff --git a/verification/lean-mathlib/OIBridge/EqvK2MaxCone.lean b/verification/lean-mathlib/OIBridge/EqvK2MaxCone.lean new file mode 100644 index 000000000..5b4b98c8e --- /dev/null +++ b/verification/lean-mathlib/OIBridge/EqvK2MaxCone.lean @@ -0,0 +1,236 @@ +/- + OIBridge/EqvK2MaxCone.lean — conditional pair-cone infrastructure (OI-PAIR-MAXCONE-1). + + Separate upper/lower pair-cone inclusions with explicit cone closure and maxCone; available sharp-product tests supply the upper bound. + + 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.EqvK2Generation +import OIBridge.EffectSpace + +namespace OIBridge +namespace EqvK2MaxCone + +open Matrix CompositeDimension MonoidalCompletion EqvK2Schema EqvK2Converse EqvK2Block +open scoped ComplexOrder + +noncomputable section + +/-- Symmetry of the real table pairing. -/ +theorem ipW_comm (ω η : W 3) : ipW ω η = ipW η ω := by + unfold ipW + apply Finset.sum_congr rfl + intro μ _ + apply Finset.sum_congr rfl + intro ν _ + exact mul_comm _ _ + +/-- The product-state table represents the unscaled product quadratic test. -/ +theorem ipW_prodState (ω : W 3) (x y : Fin 3 → ℝ) : + ipW ω (prodState x y) = pairVal (hom x) (hom y) ω := by + unfold ipW prodState pairVal + apply Finset.sum_congr rfl + intro μ _ + apply Finset.sum_congr rfl + intro ν _ + ring + +/-- A maxCone bound makes every product table a member of the dual. -/ +theorem products_mem_dualW_of_maxCone {K : Set (W 3)} + (hmax : K ⊆ maxCone (TransitiveBody.eball 3)) : + ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, + prodState x y ∈ dualW K := by + intro x hx y hy + rw [mem_dualW] + intro ω hω + rw [ipW_prodState] + exact pairVal_nonneg_of_maxCone (hmax hω) (lor_hom hx) (lor_hom hy) + +/-- The dual is closed under nonnegative scaling without a closedness assumption on K. -/ +theorem dualW_smul {K : Set (W 3)} (c : ℝ) (hc : 0 ≤ c) {ω : W 3} + (hω : ω ∈ dualW K) : c • ω ∈ dualW K := by + rw [mem_dualW] at hω ⊢ + intro η hη + rw [ipW_smul_right] + exact mul_nonneg hc (hω η hη) + +theorem blockMat_conjTranspose (U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ) : + (blockMat U₀ U₁)ᴴ = blockMat U₀ᴴ U₁ᴴ := by + have hP0 : P0ᴴ = P0 := by + ext i j + fin_cases i <;> fin_cases j <;> simp [P0] + have hP1 : P1ᴴ = P1 := by + ext i j + fin_cases i <;> fin_cases j <;> simp [P1] + simp only [blockMat, Matrix.conjTranspose_add, tensorOf_conjTranspose, hP0, hP1] + +/-- The inverse block action is the adjoint of the block action for the table pairing. -/ +theorem ipW_blockAct_adjoint (U₀ U₁ : Matrix (Fin 2) (Fin 2) ℂ) (ω η : W 3) : + ipW ω (blockAct U₀ U₁ η) = ipW (blockAct U₀ᴴ U₁ᴴ ω) η := by + apply Complex.ofReal_injective + rw [ipW_eq_trace, ipW_eq_trace, dict_blockAct, dict_blockAct] + rw [← blockMat_conjTranspose U₀ U₁, Matrix.conjTranspose_conjTranspose] + congr 1 + calc + Matrix.trace (dict ω * (blockMat U₀ U₁ * dict η * (blockMat U₀ U₁)ᴴ)) = + Matrix.trace ((dict ω * blockMat U₀ U₁ * dict η) * (blockMat U₀ U₁)ᴴ) := by + simp only [Matrix.mul_assoc] + _ = Matrix.trace ((blockMat U₀ U₁)ᴴ * (dict ω * blockMat U₀ U₁ * dict η)) := + Matrix.trace_mul_comm _ _ + _ = Matrix.trace (((blockMat U₀ U₁)ᴴ * dict ω * blockMat U₀ U₁) * dict η) := by + simp only [Matrix.mul_assoc] + +/-- Block invariance transfers to the dual through the available inverse block actions. -/ +theorem dualW_blockInvariant {K : Set (W 3)} (hB : BlockInvariant K) : + BlockInvariant (dualW K) := by + intro U₀ U₁ hU₀ hU₁ η hη + rw [mem_dualW] at hη ⊢ + intro ω hω + rw [ipW_blockAct_adjoint] + exact hη _ (hB U₀ᴴ U₁ᴴ (isSU_conjTranspose hU₀) (isSU_conjTranspose hU₁) ω hω) + +/-- Products and scaling suffice to carry the proved pure-state orbit into K. -/ +theorem pure_mem_of_products_scaling_block {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K) + (hB : BlockInvariant K) : + ∀ x : Fin 2 × Fin 2 → ℂ, ∃ ω ∈ K, dict ω = Matrix.vecMulVec x (star x) := by + intro x + obtain ⟨U₀, U₁, hU₀, hU₁, x₀, hx₀, c, hc, h⟩ := reach_block x + refine ⟨blockAct U₀ U₁ (c • prodState x₀ z3), + hB U₀ U₁ hU₀ hU₁ _ (hsmul c hc _ (hH1 x₀ hx₀ z3 z3_mem_eball)), ?_⟩ + rw [dict_blockAct, h] + +/-- LOWER: every PSD table is in K. Addition is explicit; no self-duality is used. -/ +theorem Q3_subset_of_products_cone_block {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K) + (hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K) + (hB : BlockInvariant K) : Q3 ⊆ K := + Q3_subset_of_pure hadd (pure_mem_of_products_scaling_block hH1 hsmul hB) + +/-- UPPER: product-test positivity and block invariance force every table in K to be PSD. +This inclusion does not assume that K contains products or is a cone. -/ +theorem subset_Q3_of_maxCone_block {K : Set (W 3)} + (hmax : K ⊆ maxCone (TransitiveBody.eball 3)) (hB : BlockInvariant K) : K ⊆ Q3 := by + have hpure := pure_mem_of_products_scaling_block (products_mem_dualW_of_maxCone hmax) + (fun c hc ω hω => dualW_smul c hc hω) (dualW_blockInvariant hB) + intro η hη + show (dict η).PosSemidef + refine posSemidef_dict_of_pure fun x => ?_ + obtain ⟨ω, hω, heq⟩ := hpure x + refine ⟨ω, heq, ?_⟩ + have h0 := mem_dualW.mp hω η hη + rw [ipW_comm] at h0 + exact h0 + +/-- The conditional block theorem with cone closure and maxCone replacing H3. -/ +theorem pairCone_eq_Q3_of_block_maxCone {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K) + (hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K) + (hmax : K ⊆ maxCone (TransitiveBody.eball 3)) (hB : BlockInvariant K) : K = Q3 := + Set.Subset.antisymm (subset_Q3_of_maxCone_block hmax hB) + (Q3_subset_of_products_cone_block hH1 hadd hsmul hB) + +/-- Forward witness for the block equivalence. -/ +theorem blockInvariant_of_eq_Q3 {K : Set (W 3)} (h : K = Q3) : BlockInvariant K := by + rw [h] + exact Q3_blockInvariant + +/-- Given the cone/product/maxCone premises, equality is equivalent to block invariance. +Witnesses: blockInvariant_of_eq_Q3 and pairCone_eq_Q3_of_block_maxCone. -/ +theorem pairCone_eq_Q3_iff_block_maxCone {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K) + (hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K) + (hmax : K ⊆ maxCone (TransitiveBody.eball 3)) : K = Q3 ↔ BlockInvariant K := + ⟨blockInvariant_of_eq_Q3, pairCone_eq_Q3_of_block_maxCone hH1 hadd hsmul hmax⟩ + +/-- Generator form: exact CNOT and full-flow/cyclic invariance generate the needed blocks. -/ +theorem pairCone_eq_Q3_of_drive_maxCone {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K) + (hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K) + (hmax : K ⊆ maxCone (TransitiveBody.eball 3)) + (hH2 : ∀ ω ∈ K, cnot ω ∈ K) + (hA : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) : K = Q3 := + pairCone_eq_Q3_of_block_maxCone hH1 hadd hsmul hmax + (EqvK2Generation.blockInvariant_of_drive hH2 hA) + +/-- Forward witness for the generator equivalence. -/ +theorem driveInvariant_of_eq_Q3 {K : Set (W 3)} (h : K = Q3) : + (∀ ω ∈ K, cnot ω ∈ K) ∧ ∀ t : ℝ, ∀ ω ∈ K, + actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K := by + rw [h] + exact ⟨EqvK2Generation.Q3_cnot, Q3_aMiss⟩ + +/-- Given cone/product/maxCone premises, equality is equivalent to the full generator invariance. +Witnesses: driveInvariant_of_eq_Q3 and pairCone_eq_Q3_of_drive_maxCone. -/ +theorem pairCone_eq_Q3_iff_drive_maxCone {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K) + (hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K) + (hmax : K ⊆ maxCone (TransitiveBody.eball 3)) : + K = Q3 ↔ ((∀ ω ∈ K, cnot ω ∈ K) ∧ ∀ t : ℝ, ∀ ω ∈ K, + actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) := + ⟨driveInvariant_of_eq_Q3, fun ⟨hH2, hA⟩ => + pairCone_eq_Q3_of_drive_maxCone hH1 hadd hsmul hmax hH2 hA⟩ + +/-- EFF-1's sharp-product tests suffice for the upper inclusion. -/ +theorem subset_Q3_of_sharp_products_block {K : Set (W 3)} + (hsharp : K ⊆ EffectSpace.maxConeOf (EffectSpace.sharpFamily 3)) + (hB : BlockInvariant K) : K ⊆ Q3 := + subset_Q3_of_maxCone_block (fun _ hω => + EffectSpace.maxConeOf_sharp_subset_maxCone (by norm_num) (hsharp hω)) hB + +/-- Validity on an available family containing the sharp tests supplies the maxCone bound. +Only this inclusion is used: no EffectsOn or full-affine-effect availability is assumed. -/ +theorem maxCone_bound_of_sharp_available {K : Set (W 3)} + {avail : Set ((Fin 3 → ℝ) →ᵃ[ℝ] ℝ)} + (hvalid : K ⊆ EffectSpace.maxConeOf avail) + (hsharp : EffectSpace.sharpFamily 3 ⊆ avail) : + K ⊆ maxCone (TransitiveBody.eball 3) := fun _ hω => + EffectSpace.maxConeOf_sharp_subset_maxCone (by norm_num) + (EffectSpace.maxConeOf_anti hsharp (hvalid hω)) + +/-- The generator theorem in the available-sharp-test reading. +The actual pair validity and the inclusion of sharp tests remain explicit hypotheses. -/ +theorem pairCone_eq_Q3_of_sharp_available {K : Set (W 3)} + {avail : Set ((Fin 3 → ℝ) →ᵃ[ℝ] ℝ)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K) + (hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K) + (hvalid : K ⊆ EffectSpace.maxConeOf avail) + (hsharp : EffectSpace.sharpFamily 3 ⊆ avail) + (hH2 : ∀ ω ∈ K, cnot ω ∈ K) + (hA : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) : K = Q3 := + pairCone_eq_Q3_of_drive_maxCone hH1 hadd hsmul + (maxCone_bound_of_sharp_available hvalid hsharp) hH2 hA + +end +end EqvK2MaxCone +end OIBridge + +#print axioms OIBridge.EqvK2MaxCone.ipW_prodState +#print axioms OIBridge.EqvK2MaxCone.products_mem_dualW_of_maxCone +#print axioms OIBridge.EqvK2MaxCone.ipW_blockAct_adjoint +#print axioms OIBridge.EqvK2MaxCone.dualW_blockInvariant +#print axioms OIBridge.EqvK2MaxCone.pure_mem_of_products_scaling_block +#print axioms OIBridge.EqvK2MaxCone.Q3_subset_of_products_cone_block +#print axioms OIBridge.EqvK2MaxCone.subset_Q3_of_maxCone_block +#print axioms OIBridge.EqvK2MaxCone.pairCone_eq_Q3_of_block_maxCone +#print axioms OIBridge.EqvK2MaxCone.blockInvariant_of_eq_Q3 +#print axioms OIBridge.EqvK2MaxCone.pairCone_eq_Q3_iff_block_maxCone +#print axioms OIBridge.EqvK2MaxCone.pairCone_eq_Q3_of_drive_maxCone +#print axioms OIBridge.EqvK2MaxCone.driveInvariant_of_eq_Q3 +#print axioms OIBridge.EqvK2MaxCone.pairCone_eq_Q3_iff_drive_maxCone +#print axioms OIBridge.EqvK2MaxCone.subset_Q3_of_sharp_products_block +#print axioms OIBridge.EqvK2MaxCone.maxCone_bound_of_sharp_available +#print axioms OIBridge.EqvK2MaxCone.pairCone_eq_Q3_of_sharp_available diff --git a/verification/lean-mathlib/OIBridge/EqvK2Schema.lean b/verification/lean-mathlib/OIBridge/EqvK2Schema.lean new file mode 100644 index 000000000..c634beb82 --- /dev/null +++ b/verification/lean-mathlib/OIBridge/EqvK2Schema.lean @@ -0,0 +1,451 @@ +/- + OIBridge/EqvK2Schema.lean — conditional pair-cone infrastructure (OI-PAIR-MAXCONE-1). + + The real table / Hermitian matrix dictionary, trace pairing, pure-state cone inclusions, and the conditional H3 drive schema. + + 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.CompositeDimension +import OIBridge.BoundaryAudit +import Mathlib.LinearAlgebra.Matrix.PosDef + +namespace OIBridge +namespace EqvK2Schema + +open Matrix CompositeDimension MonoidalCompletion +open scoped ComplexOrder + +noncomputable section + +/-! ### §A — the Pauli matrices -/ + +/-- The Pauli matrices `σ₀ = 1, σ₁ = X, σ₂ = Y, σ₃ = Z` (the bridge draft's `pauli`, verbatim). -/ +noncomputable def pauli : Fin 4 → Matrix (Fin 2) (Fin 2) ℂ := + ![1, !![0, 1; 1, 0], !![0, -Complex.I; Complex.I, 0], !![1, 0; 0, -1]] + +/-- Each Pauli matrix is Hermitian. -/ +theorem pauli_conjTranspose (μ : Fin 4) : (pauli μ)ᴴ = pauli μ := by + fin_cases μ <;> (ext i j; fin_cases i <;> fin_cases j <;> simp [pauli, Matrix.one_apply]) + +/-- Orthogonality of the Pauli matrices under the trace pairing. -/ +theorem trace_pauli_mul (μ ν : Fin 4) : + Matrix.trace (pauli μ * pauli ν) = if μ = ν then 2 else 0 := by + fin_cases μ <;> fin_cases ν <;> + simp +decide [pauli, Matrix.trace_fin_two, Matrix.mul_apply, Fin.sum_univ_two, + Matrix.one_apply] <;> norm_num + +/-- Completeness of the Pauli matrices, entrywise. -/ +theorem pauli_complete (a b c d : Fin 2) : + ∑ μ : Fin 4, pauli μ a b * pauli μ c d = if a = d ∧ b = c then 2 else 0 := by + fin_cases a <;> fin_cases b <;> fin_cases c <;> fin_cases d <;> + simp +decide [pauli, Fin.sum_univ_four, Matrix.one_apply] <;> norm_num + +/-! ### §B — the kernel tensor on one-token matrices -/ + +theorem tensorOf_mul (A B C D : Matrix (Fin 2) (Fin 2) ℂ) : + tensorOf A B * tensorOf C D = tensorOf (A * C) (B * D) := by + ext ⟨a1, a2⟩ ⟨b1, b2⟩ + simp only [Matrix.mul_apply, tensorOf_apply, Fintype.sum_prod_type, Fin.sum_univ_two] + ring + +theorem trace_tensorOf (A B : Matrix (Fin 2) (Fin 2) ℂ) : + Matrix.trace (tensorOf A B) = Matrix.trace A * Matrix.trace B := by + simp only [Matrix.trace, Matrix.diag_apply, tensorOf_apply, Fintype.sum_prod_type, + Fin.sum_univ_two] + ring + +theorem tensorOf_conjTranspose (A B : Matrix (Fin 2) (Fin 2) ℂ) : + (tensorOf A B)ᴴ = tensorOf Aᴴ Bᴴ := by + ext ⟨a1, a2⟩ ⟨b1, b2⟩ + simp only [Matrix.conjTranspose_apply, tensorOf_apply] + exact star_mul' _ _ + +/-- Orthogonality of the Pauli tensors. -/ +theorem trace_T_mul_T (μ ν μ' ν' : Fin 4) : + Matrix.trace (tensorOf (pauli μ) (pauli ν) * tensorOf (pauli μ') (pauli ν')) = + (if μ = μ' then 2 else 0) * (if ν = ν' then 2 else 0) := by + rw [tensorOf_mul, trace_tensorOf, trace_pauli_mul, trace_pauli_mul] + +/-! ### §C — the dictionary and its compatibilities -/ + +/-- One token's homogenized vector as a 2 × 2 complex matrix: `v ↦ ½ Σ v_μ σ_μ` (bridge draft). -/ +noncomputable def tokMat (v : HVec 3) : Matrix (Fin 2) (Fin 2) ℂ := + ∑ μ : Fin 4, ((v μ : ℂ) / 2) • pauli μ + +/-- The two-token dictionary: `ω ↦ ¼ Σ ω_μν σ_μ ⊗ σ_ν` (bridge draft). -/ +noncomputable def dict (ω : W 3) : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ := + ∑ μ : Fin 4, ∑ ν : Fin 4, ((ω μ ν : ℂ) / 4) • tensorOf (pauli μ) (pauli ν) + +/-- **The product law of the dictionary.** -/ +theorem dict_tens (X Y : HVec 3) : dict (tens X Y) = tensorOf (tokMat X) (tokMat Y) := by + ext ⟨i, j⟩ ⟨k, l⟩ + simp only [dict, tokMat, tens_apply, Matrix.sum_apply, Matrix.add_apply, Matrix.smul_apply, + tensorOf_apply, smul_eq_mul, Complex.ofReal_mul, Fin.sum_univ_four] + ring + +/-- **First compatibility**: product states of the ball go to Kronecker products. -/ +theorem dict_prodState (x y : Fin 3 → ℝ) : + dict (prodState x y) = tensorOf (tokMat (hom x)) (tokMat (hom y)) := + dict_tens (hom x) (hom y) + +theorem dict_add (ω η : W 3) : dict (ω + η) = dict ω + dict η := by + ext a b + simp only [dict, Matrix.add_apply, Matrix.sum_apply, Matrix.smul_apply, Pi.add_apply, + smul_eq_mul, Complex.ofReal_add, Fin.sum_univ_four] + ring + +theorem dict_smul (c : ℝ) (ω : W 3) : dict (c • ω) = c • dict ω := by + ext a b + simp only [dict, Matrix.sum_apply, Matrix.add_apply, Matrix.smul_apply, Pi.smul_apply, + smul_eq_mul, Complex.real_smul, Complex.ofReal_mul, Fin.sum_univ_four] + ring + +/-- The dictionary as a real linear map. -/ +noncomputable def dictLin : W 3 →ₗ[ℝ] Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ where + toFun := dict + map_add' := dict_add + map_smul' := dict_smul + +theorem dict_sum {ι : Type*} (s : Finset ι) (g : ι → W 3) : + dict (∑ k ∈ s, g k) = ∑ k ∈ s, dict (g k) := + map_sum dictLin g s + +theorem star_ofReal_div_four (r : ℝ) : star ((r : ℂ) / 4) = (r : ℂ) / 4 := by + have h : (starRingEnd ℂ) ((r : ℂ) / 4) = (r : ℂ) / 4 := + Complex.conj_eq_iff_real.mpr ⟨r / 4, by norm_num⟩ + rwa [starRingEnd_apply] at h + +/-- The dictionary image of a table is Hermitian. -/ +theorem dict_conjTranspose (ω : W 3) : (dict ω)ᴴ = dict ω := by + simp only [dict, Matrix.conjTranspose_sum, Matrix.conjTranspose_smul, tensorOf_conjTranspose, + pauli_conjTranspose, star_ofReal_div_four] + +theorem dict_isHermitian (ω : W 3) : (dict ω).IsHermitian := + dict_conjTranspose ω + +/-- The coordinate functionals read the dictionary back. -/ +theorem trace_T_mul_dict (η : W 3) (μ ν : Fin 4) : + Matrix.trace (tensorOf (pauli μ) (pauli ν) * dict η) = (η μ ν : ℂ) := by + simp only [dict, Finset.mul_sum, Matrix.mul_smul, Matrix.trace_sum, Matrix.trace_smul, + trace_T_mul_T, smul_eq_mul] + fin_cases μ <;> fin_cases ν <;> simp [Fin.sum_univ_four] <;> ring + +theorem dict_mul_left (ω : W 3) (M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : + dict ω * M = + ∑ μ : Fin 4, ∑ ν : Fin 4, ((ω μ ν : ℂ) / 4) • (tensorOf (pauli μ) (pauli ν) * M) := by + simp only [dict, Finset.sum_mul, Matrix.smul_mul] + +/-- The Euclidean table pairing of the joint carrier. -/ +def ipW (ω η : W 3) : ℝ := ∑ μ : Fin 4, ∑ ν : Fin 4, ω μ ν * η μ ν + +theorem trace_dict_mul (ω η : W 3) : + Matrix.trace (dict ω * dict η) = ((ipW ω η : ℝ) : ℂ) / 4 := by + rw [dict_mul_left] + simp only [Matrix.trace_sum, Matrix.trace_add, Matrix.trace_smul, trace_T_mul_dict, smul_eq_mul, + ipW, Complex.ofReal_sum, Complex.ofReal_mul, Complex.ofReal_add, Fin.sum_univ_four] + ring + +/-- **Second compatibility**: the table pairing is four times the trace pairing. -/ +theorem ipW_eq_trace (ω η : W 3) : + ((ipW ω η : ℝ) : ℂ) = 4 * Matrix.trace (dict ω * dict η) := by + rw [trace_dict_mul] + ring + +/-- The coordinates of a matrix in the Pauli tensors. -/ +def coordOf (H : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : Fin 4 → Fin 4 → ℝ := + fun μ ν => (Matrix.trace (tensorOf (pauli μ) (pauli ν) * H)).re + +theorem coordOf_dict (ω : W 3) : coordOf (dict ω) = ω := by + funext μ ν + simp only [coordOf, trace_T_mul_dict, Complex.ofReal_re] + +theorem dict_injective : Function.Injective dict := fun ω η h => by + have h2 := congrArg coordOf h + rwa [coordOf_dict, coordOf_dict] at h2 + +/-! ### §D — completeness, and the linear equivalence with the Hermitian matrices -/ + +set_option maxHeartbeats 2000000 in +theorem sum_T_entry (H : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (a1 a2 b1 b2 : Fin 2) : + (∑ μ : Fin 4, ∑ ν : Fin 4, Matrix.trace (tensorOf (pauli μ) (pauli ν) * H) * + tensorOf (pauli μ) (pauli ν) (a1, a2) (b1, b2)) = + ∑ p1 : Fin 2, ∑ p2 : Fin 2, ∑ q1 : Fin 2, ∑ q2 : Fin 2, H (q1, q2) (p1, p2) * + ((∑ μ : Fin 4, pauli μ p1 q1 * pauli μ a1 b1) * + (∑ ν : Fin 4, pauli ν p2 q2 * pauli ν a2 b2)) := by + simp only [Matrix.trace, Matrix.diag_apply, Matrix.mul_apply, tensorOf_apply, + Fintype.sum_prod_type, Fin.sum_univ_two, Fin.sum_univ_four] + ring + +set_option maxHeartbeats 2000000 in +/-- **Completeness of the Pauli tensors.** -/ +theorem dict_complete4 (H : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : + ∑ μ : Fin 4, ∑ ν : Fin 4, Matrix.trace (tensorOf (pauli μ) (pauli ν) * H) • + tensorOf (pauli μ) (pauli ν) = (4 : ℂ) • H := by + ext ⟨a1, a2⟩ ⟨b1, b2⟩ + simp only [Matrix.sum_apply, Matrix.smul_apply, smul_eq_mul] + rw [sum_T_entry] + simp only [pauli_complete] + fin_cases a1 <;> fin_cases a2 <;> fin_cases b1 <;> fin_cases b2 <;> + simp [Fin.sum_univ_two] <;> ring + +/-- The Pauli coordinates of a Hermitian matrix are real. -/ +theorem trace_T_mul_real (H : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (hH : H.IsHermitian) + (μ ν : Fin 4) : + (((Matrix.trace (tensorOf (pauli μ) (pauli ν) * H)).re : ℝ) : ℂ) = + Matrix.trace (tensorOf (pauli μ) (pauli ν) * H) := by + rw [← Complex.conj_eq_iff_re, starRingEnd_apply, ← Matrix.trace_conjTranspose, + Matrix.conjTranspose_mul, hH.eq, tensorOf_conjTranspose, pauli_conjTranspose, + pauli_conjTranspose, Matrix.trace_mul_comm] + +/-- The dictionary of the coordinates of a Hermitian matrix is the matrix. -/ +theorem dict_coordOf (H : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) (hH : H.IsHermitian) : + dict (coordOf H) = H := by + have h4 := dict_complete4 H + have hr := trace_T_mul_real H hH + ext a b + have hab := congrFun (congrFun h4 a) b + simp only [Matrix.sum_apply, Matrix.add_apply, Matrix.smul_apply, smul_eq_mul, + Fin.sum_univ_four] at hab + simp only [dict, coordOf, hr, Matrix.sum_apply, Matrix.add_apply, Matrix.smul_apply, + smul_eq_mul, Fin.sum_univ_four] + linear_combination hab / 4 + +/-- **The dictionary as a linear equivalence** `W 3 ≃ Herm(ℂ² ⊗ ℂ²)`. -/ +noncomputable def dictEquiv : + W 3 ≃ₗ[ℝ] selfAdjoint (Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) where + toFun ω := ⟨dict ω, selfAdjoint.mem_iff.mpr + (Matrix.isHermitian_iff_isSelfAdjoint.mp (dict_isHermitian ω))⟩ + map_add' ω η := Subtype.ext (dict_add ω η) + map_smul' c ω := Subtype.ext (dict_smul c ω) + invFun H := coordOf H.1 + left_inv ω := coordOf_dict ω + right_inv H := Subtype.ext (dict_coordOf H.1 + (Matrix.isHermitian_iff_isSelfAdjoint.mpr (selfAdjoint.mem_iff.mp H.2))) + +theorem dictEquiv_apply (ω : W 3) : (dictEquiv ω : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) = + dict ω := rfl + +/-! ### §E — the cone step -/ + +/-- The dual of a set of tables under the table pairing. -/ +def dualW (K : Set (W 3)) : Set (W 3) := {η | ∀ ω ∈ K, 0 ≤ ipW ω η} + +theorem mem_dualW {K : Set (W 3)} {η : W 3} : η ∈ dualW K ↔ ∀ ω ∈ K, 0 ≤ ipW ω η := + Iff.rfl + +/-- `Q3`: the tables whose dictionary image is positive semidefinite. -/ +def Q3 : Set (W 3) := {ω | (dict ω).PosSemidef} + +theorem mem_Q3 {ω : W 3} : ω ∈ Q3 ↔ (dict ω).PosSemidef := Iff.rfl + +theorem ipW_add_right (ω η ζ : W 3) : ipW ω (η + ζ) = ipW ω η + ipW ω ζ := by + simp only [ipW, Pi.add_apply, Fin.sum_univ_four] + ring + +theorem ipW_smul_right (c : ℝ) (ω η : W 3) : ipW ω (c • η) = c * ipW ω η := by + simp only [ipW, Pi.smul_apply, smul_eq_mul, Fin.sum_univ_four] + ring + +theorem trace_vecMulVec_mul (x : Fin 2 × Fin 2 → ℂ) + (M : Matrix (Fin 2 × Fin 2) (Fin 2 × Fin 2) ℂ) : + Matrix.trace (Matrix.vecMulVec x (star x) * M) = star x ⬝ᵥ (M *ᵥ x) := by + simp only [Matrix.trace, Matrix.diag_apply, Matrix.mul_apply, Matrix.vecMulVec_apply, + dotProduct, Matrix.mulVec, Pi.star_apply, Fintype.sum_prod_type, Fin.sum_univ_two] + ring + +/-- A table whose pairing with a table of every rank-one positive matrix is nonnegative has a +positive semidefinite dictionary image. -/ +theorem posSemidef_dict_of_pure {η : W 3} + (h : ∀ x : Fin 2 × Fin 2 → ℂ, + ∃ ω : W 3, dict ω = Matrix.vecMulVec x (star x) ∧ 0 ≤ ipW ω η) : + (dict η).PosSemidef := by + refine Matrix.PosSemidef.of_dotProduct_mulVec_nonneg (dict_isHermitian η) fun x => ?_ + obtain ⟨ω, hω, h0⟩ := h x + have htr : star x ⬝ᵥ (dict η *ᵥ x) = ((ipW ω η : ℝ) : ℂ) / 4 := by + rw [← trace_vecMulVec_mul, ← hω, trace_dict_mul] + rw [htr, Complex.nonneg_iff, Complex.div_ofNat_re, Complex.div_ofNat_im, Complex.ofReal_re, + Complex.ofReal_im] + exact ⟨div_nonneg h0 (by norm_num), by norm_num⟩ + +/-- **UPPER.** A set containing a table of every rank-one positive matrix and lying in its own +dual lies in `Q3`. -/ +theorem subset_Q3_of_pure_dual {K : Set (W 3)} + (hpure : ∀ x : Fin 2 × Fin 2 → ℂ, ∃ ω ∈ K, dict ω = Matrix.vecMulVec x (star x)) + (hdual : K ⊆ dualW K) : K ⊆ Q3 := by + intro η hη + show (dict η).PosSemidef + refine posSemidef_dict_of_pure fun x => ?_ + obtain ⟨ω, hωK, hω⟩ := hpure x + exact ⟨ω, hω, mem_dualW.mp (hdual hη) ω hωK⟩ + +/-- **LOWER.** A set closed under addition and containing a table of every rank-one positive matrix +contains `Q3`. -/ +theorem Q3_subset_of_pure {K : Set (W 3)} + (hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K) + (hpure : ∀ x : Fin 2 × Fin 2 → ℂ, ∃ ω ∈ K, dict ω = Matrix.vecMulVec x (star x)) : + Q3 ⊆ K := by + intro ω hω + have hω' : (dict ω).PosSemidef := hω + obtain ⟨B, hB⟩ := BoundaryAudit.psdFactorization_discharged (Fin 2 × Fin 2) (dict ω) hω' + choose f hfK hf using hpure + have hsum : dict ω = ∑ k : Fin 2 × Fin 2, dict (f (fun i => B i k)) := by + rw [hB] + ext i j + simp only [hf, Matrix.mul_apply, Matrix.conjTranspose_apply, Matrix.sum_apply, + Matrix.vecMulVec_apply, Pi.star_apply] + have heq : ω = ∑ k : Fin 2 × Fin 2, f (fun i => B i k) := by + apply dict_injective + rw [hsum, dict_sum] + rw [heq] + exact Finset.sum_induction_nonempty (fun k => f (fun i => B i k)) (· ∈ K) + (fun a b ha hb => hadd a ha b hb) Finset.univ_nonempty (fun k _ => hfK _) + +/-- Positive control, first inclusion: `Q3` lies in its dual. -/ +theorem Q3_subset_dualW : Q3 ⊆ dualW Q3 := by + intro η hη + rw [mem_dualW] + intro ω hω + have hη' : (dict η).PosSemidef := hη + have hω' : (dict ω).PosSemidef := hω + obtain ⟨B, hB⟩ := BoundaryAudit.psdFactorization_discharged (Fin 2 × Fin 2) (dict ω) hω' + have hdec : dict ω = ∑ k : Fin 2 × Fin 2, + Matrix.vecMulVec (fun i => B i k) (star fun i => B i k) := by + rw [hB] + ext i j + simp only [Matrix.mul_apply, Matrix.conjTranspose_apply, Matrix.sum_apply, + Matrix.vecMulVec_apply, Pi.star_apply] + have htr : Matrix.trace (dict ω * dict η) = + ∑ k : Fin 2 × Fin 2, star (fun i => B i k) ⬝ᵥ (dict η *ᵥ fun i => B i k) := by + rw [hdec, Finset.sum_mul, Matrix.trace_sum] + simp only [trace_vecMulVec_mul] + have hre : (Matrix.trace (dict ω * dict η)).re = ipW ω η / 4 := by + rw [trace_dict_mul, Complex.div_ofNat_re, Complex.ofReal_re] + have hnn : 0 ≤ (Matrix.trace (dict ω * dict η)).re := by + rw [htr, Complex.re_sum] + exact Finset.sum_nonneg fun k _ => + (Complex.nonneg_iff.mp (hη'.dotProduct_mulVec_nonneg _)).1 + linarith + +/-- Positive control, second inclusion: the dual of `Q3` lies in `Q3`. -/ +theorem dualW_Q3_subset : dualW Q3 ⊆ Q3 := by + intro η hη + show (dict η).PosSemidef + refine posSemidef_dict_of_pure fun x => ⟨coordOf (Matrix.vecMulVec x (star x)), ?_, ?_⟩ + · exact dict_coordOf _ (Matrix.posSemidef_vecMulVec_self_star x).isHermitian + · refine mem_dualW.mp hη _ ?_ + show (dict (coordOf (Matrix.vecMulVec x (star x)))).PosSemidef + rw [dict_coordOf _ (Matrix.posSemidef_vecMulVec_self_star x).isHermitian] + exact Matrix.posSemidef_vecMulVec_self_star x + +/-- **Positive control for H3**: `Q3` is self-dual under the table pairing. -/ +theorem Q3_selfDual : Q3 = dualW Q3 := + Set.Subset.antisymm Q3_subset_dualW dualW_Q3_subset + +/-! ### §F — the drive words and the assembly -/ + +/-- `N` acting on the target token, as a linear map of the pair carrier. -/ +noncomputable def actTLin (N : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) : W 3 →ₗ[ℝ] W 3 where + toFun := actT N + map_add' ω η := by + funext μ ν + simp only [actT_apply, Pi.add_apply, map_add] + map_smul' c ω := by + funext μ ν + simp only [actT_apply, Pi.smul_apply, map_smul, RingHom.id_apply] + +/-- The generators: `cnot`, the target token's rotations about the third axis (the linear part of +`ball3Drive`'s flow) and its cyclic permutation (`ball3Drive`'s `J`). -/ +noncomputable def driveGens : Set (Module.End ℝ (W 3)) := + {(cnot : W 3 →ₗ[ℝ] W 3)} ∪ Set.range (fun t : ℝ => actTLin (KInfFoundations.rotLin t)) ∪ + {actTLin (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ))} + +/-- The drive words: the monoid the generators generate. -/ +noncomputable def driveWords : Submonoid (Module.End ℝ (W 3)) := Submonoid.closure driveGens + +/-- H2 and A_miss make a set invariant under every drive word. -/ +theorem driveWords_preserve {K : Set (W 3)} (hH2 : ∀ ω ∈ K, cnot ω ∈ K) + (hA : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) + {g : Module.End ℝ (W 3)} (hg : g ∈ driveWords) : ∀ ω ∈ K, g ω ∈ K := by + induction hg using Submonoid.closure_induction with + | mem g hg => + intro ω hω + simp only [driveGens, Set.mem_union, Set.mem_singleton_iff, Set.mem_range] at hg + rcases hg with (rfl | ⟨t, rfl⟩) | rfl + · exact hH2 ω hω + · exact (hA t ω hω).1 + · exact (hA 0 ω hω).2 + | one => intro ω hω; exact hω + | mul g h _ _ ihg ihh => intro ω hω; exact ihg _ (ihh _ hω) + +/-- **L4, as a hypothesis**: every pure two-token state is, up to a nonnegative scale, the image of a +product state of the ball under a drive word. -/ +def ReachPure : Prop := + ∀ x : Fin 2 × Fin 2 → ℂ, ∃ g ∈ driveWords, ∃ x₀ ∈ TransitiveBody.eball 3, + ∃ y₀ ∈ TransitiveBody.eball 3, ∃ c : ℝ, 0 ≤ c ∧ + dict (c • g (prodState x₀ y₀)) = Matrix.vecMulVec x (star x) + +/-- **The pair-level K2 schema.** Products (H1), `cnot`-invariance (H2), self-duality (H3) and +invariance under one token's rotations about the third axis and its cyclic permutation (A_miss) force +the pair cone to be `Q3`, given the reachability statement `ReachPure`. -/ +theorem pairCone_eq_Q3_of_drive {K : Set (W 3)} + (hH1 : ∀ x ∈ TransitiveBody.eball 3, ∀ y ∈ TransitiveBody.eball 3, prodState x y ∈ K) + (hH2 : ∀ ω ∈ K, cnot ω ∈ K) + (hH3 : K = dualW K) + (hA : ∀ t : ℝ, ∀ ω ∈ K, actT (KInfFoundations.rotLin t) ω ∈ K ∧ + actT (KInfFoundations.cycEquiv : (Fin 3 → ℝ) →ₗ[ℝ] (Fin 3 → ℝ)) ω ∈ K) + (hreach : ReachPure) : + K = Q3 := by + have hK : ∀ ω, ω ∈ K ↔ ω ∈ dualW K := fun ω => Set.ext_iff.mp hH3 ω + have hsmul : ∀ c : ℝ, 0 ≤ c → ∀ ω ∈ K, c • ω ∈ K := by + intro c hc ω hω + rw [hK] at hω ⊢ + rw [mem_dualW] at hω ⊢ + intro η hη + rw [ipW_smul_right] + exact mul_nonneg hc (hω η hη) + have hadd : ∀ ω ∈ K, ∀ η ∈ K, ω + η ∈ K := by + intro ω hω η hη + rw [hK] at hω hη ⊢ + rw [mem_dualW] at hω hη ⊢ + intro ζ hζ + rw [ipW_add_right] + exact add_nonneg (hω ζ hζ) (hη ζ hζ) + have hpure : ∀ x : Fin 2 × Fin 2 → ℂ, ∃ ω ∈ K, dict ω = Matrix.vecMulVec x (star x) := by + intro x + obtain ⟨g, hg, x₀, hx₀, y₀, hy₀, c, hc, h⟩ := hreach x + exact ⟨c • g (prodState x₀ y₀), + hsmul c hc _ (driveWords_preserve hH2 hA hg _ (hH1 x₀ hx₀ y₀ hy₀)), h⟩ + apply Set.Subset.antisymm + · exact subset_Q3_of_pure_dual hpure fun ω hω => (hK ω).mp hω + · exact Q3_subset_of_pure hadd hpure + +end + +end EqvK2Schema +end OIBridge + +#print axioms OIBridge.EqvK2Schema.pauli_conjTranspose +#print axioms OIBridge.EqvK2Schema.trace_pauli_mul +#print axioms OIBridge.EqvK2Schema.pauli_complete +#print axioms OIBridge.EqvK2Schema.trace_T_mul_T +#print axioms OIBridge.EqvK2Schema.dict_tens +#print axioms OIBridge.EqvK2Schema.dict_prodState +#print axioms OIBridge.EqvK2Schema.dict_sum +#print axioms OIBridge.EqvK2Schema.dict_isHermitian +#print axioms OIBridge.EqvK2Schema.trace_T_mul_dict +#print axioms OIBridge.EqvK2Schema.trace_dict_mul +#print axioms OIBridge.EqvK2Schema.ipW_eq_trace +#print axioms OIBridge.EqvK2Schema.dict_injective +#print axioms OIBridge.EqvK2Schema.dict_complete4 +#print axioms OIBridge.EqvK2Schema.dict_coordOf +#print axioms OIBridge.EqvK2Schema.dictEquiv +#print axioms OIBridge.EqvK2Schema.trace_vecMulVec_mul +#print axioms OIBridge.EqvK2Schema.posSemidef_dict_of_pure +#print axioms OIBridge.EqvK2Schema.subset_Q3_of_pure_dual +#print axioms OIBridge.EqvK2Schema.Q3_subset_of_pure +#print axioms OIBridge.EqvK2Schema.Q3_selfDual +#print axioms OIBridge.EqvK2Schema.driveWords_preserve +#print axioms OIBridge.EqvK2Schema.pairCone_eq_Q3_of_drive diff --git a/verification/lean/oi_maxcone_check.py b/verification/lean/oi_maxcone_check.py new file mode 100644 index 000000000..09d2abcd6 --- /dev/null +++ b/verification/lean/oi_maxcone_check.py @@ -0,0 +1,181 @@ +#!/usr/bin/env python3 +"""Finite independent exact controls for the MaxCone design proof, in Q(i).""" +import argparse +import importlib.util +import itertools +import sys +from collections import Counter +from fractions import Fraction as R +from functools import lru_cache +from pathlib import Path + +spec = importlib.util.spec_from_file_location('maxcone_gaussian', Path(__file__).with_name('oi_maxcone_gaussian.py')) +g = importlib.util.module_from_spec(spec) +sys.modules[spec.name] = g +spec.loader.exec_module(g) +G, I = g.G, g.I +matrix, eye, diag, add, scale, mul, adj = g.matrix, g.eye, g.diag, g.add, g.scale, g.mul, g.adj +tensor, trace, det, rank, extract = g.tensor, g.trace, g.det, g.rank, g.extract +E = eye(2) +pauli = [E, matrix([[0, 1], [1, 0]]), matrix([[0, -I], [I, 0]]), diag(1, -1)] +P0, P1 = diag(1, 0), diag(0, 1) +CNOT = matrix([[1, 0, 0, 0], [0, 1, 0, 0], [0, 0, 0, 1], [0, 0, 1, 0]]) +count = Counter() + + +def require(code, condition): + if not bool(condition): + raise AssertionError(code) + count[code] += 1 + + +def inner(A, B): + return trace(mul(A, B)) + + +def vec(v): + return matrix([[a] for a in v]) + + +def outer(v): + return mul(v, adj(v)) + + +def conj(B, A): + return mul(mul(B, A), adj(B)) + + +def block(U, V): + return add(tensor(P0, U), tensor(P1, V)) + + +def bloch(v): + A = E + for j in range(3): + A = add(A, scale(v[j], pauli[j + 1])) + return scale(R(1, 2), A) + + +@lru_cache(maxsize=None) +def table(A): + return tuple(tuple(inner(tensor(pauli[j], pauli[k]), A) for k in range(4)) for j in range(4)) + + +def ip(A, B): + a, b = table(A), table(B) + return sum(a[j][k] * b[j][k] for j in range(4) for k in range(4)) + + +def psd(A): + return A == adj(A) and all(det(extract(A, ix)).nonnegative() + for n in range(1, 5) for ix in itertools.combinations(range(4), n)) + + +def partial_transpose(A): + return matrix([[A[2 * (j // 2) + k % 2][2 * (k // 2) + j % 2] + for k in range(4)] for j in range(4)]) + + +def su_to(v, norm): + if norm == 0: + return E + return scale(R(1, norm), matrix([[v[0][0].conj(), v[1][0].conj()], [-v[1][0], v[0][0]]])) + + +def run(mutation=None): + count.clear() + basis = [scale(R(1, 4), tensor(a, b)) for a in pauli for b in pauli] + factor = 8 if mutation == 'trace-factor' else 4 + for A, B in itertools.product(basis, repeat=2): + require('TRACE', ip(A, B) == factor * inner(A, B)) + directions = [(0, 0, 0), (1, 0, 0), (-1, 0, 0), (0, 1, 0), (0, -1, 0), + (0, 0, 1), (0, 0, -1), (R(3, 5), R(4, 5), 0), (R(1, 3), R(2, 3), R(2, 3))] + for x, y in itertools.product(directions, repeat=2): + A = tensor(bloch(x), bloch(y)) + require('PRODUCT-PSD', psd(A)) + require('PRODUCT-RANK', rank(A) in (1, 2, 4)) + homx, homy = (1,) + x, (1,) + y + for T in basis: + raw = sum(homx[j] * table(T)[j][k] * homy[k] for j in range(4) for k in range(4)) + require('PRODUCT-PAIR', raw == ip(T, A) == 4 * inner(T, A)) + + vectors = [(1, 0), (0, 1), (I, 0), (R(3, 5), R(4, 5)), + (3 * I / 5, R(4, 5)), (R(1, 3), R(2, 3) + 2 * I / 3)] + entries = [(vec((0, 0)), 0)] + entries += [(scale(t, vec(v)), t) for v in vectors for t in (1, 2)] + for (a, na), (b, nb) in itertools.product(entries, repeat=2): + Ua, Ub = su_to(a, na), su_to(b, nb) + require('SU', mul(Ua, adj(Ua)) == E and det(Ua) == 1) + require('SU', mul(Ub, adj(Ub)) == E and det(Ub) == 1) + psi, prod = a + b, vec((na, 0, nb, 0)) + B = block(adj(Ua), adj(Ub)) + require('PURE-ORBIT', mul(B, prod) == psi) + require('PURE-PROJECTOR', conj(B, outer(prod)) == outer(psi)) + c = na ** 2 + nb ** 2 + x = (R(2 * na * nb, c), 0, R(na ** 2 - nb ** 2, c)) if c else (0, 0, 0) + require('PURE-PRODUCT', outer(prod) == scale(c, tensor(bloch(x), bloch((0, 0, 1))))) + A, X = diag(1, 2, 3, 4), add(outer(psi), basis[6]) + badj = B if mutation == 'omit-adjoint' else adj(B) + require('ADJOINT', ip(A, conj(B, X)) == ip(mul(mul(badj, A), B), X)) + + cyclic = scale(R(1, 2), add(add(add(E, scale(-I, pauli[1])), scale(-I, pauli[2])), scale(-I, pauli[3]))) + local = tensor(E, cyclic) + require('CYCLIC-SU', mul(cyclic, adj(cyclic)) == E and det(cyclic) == 1) + phi = vec((1, 0, 0, 1)) + fixtures = [outer(phi), diag(1, 2, 3, 4), eye(4)] + for U, A in itertools.product([CNOT, local], fixtures): + transformed = conj(U, A) + require('QUANTUM-CONTROL', psd(transformed) and rank(transformed) == rank(A)) + + kappa = R(3, 2) + expanded = matrix([[R(1, 2), 0, kappa / 2, 0], [0, R(1, 2), 0, kappa / 2], + [kappa / 2, 0, R(1, 2), 0], [0, kappa / 2, 0, R(1, 2)]]) + p = vec((1, 0, -1, 0)) + require('KAPPA-PRODUCT', mul(mul(adj(p), expanded), p)[0][0] == -R(1, 2)) + effect = tensor(bloch((-1, 0, 0)), bloch((0, 0, 1))) + value = R(1, 4) if mutation == 'product-sign' else -R(1, 4) + require('KAPPA-EFFECT', inner(expanded, effect) == value) + for U in [CNOT, local]: + transformed = conj(U, expanded) + off = matrix([row[2:] for row in transformed[:2]]) + require('KAPPA-INSTANCES', extract(transformed, (0, 1)) == scale(R(1, 2), E) + and extract(transformed, (2, 3)) == scale(R(1, 2), E) + and mul(off, adj(off)) == scale(kappa ** 2 / 4, E)) + + normalized = scale(R(1, 2), outer(phi)) + require('SCALE-CONTROL', trace(normalized) == 1 and trace(scale(2, normalized)) != 1) + A, B = diag(1, 1, 0, 0), diag(0, 0, 1, 0) + require('ADD-CONTROL', psd(A) and psd(B) and psd(add(A, B)) + and rank(A) == 2 and rank(B) == 1 and rank(add(A, B)) == 3) + require('ZERO-H1-CONTROL', tensor(bloch((0, 0, 0)), bloch((0, 0, 0))) != scale(0, eye(4))) + entangled = scale(R(1, 2), conj(CNOT, outer(vec((1, 0, 1, 0))))) + pt = partial_transpose(entangled) + require('SEPARABLE-GATE-CONTROL', psd(entangled) and det(extract(pt, (1, 2))) == -R(1, 4)) + return dict(sorted(count.items())) + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--self-test', action='store_true') + args = ap.parse_args() + counts = run() + if args.self_test: + for mutation, code in [('trace-factor', 'TRACE'), ('omit-adjoint', 'ADJOINT'), + ('product-sign', 'KAPPA-EFFECT')]: + try: + run(mutation) + except AssertionError as error: + if str(error) != code: + raise + print('MUTATION', mutation, 'REJECTED', code) + else: + raise AssertionError('mutation escaped: ' + mutation) + print('SELF-TEST PASS; positive fixture and 3 mutations') + else: + for key, value in counts.items(): + print(key + ': PASS (' + str(value) + ')') + print('MAXCONE-EXACT: PASS; ' + str(sum(counts.values())) + ' finite exact checks') + + +if __name__ == '__main__': + main() diff --git a/verification/lean/oi_maxcone_gaussian.py b/verification/lean/oi_maxcone_gaussian.py new file mode 100644 index 000000000..eff710c93 --- /dev/null +++ b/verification/lean/oi_maxcone_gaussian.py @@ -0,0 +1,133 @@ +"""Small exact Q(i) matrix arithmetic for the independently written design controls.""" +from dataclasses import dataclass +from fractions import Fraction +from functools import lru_cache + + +@dataclass(frozen=True) +class G: + re: Fraction = Fraction(0) + im: Fraction = Fraction(0) + + def __post_init__(self): + object.__setattr__(self, 're', Fraction(self.re)) + object.__setattr__(self, 'im', Fraction(self.im)) + + @staticmethod + def of(value): + return value if isinstance(value, G) else G(value) + + def __add__(self, other): + other = G.of(other) + return G(self.re + other.re, self.im + other.im) + __radd__ = __add__ + + def __neg__(self): + return G(-self.re, -self.im) + + def __sub__(self, other): + return self + -G.of(other) + + def __rsub__(self, other): + return G.of(other) + -self + + def __mul__(self, other): + other = G.of(other) + return G(self.re * other.re - self.im * other.im, + self.re * other.im + self.im * other.re) + __rmul__ = __mul__ + + def conj(self): + return G(self.re, -self.im) + + def __truediv__(self, other): + other = G.of(other) + norm = other.re ** 2 + other.im ** 2 + if norm == 0: + raise ZeroDivisionError + return self * G(other.re / norm, -other.im / norm) + + def __eq__(self, other): + other = G.of(other) + return (self.re, self.im) == (other.re, other.im) + + def nonnegative(self): + return self.im == 0 and self.re >= 0 + + +I = G(0, 1) +Z = G() + + +def matrix(rows): + return tuple(tuple(G.of(x) for x in row) for row in rows) + + +def eye(n): + return matrix([[int(j == k) for k in range(n)] for j in range(n)]) + + +def diag(*values): + return matrix([[v if j == k else 0 for k in range(len(values))] + for j, v in enumerate(values)]) + + +def add(A, B): + return tuple(tuple(a + b for a, b in zip(ra, rb)) for ra, rb in zip(A, B)) + + +def scale(c, A): + return tuple(tuple(G.of(c) * a for a in row) for row in A) + + +def mul(A, B): + return tuple(tuple(sum((A[j][k] * B[k][l] for k in range(len(B))), Z) + for l in range(len(B[0]))) for j in range(len(A))) + + +def adj(A): + return tuple(tuple(A[k][j].conj() for k in range(len(A))) for j in range(len(A[0]))) + + +def tensor(A, B): + return tuple(tuple(A[j][k] * B[l][m] for k in range(len(A[0])) for m in range(len(B[0]))) + for j in range(len(A)) for l in range(len(B))) + + +def trace(A): + return sum((A[j][j] for j in range(len(A))), Z) + + +def extract(A, ix): + return tuple(tuple(A[j][k] for k in ix) for j in ix) + + +@lru_cache(maxsize=None) +def det(A): + n = len(A) + if n == 0: + return G(1) + if n == 1: + return A[0][0] + return sum(((-1) ** k * A[0][k] * det(tuple(tuple(row[l] for l in range(n) if l != k) + for row in A[1:])) for k in range(n)), Z) + + +def rank(A): + rows = [list(row) for row in A] + pivot = 0 + for col in range(len(A[0])): + found = next((j for j in range(pivot, len(A)) if rows[j][col] != 0), None) + if found is None: + continue + rows[pivot], rows[found] = rows[found], rows[pivot] + div = rows[pivot][col] + rows[pivot] = [a / div for a in rows[pivot]] + for j in range(len(A)): + if j != pivot: + fac = rows[j][col] + rows[j] = [a - fac * b for a, b in zip(rows[j], rows[pivot])] + pivot += 1 + if pivot == len(A): + break + return pivot diff --git a/verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/controls.py b/verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/controls.py new file mode 100644 index 000000000..fd17f1acc --- /dev/null +++ b/verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/controls.py @@ -0,0 +1,236 @@ +#!/usr/bin/env python3 +"""Frozen content controls for OI-PAIR-MAXCONE-1; host attestations are checked separately.""" +import argparse +import hashlib +import json +from pathlib import Path +import re +import subprocess +import sys + +D = 'f2415108601a9c36bb985b3374c56f0eb34c2962' +ROUND = 'verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/' +PROBE = 'verification/lean/oi_maxcone_check.py' +SUPPORT = 'verification/lean/oi_maxcone_gaussian.py' +WORKFLOW = '.github/workflows/verify.yml' +ROOT = 'verification/lean-mathlib/OIBridge.lean' +REGISTRY = 'verification/lean-manuscript-census.json' +ROADMAP = 'verification/ROADMAP.md' +PIN = {'verification/lean-mathlib/OIBridge/EqvK2Schema.lean': 'c76991ba337ac3ac58a41eaa88c46af62e59a374117b31edecabaec9309f6a3e', 'verification/lean-mathlib/OIBridge/EqvK2Converse.lean': '58f97ca9a371b3d14148328a2816f953e6adc0d1067ea383cc802460aae26d56', 'verification/lean-mathlib/OIBridge/EqvK2Block.lean': '081b99696c104d6e3c4d50d6b9f1b7d5133976f89c9d5410ae5d3067a5b1d0ac', 'verification/lean-mathlib/OIBridge/EqvK2Generation.lean': '42c9e313ee35d7f5ee16cf0bee2abde2ad17867d6eaf65a76e5abb2be469c6d3', 'verification/lean-mathlib/OIBridge/BridgeDictionary.lean': 'f32304db1803ee31141f3a805ac9c15c7ea7c02042e6e2234c77f3863850e065', 'verification/lean-mathlib/OIBridge/BridgeConverge.lean': 'f1c43d1ca223c8a924a1afee55ee97a661e49079ec757c80df53aa5637de7c42', 'verification/lean-mathlib/OIBridge/EqvK2MaxCone.lean': '9222038440f742856480706c27569611bed15b82f650b3eab76c9c61e258169f', 'verification/lean-mathlib/OIBridge.lean': 'a031136f6c7eddc7c9d5cc0162119dfcd9bb5fa2ec8be996628a99cc94a400c8', 'verification/lean/oi_maxcone_check.py': 'd322c9139666c00821fbf85bb2c63dbf5b977ce329dca180bbf652b55c7ca72a', 'verification/lean/oi_maxcone_gaussian.py': '8e4573f6f5a916202cc5770809809bbbbabd682cc2aefd5d3e4567d2b0282df1', 'verification/lean-manuscript-census.json': 'd23abaf21d73f2410d932f47ff6f29e68fe3d12f482714c462c6276d807eb547', '.github/workflows/verify.yml': '62fb29a5348e02828044c4e34d8a1281b00c20d4c7e0a5de9aefc5ab43d1535d'} +PIN_BLOB = {'verification/lean-mathlib/OIBridge/EqvK2Schema.lean': 'c634beb82193eb7372ccaf498dba56dd2ec8538c', 'verification/lean-mathlib/OIBridge/EqvK2Converse.lean': 'f01fc607eab88d8d8ffe24b48d164830e2dad3e6', 'verification/lean-mathlib/OIBridge/EqvK2Block.lean': '23c74144073ef001d69c718f1fa3c0be5b8c1896', 'verification/lean-mathlib/OIBridge/EqvK2Generation.lean': '1251afd7aa8667cf73fb8b19a669e6a3d7bb026e', 'verification/lean-mathlib/OIBridge/BridgeDictionary.lean': 'f997b33ec7ff8402246c7250d38f3e935e4f92df', 'verification/lean-mathlib/OIBridge/BridgeConverge.lean': 'e1647b1dc6585073b5b27be2b5e7e13ac803eb0c', 'verification/lean-mathlib/OIBridge/EqvK2MaxCone.lean': '5b4b98c8e81e21eb002de25383eada381b65e3dd', 'verification/lean-mathlib/OIBridge.lean': '281b6a52412ea3e51cb412997c9984d5806bad82', 'verification/lean/oi_maxcone_check.py': '09d2abcd66f0e230b1a1895e015cb3183297f900', 'verification/lean/oi_maxcone_gaussian.py': 'eff710c93f2211b90472eec8f6d3d5884e3c9421', 'verification/lean-manuscript-census.json': 'dd59b8938c12d87be9d3a007900eca2c3020518a', '.github/workflows/verify.yml': '7c85970db08f8326ff3bca86c62cebab1e3159db'} +BASE_HASH = {'.github/workflows/verify.yml': 'bd71bdc270753be8296c4a5c9723e23673c2f8acdaa9417fb70a6ddd6cbe2443', 'verification/lean-mathlib/OIBridge.lean': 'e5af9614009889dab616d7f02f75bb395f1ae1fb01307f46ef82d3b282b4c313', 'verification/lean-manuscript-census.json': 'cdadb02e0463366c036834f2ca58ae904ad70e05dfe981fd1f37d9bc928e0bbf', 'verification/ROADMAP.md': 'a64835c2107131530f2396311b3e8fa291bc690462ffbbde225f3479d89a2c2c', 'verification/lean-mathlib/OIBridge/OperationalValidity.lean': 'ba316747d23820f75f4bbd25105d87a85febb3bd1d0eaa123913b629b34f05f0', 'verification/lean-mathlib/OIBridge/ImplementationLocality.lean': '4e5b4b22298dfba7b0ee7ba26109ef3090eb48b23227734bb26bbf6834a545ac'} +OUTPUT_SHA = '492bfc19254a39193222a90e828dc16c4ae58bc434bb00c90f03931c6a0adeee' +ROADMAP_SHA = 'a6a4e9e7f5d1e3e363c9abef34e1123002fb1a9494c65bef690450f833b3e160' +FAMILY = {'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/."} +SPLICES = [[' # Act 42. Two shards run on every event;', " probes_oimaxcone:\n name: Numerical probes / OI pair maxCone\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 maxCone and cone controls\n run: python3 -I -B verification/lean/oi_maxcone_check.py\n - name: Native control mutation tests\n run: python3 -I -B verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/controls.py --self-test\n\n # Act 42. Two shards run on every event;"], ['probes_oichannel1, probes_a42_witness', 'probes_oichannel1, probes_oimaxcone, probes_a42_witness'], [' OICHANNEL1_RESULT: ${{ needs.probes_oichannel1.result }}\n', ' OICHANNEL1_RESULT: ${{ needs.probes_oichannel1.result }}\n OIMAXCONE_RESULT: ${{ needs.probes_oimaxcone.result }}\n'], [' echo "oichannel1=${OICHANNEL1_RESULT}"\n', ' echo "oichannel1=${OICHANNEL1_RESULT}"\n echo "oimaxcone=${OIMAXCONE_RESULT}"\n'], [' test "${OICHANNEL1_RESULT}" = success\n', ' test "${OICHANNEL1_RESULT}" = success\n test "${OIMAXCONE_RESULT}" = success\n']] +ROADMAP_SPLICE = ("- **K2 — the composite. OPEN.** Read-only research has mapped a candidate `d = 3` composition\n route, but no governed round records the classification or the cone theorem. Its obligations\n include local tomography, which DIM-1's carrier `W d` encodes as a premise, the composite cone,\n local actions compatible with it, the formal composition theorem, the antiunitary and\n complete-positivity bridge, and the relation to the K3 machinery; all are open. K2 does not\n discharge H-Bell.", "- **K2 — the composite. OPEN.** OI-PAIR-MAXCONE-1 records the conditional two-token cone theorem:\n a set containing the products of `eball 3`, closed under addition and nonnegative scaling,\n contained in `maxCone`, and invariant under CNOT and the full rotation/cyclic actions is `Q3`\n (`pairCone_eq_Q3_of_drive_maxCone`). Product-test validity on an available family containing\n the sharp tests suffices for the upper bound (`pairCone_eq_Q3_of_sharp_available`). The\n hypotheses remain explicit; the theorem does not derive them for the observer's pair cone.\n Local tomography, the physical state/test identification and cone realization, the sources of\n compatible local actions, composition beyond two tokens, the antiunitary and complete-positivity\n bridge, and the relation to the K3 machinery remain open. K2 does not discharge H-Bell.") + +RESULT_TEMPLATE = '''# OI-PAIR-MAXCONE-1 — conditional pair-cone theorem + +Outcome: OI-PAIR-MAXCONE-1-PROVED + +For a set of two-token tables containing every product state of eball 3 and closed under addition and nonnegative scaling, the maxCone upper bound together with CNOT and full rotation/cyclic invariance implies K=Q3. The upper inclusion uses maxCone and block invariance; the lower uses products and cone closure. Available sharp product tests suffice for the upper bound. These conditional statements use neither self-duality nor closedness nor an assumed ReachPure witness. + +The block and generator equivalences have separate witnesses: blockInvariant_of_eq_Q3 / pairCone_eq_Q3_of_block_maxCone, and driveInvariant_of_eq_Q3 / pairCone_eq_Q3_of_drive_maxCone. The physical state/test identification, product preparation and cone realization, validity of product tests on the actual pair, enough available tests, and preservation by the gate and full rotation/cyclic actions retain their source obligations. A one-angle or channel-limit route retains its own closure assumptions. + +The finite controls do not show that OI implies QM. Nothing here sources H3; neither physical sourcing nor full-model independence is labelled kernel-certified. The 118 reached rows and 68 NOT REACHED rows remain distinct; the latter are unresolved. Arbitrary finite-carrier reconstruction and the full operation/instrument correspondence remain open. + +Exact controls: MAXCONE-EXACT: PASS; 2743 finite exact checks +The checker uses Q(i), replay is byte-identical, and its three mutations are rejected. Finite witnesses are not universal proofs. Density states fail scaling; the rank-three-excluded PSD family fails addition; the expanded kappa family fails a product test; the zero cone fails product inclusion; the separable family fails CNOT invariance. Whole-family statements have written proofs in the preregistration at their stated scope. + +Design evidence: core 4d7d71d6, run 38205087980, 13 standard axiom reports; sharp-test refinement bbcdbab5, run 38205760341, 16 standard axiom reports. Both Build steps succeeded and their release gates failed only the seven unregistered design modules' census. Predictive execution evidence is recorded in the preregistration. The execution includes the matching proof bodies, truthful conditional headers, the kernel-only registry family, the exact checker and control shard. Six E19 dependency bodies are unchanged; the new MaxCone proof body is unchanged from the measured refinement. + +F: {F} +F workflow run: {F_RUN} +S1: {S1} +S1 workflow run: {S1_RUN} + +The execution's sixteen named MaxCone axiom reports must be standard, with no sorryAx, and all required host checks must be green before E designation. The owner's E designation and its exact-head workflow attestation are recorded outside this result note and in the receipt. The proof is conditional mathematics; this package supplies no unconditional reconstruction or full-model independence result. +''' + + +def sha(body): + return hashlib.sha256(body).hexdigest() + + +def git(*args): + return subprocess.check_output(['git', *args]) + + +def workflow(base): + text = base.decode() + for old, new in SPLICES: + if text.count(old) != 1: + raise ValueError('W: splice anchor is not unique') + text = text.replace(old, new) + return text.encode() + + +def roadmap(base): + old, new = ROADMAP_SPLICE + text = base.decode() + if text.count(old) != 1: + raise ValueError('M: roadmap anchor is not unique') + return text.replace(old, new).encode() + + +def render_result(f, frun, s1, srun): + return RESULT_TEMPLATE.format(F=f, F_RUN=frun, S1=s1, S1_RUN=srun).encode() + + +def result_fields(body): + pattern = re.escape(RESULT_TEMPLATE) + for key, expression in [('F', '[0-9a-f]{40}'), ('S1', '[0-9a-f]{40}'), + ('F_RUN', '[1-9][0-9]*'), ('S1_RUN', '[1-9][0-9]*')]: + pattern = pattern.replace(re.escape('{' + key + '}'), '(?P<' + key + '>' + expression + ')') + match = re.fullmatch(pattern, body.decode()) + return match.groupdict() if match else None + + +def failures(files, original, freeze, output, stderr, rc, required, f=None, s1=None): + errors = [] + for path, digest in BASE_HASH.items(): + if sha(original.get(path, b'')) != digest: + errors.append('D') + for path, digest in PIN.items(): + if sha(files.get(path, b'')) != digest: + errors.append('P') + if files.get(WORKFLOW) != workflow(original[WORKFLOW]): + errors.append('W') + anchor = b'import OIBridge.RelcSelectC5\n' + expected_root = original[ROOT].replace(anchor, anchor + b'import OIBridge.EqvK2MaxCone\n') + if original[ROOT].count(anchor) != 1 or files.get(ROOT) != expected_root: + errors.append('H') + try: + expected = json.loads(original[REGISTRY]) + expected['families'].append(FAMILY) + if json.loads(files.get(REGISTRY, b'')) != expected: + errors.append('J') + except (ValueError, KeyError): + errors.append('J') + for path in original: + if path not in (WORKFLOW, ROOT, REGISTRY, ROADMAP) and files.get(path) != original[path]: + errors.append('L') + roadmap_digest = ROADMAP_SHA if required else BASE_HASH[ROADMAP] + expected_roadmap = roadmap(original[ROADMAP]) if required else original[ROADMAP] + if sha(files.get(ROADMAP, b'')) != roadmap_digest or files.get(ROADMAP) != expected_roadmap: + errors.append('M') + if files.get(ROUND + 'preregistration.md') != freeze: + errors.append('F') + 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'')) != control_hash.group(1).decode(): + errors.append('C') + names = {'preregistration.md', 'controls.py'} | ({'result.md'} if required else set()) + if {p[len(ROUND):] for p in files if p.startswith(ROUND)} != names: + errors.append('R') + if rc or stderr or sha(output) != OUTPUT_SHA: + errors.append('V') + if required: + fields = result_fields(files.get(ROUND + 'result.md', b'')) + if fields is None or (f and fields['F'] != f) or (s1 and fields['S1'] != s1): + errors.append('S') + return sorted(set(errors)) + + +def self_test(root, base_root): + root = Path(root) + original = {p: (Path(base_root) / p).read_bytes() if base_root else git('show', D + ':' + p) + for p in BASE_HASH} + # CI replays the frozen fixture, rather than permanently pinning the live + # shared workflow, registry, aggregator or kernel at every later head. + # The local pre-freeze fixture uses the staged files before these blobs + # have been published. The two owned checker files remain live regression + # inputs, and the independent checker is actually executed below. + files = {p: (root / p).read_bytes() if base_root else git('cat-file', 'blob', PIN_BLOB[p]) + for p in PIN} + for p in (PROBE, SUPPORT): + files[p] = (root / p).read_bytes() + files.update({p: original[p] for p in original if p not in files and p != ROADMAP}) + files[ROADMAP] = roadmap(original[ROADMAP]) + controls = Path(__file__).read_bytes() + pre = root / ROUND / 'preregistration.md' + freeze = pre.read_bytes() if pre.exists() else ('Controls SHA256: ' + sha(controls) + '\n').encode() + files[ROUND + 'preregistration.md'] = freeze + files[ROUND + 'controls.py'] = controls + f, s1 = 'a' * 40, 'b' * 40 + files[ROUND + 'result.md'] = render_result(f, 1, s1, 2) + proc = subprocess.run([sys.executable, '-I', '-B', str(root / PROBE)], capture_output=True) + def test(current, out=proc.stdout, err=proc.stderr, rc=proc.returncode): + return failures(current, original, freeze, out, err, rc, True, f, s1) + if test(files): + raise ValueError('positive fixture fails ' + str(test(files))) + stage1 = dict(files) + stage1.pop(ROUND + 'result.md') + stage1[ROADMAP] = original[ROADMAP] + if failures(stage1, original, freeze, proc.stdout, proc.stderr, proc.returncode, False): + raise ValueError('stage-one positive fixture fails') + mutations = [(p, b'changed', 'P') for p in PIN] + mutations += [(WORKFLOW, original[WORKFLOW], 'W'), (ROOT, original[ROOT], 'H'), + (REGISTRY, original[REGISTRY], 'J'), (ROADMAP, original[ROADMAP], 'M'), + (ROUND + 'preregistration.md', b'changed', 'F'), + (ROUND + 'controls.py', b'changed', 'C'), (ROUND + 'extra', b'extra', 'R'), + (ROUND + 'result.md', files[ROUND + 'result.md'] + b'It establishes unconditional reconstruction.', 'S'), + (ROUND + 'result.md', render_result('c' * 40, 1, s1, 2), 'S')] + anchor = next(p for p in original if p not in (WORKFLOW, ROOT, REGISTRY, ROADMAP)) + mutations.append((anchor, b'changed', 'L')) + for p, value, code in mutations: + changed = dict(files) + changed[p] = value + if code not in test(changed): + raise ValueError('mutation escaped ' + code + ' at ' + p) + for out, err, rc in [(b'PASS', b'', 0), (proc.stdout, b'error', 0), (proc.stdout, b'', 1)]: + if 'V' not in test(files, out, err, rc): + raise ValueError('output mutation escaped') + print('controls self-test: PASS; two positive fixtures and ' + str(len(mutations) + 3) + ' mutations') + + +def check(head, freeze): + original = {p: git('show', D + ':' + p) for p in BASE_HASH} + names = git('ls-tree', '-r', '--name-only', head, '--', ROUND).decode().splitlines() + paths = set(PIN) | set(BASE_HASH) | set(names) + files = {p: git('show', head + ':' + p) for p in paths} + fixed = git('show', freeze + ':' + ROUND + 'preregistration.md') + changed = set(git('diff', '--name-only', D, head).decode().splitlines()) + allowed = set(PIN) | {ROADMAP, ROUND + 'preregistration.md', ROUND + 'controls.py', ROUND + 'result.md'} + if not changed <= allowed: + raise ValueError('G: changed path outside declared scope') + if git('diff', '--name-only', D, freeze).decode().splitlines() != [ROUND + 'preregistration.md']: + raise ValueError('G: freeze delta is not the preregistration alone') + subprocess.run(['git', 'merge-base', '--is-ancestor', freeze, head], check=True) + ancestry = git('rev-list', '--reverse', '--parents', freeze + '..' + head).decode().splitlines() + if not ancestry or any(len(line.split()) != 2 for line in ancestry): + raise ValueError('T: execution is not linear after F') + s1 = ancestry[0].split()[0] + for path in (PROBE, SUPPORT): + if Path(path).read_bytes() != files[path]: + raise ValueError('P: local checker/support differs from checked object') + if Path(__file__).read_bytes() != files[ROUND + 'controls.py']: + raise ValueError('C: running controls differ from checked object') + proc = subprocess.run([sys.executable, '-I', '-B', PROBE], capture_output=True) + required = ROUND + 'result.md' in files + failed = failures(files, original, fixed, proc.stdout, proc.stderr, proc.returncode, + required, freeze, s1) + if failed: + raise ValueError('controls failed: ' + ','.join(failed)) + print('controls: PASS') + sys.stdout.write(proc.stdout.decode()) + + +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('--root', default='.') + parser.add_argument('--base-root') + args = parser.parse_args() + try: + if args.self_test: + self_test(args.root, args.base_root) + 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-pair-maxcone-1/preregistration.md b/verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/preregistration.md new file mode 100644 index 000000000..3917cde76 --- /dev/null +++ b/verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/preregistration.md @@ -0,0 +1,280 @@ +# OI-PAIR-MAXCONE-1 — conditional pair-cone proof package + +Status: candidate freeze, native V3 draft. Owner direction to prepare this work: ChatGPT, +2026-10-12T04:24:46Z, “Ok let's proceed as suggested”. Parallel design work was authorized +at 2026-10-12T05:10:00Z, “Can we work on both PR's in parallel?” This control plane is +prepared on one PR from D. An instruction to proceed is not an exact-object F or E designation. +The owner designates F only after an all-green workflow_dispatch run held on that exact head. + +```v3-round +round OI-PAIR-MAXCONE-1 +kind non-sealing +record-directory verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/ +``` + +```v3-governed-paths +record AM verification/programmes/oi-qm/reconstruction/round-oi-pair-maxcone-1/ +record AM verification/receipts/OI-PAIR-MAXCONE-1.json +execution A verification/lean-mathlib/OIBridge/EqvK2Schema.lean +execution A verification/lean-mathlib/OIBridge/EqvK2Converse.lean +execution A verification/lean-mathlib/OIBridge/EqvK2Block.lean +execution A verification/lean-mathlib/OIBridge/EqvK2Generation.lean +execution A verification/lean-mathlib/OIBridge/BridgeDictionary.lean +execution A verification/lean-mathlib/OIBridge/BridgeConverge.lean +execution A verification/lean-mathlib/OIBridge/EqvK2MaxCone.lean +execution M verification/lean-mathlib/OIBridge.lean +execution A verification/lean/oi_maxcone_check.py +execution A verification/lean/oi_maxcone_gaussian.py +execution M verification/lean-manuscript-census.json +execution M .github/workflows/verify.yml +execution M verification/ROADMAP.md +``` + +D: f2415108601a9c36bb985b3374c56f0eb34c2962. +D tree: 31b2cd14bdc9e20ec12d153b56718db6294d607c. +D to F changes this preregistration alone. S1 and S2 are linear children after F; +unrelated history enters only in the prescribed reconciliation after E. This non-sealing +round promotes conditional mathematics; it changes no manuscript or other round's record. + +## Productivity test and questions + +The original design protocol was fixed before its first build. This is stronger mathematics +only if the forcing theorem removes self-duality H3, closedness and assumed ReachPure, +while exposing addition and nonnegative scaling explicitly, and the named kernel reports +contain only standard axioms, with no sorryAx. The actual OI sources remain separately +open. A failed frozen control halts execution under S12; neither a threshold nor an earned +reading is revised after F. + +| Question | Named witnesses / checkpoint | Earned scope | +|---|---|---| +| Upper inclusion without H3 or cone closure | subset_Q3_of_maxCone_block | K⊆maxCone and block invariance give K⊆Q3 | +| Lower inclusion without H3 | Q3_subset_of_products_cone_block | Products, addition, nonnegative scaling and block invariance give Q3⊆K | +| Generator form | blockInvariant_of_drive; pairCone_eq_Q3_of_drive_maxCone | CNOT plus every-angle rotation and cyclic invariance derive the required block action | +| Block equivalence | blockInvariant_of_eq_Q3 / pairCone_eq_Q3_of_block_maxCone | Separate directions under stated cone and positivity premises | +| Generator equivalence | driveInvariant_of_eq_Q3 / pairCone_eq_Q3_of_drive_maxCone | Separate directions, retaining the full-flow/cyclic datum | +| Available sharp tests suffice | maxCone_bound_of_sharp_available; subset_Q3_of_sharp_products_block; pairCone_eq_Q3_of_sharp_available | Validity on an available family containing sharpFamily 3 gives the upper bound, without EffectsOn in this direction | +| Actual pair sourcing | Complete I3/I4 review and conditional result template | No source of an actual observer's cone, state/test identification or pair-preserving action is upgraded | + +The sufficient subgroup is SU(2)×SU(2). No claim that the resources generate every pair +of arbitrary U(2) blocks is made. A prior one-angle/channel-limit route retains its own +closure assumptions. Six E19 dependencies retain their proof bodies; EqvOneDictionary +is not part of this package and no unneeded design module is imported. + +## Frozen S1 files and independent reconstruction + +| Destination | SHA256 | Git blob | +|---|---|---| +| verification/lean-mathlib/OIBridge/EqvK2Schema.lean | c76991ba337ac3ac58a41eaa88c46af62e59a374117b31edecabaec9309f6a3e | c634beb82193eb7372ccaf498dba56dd2ec8538c | +| verification/lean-mathlib/OIBridge/EqvK2Converse.lean | 58f97ca9a371b3d14148328a2816f953e6adc0d1067ea383cc802460aae26d56 | f01fc607eab88d8d8ffe24b48d164830e2dad3e6 | +| verification/lean-mathlib/OIBridge/EqvK2Block.lean | 081b99696c104d6e3c4d50d6b9f1b7d5133976f89c9d5410ae5d3067a5b1d0ac | 23c74144073ef001d69c718f1fa3c0be5b8c1896 | +| verification/lean-mathlib/OIBridge/EqvK2Generation.lean | 42c9e313ee35d7f5ee16cf0bee2abde2ad17867d6eaf65a76e5abb2be469c6d3 | 1251afd7aa8667cf73fb8b19a669e6a3d7bb026e | +| verification/lean-mathlib/OIBridge/BridgeDictionary.lean | f32304db1803ee31141f3a805ac9c15c7ea7c02042e6e2234c77f3863850e065 | f997b33ec7ff8402246c7250d38f3e935e4f92df | +| verification/lean-mathlib/OIBridge/BridgeConverge.lean | f1c43d1ca223c8a924a1afee55ee97a661e49079ec757c80df53aa5637de7c42 | e1647b1dc6585073b5b27be2b5e7e13ac803eb0c | +| verification/lean-mathlib/OIBridge/EqvK2MaxCone.lean | 9222038440f742856480706c27569611bed15b82f650b3eab76c9c61e258169f | 5b4b98c8e81e21eb002de25383eada381b65e3dd | +| verification/lean-mathlib/OIBridge.lean | a031136f6c7eddc7c9d5cc0162119dfcd9bb5fa2ec8be996628a99cc94a400c8 | 281b6a52412ea3e51cb412997c9984d5806bad82 | +| verification/lean/oi_maxcone_check.py | d322c9139666c00821fbf85bb2c63dbf5b977ce329dca180bbf652b55c7ca72a | 09d2abcd66f0e230b1a1895e015cb3183297f900 | +| verification/lean/oi_maxcone_gaussian.py | 8e4573f6f5a916202cc5770809809bbbbabd682cc2aefd5d3e4567d2b0282df1 | eff710c93f2211b90472eec8f6d3d5884e3c9421 | +| verification/lean-manuscript-census.json | d23abaf21d73f2410d932f47ff6f29e68fe3d12f482714c462c6276d807eb547 | dd59b8938c12d87be9d3a007900eca2c3020518a | +| .github/workflows/verify.yml | 62fb29a5348e02828044c4e34d8a1281b00c20d4c7e0a5de9aefc5ab43d1535d | 7c85970db08f8326ff3bca86c62cebab1e3159db | + +Controls SHA256: c5a13a2f7ae09f705e653a101d48210ac6be018a46dece35bc0ff66c2b85bedd + +The seven new module headers describe conditional infrastructure truthfully. The six E19 +proof bodies are from dev-equivalence/r5-design f0c36cf9fa8395ac4349d944dc21dda80e4c2658 +(design run 38134245361); the MaxCone proof body is from bbcdbab531af5c6ce14d43625e6dc1df16e2063f. +Each body here means every byte after the first header-closing -/, including imports and +axiom-report commands. Only the new headers differ from those measured design sources. + +| Module | Preserved body SHA256 | +|---|---| +| EqvK2Schema | 89d4b787eed4a118b19ca5f10778f35b8e35bca64ac10545cf72fef0de6d401d | +| EqvK2Converse | a3781383974dbf7b48d474395d99f7ad110400c41496157febc959adee61777a | +| EqvK2Block | 7117ea8ac51b5a14ff4d9420298469890b74bbd94da82f5901da7767f76bbe08 | +| EqvK2Generation | 2a1b833d13e9acd679748ceba8a0b1e0c1daf3c917b6ea695f911fc942bf9da4 | +| BridgeDictionary | e06a491f0ce1a0c866214b89ebaca1d8cd9a3145727b68a20e6aeb1dc46bd68a | +| BridgeConverge | 7ac67b54b4271e545fd3fa7b9fb6d203d708dcdaa7f25aed8d4b99bcc4321f71 | +| EqvK2MaxCone | 4f12fb1693b6b13843f58f9c562a4c1143e2b2027e730b6350877b0e2d78866a | + +The aggregate import has one insertion after import OIBridge.RelcSelectC5: +import OIBridge.EqvK2MaxCone. The registry keeps every original family and supersession +and appends one kernel-only family covering exactly the seven new modules, with manuscript=[] +and explicit conditional scope. No current manuscript family or publication-facing theorem +is strengthened. Kernel-only is the actual disposition, not a claim that a paper carries it. + +The workflow changes only five declared splices: the new OI pair maxCone shard, one needs +entry, one result environment variable, one echo and one required-success test. The shard +uses Python 3.11, checkout with fetch-depth 0, the standard-library exact checker and +controls --self-test. Existing jobs and source modules retain their bytes. The controls +reconstruct all five splices, the import and the semantic registry append from D. + +| D anchor | SHA256 | +|---|---| +| .github/workflows/verify.yml | bd71bdc270753be8296c4a5c9723e23673c2f8acdaa9417fb70a6ddd6cbe2443 | +| verification/lean-mathlib/OIBridge.lean | e5af9614009889dab616d7f02f75bb395f1ae1fb01307f46ef82d3b282b4c313 | +| verification/lean-manuscript-census.json | cdadb02e0463366c036834f2ca58ae904ad70e05dfe981fd1f37d9bc928e0bbf | +| verification/ROADMAP.md | a64835c2107131530f2396311b3e8fa291bc690462ffbbde225f3479d89a2c2c | +| verification/lean-mathlib/OIBridge/OperationalValidity.lean | ba316747d23820f75f4bbd25105d87a85febb3bd1d0eaa123913b629b34f05f0 | +| verification/lean-mathlib/OIBridge/ImplementationLocality.lean | 4e5b4b22298dfba7b0ee7ba26109ef3090eb48b23227734bb26bbf6834a545ac | + +The frozen execution controls compare all twelve output files to their SHA256s and these +anchors to D; bound every changed path; require the preregistration to remain exactly F; +require exact record population; enforce linear ancestry from F; and run the actual checker. +At later heads, CI self-test reconstructs a virtual fixture from the immutable Git blobs +above instead of pinning the live shared workflow, registry, aggregator or kernel. The +owned checker/support and actual checker output remain live regression inputs. A separate +local replay changed every shared fixture file and still passed; actual execution controls +continue to reject every changed frozen output. This is essential for later native rounds +and the parallel transfer successor. + +## Exact controls and their limits + +The independent checker reads no research or Lean source, computes in Q(i) with the +standard library, and prints 2743 finite exact checks. Its SHA256 stdout is +492bfc19254a39193222a90e828dc16c4ae58bc434bb00c90f03931c6a0adeee, stderr empty, exit zero. Final line: +MAXCONE-EXACT: PASS; 2743 finite exact checks + +Its checks include all 16 matrix units and 256 trace pairings; 81 products and 1296 +product identities; 169 pure-state block reductions including zero blocks and complex +phases, 338 SU checks and 169 adjoint checks; exact PSD/minor/rank witnesses. Mutations +of the trace factor, omitted adjoint and product-test sign must be rejected. The checker +has an independent Gaussian-rational helper; changing the support file also trips P. +Finite computations are controls, not universal proofs or a full OI model. + +The frozen content controls pass two positive fixtures (S1 and S2) and reject 25 mutations: +each of twelve S1 files, workflow reconstruction, import, registry, roadmap, preregistration, +controls, extra record, result overclaim, wrong F, source anchor, stdout, stderr and exit code. +The result check uses the full exact earned template below with four bounded attestation +fields; negated sentences containing kernel-certified, sources H3 or OI implies QM pass. +Appending an affirmative overclaim fails. No context-blind forbidden-word list is used. + +## Source audit and family controls + +# MaxCone theorem: premise provenance and scope + +Certified snapshot: main f2415108601a9c36bb985b3374c56f0eb34c2962. It adds OI-CHANNEL-1 records to the inventory's base 9f9f8257 and changes no kernel definition used below. Reference inventory: research/archive 4dc0321ca2aac6f6aca6f55efc90b7f51330334a, I3 and I4. + +## Premises in the new theorem + +| Premise | Inventory / current source | Standing for an observer's actual pair cone | +|---|---|---| +| Carrier W 3 and two elementary eball 3 factors | I3.1-I3.3; K1/K2 roadmap; CompositeDimension | Conditional coordinate realization. Local tomography, the elementary ball and its dimension have their own source obligations. | +| Products in K (H1) | I3.43 CandidateCone; I3.147 | Assumed for K. The theorem placing products in maxCone does not place them in arbitrary K. | +| Addition and nonnegative scaling | I3.130 IsConvexCone / PairAdm, design hypothesis | Explicit. These properties were consequences of H3 in the previous proof. Convexity of a normalized body alone is not closure under nonnegative scaling. | +| K subset maxCone | I3.3 definition; I3.43 CandidateCone | Assumed for K. The definition of maxCone is not a source of pair validity. | +| CNOT preserves K (H2) | I3.148; kernel cnot and NativeGate positivity on product inputs | Pair invariance remains additional. Availability of the permutation gate and its product-input positivity do not prove invariance on K. | +| Full rotation flow and cyclic datum preserve K (A_miss) | I3.66, I3.165; E23 source table; E19 exact generator form | Pair invariance remains additional. The full-flow statement includes the cyclic datum and does not follow merely from having a drive on one token. | +| Block invariance | E19 blockInvariant_of_drive, measured design source f0c36cf9 | Derived mathematically from H2 and the stated A_miss. The needed group is SU(2) x SU(2); arbitrary U(2) block pairs are not asserted to be generated. | +| Pure-state reachability | E19 reach_block | Derived in the existing design proof; no ReachPure premise appears in the replacement. | + +Self-duality and closedness are absent from the new forcing theorem. In a route that first upgrades a one-angle or channel sequence to the full flow, its own closure assumptions still need to be sourced: absence from this theorem does not remove them from that earlier route. + +## The test-side reduction + +EFF-1's kernel theorem EffectSpace.maxConeOf_sharp_subset_maxCone proves that sharp product tests suffice for the full maxCone upper bound. The contravariance theorem maxConeOf_anti then gives: + +- K subset maxConeOf avail, together with sharpFamily 3 subset avail, implies K subset maxCone. +- This direction does not need EffectsOn avail: that predicate enters EFF-1's reverse inclusion when equality of test cones is asserted. +- It does not assume availability of every affine effect. OG-1/EFF-1 derive sharpFamily subset avail under body preservation, a sharp seed, boundary transitivity and seed-orbit availability (I3.51). Those premises retain their inventory statuses. +- DenseOrbit supplies an alternative involving a dense seed orbit. Availability of limits is a separate issue; positivity of a continuous evaluation extends along a dense family mathematically. No derivation of such an orbit for the observer is supplied here. + +Two concrete source obligations remain: validity of the product tests on the actual pair body, and enough available tests to determine the upper bound. They must be traced separately. A possible common principle connecting test validity to operation transfer is a research question, not a proved identification. + +## Existing composite and operational validity interfaces + +COMP-1's PreComposite.prodEff_effect makes product effects valid on its composite body as a field of an assumed structure. Its Composite.lt is a local-tomography field. These give a precise place to state the requisite test soundness, but neither constructs the observer's composite from the hidden-history inventory. + +I4.38 validity_of_implementationLocality derives I4.66 CompositeOperationalValidity on the complex matrix carriers of FiniteOperationalTheory. I4.66 assumes PSD input matrices. To apply this result to dict '' K as the whole physical state space needs an independently justified identification and validity on that space. Identifying it with the PSD cone would already assert K=Q3. It also does not by itself supply the operational context and label premises used to transport a local protocol to a pair. + +Repository-wide default-branch searches for maxCone, product effects and implementation locality located EffectSpace, K1Bridge, DenseOrbit, CompositeInterface, K2Guard, the current roadmap, OperationalValidity/ImplementationLocality, and the GR source discussion. The inventory's level and status distinctions are preserved; no unseen source is claimed absent merely because a search returned no hit. + +## Exact countercontrols and written family scope + +The saved checker measures finite instances and witnesses. The following family statements are separate written arguments: + +1. Normalized density matrices contain all normalized product states, obey maxCone, are convex and are invariant under unitary conjugation. They fail nonnegative scaling: a trace-one state doubled has trace two. Hence normalized convexity cannot substitute for the cone assumptions. +2. The PSD matrices with rank in {0,1,2,4} contain all products of two PSD 2x2 states (product ranks are 1,2 or 4), are closed under nonnegative scaling and all unitary conjugations, and obey maxCone. They fail addition: diag(1,1,0,0) plus diag(0,0,1,0) has rank three and is excluded. These properties do not assert topological closedness or convexity. +3. The expanded kappa family of OI-CHANNEL-1 is closed and convex, contains products and is preserved by CNOT and every target channel, as proved in that record's written argument. Its X+ at kappa=3/2 fails a product test: the unnormalized vector (1,0,-1,0) gives -1/2, and the normalized sharp product effect gives -1/4. It is excluded by the replacement bound and is not a full OI model. +4. The zero cone fails H1. The separable cone satisfies product positivity and all local unitary invariances but its |+0> product is mapped by CNOT to a Bell state with a negative partial-transpose minor (-1/4), so it fails H2. + +These are controls for the named pair-level premises. They do not establish independence from the full OI inventory. The 68 NOT REACHED rows remain unresolved; B24 needs a model satisfying every applicable row or a precisely scoped OPEN. + +## Next decisive fork + +The theorem replaces the self-duality obligation in this route with explicit cone structure and test validity. The source audit does not convert these into adopted OI axioms. The next research target is the realization of the pair's test positivity and operation preservation under a single, independently sourced state/test identification. If that cannot be derived, B24's full-model construction must check the entire applicable inventory. Subsequent work retains the K-infinity/K1 origin, arbitrary finite-carrier K_n, and operation/instrument K3 obligations. + + +## S2 roadmap and exact result note + +The sole roadmap splice replaces the K2 paragraph, retaining K2 OPEN, and states the new +conditional theorem and all remaining sources. Every byte outside that uniquely identified +paragraph is D. Its complete predicted SHA256 is a6a4e9e7f5d1e3e363c9abef34e1123002fb1a9494c65bef690450f833b3e160. +The controls reconstruct that one replacement from D; the precise old/new paragraphs are +literal ROADMAP_SPLICE values in the frozen controls. No K∞, K1, K_n, K3 or H-Bell status changes. + +The result has exactly this template. Only F and S1 may be replaced by lowercase 40-hex +commit IDs and F_RUN/S1_RUN by positive workflow IDs; the former must equal the actual +freeze and first execution commit. Host metadata separately establishes event, head SHA, +conclusion and job results. Template matching cannot establish host attestations. + +```text +# OI-PAIR-MAXCONE-1 — conditional pair-cone theorem + +Outcome: OI-PAIR-MAXCONE-1-PROVED + +For a set of two-token tables containing every product state of eball 3 and closed under addition and nonnegative scaling, the maxCone upper bound together with CNOT and full rotation/cyclic invariance implies K=Q3. The upper inclusion uses maxCone and block invariance; the lower uses products and cone closure. Available sharp product tests suffice for the upper bound. These conditional statements use neither self-duality nor closedness nor an assumed ReachPure witness. + +The block and generator equivalences have separate witnesses: blockInvariant_of_eq_Q3 / pairCone_eq_Q3_of_block_maxCone, and driveInvariant_of_eq_Q3 / pairCone_eq_Q3_of_drive_maxCone. The physical state/test identification, product preparation and cone realization, validity of product tests on the actual pair, enough available tests, and preservation by the gate and full rotation/cyclic actions retain their source obligations. A one-angle or channel-limit route retains its own closure assumptions. + +The finite controls do not show that OI implies QM. Nothing here sources H3; neither physical sourcing nor full-model independence is labelled kernel-certified. The 118 reached rows and 68 NOT REACHED rows remain distinct; the latter are unresolved. Arbitrary finite-carrier reconstruction and the full operation/instrument correspondence remain open. + +Exact controls: MAXCONE-EXACT: PASS; 2743 finite exact checks +The checker uses Q(i), replay is byte-identical, and its three mutations are rejected. Finite witnesses are not universal proofs. Density states fail scaling; the rank-three-excluded PSD family fails addition; the expanded kappa family fails a product test; the zero cone fails product inclusion; the separable family fails CNOT invariance. Whole-family statements have written proofs in the preregistration at their stated scope. + +Design evidence: core 4d7d71d6, run 38205087980, 13 standard axiom reports; sharp-test refinement bbcdbab5, run 38205760341, 16 standard axiom reports. Both Build steps succeeded and their release gates failed only the seven unregistered design modules' census. Predictive execution evidence is recorded in the preregistration. The execution includes the matching proof bodies, truthful conditional headers, the kernel-only registry family, the exact checker and control shard. Six E19 dependency bodies are unchanged; the new MaxCone proof body is unchanged from the measured refinement. + +F: {F} +F workflow run: {F_RUN} +S1: {S1} +S1 workflow run: {S1_RUN} + +The execution's sixteen named MaxCone axiom reports must be standard, with no sorryAx, and all required host checks must be green before E designation. The owner's E designation and its exact-head workflow attestation are recorded outside this result note and in the receipt. The proof is conditional mathematics; this package supplies no unconditional reconstruction or full-model independence result. +``` + +## Design evidence and bounded execution + +Original design registration and controls were recorded at research/equivalence +a163b9246a98ef100cbf256e51b00e39a1fc564a before the first design run. +Core head 4d7d71d6b1c771e2f6c578b4cdead45d3a63ff96, run 38205087980: +Build succeeded, thirteen standard named reports; the release gate failed only on seven +unregistered design modules at lean-manuscript. Refinement registration at research/equivalence +9430c4635c34ef8f252176925201737a6966235d preceded the next design run. +Refinement bbcdbab531af5c6ce14d43625e6dc1df16e2063f, run 38205760341: +Build succeeded, sixteen standard named reports, 5967 named global axiom reports and no +sorryAx; release gate failed only the same seven-module census. The other eighteen jobs +passed, with the dispatch-only Act42 matrix job intentionally skipped. All44 existing +native receipts held in both runs. These are design evidence, not F/E attestations. + +Predictive S1 execution evidence: pending before F. The third and final prospectively +registered design build uses the twelve exact S1 files, frozen controls and draft control +plane, with D's roadmap and no result note. Unlike the first two design runs, the maintained +kernel-only disposition and added control shard are included; the expected census outcome +is success. Exact head, run and job conclusions are filled in before requesting F. +This disclosed design evidence is exploratory rather than a blind prediction. + +1. Before F: complete the predictive check, hold the control-plane PR at its proposed exact + F and dispatch verify.yml on that head. Every job must be green before owner F designation. +2. S1 after F: add the twelve frozen files plus controls.py in one single-parent commit, + retaining D's roadmap. Run controls HEAD --freeze F, mutation tests and CI; the Build must + emit all sixteen named standard reports with no sorryAx and the release gate must pass. +3. S2: add the exact result note and only the roadmap splice. Run the frozen controls; + hold E for an all-green exact-head workflow_dispatch run and owner E designation. +4. Reconcile under S9 even if the current base has not advanced; resolve any differing + shared rows by merits. Build a receipt-only single-parent Q, require v3_verifier + --verify-round Q to print VERDICT HOLDS and obtain exact-object landing authorization + before ordinary review and merge. No native validity is inferred from a green PR badge. + +Any failed frozen check halts the round under S12; it does not license editing the control +plane. A halt also requires the governed record, reconciliation, valid receipt and normal +landing review. The theorem and source audit leave bare OI reconstruction and full-model +independence open. The transfer successor has its own design and adoption scope and is +not assumed to be part of this round.