Supplying the ambient introspection contract

The sampler, executable decision kernel, universal clock, all-index budgets, honest PCC encoding, and actual QLD soundness theorem supply Introspection 7. This is the ambient contract of blueprint lem:introspection-supply, with its polynomial-exponent runtime convention and positive-index soundness domain. The source-model statement for arbitrary levels remains a separate statement.

Phase 4 of planning/mipco-track.md: the compiler seven is defined with its constants chosen explicitly, so that its soundness clause can be read in every value model (Introspection.seven_soundIn): in every value model approached by projective strategies of models where the Pauli basis test is sound, and by the projective strategies of the models it dominates. Its soundness field is the instance at val*, where both hold (QLD.approxSoundIn_tensor, ValueModel.tensor_projApprox); at ω_co, both hold as soon as the test is sound in every commuting-operator model (seven_soundIn_commuting).

noncomputable def MIPRE.Introspection.sevenConstant : ℕ

The compiler's parameter constant: an even constant large against the QLD constants.

Equations

• MIPRE.Introspection.sevenConstant = ⋯.choose

theorem MIPRE.Introspection.sevenConstant_spec : 2 ≤ sevenConstant ∧ Even sevenConstant ∧ 2 * RestrictedSoundness.qldCoefficient + 2 ≤ ↑sevenConstant * RestrictedSoundness.qldExponent

theorem MIPRE.Introspection.one_le_sevenConstant : 1 ≤ sevenConstant

noncomputable def MIPRE.Introspection.sevenC : ℕ

The compiler's complexity constant.

Equations

• MIPRE.Introspection.sevenC = MIPRE.Introspection.sevenC._proof_2.choose

theorem MIPRE.Introspection.sevenC_spec : (∀ (source : Cost.Prog × Cost.Prog) (lam n : ℕ), (DecisionCompiler.output sevenConstant one_le_sevenConstant ⋯ Cost.selfClockedUniversal source lam).Within n (budget sevenC lam n)) ∧ (∀ (source : Cost.Prog × Cost.Prog) (lam : ℕ), (DecisionCompiler.output sevenConstant one_le_sevenConstant ⋯ Cost.selfClockedUniversal source lam).decider.size ≤ sevenC * (lam + 1) ^ sevenC) ∧ ∀ (lam n : ℕ), DecisionCompiler.cutoffAt sevenConstant lam n ≤ ansBound sevenC lam n

theorem MIPRE.Introspection.sevenOutput_soundness (ω : ValueModel) (hω : ω.ProjApprox) (hA : QLD.ApproxSoundIn ω) (V : Verifier 7) (lam n : ℕ) (ε : ℝ) (hV : V.IsBounded lam) (hn : 1 ≤ n) (hε : 0 < ε) (hv : 1 - ε < (DecisionCompiler.output sevenConstant one_le_sevenConstant ⋯ Cost.selfClockedUniversal (V.sampler.prog, V.decider.prog) lam).val ω n (ansBound sevenC lam n)) : 1 - delta (CompiledSoundness.coefficient sevenConstant) CompiledSoundness.exponent lam n ε ≤ V.val ω (2 ^ n) ((2 ^ n) ^ lam)

The soundness clause of the compiler's output in a value model: in every value model approached by projective strategies of models where the Pauli basis test is sound, and by the projective strategies of the models it dominates.

noncomputable def MIPRE.Introspection.seven : Introspection 7

The complete ambient introspection compiler for seven-level source verifiers. Its only rigidity input is the Pauli basis test; its soundness field is the tensor-product instance of sevenOutput_soundness, where the test is the proved thm:qld.

Equations

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

theorem MIPRE.Introspection.exists_seven : Nonempty (Introspection 7)

The ambient introspection compiler exists.

theorem MIPRE.Introspection.seven_soundIn (ω : ValueModel) (hω : ω.ProjApprox) (hA : QLD.ApproxSoundIn ω) : seven.SoundIn ω

Introspection is sound in every value model approached by projective strategies of models where the Pauli basis test is sound, and by the projective strategies of the models it dominates.

theorem MIPRE.Introspection.seven_soundIn_commuting (h : QLD.SoundCo) : seven.SoundIn ValueModel.commuting

Introspection is sound in the commuting-operator model, as soon as the Pauli basis test is sound in the model of every commuting-operator strategy (QLD.SoundCo, Phase 5 of planning/mipco-track.md).