domainCost
plain-language theorem explainer
Domain cost assigns to a pair of reals the recognition cost of their ratio. Standard-Model structural certificates in Recognition Science use it as the local cost on mass-scale pairs. The body is a one-line definitional wrapper around the forced J-cost.
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
This module is Standard Model RS Structural Module 7. Its theme is J-cost symmetry: recognition cost is ratio-symmetric, $J(x)=J(1/x)$, with status structural (no sorry, no axioms).
The underlying cost is the RS recognition functional $J(x)=\frac{1}{2}(x+x^{-1})-1$ on positive ratios. Upstream docs identify it as the unique cost forced by the Recognition Composition Law; a genuine distinction (ratio not one) has strictly positive cost, and $J$ is nonnegative for positive arguments.
Here the two arguments are treated as a scale pair; the cost depends only on the dimensionless ratio $m/e$, not on an absolute unit choice.
proof idea
Definitional one-liner: domain cost is exactly $J$ evaluated at the ratio of the two inputs. No tactics, no lemmas, no proof obligations beyond the ambient definition of $J$.
why it matters
Gives the local cost functional for the structural certificate chain in this module (siblings include nonnegativity of domain cost, evaluation identities, a canonical threshold, and the RS-STD structural 007 certificate). It packages the T5 J-uniqueness cost so Standard Model scale comparisons sit on the same functional as the rest of the forcing chain and the Recognition Composition Law. With no external used-by edges yet, its role is internal scaffolding for those sibling lemmas and the module certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.