domainCost
plain-language theorem explainer
Defines the domain cost of a mass-to-energy ratio as the RS recognition cost J(m/e). Cosmology and structural-prediction arguments cite it whenever a positive scale ratio must be scored by the unique J-cost. The body is a one-line abbreviation of Jcost on the quotient.
Claim. For real numbers $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
This module records structural RS cosmology claims: the cost functional is forced to $J(x)=\frac12(x+x^{-1})-1$, $\varphi$ is the golden ratio fixed point, and $D=3$ is forced. Status is structural theorem (no sorry, no axioms).
The recognition cost $J$ is the unique nonnegative functional compatible with the Recognition Composition Law. Upstream copies state it as $J(x)=\frac12(x+x^{-1})-1$ for $x>0$, with $J(x)=0$ iff $x=1$ and $J(x)>0$ for genuine distinctions. Energy-processing and coherence modules reuse the same $J$ as the forced cost.
Here the two arguments are a mass-like scale $m$ and an energy-like scale $e$. Their ratio is the dimensionless input to $J$, so domain cost measures how far that ratio sits from unity on the RS cost landscape.
proof idea
Pure definitional abbreviation: domainCost m e is definitionally Jcost (m / e). No lemmas or tactics; the meaning is inherited entirely from the upstream $J$-cost definition.
why it matters
Gives the cosmology module a named handle for scoring mass/energy scale ratios by the forced RS cost $J$, the T5 landmark $J(x)=\cosh(\log x)-1$. Sibling facts (domainCost_nonneg, domainCost_at_eq, canonicalThreshold) build nonnegativity, equality cases, and threshold comparisons on top of this def. Even with no recorded downstream users yet, it is the local primitive for RS_COS structural certificates that compare domain costs to canonical thresholds. It does not itself force $\varphi$ or $D=3$; those sit in the broader forcing chain (T6, T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.