Cook–Levin machines: multiplication of computed unary outputs

Proved

CookLevin.machine_multiply_unary_bank_outputs

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

arithmeticcook-levinpolynomial-timeturing-machines

For any alphabet of at least four symbols and two spectator work banks, a fixed well-formed Turing machine multiplies two terminated unary prefixes into the last tape within m*(2n+2)+2 steps. The source heads and blank destination head begin at zero. The inner source marker is restored even if an earlier computation overwrote it. Source contents beyond their first non-one terminators may be arbitrary. The input and spectator tapes are preserved exactly; the output is the complete standard unary encoding of mn. This supplies multiplication of computed counters for the Cook–Levin emitter; the full reduction computation theorem remains separate.

Preamble

import Definitions.Def_CookLevin_Cost
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.machine_multiply_unary_bank_outputs {a b G : Nat} (hG : 4 ≤ G) :
    ∃ R : Machine, TuringMachine (a + b + 4) G R ∧
      ∀ (m n : Nat) (input : Tape) (f g : Nat → Symbol)
        (left right : List Tape), left.length = a → right.length = b →
        (∀ j, j < m → f (1 + j) = oneSymbol) → f (1 + m) ≠ oneSymbol →
        (∀ j, j < n → g (1 + j) = oneSymbol) → g (1 + n) ≠ oneSymbol →
        Transforms R (input :: (left ++ (f, 0) :: (g, 0) :: (right ++ [(contents [], 0)])))
          (m * (2 * n + 2) + 2)
          (input :: (left ++ (f, 1 + m) ::
            ((fun i => if i = 0 then startSymbol else g i), 1) ::
            (right ++ [(contents (boolsToSymbols (List.replicate (m * n) true)),
              1 + m * n)]))) := by sorry

Source

Nested-loop multiplication with inner-marker restoration, stationary spectator padding, and verified tape permutation.

View graph