domainCost
plain-language theorem explainer
Domain cost assigns to a mass scale m and an energy scale e the recognition cost of their ratio. Anyone working the structural Physics certificate at rung 76 cites it as the local cost functional. The body is a one-line abbreviation: apply the standard J-cost to m/e.
Claim. For real $m$ and $e$, the domain cost is $J(m/e)$, where the recognition cost is $J(x)=\frac{x+x^{-1}}{2}-1$.
background
The module is the Recognition Science structural certificate for Physics at recognition rung 76 (Plan v7, 120th pass), marked as a structural theorem with no sorry and no axioms.
The only primitive used here is the J-cost functional $J(x)=\frac{1}{2}(x+x^{-1})-1$, the unique nonnegative cost of a positive ratio forced by the Recognition Composition Law and T5 uniqueness. Upstream docs state it as "the RS recognition cost of a positive ratio" and note that a genuine distinction (ratio not one) has strictly positive cost; nonnegativity for positive $x$ is recorded in the Gravity and Cost modules.
Domain cost simply specializes that functional to the dimensionless ratio of a mass parameter to an energy scale, the natural comparison variable in the structural Physics layer.
proof idea
Pure definition: one-line abbreviation that feeds the ratio $m/e$ into Jcost. No tactics, no lemmas, no proof obligations.
why it matters
This is the local cost primitive for the structural Physics certificate at rung 76. Sibling lemmas (nonnegativity of domain cost, evaluation identities, the canonical threshold and its positivity, and the inhabited certificate bundle) are built directly on it. In the broader RS chain it is the T5 J-cost specialized to a mass-to-energy ratio, the same functional that appears in the forcing chain, the RCL identity, and the phi-ladder mass formula. It does not itself close a paper proposition; it supplies the cost object those siblings and the certificate inhabit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.