cert_inhabited
plain-language theorem explainer
The Module 4 physics certificate is inhabited: a single package records that the domain cost vanishes on the diagonal, is nonnegative for positive inputs, and that the canonical threshold is positive. Anyone citing the structural status of the tree-level Weinberg-angle module uses this inhabitation fact. The proof is a one-line term supplying the prebuilt certificate as the Nonempty witness.
Claim. The certificate type for RS Physics Module 4 is nonempty: there exists a record packing (i) vanishing of the domain cost on the diagonal for every nonzero real argument, (ii) nonnegativity of the domain cost for positive mass and energy, and (iii) strict positivity of the canonical threshold.
background
Physics RS Module 4 packages the tree-level Weinberg angle in Recognition units as $\sin^2\theta_W = J(\phi)/(1+J(\phi)) \approx 0.1054$, with a quoted loop correction to $0.231$. The module is marked structural (zero sorry, zero axiom).
The certificate structure is a three-field record. Its first field asserts that the local domain cost vanishes whenever both arguments equal a common nonzero real. The second asserts nonnegativity of that cost for positive mass and energy. The third asserts that the module's canonical threshold is strictly positive. These are the elementary cost and threshold facts the angle formula sits on top of.
Upstream, the structure is defined in-module; the inhabitation theorem only needs a concrete value of that structure.
proof idea
One-line term-mode proof. The already-constructed in-module value cert has type equal to the certificate structure, so the angle-bracket Nonempty constructor ⟨cert⟩ is a complete witness. No tactics, no further lemmas.
why it matters
This is the terminal inhabitation check for Module 4: once the three cost/threshold lemmas are packed into a certificate value, this theorem records that the package type is nonempty. Downstream code can therefore assume a certificate exists without rebuilding the three fields. The module itself links the J-cost (forcing-chain T5) and the golden-ratio fixed point $\phi$ (T6) to an electroweak observable. No further dependents are recorded in the graph yet; the declaration closes the module's structural obligation rather than feeding a larger named theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.