domainCost
plain-language theorem explainer
Domain cost scores a measured quantity against an expected baseline by feeding their ratio into the recognition cost J. Fine-structure and equilibrium arguments in this module cite it as the local mismatch functional. The body is a one-line definitional wrapper around Jcost.
Claim. For real numbers $m$ (measured) and $e$ (expected), 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 fine-structure interval $\alpha^{-1}\in(137.030,137.039)$ from Recognition Science structure (structural theorem, zero sorry). The working cost is the unique J-functional forced by the Recognition Composition Law: $J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$ (forcing chain T5).
Upstream, every copy of Jcost is that same map: cost of a positive ratio, strictly positive off the identity ratio, and nonnegative for $x>0$. Domain cost simply specializes it to a measured-versus-expected ratio, so equilibrium is the unit ratio and any genuine mismatch carries positive cost.
Sibling facts in the file (nonnegativity, vanishing at equilibrium, a canonical threshold) build on this abbreviation toward the fine-structure certificate.
proof idea
Definitional one-liner: evaluate the recognition cost $J$ at the ratio of the two real arguments. No lemmas, tactics, or side conditions are discharged at this declaration; positivity and equilibrium properties are proved separately on the siblings.
why it matters
Gives the module a single named mismatch score for comparing a measured electromagnetic scale to its RS-expected value. That score is the natural input to nonnegativity, equilibrium, and threshold lemmas that feed the fine-structure certificate and the claimed $\alpha^{-1}$ band. Framework-wise it is the local use of the T5-unique J-cost (and the RCL) inside the EM/fine-structure derivation path, rather than a new physical law.
No external used-by edges are recorded; the immediate consumers are the in-module siblings (domainCost_at_equilibrium, domainCost_nonneg, canonicalThreshold, FineStructure2Cert).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.