The bounded verifier as the source of introspection

The semantic source game has exactly the verifier's distribution and decision predicate. Padding preserves perfect PCC strategies and can be removed from the soundness conclusion without any additional error.

Stated in a value model (Phase 4 of planning/mipco-track.md): removing the padding loses no value in every value model approached by the projective strategies of the models it dominates (ValueModel.ProjApprox), val* (ValueModel.tensor_projApprox) and ω_co among them.

noncomputable def MIPRE.Introspection.VerifierSource.predicate (V : Verifier 7) (n B : ℕ) : V.Questions (2 ^ n) → V.Questions (2 ^ n) → Verifier.Answers B → Verifier.Answers B → Bool

Equations

• MIPRE.Introspection.VerifierSource.predicate V n B x y a b = decide (V.decider.Accepts (2 ^ n) (MIPRE.CL.toBits x) (MIPRE.CL.toBits y) ↑a ↑b)

theorem MIPRE.Introspection.VerifierSource.sourceGame_eq (V : Verifier 7) (n B : ℕ) : Honest.sourceGame (SourcePadding.Program.sourceFamily V n) (predicate V n B) = V.game (2 ^ n) B

noncomputable def MIPRE.Introspection.VerifierSource.paddedPredicate {n Q : ℕ} (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Q) (B : ℕ) : (Fin Q → CL.𝔽₂) → (Fin Q → CL.𝔽₂) → Verifier.Answers B → Verifier.Answers B → Bool

Equations

• MIPRE.Introspection.VerifierSource.paddedPredicate V hs B x y a b = MIPRE.Introspection.AuxiliaryDecision.sourcePredicate V hs x y ↑a ↑b

theorem MIPRE.Introspection.VerifierSource.dimension_le_registerBits {c lam n : ℕ} (hc : 2 ≤ c) (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) : V.sampler.dim (2 ^ n) ≤ SourceCompiler.registerBits c lam n

Canonical registers contain the entire original question space.

theorem MIPRE.Introspection.VerifierSource.padded_hasPerfectPCC {n Q B : ℕ} (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Q) (h : V.HasPerfectPCC (2 ^ n) B) : ∃ (R : SyncStrategy (Honest.sourceGame (AuxiliaryDecision.padded V hs) (paddedPredicate V hs B)).doubled), R.IsPCC ∧ R.value = 1

The padded source retains a perfect PCC strategy.

theorem MIPRE.Introspection.VerifierSource.padded_quantumValue_le {n Q B : ℕ} (V : Verifier 7) (hs : V.sampler.dim (2 ^ n) ≤ Q) {ω : ValueModel} (hω : ω.ProjApprox) : ω.val (Honest.sourceGame (AuxiliaryDecision.padded V hs) (paddedPredicate V hs B)) ≤ V.val ω (2 ^ n) B

Removing the padded coordinates loses no source-game value, in every value model approached by the projective strategies of the models it dominates.