J_nonneg
plain-language theorem explainer
For every positive real x the recognition cost J(x) equals ½(x + 1/x) - 1 and is nonnegative. Stellar-assembly calculations that partition emission and storage costs on the phi-ladder cite this to guarantee the differential is well-defined and the resulting M/L values remain positive. The proof reduces J algebraically to the squared form (x-1)^2/(2x) and invokes nonnegativity of squares and positive denominators.
Claim. For every real number $x > 0$, the recognition cost $J(x) := ½(x + 1/x) - 1$ satisfies $J(x) ≥ 0$.
background
The recognition cost is defined by J(x) = ½(x + 1/x) - 1 and is the unique convex function minimized at x = 1 with value zero. In the StellarAssembly module this cost is applied separately to emission-scale and storage-scale ratios during collapse; the difference determines the integer step n on the phi-ladder that fixes the mass-to-light ratio. Upstream results supply the scale map k ↦ phi^k and the Configuration structure whose entries are required to be positive reals so that total defect is a sum of individual J terms.
proof idea
The tactic proof unfolds J to the underlying Cost.Jcost, derives the closed form (x-1)^2/(2x) by field simplification and ring, then applies div_nonneg together with sq_nonneg and a linarith fact that the denominator is positive.
why it matters
The lemma guarantees that recognition costs remain nonnegative throughout the stellar M/L derivation, allowing the module to conclude that observed ratios lie in {phi^n : n = 0,1,2,3}. It directly supports the claim that typical populations give M/L ≈ phi^1 and rests on the J-uniqueness property (T5) of the forcing chain together with the eight-tick octave that fixes the admissible steps n.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.