domainCost
plain-language theorem explainer
Domain cost scores a stellar mass m against an energy (or mass) scale e by the recognition cost of their ratio. Astrophysicists deriving the Salpeter IMF from the φ-ladder cite it as the local cost density on the mass axis. The body is a one-line specialization of the standard J-cost to m/e.
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 cost of a positive ratio.
background
The module builds a structural account of the Salpeter initial mass function $N(M)\propto M^{-2.35}$ from the φ-ladder, aiming for an exponent near $-(1+3/\varphi^2)\approx-2.146$. Status is a zero-sorry structural theorem package.
The recognition cost $J(x)=\frac{x+x^{-1}}{2}-1$ (equivalently $\cosh(\log x)-1$) is the unique nonnegative functional forced by the Recognition Composition Law and T5 J-uniqueness. It vanishes only at ratio one and measures genuine distinction. Upstream modules (Cost, Cosmology.RefineTrigger, Gravity.CoherenceCollapse) all expose the same $J$ on positive reals.
Here the two arguments are a stellar mass $m$ and a reference scale $e$ (energy or mass yardstick). Their ratio is the dimensionless input to $J$, so domain cost is the local cost of placing mass $m$ on that scale.
proof idea
Pure definitional abbreviation: apply the standard $J$-cost to the single ratio $m/e$. No lemmas, tactics, or side conditions appear in the body.
why it matters
This is the cost primitive for the φ-ladder IMF construction in Astrophysics.StellarMassFunction_FromPhiLadder. Sibling facts (nonnegativity, evaluation identities, canonical threshold positivity) and the SalpeterIMFCert package sit on top of it. In the broader RS chain it is the same $J$ fixed at T5, specialized to a mass-to-scale ratio so that ladder rungs and gap corrections can feed an IMF slope. The module notes the naive $-(1+1/J(\varphi))$ is far too steep, while $-(1+3/\varphi^2)$ is close to Salpeter; domain cost is the quantity those slope heuristics evaluate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.