domainCost
plain-language theorem explainer
Domain cost scores a mass-to-energy ratio by the unique RS recognition cost J. Cosmology proofs that compare Planck-scale mass and energy scales against the Hubble ladder cite it as the local cost functional. The body is a one-line specialization of J to the quotient 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 ambient module derives a structural match of the observed Hubble constant $H_0\approx 67.4,\mathrm{km/s/Mpc}$ to a pure phi-ladder expression $H_0=\phi^k/\tau_{\mathrm{universe}}$ with $\tau_{\mathrm{universe}}=13.8,\mathrm{Gyr}$, at the Planck rung $\phi^{67}$. Status is structural: zero sorry, zero axiom.
The cost functional used throughout is the J-cost forced by the Recognition Composition Law (T5): $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$. Upstream docs state it is the unique cost of a positive ratio and is strictly positive whenever the ratio is not one. Domain cost simply feeds the mass-to-energy quotient into that same $J$.
proof idea
Pure definitional abbreviation: apply the imported J-cost to the real quotient $m/e$. No lemmas, no tactics, no side conditions are discharged at the definition site.
why it matters
Gives the module a named cost on mass/energy pairs so later certificates (canonical threshold positivity, the HubblePrecise2Cert bundle, and the inhabited cert) can speak about when a domain is costly enough to sit on the Hubble ladder. It is the local instance of the T5 J-uniqueness landmark inside the cosmology derivation of $H_0$ from $\phi^k/\tau_{\mathrm{universe}}$. 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.