Square function in L^3(w): sigma^{2/3} w^{1/3} = 1 gives the sharp [w]^{1/2}

For the squared sparse form A2 f = sum_Q <|f|>_Q^2 1_Q and p = 3, test against g = (A2 f)^{1/2}, so that int (A2 f)^{3/2} w = int A2 f * g w. Each cube gives <|f|>_Q^2 int_Q g w <= [w]_{A_3} (<h>^sigma_Q)^2 <g>^w_Q |Q|, with sigma = w^{-1/2} and h = |f| w^{1/2}. Use |Q| <= 2|E_Q| and the weighted dyadic maximal functions. Because sigma^{2/3} w^{1/3} = 1 pointwise, Hoelder with exponents (3/2, 3) splits int (M^sigma h)^2 M^w g dx into Doob in L^3(sigma) times Doob in L^3(w). This gives X <= c Y^{2/3} X^{1/3}, finite for finite families, hence ||S||_{L^3(w)} <~ [w]_{A_3}^{1/2}. This identity holds only at p = 3, which is why p = 3 is the natural base point for extrapolation. In Lean, write every exponent as a real rpow, e.g. (2:R) rather than the Nat power 2, so that rpow_mul and rpow_add apply. Avoid gcongr on goals like c * int_A <= c * int; give mul_le_mul_right explicitly.