domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the Recognition J-cost of that ratio: J(m/e) = (m/e + e/m)/2 - 1. Used in the RS neutron-proton mass-difference module to score how far a candidate mass scale sits from a reference energy. Pure abbreviation of the forced cost functional on the positive reals; no proof content.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ is the Recognition cost of a positive ratio.
background
Recognition Science forces a unique nonnegative cost on positive ratios via the Recognition Composition Law. That functional is $J(x) = \frac{x + x^{-1}}{2} - 1$ (equivalently $\cosh(\log x) - 1$), fixed at the T5 step of the forcing chain. It vanishes only at $x = 1$ and is strictly positive for every genuine distinction.
This module targets the neutron-proton mass split $m_n - m_p = 1.293,\mathrm{MeV}$. The RS account writes the split as a multiple of $J(\varphi)$ against a hadronic energy yardstick (roughly $10.96,\mathrm{MeV}$), recovering the observed $1.293,\mathrm{MeV}$ exactly once the W-mass correction is inserted.
domainCost packages the raw J-evaluation on a mass-over-energy ratio so later lemmas can talk about nonnegativity and threshold comparisons without repeating the quotient.
proof idea
Definitional one-liner: apply the imported J-cost functional to the quotient $m/e$. No tactics, no lemmas, no hypotheses. Downstream facts (nonnegativity, evaluation at equality) inherit directly from the corresponding properties of $J$.
why it matters
Supplies the local cost primitive for the RS5 neutron-proton difference certificate. The module status is structural (zero sorry, zero axiom): the observed $1.293,\mathrm{MeV}$ is recovered as $J(\varphi)$ times a fixed MeV yardstick. That uses the T5 uniqueness of $J$ and the golden-ratio fixed point $\varphi$ from T6. Siblings such as nonnegativity of domain cost and the canonical threshold sit on top of this abbreviation; the inhabited certificate then closes the numerical claim. No further downstream edges are recorded yet, so the definition is presently module-local scaffolding for the mass-split identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.