4.1. Nat is bignum🔗

Lean's Nat is arbitrary-precision. Every +, *, / runs in roughly O(k) (or O(k log k) for multiplication) where k is the bit width of the operands. A loop that "obviously" performs n additions can easily turn into O(n²) total work if the accumulator's bit width grows linearly per iteration.

Compare:

-- Repeated doubling: after iteration i the accumulator is 2^i, so
-- it has Θ(i) bits. Per-iteration `s + s` costs Θ(i). Total work:
-- Θ(n^2), not Θ(n).
def doubleN (n : Nat) : Nat := Id.run do
  let mut s : Nat := 1
  for _ in [0:n] do s := s + s
  return s

-- Same shape, fixed-width arithmetic. Per-iteration cost is constant
-- (truncates mod 2^64), and the loop is genuinely Θ(n).
def doubleU64 (n : Nat) : UInt64 := Id.run do
  let mut s : UInt64 := 1
  for _ in [0:n] do s := s + s
  return s

setup_benchmark doubleN   n => n  -- declares O(n); β comes back ≈ 1
setup_benchmark doubleU64 n => n  -- declares O(n); β comes back ≈ 0

doubleN's verdict line will report a positive log-log slope β near 1, because the actual growth is n² while you declared n. The fix is either to tighten the model (setup_benchmark doubleN n => n * n) or to switch to fixed-width arithmetic (UInt64, USize) when the benchmark's intent is to measure something other than bignum cost.

The same trap surfaces less obviously in:

factorials, products on large numbers — n! has Θ(n log n) bits, so even a "single" * near the end of the computation costs more than the entire start of the loop.
gcds on growing inputs — Euclidean steps on k-bit numbers cost O(k²) per step in the schoolbook implementation.
n.factorial-shaped helpers used as test inputs — the input size in bits, not the value of n, is what the algorithm sees.

A subtler case: a loop that sums 0 + 1 + … + (n-1) looks like it should hit the same trap, but the partial sum is Θ(log n)-bit wide for most iterations (the value reaches n²/2, but its bit width is only Θ(log n)). Total work is Θ(n log n), not Θ(n²). The bignum penalty bites when the bit width of the accumulator grows linearly per step, not just its value.

When in doubt, declare the complexity that includes the bignum cost (n * n for an O(n) loop whose accumulator grows linearly), or switch to UInt64 / USize / Float if the algorithm is supposed to be doing fixed-width work and the bignum drift is incidental.