FlatCellChainPropagation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Flatness propagation along cell chains

A flat initial cell and oscillation bounds on its ancestors control bilateral beta at every descendant center. Six binary steps correspond to one lattice depth; nearby-ball transfer provides the intervening dyadic bounds required by flat-seed propagation.

theorem OAI.RieszRectifiability.exists_uniform_flat_cell_chain_propagation line 24