domainCost
plain-language theorem explainer
Domain cost assigns the RS recognition cost of a mass-to-energy ratio: J(m/e) with the unique cost J(x)=(x+x^{-1})/2-1. Structural Physics certificate work at rung 86 cites it as the scalar cost of a domain pair (m,e). The body is a one-line abbreviation of the standard J-cost on the ratio.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where $J(x)=\frac{x+x^{-1}}{2}-1$ is the Recognition Science cost of a positive ratio.
background
The module is the Structural Certificate 86 for Physics: a zero-sorry structural RS prediction at recognition rung 86. It packages domain-level cost and threshold facts used in the physics sector of the monolith.
The only primitive is the J-cost functional $J(x)=\frac{1}{2}(x+x^{-1})-1$, also written $\cosh(\log x)-1$. Upstream docs call it "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost, and that $J$ is nonnegative for positive $x$. This is the T5-unique cost from the forcing chain and the left-hand side of the Recognition Composition Law.
Here the ratio is mass over energy scale: domain cost is simply $J$ evaluated at $m/e$. Sibling lemmas then record evaluation identities and nonnegativity.
proof idea
Pure definition: one-line abbreviation that applies the imported J-cost to the ratio $m/e$. No tactics, no lemmas, no proof obligations.
why it matters
Gives the Physics-domain scalar that Structural Certificate 86 builds on: cost of a mass/energy pair before thresholds and certificate packing. Siblings (evaluation at equality, nonnegativity, canonical threshold positivity, and the inhabited cert) sit on top of this abbreviation.
In the broader framework it is the local instance of T5 J-uniqueness: every domain comparison is measured by the same $J$ forced by the Recognition Composition Law. Rung 86 is the structural physics slot in the certificate plan; this def is the cost entry point for that slot. It does not itself force constants or masses; it only names the cost used by those later facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.