The compiled five-level verifier and its complete resource contract

theorem MIPRE.Introspection.DecisionCompiler.graphDim_label : CL.Detyping.graphDim DecisionKernel.Label = 4 * (Fintype.card QLD.Ty + 2 * 7 + 6)

noncomputable def MIPRE.Introspection.DecisionCompiler.output (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) (lam : ℕ) : Verifier 5

Equations

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

@[simp]

theorem MIPRE.Introspection.DecisionCompiler.output_sampler (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) (lam : ℕ) : (output c hc he U source lam).sampler = PauliSampler.finalSampler c hc he 7 lam

@[simp]

theorem MIPRE.Introspection.DecisionCompiler.output_decider (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) (source : Cost.Prog × Cost.Prog) (lam : ℕ) : (output c hc he U source lam).decider.prog = (compute c U).toFun (source, lam)

theorem MIPRE.Introspection.DecisionCompiler.resources_with_cutoff (c : ℕ) (hc : 1 ≤ c) (he : Even c) (U : Cost.ClockedUniversalMachine) : ∃ (C : ℕ), (∀ (source : Cost.Prog × Cost.Prog) (lam n : ℕ), (output c hc he U source lam).Within n (budget C lam n)) ∧ (∀ (source : Cost.Prog × Cost.Prog) (lam : ℕ), (output c hc he U source lam).decider.size ≤ C * (lam + 1) ^ C) ∧ ∀ (lam n : ℕ), cutoffAt c lam n ≤ ansBound C lam n

All compiler inputs and all indices satisfy the pipeline's exact Within contract, with the same fixed exponent also bounding output descriptions.