Perfect acceptance along the honest adaptive hiding chain

A nonzero product of two neighboring honest measurements satisfies the actual CL hiding check. The proof follows the same adaptive branches as the concrete operators, using zero products to exclude incompatible earlier outcomes.

theorem MIPRE.Introspection.Honest.exists_entry_ne_zero {I : Type u_3} (M : Matrix I I ℂ) (h : M ≠ 0) : ∃ (i : I) (j : I), M i j ≠ 0

theorem MIPRE.Introspection.Honest.hideRegister_supported {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 : HideLabel F ι) (ha : hideRegister P k V h a ≠ 0) : (CL.proj V) a.1 = a.1 ∧ (CL.proj V) a.2.1 = a.2.1 ∧ (CL.proj V) a.2.2 = a.2.2

theorem MIPRE.Introspection.Honest.readRegister_supported {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 ι) (h : P.SupportedOn V) (a : ReadLabel F ι) (ha : readRegister P V h a ≠ 0) : (CL.proj V) a.1 = a.1 ∧ (CL.proj V) a.2 = a.2

theorem MIPRE.Introspection.Honest.hideRegister_accepts_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 : ℕ) (hk : k + 1 < ℓ) (V : Finset ι) (h : P.SupportedOn V) (a b : HideLabel F ι) (hab : hideRegister P k V h a * hideRegister P (k + 1) V h b ≠ 0) : CLChecks.hidingNext P k a b

Nonzero neighboring Hide products satisfy all four actual hiding comparisons.

theorem MIPRE.Introspection.Honest.readRegister_zero_eq {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) (a : ReadLabel F ι) : readRegister P V h a = if a = (0, 0) then 1 else 0

theorem MIPRE.Introspection.Honest.hideRegister_accepts_read {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : k + 1 = ℓ) (V : Finset ι) (h : P.SupportedOn V) (a : HideLabel F ι) (b : ReadLabel F ι) (c : A) (hab : hideRegister P k V h a * readRegister P V h b ≠ 0) : CLChecks.hidingRead P a (b.1, b.2, c)

The terminal Hide/Read product satisfies the actual common-prefix/full-dual check.

theorem MIPRE.Introspection.Honest.hideOp_reject_next_zero {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 b : HideLabel F ι) (hab : ¬CLChecks.hidingNext P k a b) : hideOp P k h a * hideOp P (k + 1) h b = 0

Every rejected actual adjacent hiding comparison has zero honest operator product.

theorem MIPRE.Introspection.Honest.hideOp_reject_read_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} (P : CL.CLFun F ι ℓ) (k : ℕ) (hk : k + 1 = ℓ) (h : P.SupportedOn Finset.univ) (a : HideLabel F ι) (b : ReadLabel F ι) (c : A) (hab : ¬CLChecks.hidingRead P a (b.1, b.2, c)) : hideOp P k h a * readOp P h b = 0

Every rejected terminal hiding/Read comparison has zero honest register product.