Documentation

MIPRE.Background.Introspection.AmbientRawGame

Restricting the output verifier to its actual typed kernel #

The outer answer alphabet is first reduced to the enforced binary cutoff. Finite graph detyping then gives the same-state typed strategy with its fixed loss factor, and carries perfect PCC completeness in the other direction.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the restriction is one of projective strategies in any model, and the value identities hold in every value model.

source
@[reducible, inline]
abbrev MIPRE.Introspection.DecisionCompiler.outerBound (c lam n : ℕ) :
ℕ
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    noncomputable abbrev MIPRE.Introspection.DecisionCompiler.rawPredicate (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) (lam n : ℕ) :
    CL.Detyping.Question (QuestionType QLD.Ty 7) (Fin ((extendedSampler c hc he lam).dim n)) → CL.Detyping.Question (QuestionType QLD.Ty 7) (Fin ((extendedSampler c hc he lam).dim n)) → Verifier.Answers ((constantCutoff (outerBound c lam n)).outer n) → Verifier.Answers ((constantCutoff (outerBound c lam n)).outer n) → Bool
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[reducible, inline]
      noncomputable abbrev MIPRE.Introspection.DecisionCompiler.rawGame (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) (lam n : ℕ) :
      Game (CL.Detyping.Question (QuestionType QLD.Ty 7) (Fin ((extendedSampler c hc he lam).dim n))) (CL.Detyping.Question (QuestionType QLD.Ty 7) (Fin ((extendedSampler c hc he lam).dim n))) (Verifier.Answers ((constantCutoff (outerBound c lam n)).outer n)) (Verifier.Answers ((constantCutoff (outerBound c lam n)).outer n))
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.Introspection.DecisionCompiler.raw_accepts_iff (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) {lam n : ℕ} (V : Verifier 7) (hV : V.IsBounded lam) (q r : CL.Detyping.Question DecisionKernel.Label (Fin (PauliSampler.dimension c lam n))) (a b : Verifier.Answers (outerBound c lam n)) :
        (rawGame c hc he U (V.sampler.prog, V.decider.prog) lam n).D q r a b = true ↔ (DecisionKernel.program U).toFun (DecisionKernel.canonicalInput V lam n (SourceCompiler.registerBits c lam n) (SourceCompiler.originalBound lam n) (PauliSamplerParameters.parameters c lam n) q.1 r.1 (CL.toBits q.2) (CL.toBits r.2) ↑a ↑b) = true
        source
        theorem MIPRE.Introspection.DecisionCompiler.output_val_cutoff (ω : ValueModel) (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) {lam n B : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (hB : outerBound c lam n ≤ B) :
        (output c hc he U source lam).val ω n B = (output c hc he U source lam).val ω n (outerBound c lam n)

        Answers beyond the enforced cutoff never help, in every value model.

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

        The output verifier's value is the reference verifier's at the cutoff, in every value model.

        source
        theorem MIPRE.Introspection.DecisionCompiler.output_hasPerfectPCC_of_raw (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) {lam n B : ℕ} (hl : 1 ≤ lam) (hn : 1 ≤ n) (hB : outerBound c lam n ≤ B) (S : SyncStrategy (rawGame c hc he U source lam n).doubled) (hS : S.IsPCC) (hv : S.value = 1) :
        (output c hc he U source lam).HasPerfectPCC n B

        A perfect typed raw-kernel strategy gives completeness of the actual output.

        source
        def MIPRE.Introspection.DecisionCompiler.detypingLoss :
        ℝ
        Equations
        Instances For
          source
          theorem MIPRE.Introspection.DecisionCompiler.detypingLoss_nonneg :
          0 ≤ detypingLoss
          source
          theorem MIPRE.Introspection.DecisionCompiler.exists_raw_failure_le {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) {lam n : ℕ} {M : BipartiteModel 𝒞 𝒜 ℬ} (S : M.ProjStrat ((reference c hc he U source lam n).game n (outerBound c lam n))) {ε : ℝ} (hS : 1 - S.value ≤ ε) :
          ∃ (R : M.ProjStrat (rawGame c hc he U source lam n)), 1 - R.value ≤ detypingLoss * ε

          A strategy for the reference verifier's game restricts to a typed raw strategy, in the same model, with the detyping loss. With output_val_eq_reference, a value of the output verifier above 1 - ε in a value model approached by projective strategies gives such a raw strategy of failure at most detypingLoss * ε.