Certified decimal quantile bounds — Φ⁻¹ leaves symbolic-land #

The scorecard's radii are σ·Φ⁻¹(q₀) with Φ⁻¹ SYMBOLIC; the driver prints decimals via float Acklam. This file closes that gap with certified rational LOWER bounds on Φ⁻¹:

• stdNormalCDF_panel — one upper-Riemann panel Φ(b) ≤ Φ(a) + (b−a)·φ(a) on [0,∞) (the density is antitone there), by bounding the Gaussian measure of Ioc a b through gaussianReal_apply + setLIntegral — no FTC, no improper integrals;
• ratExpLB/ratPdfUB/ratCeil9 — a KERNEL-COMPUTABLE rational upper bound for the density: 32-term Taylor lower bound for exp (Real.sum_le_exp_of_nonneg), √(2π) ≥ 2.5066282 (Real.pi_gt_d20), each panel value ceiling-rounded to 10⁻⁹ so the grid fold's denominators stay bounded (the exact values' lcm explodes);
• phiGridUB + stdNormalCDF_le_phiGridUB — the cumulative grid fold: Φ(m·h) ≤ phiGridUB h m, a computable ℚ;
• le_stdNormalQuantile_of_grid — the workhorse: ONE decide +kernel rational check phiGridUB h m ≤ q₀ certifies m·h ≤ Φ⁻¹(q₀).

For the whole corpus, the §prefix-scan section makes per-image checks cheap: phiScanRev computes ALL grid values in one kernel pass (the head's two uses stay shared through the kernel's whnf cache), phiScanRev_getD indexes it, and le_stdNormalQuantile_of_scan/smooth_radius_dec turn one O(index) lookup against the one-shot literal into a certified decimal radius — see the generated SmoothingDecScorecard.lean (279 images). The literal is verified in CHUNKS (phiScanRevFrom + phiScanRevFrom_append): one whole-grid evaluation peaks at 15 GB of retained kernel-cache bignums (an OOM on 16 GB CI runners); per-declaration chunks are freed in between.

All results are propext / Classical.choice / Quot.sound-clean.