domainCost
plain-language theorem explainer
Domain cost assigns to a real pair (m,e) the recognition cost of their ratio m/e. Anyone deriving the solar constant on the φ-ladder uses it as the local cost on mass-energy scale ratios. The body is a one-line specialization of the unique RS cost functional J.
Claim. For $m,e \in \mathbb{R}$, 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 ambient module places the solar constant on the φ-ladder: $S_0 \approx 1361,\mathrm{W/m^2}$ sits near $\varphi^{15}\approx 1364$, via the structural identity $S_0=\sigma_{\mathrm{SB}}T_{\mathrm{sun}}^4(R_{\mathrm{sun}}/\mathrm{AU})^2$. Status is a structural theorem (no sorry, no axiom).
The cost functional is the standard RS J-cost $J(x)=\frac12(x+x^{-1})-1$. Upstream docs state it is "the unique cost functional forced by the Recognition Composition Law" and that "a genuine distinction (ratio not one) has strictly positive cost." Domain cost simply evaluates that functional on the scale ratio $m/e$.
proof idea
Pure definition: apply J-cost to the quotient $m/e$. No lemmas, no tactics; the body is the term Jcost (m / e).
why it matters
Gives the module a named cost on mass-energy pairs so later certificates (canonical threshold, solar-constant cert, nonnegativity) can speak about $J(m/e)$ without repeating the formula. It is the local instance of the T5 J-uniqueness cost inside the solar-constant φ-ladder argument (rung 15 in W/m² units). Downstream siblings such as nonnegativity and the inhabited solar-constant certificate are the intended consumers; the graph currently lists no external used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.