cert
plain-language theorem explainer
Packages three structural facts about the carbon-ionization domain cost into one certificate: the cost vanishes on the diagonal, stays nonnegative for positive mass and energy, and the canonical threshold is positive. Chemists or RS auditors citing the Module 3 carbon match (phi^5 eV versus 11.26 eV) use this bundle. The definition is a pure record assembly of three already-proved 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 reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
Module 3 treats carbon ionization in Recognition Science units. The reported match is $\varphi^5,\mathrm{eV}\approx 11.09,\mathrm{eV}$ against the experimental $11.26,\mathrm{eV}$ (about $1.5%$ relative error), labeled MATCH and carried as a structural theorem with no sorry and no axioms.
The domain cost is the local specialization of the RS J-cost (the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$). Nonnegativity of recognition cost is a foundation fact: any recognition event has cost $\ge 0$, via $J$-cost nonnegativity on positive states. The certificate structure simply names the three properties needed downstream: diagonal vanishing, positivity of cost off the identity, and a positive canonical threshold.
proof idea
One-line record construction. The three fields of the certificate structure are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra is performed at this site; the definition only packages those proofs.
why it matters
Gives a single named inhabitant of the Module 3 certificate type so later chemistry lemmas can assume the carbon-ionization cost package without re-proving diagonal vanishing, nonnegativity, or threshold positivity. It sits under the module claim that carbon ionization is a structural MATCH at the $\varphi^5$ rung (linked to the RS constant $Z_{\mathrm{cf}}=\varphi^5\in(11,12)$ and the broader phi-ladder mass/energy bookkeeping). No downstream users are recorded yet; the value is local packaging for the chemistry forcing chain rather than a new physical identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.