Commutation along the honest hiding chain

The base step uses the concrete dual-X/tail factorization of the stopping measurement. Earlier adaptive stages lift the step using orthogonality of the shared local Z/dual-X measurement. Different branch labels therefore vanish before any commutation claim about different continuations is needed.

theorem MIPRE.Introspection.Honest.pvm_commute {I : Type u_1} {A : Type u_3} [Fintype I] [DecidableEq I] [Fintype A] [DecidableEq A] {P : A → Matrix I I ℂ} (hP : IsPVM P) (a b : A) : Commute (P a) (P b)

theorem MIPRE.Introspection.Honest.coarseOp_commute {I : Type u_1} {A : Type u_3} {B : Type u_4} {U : Type u_6} {V : Type u_7} [Fintype I] [DecidableEq I] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype U] [DecidableEq U] [Fintype V] [DecidableEq V] (f : A → U) (g : B → V) (P : A → Matrix I I ℂ) (Q : B → Matrix I I ℂ) (hc : ∀ (a : A) (b : B), Commute (P a) (Q b)) (u : U) (v : V) : Commute (coarseOp f P u) (coarseOp g Q v)

theorem MIPRE.Introspection.Honest.registerOp_commute {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) {P Q : Matrix J J ℂ} (hc : Commute P Q) : Commute (registerOp e P) (registerOp e Q)

theorem MIPRE.Introspection.Honest.kronecker_commute {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {P P' : Matrix I I ℂ} {Q Q' : Matrix J J ℂ} (hP : Commute P P') (hQ : Commute Q Q') : Commute (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P Q) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P' Q')

theorem MIPRE.Introspection.Honest.adaptiveTensor_commute {I : Type u_1} {J : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [Fintype C] [DecidableEq C] (P : A → Matrix I I ℂ) (hP : IsPVM P) (Q : A → B → Matrix J J ℂ) (R : A → C → Matrix J J ℂ) (hc : ∀ (a : A) (b : B) (c : C), Commute (Q a b) (R a c)) (ab : A × B) (ac : A × C) : Commute (adaptiveTensor P Q ab) (adaptiveTensor P R ac)

Shared earlier outcomes either agree, or orthogonality kills both products.

theorem MIPRE.Introspection.Honest.pauliX_commute_stopHide {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (V : Finset ι) (x : ↥V → F) (a : HideLabel F ι) : Commute (Weyl.proj Weyl.wX x) (stopHide P V a)

theorem MIPRE.Introspection.Honest.localDual_commute_read {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S : Finset ι} (L : CL.RegLinear F S) (b : Fin (Fintype.card ↥S) → F) (a : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) : Commute (Weyl.synOf Weyl.wX (⇑(CL.lperp (coordinateLinear L))) b) (localRead L a)

theorem MIPRE.Introspection.Honest.stopHide_commute_adaptive {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {B : Type u_3} {U : Type u_4} [Fintype B] [DecidableEq B] [Fintype U] [DecidableEq U] (S V : Finset ι) (h : S ⊆ V) (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (Q : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F) → B → Matrix (↥(V \ S) → F) (↥(V \ S) → F) ℂ) (hc : ∀ (z : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (x : ↥(V \ S) → F) (b : B), Commute (Weyl.proj Weyl.wX x) (Q z b)) (f : ((Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) × B → U) (a : HideLabel F ι) (b : U) : Commute (stopHide (CL.CLFun.cons S L next) V a) (registerOp (coordinateSplit S V h) (coarseOp f (adaptiveTensor (localRead L) Q) b))

A stopping node commutes with the next local joint read and any X-compatible tail.

theorem MIPRE.Introspection.Honest.hideRegister_commute_next {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (V : Finset ι) (h : P.SupportedOn V) (a b : HideLabel F ι) : Commute (hideRegister P k V h a) (hideRegister P (k + 1) V h b)

Every pair of neighboring honest hiding levels commutes on every answer label.

theorem MIPRE.Introspection.Honest.pauliX_commute_readRegister_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (P : CL.CLFun F ι 0) (V : Finset ι) (h : P.SupportedOn V) (x : ↥V → F) (a : ReadLabel F ι) : Commute (Weyl.proj Weyl.wX x) (readRegister P V h a)

theorem MIPRE.Introspection.Honest.hideRegister_commute_read {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : ℓ ≤ k + 1) (V : Finset ι) (h : P.SupportedOn V) (a : HideLabel F ι) (b : ReadLabel F ι) : Commute (hideRegister P k V h a) (readRegister P V h b)

The terminal honest hiding level commutes with the complete adaptive Read family.

theorem MIPRE.Introspection.Honest.hideOp_commute_next {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (h : P.SupportedOn Finset.univ) (a b : HideLabel F ι) : Commute (hideOp P k h a) (hideOp P (k + 1) h b)

theorem MIPRE.Introspection.Honest.hideOp_commute_read {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : ℓ ≤ k + 1) (h : P.SupportedOn Finset.univ) (a : HideLabel F ι) (b : ReadLabel F ι) : Commute (hideOp P k h a) (readOp P h b)