J_unit_zero
plain-language theorem explainer
The recognition cost J satisfies J(1) = 0, fixing the minimum of the convex cost at unit scale ratio. Astrophysicists deriving stellar mass-to-light ratios from recognition-weighted collapse during photon emission versus mass storage would cite this as the anchor point for cost differentials. The proof is a one-line wrapper referencing the unit-zero lemma in the Cost module.
Claim. $J(1) = 0$, where the recognition cost is $J(x) = ½(x + 1/x) - 1$ for positive real $x$.
background
The StellarAssembly module defines the recognition cost as J(x) := Cost.Jcost x. The supplied doc-comment states that J is minimized at x = 1 with J(1) = 0. This cost enters the derivation of stellar mass-to-light ratios from the differential between emission cost δ_emit = J(r_emit) and storage cost δ_store = J(r_store) at collapse equilibrium.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma from the Cost module, which itself reduces by simplification of the squared-ratio form of the cost.
why it matters
This anchors the partition step in the module's main result that M/L lies on the phi-ladder with typical value φ^1. It instantiates the J-uniqueness property from the forcing chain (T5) and supplies the zero baseline required for the Recognition Composition Law applications in stellar ledger accounting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.