Exact coarse-measurement algebra for honest Pauli edges

theorem MIPRE.QLD.Honest.fibre_commute {I : Type u_1} {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype I] [Fintype X] [Fintype Y] [DecidableEq A] [DecidableEq B] (M : X → Matrix I I ℂ) (N : Y → Matrix I I ℂ) (f : X → A) (g : Y → B) (hc : ∀ (x : X) (y : Y), Commute (M x) (N y)) (a : A) (b : B) : Commute (fibSum M f a) (fibSum N g b)

theorem MIPRE.QLD.Honest.fibre_reject {I : Type u_1} {X : Type u_2} {Y : Type u_3} {A : Type u_4} {B : Type u_5} [Fintype I] [Fintype X] [Fintype Y] [DecidableEq A] [DecidableEq B] (M : X → Matrix I I ℂ) (N : Y → Matrix I I ℂ) (f : X → A) (g : Y → B) (D : A → B → Bool) (hz : ∀ (x : X) (y : Y), D (f x) (g y) = false → M x * N y = 0) (a : A) (b : B) (hr : D a b = false) : fibSum M f a * fibSum N g b = 0

theorem MIPRE.QLD.Honest.pvm_fibre_commute {I : Type u_1} {X : Type u_2} {A : Type u_4} {B : Type u_5} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq A] [DecidableEq B] (P : X → Matrix I I ℂ) (hP : IsPVM P) (f : X → A) (g : X → B) (a : A) (b : B) : Commute (fibSum P f a) (fibSum P g b)

theorem MIPRE.QLD.Honest.pvm_fibre_reject {I : Type u_1} {X : Type u_2} {A : Type u_4} {B : Type u_5} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq A] [DecidableEq B] (P : X → Matrix I I ℂ) (hP : IsPVM P) (f : X → A) (g : X → B) (D : A → B → Bool) (hgood : ∀ (x : X), D (f x) (g x) = true) (a : A) (b : B) (hr : D a b = false) : fibSum P f a * fibSum P g b = 0

theorem MIPRE.QLD.Honest.readout_constant {I : Type u_1} {A : Type u_4} [DecidableEq I] [DecidableEq A] (x₀ x : A) : Introspection.readout (fun (x : I) => x₀) x = if x₀ = x then 1 else 0

theorem MIPRE.QLD.Honest.readout_constant_commute {I : Type u_1} {A : Type u_4} [Fintype I] [DecidableEq I] [DecidableEq A] (x₀ x : A) (M : Matrix I I ℂ) : Commute (Introspection.readout (fun (x : I) => x₀) x) M

theorem MIPRE.QLD.Honest.fibre_comp {I : Type u_1} {X : Type u_2} {A : Type u_4} {B : Type u_5} [Fintype X] [DecidableEq A] [DecidableEq B] [Fintype A] (P : X → Matrix I I ℂ) (f : X → A) (g : A → B) (b : B) : fibSum (fibSum P f) g b = fibSum P (fun (x : X) => g (f x)) b

theorem MIPRE.QLD.Honest.liftOp_fibSum {F : Type u_1} {m : ℕ} {X : Type u_2} {A : Type u_3} [Fintype X] [DecidableEq A] (P : X → Matrix (Register F m) (Register F m) ℂ) (f : X → A) (a : A) : liftOp (fibSum P f a) = fibSum (fun (x : X) => liftOp (P x)) f a

theorem MIPRE.QLD.Honest.probeLift_eq_fibSum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {m : ℕ} (ω : Omega F m) (W : Bas) : probeLift ω W = fibSum (pauliLift W) (probeLabel ω W)