Sphere Rigidity | MathlibAnnex Project

MathlibAnnex / Progressive Research Companion

The mathematical goal

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: MathlibAnnex v0.4.0 Project entry · Source manifest

Declaration Cards are in preparation. These 467 current-source tiles preserve the existing Project scope; route presets remain inactive because exact terminal metadata has not been owner-adopted.

Scope

Finite-dimensional real normed spaces and surjective isometries between their unit spheres, with the theorem stated when at least one ambient space is finite-dimensional. The formalization includes radial extension, dimension transfer, determinant and Pluecker methods, analytic orientation tools, finite recovery, and ball-volume rigidity used in the proof architecture.

Scope limits

This Research Companion describes exact formal source and dependency structure. It does not assert completed Declaration Cards, document correspondence, or public LFH review.

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

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

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

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

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

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

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

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

R09 · Determinant Factorization

A factorization route from proportional maximal minors, retained as a heavy-refactor proof seed rather than an independently completed tool. Scale, sign, row order, and nondegeneracy conditions remain explicit to prevent degenerate overgeneralization.

20 selected declarations

Boundary Inputs

3439 exact Boundary Inputs: EXTERNAL_COMPILED_DECLARATION 2632, OMITTED_INTERNAL_NATIVE_DECLARATION 807. Selected reachability is retained through every omitted internal declaration.

Inspect Boundary Inputs

Real — Compiled external provider used by selected Project declarations.
Nat — Compiled external provider used by selected Project declarations.
Eq — Compiled external provider used by selected Project declarations.
OfNat.ofNat — Compiled external provider used by selected Project declarations.
Real.normedField — Compiled external provider used by selected Project declarations.
NormedAddCommGroup.toSeminormedAddCommGroup — Compiled external provider used by selected Project declarations.
Real.semiring — Compiled external provider used by selected Project declarations.
Semiring.toNonAssocSemiring — Compiled external provider used by selected Project declarations.
DFunLike.coe — Compiled external provider used by selected Project declarations.
UniformSpace.toTopologicalSpace — Compiled external provider used by selected Project declarations.
PseudoMetricSpace.toUniformSpace — Compiled external provider used by selected Project declarations.
NormedAddCommGroup.toAddCommGroup — Compiled external provider used by selected Project declarations.
id — Compiled external provider used by selected Project declarations.
NormedSpace.toModule — Compiled external provider used by selected Project declarations.
NormedAddCommGroup — Compiled external provider used by selected Project declarations.

Dependency-first reading route

Levels belong to this Project. Select a level or follow a relation to another declaration tile.

Search declarations Route 467 declarations

Level 0

46 declarations

Level 0R05Focus target

AEConstantOn

MathlibAnnex.AEConstantOn

Mathematical construction

Immediate prerequisites in this Project
None in this Project

Used by in this Project
targetJacobianSign_const_is_pm_one, compactLocalization_aeConstant_inner, aeConstantOn_of_countableCover

Show 2 more

The mathematical goal

Scope

Scope limits

Proof architecture

R01 · Radial Extensions and Dimension

R02 · Compact Convex Hulls and Support Faces

R03 · Determinant Methods

R04 · Piola Identity and Null Lagrangians

R05 · Weak Gradient Zero and A.E. Constancy

R06 · Orientation and Signed Jacobians

R07 · Determinant-Maximizing Dual Frames

R08 · Sphere-Volume Rigidity

R09 · Determinant Factorization

Boundary Inputs

Dependency-first reading route

Level 0

AEConstantOn

BiLipschitzOpenData

volume_image_eq_zero_of_lipschitzWith

CompactC1VectorField

Frame

NearMaxInverseBound

coordinateEquiv

functionalCoordinates

unitRowSet

EquivalentSeminorm

norm_apply_le_seminorm_of_lipschitz

satelliteAmbientDim

LocalAEConstantAt

MaximalMinorIndex

chartFactor

det_smul_vecMul_nonsingInv_eq_updateRowDet

exists_orderEmbedding_perm_of_injective

orientedMaximalMinor

rowL1Norm

submatrix_update_rowTuple

StrongLnOperatorField

lipschitz_fderiv_memLpOn_compact

standardMollifier

maximizer

basisRow

coordinateDivergence

det_updateRow_finset_sum

exists_open_box_containing_compact

outputHybrid

sum_symmetric_mul_antisymmetric_eq_zero

FiniteCoefficientNet

SatelliteRows

abs_affine_endpoint_rigidity

coefficientAnnulus

interior_sdiff_nonempty

map_le

isometryEquiv_of_linearIsometryEquiv

normalizeToSphere

scaled_normalize_dist_le_two

LocalBallData

compactLocalization

shrinkingBump

coordinate

divergence

isCompact_convexHull_pi

trace_smulRight

Level 1

f_injective

lipschitz_f

lipschitz_g

domainJacobianSign

fderiv_lower_bound

target_exceptional_null

carrier

contDiff

hasCompactSupport

ofSupport

K_nonneg

frameCoordinates

frameMap

frameMatrix

functional_apply_eq_sum

inverseCoordinateMap

unitRowSet_isCompact