domainCost
plain-language theorem explainer
Domain cost of a mass-to-energy ratio is the recognition cost J(m/e). Cosmology proofs that compare multipole or polarization scales to a J-threshold cite this wrapper. It is a one-line abbreviation of the unique RS cost functional on the positive 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 treats CMB E-mode polarization as a structural consequence of the RS J-cost. The stated target is that the E/T ratio sits near $J(\varphi)\approx 0.118$ (about 10% of the temperature anisotropy), consistent with the observed E-mode fraction.
The cost functional is the unique $J$ forced by the Recognition Composition Law: $J(x)=\frac{x+x^{-1}}{2}-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream modules (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge) all expose the same $J$, with the standing fact that a genuine distinction (ratio not one) has strictly positive cost and $J\ge 0$ on positives.
Here the two arguments are a mass-like scale $m$ and an energy-like scale $e$; their ratio is the dimensionless input to $J$.
proof idea
Pure definitional wrapper: domain cost is defined by substituting the ratio $m/e$ into $J$. No tactics, no lemmas, no side conditions at the definition site. Non-negativity and evaluation identities appear in sibling lemmas that unfold this abbreviation.
why it matters
Gives the cosmology layer a named cost of a mass/energy domain ratio so polarization and threshold statements can speak in RS units rather than raw $J$ applications. The module status is structural (0 sorry, 0 axiom) and aims at the E-mode fraction via $J(\varphi)$ or a related $\varphi$-ladder combination (primer T5 J-uniqueness, T6 $\varphi$ fixed point). Sibling facts (evaluation at equality, non-negativity, canonical threshold positivity, and the CMBPolar3 certificate) sit on top of this abbreviation. No downstream edges are recorded yet; the def is local scaffolding for the polarization certificate chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.