domainCost
plain-language theorem explainer
Domain cost assigns the recognition cost of a mass-to-energy ratio: J(m/e). Cosmologists working the Alcock-Paczynski structural claim in this module use it as the scalar that feeds thresholds and certificates. The body is a one-line definitional wrapper around the unique J-cost functional.
Claim. For real $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 the Alcock-Paczynski (AP) geometric distortion $\alpha_\perp/\alpha_\parallel$ as a structural consequence of recognition cost. In RS units the predicted ratio is $\varphi^{J(\varphi)/D}=\varphi^{0.118/3}=\varphi^{0.039}\approx 1.064$, with $D=3$ from the forcing chain.
The cost functional is the unique $J$ forced by the Recognition Composition Law: $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream modules define the same $J$ as "the RS recognition cost of a positive ratio" and note that any genuine distinction (ratio not one) has strictly positive cost. Domain cost simply evaluates that functional on the dimensionless ratio $m/e$.
proof idea
Definitional wrapper only: domainCost m e is definitionally equal to Jcost (m / e). No tactics, no lemmas, no hypotheses. Downstream lemmas (non-negativity, evaluation at equality) unfold this abbreviation and apply standard $J$ properties.
why it matters
Gives the module a named scalar for "how costly is this mass-energy mismatch," which the AP structural theorem and the certificate bundle (Alcock5Cert, cert) sit on. It ties cosmology numerics to the same $J$ that appears in T5 J-uniqueness and the RCL, so the AP ratio $\varphi^{J(\varphi)/3}$ is not an ad-hoc fit but an instance of the forced cost. No used-by edges are recorded yet; siblings such as non-negativity and the canonical threshold are the immediate consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.