step_eq_sq
plain-language theorem explainer
Factorization of a self-similar dressing forces the unit-load response to equal the square of the half-load response: g(1) = g(1/2)^2. Anyone proving the dressing step is nonnegative (hence admissible under the self-similar balance) without a unit-linear-response calibration cites this identity. The proof is a short tactic argument: instantiate factorization at equal half-loads, rewrite the sum to 1, and simplify by ring.
Claim. If $g$ is the response of a self-similar dressing (factorizing over independent nonnegative loads), then $g(1) = g(1/2)^2$.
background
Module M5 (Calibration Forcing) eliminates the unit-linear-response normalization that earlier Alpha Genesis layers treated as an input. A self-similar dressing is a load response $g$ obeying three structural premises only: factorization over independent loads, antitonicity on nonnegative loads, and the self-similar balance $g(1)=1/(1+g(1))$ on the single step (the same balance that forces the T9 measure step).
Factorization is the inherited ledger premise: for nonnegative loads $x,y$ one has $g(x+y)=(1+g(x))(1+g(y))-1$ (equivalently a multiplicative form on $1+g$). The present lemma specializes that identity to equal half-loads. In RS-native units the forced step is $g(1)=\varphi^{-1}$; positivity of that step is not assumed but derived from this square identity together with the balance equation having a unique admissible root.
The ambient goal is that every self-similar dressing equals $\varphi^{-t}$ on nonnegative loads, so the forward $\alpha$ object carries zero calibration input.
proof idea
Instantiate the dressing's factorization axiom at the pair of loads $(1/2,1/2)$, both nonnegative by norm_num. That yields an identity whose left-hand load sum is $1/2+1/2$. Rewrite the sum to $1$ (again norm_num), substitute, and finish with ring to obtain $g(1)=g(1/2)^2$. No external lemmas beyond the structure's factorization field are required.
why it matters
This is the algebraic hinge that turns factorization into positivity of the step. Downstream, step_nonneg rewrites via this identity and applies nonnegativity of squares, so $0\le g(1)$ with no sign hypothesis on $g$. That nonnegativity, plus the self-similar balance, forces the unique admissible root $g(1)=\varphi^{-1}$ (step_forced), and thence the full response $g=\varphi^{-t}$ (selfSimilar_response_forced).
In the Alpha Genesis chain this discharges residual normalization worry: the (D1)+(D2) dressing of M1 demotes to a natural-units display of a fully forced object, and $\alpha^{-1}$ is recovered from every self-similar dressing. The same two structural facts (factorization, self-similar balance) that force the recognition measure also force the dressing step; no CODATA or unit convention enters. Framework landmarks: T6 $\varphi$ as self-similar fixed point, and the T9/W2 step balance reused here as a premise rather than a calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.