Honest guarded quotient completeness with the actual register numbering

The source CL family remains on its given coordinate type. Only its honest construction is expressed temporarily in the binary Weyl coordinates. Quotient transport then returns the strategy to the original coordinates, with exact dimension and with support certificates for both kinds of executable guards.

noncomputable def MIPRE.Introspection.NumberedComplete.project {F : Type u_1} {I : Type u_3} [Field F] [Algebra (ZMod 2) F] {m t d : ℕ} (e : I ≃ BinaryComplete.Coord m t) (b : Module.Basis (Fin t) (ZMod 2) F) (a : QLD.Answer F m d) : I → ZMod 2

Equations

• MIPRE.Introspection.NumberedComplete.project e b a = (MIPRE.CL.reindexEquiv e).symm (MIPRE.Introspection.BinaryComplete.project b a)

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.NumberedComplete.game {F : Type u_1} {A : Type u_2} {I : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) : Game (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (ParsedAnswer (I → ZMod 2) A (QLD.Answer F m d)) (ParsedAnswer (I → ZMod 2) A (QLD.Answer F m d))

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.NumberedComplete.guardedGame {F : Type u_1} {A : Type u_2} {I : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) : Game (QuestionType QLD.Ty ℓ × (Fin ((3 * m + 3) * t) → ZMod 2)) (QuestionType QLD.Ty ℓ × (Fin ((3 * m + 3) * t) → ZMod 2)) (ParsedAnswer (I → ZMod 2) A (QLD.Answer F m d)) (ParsedAnswer (I → ZMod 2) A (QLD.Answer F m d))

Equations

• MIPRE.Introspection.NumberedComplete.guardedGame e L D hm b χ π = MIPRE.Introspection.PrefixGuard.game L Prod.fst (MIPRE.Introspection.NumberedComplete.game e L D hm b χ π)

theorem MIPRE.Introspection.NumberedComplete.coordinate_exists_perfectPCC_with_format {F : Type u_1} {A : Type u_2} {I : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hb : LowDegree.IsSelfDualBasis b) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (hd : 1 ≤ d) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hv : R.value = 1) : ∃ (Q : SyncStrategy (AuxiliaryQuotient.reindexedGame e QLD.adj (QLD.Ty.pauli QLD.Bas.X) (QLD.Ty.pauli QLD.Bas.Z) (QLD.PauliCL.ExplicitSeed.binaryPresentation χ b) L (project e b) D (ExplicitGame.pauliCheck hm π b)).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = 2 * Fintype.card (BinaryComplete.Seed m t) * R.d ∧ (∀ (q : Bool × CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (a : ParsedAnswer (BinaryComplete.Coord m t → ZMod 2) A (QLD.Answer F m d)), Q.P.M q a ≠ 0 → PrefixGuard.holds (SourceReindex.family e L) q.2.1 a) ∧ (∀ (side w : Bool) (payload : Fin ((3 * m + 3) * t) → ZMod 2) (y : BinaryComplete.Coord m t → ZMod 2) (a : A), Q.P.M (side, Sum.inr (AuxType.introspect, w), payload) (ParsedAnswer.pair y a) ≠ 0 → ∃ (x : BinaryComplete.Coord m t → ZMod 2), (SourceReindex.family e L w).eval x = y) ∧ ∀ (side : Bool) (p : QLD.Ty) (payload : Fin ((3 * m + 3) * t) → ZMod 2) (a : QLD.Answer F m d), Q.P.M (side, Sum.inl p, payload) (ParsedAnswer.pauli a) ≠ 0 → (QLD.PauliCL.ExplicitSeed.binaryDecode π b p payload).fmtOk a = true

The temporary coordinate game has a perfect honest PCC strategy, including the exact support facts needed after transporting back to the finite register.

theorem MIPRE.Introspection.NumberedComplete.exists_perfectPCC_with_format {F : Type u_1} {A : Type u_2} {I : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] [Fintype I] [DecidableEq I] {m t d ℓ : ℕ} [NeZero m] (e : I ≃ BinaryComplete.Coord m t) (L : Bool → CL.CLFun (ZMod 2) I ℓ) (D : (I → ZMod 2) → (I → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (χ : F → Fin m) (π : F ≃ F) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hb : LowDegree.IsSelfDualBasis b) (hχ : ∀ (s : F), LIDT.CL.chi hm (π s) = χ s) (hd : 1 ≤ d) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hv : R.value = 1) : ∃ (Q : SyncStrategy (guardedGame e L D hm b χ π).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = 2 * Fintype.card (BinaryComplete.Seed m t) * R.d ∧ (∀ (q : Bool × QuestionType QLD.Ty ℓ × (Fin ((3 * m + 3) * t) → ZMod 2)) (a : ParsedAnswer (I → ZMod 2) A (QLD.Answer F m d)), Q.P.M q a ≠ 0 → PrefixGuard.holds L q.2.1 a) ∧ (∀ (side w : Bool) (payload : Fin ((3 * m + 3) * t) → ZMod 2) (y : I → ZMod 2) (a : A), Q.P.M (side, Sum.inr (AuxType.introspect, w), payload) (ParsedAnswer.pair y a) ≠ 0 → ∃ (x : I → ZMod 2), (L w).eval x = y) ∧ ∀ (side : Bool) (p : QLD.Ty) (payload : Fin ((3 * m + 3) * t) → ZMod 2) (a : QLD.Answer F m d), Q.P.M (side, Sum.inl p, payload) (ParsedAnswer.pauli a) ≠ 0 → (QLD.PauliCL.ExplicitSeed.binaryDecode π b p payload).fmtOk a = true

Perfect PCC completeness after coordinate transport and executable prefix guards. Introspect labels still lie in the actual original source-output range.