cert_inhabited
plain-language theorem explainer
The certificate bundle for RS Physics Module 7 (top Yukawa y_t = 1 at unification) is nonempty. Anyone citing the structural package for the top as the phi^0 coupling uses this inhabitation fact. The proof is a one-line term that exhibits the concrete certificate already built in-module.
Claim. There exists a certificate asserting: (i) the domain cost vanishes on the diagonal, $C(r,r)=0$ for all $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
Module 7 packages the Recognition Science claim that the top Yukawa equals one at unification: the top sits at the $\phi^0=1$ rung of the coupling ladder. The local certificate structure collects three elementary analytic facts about the module's domain cost $C$ and its canonical threshold $T_*$.
Domain cost is the in-module cost functional on pairs of positive reals (mass-like and energy-like arguments). The certificate demands diagonal vanishing $C(r,r)=0$ off zero, nonnegativity on the positive quadrant, and $T_*>0$. These are the minimal structural side-conditions the module exposes before any numerical matching to SM Yukawas.
The structure itself is pure data: three propositions, no axioms. Inhabitation is the statement that those three propositions are simultaneously realized by the concrete definitions already present in the file.
proof idea
One-line term proof. Lean’s Nonempty is witnessed by a single inhabitant; the proof supplies the already-constructed term cert (the in-module value of type RSPhysics007Cert) inside an anonymous constructor. No tactics, no further lemmas: inhabitation reduces to pointing at that witness.
why it matters
Closes the structural layer of Physics Module 7: once the certificate type is inhabited, downstream consumers can assume diagonal vanishing, nonnegativity, and a positive threshold without re-proving them. The module frames the top as the $\phi^0=1$ coupling (top Yukawa $y_t=1$ at unification), consistent with the phi-ladder mass/coupling organization and the forcing chain’s self-similar fixed point $\phi$ (T6). No used_by edges are recorded yet; the theorem is the export hook for any later matching or renormalization argument that needs a certified cost package for the top sector. Status is fully proved (zero sorry, zero axiom).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.