Full typed introspection completeness for arbitrary binary source lengths

The original s coordinates are placed in the first s positions of an explicitly numbered 2^m*t-qubit register. The original CL presentation is extended by zero and its decider restricts to the original coordinates. No field-linearity condition is imposed on the source CL functions.

The same-depth depthPaddedGame uses full-register auxiliary checks. Enlarging the first factor can give dual Read/Hide labels with nonzero spectator bits, even though the ordinary CL output is zero there. An executable verifier with strict original-subspace answer guards therefore needs full-register checks or a separate answer-format/coarsening bridge; that compiler identification is not asserted by this finite-game theorem.

def MIPRE.Introspection.BinaryComplete.coordNumbering (m t : ℕ) : Coord m t ≃ Fin (2 ^ m * t)

Binary ordering of the Boolean hypercube, then the field-basis bit.

Equations

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

def MIPRE.Introspection.BinaryComplete.paddingEmbedding {s m t : ℕ} (hs : s ≤ 2 ^ m * t) : Fin s ↪ Coord m t

Pad in the initial numbered coordinates, with an explicit inverse label.

Equations

• MIPRE.Introspection.BinaryComplete.paddingEmbedding hs = (Fin.castLEEmb hs).trans (MIPRE.Introspection.BinaryComplete.coordNumbering m t).symm.toEmbedding

theorem MIPRE.Introspection.BinaryComplete.paddingEmbedding_number {s m t : ℕ} (hs : s ≤ 2 ^ m * t) (i : Fin s) : ↑((coordNumbering m t) ((paddingEmbedding hs) i)) = ↑i

theorem MIPRE.Introspection.BinaryComplete.card_seed (m t : ℕ) : Fintype.card (Seed m t) = 2 ^ (2 ^ m * t)

noncomputable def MIPRE.Introspection.BinaryComplete.paddedGame {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] {m d ℓ t s : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Fin s) ℓ) (D : (Fin s → ZMod 2) → (Fin s → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hs : s ≤ 2 ^ m * t) : Game (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (ParsedAnswer (Coord m t → ZMod 2) A (QLD.Answer F m d)) (ParsedAnswer (Coord m t → ZMod 2) A (QLD.Answer F m d))

The actual full parsed game on the padded original CL maps.

Equations

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

theorem MIPRE.Introspection.BinaryComplete.exists_padded_perfectPCC {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t s : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Fin s) ℓ) (D : (Fin s → ZMod 2) → (Fin s → ZMod 2) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hb : LowDegree.IsSelfDualBasis b) (hd : 1 ≤ d) (hs : s ≤ 2 ^ m * t) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (hR : R.IsPCC) (hv : R.value = 1) : ∃ (Q : SyncStrategy (paddedGame L D hm b hs).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = 2 ^ (2 ^ m * t + 1) * R.d

Any binary original CL game fits the honest construction after explicit zero padding. The extra dimension is exactly the full qubit register and one Magic Square qubit; the original strategy dimension is retained.

noncomputable def MIPRE.Introspection.BinaryComplete.depthPaddedGame {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] {m d ℓ t s : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Fin s) ℓ) (D : (Fin s → ZMod 2) → (Fin s → ZMod 2) → A → A → Bool) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hs : s ≤ 2 ^ m * t) : Game (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (CL.Detyping.Question (QuestionType QLD.Ty ℓ) (Fin ((3 * m + 3) * t))) (ParsedAnswer (Coord m t → ZMod 2) A (QLD.Answer F m d)) (ParsedAnswer (Coord m t → ZMod 2) A (QLD.Answer F m d))

The exact-partition construction at the original positive depth.

Equations

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

theorem MIPRE.Introspection.BinaryComplete.exists_depthPadded_perfectPCC {F : Type u_1} {A : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {m d ℓ t s : ℕ} [NeZero m] (L : Bool → CL.CLFun (ZMod 2) (Fin s) ℓ) (D : (Fin s → ZMod 2) → (Fin s → ZMod 2) → A → A → Bool) (R : SyncStrategy (Honest.sourceGame L D).doubled) (hm : m ∣ Fintype.card F) (b : Module.Basis (Fin t) (ZMod 2) F) (hb : LowDegree.IsSelfDualBasis b) (hd : 1 ≤ d) (hs : s ≤ 2 ^ m * t) (hℓ : 0 < ℓ) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (hR : R.IsPCC) (hv : R.value = 1) : (∀ (w : Bool), (SourcePadding.depthFamily (paddingEmbedding hs) L w).ExactlyOn Finset.univ) ∧ ∃ (Q : SyncStrategy (depthPaddedGame L D hm b hs).doubled), Q.IsPCC ∧ Q.value = 1 ∧ Q.d = 2 ^ (2 ^ m * t + 1) * R.d

Arbitrary binary exact CL samplers extend to the complete typed introspection game without changing their level count.