Attained outputs of honest Introspect measurements

The honest Introspect readout has zero effect on every claimed question outside the source computation's image. This support statement needs no assumption on the source strategy's value or commutation.

theorem MIPRE.Introspection.Honest.coreOp_eq_zero_of_unattained {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (t : CoreType) (y : ι → F) (a : A) (hy : ¬∃ (x : ι → F), displayed L t x = y) : coreOp L D R t (y, a) = 0

theorem MIPRE.Introspection.Honest.coreOp_displayed_attained {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (t : CoreType) (y : ι → F) (a : A) (ha : coreOp L D R t (y, a) ≠ 0) : ∃ (x : ι → F), displayed L t x = y

theorem MIPRE.Introspection.Honest.introspectOp_output_attained {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (w : Bool) (y : ι → F) (a : A) (ha : coreOp L D R (false, w) (y, a) ≠ 0) : ∃ (x : ι → F), (L w).eval x = y

A nonzero honest Introspect answer reports an actual full source output.

theorem MIPRE.Introspection.Honest.parsedIntrospectOp_output_attained {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [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) (y : ι → F) (a : A) (ha : parsedCoreOp L D R (false, w) (ParsedAnswer.pair y a) ≠ 0) : ∃ (x : ι → F), (L w).eval x = y

theorem MIPRE.Introspection.Honest.auxOp_introspect_output_attained {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype PA] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (R : SyncStrategy (sourceGame L D).doubled) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (w : Bool) (y : ι → F) (a : A) (ha : auxOp L D R hL (AuxType.introspect, w) (ParsedAnswer.pair y a) ≠ 0) : ∃ (x : ι → F), (L w).eval x = y