step_forced
plain-language theorem explainer
The self-similar balance equation forces the dressing step g(1) to equal φ⁻¹, with no calibration input. Anyone closing the α-genesis chain without a unit convention cites this. The proof reduces balance to the quadratic ρ²+ρ−1=0, matches it against 1/φ via φ²=φ+1, and kills the second root by positivity.
Claim. For any self-similar dressing, the step value satisfies $g(1)=\varphi^{-1}$, where $\varphi$ is the unique positive root of $r^2=r+1$. Equivalently, the balance $g(1)=1/(1+g(1))$ together with $g(1)>0$ admits exactly one admissible root.
background
Module M5 (Calibration Forcing) eliminates the unit-linear-response normalization that earlier α-genesis stages treated as an input. A self-similar dressing is a response obeying three structural premises only: factorization over independent loads, antitonicity on nonnegative loads, and the single-step balance $g(1)=1/(1+g(1))$. That balance is the same equation that forces the T9 recognition-measure step.
The golden ratio $\varphi$ is fixed upstream by T6 as the unique positive solution of $r^2=r+1$ (equivalently $\varphi^2=\varphi+1$, lemma phi_sq_eq). The companion lemma step_pos already derives $g(1)>0$ from factorization ($g(1)=g(1/2)^2$), so positivity is not an extra hypothesis. The local claim is that balance plus positivity pin the step exactly at $\varphi^{-1}$.
proof idea
Set $\rho:=g(1)$. Positivity is step_pos; balance is the self-similarity premise $\rho=1/(1+\rho)$. Clearing the denominator yields $\rho(1+\rho)=1$, hence the quadratic $\rho^2+\rho-1=0$ (via nlinarith).
Separately, $\varphi^2=\varphi+1$ (phi_sq_eq) implies that $1/\varphi$ solves the same quadratic. Subtracting the two quadratic identities factors as $(\rho-1/\varphi)(\rho+1/\varphi+1)=0$. The second factor is strictly positive by $\rho>0$ and $\varphi>0$, so mul_eq_zero forces $\rho=1/\varphi$.
why it matters
This is the step-forcing half of M5: the dressing rate is derived, not calibrated. Downstream, response_forced rewrites $g(1)$ via this theorem and concludes $g(t)=\varphi^{-t}$ on all nonnegative loads (the forced recognition measure, no derivative condition). The certificate CalibrationForcingCert bundles the same equality as clause (1) of M5 closure.
Framework landmark: the reciprocal of the step satisfies the T6 self-similarity equation whose unique positive root is $\varphi$. Together with factorization and antitonicity, this discharges the residual normalization worry for the α seed: form, rate, and step are forced by the same structural facts that force the recognition measure itself. No CODATA input enters.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.