Preparing shared resources for the introspection decision kernel

The uniform program receives cons (encode ((S,D),λ)) raw. It generates the single unary clock, exponential source index, canonical unary Pauli parameters and binary register bounds. The raw decision input and source metadata are retained verbatim. A fixed polynomial-time kernel then consumes these resources.

@[reducible, inline]

abbrev MIPRE.Introspection.DecisionPreparation.Metadata : Type

Equations

• MIPRE.Introspection.DecisionPreparation.Metadata = ((MIPRE.Cost.Prog × MIPRE.Cost.Prog) × ℕ)

@[reducible, inline]

abbrev MIPRE.Introspection.DecisionPreparation.Resources : Type

Equations

• MIPRE.Introspection.DecisionPreparation.Resources = (MIPRE.Cost.Data × MIPRE.Cost.Data × MIPRE.Cost.Unary × ℕ × MIPRE.Introspection.PauliSamplerParameters.Parameters × ℕ × ℕ)

@[reducible, inline]

abbrev MIPRE.Introspection.DecisionPreparation.KernelInput : Type

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.inputMetadata : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.DecisionPreparation.inputMetadata = MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Introspection.DecisionPreparation.inputRaw : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.DecisionPreparation.inputRaw = MIPRE.Cost.PolyTimeFun.treeTail

noncomputable def MIPRE.Introspection.DecisionPreparation.inputLambda : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.Introspection.DecisionPreparation.inputLambda = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Introspection.DecisionPreparation.inputMetadata)

noncomputable def MIPRE.Introspection.DecisionPreparation.inputIndex : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.Introspection.DecisionPreparation.inputIndex = MIPRE.Introspection.ClockSimulation.indexReader.comp MIPRE.Introspection.DecisionPreparation.inputRaw

noncomputable def MIPRE.Introspection.DecisionPreparation.parameterInput : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.resources (c : ℕ) (z : Cost.Data) : Resources

The output format, before any kernel-specific conversion.

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.kernelInput (c : ℕ) (M : Metadata) (x : Cost.Data) : KernelInput

The same prepared layout with canonically supplied source programs typed.

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.raw : Cost.PolyTimeFun Cost.Data Cost.Data

Getters are total even on malformed output trees. Program metadata is retained as data; its canonical sampler/decider projections are named below.

Equations

• MIPRE.Introspection.DecisionPreparation.raw = MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Introspection.DecisionPreparation.rest : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.DecisionPreparation.rest = MIPRE.Cost.PolyTimeFun.treeTail

noncomputable def MIPRE.Introspection.DecisionPreparation.metadata : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.DecisionPreparation.metadata = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Introspection.DecisionPreparation.rest

noncomputable def MIPRE.Introspection.DecisionPreparation.resourceTail : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.DecisionPreparation.resourceTail = MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Introspection.DecisionPreparation.rest

noncomputable def MIPRE.Introspection.DecisionPreparation.budget : Cost.PolyTimeFun Cost.Data Cost.Unary

Equations

• MIPRE.Introspection.DecisionPreparation.budget = MIPRE.Introspection.SourceCompiler.readUnary.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Introspection.DecisionPreparation.resourceTail)

@[simp]

theorem MIPRE.Introspection.DecisionPreparation.inputLambda_canonical (S D : Cost.Prog) (lam : ℕ) (x : Cost.Data) : inputLambda.toFun ((Cost.encode ((S, D), lam)).cons x) = lam

@[simp]

theorem MIPRE.Introspection.DecisionPreparation.inputIndex_canonical (M x : Cost.Data) : inputIndex.toFun (M.cons x) = ClockSimulation.indexReader.toFun x

theorem MIPRE.Introspection.DecisionPreparation.encode_kernelInput (c : ℕ) (M : Metadata) (x : Cost.Data) : Cost.encode (kernelInput c M x) = Cost.encode (resources c ((Cost.encode M).cons x))

noncomputable def MIPRE.Introspection.DecisionPreparation.appendRoute (arg : Cost.PolyTimeFun Cost.Data Cost.Data) : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

Append a subroutine result while retaining its entire input as context.

Equations

• MIPRE.Introspection.DecisionPreparation.appendRoute arg = (MIPRE.Cost.PolyTimeFun.const true).pair (MIPRE.Cost.PolyTimeFun.treePair.ap₂ arg (MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Data))

noncomputable def MIPRE.Introspection.DecisionPreparation.appendStage (arg : Cost.PolyTimeFun Cost.Data Cost.Data) (p : Cost.Prog) : Cost.Prog

Equations

• MIPRE.Introspection.DecisionPreparation.appendStage arg p = MIPRE.Cost.Prog.routeOneCall (MIPRE.Introspection.DecisionPreparation.appendRoute arg) p MIPRE.Cost.PolyTimeFun.treePair

theorem MIPRE.Introspection.DecisionPreparation.appendStage_closed (arg : Cost.PolyTimeFun Cost.Data Cost.Data) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) : Cost.Prog.WellScoped 1 (appendStage arg p)

theorem MIPRE.Introspection.DecisionPreparation.appendStage_runs (arg : Cost.PolyTimeFun Cost.Data Cost.Data) {p : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (x r : Cost.Data) (t : ℕ) (hr : p.Runs (arg.toFun x) r t) : ∃ (time : ℕ), (appendStage arg p).Runs x (x.cons r) time

noncomputable def MIPRE.Introspection.DecisionPreparation.clockStage : Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.indexStage : Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.pauliStage (c : ℕ) : Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.boundsStage (c : ℕ) : Cost.Prog

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.origin : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.preparedClock : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.preparedIndex : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.preparedParameters : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.Introspection.DecisionPreparation.preparedParameters = MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.Introspection.DecisionPreparation.finish : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

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

def MIPRE.Introspection.DecisionPreparation.sequence (p q : Cost.Prog) : Cost.Prog

Sequence closed programs, retaining the ambient input discipline.

Equations

• MIPRE.Introspection.DecisionPreparation.sequence p q = p.let_ q

theorem MIPRE.Introspection.DecisionPreparation.sequence_closed {p q : Cost.Prog} (hp : Cost.Prog.WellScoped 1 p) (hq : Cost.Prog.WellScoped 1 q) : Cost.Prog.WellScoped 1 (sequence p q)

theorem MIPRE.Introspection.DecisionPreparation.sequence_runs {p q : Cost.Prog} (hq : Cost.Prog.WellScoped 1 q) {x y z : Cost.Data} {s t : ℕ} (hp : p.Runs x y s) (hr : q.Runs y z t) : (sequence p q).Runs x z (s + t + 1)

noncomputable def MIPRE.Introspection.DecisionPreparation.prog (c : ℕ) : Cost.Prog

The budget appears once in the program; all later stages only retain it.

Equations

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

theorem MIPRE.Introspection.DecisionPreparation.prog_closed (c : ℕ) : Cost.Prog.WellScoped 1 (prog c)

noncomputable def MIPRE.Introspection.DecisionPreparation.clockResult (z : Cost.Data) : Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.indexResult (z : Cost.Data) : Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.pauliResult (c : ℕ) (z : Cost.Data) : Cost.Data

Equations

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

noncomputable def MIPRE.Introspection.DecisionPreparation.boundsResult (c : ℕ) (z : Cost.Data) : Cost.Data

Equations

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

theorem MIPRE.Introspection.DecisionPreparation.prog_runs (c : ℕ) (z : Cost.Data) : ∃ (time : ℕ), (prog c).Runs z (Cost.encode (resources c z)) time

Exact resource preparation is total for every input tree, including zero parameters and malformed raw decision inputs.

noncomputable def MIPRE.Introspection.DecisionPreparation.kernelProg (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) : Cost.Prog

Equations

• MIPRE.Introspection.DecisionPreparation.kernelProg c kernel = MIPRE.Introspection.DecisionPreparation.sequence (MIPRE.Introspection.DecisionPreparation.prog c) kernel.code

theorem MIPRE.Introspection.DecisionPreparation.kernelProg_closed (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) : Cost.Prog.WellScoped 1 (kernelProg c kernel)

theorem MIPRE.Introspection.DecisionPreparation.kernelProg_runs (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) (M : Metadata) (x : Cost.Data) : ∃ (time : ℕ), (kernelProg c kernel).Runs ((Cost.encode M).cons x) (Cost.encode (kernel.toFun (kernelInput c M x))) time

noncomputable def MIPRE.Introspection.DecisionPreparation.compiler (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) : Cost.PolyTimeFun Metadata Cost.Prog

The compiler specializes only the binary source metadata.

Equations

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

@[simp]

theorem MIPRE.Introspection.DecisionPreparation.compiler_apply (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) (M : Metadata) : (compiler c kernel).toFun M = Cost.hardcode (kernelProg c kernel) (Cost.encode M)

theorem MIPRE.Introspection.DecisionPreparation.compiler_closed (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) (M : Metadata) : Cost.Prog.WellScoped 1 ((compiler c kernel).toFun M)

theorem MIPRE.Introspection.DecisionPreparation.compiler_runs (c : ℕ) (kernel : Cost.PolyTimeFun KernelInput Bool) (M : Metadata) (x : Cost.Data) : ∃ (time : ℕ), ((compiler c kernel).toFun M).Runs x (Cost.encode (kernel.toFun (kernelInput c M x))) time