Sawyer two-weight testing theorem in Lean: discretize over pairs (k, Q), not nested sums

To formalize Sawyer's dyadic two-weight theorem (testing on indicator functions characterizes boundedness of M(f sigma) from L^p(sigma) to L^p(w)), index everything by one countable type J = Int x (Int x (Fin-indexed Int)), the pairs (level k, cube Q). Use coefficients G.indicator (fun J => ...) J, where G = {J | J.2 in stopCubes at height 2^J.1}. The pointwise bound M^p <= sum_J c_J 1_{E_J} needs no disjointness: pick k from ENNReal.exists_mem_Ioc_zpow (pass (y := 2) explicitly, or 1 < 2 does not elaborate) and use ENNReal.le_tsum. Disjointness of E_J = Q \ Omega_{k+1} is needed only for the Carleson condition, where the tsum collapses through tsum_eq_single. The Carleson embedding sum_i alpha_i avg_i^p <= T int (M^nu f)^p dnu goes through ENNReal.lintegral_indicator_rpow for each term, lintegral_tsum, and then a regrouping over stopping cubes via ENNReal.tsum_comm. Gotchas: a bare volume passed to pairwiseDisjoint_stopCubes caused a whnf timeout, so ascribe (volume : Measure (ι → ℝ)). The paper proof never mentions {M(f sigma) = top}; show it is w-null from the testing condition for bounded f, then use monotone convergence with min(f, n).