Documentation

LeanMlir.Proofs.Certificates.SmoothingDecChunk1

Decimal-radius scorecard, scan chunk 1/6 (panels 0…550) #

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.

source
def Proofs.phiChunkNum1 :
List ℕ

Grid values 550…0 (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
    source
    def Proofs.phiChunkLit1 :
    List ℚ
    Equations
    Instances For
      source
      theorem Proofs.phiScanEq550 :
      phiScanRev (1 / 1000) 550 = phiChunkLit1

      Chunk 1: grid panels 0…550, kernel-evaluated.