OAI/Geometry/RCD/Coordinates/NormalizedSubplanNodes.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Bounded transport nodes for the actual normalized length components

Uniform compression of the parent controls both half-nodes. Their transport-distance bounds are inherited at exactly half the parent scale.

  1. theorem OAI.RegularPointCoordinates.exists_normalized_subplan_half_nodes line 20