Karatsuba–Ofman: multiplication in time on a multitape Turing machine
ProvedIntMul.TM.karatsubaKaratsuba–Ofman multiplication. There is a single deterministic multitape Turing machine that, for every and all , halts on input with output , and whose worst-case running time on -bit inputs is
The algorithm splits each operand into two halves and replaces four half-size products by three, giving the recurrence .
Formalization Note The machine model is the shared IntMul_MultitapeModel (Montanaro's -tape conventions: read-only input tape, output tape, only in cell , , frozen halting state). means a bound for all , with and depending only on the machine; sizes need only correctness.
import Mathlib import Definitions.Def_IntMul_MultitapeModel
namespace IntMul.TM theorem karatsuba : MulTimeBound fun n => (n : ℝ) ^ Real.logb 2 3 := by sorry end IntMul.TM
Read-back
What the Lean code literally says, in plain math · claude-opus-5-5
Theorem IntMul.TM.karatsuba. Let
where the exponent is the real number and the power is the real power function (for the base is positive, so this is the ordinary value ). The theorem asserts that there exists a deterministic multitape Turing machine such that:
- (Correctness for every .) For every and all bit strings (leading zeros allowed), started on input halts after finitely many steps with output (no time bound required in this clause).
- (Time bound.) There exist a real constant and a threshold (both chosen after , independent of ) such that for every with and and all , on input reaches the halting state with that output within some steps.
Definitions unfolded. reads as binary with the first (leftmost) bit most significant; . is the length- list whose -th entry () is bit number of , i.e. written MSB-first, left-padded with zeros to exactly bits; since this is the exact product. "Started on input " means: state , tape holds (bits as symbols ), every other tape , all heads at cell . "Halts with output at step " means: after exactly steps the state is and the whole output tape (tape ) is — no other non-blank cells; work tapes and head positions are unconstrained. Since freezes the configuration, "some " is the same as halting within steps. The machine model: finite alphabet containing pairwise distinct (plus any extra symbols), finite state set with , one-way-infinite tapes (tape input, read-only; tape output; the rest work tapes; fixed by ), only in cell and never moved left from, one step = simultaneous write/move on all tapes.
Edge cases. (input "") is not constrained at all. Inputs with , or not of the form , are not constrained. for all , so no degenerate values arise. Small are covered only by the untimed correctness clause. The statement concerns a single machine for all (uniform), with only a big- (eventual, constant-factor) bound — no explicit constant.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.