Documentation

Inverse standard-normal CDF Φ⁻¹ (probit), Peter Acklam's rational approximation (relative error < 1.15e-9 over the whole of (0,1), both tail branches included). The top p_A here (up to α^(1/n)) fall in the upper-tail branch, and the bound still holds there, so this is orders of magnitude tighter than the Monte-Carlo sampling error.

log Γ(x) for x ≥ 0.5 (the only regime we hit: a=k≥1, b=n−k+1≥1), Lanczos g=7.

Lentz continued fraction for the incomplete beta (Numerical Recipes betacf).

Regularized incomplete beta Iₓ(a,b) (Numerical Recipes betai); increasing in x.

Clopper–Pearson exact lower confidence bound for a Binomial proportion: the largest p with P[Bin(n,p) ≥ k] ≤ α, i.e. the α-quantile of Beta(k, n−k+1) — the p solving I_p(k, n−k+1) = α, found by 60-step bisection (Iₓ is monotone), returning the midpoint of the final bracket. This is the 1−α lower bound on p_A that the certified radius σ·Φ⁻¹(p_A) rests on (Cohen 2019 uses the same CP bound), evaluated in Float without a proof or a conservative rounding direction. k=0 ⇒ 0.

Randomized-smoothing certificate (Cohen–Rosenfeld–Kolter 2019) — a depth-independent certificate, for nets where the Lipschitz product is too loose to certify anything. The smoothed classifier ĝ(x) = argmax_c P[f(x+η)=c], η ~ N(0,σ²I), is certified robust at L2 radius σ·Φ⁻¹(p_A) where p_A is a lower bound on the top class's noise probability. It's forward-only: no new kernel, no input-VJP — just sample n noisy copies, run the existing proof-rendered <slug>_fwd, count argmax votes, Clopper–Pearson lower-bound p_A. The base classifier is trained with matched Gaussian augmentation (every batch corrupted with N(0,σ²I) host-side before the proof-rendered SGD step — the forward/backward graph is untouched), the Cohen recipe. Architecture-agnostic + depth-independent, so it certifies a non-vacuous radius on the very nets (CIFAR, deep) where ∏‖Wᵢ‖₂ is astronomically loose. Generic over any VerifiedNet (fwd + train-step only).

n (SMOOTH_N, default 10000 — Cohen's large-n regime) is the estimation budget and the only tightening lever: the per-point radius is capped at σ·Φ⁻¹(α^(1/n)) (a unanimous vote certifies only p_A ≥ α^(1/n)), so larger n lifts the ceiling and tightens the CP bound toward the true noise-probability — bigger certified radii at the same 1−α guarantee.