domainCost
plain-language theorem explainer
Domain cost of a mass-energy pair is the recognition cost of their ratio m/e. Cosmologists in the RS inflation-parameter suite use it when relating spectral observables to the J-cost of scale ratios. The declaration is a one-line abbreviation: apply J to m/e.
Claim. For real numbers $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
The module fixes RS inflation parameters against Planck-scale targets: spectral index $n_s$ and tensor-to-scalar ratio $r$, with RS predictions $n_s=1-2/45$ and $r=2/(45\phi^2)$ reported inside observational bands.
The underlying cost is the unique J-functional forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$. Upstream copies state the same formula and record that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive arguments.
Here the two arguments are treated as a mass-like scale $m$ and an energy-like scale $e$; their ratio is the dimensionless input to $J$.
proof idea
Pure definitional abbreviation. The body is the single application of the shared J-cost functional to the quotient $m/e$. No tactics, no lemmas, no side conditions are discharged at this site.
why it matters
Gives the inflation-parameter development a named cost of a mass-to-energy domain ratio, so later certificates (canonical threshold positivity, the InflationParam5Cert bundle, and the inhabited cert) can speak about domain cost without reopening the J formula. It sits on the T5 J-uniqueness landmark: the same $J$ forced by RCL is reused in cosmology rather than a bespoke inflation cost. No downstream edges are recorded yet; siblings such as nonnegativity and the equality-at-equality lemma are the immediate consumers inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.