cert
plain-language theorem explainer
Packages three structural properties of the Na-ionization domain cost into one certificate: diagonal vanishing, nonnegativity for positive mass/energy, and a positive canonical threshold. Chemists or RS auditors citing the Module 2 ionization match would reference this record. The body is a pure structure assembly of three already-proved field lemmas.
Claim. There is a certificate asserting: (i) the domain cost of any nonzero ratio against itself is zero; (ii) for positive mass and energy parameters the domain cost is nonnegative; (iii) the canonical threshold is strictly positive.
background
Chemistry RS Module 2 targets the sodium ionization energy match $\phi^4 \cdot 0.750,\mathrm{eV} \approx 5.14,\mathrm{eV}$ against the experimental $5.139,\mathrm{eV}$. The module is marked structural (zero sorry, zero axiom).
The certificate type bundles three Prop fields on a real-valued domain cost: equality to zero when both arguments coincide and are nonzero; nonnegativity whenever both arguments are positive; and positivity of a fixed canonical threshold. Domain cost is the local specialization of the Recognition J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$).
Upstream, nonnegativity of recognition-event cost is already available from ObserverForcing via $J$-cost nonnegativity on positive states. The three field lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge the structure obligations in this module.
proof idea
Pure structure construction. The definition is noncomputable only because the ambient reals and cost infrastructure are; no computation runs. Each field is filled by the corresponding sibling lemma: diagonal vanishing by domainCost_at_eq, nonnegativity by domainCost_nonneg (itself resting on the foundation cost-nonnegativity fact), and threshold positivity by canonicalThreshold_pos. No further tactics or rewriting.
why it matters
Gives a single named inhabitant of the Module 2 certificate type so downstream chemistry results can assume the three cost axioms without re-proving them. The module doc frames this as the structural half of the Na ionization match ($\phi^4$ yardstick times the $0.750,\mathrm{eV}$ rung factor). No used_by edges are recorded yet; the certificate is the export surface for later ionization or rung-ladder theorems in the chemistry layer. It sits under the broader RS cost forcing (T5 J-uniqueness and the RCL) rather than under the geometric T7/T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.