Composition with an explicit polynomial bound

Open

PvsNP.composition_runtime

by alexcarter · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryformalizationp-vs-np

For any supplied polynomial-time string machines for f and g, construct a machine for g composed with f, together with the displayed uniform polynomial comparison involving a positive machine-dependent constant. This obligation includes intermediate-output growth and cannot be discharged by assuming a composition typeclass.

Status: Known mathematics / implementation obligation awaiting formal proof.

Formal statement

import Definitions.Def_PvsNPFrontier

namespace PvsNP
theorem composition_runtime (f g : Str → Str)
    (Mf : Turing.TM2ComputableInPolyTime (id : Str → Str) (id : Str → Str) f)
    (Mg : Turing.TM2ComputableInPolyTime (id : Str → Str) (id : Str → Str) g) :
    ∃ M : Turing.TM2ComputableInPolyTime (id : Str → Str) (id : Str → Str) (g ∘ f),
      ∃ C : ℕ, 0 < C ∧ ∀ n,
        M.time.eval n ≤ C * (Mf.time.eval n +
          Mg.time.eval (C * (n + Mf.time.eval n + 1)) + n + 1) := by sorry
end PvsNP

Source

Mathlib exact revision 0df444a360eaa60ab8c11dca51a86af692955474, Mathlib/Computability/TuringMachine/Computable.lean and StackTuringMachine.lean; https://github.com/leanprover-community/mathlib4/blob/0df444a360eaa60ab8c11dca51a86af692955474/Mathlib/Computability/TuringMachine/Computable.lean; requested TM2 composition infrastructure; precise displayed bound is an implementation refinement of textbook polynomial closure, not a quoted formula.

Read-back

What the Lean code literally says, in plain math · gpt-6-astra

For every two total functions $f,g:B^*\to B^*$ and every pair of supplied polynomial-time witnesses $M_f,M_g$ computing $f,g$ respectively from raw input words to raw output words, let $p_f,p_g\in\mathbb N[X]$ be their particular time polynomials. There exist a polynomial-time witness $M$ computing $g\circ f$ , with its own time polynomial $p_M$ , and a natural constant $C>0$ such that $\forall n\in\mathbb N,\ p_M(n)\le C\bigl(p_f(n)+p_g(C(n+p_f(n)+1))+n+1\bigr)$ . Each supplied witness computes its function on every word within the value of its polynomial at the input length; the displayed comparison concerns those selected bound polynomials, not necessarily minimal or actual running times, and includes $n=0$ . Here $B=\{\mathrm{false},\mathrm{true}\}$ , $B^*$ is the set of all finite Boolean lists, including the empty list, and $|w|$ is list length. A machine in these assertions is a Mathlib TM2 stack machine with finitely many stack indices, instruction labels, and control states, a finite input-stack alphabet, designated input and output stacks, a program, and initial label and control state; its other stack alphabets need not be finite. Input and output alphabet bijections transport the specified encoded lists to the corresponding stack alphabets. Computation starts with only the input stack populated, and reaches a halted configuration with the specified output on the output stack, all other stacks empty, and the control state reset to its initial value. Time counts executions of whole TM2 statements, each of which may contain several stack operations. The supplied body is admitted with sorry; no proof of this assertion is supplied there.

View graph