cert_inhabited
plain-language theorem explainer
The certificate bundle for Physics Module 2 is inhabited: there exists a record packing diagonal vanishing of the domain cost, its nonnegativity on the positive quadrant, and positivity of the canonical threshold. Anyone citing the module's structural pass for the EM fine-structure band uses this existence fact. The proof is a one-line term that packages the already-built certificate value.
Claim. The type of Physics Module 2 certificates is nonempty: there exists a record whose fields assert that the domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive arguments, and that the canonical threshold is strictly positive.
background
Physics RS Module 2 is the structural package for the electromagnetic fine-structure window: $\alpha^{-1}$ forced into $(137.030,137.039)$, with CODATA $137.036$ inside, marked RS_PASS and free of sorry or axioms.
The certificate structure packages three elementary cost facts used as the module's gate: the domain cost $C$ vanishes on the diagonal away from zero, $C$ is nonnegative when both arguments are positive, and the canonical threshold (the scale against which the fine-structure band is checked) is strictly positive. These are the three fields of the certificate record.
Existence of such a record is the standard Lean pattern that turns a concrete witness into a Nonempty fact, so downstream code can assume the module's structural hypotheses without naming the witness.
proof idea
One-line term proof. The module already defines a concrete certificate value cert inhabiting the structure. The theorem is just the anonymous constructor ⟨cert⟩, which is the standard way to promote a witness to Nonempty RSPhysics002Cert. No tactics, no further lemmas.
why it matters
This is the inhabitance seal for Module 2's structural theorem status (0 sorry, 0 axiom). The module's claim is the RS fine-structure band $\alpha^{-1}\in(137.030,137.039)$ containing CODATA $137.036$; the certificate fields are the cost and threshold side-conditions that underwrite that pass.
In the broader Recognition chain the band sits with the RS-native constants ($c=1$, $\hbar=\varphi^{-5}$, $G=\varphi^5/\pi$) and the J-cost uniqueness (T5) that forces the cost functional. No downstream consumers are wired yet in the graph; the declaration exists so any later theorem that needs "Module 2 is certified" can take a Nonempty hypothesis rather than reopen the three field proofs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.