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

The scorecard's radii are σ·Φ⁻¹(q₀) with Φ⁻¹ SYMBOLIC; the driver prints decimals via float Acklam. This file supplies 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 Smoothing.DecScorecard (279 images). The literal is verified in CHUNKS (phiScanRevFrom + phiScanRevFrom_append): one whole-grid evaluation retains its kernel-cache bignums across the whole evaluation (an OOM on 16 GB CI runners), and kernel memory is not reclaimed between declarations within one lean process, so each chunk is its own module (Smoothing.DecChunk1–Smoothing.DecChunk6).

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