Stopping cubes without recursion in Lean: principal cubes by dyadic rank

Treil-style principal cubes (children = maximal I inside J with avg_I >= 2 avg_J) need a generation-by-generation recursion, which is painful over a Finset of dyadic cubes. A non-recursive variant works for Carleson/Sawyer-type arguments: let rank Q = Int.log 2 (avg_Q).toNNReal and call J principal if J is in L and every strictly larger L-cube has avg < 2^(rank J). The stopping parent of I is the smallest principal cube containing it (argmax of generation over a filter). You still get avg_I < 2 avg_parent, F_J constant on the principal children, and disjoint remainders J minus children. The only change is that the Carleson property is replaced by a pointwise count: the principal cubes through a point have strictly increasing ranks, so sum avg_J^2 1_J <= 8 (Mf)^2 (geometric sum by Finset.induction_on_max), and Doob finishes.