J_light
plain-language theorem explainer
J_light supplies the luminosity term in total J-cost at scale ratio r for stellar observability bounds. Researchers computing M/L ratios under recognition constraints cite it when forming J_total from separate mass and light contributions. The definition is a direct one-line alias to the core cost function induced by the multiplicative recognizer.
Claim. The J-cost for the luminosity configuration at scale ratio $r$ is defined by $J(r) := C(r)$, where $C$ is the cost function induced by a multiplicative recognizer on positive ratios.
background
This definition appears in the Astrophysics.ObservabilityLimits module, which derives mass-to-light ratios from recognition-bounded observability. Observable flux must exceed the coherence energy divided by the fundamental tick, while mass assembly is limited by coherence volume $l_{rec}^3$. J-cost is the cost of a recognition event, given explicitly as the derived cost of the comparator on positive ratios.
proof idea
One-line wrapper that applies the Cost.Jcost function to the input scale ratio $r$.
why it matters
J_light supplies the light term in J_total, which is minimized subject to observability to recover M/L ratios in powers of phi. This step closes part of the derivation that M/L lies in {phi^n : n in [0,3]}, consistent with the Recognition Composition Law and the J-uniqueness fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.