Acceptance and global answer bounds for the detyping compiler

theorem MIPRE.CL.Detyping.DeciderProgram.decisionStage_accepts_direct {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) (c r : Cost.Data) (h : (route E).toFun c = (false, r)) : (∃ (time : ℕ), (decisionStage E D).Runs c (Cost.encode true) time) ↔ r = Cost.encode true

theorem MIPRE.CL.Detyping.DeciderProgram.decisionStage_accepts_indirect {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) (c arg ctx : Cost.Data) (h : (route E).toFun c = (true, arg.cons ctx)) (hD : Cost.Halts D.prog arg) : (∃ (time : ℕ), (decisionStage E D).Runs c (Cost.encode true) time) ↔ ∃ (time : ℕ), D.prog.Runs arg (Cost.encode true) time

theorem MIPRE.CL.Detyping.DeciderProgram.prog_accepts_iff_stage {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hD : D.Total) (input : Cost.Data) : (∃ (time : ℕ), (prog E S D C).Runs input (Cost.encode true) time) ↔ ∃ (time : ℕ), (decisionStage E D).Runs (context input (S.dim (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) (C.inner (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) (C.outer (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input)))) (Cost.encode true) time

A raw-input acceptance law: the executable preliminary stages merely supply their verified dimension and cutoffs to the final router.

theorem MIPRE.CL.Detyping.DeciderProgram.decisionStage_accepts_iff {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (D : TypedDecider T) (hD : D.Total) (c : Cost.Data) : (∃ (time : ℕ), (decisionStage E D).Runs c (Cost.encode true) time) ↔ match routeResult E c with | (false, r) => r = Cost.encode true | (true, payload) => ∃ (time : ℕ), D.prog.Runs (Cost.PolyTimeFun.treeHead.toFun payload) (Cost.encode true) time

The decision-stage acceptance law on arbitrary trees. A routed call accepts precisely when the supplied typed program returns canonical Boolean true.

theorem MIPRE.CL.Detyping.DeciderProgram.raw_accepts_iff {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hD : D.Total) (input : Cost.Data) : (∃ (time : ℕ), (prog E S D C).Runs input (Cost.encode true) time) ↔ match routeResult E (context input (S.dim (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) (C.inner (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input))) (C.outer (Program.readNat.toFun (Cost.PolyTimeFun.treeHead.toFun input)))) with | (false, r) => r = Cost.encode true | (true, payload) => ∃ (time : ℕ), D.prog.Runs (Cost.PolyTimeFun.treeHead.toFun payload) (Cost.encode true) time

Fully explicit raw-input acceptance after the two executable index queries. The routing function includes canonical format, dimension and cutoff checks.

theorem MIPRE.CL.Detyping.DeciderProgram.accepts_iff {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hD : D.Total) (n : ℕ) (x y a b : Cost.BitStr) : (decider E S D C).Accepts n x y a b ↔ List.length x = graphDim T + S.dim n ∧ List.length y = graphDim T + S.dim n ∧ List.length a ≤ C.outer n ∧ List.length b ≤ C.outer n ∧ match selectedEdge E (graphOfBits x) (graphOfBits y) with | none => True | some uv => List.length a ≤ C.inner n ∧ List.length b ≤ C.inner n ∧ D.Accepts n uv.1 (List.drop (graphDim T) x) uv.2 (List.drop (graphDim T) y) a b

Exact typed-input acceptance. Nonedges accept within the global cutoff; genuine edges retain the source's inner cutoff and the unchanged answers.

noncomputable def MIPRE.CL.Detyping.DeciderProgram.verifier {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) : Verifier (ℓ + 2)

The executable sampler and decider form a normal-form ambient verifier.

Equations

• MIPRE.CL.Detyping.DeciderProgram.verifier E S D C hℓ hD = { sampler := MIPRE.CL.Detyping.sampler E S hℓ, decider := MIPRE.CL.Detyping.DeciderProgram.decider E S D C, accepts_length := ⋯ }

theorem MIPRE.CL.Detyping.DeciderProgram.verifier_rejectsLong {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (S : TypedSampler ℓ T) (D : TypedDecider T) (C : CutoffProgram) (hℓ : 0 < ℓ) (hD : D.Total) (n : ℕ) : (verifier E S D C hℓ hD).RejectsLong n (C.outer n)

The outer answer cut is enforced globally, including malformed graph views.