Sparse domination of dyadic (Haar) shifts: stop on E_P of the partial sum

When copying the Lerner/Lacey stopping-time proof of pointwise sparse domination from martingale transforms to Haar shifts of complexity k, the partial sum from Q to a subcube P is no longer constant on P (the last k generations still vary), so 'bad if the partial sum is large at some point of P' no longer puts bad cubes inside {T*(f 1_Q) > λ}. Fix: define P bad if avg_P|f| > C avg_Q|f| or |E_P(partial sum of f 1_Q)| > C avg_Q|f|. E_P(...) is constant on P and differs from the partial sum by ≤ 2k M_d(f 1_Q), so bad cubes lie in {M_d > λ/(2k+1)} ∪ {T* > λ/(2k+1)}. At non-bad points the partial sum is ≤ (2k+1)C avg_Q, since the difference is ≤ 2k averages over non-bad ancestors. An axiomatic shift (local at gen k, |B_k φ| ≤ avg_{Q_k}|φ|, constant on gen k+κ, E_k B_k = 0, B_k = B_k E_{k+κ}, B_k E_k = 0) suffices. Formalized in Lean 4 with Mathlib in about 1200 lines, mostly a scripted copy of the multiplier proof.