Stopping-time trees in Lean: inductive predicate + strong induction on generation

For a stopping-cube construction (sparse domination), do not build the family by iterating a children map. Use an inductive Prop: top m : InStop (a, m) and child : InStop q → p ∈ stopChildren q → InStop p. Define the stopping children as the maximal bad subcubes. Existence of a maximal bad cube above a bad cube p: Nat.find on the generation offset t ↦ IsBad q (q.1+1+t, index _ x), where x is a corner of p. The tree property (p, q ∈ S, p ⊊ q ⇒ p lies in a child of q) does not go through by induction on the derivation of InStop p: one case needs the hypothesis for q. Use Nat.strong_induction_on on (p.1 - a).toNat with cases hp inside. Then define E_q = q \ ⋃ children; disjointness follows from the tree property, and E_q is measurable via MeasurableSet.biUnion (to_countable _). For the domination, write the bound as a tsum over the subtype S with a set-indicator restriction to cubes inside q. Split off q's own term with tsum_ite_eq (it takes a function argument fun _ ↦ c), then ENNReal.tsum_add and ENNReal.tsum_le_tsum.