Completeness of the actual compiled introspection verifier

The finite honest PCC strategy supplies prefix, source-output, and Pauli-format support. Encoding those outcomes preserves perfect play in the executable typed game. Graph detyping and the zero-index wrapper finish the ambient contract.

@[reducible, inline]

abbrev MIPRE.Introspection.CanonicalComplete.Answer (c lam n : ℕ) : Type

Equations

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

noncomputable def MIPRE.Introspection.CanonicalComplete.encodeAnswer (c : ℕ) (hc : 2 ≤ c) (lam n : ℕ) (a : Answer c lam n) : Verifier.Answers (DecisionCompiler.outerBound c lam n)

Equations

• MIPRE.Introspection.CanonicalComplete.encodeAnswer c hc lam n a = ⟨MIPRE.Introspection.DecisionKernel.Answer.bits (MIPRE.Introspection.CanonicalGame.field c lam n) a, ⋯⟩

theorem MIPRE.Introspection.CanonicalComplete.sourceOutput_of_support (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (S : SyncStrategy (CanonicalGame.guarded c hc he lam n V hs).doubled) (hi : ∀ (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) (q : Bool × CL.Detyping.Question DecisionKernel.Label (Fin (PauliSampler.dimension c lam n))) (a : Answer c lam n) (ha : S.P.M q a ≠ 0) : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) q.2.1 (DecisionKernel.Answer.toRaw (CanonicalGame.field c lam n) a)

theorem MIPRE.Introspection.CanonicalComplete.pauliFormatted_of_support (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam n : ℕ) (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (S : SyncStrategy (CanonicalGame.guarded c hc he lam n V hs).doubled) (hp : ∀ (side : Bool) (t : QLD.Ty) (payload : Fin ((3 * SourceCompiler.registerPower c lam n + 3) * SourceCompiler.fieldBits c lam n) → ZMod 2) (a : QLD.Answer (CanonicalGame.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 (CanonicalGame.permutation c lam n) (CanonicalGame.basis c he lam n) t payload).fmtOk a = true) (q : Bool × CL.Detyping.Question DecisionKernel.Label (Fin (PauliSampler.dimension c lam n))) (a : Answer c lam n) (ha : S.P.M q a ≠ 0) : DecisionKernel.Answer.PauliFormatted (SourceCompiler.fieldBits c lam n) ⋯ ⋯ (PauliSamplerParameters.selectorBits c lam n) (SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) q.2.1 (CL.toBits q.2.2) a

theorem MIPRE.Introspection.CanonicalComplete.encoded_accepts (c : ℕ) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hs : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n) (q r : CL.Detyping.Question DecisionKernel.Label (Fin (PauliSampler.dimension c lam n))) (a b : Answer c lam n) (ha : DecisionKernel.Answer.PauliFormatted (SourceCompiler.fieldBits c lam n) ⋯ ⋯ (PauliSamplerParameters.selectorBits c lam n) (SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) q.1 (CL.toBits q.2) a) (hb : DecisionKernel.Answer.PauliFormatted (SourceCompiler.fieldBits c lam n) ⋯ ⋯ (PauliSamplerParameters.selectorBits c lam n) (SourceCompiler.registerBits c lam n) ((2 ^ n) ^ lam) r.1 (CL.toBits r.2) b) (hga : PrefixGuard.holds (AuxiliaryDecision.padded V hs) q.1 a) (hgb : PrefixGuard.holds (AuxiliaryDecision.padded V hs) r.1 b) (hsa : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) q.1 (DecisionKernel.Answer.toRaw (CanonicalGame.field c lam n) a)) (hsb : AuxiliaryDecision.sourceOutput (V.sampler.dim (2 ^ n)) r.1 (DecisionKernel.Answer.toRaw (CanonicalGame.field c lam n) b)) (h : (CanonicalGame.quotient c ⋯ he lam n V hs).D q r a b = true) : (DecisionCompiler.rawGame c ⋯ he U (V.sampler.prog, V.decider.prog) lam n).D q r (encodeAnswer c hc lam n a) (encodeAnswer c hc lam n b) = true

theorem MIPRE.Introspection.CanonicalComplete.exists_raw_perfectPCC (c : ℕ) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hv : V.HasPerfectPCC (2 ^ n) ((2 ^ n) ^ lam)) : ∃ (R : SyncStrategy (DecisionCompiler.rawGame c ⋯ he U (V.sampler.prog, V.decider.prog) lam n).doubled), R.IsPCC ∧ R.value = 1

The actual typed binary kernel has a perfect PCC strategy whenever the source verifier does, using the finite honest strategy's support certificates.

theorem MIPRE.Introspection.CanonicalComplete.output_hasPerfectPCC (c : ℕ) (hc : 2 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (C : ℕ) (hcut : ∀ (lam n : ℕ), DecisionCompiler.cutoffAt c lam n ≤ ansBound C lam n) (V : Verifier 7) (lam n : ℕ) (hV : V.IsBounded lam) (hv : V.HasPerfectPCC (2 ^ n) ((2 ^ n) ^ lam)) : (DecisionCompiler.output c ⋯ he U (V.sampler.prog, V.decider.prog) lam).HasPerfectPCC n (ansBound C lam n)

Completeness for every source index, including the zero-index wrapper.