Documentation

MIPRE.Background.Introspection.AmbientVerifierTransport

The compiled verifier and its finite detyping game #

The compiler shares its resource preparation between the graph router and the typed decision kernel. Its acceptance agrees with the generic detyping compiler at each positive index. The sampler wrapper preserves the CL presentations there.

source
def MIPRE.Introspection.DecisionCompiler.constantCutoff (B : ℕ) :
CL.Detyping.CutoffProgram

A reference cutoff can be constant because comparison is at one index.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.Introspection.DecisionCompiler.extendedSampler (c : ℕ) (hc : 1 ≤ c) (he : Even c) (lam : ℕ) :
    CL.TypedSampler 3 (QuestionType QLD.Ty 7)
    Equations
    Instances For
      source
      noncomputable def MIPRE.Introspection.DecisionCompiler.reference (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) (lam n : ℕ) :
      Verifier 5

      The generic detyping verifier with the same positive-index predicate.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.DecisionCompiler.accepts_reference (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (x y a b : Cost.BitStr) :
        (output c hc he U source lam).decider.Accepts n x y a b ↔ (reference c hc he U source lam n).decider.Accepts n x y a b

        Sharing preparation changes no positive-index acceptance decision.

        source
        theorem MIPRE.Introspection.DecisionCompiler.samplerAgreement_reference (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) :
        (output c hc he U source lam).SamplerAgreement (reference c hc he U source lam n) n
        source
        theorem MIPRE.Introspection.DecisionCompiler.val_reference (ω : ValueModel) (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (B : ℕ) :
        (output c hc he U source lam).val ω n B = (reference c hc he U source lam n).val ω n B

        The output verifier and the reference verifier have the same value at a positive index, in every value model.

        source
        theorem MIPRE.Introspection.DecisionCompiler.hasPerfectPCC_reference (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) {lam n : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (B : ℕ) :
        (output c hc he U source lam).HasPerfectPCC n B ↔ (reference c hc he U source lam n).HasPerfectPCC n B
        source
        theorem MIPRE.Introspection.DecisionCompiler.hasPerfectPCC_zero (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) (lam n B : ℕ) (hz : lam = 0 ∨ n = 0) :
        (output c hc he U source lam).HasPerfectPCC n B

        Empty questions admit the constant empty-answer PCC strategy.