Honest measurements on the complete parsed-answer alphabet

The actual core, Read and Hide operators act on one common register/source space. Wrong constructors have zero effect. This retains every answer label, gives genuine PVMs, and makes the Introspect/Read operator tests apply without a promise that the reported constructors are well formed.

theorem MIPRE.Introspection.Honest.sum_supported {B : Type u_5} {C : Type u_6} {M : Type u_7} [Fintype B] [Fintype C] [AddCommMonoid M] (f : B → C) (hf : Function.Injective f) (g : C → M) (hz : ∀ c ∉ Set.range f, g c = 0) : ∑ c : C, g c = ∑ b : B, g (f b)

def MIPRE.Introspection.Honest.parsedCoreOp {F : Type u_1} {ι : Type u_2} {A : Type u_3} {PA : Type u_4} [Field F] [Fintype F] [DecidableEq 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) : ParsedAnswer (ι → F) A PA → Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Introspect and Sample use their actual core operators on pair answers.

Equations

• MIPRE.Introspection.Honest.parsedCoreOp L D R t (MIPRE.Introspection.ParsedAnswer.pair y a) = MIPRE.Introspection.Honest.coreOp L D R t (y, a)
• MIPRE.Introspection.Honest.parsedCoreOp L D R t x✝ = 0

noncomputable def MIPRE.Introspection.Honest.parsedReadOp {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] {ℓ : ℕ} (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) : ParsedAnswer (ι → F) A PA → Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Read uses the full adaptive register and source-answer measurement.

Equations

• MIPRE.Introspection.Honest.parsedReadOp L D R w h (MIPRE.Introspection.ParsedAnswer.read y yp a) = MIPRE.Introspection.Honest.fullReadOp L D R w h ((y, yp), a)
• MIPRE.Introspection.Honest.parsedReadOp L D R w h x✝ = 0

noncomputable def MIPRE.Introspection.Honest.parsedHideOp {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] {ℓ : ℕ} (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) : ParsedAnswer (ι → F) A PA → Matrix ((ι → F) × Fin R.d) ((ι → F) × Fin R.d) ℂ

Hide acts on the genuine adaptive hiding register, leaving the source register alone.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.Honest.parsedHideOp L D R w k h x✝ = 0

@[simp]

theorem MIPRE.Introspection.Honest.parsedCoreOp_pair {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) (t : CoreType) (y : ι → F) (a : A) : parsedCoreOp L D R t (ParsedAnswer.pair y a) = coreOp L D R t (y, a)

@[simp]

theorem MIPRE.Introspection.Honest.parsedReadOp_read {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) (h : (L w).SupportedOn Finset.univ) (y yp : ι → F) (a : A) : parsedReadOp L D R w h (ParsedAnswer.read y yp a) = fullReadOp L D R w h ((y, yp), a)

@[simp]

theorem MIPRE.Introspection.Honest.parsedHideOp_hide {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) (k : ℕ) (h : (L w).SupportedOn Finset.univ) (y yp x : ι → F) : parsedHideOp L D R w k h (ParsedAnswer.hide y yp x) = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (hideOp (L w) k h (y, yp, x)) 1

theorem MIPRE.Introspection.Honest.parsedCoreOp_isPVM {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) (t : CoreType) : IsPVM (parsedCoreOp L D R t)

theorem MIPRE.Introspection.Honest.parsedReadOp_isPVM {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) (h : (L w).SupportedOn Finset.univ) : IsPVM (parsedReadOp L D R w h)

theorem MIPRE.Introspection.Honest.parsedHideOp_isPVM {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) (k : ℕ) (h : (L w).SupportedOn Finset.univ) : IsPVM (parsedHideOp L D R w k h)

theorem MIPRE.Introspection.Honest.parsedCore_read_commute {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) (h : (L w).SupportedOn Finset.univ) (a b : ParsedAnswer (ι → F) A PA) : Commute (parsedCoreOp L D R (false, w) a) (parsedReadOp L D R w h b)

Wrong constructor labels commute trivially; proper labels use the actual Read refinement.

theorem MIPRE.Introspection.Honest.parsedRead_core_commute {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) (h : (L w).SupportedOn Finset.univ) (a b : ParsedAnswer (ι → F) A PA) : Commute (parsedReadOp L D R w h a) (parsedCoreOp L D R (false, w) b)

theorem MIPRE.Introspection.Honest.parsedCore_read_reject_zero {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) {P : Type u_5} (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (w : Bool) (h : (L w).SupportedOn Finset.univ) (a b : ParsedAnswer (ι → F) A PA) (hr : TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.introspect, w)) (Sum.inr (AuxType.read, w)) a b = false) : parsedCoreOp L D R (false, w) a * parsedReadOp L D R w h b = 0

Every rejected pair of parsed labels on the reading edge has zero operator product.

theorem MIPRE.Introspection.Honest.parsedRead_core_reject_zero {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) {P : Type u_5} (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (w : Bool) (h : (L w).SupportedOn Finset.univ) (a b : ParsedAnswer (ι → F) A PA) (hr : TypedPredicate.check L X Z projectPauli D DP (Sum.inr (AuxType.read, w)) (Sum.inr (AuxType.introspect, w)) a b = false) : parsedReadOp L D R w h a * parsedCoreOp L D R (false, w) b = 0

The reversed ordered reading edge has the same all-label rejection guarantee.