Perfect PCC completeness of the four-type introspection core

This is the actual induced subgraph on the two Introspect and two Sample types, with the restriction of the parsed typed predicate. The constructed strategy is a concrete seed-register extension of the original PCC strategy. Read, Hide, and Pauli vertices are not part of this intermediate theorem.

def MIPRE.Introspection.Honest.CoreAdj (t u : CoreType) : Prop

Equations

• MIPRE.Introspection.Honest.CoreAdj t u = (t.2 = u.2 ∨ t.1 = false ∧ u.1 = false)

noncomputable def MIPRE.Introspection.Honest.coreCheck {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) (t u : CoreType) (a b : (ι → F) × A) : Bool

Restrict the actual parsed predicate to core types and pair-format answers.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.Honest.coreCheck_eq {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) {P : Type u_4} {PA : Type u_5} (X Z : P) (projectPauli : PA → ι → F) (DP : P → P → PA → PA → Bool) (t u : CoreType) (a b : (ι → F) × A) : coreCheck L D t u a b = TypedPredicate.check L X Z projectPauli D DP (coreType t) (coreType u) (ParsedAnswer.pair a.1 a.2) (ParsedAnswer.pair b.1 b.2)

The Pauli parameters have no effect on this restriction.

theorem MIPRE.Introspection.Honest.coreCheck_common {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (hR : R.IsPCC) (hval : R.value = 1) (t u : CoreType) (z : ι → F) (a b : A) (hNZ : R.P.M (t.2, (L t.2).eval z) a * R.P.M (u.2, (L u.2).eval z) b ≠ 0) : coreCheck L D t u (displayed L t z, a) (displayed L u z, b) = true

A nonzero honest seed block always produces an accepted core answer pair.

theorem MIPRE.Introspection.Honest.coreOp_reject_zero {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (hR : R.IsPCC) (hval : R.value = 1) (t u : CoreType) (ya zb : (ι → F) × A) (hD : coreCheck L D t u ya zb = false) : coreOp L D R t ya * coreOp L D R u zb = 0

Rejected answers have zero operator product, for every core question pair.

noncomputable def MIPRE.Introspection.Honest.coreGame {F : Type u_1} {ι : Type u_2} {A : Type u_3} [Field F] [Fintype F] [Fintype ι] [DecidableEq ι] [Fintype A] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (D : (ι → F) → (ι → F) → A → A → Bool) : Game CoreType CoreType ((ι → F) × A) ((ι → F) × A)

The uniform ordered-edge game on the induced core graph.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPRE.Introspection.Honest.coreStrategy {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) : SyncStrategy (coreGame L D).doubled

A concrete synchronous honest strategy; the outer doubling tag is ignored.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.Honest.coreStrategy_dimension {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) : (coreStrategy L D R).d = Fintype.card (ι → F) * R.d

theorem MIPRE.Introspection.Honest.coreStrategy_isPCC {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (hR : R.IsPCC) : (coreStrategy L D R).IsPCC

theorem MIPRE.Introspection.Honest.coreStrategy_value {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (hR : R.IsPCC) (hval : R.value = 1) : (coreStrategy L D R).value = 1

theorem MIPRE.Introspection.Honest.exists_corePerfectPCC {F : Type u_1} {ι : Type u_2} {A : Type u_3} [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) (hR : R.IsPCC) (hval : R.value = 1) : ∃ (Q : SyncStrategy (coreGame L D).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = Fintype.card (ι → F) * R.d

Perfect PCC completeness for all four honest core types and every source CL depth.