Cook–Levin machines: unary counter multiplication from zero heads

Proved

CookLevin.machine_unary_multiply_from_zero

by Robertboy18 · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticcook-levinpolynomial-timeturing-machines

A fixed well-formed four-tape, four-symbol Turing machine multiplies two unary counters. From input, unary m, unary n, and a blank destination with all three work heads at zero, it halts within m*(2n+2)+2 steps. The destination is exactly the complete encoding of mn ones, including start marker and blank tail. Both source contents and the input tape are preserved, the outer head ends at 1+m, the inner head at 1, and the destination head at 1+m*n. Empty counters are included. This is a counter-arithmetic primitive for the Cook–Levin tableau emitter, not yet the reduction computation theorem.

Preamble

import Definitions.Def_CookLevin_Cost
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_unary_multiply_from_zero :
    ∃ M : Machine, TuringMachine 4 4 M ∧
      ∀ (m n : Nat) (input : Tape),
        Transforms M [input,
          (contents (boolsToSymbols (List.replicate m true)), 0),
          (contents (boolsToSymbols (List.replicate n true)), 0), (contents [], 0)]
          (m * (2 * n + 2) + 2)
          [input, (contents (boolsToSymbols (List.replicate m true)), 1 + m),
            (contents (boolsToSymbols (List.replicate n true)), 1),
            (contents (boolsToSymbols (List.replicate (m * n) true)), 1 + m * n)] := by sorry

Source

Direct nested-loop construction in the CookLevin Basic/Cost semantics, with head preparation composed through machine_sequence_preserves_turing_and_time.

View graph