feat(Computability): Step counting and complexity classes P/NP for TM1

[KrystianYCSilva]

Summary

I have a working formalization of computational complexity classes P and NP built on top of Mathlib's existing Turing.TM1 model (from PostTuringMachine.lean). The code compiles against Mathlib v4.28.0-rc1 with zero sorry, zero warnings under Mathlib lint rules.

I would like to contribute this to Mathlib, incrementally, and am opening this issue to discuss the approach before submitting PRs.

What this adds

1. Turing.TM1.step_none_iff: Basic lemma — step M c = none ↔ c.l = none (follows directly from the definition).

2. Turing.TM1.runN: Fuel-based step counter — execute a TM1 machine for at most n steps. Key lemmas: runN_stable (halted configs are fixed), runN_comp (composition: runN (a+b) = runN b ∘ runN a), runN_eq_of_halted (output stability).

3. Complexity classes:

   • haltedAt, outputAt, acceptsAt, rejectsAt — predicates on TM1 execution
   • IsPolynomial — polynomial bound on functions ℕ → ℕ
   • DecidableInTime — machine decides language within time bound
   • InP, InNP — complexity classes parameterized by acceptance predicate on tape head
   • p_sub_np — P ⊆ NP (proven, zero sorry)
   • PEqNP, PNeNP — formal propositions for the open problem

Relation to existing work

• PostTuringMachine.lean (Carneiro 2018): Defines TM0/TM1 models, Turing.eval, Turing.Reaches. No step counting or time bounds. Our work extends this.
• PR feat(Computability): Single-tape TM complexity #33132 (BoltonBailey): Defines a new FinTM0 bundled type with EvalsTo/EvalsToInTime. Complementary approach — builds new TM definitions, while ours builds on existing Turing.TM1.
• TMComputable.lean: Multi-tape TM2 complexity. Orthogonal.
• Simas (2026, arXiv:2601.15571): Polynomial-time reductions in Lean 4, but does not use Mathlib's TMs and does not define P/NP classes.

Design choices

• Fuel-based runN vs. structural EvalsTo: We use runN : Nat → Cfg → Cfg (fuel-based), which makes monotonicity proofs straightforward. PR feat(Computability): Single-tape TM complexity #33132 uses EvalsTo (a struct with steps + proof). Both are valid; ours is simpler but less informative.
• Acceptance via tape head predicate: TM1 has no accept/reject states. We parameterize by accept : Γ → Prop on the tape head at halt, following Sipser §3.1.
• Generalized alphabet: InP and InNP are parameterized over {Γ : Type*} [Inhabited Γ], not a fixed alphabet.

Proposed PR sequence

1. PR 1 (small): step_none_iff lemma in PostTuringMachine.lean
2. PR 2 (medium): runN + lemmas in a new file Mathlib/Computability/TM1Complexity.lean
3. PR 3 (large): Complexity classes + p_sub_np theorem

Questions for maintainers

1. Is building on Turing.TM1 the right base model, or should this wait for/coordinate with PR feat(Computability): Single-tape TM complexity #33132's FinTM0 approach?
2. Is runN (fuel-based) acceptable, or would a relational approach (EvalsTo-style) be preferred?
3. Should IsPolynomial live in a separate file (e.g., Mathlib/Computability/Polynomial.lean)?

The full code is available at: https://github.com/KrystianYCSilva/cli-and-ai/blob/main/prompt_os_lean/agente_matematico/AgenteMatematico/MathComplexityContrib.lean