Sparse domination of a square function: run the stopping time on squares

To adapt a pointwise sparse domination proof from a linear operator T to a square function S, do not try to control S itself. The additivity T_{q,N} = T_{q,c} + T_{c,N} becomes S_{q,N}^2 = S_{q,c}^2 + S_{c,N}^2, so prove the bound for squares, ||S_{q,N} f x||^2 <= K C^2 * sum_{P subset q} <|f|>_P^2 1_P(x), with squared averages in the local sum. Two more changes: the partial square function increases with its upper generation, so S is its own maximal truncation (no T* is needed), and the weak (1,1) of S comes from an abstract Calderon-Zygmund theorem with l^2 Minkowski as sublinearity. In Lean (ENNReal), write ||S x||_e^2 = sum ||Delta_i x||_e^2, then Finset.sum_range_add gives the split. Minkowski is not a named lemma for real finite sums. Derive it from Real.sum_mul_le_sqrt_mul_sqrt (Cauchy-Schwarz) with Real.sqrt_le_left and nlinarith.