Exact products at an honest hiding transition

theorem MIPRE.Introspection.Honest.registerOp_ne_zero {I : Type u_1} {J : Type u_2} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ≃ J) (P : Matrix J J ℂ) : registerOp e P ≠ 0 ↔ P ≠ 0

theorem MIPRE.Introspection.Honest.coarseOp_product_ne_zero {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 ℂ) (u : U) (v : V) (h : coarseOp f P u * coarseOp g Q v ≠ 0) : ∃ (a : A) (b : B), f a = u ∧ g b = v ∧ P a * Q b ≠ 0

theorem MIPRE.Introspection.Honest.adaptiveTensor_product_ne_zero {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 ℂ) (ab : A × B) (ac : A × C) (h : adaptiveTensor P Q ab * adaptiveTensor P R ac ≠ 0) : ab.1 = ac.1 ∧ Q ab.1 ab.2 * R ac.1 ac.2 ≠ 0

theorem MIPRE.Introspection.Honest.pauliX_mul_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 ι) : Weyl.proj Weyl.wX x * stopHide P V a = if stopHideAnswer P V x = a then Weyl.proj Weyl.wX x else 0

A complete X answer fixes the stopping Hide answer exactly.

theorem MIPRE.Introspection.Honest.localDual_mul_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)) : Weyl.synOf Weyl.wX (⇑(CL.lperp (coordinateLinear L))) b * localRead L a = if b = a.2 then localRead L a else 0

The current local dual value is retained by the next joint Z/dual-X read.

theorem MIPRE.Introspection.Honest.stop_local_product {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (S V : Finset ι) (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (bt : (Fin (Fintype.card ↥S) → F) × (↥(V \ S) → F)) (a : (Fin (Fintype.card ↥S) → F) × (Fin (Fintype.card ↥S) → F)) (v : HideLabel F ι) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.synOf Weyl.wX (⇑(CL.lperp (coordinateLinear L))) bt.1) (Weyl.proj Weyl.wX bt.2) * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (localRead L a) (stopHide (next ((coordinateInsert S) a.1)) (V \ S) v) = if bt.1 = a.2 ∧ stopHideAnswer (next ((coordinateInsert S) a.1)) (V \ S) bt.2 = v then Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (localRead L a) (Weyl.proj Weyl.wX bt.2) else 0

Both tested X data are retained at the first actual adaptive hiding transition.