domainCost
plain-language theorem explainer
Domain cost of a mass–energy pair is the recognition cost of their ratio m/e. Cosmology arguments that compare mass and energy scales on the phi-ladder cite this as the local mismatch measure. The definition is a one-line specialization of the unique J-cost functional to that ratio.
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 measures mismatch of positive ratios by the J-cost $J(x)=\frac{x+x^{-1}}{2}-1$. Upstream modules record that this is the unique cost forced by the Recognition Composition Law (T5), and that a genuine distinction (ratio not one) has strictly positive cost.
This module is Cosmology RS Structural 8: adjacent rungs on the mass ladder are separated by the golden ratio $\varphi\approx 1.618$. Domain cost is the local cost of comparing a mass scale $m$ to an energy scale $e$ by feeding their ratio into $J$.
Sibling lemmas then establish evaluation identities and non-negativity; a canonical threshold is built from the same cost for structural certificates in the module.
proof idea
Pure definition: apply the shared J-cost functional to the single ratio $m/e$. No tactics, no lemmas beyond the imported $J$ abbreviation.
why it matters
Gives the cosmology layer a named cost for mass–energy domain mismatch, aligned with the forced J-functional from the forcing chain (T5) and the RCL. The module status is structural (zero sorry, zero axiom) and centers on $\varphi$-rung spacing.
Siblings domainCost_nonneg, domainCost_at_eq, and the canonical-threshold certificate build directly on this abbreviation. No downstream edges are recorded yet; the def is infrastructure for those local structural claims rather than a parent theorem itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.