step_nonneg
plain-language theorem explainer
The unit step of any self-similar dressing response is nonnegative: g(1) ≥ 0. Calibration-forcing and α-genesis arguments cite this before proving the step is strictly positive and equals φ⁻¹. The proof rewrites the step as a square via load factorization, then applies nonnegativity of squares.
Claim. For a self-similar dressing response $g$ (factorizing, antitone on nonnegative loads, and satisfying the balance $g(1)=1/(1+g(1))$), the unit step obeys $0 \leq g(1)$.
background
Module M5 (Calibration Forcing) eliminates the unit-linear-response normalization from the α dressing. A self-similar dressing is a response $g$ with three structural premises only: factorization over independent loads, antitonicity on nonnegative loads, and the balance $g(1)=1/(1+g(1))$ on the single step (the same balance that forces the T9 measure step).
The step value is $g(1)$. Upstream, factorization at equal half-loads gives the identity $g(1)=g(1/2)^2$ (step_eq_sq). That square representation is the only input needed for nonnegativity; no derivative condition or CODATA constant enters.
The broader Alpha Genesis chain then forces $g=\varphi^{-t}$ on all nonnegative loads, so the step itself is derived rather than calibrated.
proof idea
Term proof in two steps. Rewrite the goal with step_eq_sq, replacing $g(1)$ by $g(1/2)^2$. Discharge the rewritten goal by sq_nonneg, the standard fact that every real square is nonnegative. No case split and no appeal to the balance equation.
why it matters
This is the first half of step positivity in the calibration-free α pipeline. Downstream step_pos combines it with step_ne_zero (balance forbids $g(1)=0$) to get $0<g(1)$. From there step_forced solves the balance and obtains the unique admissible root $g(1)=\varphi^{-1}$, linking T6 self-similarity ($r^2=r+1$) to the dressing step.
Module doc states the point: positivity of the step follows from factorization alone, so the dressing of the α seed carries zero calibration input. The same nonnegativity is reused in ledger-counted convergence (M_nonneg, gravity SevenGaps), where step weights must stay in the nonnegative cone.
Landmark contact: T6 φ fixed point, and the shared balance equation with the T9 measure step (W2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.