step_ne_zero
plain-language theorem explainer
The unit step of a self-similar dressing cannot vanish: g(1)=0 contradicts the balance g(1)=1/(1+g(1)). Anyone deriving step positivity without a calibration input cites this. Proof is pure contradiction: substitute zero into the balance and reduce by arithmetic to 0=1.
Claim. Let $g$ be the response of a self-similar dressing (factorization, antitonicity, and the balance $g(1)=1/(1+g(1))$). Then the unit step satisfies $g(1)\neq 0$.
background
Alpha Genesis M5 (Calibration Forcing) eliminates the unit-linear-response calibration that earlier dressing axioms carried. A self-similar dressing is a response $g$ on nonnegative loads with three structural premises only: factorization over independent loads, antitonicity (more load never helps), and the self-similar balance $g(1)=1/(1+g(1))$ on the single step. That balance is the same equation that forces the T9 measure step.
The module target is to force $g=\varphi^{-t}$ on all nonnegative loads, with step value $g(1)=\varphi^{-1}$ derived rather than calibrated. Nonzeroness of the step is the intermediate fact needed before strict positivity and uniqueness of the admissible balance root.
proof idea
Contradiction on the balance field of the dressing. Assume $g(1)=0$. Rewrite the self-similar balance $g(1)=1/(1+g(1))$ at that hypothesis to obtain $0=1/(1+0)$, i.e. $0=1$. A norm_num close finishes. No external lemmas; only the balance identity carried by the self-similar dressing.
why it matters
Immediate parent is step positivity, obtained by combining this nonzeroness with the already-proved nonnegativity of the step (via lt_of_le_of_ne). Strict positivity is required for step forcing: the balance then has exactly one admissible root $g(1)=\varphi^{-1}$, whose reciprocal solves the T6 self-similarity equation $r^2=r+1$.
In the broader Alpha Genesis chain this discharges residual normalization worry. The dressing of the $\alpha$ seed carries zero calibration input; form, rate, and step are forced by factorization and self-similar balance alone, the same structural facts that force the recognition measure. Downstream, every self-similar dressing yields the forward $\alpha$ object with no CODATA reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.