Absolute volume and ball rigidity

Scope

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. This count is a selected Card closure, not a source-declaration count.

Route reading PDF · Preserved source exploration

Cards 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

Reference index: direct Cards and reused prerequisites

Direct references: SR168 — A compact proper subset of a seminorm ball has smaller Haar measure · SR170 — Equality of seminorm balls under a linear bijection preserves the seminorms · SR399 — The absolute Jacobian integral of a radial sphere extension · SR356 — A volume-normalized linear contraction obtained by a limit · SR358 — The recovered contraction maps one unit ball onto the other

Reused prerequisites: SR302 — The chosen support slice consists of almost-isometric generators · SR328 — The satellite polynomial is linear in the maximal-minor vector · SR081 — Successive maximum refinement by an ordered list of functionals · SR098 — Compactness of the signed generator set · SR406 — The family of maximal minors in increasing row order · SR392 — The inverse sphere isometry gives the inverse radial map · SR093 — The symmetric convex body of contraction minors · SR425 — Cramer’s rule for coordinates of a row · SR387 — Radial extension of an isometry between unit spheres · SR230 — A common inverse estimate from row Cramer · SR264 — A seminorm with two-sided bounds against a reference norm · SR235 — A weighted determinant polynomial with satellites · SR325 — A strict lower bound on a norm’s unit sphere · SR263 — A finite absolute-maximizing family almost norms the unit sphere · SR086 — A common generator selected from equal convex hulls · SR253 — Absolute maximization forces a near-maximal base · SR272 — Continuous linear maps bounded by a seminorm · SR297 — A determinant difference bound in the sup operator norm · SR439 — Maximal minors scaled by the reference ball volume · SR258 — One fixed satellite family almost norms every detected unit vector · SR394 — The radial extension is 3-Lipschitz · SR216 — The set of near-maximal dual frames · SR190 — An attained absolute determinant maximum · SR207 — Positivity of the determinant maximum · SR077 — A support face is the convex hull of the maximizing generators · SR365 — Almost-contractive linear recovery with exact volume scaling · SR255 — Each satellite norms its coefficient preimage in absolute value · SR257 — A nearby norming point gives an almost-norming evaluation

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 33 Cards

Level 0 (11 Cards)

Level 0

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

Finds a nonempty open part of the missing set and uses finiteness of the compact set to make the measure comparison strict.

MathlibAnnex.SeminormBall.measure_lt

Immediate Card prerequisites: None in this selected scope

Used by in this scope: The recovered contraction maps one unit ball onto the other

Scope

Cards in this route

Dependency-first reading route

Level 0 (11 Cards)

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

Equality of seminorm balls under a linear bijection preserves the seminorms

A weighted determinant polynomial with satellites

The family of maximal minors in increasing row order

A determinant difference bound in the sup operator norm

Successive maximum refinement by an ordered list of functionals

Cramer’s rule for coordinates of a row

Radial extension of an isometry between unit spheres

A support face is the convex hull of the maximizing generators

A seminorm with two-sided bounds against a reference norm

An attained absolute determinant maximum

Level 1 (12 Cards)

The recovered contraction maps one unit ball onto the other

Absolute maximization forces a near-maximal base

Positivity of the determinant maximum

Continuous linear maps bounded by a seminorm

A strict lower bound on a norm’s unit sphere

The satellite polynomial is linear in the maximal-minor vector

Maximal minors scaled by the reference ball volume

The set of near-maximal dual frames

The radial extension is 3-Lipschitz

The inverse sphere isometry gives the inverse radial map

A nearby norming point gives an almost-norming evaluation

A common generator selected from equal convex hulls

Level 2 (5 Cards)

The absolute Jacobian integral of a radial sphere extension

A common inverse estimate from row Cramer

Compactness of the signed generator set

The symmetric convex body of contraction minors

Each satellite norms its coefficient preimage in absolute value

Level 3 (1 Card)

One fixed satellite family almost norms every detected unit vector

Level 4 (2 Cards)

A finite absolute-maximizing family almost norms the unit sphere

The chosen support slice consists of almost-isometric generators

Level 5 (1 Card)

Almost-contractive linear recovery with exact volume scaling

Level 6 (1 Card)

A volume-normalized linear contraction obtained by a limit