Pillar 3 · Epistemic Trust
De Bruijn Criterion for Physics
Non-Vacuity Sanity Checks
Audit the PlasmaLean Kernel in 10 Minutes
How can a plasma physicist or differential geometer trust a machine-checked stellarator certificate without reading tens of thousands of lines of proof tactics? By auditing **only the small specification kernel and its sanity checks**. Select each of the 4 kernel modules below to inspect its exact Lean 4 specification, what specification trap it guards against, and the compiled sanity-check theorem that validates it.
Minutes 0–2
Trusted Specification Layer
Compiled Non-Vacuity Sanity Check
Auditor's Commentary
Why This Definition Is Structured This Way
⚠️ Specification Bug Prevented
✓ Auditor's Checklist
- No project-specific
axiomorsorryin kernel types. - All division operations guarded by explicit positivity hypotheses (e.g.
d_min > 0). - Level sets explicitly witnessed as
Nonemptyand regular (grad ψ x ≠ 0).