domainCost
plain-language theorem explainer
Domain cost assigns to a mass–energy pair the recognition cost of their ratio. Cosmology arguments that place CMB temperature on the phi-ladder use it as the local cost on scale ratios. It is a one-line abbreviation of the forced J-functional at 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 temperature as a structural identity on the phi-ladder: $T_{\mathrm{CMB}}/T_{\mathrm{vac}}=\varphi^{-k}$ with $T_{\mathrm{vac}}$ at the Planck scale and $k=196$, recovering $T_{\mathrm{CMB}}\approx 2.73,\mathrm{K}$ (observed $2.725,\mathrm{K}$). Status is a structural theorem with no sorry and no axioms.
The underlying cost is the RS J-functional $J(x)=\frac12(x+x^{-1})-1$, forced uniquely by the Recognition Composition Law (T5). Upstream copies state that $J$ is the recognition cost of a positive ratio, is nonnegative for $x>0$, and vanishes only at ratio one. Domain cost simply evaluates that functional on a mass-to-energy (or scale) ratio $m/e$, the natural argument when comparing cosmological temperatures or energy densities.
proof idea
Definitional abbreviation only: domainCost m e is definitionally Jcost (m / e). No tactics, no lemmas, no proof obligations. Downstream equalities and nonnegativity facts unfold this definition and apply the corresponding properties of $J$.
why it matters
Gives the module a named cost on cosmological scale ratios so that threshold and certificate lemmas (canonical threshold positivity, the CMBTemp3v2 certificate) can speak in domain language rather than raw $J$. It sits under the T5 J-uniqueness landmark: the same forced cost that appears in the forcing chain is reused for CMB scale comparison. The parent structural claim is the phi-ladder identity $T_{\mathrm{CMB}}=T_{\mathrm{vac}}\varphi^{-196}$. No external used_by edges are recorded; consumption is local to the CMBTemp3 certificate stack in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.