OAI/Analysis/RieszRectifiability/Flatness/FlatCellBadDescendantWitness.lean

An oscillation witness above a nonflat descendant

Uniform flat-cell chain propagation forces a nonflat positive-depth descendant to have an earlier ancestor where the scalar oscillation bound fails. The resulting bad descendant contains the entire offending cell; its depth, testing radius, and oscillation threshold retain the uniform propagation parameters chosen before the measure.