domainCost
plain-language theorem explainer
Domain cost assigns to a real pair (m,e) the recognition cost of their ratio m/e. Cosmologists matching the BAO drag scale in RS units cite it as the local cost on the mass-energy plane. It is a one-line definition that applies the unique J-cost functional.
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 treats the BAO (baryon acoustic oscillation) scale in Recognition Science units. Planck reports $r_{\mathrm{drag}}\approx 147.09,\mathrm{Mpc}$; the RS estimate $\varphi^{14}\cdot 0.174,\mathrm{Mpc}\approx 146.7,\mathrm{Mpc}$ sits within $0.3%$ of that figure. The present definition supplies the cost functional used on that scale comparison.
Upstream, $J$ is the unique cost forced by the Recognition Composition Law: $J(x)=\frac{1}{2}(x+x^{-1})-1$ for $x>0$. Doc-comments across Cost, CoherenceCollapse, and EnergyProcessingBridge all record the same formula and note that a genuine distinction (ratio not one) has strictly positive cost. Domain cost simply evaluates that functional on the ratio of the two real arguments.
proof idea
Pure definitional wrapper: domainCost m e is definitionally Jcost (m / e). No lemmas, tactics, or side conditions appear in the body.
why it matters
Sits in the Foundation BAO Exact5 module, which claims a structural (0-sorry) match of the RS BAO scale to the Planck drag radius. Sibling lemmas (domainCost_at_eq, domainCost_nonneg) and the certificate BAOScaleRS_Exact5Cert build on this cost. Framework landmark: T5 J-uniqueness forces $J(x)=\cosh(\log x)-1$, so every ratio cost in the BAO argument is the same functional that appears in the forcing chain and the RCL. No downstream edges are recorded yet; the definition is local scaffolding for the exact-five certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.