domainCost
plain-language theorem explainer
Defines the domain cost of a real pair (m, e) as the recognition cost J of their ratio m/e. Cosmology arguments that compare mass and energy scales against a J-threshold cite this abbreviation. It is a one-line wrapper around the standard J-cost functional.
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 ambient module treats the cosmological horizon problem in Recognition Science: inflation supplies $N_e = 44$ e-folds at temperature $T = J(\varphi), T_{\mathrm{Planck}}$, with expansion factor $\varphi^{44} \sim 10^9$ interpreted against the usual $10^{24}$–$10^{26}$ requirement.
The unique cost forced by the Recognition Composition Law is $J(x) = \frac{1}{2}(x + x^{-1}) - 1$ (equivalently $\cosh(\log x) - 1$). Upstream docs state that $J$ is the RS recognition cost of a positive ratio, is nonnegative for $x > 0$, and is strictly positive when the ratio is not one. Domain cost simply evaluates that functional on the ratio of two real parameters (mass-like over energy-like, or any comparable pair of scales).
proof idea
Pure definitional abbreviation: domainCost m e is definitionally equal to Jcost (m / e). No lemmas or tactics; the body is the single application of the imported J-cost functional to the quotient.
why it matters
Gives the local cost primitive for the horizon-problem certificate chain in this module (siblings include nonnegativity, evaluation lemmas, a canonical threshold, and HorizonProb3Cert). In the broader RS picture it ties cosmological scale comparisons to the T5 J-uniqueness landmark and the RCL-forced cost, so that horizon resolution can be stated as a threshold inequality on J rather than an ad-hoc energy functional. Downstream use inside the module is structural scaffolding for the 8-tick / $\varphi$-ladder inflation narrative; no external used-by edges are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.