Tell, Don't Compute: Precomputed Certificates for Heavy Kernel Verification

2026-06-27

A previous post described how an algebraic overapproximation ($\binom{n}{k} \leq n^k$, then power-of-2 chains) eliminated native_decide from a Sturm coefficient bound. That technique works when you need an existence proof (“some finite bound exists”) and tightness does not matter.

But there is a second, harder problem: what do you do when the proof needs the kernel to evaluate a specific large computation — not just bound it, but get the exact answer — and the computation takes hours?

The Problem

The Sturm bound certificate for the modular polynomial $\Phi_{41}$ requires bounding the contribution of each row of a $43 \times 43$ sparse coefficient matrix. Each entry is a 500-digit integer (the coefficients of polmodular(41) from PARI/GP). The bound for row $x$ is:

$$ L_1(x) = \sum_{y=0}^{42} \lvert M_{x,y} \rvert $$

The naive proof asks the Lean 4 kernel to unfold the matrix definition, compute each $\lvert M_{x,y} \rvert$, and sum 43 terms per row, for all 43 rows. Each entry requires scanning a sparse term list of 1766 elements. Total: the kernel performs millions of reductions on 500-digit integers.

Result: more than 5 hours of CPU time on a 48-core server, and still not finished.

The Insight: Tell the Kernel the Answer

The key realization is that there are two fundamentally different things you can ask a proof kernel to do:

Compute the answer from a specification (slow: the kernel re-derives every intermediate value).
Verify a claimed answer against the specification (fast: the kernel only checks equality).

Computing $L_1(x)$ from the sparse term list takes hours. But verifying that a specific 600-digit number equals $L_1(x)$ takes seconds — the kernel just needs to confirm that both sides reduce to the same numeral.

The Method

Step 1: Precompute externally. A Python script reads the sparse term data, builds the $43 \times 43$ matrix, and computes the $L_1$ norm of each row. This takes milliseconds.

Step 2: Write the answers as Lean definitions. Each row’s $L_1$ norm becomes a concrete Nat literal:

def phi41RowL1Cert (x : Nat) : Nat :=
  match x with
  | 0 => 4158671879736192729946787966...  -- 606 digits
  | 1 => 1412634656652304383474346356...  -- 605 digits
  ...
  | 42 => 1
  | _ => 0

Step 3: Verify each literal. A single native_decide call checks that the precomputed literal matches the actual matrix computation:

theorem phi41RowL1Cert_correct (x : Nat) (hx : x ≤ 42) :
    (Finset.range 43).sum (fun y =>
      Int.natAbs (matrix.getD x ...).getD y 0)) =
    phi41RowL1Cert x := by
  interval_cases x <;> native_decide

This compiles in seconds, not hours. The native_decide tactic uses compiled native code to evaluate the equality, then the kernel checks the Boolean result. The trusted base expands slightly (the native compiler is trusted), but the computation is verified.

Step 4: Use the certificate. The main proof now references phi41RowL1Cert x — a cheap pattern-match on x returning a concrete numeral — instead of phi41SparseCoeffRowL1 x, which triggers the expensive matrix unfold. The kernel never sees the sparse term list again.

A Subtlety: Big Literals and `ring`

Even after the certificate is in place, Lean’s ring and simp tactics can blow up on goals containing 500-digit number literals. The tactic ring normalizes its input, which involves traversing the entire expression tree — including the huge numerals.

The fix is the set trick: abstract the big literals into opaque local variables before calling ring.

_ = 87 * ↑(phi41RowL1Cert x) * ↑QrowBigBound * ↑QrowPullBound := by
    set a := (phi41RowL1Cert x : Z)
    set b := (QrowBigBound : Z)
    set c := (QrowPullBound : Z)
    ring

Now ring sees 87 * a * b * c — four symbolic variables — instead of 87 * (415867...0001) * (10^2400) * (10^2400). It closes the goal instantly.

The Pattern

This “tell, don’t compute” pattern applies whenever:

A computation is decidable but too expensive for the kernel to evaluate from the specification.
The answer can be precomputed externally (by a script, a CAS, or native code).
The precomputed answer can be verified faster than it can be derived.

The verification step can use native_decide (fast, slightly larger trusted base), decide +kernel (slower, fully kernel-verified), or even norm_num (for arithmetic goals). The choice depends on how much trust you need and how large the individual verification steps are.

For the Sturm certificate: the full computation took $>5$ hours in the kernel. After restructuring into 43 precomputed row certificates, the entire file compiles in under a minute.

Current Status

The Ripple project’s modular forms sub-tree now has:

Analytical coefficient bound (SturmCRTBound.lean): 0 sorry, 0 tactic-level native_decide. Uses Vandermonde convolution majorants + power-of-2 overapproximation (previous post).
Row L1 certificates (SturmCRTBoundCert.lean): precomputed literals verified by native_decide in seconds.
Legacy paths (ModularPolynomialSturmCertificate.lean, SturmCertificateCRT.lean): still contain native_decide for the direct zero-check. These are candidates for the next round of elimination, likely via a multi-prime CRT approach with kernel-verified modular arithmetic.