Soundness of the actual compiled introspection verifier

The compiled strategy is restricted through finite detyping, decoded to the canonical quotient game, and passed to the proved QLD theorem. Coordinate padding is removed and the fixed detyping factor is absorbed into the uniform error profile. The answer budget may be any budget above the enforced cutoff.

Stated in a value model (Phase 4 of planning/mipco-track.md): a raw strategy is a projective strategy of a model in which the Pauli basis test is sound (QLD.SoundIn ω M), and the output's value is that of any value model approached by such strategies (QLD.ApproxSoundIn ω) and by the projective strategies of the models it dominates (ValueModel.ProjApprox, for the padding). Both hold for val* (QLD.approxSoundIn_tensor, ValueModel.tensor_projApprox) and, when the test is sound in every commuting-operator model, for ω_co.

noncomputable def MIPRE.Introspection.CompiledSoundness.sourceCoefficient (c : ℕ) : ℝ

Equations

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

noncomputable def MIPRE.Introspection.CompiledSoundness.exponent : ℝ

Equations

• MIPRE.Introspection.CompiledSoundness.exponent = MIPRE.Introspection.RestrictedSoundness.qldExponent * MIPRE.Introspection.rootExponent (6 * 7 + 2)

noncomputable def MIPRE.Introspection.CompiledSoundness.coefficient (c : ℕ) : ℝ

Equations

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

theorem MIPRE.Introspection.CompiledSoundness.sourceCoefficient_one_le (c : ℕ) : 1 ≤ sourceCoefficient c

theorem MIPRE.Introspection.CompiledSoundness.coefficient_one_le (c : ℕ) : 1 ≤ coefficient c

theorem MIPRE.Introspection.CompiledSoundness.exponent_pos : 0 < exponent

theorem MIPRE.Introspection.CompiledSoundness.exponent_le_one : exponent ≤ 1

theorem MIPRE.Introspection.CompiledSoundness.scale_error {x ε : ℝ} (c : ℕ) (hx : 1 ≤ x) (hε : 0 ≤ ε) : errorProfile (sourceCoefficient c) exponent x (DecisionCompiler.detypingLoss * ε) ≤ errorProfile (coefficient c) exponent x ε

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

theorem MIPRE.Introspection.CompiledSoundness.source_value_ge_of_raw {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (ω : ValueModel) (hω : ω.ProjApprox) (c : ℕ) (hc : 2 ≤ c) (he : Even c) (hcb : 2 * RestrictedSoundness.qldCoefficient + 2 ≤ ↑c * RestrictedSoundness.qldExponent) (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (hn : 1 ≤ n) {M : BipartiteModel 𝒞 𝒜 ℬ} (hQ : QLD.SoundIn ω M) (S : M.ProjStrat (DecisionCompiler.rawGame c ⋯ he U (V.sampler.prog, V.decider.prog) lam n)) {ε : ℝ} (hε : 0 ≤ ε) (hS : 1 - S.value ≤ ε) : 1 - errorProfile (sourceCoefficient c) exponent (↑lam * ↑n) ε ≤ V.val ω (2 ^ n) ((2 ^ n) ^ lam)

A raw typed strategy, in a model where the Pauli basis test is sound, already gives the original verifier's source value, in every value model approached by projective strategies.

theorem MIPRE.Introspection.CompiledSoundness.output_soundness (ω : ValueModel) (hω : ω.ProjApprox) (hA : QLD.ApproxSoundIn ω) (c : ℕ) (hc : 2 ≤ c) (he : Even c) (hcb : 2 * RestrictedSoundness.qldCoefficient + 2 ≤ ↑c * RestrictedSoundness.qldExponent) (U : Cost.ClockedUniversalMachine) (V : Verifier 7) (lam n B : ℕ) (ε : ℝ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hε : 0 < ε) (hB : DecisionCompiler.outerBound c lam n ≤ B) (hv : 1 - ε < (DecisionCompiler.output c ⋯ he U (V.sampler.prog, V.decider.prog) lam).val ω n B) : 1 - delta (coefficient c) exponent lam n ε ≤ V.val ω (2 ^ n) ((2 ^ n) ^ lam)

Soundness in exactly the ambient verifier-value form used by the pipeline, in every value model approached by projective strategies of models where the Pauli basis test is sound.