The executable detyping decision router

This is an explicit ambient adaptation of types.tex's detyped decider. Canonical field encodings and question dimensions are checked first. An outer answer cutoff is enforced globally, as required by the ambient verifier budget. Within that cutoff nonedge views accept, and edge views use the source typed answer cutoff before invoking the typed decider. No uniform graph compilation or absolute source-model timeout bound is claimed here.

Thus malformed graph patterns in binary questions accept within the outer cutoff, while noncanonical raw data encodings reject. The latter convention has no effect on the finite games, whose fields are binary strings.

noncomputable def MIPRE.CL.Detyping.DeciderProgram.selectedEdge {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (x y : Graph.Coord T → 𝔽₂) : Option (T × T)

Recognize a genuine ordered edge from the complete graph-view patterns.

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.edgeData {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (x y : Graph.Coord T → 𝔽₂) : Cost.Data

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.edgeAction {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] : Cost.PolyTimeFun ((Fin (graphDim T) → 𝔽₂) × (Fin (graphDim T) → 𝔽₂)) Cost.Data

The finite graph recognition table is an actual ambient program.

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.lengthNat : Cost.PolyTimeFun Cost.BitStr ℕ

Equations

• MIPRE.CL.Detyping.DeciderProgram.lengthNat = MIPRE.Cost.PolyTimeFun.addUnary.ap₂ (MIPRE.Cost.PolyTimeFun.const 0) MIPRE.Cost.PolyTimeFun.length

@[simp]

theorem MIPRE.CL.Detyping.DeciderProgram.lengthNat_apply (x : Cost.BitStr) : lengthNat.toFun x = List.length x

def MIPRE.CL.Detyping.DeciderProgram.context (input : Cost.Data) (s inner outer : ℕ) : Cost.Data

A raw input context after the dimension and cutoff routines have returned.

Equations

• MIPRE.CL.Detyping.DeciderProgram.context input s inner outer = (input.cons (MIPRE.Cost.encode s)).cons (MIPRE.Cost.encode (inner, outer))

noncomputable def MIPRE.CL.Detyping.DeciderProgram.inputReader : Cost.PolyTimeFun Cost.Data Cost.Data

Equations

• MIPRE.CL.Detyping.DeciderProgram.inputReader = MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeHead

noncomputable def MIPRE.CL.Detyping.DeciderProgram.indexReader : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.CL.Detyping.DeciderProgram.indexReader = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.CL.Detyping.DeciderProgram.inputReader)

noncomputable def MIPRE.CL.Detyping.DeciderProgram.xReader : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.yReader : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.aReader : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.bReader : Cost.PolyTimeFun Cost.Data Cost.BitStr

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.dimensionReader : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.CL.Detyping.DeciderProgram.dimensionReader = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeHead)

noncomputable def MIPRE.CL.Detyping.DeciderProgram.innerReader : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.CL.Detyping.DeciderProgram.innerReader = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.Cost.PolyTimeFun.treeTail)

noncomputable def MIPRE.CL.Detyping.DeciderProgram.outerReader : Cost.PolyTimeFun Cost.Data ℕ

Equations

• MIPRE.CL.Detyping.DeciderProgram.outerReader = MIPRE.CL.Detyping.Program.readNat.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.Cost.PolyTimeFun.treeTail)

def MIPRE.CL.Detyping.DeciderProgram.typedArgument (n : ℕ) (u v : Cost.Data) (x y a b : Cost.BitStr) : Cost.Data

The typed decider is called using the seven-field input convention from the source.

Equations

• MIPRE.CL.Detyping.DeciderProgram.typedArgument n u v x y a b = (MIPRE.Cost.encode n).cons (u.cons ((MIPRE.Cost.encode x).cons (v.cons (MIPRE.Cost.encode (y, a, b)))))

noncomputable def MIPRE.CL.Detyping.DeciderProgram.routeResult {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (c : Cost.Data) : Bool × Cost.Data

The precise routing rule, including every malformed-input branch.

Equations

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

noncomputable def MIPRE.CL.Detyping.DeciderProgram.route {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] : Cost.PolyTimeFun Cost.Data (Bool × Cost.Data)

All routing and format checks are concrete polynomial-time ambient computations.

Equations

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

theorem MIPRE.CL.Detyping.DeciderProgram.route_apply {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (c : Cost.Data) : (route E).toFun c = routeResult E c

theorem MIPRE.CL.Detyping.DeciderProgram.route_context {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (n s inner outer : ℕ) (x y a b : Cost.BitStr) : (route E).toFun (context (Cost.encode (n, x, y, a, b)) s inner outer) = if List.length x = graphDim T + s ∧ List.length y = graphDim T + s ∧ List.length a ≤ outer ∧ List.length b ≤ outer then match selectedEdge E (graphOfBits x) (graphOfBits y) with | none => (false, Cost.encode true) | some uv => if List.length a ≤ inner ∧ List.length b ≤ inner then (true, (Cost.encode (n, uv.1, List.drop (graphDim T) x, uv.2, List.drop (graphDim T) y, a, b)).cons Cost.Data.nil) else (false, Cost.encode false) else (false, Cost.encode false)

theorem MIPRE.CL.Detyping.DeciderProgram.route_preserves {T : Type u_1} [Fintype T] [DecidableEq T] [Cost.SizedEncoding T] (E : T → T → Prop) [DecidableRel E] (c payload : Cost.Data) (h : (route E).toFun c = (true, payload)) : ∃ (d : Cost.Data) (ctx : Cost.Data), payload = ((Cost.encode (indexReader.toFun c)).cons d).cons ctx

Successful routing preserves the normalized original index on all raw input trees.

noncomputable def MIPRE.CL.Detyping.DeciderProgram.post : Cost.PolyTimeFun (Cost.Data × Cost.Data) Cost.Data

An arbitrary typed output is accepted exactly when it is the canonical Boolean true.

Equations

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

theorem MIPRE.CL.Detyping.DeciderProgram.post_apply (ctx out : Cost.Data) : post.toFun (ctx, out) = Cost.encode (decide (out = Cost.encode true))