J_mass
plain-language theorem explainer
J_mass(r) assigns the recognition cost to mass configurations at scale ratio r. Astrophysicists deriving stellar mass-to-light ratios from observability constraints would cite this when building total-cost models. It is a direct one-line alias to the core Jcost function.
Claim. The recognition cost for a mass configuration at scale ratio $r$ is defined by $J_ {mass}(r) := J(r)$, where $J$ is the cost function induced by the multiplicative recognizer on positive ratios.
background
The module develops Strategy 3 for recognition-bounded observability. Observable stellar systems require photon flux above the coherence threshold and mass assembly inside coherence volumes of size $l_rec^3$. The total cost is the sum of separate mass and light contributions, minimized subject to these geometric limits, yielding $M/L$ ratios that are powers of phi. J-cost itself is the cost of a recognition event, obtained from the derivedCost of a multiplicative recognizer comparator and from the Jcost applied to RecognitionEvent states. The upstream scale definition supplies the discrete phi-powers used for rung assignments on the ladder.
proof idea
One-line definition that directly delegates to Cost.Jcost r.
why it matters
J_mass supplies the mass term inside J_total, whose minimization produces the main result M/L in {phi^n : n in [0,3]} with typical value phi. This closes the loop from the forcing chain (T5 J-uniqueness, T6 phi fixed point) through the Recognition Composition Law to concrete astrophysical ratios, matching the outcomes of Strategies 1 and 2. It touches the phi-ladder mass formula and the eight-tick octave periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.