This Project view is available with the MathlibAnnex v0.2.0 source. Public Declaration Cards: 0. Mathematical review scope is recorded in the Project.
Read PDF · Project JSON · Presentation binding
Sphere Rigidity
If at least one of two real normed spaces is finite-dimensional, their unit spheres are isometric in the chord metric exactly when the ambient spaces are linearly isometric. Equivalently, a surjective unit-sphere isometry yields a linear isometry equivalence of the ambient spaces under that finite-dimensional hypothesis.
Exact source and release details
MathlibAnnex v0.2.0, commit 30963f26ac8ffa3dc3e9ec9de91fd0f9daf05305, tree b3378851a5287f5e3c8418f668e4d0ba52718739. Project entry · Project Source Manifest.
Goal-first proof architecture
R01 - Radial Extensions and Dimension
Radial extension of sphere isometries and transfer of finite-dimensional information. The route does not claim that the radial extension is linear or globally isometric; the recorded 3-Lipschitz bound is the source constant, not an optimality claim.
16 selected declarations; a route grouping, not a separate Route Project.
R02 - Compact Convex Hulls and Support Faces
Compact hulls, support faces, and finite lexicographic selection. The raw sets need not themselves be convex, nonemptiness is explicit, and finite-dimensional hypotheses appearing in the exact source are preserved.
27 selected declarations; a route grouping, not a separate Route Project.
R03 - Determinant Methods
Maximal-minor and determinant estimates with fixed row-order and sign conventions. Ordered row embeddings are not conflated with unordered row sets, and displayed bounds are not silently reinterpreted as Euclidean operator-norm statements.
24 selected declarations; a route grouping, not a separate Route Project.
R04 - Piola Identity and Null Lagrangians
Piola-type identities, null Lagrangians, determinant continuity, and boundary traces. The whole-space perturbation identity concerns the integral of the determinant difference; Strong L^n includes eventual integrability, and the trace used here is pointwise on the sphere.
33 selected declarations; a route grouping, not a separate Route Project.
R05 - Weak Gradient Zero and A.E. Constancy
Weak gradient zero implies local and global almost-everywhere constancy, not pointwise constancy. Compact C1 test fields and divergence form the shared analytic base used by the orientation route.
14 selected declarations; a route grouping, not a separate Route Project.
R06 - Orientation and Signed Jacobians
Orientation and signed Jacobians on connected domains. No single global sign is asserted on a disconnected domain, and the null-image statement retained here is the same-dimension version present in the exact source.
0 selected declarations; a route grouping, not a separate Route Project.
R07 - Determinant-Maximizing Dual Frames
Determinant-maximizing dual frames and inverse bounds, including the zero-dimensional case. Mathlib providers are preferred for norming functionals; application-specific satellite-polynomial material remains provenance rather than a new public API claim.
61 selected declarations; a route grouping, not a separate Route Project.
R08 - Sphere-Volume Rigidity
Sphere-volume and ball-image rigidity. Compactness and inclusion in the relevant ball are explicit; equality of volume alone is not used to infer equality of sets without the separate inclusion hypothesis.
7 selected declarations; a route grouping, not a separate Route Project.
R09 - Determinant Factorization
A factorization route from proportional maximal minors, presented as a proof outline rather than an independently completed tool. Scale, sign, row order, and nondegeneracy conditions remain explicit to prevent degenerate overgeneralization.
20 selected declarations; a route grouping, not a separate Route Project.
Boundary Inputs
The exact provider ledger contains 2,885 dependencies. The curated reader-facing projection contains 591 mathematically relevant boundary declarations; these are not project-local level nodes.
| Mathematical role | Count |
|---|---|
| Measure Theory | 146 |
| Normed Space Geometry | 129 |
| Continuous Linear Maps | 75 |
| Matrix Linear Algebra | 48 |
| Seminormed Geometry | 46 |
| Differential Calculus | 42 |
| Compactness Topology | 36 |
| Determinant Algebra | 22 |
| Convex Geometry | 12 |
| Isometry And Metric Geometry | 11 |
| Finite Dimensional Linear Algebra | 9 |
| Lipschitz Analysis | 9 |
| Sphere Geometry | 2 |
| Topological Equivalence | 2 |
| Integration | 1 |
| Volume And Measure | 1 |
Representative high-use inputs
Real.normedField - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Field.Basic
Boundary reference (no public Card link); routes: R01, R02, R04, R05, R07, R08.
Real.normedCommRing - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Ring.Basic
Boundary reference (no public Card link); routes: R02, R03, R04, R05, R07, R08.
NormedAddCommGroup.toSeminormedAddCommGroup - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Normed.Group.Defs
Boundary reference (no public Card link); routes: R01, R02, R04, R05, R07, R08.
NormedCommRing.toSeminormedCommRing - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Normed.Ring.Basic
Boundary reference (no public Card link); routes: R02, R03, R04, R05, R07, R08.
NonUnitalSeminormedRing.toSeminormedAddCommGroup - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Normed.Ring.Basic
Boundary reference (no public Card link); routes: R02, R03, R04, R05, R07.
NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Normed.Ring.Basic
Boundary reference (no public Card link); routes: R02, R03, R04, R05, R07.
SeminormedCommRing.toNonUnitalSeminormedCommRing - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Normed.Ring.Basic
Boundary reference (no public Card link); routes: R02, R03, R04, R05, R07.
InnerProductSpace.toNormedSpace - Normed Space Geometry
MATHLIB / Mathlib.Analysis.InnerProductSpace.Defs
Boundary reference (no public Card link); routes: R02, R03, R04, R07.
Real.normedAddCommGroup - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Group.Real
Boundary reference (no public Card link); routes: R02, R04, R07, R08.
NormedAddCommGroup.toAddCommGroup - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Group.Defs
Boundary reference (no public Card link); routes: R01, R02, R04, R05, R07, R08.
Pi.normedSpace - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Module.Basic
Boundary reference (no public Card link); routes: R02, R03, R04, R07.
NormedSpace.toModule - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Module.Basic
Boundary reference (no public Card link); routes: R01, R02, R04, R05, R07, R08.
Pi.normedAddCommGroup - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Group.Constructions
Boundary reference (no public Card link); routes: R02, R04.
SeminormedAddCommGroup.toPseudoMetricSpace - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Normed.Group.Defs
Boundary reference (no public Card link); routes: R01, R02, R04, R05, R07, R08.
ContinuousLinearMap - Continuous Linear Maps
MATHLIB / Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Boundary reference (no public Card link); routes: R02, R03, R04, R07.
NormedAddCommGroup - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Group.Defs
Boundary reference (no public Card link); routes: R01, R02, R05, R07, R08.
NormedSpace - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Module.Basic
Boundary reference (no public Card link); routes: R01, R02, R05, R07, R08.
SeminormedCommRing.toSeminormedRing - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Normed.Ring.Basic
Boundary reference (no public Card link); routes: R03, R04, R07, R08.
ContinuousLinearMap.funLike - Continuous Linear Maps
MATHLIB / Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
Boundary reference (no public Card link); routes: R02, R04, R07.
Seminorm - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Seminorm
Boundary reference (no public Card link); routes: R08.
Seminorm.instFunLike - Seminormed Geometry
MATHLIB / Mathlib.Analysis.Seminorm
Boundary reference (no public Card link); routes: R08.
Norm.norm - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Group.Defs
Boundary reference (no public Card link); routes: R01, R03, R04, R07, R08.
DenselyNormedField.toNontriviallyNormedField - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Field.Basic
Boundary reference (no public Card link); routes: R01, R03, R04, R07.
Real.denselyNormedField - Normed Space Geometry
MATHLIB / Mathlib.Analysis.Normed.Field.Basic
Boundary reference (no public Card link); routes: R01, R03, R04, R07.
Dependency-first declaration route
467 declarations shown.
Graph, levels and Boundary Input records
Project levels · Display graph · Canonical reachability · Boundary Inputs · Route memberships
These machine-readable records retain their exact source and provider bindings. Historical workflow fields in those records do not describe the publication state of this Project view.