Decimal-radius scorecard, scan chunk 6/6 (panels 2750…3300) #
GENERATED by scripts/smooth_dec_scorecard_gen.py — see SmoothingDecScorecard.lean for the corpus story. Each chunk lives in its own module because (a) one whole-grid kernel evaluation retains ~15 GB of kernel-cache bignums (OOM on 16 GB CI runners) and (b) memory is NOT reclaimed between declarations within one lean process — per-module processes cap the worst chunk at ~5 GB.
Grid values 3300…2750 (descending) as NUMERATORS over the common
denominator 10¹² (every grid value is 1/2 + Σ (1/1000)·(k/10⁹)).
ℕ literals elaborate in ~1 s where flat ℚ division literals price
out in pending-mvar instance synthesis (>10 min). Untrusted input —
verified by the kernel checks below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Proofs.phiChunkLit6 = List.map (fun (n : ℚ) => n / 1000000000000) do let a ← Proofs.phiChunkNum6 pure ↑a
Instances For
Checkpoint: the grid value at panel 2750, read off the verified scan.
Chunk 6: panels 2750…3300, kernel-evaluated FROM the checkpoint.
Panels 0…3300: chunk 6 glued onto the verified prefix.