The efficient computability toolkit

The efficient versions of the universal machine, the s-m-n theorem, and Kleene's recursion theorem, in the ambient cost model — blueprint Section sec:rr-computability (lem:universal-tm, lem:smn, lem:kleene), following [MNY, Lemmas 2.1–2.3]. Mathlib has the computability halves for Nat.Partrec.Code (Nat.Partrec.Code.smn, eval_part, fixed_point); everything with a time bound is new.

Contents:

• hardcode: the efficient s-m-n. hardcode p d = let_ (cons (const d) (var 0)) p binds the pair (d, input) as the input of p. The witness makes [MNY, Lemma 2.2] quantitative and stronger than stated there: the time overhead is additive and linear in the sizes of d and of the input, and the description grows by exactly d.size + 35 nodes (paper: polynomial). smn_polyTime is the runtime version — the map is itself polynomial-time computable in the model (smnProg, linear time) — generic in the type of the hardcoded value.
• UniversalMachine / exists_efficient_universal (lem:universal-tm): a fixed closed program univ that, on the pair (encode c, v), halts exactly when c halts on v, with the same result and polynomial time overhead — packaged as data (the program and its overhead polynomial); its existence is proved in Cost/Universal.lean by a self-interpreter.
• ClockedUniversalMachine / exists_clocked_universal: the time-bounded variant ("run c on v for k steps"), used by the recursive compression argument and by the pipeline's deciders (introspection and repetition simulate other deciders under a budget).
• efficient_fixed_point (lem:kleene, in Cost/Kleene.lean): Kleene's recursion theorem for a polynomial-time map on programs, with the runs of the fixed point bounded by those of its image at polynomial overhead — proved from the universal machine and hardcode.

The statement shapes were audited against the proof of the recursive compression lemma (planning/compression-track.md, K0): the universal machines are structures so that downstream definitions can name the program and its polynomial without any sorried def; the runtime s-m-n is generic in the hardcoded type; Kleene is stated in the one direction the argument uses (see its docstring).

Effort notes (matching the blueprint's \effortHard on this section): the s-m-n lemmas are elementary. The two universal-machine theorems are the hard core — a self-interpreter of Prog written in Prog with polynomial overhead (Cost/Interpreter.lean, Cost/MachineBound.lean, Cost/Universal.lean); this is the same kind of artifact as the interpreter underlying the succinct Cook–Levin gateway (thm:succinct-sat), and the two developments should share design.

The efficient s-m-n (blueprint lem:smn; [MNY, Lemma 2.2])

def MIPRE.Cost.hardcode (p : Prog) (d : Data) : Prog

The s-m-n transformation: hardcode p d runs p on the pair (d, input).

Equations

• MIPRE.Cost.hardcode p d = ((MIPRE.Cost.Prog.const d).cons (MIPRE.Cost.Prog.var 0)).let_ p

theorem MIPRE.Cost.hardcode_wellScoped {p : Prog} (hp : Prog.WellScoped 1 p) (d : Data) : Prog.WellScoped 1 (hardcode p d)

theorem MIPRE.Cost.hardcode_prefix_eval (d x : Data) : Eval [x] ((Prog.const d).cons (Prog.var 0)) (d.cons x) (d.size + (x.size + 1) + 1)

The run of the pairing prefix of hardcode.

theorem MIPRE.Cost.hardcode_time {p : Prog} (hp : Prog.WellScoped 1 p) {d x r : Data} {t : ℕ} (h : p.Runs (d.cons x) r t) : (hardcode p d).Runs x r (t + d.size + x.size + 3)

Efficient s-m-n, functional equation and forward time transfer: a run of p on cons d x yields a run of hardcode p d on x with additive, linear overhead.

theorem MIPRE.Cost.hardcode_time_rev {p : Prog} (hp : Prog.WellScoped 1 p) {d x r : Data} {t : ℕ} (h : (hardcode p d).Runs x r t) : ∃ t' ≤ t, p.Runs (d.cons x) r t'

Efficient s-m-n, backward time transfer: runs of hardcode p d restrict to runs of p.

theorem MIPRE.Cost.toData_hardcode (p : Prog) (d : Data) : (hardcode p d).toData = (Data.ofNat 4).cons (((Data.ofNat 2).cons (((Data.ofNat 6).cons d).cons (Data.nil.cons Data.nil))).cons p.toData)

The description of a hardcoded program, spelled out.

theorem MIPRE.Cost.hardcode_size (p : Prog) (d : Data) : esize (hardcode p d) = esize p + d.size + 35

Efficient s-m-n, size: hardcoding adds exactly d.size + 35 nodes to the description.

def MIPRE.Cost.smnProg : Prog

The program computing the s-m-n map on descriptions: from (toData p, encode a) it assembles toData (hardcode p (encode a)) — a fixed-shape tree around the two inputs.

Equations

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

theorem MIPRE.Cost.smnProg_wellScoped : Prog.WellScoped 1 smnProg

theorem MIPRE.Cost.smnProg_runs (x d : Data) : smnProg.Runs (x.cons d) ((Data.ofNat 4).cons (((Data.ofNat 2).cons (((Data.ofNat 6).cons d).cons (Data.nil.cons Data.nil))).cons x)) (x.size + d.size + 38)

noncomputable def MIPRE.Cost.PolyTimeFun.smn (α : Type u_1) [SizedEncoding α] : PolyTimeFun (Prog × α) Prog

The s-m-n map as a polynomial-time function: (p, a) ↦ hardcode p (encode a), computed by smnProg in linear time.

Equations

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

@[simp]

theorem MIPRE.Cost.PolyTimeFun.smn_apply (α : Type u_1) [SizedEncoding α] (p : Prog) (a : α) : (smn α).toFun (p, a) = hardcode p (encode a)

theorem MIPRE.Cost.smn_polyTime (α : Type u_1) [SizedEncoding α] : ∃ (S : PolyTimeFun (Prog × α) Prog), ∀ (p : Prog) (a : α), S.toFun (p, a) = hardcode p (encode a)

The s-m-n map itself is polynomial-time computable in the model — the clause of [MNY, Lemma 2.2] that the recursive compression argument uses at runtime (the self-referential decider builds hardcoded programs while executing). The argument hardcodes encoded programs and tuples, not only bit strings, hence the statement is generic in the hardcoded type α.

The efficient universal machine (blueprint lem:universal-tm; [MNY, Lemma 2.1])

The two universal machines are structures: the program and its overhead polynomial are fields, so that downstream definitions (deciders simulating other deciders under a budget; the λ-bookkeeping of [JNVWY, §12.2], which chooses λ above the concrete overhead polynomials) can refer to them as data. Their existence is proved in Cost/Universal.lean (selfUniversal, selfClockedUniversal).

structure MIPRE.Cost.UniversalMachine : Type

Efficient universal machine. A fixed closed program univ simulating any c on any v — with the same halting behavior and result — at polynomial time overhead in esize c + v.size + runtime. Its input is the pair (encode c, v).

• univ : Prog

  The universal program.

• closed : Prog.WellScoped 1 self.univ

  It is closed.

• bound : Polynomial ℕ

  The overhead polynomial.

• time_le (c : Prog) (v r : Data) (t : ℕ) : c.Runs v r t → ∃ t' ≤ Polynomial.eval (esize c + v.size + t) self.bound, self.univ.Runs ((encode c).cons v) r t'

  A run of c yields a run of the simulation, with the same result, at polynomial overhead.

• halts_of (c : Prog) (v r : Data) (t' : ℕ) : self.univ.Runs ((encode c).cons v) r t' → ∃ (t : ℕ), c.Runs v r t

  The simulation halts only if the simulated program does, with the same result.

exists_efficient_universal : Nonempty UniversalMachine (blueprint lem:universal-tm) is proved in Cost/Universal.lean by the self-interpreter.

noncomputable def MIPRE.Cost.evalWithin (c : Prog) (v : Data) (k : ℕ) : Option Data

The result of running c on v for at most k cost, if it halts within the budget (well-defined by Eval.deterministic).

Equations

• MIPRE.Cost.evalWithin c v k = if h : ∃ (r : MIPRE.Cost.Data), ∃ t ≤ k, c.Runs v r t then some h.choose else none

theorem MIPRE.Cost.evalWithin_isSome_iff (c : Prog) (v : Data) (k : ℕ) : (evalWithin c v k).isSome = true ↔ ∃ (r : Data), ∃ t ≤ k, c.Runs v r t

noncomputable def MIPRE.Cost.clockedResult (c : Prog) (v : Data) (k : ℕ) : Data

The value a clocked simulation returns: cons (cons nil nil) r ("halted, with result r") on in-budget halting, and nil ("timeout") on budget exhaustion.

Equations

• MIPRE.Cost.clockedResult c v k = match MIPRE.Cost.evalWithin c v k with | some r => (MIPRE.Cost.Data.nil.cons MIPRE.Cost.Data.nil).cons r | none => MIPRE.Cost.Data.nil

structure MIPRE.Cost.ClockedUniversalMachine : Type

Clocked universal machine: total simulation under a step budget k (supplied in unary), returning clockedResult c v k in time polynomial in the budget, the program size and the input size. Its input is (ofNat k, (encode c, v)). This is the primitive with which deciders of the pipeline run other deciders, and with which the recursive compression argument runs "e for log n steps".

• univT : Prog

  The clocked universal program.

• closed : Prog.WellScoped 1 self.univT

  It is closed.

• bound : Polynomial ℕ

  The overhead polynomial.

• run (c : Prog) (v : Data) (k : ℕ) : ∃ t ≤ Polynomial.eval (k + esize c + v.size) self.bound, self.univT.Runs ((Data.ofNat k).cons ((encode c).cons v)) (clockedResult c v k) t

  Total, budget-bounded simulation.

exists_clocked_universal : Nonempty ClockedUniversalMachine (blueprint lem:universal-tm) is proved in Cost/Universal.lean by the clocked self-interpreter.

Efficient Kleene recursion

efficient_fixed_point (blueprint lem:kleene; [MNY, Lemma 2.3]) is proved in Cost/Kleene.lean from hardcode, smnProg and a UniversalMachine.