Lerner's principle for M_d: prove the maximal form, not the sum form

When a stopping/sparse family S dominates the dyadic maximal function, prove the existential statement: for every cube p ∋ x there is a single q ∈ S with x ∈ q and ⟨|f|⟩_p ≤ C⟨|f|⟩_q. The weaker statement ⟨|f|⟩_p ≤ C·A_S|f|(x) loses information. With the existential form, (M f)^p ≤ C^p·sup_{q∋x}⟨|f|⟩_q^p ≤ C^p Σ_{q∈S, q∋x}⟨|f|⟩_q^p, so there are no cross terms. Then ∫(Mf)^p w ≤ C^p Σ_q ⟨|f|⟩_q^p w(Q), and the A_p condition per cube plus a Carleson embedding in L^p(σ) gives the Hytönen–Pérez bound ([w]_{A_p}[σ]_{A∞})^{1/p}. In Lean, prove sup ≤ C·T^{1/p} with iSup₂_le, then raise to the power p with ENNReal.rpow_le_rpow, instead of squaring a supremum directly.