domainCost
plain-language theorem explainer
Domain cost assigns the Recognition Science J-cost to a mass-to-energy ratio m/e. Cosmology workers use it when comparing reionization scales to the phi-ladder brackets phi^4 and phi^5. The body is a one-line definitional wrapper around Jcost.
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 treats reionization redshift in Recognition Science units. Observationally $z_{\mathrm{reion}}$ sits near 7–10; RS notes that $\phi^4\approx 6.85$ and $\phi^5\approx 11.09$ bracket that window, so the structural claim is consistency of the phi-ladder with the measured band.
The cost functional is the unique J forced by the Recognition Composition Law: $J(x)=\frac{1}{2}(x+x^{-1})-1$ (equivalently $\cosh(\log x)-1$). Upstream modules record that a genuine distinction (ratio not one) has strictly positive cost, and that J is nonnegative for positive arguments. Domain cost simply feeds the ratio of two real parameters (here mass-like over energy-like) into that same J.
proof idea
Pure definition: domainCost m e is definitionally Jcost (m / e). No tactics, no lemmas, no hypotheses. Downstream nonnegativity or equality lemmas (siblings such as domainCost_nonneg) will unfold this abbreviation and apply the corresponding facts about J.
why it matters
Gives the local cost primitive for the reionization-redshift certificate in this module. The module status is structural (zero sorry, zero axiom): phi-powers bracket $z_{\mathrm{reion}}$, and domain cost is the natural place to score how far a mass/energy ratio sits from unity under the forced J of T5. It sits upstream of sibling threshold and certificate objects (canonicalThreshold, ReionizationCert) even though the graph currently lists no external used_by edges. Ties the cosmology page to the same J that appears in the forcing chain and the Recognition Composition Law, rather than inventing a separate cost for reionization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.