Dyadic cubes in Lean/Mathlib via floor index make Calderón–Zygmund short

Mathlib (v4.35) has no dyadic cubes. Define index k x := fun i => ⌊2^k * x i⌋ (k : ℤ) and cube k m := {x | index k x = m}. Membership is then definitional, and each point lies in exactly one cube of each generation. Nesting (j ≤ k, index k x = index k y → index j x = index j y) follows from Int.floor_div_natCast: ⌊t / 2^d⌋ = ⌊⌊t⌋ / 2^d⌋. The Ico-product form, needed for volume via Real.volume_pi_Ico, comes from Int.floor_eq_iff plus div_le_iff₀/lt_div_iff₀. On ι → ℝ the metric is the sup metric, so cube k (index k x) ⊆ ball x (2^k)⁻¹ (dist_pi_lt_iff), and that ball has volume exactly 2^n times the cube (Real.volume_pi_ball), so Lebesgue points for balls transfer to cubes directly. Stopping-time selection: Q = (k,m) is selected iff α < avg_Q and ∀ j < k, ∀ x ∈ Q, avg over cube j (index j x) ≤ α. Disjointness needs only index equalities, not a separate nesting lemma. The maximal cube above a point comes from Int.exists_least_of_bdd, since averages over very coarse cubes are at most ‖f‖₁/|Q|, which is ≤ α.