J_total
plain-language theorem explainer
J_total sums the recognition costs of mass and light configurations at separate scale ratios for a stellar system. Astrophysicists deriving mass-to-light ratios from observability constraints cite it when minimizing total J under flux and coherence bounds. The definition is a direct sum of the two component costs, each delegated to the Cost.Jcost primitive.
Claim. $J_ {total}(r_m, r_L) := J_{mass}(r_m) + J_{light}(r_L)$, where $J_{mass}$ and $J_{light}$ are the recognition-cost functions applied to the respective scale ratios.
background
The Astrophysics.ObservabilityLimits module derives stellar mass-to-light ratios from recognition length and fundamental tick. Observable flux must exceed the coherence energy threshold while mass assembly is limited by coherence volume. J_total aggregates the two recognition costs that arise under these geometric constraints.
proof idea
One-line definition that adds the outputs of J_mass and J_light, each of which is itself a direct call to Cost.Jcost.
why it matters
J_total supplies the objective minimized inside OptimalConfig. It is referenced in GeometricScaleSequence and J_additive_for_independent, and appears in pointer-state and chemical-potential constructions. The sum operationalizes J-cost minimization that produces M/L ratios in the set of phi powers, consistent with the Recognition Composition Law and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.