step_pos
plain-language theorem explainer
The unit step of a self-similar dressing response is strictly positive: g(1) > 0. Anyone deriving the forced step value g(1) = φ⁻¹ cites this as the positivity half of the admissible-root argument. The proof is a one-line combination of nonnegativity (from factorization as a square) with nonzero-ness (from the balance equation).
Claim. If $g$ is the response of a self-similar dressing, then $g(1) > 0$.
background
In Alpha Genesis M5 (Calibration Forcing), a self-similar dressing is a response $g$ on nonnegative loads obeying factorization over independent loads, antitonicity, and the self-similar balance $g(1) = 1/(1+g(1))$ on the single step. No unit-linear-response calibration is assumed. The goal is to force $g = \varphi^{-t}$ entirely from structure.
The quantity $g(1)$ is the step. Upstream, nonnegativity is already proved: factorization gives $g(1) = g(1/2)^2$, hence $g(1) \ge 0$. Separately, $g(1) \ne 0$, because substituting zero into the balance equation yields a numerical contradiction. The present result upgrades those two facts to strict positivity.
The same balance equation appears in the T9 measure's step forcing (W2). Here it is reused so that the dressing step is derived rather than calibrated, discharging residual normalization input into $\alpha$.
proof idea
Term-mode one-liner. Apply lt_of_le_of_ne to the already-proved nonnegativity step_nonneg ($0 \le g(1)$) and the symmetric form of step_ne_zero ($g(1) \ne 0$). The combination is exactly $0 < g(1)$. No further algebraic work.
why it matters
Feeds directly into step_forced, which shows the balance equation has exactly one admissible root $g(1) = \varphi^{-1}$. That theorem opens by setting $\rho := g(1)$ and invoking this positivity lemma before rearranging the balance into the T6 self-similarity equation $r^2 = r + 1$ for the reciprocal.
In the Recognition chain this closes the calibration gap for $\alpha$ genesis: the step is forced by factorization plus self-similar balance, the same structural pair that forces the recognition measure. Downstream, every self-similar dressing yields the forward $\alpha$ object with zero CODATA or unit convention. Landmarks: T6 $\varphi$ fixed point; the self-similar balance shared with the T9 measure step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.