Lean Kernel Arena / perf/let-fold

The declaration to check is

let d := bits #n 0; (rfl : d + 0 = Nat.add d 0)

where bits #n 0 is a closed Nat whose evaluation makes 2^n recursive calls, and the rfl is wrapped in id so that its type is compared with d + 0 = Nat.add d 0 inside the body of the let.

The two sides differ only in how the addition is written. Unfolding HAdd.hAdd turns the left side into the right, for Θ(1). But both sides are additions of literals to a closed term, so a checker that folds closed Nat arithmetic (Nat.add on literals via GMP) will try to evaluate d first, for Θ(2^n). The official kernel only folds terms without free variables, and it checks the body of a let with d as a free variable (bound to its value in the local context), so it never evaluates bits. A checker that substitutes the value for d before checking the body makes the comparison closed and pays for the evaluation.

Found by con-leche on openai/math (SquareDifference, OAI.SquareDifference.source_ordered_contraction), where the bound value is Fintype.card TupleVertex, whose evaluation enumerates permutations and takes the checker past 6 GB; the official kernel checks that declaration in 16 ms.

N=16 in the Lean source.