domainCost
plain-language theorem explainer
Domain cost is the recognition cost of a mass-to-energy ratio: J(m/e). Cosmology and CMB anisotropy arguments cite it when converting a local mass/energy contrast into a dimensionless J-cost. The definition is a one-line application of the forced cost functional J to the ratio m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{1}{2}(x+x^{-1})-1$ is the recognition cost of a positive ratio.
background
The module develops a structural account of CMB temperature anisotropy from Recognition Science J-cost. The stated target scale is $\Delta T/T\sim 10^{-5}$, compared with the RS estimate $J(\varphi)^{D+1}=J(\varphi)^4\approx 1.94\times 10^{-4}$.
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 record the same definition and the elementary facts that $J(1)=0$ and $J(x)>0$ for genuine distinctions $x\neq 1$ (positive $x$).
Here the inputs are a mass-like scale $m$ and an energy-like scale $e$. Their ratio is the dimensionless argument fed to $J$, so domain cost measures how far the pair $(m,e)$ sits from the balanced ratio $1$.
proof idea
Pure definition: no proof obligations. The body applies the shared noncomputable $J$-cost to the quotient $m/e$. Sibling lemmas in the same file (nonnegativity, evaluation identities) are expected to inherit the corresponding properties of $J$.
why it matters
In the CMB anisotropy stack, physical contrasts must be scored by the same cost that the forcing chain uniquely selects (T5 J-uniqueness). Packaging $J(m/e)$ as domain cost gives cosmology proofs a single named hook for mass/energy imbalance before thresholds and certificates (canonical threshold, MatterPert4Cert) are applied.
The module status is structural theorem with zero sorry and zero axiom; this definition is the local cost primitive that those later statements quantify. It ties the cosmology layer to the global RS landmarks: RCL-forced $J$, $\varphi$-ladder scales, and the $D=3$ power that produces $J(\varphi)^4$ as the anisotropy yardstick. No downstream uses are recorded yet in the graph, so its immediate role is in-module scaffolding for the MatterPert4 certificate path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.