domainCost
plain-language theorem explainer
Domain cost assigns to a mass m and energy scale e the recognition cost of their ratio m/e. Cosmology proofs that compare mass and energy on the phi-ladder cite this as the local cost functional. It is a one-line definition wrapping the standard J-cost on the positive ratio.
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 measures mismatch of positive ratios by the J-cost $J(x) = \frac{x + x^{-1}}{2} - 1$, equivalently $\cosh(\log x) - 1$. It vanishes only at $x = 1$ and is nonnegative for $x > 0$. The same functional appears as the unique solution of the Recognition Composition Law (forcing step T5).
This module (Cosmology RS Module 5) is a structural block with zero sorry and zero axioms. Its headline check is the tensor ratio $r = 2/(44\phi^2) \approx 0.0174$, which lies below the Planck bound $0.036$. Domain cost supplies the local cost of a mass-to-energy ratio inside that setting.
Upstream, Jcost is defined identically in Cost, RefineTrigger, and CoherenceCollapse: the RS recognition cost of a positive ratio, with the companion fact that a genuine distinction (ratio not one) has strictly positive cost.
proof idea
Pure definition: domain cost is the abbreviation $J(m/e)$. No proof obligations; the body is the single application of the shared J-cost functional to the ratio of the two real arguments.
why it matters
Gives cosmology a named cost for mass versus energy scale, so later inequalities (nonnegativity, threshold comparisons) can speak in domain language rather than raw $J$. The module status line marks the surrounding development as a structural theorem with no sorry and no axioms, and the $r$-tensor consistency check ($2/(44\phi^2)$ under the Planck bound) is the physical target of the file.
No downstream dependents are recorded yet; sibling lemmas in the same module (equality at a point, nonnegativity, canonical threshold positivity, and the RSCosmo005 certificate) are the natural consumers. Framework landmark: J-uniqueness (T5) and the forced $\phi$ fixed point (T6) underwrite why this cost, rather than an ad hoc penalty, is the right scalar on cosmological ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.