domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio by evaluating the J-cost on m/e. Cosmologists deriving the reionization endpoint from RS cost structure cite it as the local scale mismatch measure. The body is a one-line definition wrapping Jcost.
Claim. For real numbers $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module treats the end of reionization as a structural consequence of J-cost geometry. Observationally $z_{\mathrm{end}}\sim 5.5$–$6$; RS compares this to golden-ratio powers ($\phi^3\approx 4.24$, $\phi^4\approx 6.85$), taking $z_{\mathrm{end}}=\phi^4$ as the matching scale.
The unique cost forced by the Recognition Composition Law is $J(x)=\frac12(x+x^{-1})-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream docs state that any genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative on positives. Domain cost specializes that functional to a mass-over-energy ratio, the natural dimensionless argument when a domain mass scale is compared to an energy scale in the reionization argument.
proof idea
Pure definition: apply the shared J-cost functional to the ratio $m/e$. No lemmas, no tactics; the body is the single term Jcost (m / e).
why it matters
This is the cost primitive for the reionization-endpoint module (Plan v7, 118th pass), which aims at a structural theorem with zero sorry and zero axioms linking $z_{\mathrm{end}}$ to $\phi$-ladder scales. Sibling lemmas (domainCost_at_eq, domainCost_nonneg) and the certificate stack (canonicalThreshold, ReionEnd3Cert, cert) sit on top of it. Framework-wise it instantiates T5 J-uniqueness in a cosmological ratio, the same $J$ that appears across gravity and spiral modules. No downstream users are recorded yet; the def exists to feed the local nonnegativity and threshold certificates that close the endpoint claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.