SourceDensityForest.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Density witnesses generate an actual finite keeper forest. The disjointness, area budget, angular nesting and enlarged spatial assignment are conclusions of the selection, not assumptions on the forest.

theorem OAI.LipschitzHilbert.exists_dyadic_density_forest line 13