domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Cosmology proofs that bound reionization optical depth from J-cost cite it as the local cost functional. The body is a one-line abbreviation of the forced cost J on m/e.
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 derives the CMB reionization optical depth from Recognition Science J-cost, targeting Planck 2018 $\tau\approx 0.054$. Status is structural: zero sorry, zero axiom. Candidate closed forms include $\tau=J(\varphi)/2\approx 0.059$ (within about 10%).
The recognition cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law: $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$). Upstream modules (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge) all expose this same $J$ as the cost of a genuine distinction when the ratio is not one. Domain cost simply specializes $J$ to a mass-over-energy ratio, the natural dimensionless argument in the optical-depth setting.
proof idea
Pure definition: no proof obligations. The right-hand side is the standard J-cost applied to the ratio $m/e$. Downstream lemmas (nonnegativity, evaluation identities) inherit directly from properties of $J$.
why it matters
Gives the module a named cost on mass–energy pairs so optical-depth certificates can speak in RS-native units rather than raw $J$. Siblings include nonnegativity of domain cost, a canonical positive threshold, and the CMB optical-depth certificate inhabiting that threshold. Ties to the forcing chain at T5 (J-uniqueness) and the RCL that forces $J$. The module’s numerical target is Planck $\tau\approx 0.054$ via forms such as $J(\varphi)/2$. No downstream users are recorded yet; the def is local scaffolding for the certificate chain in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.