OAI/Geometry/RCD/Transport/ComponentScalarMidpoint.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Scalar reduced midpoint bounds for actual length components

The component length bound, rather than the parent diameter, appears in both half estimates. Normalization cancels exactly. Midpoint maximality is inherited from the parent and is not postulated for the component.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.component_scalar_midpoints line 22