LengthReplacementSeparation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Length-preserving replacements remain separated from untouched mass

Fixing one interior component marginal preserves its length class. Every other interior marginal of that replacement is therefore singular to the untouched complementary component. This supplies the geometric premise of the proved Rényi subplan comparison.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.length_replacement_separated line 20