domainCost
plain-language theorem explainer
Domain cost of a mass–energy pair is the recognition cost of their ratio. Structural-calibration work that fixes E_coh from the electron mass cites this abbreviation. It is a one-line definition: apply the unique J-cost to m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the recognition cost of a positive ratio.
background
Recognition Science forces a unique cost on positive ratios: $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream modules record that this $J$ is the unique functional obeying the Recognition Composition Law, is nonnegative for $x>0$, and vanishes only at $x=1$.
This module is Foundation structural item 10. Its charter is RS calibration: the coherence energy $E_{\mathrm{coh}}$ is fixed once by the electron mass, after which predictions are parameter-free. Domain cost packages the mass-to-energy ratio that appears in that calibration as a single $J$-evaluation.
Sibling lemmas immediately record evaluation at equality and nonnegativity; a canonical threshold is defined from the same cost.
proof idea
Pure definitional abbreviation. The body is the term $J(m/e)$ with no tactics, no lemmas, and no hypotheses. All analytic content lives in the upstream definition of $J$ and in the sibling lemmas that inherit nonnegativity and the equality case.
why it matters
Gives the structural module a named cost for mass–energy ratios used when $E_{\mathrm{coh}}$ is pinned by the electron mass. That calibration step is the module’s stated purpose: one fixed scale, then parameter-free predictions. The definition sits on the T5 landmark (uniqueness of $J$) and feeds the local certificate and threshold apparatus (canonical threshold, nonnegativity, structural cert). No downstream consumers are wired yet; the declaration is infrastructure for the calibration narrative rather than a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.