Documentation

MIPRE.Background.Tailored.Intro.Inhabit

Question reduction for tailored verifiers #

TailoredIntrospection 7 inhabited (blueprint thm:tailored-qr, paper II's thm:h_level_question_reduciton, II:5712, in value form), on Route A of planning/aldous-lyons-track.md: the tailored presentation of Introspection.seven.

The input's normal form verifier is C₀ λ-bounded for a λ-bounded input (TailoredVerifier.ofTNFVT_isBounded), so the output at λ is the output tailored verifier Output.outTV at M λ, with M = 2^{C₀+1} ≥ max(C₀, 2) a power of two so that λ ↦ M λ is a polynomial-time function (Scale.mulPow2F): seven's sampler, the answer-length calculator LenIntro.lenIntro and the linear-constraints processor LpIntro.lpIntro, both at M λ. The two programs meet the specification Output.IntroSpec (LpIntro.introSpec_lenIntro_lpIntro), so soundness is Output.soundness_contract and completeness at n ≥ 1 is Output.completeness_contract; at n = 0 both programs output nothing and the trivial strategy is perfect (Scale.hasPerfectZPC_of_zero). The budgets at M λ are budgets at λ with the exponent multiplied by M (Budget.sampler_within, Scale.ansBound_scale).

source
theorem MIPRE.Tailored.TailoredVerifier.IsBounded.mono {ℓ : ℕ} {T : TailoredVerifier ℓ} {lam lam' : ℕ} (h : T.IsBounded lam) (hle : lam ≤ lam') :
T.IsBounded lam'

λ-boundedness of a tailored verifier is monotone in λ.

The constants #

source
noncomputable def MIPRE.Tailored.Intro.Inhabit.C₀ :
ℕ

The constant of ofTNFVT_isBounded for selfUniversal.

Equations
Instances For
    source
    theorem MIPRE.Tailored.Intro.Inhabit.C₀_spec {ℓ : ℕ} (V : TailoredVerifier ℓ) (lam : ℕ) (h : V.IsBounded lam) :
    (V.ofTNFVT Cost.selfUniversal).IsBounded (C₀ * lam)
    source
    noncomputable def MIPRE.Tailored.Intro.Inhabit.kM :
    ℕ

    The exponent of the scale.

    Equations
    Instances For
      source
      noncomputable def MIPRE.Tailored.Intro.Inhabit.M :
      ℕ

      The scale M = 2^{C₀+1}.

      Equations
      Instances For
        source
        theorem MIPRE.Tailored.Intro.Inhabit.C₀_le_M :
        C₀ ≤ M
        source
        theorem MIPRE.Tailored.Intro.Inhabit.two_le_M :
        2 ≤ M
        source
        theorem MIPRE.Tailored.Intro.Inhabit.one_le_M :
        1 ≤ M
        source
        noncomputable def MIPRE.Tailored.Intro.Inhabit.C₁ :
        ℕ

        The calculator's constant.

        Equations
        Instances For
          source
          noncomputable def MIPRE.Tailored.Intro.Inhabit.C₂ :
          ℕ

          The processor's time constant.

          Equations
          Instances For
            source
            noncomputable def MIPRE.Tailored.Intro.Inhabit.C₃ :
            ℕ

            The processor's size constant.

            Equations
            Instances For
              source
              noncomputable def MIPRE.Tailored.Intro.Inhabit.Cf :
              ℕ

              The complexity constant of the stage.

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

                The stage #

                source
                noncomputable def MIPRE.Tailored.Intro.Inhabit.output (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) :
                TailoredVerifier 5

                The output at λ: the output tailored verifier at M λ.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem MIPRE.Tailored.Intro.Inhabit.pow_le_pow_Cf (u k : ℕ) (hk : k ≤ Cf) :
                  (u + 1) ^ k ≤ (u + 1) ^ Cf
                  source
                  theorem MIPRE.Tailored.Intro.Inhabit.within (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam n : ℕ) :
                  (output V lam).Within n (Introspection.budget Cf lam n)
                  source
                  theorem MIPRE.Tailored.Intro.Inhabit.lp_size (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam : ℕ) :
                  (output V lam).lp.size ≤ Cf * (lam + 1) ^ Cf
                  source
                  theorem MIPRE.Tailored.Intro.Inhabit.completeness (T : TailoredVerifier 7) (lam n : ℕ) (hT : T.IsBounded lam) (hZ : T.HasPerfectZPC (2 ^ n)) :
                  (output T.progs lam).HasPerfectZPC n
                  source
                  theorem MIPRE.Tailored.Intro.Inhabit.soundness (T : TailoredVerifier 7) (lam n : ℕ) (ε : ℝ) (hT : T.IsBounded lam) (hn : 1 ≤ n) (hε : 0 < ε) (hv : 1 - ε < (output T.progs lam).valStar n) :
                  1 - Introspection.delta (Introspection.CompiledSoundness.coefficient Introspection.sevenConstant * ↑M ^ Introspection.CompiledSoundness.coefficient Introspection.sevenConstant) Introspection.CompiledSoundness.exponent lam n ε ≤ T.valStar (2 ^ n)
                  source
                  noncomputable def MIPRE.Tailored.Intro.Inhabit.tailoredIntrospection :
                  TailoredIntrospection 7

                  Question reduction for tailored verifiers (blueprint thm:tailored-qr, II:5712), at input level 7: the tailored presentation of Introspection.seven at M λ.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem MIPRE.Tailored.Intro.Inhabit.exists_tailoredIntrospection :
                    Nonempty (TailoredIntrospection 7)

                    TailoredIntrospection 7 is inhabited.