cert
plain-language theorem explainer
Packages three structural facts for the Z-boson mass module into one certificate: domain cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is positive. Anyone citing the module's zero-sorry structural status uses this witness. The body is a pure structure assembly from three sibling lemmas.
Claim. There is a certificate asserting: (i) for every nonzero real $r$, the domain cost at $(r,r)$ is zero; (ii) for all positive mass $m$ and energy $e$, the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
Physics RS Module 11 records the Z-boson mass match $M_Z \approx 91.2,\mathrm{GeV} \sim \varphi^{13}\cdot 0.175$, marked as a structural theorem with no sorry and no axioms. The local cost is a domain-level recognition cost (J-cost style) on mass and energy arguments, imported from the Cost and Constants layers.
The certificate structure demands three properties: diagonal vanishing of domain cost, nonnegativity for positive inputs, and positivity of a canonical threshold. Upstream, the foundation lemma that every recognition-event cost is nonnegative (via $J$-cost nonnegativity on positive states) supplies the conceptual precedent for the nonnegativity field.
Sibling lemmas already prove each field: domain cost equals zero when the two arguments coincide (nonzero), domain cost is nonnegative on the positive quadrant, and the canonical threshold is positive.
proof idea
One-line structure construction. The definition fills the three fields of the certificate by pointing at the sibling proofs domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No new algebra is done here; it is pure packaging of already-established facts.
why it matters
Gives the inhabited structural witness for Module 11's Z-boson mass certificate. The module claims a clean MATCH of $M_Z$ to the $\varphi$-ladder rung near $\varphi^{13}$ times the yardstick factor $0.175$, and this definition is the concrete value that discharges the certificate type. Together with the inhabitedness sibling it underwrites the module's "STRUCTURAL THEOREM (0 sorry, 0 axiom)" status. It sits in the physics layer that uses the forced $J$-cost and $\varphi$ from the T5–T6 forcing chain, without reopening those uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.