domainCost
plain-language theorem explainer
The domain cost of a mass scale m relative to an energy yardstick e is the recognition cost of their ratio. Cosmology proofs that place the inflaton on the phi-ladder cite this as the local cost functional. It is a one-line abbreviation of J applied to m/e.
Claim. For real $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
The module treats the inflaton mass as a structural placement on the phi-ladder: $m_{\mathrm{inflaton}} = \varphi^k E_{\mathrm{coh}}$. With $E_{\mathrm{coh}} \approx 0.121,\mathrm{MeV}$ and rung $k \approx 57$, the scale lands near $10^{13},\mathrm{GeV}$. Status is structural (no sorry, no axiom).
The underlying cost is the unique J-functional forced by the Recognition Composition Law: $J(x) = \frac{x + x^{-1}}{2} - 1$ for $x > 0$. Upstream modules (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge) all expose the same $J$. A genuine distinction (ratio not one) has strictly positive cost.
Here the ratio is mass over energy yardstick, so domain cost measures how far the candidate mass sits from the reference scale in recognition units.
proof idea
Pure definitional abbreviation: domain cost of $(m,e)$ is defined to be $J(m/e)$. No proof obligations; the body is the single application of the shared J-cost functional to the ratio.
why it matters
Gives the module a named cost on mass-energy pairs so later lemmas (non-negativity, evaluation at equality, canonical threshold, and the InflatonMass3 certificate) can speak about inflaton placement without reopening the J definition. Ties the cosmology pass to the T5 uniqueness of $J$ and to the phi-ladder mass formula used throughout RS. No downstream edges are recorded yet; siblings in the same file are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.