domainCost
plain-language theorem explainer
Defines the domain cost of a pair of positive reals as the recognition cost of their ratio. Cosmology proofs that compare multipole or polarization amplitudes against a J-cost yardstick cite this abbreviation. The body is a one-line alias of the standard J-cost on m/e.
Claim. For real numbers $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 a structural CMB E/B polarization ratio from Recognition Science J-cost. Module status is a structural theorem with no sorry and no axioms: RS predicts $B/E=r/(8J(\varphi))$ for tensor-scalar ratio $r$, giving roughly $1.8%$ at $r=0.017$.
The recognition cost $J$ is the unique nonnegative functional forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$ for $x>0$, equivalently $\cosh(\log x)-1$. Upstream copies (Cost, RefineTrigger, CoherenceCollapse, EnergyProcessingBridge) all fix this same formula; EnergyProcessingBridge notes it is the unique cost forced by RCL. Domain cost simply evaluates that functional on a ratio of two real parameters (mass-like over energy-like, or any comparable pair in the polarization argument).
proof idea
Pure definitional abbreviation: domainCost m e unfolds to Jcost (m / e). No tactics, no lemmas, no side conditions in the body. Downstream nonnegativity and evaluation lemmas (siblings such as domainCost_nonneg and domainCost_at_eq) inherit the corresponding properties of $J$.
why it matters
Gives the module a named cost on amplitude or multipole ratios so the CMB polarization certificate can speak in RS-native units rather than raw $J(m/e)$. It sits under the Plan v7 structural claim $B/E=r/(8J(\varphi))$, tying the E-mode dominance story to T5 J-uniqueness and the golden-ratio fixed point $\varphi$ from the forcing chain. No downstream edges are recorded yet; siblings (canonicalThreshold, CMBPolarRatio3Cert, cert) are the intended consumers that turn this cost into a numerical polarization bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.