Sphere Rigidity | Exact Mathematics

MathlibAnnex / Selected reading scope

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.

75 approved Cards in this selected reading scope. The catalog contains 188 distinct Cards across the four Projects.

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 mathematical routes.

Scope limits

The ambient spaces are real, and at least one is finite-dimensional. The conclusion is the existence of a linear isometry equivalence. This result does not assert that a specified sphere isometry extends linearly. The selected Cards retain their recorded formal-source qualification and document-correspondence boundaries.

Mathematical routes

A surjective isometry between unit spheres first gives a radial map and transfers finite-dimensionality. Boundary-integral and orientation arguments then identify the Plücker bodies associated with the two norms. Determinant-maximizing frames, finite support selections and maximal-minor factorization provide linear recovery; a limiting and ball-volume argument yields an ambient linear isometry. This is an existence statement and does not claim that the prescribed sphere isometry extends linearly.

Each route shows its direct Cards and the reused prerequisites needed in the selected reading graph. Shared Cards count once within each route and once in the Catalog.

Radial extension and dimension transfer

A surjective isometry between unit spheres produces a radial map and transfers finite-dimensionality between the ambient spaces. The radial map has the recorded metric bounds; it is not asserted to be linear or globally isometric.

7 direct Cards + 0 reused prerequisites = 7 unique Cards. Shared Cards count once in this route.

Key result: Isometric unit spheres force equal finite dimensions
Key definition: Radial extension of an isometry between unit spheres

Read this route with prerequisites

Compact hulls and support-face selection

Compact hulls and support faces provide successive finite refinements and a common generator. The sets need not themselves be convex; nonemptiness and the stated finite-dimensional hypotheses remain in the individual Cards.

4 direct Cards + 0 reused prerequisites = 4 unique Cards. Shared Cards count once in this route.

Key result: A common generator selected from equal convex hulls
Key definition: Successive maximum refinement by an ordered list of functionals

Read this route with prerequisites

Determinants and maximal-minor factorization

Determinant differences and maximal minors turn coordinate changes into controlled algebraic data. Cramer coordinates and the uniqueness of a right factor will later translate matching minor vectors into a linear map.

7 direct Cards + 2 reused prerequisites = 9 unique Cards. Shared Cards count once in this route.

Key result: A unique right factor from proportional oriented maximal minors
Key result: Cramer’s rule for coordinates of a row

Read this route with prerequisites

Piola identities and boundary integrals

Mollification, the Piola identity and determinant telescoping give integral identities for compact perturbations. Strong local convergence then passes to Lipschitz maximal minors, whose integrals are determined by boundary agreement.

10 direct Cards + 1 reused prerequisite = 11 unique Cards. Shared Cards count once in this route.

Key result: Boundary agreement determines maximal-minor integrals
Key result: The divergence-free cofactor identity

Read this route with prerequisites

Zero weak gradients and constancy

The weak equation makes local mollifications constant, giving local almost-everywhere constancy of the original function. Overlap and countable gluing arguments give global almost-everywhere constancy on an open preconnected domain. The separate continuous case upgrades this to pointwise constancy.

10 direct Cards + 0 reused prerequisites = 10 unique Cards. Shared Cards count once in this route.

Key result: Global almost-everywhere constancy on a preconnected domain
Continuous case: A continuous function with zero weak gradient is constant

Read this route with prerequisites

Orientation and signed Jacobian transfer

Metric inverse bounds and the absolute Jacobian formula provide signed transfer. A weak Piola identity shows that the transported sign has zero weak gradient; on a preconnected target the sign is almost everywhere constant and the signed integral is that sign times target volume.

7 direct Cards + 19 reused prerequisites = 26 unique Cards. Shared Cards count once in this route.

Key result: The signed Jacobian integral is a sign times target volume
Key result: The transported Jacobian sign has zero weak gradient

Read this route with prerequisites

Determinant-maximizing frames and finite recovery

An attained positive determinant maximum supplies well-conditioned dual frames. Weighted satellite arguments and a finite almost-norming family control the vectors needed for approximate linear recovery; the exact lower-unit condition remains explicit.

11 direct Cards + 1 reused prerequisite = 12 unique Cards. Shared Cards count once in this route.

Key result: A finite absolute-maximizing family almost norms the unit sphere
Key result: A common inverse estimate from row Cramer

Read this route with prerequisites

Absolute volume and ball rigidity

The absolute Jacobian integral of the radial map yields target-ball volume. A limiting linear contraction has the exact determinant-volume scaling between the two unit balls. Ball inclusion and strict compact-subset volume comparison give ball equality; the separate ball-equality result then gives norm preservation.

5 direct Cards + 28 reused prerequisites = 33 unique Cards. Shared Cards count once in this route.

Key result: The recovered contraction maps one unit ball onto the other
Key result: Equality of seminorm balls under a linear bijection preserves the seminorms

Read this route with prerequisites

Plücker bodies and linear isometry recovery

Boundary integrals and a common orientation compare the Plücker bodies of the two norms. Support slices, generator matching and maximal-minor factorization give approximate linear recovery, then the limiting volume argument gives an ambient linear isometry. This existence conclusion does not assert extension of a specified sphere isometry.

14 direct Cards + 57 reused prerequisites = 71 unique Cards. Shared Cards count once in this route.

Key result: The unit-sphere chord metric determines the ambient normed space
Key result: All Plücker bodies determine the norm up to linear isometry

Read this route with prerequisites

Dependency-first reading route

Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.

Search Cards Route 75 Cards

Level 0 (21 Cards)

Level 0

Radial extension of an isometry between unit spheres

Extends a bijective sphere isometry to all vectors by retaining each radius and transporting its unit direction.

MathlibAnnex.Sphere.radialExtension

Immediate Card prerequisites: None in this selected scope

Used by in this scope: The inverse sphere isometry gives the inverse radial map · The radial extension is 3-Lipschitz

The mathematical goal

Scope

Scope limits

Mathematical routes

Radial extension and dimension transfer

Compact hulls and support-face selection

Determinants and maximal-minor factorization

Piola identities and boundary integrals

Zero weak gradients and constancy

Orientation and signed Jacobian transfer

Determinant-maximizing frames and finite recovery

Absolute volume and ball rigidity

Plücker bodies and linear isometry recovery

Dependency-first reading route

Level 0 (21 Cards)

Radial extension of an isometry between unit spheres

A seminorm with two-sided bounds against a reference norm

Successive maximum refinement by an ordered list of functionals

A support face is the convex hull of the maximizing generators

The convex hull of a compact set in a finite real coordinate space

The family of maximal minors in increasing row order

A determinant difference bound in the sup operator norm

Cramer’s rule for coordinates of a row

Mollification by a normalized smooth kernel

A cofactor row by row replacement

Zero integral of a compactly supported divergence

Gluing one almost-everywhere constant over a countable cover

Divergence as the trace of a derivative

Identifying constants on an open overlap

Differentiating a local mollification through its kernel

Inverse maps on open sets with global metric bounds

A weighted determinant polynomial with satellites

An attained absolute determinant maximum

A compact proper subset of a seminorm ball has smaller Haar measure

Equality of seminorm balls under a linear bijection preserves the seminorms

A seminorm increment bound passes to every derivative direction

Level 1 (20 Cards)

Continuous linear maps bounded by a seminorm

The radial extension is 3-Lipschitz

The inverse sphere isometry gives the inverse radial map

A common generator selected from equal convex hulls

The satellite polynomial is linear in the maximal-minor vector

Maximal minors scaled by the reference ball volume

A unique right factor from proportional oriented maximal minors

Right multiplication scales every maximal minor by one determinant

Strong local convergence of mollified derivatives

The divergence-free cofactor identity

Determinant integrals under strong convergence

Vanishing weak gradient tested by divergence

From local to global almost-everywhere constancy

A positive lower metric bound passes to the derivative

Absolute maximization forces a near-maximal base

Positivity of the determinant maximum

A strict lower bound on a norm’s unit sphere

The set of near-maximal dual frames

A nearby norming point gives an almost-norming evaluation

The recovered contraction maps one unit ball onto the other

Level 2 (11 Cards)

Isometric unit spheres force equal finite dimensions

Finite-dimensionality transfers across a sphere isometry

A component flux gives a determinant difference

Zero weak gradient gives zero derivatives of local mollifications

Signed transfer from the absolute Jacobian formula

A common inverse estimate from row Cramer

Each satellite norms its coefficient preimage in absolute value

The absolute Jacobian integral of a radial sphere extension

Compactness of the signed generator set

The set average of derivative generators

The symmetric convex body of contraction minors

Level 3 (4 Cards)

Smooth compact perturbations preserve the determinant integral difference

Local almost-everywhere constancy from the weak equation

One fixed satellite family almost norms every detected unit vector

The average of contractive derivative generators lies in the body

Level 4 (5 Cards)

Maximal-minor integral differences for Lipschitz perturbations

Global almost-everywhere constancy on a preconnected domain

A finite absolute-maximizing family almost norms the unit sphere

One boundary extension with all five analytic properties

The chosen support slice consists of almost-isometric generators