This Project links eleven completed, reviewed canonical Declaration Cards. The route below is dependency-first; Cards remain independent library records.
The result
An isometry equivalence from an open connected subset onto an open subset of real normed spaces extends uniquely to an affine isometry equivalence of the ambient spaces. The selected route also reaches convex-domain and ball specializations.
Why it matters
Local distance information becomes a rigid affine structure. This Project exposes the reusable chain from reflection and midpoint geometry to global extension.
Hypotheses
Real normed spaces and an isometry equivalence. The principal theorem requires an open connected source and an open target. The convex specialization requires a convex source set with nonempty ambient interior and exact preservation of ambient-interior membership; the target set is not separately assumed convex. Exact assumptions, including radius conditions for balls, remain in the linked exact declarations.
Scope
The eleven declaration explanations are reviewed for source-exposition correspondence. This does not claim a line-by-line human proof audit. Boundary Inputs include Lean Core, Mathlib, and omitted MathlibAnnex support declarations.
Dependency-first Card route
Level 0: Center transport under bounded point-reflection symmetry
Identifies the distinguished centers of two bounded reflection-invariant subsets under an isometry equivalence.
Immediate prerequisites: None in the reduced Project graph
Level 0: Symmetric lens
Names the reflection-symmetric bounded region used to force preservation of a midpoint.
Immediate prerequisites: None in the reduced Project graph
Level 1: Midpoint preservation on a symmetric lens
Turns bounded reflection symmetry of equal-radius lenses into midpoint preservation.
Immediate prerequisites: Center transport under bounded point-reflection symmetry, Symmetric lens
Level 2: Midpoint preservation under lens containment
Applies the symmetric-lens midpoint theorem inside arbitrary source and target subsets.
Immediate prerequisites: Midpoint preservation on a symmetric lens
Level 3: Midpoint preservation on a quarter ball
Obtains a uniform local midpoint law from symmetric-lens center rigidity.
Immediate prerequisites: Midpoint preservation under lens containment
Level 4: Affine-segment preservation on a quarter ball
Upgrades local midpoint preservation to preservation of every affine segment parameter inside the quarter-ball chart.
Immediate prerequisites: Midpoint preservation on a quarter ball
Level 5: Local affine-isometry chart on a smaller ball
Constructs the local ambient affine chart used in the gluing proof for open connected domains.
Immediate prerequisites: Affine-segment preservation on a quarter ball
Level 6: Mankiewicz extension on open connected domains
Glues local affine-isometry charts to obtain the principal open-domain extension theorem.
Immediate prerequisites: Local affine-isometry chart on a smaller ball
Used by: Convex-set extension via ambient interiors, Affine extension from open balls
Level 7: Affine extension from open balls
Derives the open-ball form of the Mankiewicz extension theorem from the open-connected-domain theorem.
Immediate prerequisites: Mankiewicz extension on open connected domains
Used by: None in the reduced Project graph
Level 7: Convex-set extension via ambient interiors
Transfers the open-connected extension theorem to convex sets whose ambient interiors are matched exactly by the isometry.
Immediate prerequisites: Mankiewicz extension on open connected domains
Level 8: Affine extension from equal-radius closed balls
Extends an isometry of closed balls by first recovering the centers and then passing through the convex-interior extension theorem.
Immediate prerequisites: Convex-set extension via ambient interiors
Used by: None in the reduced Project graph
Exact bindings
Accepted selected-Card graph · Accepted levels · Accepted Boundary Inputs · Boundary view
Source release: MathlibAnnex v0.2.0 Project entry. Presentation binding.