The finite game at the compiler's canonical parameters

These definitions use the executable field, basis, selector, and register numbering. The original answers retain their bounded finite alphabet.

theorem MIPRE.Introspection.CanonicalGame.power_neZero (c lam n : ℕ) : NeZero (SourceCompiler.registerPower c lam n)

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalGame.field (c lam n : ℕ) : SAT.BinField (SourceCompiler.fieldBits c lam n)

Equations

• MIPRE.Introspection.CanonicalGame.field c lam n = MIPRE.SAT.shoupBinField (MIPRE.Introspection.SourceCompiler.fieldBits c lam n) ⋯

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalGame.basis (c : ℕ) (he : Even c) (lam n : ℕ) : Module.Basis (Fin (SourceCompiler.fieldBits c lam n)) (ZMod 2) (SAT.shoupBinField (SourceCompiler.fieldBits c lam n) ⋯).carrier

Equations

• MIPRE.Introspection.CanonicalGame.basis c he lam n = MIPRE.SAT.shoupSelfDualNormalBasis (MIPRE.Introspection.SourceCompiler.fieldBits c lam n) ⋯ ⋯

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalGame.selector (c : ℕ) (hc : 1 ≤ c) (lam n : ℕ) (a : (field c lam n).carrier) : Fin (2 ^ PauliSamplerParameters.selectorBits c lam n)

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalGame.permutation (c lam n : ℕ) : (field c lam n).carrier ≃ (field c lam n).carrier

Equations

• MIPRE.Introspection.CanonicalGame.permutation c lam n = MIPRE.QLD.PauliCL.ExplicitSeed.seedPermutation (MIPRE.Introspection.CanonicalGame.field c lam n)

theorem MIPRE.Introspection.CanonicalGame.divides (c : ℕ) (hc : 1 ≤ c) (lam n : ℕ) : SourceCompiler.registerPower c lam n ∣ Fintype.card (field c lam n).carrier

theorem MIPRE.Introspection.CanonicalGame.selector_eq (c : ℕ) (hc : 1 ≤ c) (lam n : ℕ) (s : (field c lam n).carrier) : LIDT.CL.chi ⋯ ((permutation c lam n) s) = selector c hc lam n s

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalGame.numbering (c lam n : ℕ) : Fin (2 ^ SourceCompiler.registerPower c lam n * SourceCompiler.fieldBits c lam n) ≃ (Fin (SourceCompiler.registerPower c lam n) → Bool) × Fin (SourceCompiler.fieldBits c lam n)

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalGame.quotient (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) : Game (CL.Detyping.Question (QuestionType QLD.Ty 7) (Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n))) (CL.Detyping.Question (QuestionType QLD.Ty 7) (Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n))) (ParsedAnswer (Fin (2 ^ SourceCompiler.registerPower c lam n * SourceCompiler.fieldBits c lam n) → ZMod 2) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (field c lam n).carrier (SourceCompiler.registerPower c lam n) 1)) (ParsedAnswer (Fin (2 ^ SourceCompiler.registerPower c lam n * SourceCompiler.fieldBits c lam n) → ZMod 2) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (field c lam n).carrier (SourceCompiler.registerPower c lam n) 1))

Equations

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

@[reducible, inline]

noncomputable abbrev MIPRE.Introspection.CanonicalGame.guarded (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) : Game (QuestionType QLD.Ty 7 × (Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n) → ZMod 2)) (QuestionType QLD.Ty 7 × (Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n) → ZMod 2)) (ParsedAnswer (Fin (SourceCompiler.registerBits c lam n) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (field c lam n).carrier (SourceCompiler.registerPower c lam n) 1)) (ParsedAnswer (Fin (SourceCompiler.registerBits c lam n) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (field c lam n).carrier (SourceCompiler.registerPower c lam n) 1))

Equations

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

theorem MIPRE.Introspection.CanonicalGame.exists_perfectPCC (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (hV : V.HasPerfectPCC (2 ^ n) ((2 ^ n) ^ lam)) : ∃ (S : SyncStrategy (guarded c hc he lam n V hs).doubled), S.IsPCC ∧ S.value = 1 ∧ (∀ (q : Bool × QuestionType QLD.Ty 7 × (Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n) → ZMod 2)) (a : ParsedAnswer (Fin (SourceCompiler.registerBits c lam n) → CL.𝔽₂) (Verifier.Answers ((2 ^ n) ^ lam)) (QLD.Answer (field c lam n).carrier (SourceCompiler.registerPower c lam n) 1)), S.P.M q a ≠ 0 → PrefixGuard.holds (AuxiliaryDecision.padded V hs) q.2.1 a) ∧ (∀ (side w : Bool) (payload : Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n) → ZMod 2) (y : Fin (SourceCompiler.registerBits c lam n) → CL.𝔽₂) (a : Verifier.Answers ((2 ^ n) ^ lam)), S.P.M (side, Sum.inr (AuxType.introspect, w), payload) (ParsedAnswer.pair y a) ≠ 0 → ∃ (x : Fin (SourceCompiler.registerBits c lam n) → CL.𝔽₂), (AuxiliaryDecision.padded V hs w).eval x = y) ∧ ∀ (side : Bool) (t : QLD.Ty) (payload : Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n) → ZMod 2) (a : QLD.Answer (field c lam n).carrier (SourceCompiler.registerPower c lam n) 1), S.P.M (side, Sum.inl t, payload) (ParsedAnswer.pauli a) ≠ 0 → (QLD.PauliCL.ExplicitSeed.binaryDecode (permutation c lam n) (basis c he lam n) t payload).fmtOk a = true

The finite honest strategy has every support certificate used by the executable prefix and source-output guards.