Support of the actual honest Read and Hide answers

A nonzero entry of either adaptive measurement forces every reported vector to lie in the active coordinate register. The statements cover the full answer alphabet: no support or honest-format assumption is imposed on the answer.

theorem MIPRE.Introspection.Honest.support_mono {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S V : Finset ι} (h : S ⊆ V) {x : ι → F} (hx : (CL.proj S) x = x) : (CL.proj V) x = x

theorem MIPRE.Introspection.Honest.proj_coordinateInsert_of_subset {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {S V : Finset ι} (h : S ⊆ V) (x : Fin (Fintype.card ↥S) → F) : (CL.proj V) ((coordinateInsert S) x) = (coordinateInsert S) x

theorem MIPRE.Introspection.Honest.stopHideAnswer_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) (x : ↥V → F) : (CL.proj V) (stopHideAnswer P V x).1 = (stopHideAnswer P V x).1 ∧ (CL.proj V) (stopHideAnswer P V x).2.1 = (stopHideAnswer P V x).2.1 ∧ (CL.proj V) (stopHideAnswer P V x).2.2 = (stopHideAnswer P V x).2.2

All three stopping-Hide vectors are supported on the active register.

theorem MIPRE.Introspection.Honest.stopHide_entry_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 : HideLabel F ι) (x x' : ↥V → F) (ha : stopHide P V a x x' ≠ 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

A nonzero stopping-Hide entry has no reported coordinates outside its register.

theorem MIPRE.Introspection.Honest.readRegister_entry_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 ι) (x x' : ↥V → F) (ha : readRegister P V h a x x' ≠ 0) : (CL.proj V) a.1 = a.1 ∧ (CL.proj V) a.2 = a.2

Both labels of every nonzero Read entry are supported in the active register.

theorem MIPRE.Introspection.Honest.hideRegister_entry_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 ι) (x x' : ↥V → F) (ha : hideRegister P k V h a x x' ≠ 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

Every component of a nonzero Hide entry is supported in the active register.