Attained prefixes of honest hiding and reading outcomes

The honest register matrices already vanish outside the image of the relevant CL computation. These lemmas expose that support on whole operators and on the complete parsed-answer alphabet, so executable prefix scans may reject unattained claims without changing honest measurements.

theorem MIPRE.Introspection.Honest.hideOp_output_attained {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 : HideLabel F ι) (ha : hideOp P k h a ≠ 0) : ∃ (x : ι → F), (CL.CLFun.truncate k P).eval x = a.1

A nonzero honest Hide outcome reports an actual output after exactly k stages.

theorem MIPRE.Introspection.Honest.hideOp_prefix_attained {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 : HideLabel F ι) (ha : hideOp P k h a ≠ 0) (j : ℕ) (hj : j ≤ k) : ∃ (x : ι → F), (CL.CLFun.truncate j P).eval x = P.outputPrefix j a.1

Every earlier prefix of a nonzero honest Hide claim is attained by the same seed.

theorem MIPRE.Introspection.Honest.readOp_output_attained {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (a : ReadLabel F ι) (ha : readOp P h a ≠ 0) : ∃ (x : ι → F), P.eval x = a.1

A nonzero honest Read outcome reports an actual complete CL output.

theorem MIPRE.Introspection.Honest.readOp_prefix_attained {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (a : ReadLabel F ι) (ha : readOp P h a ≠ 0) (j : ℕ) : ∃ (x : ι → F), (CL.CLFun.truncate j P).eval x = P.outputPrefix j a.1

Every prefix of a nonzero honest Read claim is attained, including ℓ - 1.

theorem MIPRE.Introspection.Honest.parsedHideOp_prefix_attained {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} {PA : Type u_4} [Fintype A] [DecidableEq A] [Fintype PA] (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (w : Bool) (k : ℕ) (h : (L w).SupportedOn Finset.univ) (y yp z : ι → F) (ha : parsedHideOp L D R w k h (ParsedAnswer.hide y yp z) ≠ 0) (j : ℕ) (hj : j ≤ k) : ∃ (x : ι → F), (CL.CLFun.truncate j (L w)).eval x = (L w).outputPrefix j y

Tensoring with the source identity does not create unattained Hide labels.

theorem MIPRE.Introspection.Honest.parsedReadOp_prefix_attained {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} {PA : Type u_4} [Fintype A] [DecidableEq A] [Fintype PA] (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (w : Bool) (h : (L w).SupportedOn Finset.univ) (y yp : ι → F) (a : A) (ha : parsedReadOp L D R w h (ParsedAnswer.read y yp a) ≠ 0) (j : ℕ) : ∃ (x : ι → F), (CL.CLFun.truncate j (L w)).eval x = (L w).outputPrefix j y

Tensoring with the source answer effect does not create unattained Read labels.

theorem MIPRE.Introspection.Honest.auxOp_nonzero_prefixGuard {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} {PA : Type u_4} [Fintype A] [DecidableEq A] [Fintype PA] (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) {P : Type u_5} (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (t : AuxQuestion ℓ) (a : ParsedAnswer (ι → F) A PA) (ha : auxOp L D R hL t a ≠ 0) : PrefixGuard.holds L (Sum.inr t) a

Every nonzero honest auxiliary effect passes the local prefix guard. The claim includes every parsed label, so no format promise is needed.