2a2a175
THE SYMMETRIC MAHLER CONJECTURE AND ITS EQUALITY CASES
A complete proof, written to be read with pencil and paper


================================================================
CONTENTS
================================================================

    0. What the theorem says
    1. Background: convex bodies, polarity, Hanner polytopes
    2. The lens: a conformal map with a uniform boundary law
    3. The holomorphic mass lemma
    4. Feasible bases: a probability that is always at least 1
    5. Extra boundary hits are null
    6. The real simplex identity (the main inequality)


================================================================
0. WHAT THE THEOREM SAYS
================================================================

Let n >= 1. A convex body in R^n is a compact convex set with nonempty
interior. Write K = -K for "origin-symmetric"; then the origin lies in
the interior of K.

The polar body of K is
    K° = { y in R^n : x·y <= 1 for every x in K }.
It is again a convex body with 0 in its interior. The volume product is
    P(K) = |K| · |K°|,
where |·| always means the n-dimensional volume.

For an invertible linear map T : R^n -> R^n,
    (TK)° = T^{-T} K°    and    P(TK) = P(K).
The two factors of |det T| cancel. So P is a linear invariant: it only
sees the shape of K, not its coordinates.

MAHLER'S SYMMETRIC PROBLEM: How small can P(K) become?

HANNER POLYTOPES are constructed recursively.
  * In dimension 1, a Hanner polytope is a centered interval [-a, a],
    a > 0.
  * Given Hanner polytopes H_1 in R^k and H_2 in R^l, both of the
    following are Hanner polytopes in R^{k+l}:
        H_1 ⊕_∞ H_2  =  H_1 × H_2            (Cartesian product;
                                              the ℓ_∞ sum)
        H_1 ⊕_1 H_2  =  conv((H_1 × {0}) ∪ ({0} × H_2))   (the ℓ_1 sum).

A "linear Hanner body" is any invertible linear image of a Hanner poly-
tope. Examples include the cube [-1,1]^n, the cross-polytope
{ y : |y_1| + ... + |y_n| <= 1 }, and every mixed ℓ_1/ℓ_∞ sum.

MAIN THEOREM (Symmetric Mahler, with equality cases).
For every integer n >= 1 and every origin-symmetric convex body K in R^n,
    |K| · |K°|  >=  4^n / n!.
Equality holds if and only if K is a linear Hanner body.

SANITY CHECK. The cube Q_n = [-1,1]^n has volume 2^n. Its polar is the
cross-polytope C_n = { y : |y_1| + ... + |y_n| <= 1 }, whose volume is
2^n / n!. So P(Q_n) = 4^n / n!. The cube is among the extremal bodies,
as expected. Its polar is another.

STRATEGY OF THE PROOF.

  (A) In Part 1 we prove the two norm-sum formulas and show every Hanner
      body attains exactly 4^d / d!.

  (B) In Part 2 we build a special conformal map F from the unit disk to
      a bounded convex "lens" region D. On the boundary of D, uniform
      angle on the disk becomes a uniform coordinate on [-1,1]. This
      coordinate change is what turns the complex analysis into real
      geometry.

  (C) In Part 3 we prove the holomorphic mass lemma: at an isolated zero
      of a holomorphic map, the Jacobian minors have a sharp lower
      bound (pi k)^d / d!, where k is the order of the zero.

  (D) In Part 4 we push that bound through finitely many real strip
      constraints. The output is that a certain sum S of "feasibility
      probabilities" is always at least 1.

  (E) In Part 6 we reinterpret S as a real integral over the primal body.
      That identity forces |A||A°| >= 4^d / d! for polytopes A. Part 7
      approximates arbitrary K by polytopes.

  (F) For the equality case, in Part 8 we lift K by one dimension (K ->
      K ⊕_1 [-1,1]). The deficit goes to zero under inner approximation,
      and this yields an "optimal representation" of every nonzero vector.

  (G) In Part 9 we use that representation to produce a metric median in
      the polar norm for every triple of points. Metric medians imply the
      three-ball intersection property, and the Hansen-Lima theorem then
      classifies the norm as a Hanner sum (Part 10).

  (H) Part 11 derives two corollaries: the even functional Mahler
      inequality and the symmetric entropy-transport inequality.

Only three results are imported from the literature, each cited at the
point of use: Hansen-Lima (classification of 3.2-IP spaces), Fradelizi-
Meyer (functional Mahler), and Cordero-Erausquin-Klartag / Fradelizi-
Gozlan-Zugmeyer (entropy-transport, in Part 11 only).

Notation. R^n, C^d, R, C, Z. Euclidean inner product x·y. Volume |E|.
v ≤ w is componentwise not used. Sigma means sum over an indicated
range. "iff" = "if and only if". Higher-dimensional volume is context-
dependent; we write vol_{2d} for real 2d-dimensional volume when the
complex dimension d is clear from context.


================================================================
1. BACKGROUND: POLARITY AND HANNER POLYTOPES
================================================================

All bodies in this section are origin-symmetric convex bodies. For
such a body A, the gauge (= norm with unit ball A) and support function
are
    p_A(x) = inf { t > 0 : x in tA },
    h_A(y) = max { x·y : x in A }.

KEY DUALS. Convex separation gives A°° = A and
    p_A(x) = h_{A°}(x),      h_A(y) = p_{A°}(y).        (1.1)
Reason. x in tA iff (x/t)·y <= 1 for every y in A° iff x·y <= t for
every y in A°. Taking the inf over such t gives the claim.

INVARIANCE. For any invertible T,
    (TA)° = T^{-T} A°,        P(TA) = P(A).
Reason. y in (TA)° iff (Tx)·y <= 1 for all x in A iff x·(T^T y) <= 1 for
all x in A iff T^T y in A°, iff y in T^{-T}A°. Volumes: |TA| = |det T|·|A|
and |(TA)°| = |det T^{-T}|·|A°| = |A°|/|det T|. Product unchanged.

THE TWO SUMS. For A in R^k and A' in R^l,
    A ⊕_∞ A'  =  A × A'                          (in R^{k+l}),
    A ⊕_1 A'  =  conv( (A × {0}) ∪ ({0} × A') )  (in R^{k+l}).

Their gauges are
    p_{A⊕_∞ A'}(x, x') = max( p_A(x), p_{A'}(x') ),     (1.2)
    p_{A⊕_1 A'}(x, x') = p_A(x) + p_{A'}(x').           (1.3)

Proof of (1.3). The set A⊕_1 A' is generated by (a, 0) with a in A and
(0, a') with a' in A'. A convex combination with total weight t in [0,1]
has gauge at most t·? — more carefully, any (x, x') with
p_A(x) + p_{A'}(x') <= 1 is
    (x, x') = p_A(x)·(x/p_A(x), 0) + p_{A'}(x')·(0, x'/p_{A'}(x')),
where we suppress a zero coordinate (set that term to 0 if p = 0). This
is a convex combination of a point of A×{0} and a point of {0}×A',
of total weight p_A(x) + p_{A'}(x') <= 1. The reverse inequality follows
similarly. QED.

LEMMA 1.1 (Polars and volumes of the two sums).
For origin-symmetric convex bodies A in R^k, A' in R^l,
    (A ⊕_1 A')°  =  A° ⊕_∞ (A')°,                       (1.4)
    (A ⊕_∞ A')°  =  A° ⊕_1 (A')°,                       (1.5)
    |A ⊕_∞ A'|  =  |A| · |A'|,                          (1.6)
    |A ⊕_1 A'|  =  (k! l! / (k+l)!) · |A| · |A'|,       (1.7)
and consequently
    P(A ⊕_1 A')  =  P(A ⊕_∞ A')  =  P(A) P(A') / C(k+l, k).   (1.8)

Proof of polar identities. A functional y = (y_1, y_2) in (A⊕_∞ A')° iff
(x_1, x_2)·(y_1, y_2) <= 1 for all x_1 in A, x_2 in A'. That is
x_1·y_1 + x_2·y_2 <= 1 for all such x_1, x_2, i.e. y in A°⊕_1 (A')°.
Dualizing (bipolar) gives (1.4).

Proof of product volume (1.6). Fubini.

Proof of l_1 volume (1.7). For fixed x in A, the fiber of A⊕_1 A' over
x (that is, over (x, 0) extended by varying second coordinate) is
(1 - p_A(x))·A'. Hence
    |A ⊕_1 A'|  =  ∫_A (1 - p_A(x))^l · |A'| dx.

Since |{ x in A : p_A(x) <= t }| = t^k |A| for 0 <= t <= 1, integrate:
    ∫_A (1 - p_A)^l dx  =  ∫_0^1 (1-t)^l d(t^k |A|)
                        =  k |A| ∫_0^1 t^{k-1} (1-t)^l dt
                        =  k |A| · B(k, l+1)
                        =  |A| · k! l! / (k+l)!.
Here B(k, l+1) = (k-1)! l! / (k+l)! is the Beta function. Putting the two
pieces together gives (1.7).

Proof of volume product (1.8). Combine the polar and volume identities.
P(A ⊕_1 A') = [k! l!/(k+l)!] |A||A'| · |A° ⊕_∞ A'°| = [k! l!/(k+l)!] |A||A'|·|A°||A'°|.
Since C(k+l, k) = (k+l)!/(k! l!), we get P(A⊕_1 A') = P(A) P(A')/C(k+l,k).
The ⊕_∞ case is analogous. QED.

LEMMA 1.2 (Hanner volume product). Every d-dimensional linear Hanner
body H satisfies P(H) = 4^d / d!. Polars of Hanner bodies are Hanner
bodies.

Proof. Induction on d. Base case d = 1: H = [-a, a], H° = [-1/a, 1/a],
P = 2a · 2/a = 4 = 4^1 / 1!.
Inductive step. If H = H_1 ⊕_s H_2 with dim H_i = k_i, Lemma 1.1 gives
    P(H)  =  (4^{k_1}/k_1!) · (4^{k_2}/k_2!) / C(k_1+k_2, k_1)
          =  4^{k_1+k_2} / (k_1+k_2)!.
The polar formulas (1.4), (1.5) exchange ⊕_1 and ⊕_∞ and preserve the
1-D base case. Linear images of Hanner bodies are Hanner by definition
and preserve P. QED.

Dimension one. Every origin-symmetric convex body is a centered
interval. The sharp inequality and the equality classification in
dimension one are the base case above.

What is left to do. The rest of Parts 2 through 10 proves the
inequality in every dimension d, together with the classification of
equality. The cubes and cross-polytopes we saw are the simplest
Hanner bodies; the argument has to handle arbitrary symmetric bodies
A of arbitrary dimension.


================================================================
2. THE LENS: A CONFORMAL MAP WITH A UNIFORM BOUNDARY LAW
================================================================

This section builds a specific holomorphic map from the unit disk to a
planar convex region D. The map has three properties that we exploit
later: it is convex, D is a horizontal graph, and, most important, a
uniform angle on the circle maps to a uniform imaginary coordinate
on the boundary.

Write D_0 = { z in C : |z| < 1 } for the open unit disk. Define
    F(z)  =  (8 / pi^2) · Σ_{j>=0} (-1)^j z^{2j+1} / (2j+1)^2.   (2.1)
The series converges uniformly on the closed unit disk; the coefficients
are absolutely summable.

This F is a rotation of the uniform-distribution example in Gross's
conformal Skorokhod embedding (ECP 24, 2019, section 3.2). Here we
prove every property we need directly.

LEMMA 2.1 (The planar lens).
(i)  F is a biholomorphism from D_0 onto a bounded convex domain D,
     with inverse g, and F'(0) = 8/pi^2.
(ii) There is a continuous even function lambda : [-1, 1] -> [0, inf),
     positive on (-1, 1), zero at ±1, such that the closure of D is
         D̄  =  { v + i t : |t| <= 1,  |v| <= lambda(t) }.        (2.2)
(iii) lambda is smooth on (-1, 1), with
         lambda'(t)  =  -(2/pi) arctanh(sin(pi t / 2)),           (2.3)
         lambda''(t) =  -sec(pi t / 2)  <  0.                     (2.4)
     In particular lambda is strictly concave on (-1, 1).
(iv) If Theta is uniform on [0, 2 pi), then F(e^{i Theta}) has the same
     law as
         epsilon · lambda(T) + i T,
     where T is uniform on [-1, 1] and epsilon in {-1, +1} is an
     independent fair sign.

PROOF OF LEMMA 2.1.

Step 1 (derivatives via w = arctan z). Set
    w  =  arctan(z)  =  (1/(2i)) log((1+iz)/(1-iz)).
On the disk, the fraction (1+iz)/(1-iz) has positive real part (check:
1 + iz has positive real part, 1 - iz has positive real part, quotient
has positive real part on the open right half-plane). So we may use the
principal log, and w maps D_0 into the strip |Re w| < pi/4 with w = 0
only at z = 0. Also tan(w) = z.

Differentiate the power series term by term:
    (d/dz) Σ (-1)^j z^{2j+1} / (2j+1)^2  =  Σ (-1)^j z^{2j} / (2j+1)
                                         =  arctan(z) / z.
(For j >= 0 the derivative of z^{2j+1}/(2j+1)^2 is z^{2j}/(2j+1); the
sum is arctan(z)/z, the standard Taylor series.) Hence
    F'(z)  =  (8/pi^2) · w / z,                                 (2.5)
with w = w(z). In particular F'(0) = 8/pi^2 (limit as z -> 0, where
w/z -> 1).

Differentiating once more,
    1 + z F''(z) / F'(z)  =  sin(2w) / (2w).                    (2.6)
This follows from F'(z) = (8/pi^2) w/z and dw/dz = 1/(1+z^2); expanding
gives the identity. Write w = a + i b. Then
    Re (sin(2w)/(2w))  =  [a sin(2a) cosh(2b) + b cos(2a) sinh(2b)]
                            / (2(a^2 + b^2)),
which is strictly positive for |a| < pi/4, with limit 1 as w -> 0.
Reason: for |a| < pi/4, sin(2a) and a have the same sign, and
cos(2a) > 0; the b - terms have sign of b, and sinh(2b) has sign of b.
The sum is strictly positive whenever (a, b) != 0.

In particular, F'(z) != 0 for every z in D_0.

Step 2 (positive turning). For 0 < r < 1, set
gamma_r(theta) = F(r e^{i theta}).
The curve gamma_r is smooth and regular (F' nonzero on the compact
r-disc). Its tangent angle beta(theta) = arg(gamma_r'(theta)) satisfies
    beta'(theta)  =  Re (1 + z F''(z) / F'(z))  >  0,
    beta(theta + 2 pi)  =  beta(theta) + 2 pi.
The second line uses F' zero-free on the r-disk (so the winding number
of F' around 0 is 0 over a closed loop).

Now fix a parameter theta_0. Project gamma_r onto its OUTWARD unit
normal at gamma_r(theta_0). Since beta is monotone, if we follow
theta -> gamma_r(theta) around the loop, the projection first decreases
(until beta has advanced by pi) and then increases (until it returns).
So the projection takes its unique maximum at theta_0. Every point of
gamma_r is therefore the unique supporting point of gamma_r in its own
normal direction. In other words: gamma_r is a simple closed convex
curve, positively oriented.

Step 3 (univalence and convexity). Let D_r be the bounded convex region
enclosed by gamma_r. Maximum principle for the supporting projections
shows F(r D_0) lies strictly inside gamma_r. The argument principle gives
exactly one preimage in r D_0 for every point of D_r and none outside.
So F : r D_0 -> D_r biholomorphically for each 0 < r < 1.

As r increases, the D_r increase. Set D = union_r D_r = F(D_0). Then F
is univalent on D_0, D is convex, and its inverse g is holomorphic. For
each 0 < r < 1, continuity on the closed disk gives D_r-bar = F(r D_0-bar)
⊂ D. So D is bounded, D-bar = F(D_0-bar), and every boundary value
F(zeta), |zeta| = 1, lies on ∂D.

Step 4 (boundary computation). For z = e^{is} with -pi/2 < s < pi/2,
    (1 + iz)/(1 - iz)  =  i cos(s) / (1 + sin(s)).
Hence Re w = pi/4 and Im w = (1/2) arctanh(sin s). The formulas (2.5)
extend continuously across each compact subarc so we may differentiate
the boundary values. Writing F(e^{is}) = v(s) + i t(s),
    t'(s)  =  2 / pi,
    v'(s)  =  -(4 / pi^2) · arctanh(sin s).
With t(0) = 0 we get t(s) = 2s / pi. Define lambda : [-1, 1] -> R by
lambda(t) = v(pi t / 2). Then t(s) is a linear reparametrization of s,
and differentiating:
    lambda'(t)  =  -(2 / pi) · arctanh(sin(pi t / 2)),
    lambda''(t) =  -sec(pi t / 2) < 0.
Since F(±i) are purely imaginary by an oddness check, lambda(±1) = 0.
Conjugation gives lambda even. Strict concavity plus the endpoint zeros
make lambda > 0 on (-1, 1). Oddness and conjugation together show that
the opposite semicircle traces v = -lambda(t); combined with the
right-semicircle data, ∂D is the graph (2.2).

Step 5 (boundary coordinate law). On either semicircle, Im F traverses
[-1, 1] at constant absolute speed 2/pi. Hence a uniform angle on that
semicircle gives a uniform T in [-1, 1]. Each of the two semicircles
has probability 1/2, so we get an independent fair sign epsilon. With
this, F(e^{i Theta}) has the same distribution as epsilon·lambda(T) + iT.
QED.

LEMMA 2.2 (Endpoint scaling of the lens).
As eta decreases to 0,
    lambda(1 - eta)  =  (2/pi) · eta · log(1/eta)  +  O(eta).    (2.7)
Moreover, for every 0 < a <= b < inf,
    sup_{a <= c <= b} | lambda(1 - delta c)/lambda(1 - delta) - c |
       ->  0     as delta decreases to 0.                         (2.8)

Proof of (2.7). By lambda''(t) = -sec(pi t/2),
    lambda(1 - eta)  =  (2/pi) · ∫_0^eta  log cot(pi s / 4) ds.
The integrand log cot(pi s/4) = log(1/s) + O(1) as s -> 0 (standard
asymptotic for cot near 0). So
    lambda(1 - eta)  =  (2/pi) [eta log(1/eta) + O(eta)].

Proof of (2.8). Writing L = log(1/delta) and using the same asymptotic,
    lambda(1 - delta c)/lambda(1 - delta)
         =  c · (L - log c + O(1)) / (L + O(1))
         =  c + O_{a, b}(1/L),
uniformly for a <= c <= b, and the error vanishes as delta -> 0. QED.

Two corollaries of Lemma 2.1 that we use later:
  - ∂D has two smooth regular branches v = ±lambda(t), -1 < t < 1,
    joined at the two endpoints ±i.
  - Because lambda'' < 0, the tangent direction on each branch is
    strictly monotone along the branch. So any fixed unoriented line
    direction is tangent at most finitely many times per branch.

That is what "the boundary has strictly turning tangent directions" will
mean below.


================================================================
3. THE HOLOMORPHIC MASS LEMMA
================================================================

This section establishes a sharp lower bound for a special integral at
an isolated holomorphic zero. That bound is the analytic engine of the
whole proof.

Setup. Identify C^d with R^{2d} via z_j = x_j + i y_j. Normalize volume
    dV  =  dx_1 ^ dy_1 ^ ... ^ dx_d ^ dy_d   (a (2d)-form).
For a smooth real function v, define
    d^c  =  (i/4) (dbar - d),        so       d d^c = (i/2) d dbar.
With this convention,
    d^c v(xi) = -(1/4) d v(i xi)   for a real tangent vector xi,
and
    d d^c |z|^2 = Σ_j dx_j ^ dy_j,
    (d d^c v)^d = d! · det( v_{z_i-bar z_j} ) · dV.
(The second is a unitary diagonalization of the Hermitian Hessian.)

LEMMA 3.1 (Holomorphic mass at an isolated zero).
Let d >= 1, N >= d, and U ⊂ C^d open containing 0. Let
f = (f_1, ..., f_N) : U -> C^N be holomorphic, with
  (i)  f^{-1}(0) = {0};
  (ii) for some integer k >= 1,
           f(z) = H(z) + O(|z|^{k+1}) near 0,
       where each H_i is a homogeneous polynomial of degree k and
       H(z) != 0 whenever z != 0;
  (iii) for every 0 < s < 1, the sublevel set
           { z in U : |f(z)|^2 <= s }
       is compact in U.
Then, writing tau = |f|^2,
    ∫_{tau < 1}  Σ_{|I| = d}  |det(∂f_i / ∂z_j)_{i in I, 1<=j<=d}|^2 dV
         >=  (pi k)^d / d!.                                        (3.1)
Here I runs over d-element subsets of {1, ..., N}, with rows and columns
in increasing index order, and all norms are Euclidean.

Proof. We prove a lower bound for the integral of (d d^c tau)^d, and
then identify that integrand with the Jacobian minors via Cauchy-Binet.

Step A. (d d^c tau)^d and (d d^c log tau)^d are nonnegative densities.
Let Z = (∂f_i/∂z_j)_{i,j} be the N-by-d complex derivative matrix. Then

    tau_{z_i-bar z_j} = (Z* Z)_{i j},            (complex Hessian of tau)
so the complex Hessian of tau is Z*Z, which is positive semidefinite.

Away from 0, for a complex direction xi,
    Hessian(log tau)(xi)
         =  ( |f|^2 |df(xi)|^2 - |<df(xi), f>|^2 ) / |f|^4,
which is nonnegative by Cauchy-Schwarz. So log tau has a PSD complex
Hessian away from 0 as well. Therefore their top exterior powers
    (d d^c tau)^d  and  (d d^c log tau)^d
are nonnegative.

Step B. Stokes comparison with a small sphere. Fix a regular value
s in (0,1) of tau and set E_s = { tau < s }. By compactness of the
sublevel set (assumption (iii)) and Sard's theorem, E_s is a compact
smooth manifold with boundary ∂E_s = { tau = s }. Stokes gives
    ∫_{E_s} (d d^c tau)^d  =  ∫_{∂E_s} d^c tau ^ (d d^c tau)^{d-1}.
Put gamma = d^c log tau = tau^{-1} d^c tau on U \ {0}. The identities
    d^c log tau  =  tau^{-1} d^c tau,
    d d^c log tau = tau^{-1} d d^c tau  -  tau^{-2} d tau ^ d^c tau
and the fact that d tau pulls back to zero on ∂E_s give
    s^{-d} ∫_{E_s} (d d^c tau)^d  =  ∫_{∂E_s} gamma ^ (d gamma)^{d-1}.
Because E_s contains a neighborhood of 0 (assumption (i)) we can choose
epsilon > 0 small enough that the closed ball B_epsilon-bar lies in E_s.
Orient S_epsilon = ∂B_epsilon outward. Applying Stokes on
E_s minus the interior of B_epsilon-bar,
    s^{-d} ∫_{E_s} (d d^c tau)^d  -  ∫_{S_epsilon} gamma ^ (d gamma)^{d-1}
         =  ∫_{E_s \ B_epsilon} (d d^c log tau)^d   >=  0.
So
    s^{-d} ∫_{E_s} (d d^c tau)^d  >=  ∫_{S_epsilon} gamma ^ (d gamma)^{d-1}.
We compute the right-hand side in the limit epsilon -> 0.

Step C. The homogeneous flux. Let T(z) = |H(z)|^2, homogeneous of degree
2k, and let S = { |z| = 1 }. The Taylor expansion of f makes
    epsilon^{-2k} tau(epsilon z) -> T(z)  in C^2
uniformly on a fixed annulus containing S. (Term-by-term differentiation
of the convergent Taylor series gives this for the rescaled map, hence
for its squared norm.) Because T > 0 there, the logarithms converge
in C^2 as well. Under the rescaling z -> epsilon z, the additive
constant 2k log epsilon disappears under d^c. Consequently
    lim_{epsilon -> 0}  ∫_{S_epsilon} gamma ^ (d gamma)^{d-1}
         =  ∫_S alpha ^ (d alpha)^{d-1},     alpha = d^c log T |_S.  (3.2)

Step D. Homogeneity deformation. Introduce the reference alpha_0 =
d^c (log |z|^2)|_S, and set
    beta   =  d^c (log T - k log|z|^2) |_S,
    alpha_t =  k alpha_0 + t beta,   0 <= t <= 1.
Then alpha_1 = alpha.

Two invariances. First, T(r z) = r^{2k} T(z) for r > 0, so
log T - k log|z|^2 is dilation-invariant. Second, T(e^{i theta} z) = T(z),
so log T and log|z|^2 are both rotation-invariant; therefore log T -
k log|z|^2 is also rotation-invariant. These make beta invariant under
the phase rotation z -> e^{i theta} z and satisfy beta(V) = 0 for the
phase generator V(z) = i z on S. Also alpha_0(V) = 1/2, from the
normalization of d^c. So alpha_t(V) = k/2 is constant on S.

Cartan's identity now gives
    iota_V d alpha_t  =  L_V alpha_t  -  d( alpha_t(V) )  =  0,
since alpha_t is invariant (L_V alpha_t = 0) and alpha_t(V) is constant.
Hence the top-degree form beta ^ (d alpha_t)^{d-1} on S (which is a
(2d-1)-form on a (2d-1)-dimensional odd sphere) contracts to 0 by a
nowhere-zero vector field V, so it vanishes identically. Therefore
    d/dt  ∫_S alpha_t ^ (d alpha_t)^{d-1}
        =  d ∫_S beta ^ (d alpha_t)^{d-1}
        =  0.
So the integral is constant in t and
    ∫_S alpha ^ (d alpha)^{d-1}
        =  k^d ∫_S alpha_0 ^ (d alpha_0)^{d-1}.            (3.3)

Step E. Radial reference. On the unit sphere, alpha_0 and d alpha_0 are
the restrictions of d^c|z|^2 and d d^c|z|^2 respectively. Applying
Stokes on the unit ball and using (d d^c |z|^2)^d = d! dV (with unit
coefficient),
    ∫_S alpha_0 ^ (d alpha_0)^{d-1}
        =  ∫_{ |z| < 1 } (d d^c |z|^2)^d
        =  d! · vol_{2d}(unit ball)
        =  d! · (pi^d / d!)  =  pi^d.                     (3.4)

Putting (3.2)-(3.4) together,
    lim_{epsilon -> 0}  ∫_{S_epsilon} gamma ^ (d gamma)^{d-1}  =  (pi k)^d.
Combining with Step B,
    s^{-d} ∫_{E_s} (d d^c tau)^d  >=  (pi k)^d     for every regular
                                                     s in (0, 1).

Let s increase to 1 along a sequence of regular values (Sard supplies
them; the set of regular values of tau is dense in (0,1)). The integrand
(d d^c tau)^d is nonnegative, so monotone convergence gives
    ∫_{tau < 1} (d d^c tau)^d  >=  (pi k)^d.              (3.5)

Step F. Minor identification (Cauchy-Binet). For the complex Hessian Z*Z
of tau,
    (d d^c tau)^d  =  d! · det(Z* Z) · dV,    and
    det(Z* Z)      =  Σ_{|I| = d} |det Z_I|^2
(Cauchy-Binet, where Z_I is the d-by-d submatrix formed by the rows
indexed by I). Combining with (3.5) and dividing by d!,
    ∫_{tau < 1}  Σ_{|I| = d} |det Z_I|^2 dV  >=  (pi k)^d / d!.
That is (3.1). QED.

A useful observation for Part 4. If g : D_0 -> D is holomorphic, then for
any complex vectors we can compute ∂(g(b_i z)) / ∂z_j = g'(b_i z)·b_{i, j}.
So every row of the derivative matrix of g composed with a linear form is
a scalar multiple of that row. In particular, row minors on dependent
index sets vanish. This is the "dependent subsets have zero minors"
remark used in Part 4.


================================================================
4. FEASIBLE BASES: A PROBABILITY AT LEAST 1
================================================================

Fix d >= 1 and nonzero real row vectors b_1, ..., b_m in (R^d)*, assumed
to span. Set
    A  =  { X in R^d : |b_i·X| <= 1 for every i },       (4.1)
    C  =  A°  =  conv{ ±b_1, ..., ±b_m }.                (4.2)
The spanning assumption makes A bounded; 0 is interior to A. By the
bipolar theorem, A° is exactly C.

Let B be the collection of d-element subsets I of {1, ..., m} with (b_i)_{i in I}
linearly independent. For I in B, write B_I for the d-by-d matrix whose
rows are b_i, i in I, in increasing index order, and D_I = |det B_I|.
Dependent subsets are excluded throughout.

Take any biholomorphism F : D_0 -> D from the disk onto a bounded
planar domain, continuous on the closed disk, with F(0) = 0. Let
theta_i in [0, 2 pi) be independent uniform angles for i in I, and set
    Z_I(theta)  =  B_I^{-1} ( F(e^{i theta_i}) )_{i in I}   (4.3)
(the complex vector solving b_i Z = F(e^{i theta_i}) for i in I).
Define
    P_I  =  P( b_j Z_I(theta) in D-bar for every j ),        (4.4)
    S    =  Σ_{I in B}  P_I.                                 (4.5)

The "active" coordinates i in I are automatic (they solve to the
boundary by construction). All P_I are probabilities. The next lemma is
the analytic core of the main inequality.

LEMMA 4.1 (Boundary feasibility). Under the setup above (any F, any d,
any spanning nonzero rows),
    S  >=  1.                                                (4.6)

Proof. Let g = F^{-1}. Set
    Omega  =  { z in C^d : b_j z in D for every j },
    h_j(z) =  g(b_j z),      j = 1, ..., m.
Then Omega is open, bounded, contains 0 (since b_j·0 = 0 and 0 in D).
Each h_j is holomorphic.

Apply Lemma 3.1 to f_k = (h_1^k, ..., h_m^k) for integer k >= 1. Set
    tau_k  =  Σ_{j=1}^m |h_j|^{2k}.

Check the three assumptions.
  (i) Zeros. Since g vanishes only at 0 and the b_j span, if f_k(z) = 0
      then h_j(z) = 0, so b_j z = 0 for all j, which by spanning gives
      z = 0. So f_k^{-1}(0) = {0}.
  (ii) Homogeneous leading term. Let c = g'(0) != 0. Then
         h_j(z) = c b_j z + O(|z|^2),
         h_j(z)^k = (c b_j z)^k + O(|z|^{k+1}),
       and the degree-k part H_k(z) = ((cb_1 z)^k, ..., (cb_m z)^k) is
       nonzero for z != 0 again by spanning (some b_j z != 0).
  (iii) Compact sublevels. For 0 < s < 1 and z in {tau_k <= s}, each
        |h_j(z)| <= s^{1/(2k)}, hence b_j z in F( { |w| <= s^{1/(2k)} } )
        which is compact in D. A basis of rows then bounds z. So the
        sublevel is compact.

The derivative row of h_j^k is a scalar multiple of b_j (chain rule and
the fact that d/dz_i of h_j(z) = g'(b_j z) b_{j, i}). So dependent row
subsets have zero minors. Consequently, summing (3.1) over independent
row sets gives
    Σ_{I in B}  M_{I, k}  >=  k^d · pi^d / d!,               (4.7)
where
    M_{I, k}  =  ∫_{tau_k < 1}
                 |det( ∂(h_i^k)_{i in I} / ∂(z_1, ..., z_d) )|^2 dV.   (4.8)

Now fix I and change variables u_i = h_i(z), i in I. The map
z -> (h_i(z))_{i in I} is one-to-one on its image, with inverse
    z  =  B_I^{-1} ( F(u_i) )_{i in I}.
The squared complex Jacobian of the change is its real volume Jacobian
in the complex normalization we use. The squared determinant in M_{I, k}
is this Jacobian factor times
    k^{2d} · Π_{i in I} |u_i|^{2k-2}.
The transformed domain of u is contained in
    U_I,k  =  { u in D^d :  Σ_{i in I} |u_i|^{2k} < 1,
                            b_j B_I^{-1} (F(u_i))_{i in I} in D
                            for all j }.
We use this larger domain for an upper bound. Then switch to polar coords
u_i = rho_i^{1/k} e^{i theta_i}:
    k^2 |u_i|^{2k-2} dV_2(u_i)  =  k · rho_i d rho_i d theta_i.
Combining,
    M_{I, k} / k^d
       <=  ∫_{ Σ rho_i^2 < 1, theta in [0,2pi)^d, rho_i > 0 }
             1{ b_j B_I^{-1} (F(rho_i^{1/k} e^{i theta_i}))_{i in I} in D
                for all j }
             · Π_{i in I} rho_i d rho_i d theta_i.              (4.9)

The measure in (4.9) is finite: its total mass is vol_{2d} of the unit
ball in C^d = pi^d / d!. For every positive rho_i,
continuity of F on the closed disk makes the "inferred" points converge
to Z_I(theta). So the indicator converges to the indicator of the event
{ b_j Z_I(theta) in D-bar for all j } defining P_I (the difference is
only at boundary equalities, which is fine for an upper bound). By the
upper-bound form of Fatou's lemma on this finite measure space,
    lim sup_{k -> infinity}  M_{I, k} / k^d   <=   (pi^d / d!) · P_I.
Summing over the finitely many bases:
    pi^d / d!   <=  lim sup_k  Σ_I M_{I, k} / k^d
                <=  Σ_I  lim sup_k  M_{I, k} / k^d
                <=  (pi^d / d!) · S.
Cancel pi^d / d! to get S >= 1. QED.

Two remarks. First, the lemma allows arbitrary "extra-row boundary ties":
we did not require anything about equality of additional rows on ∂D.
That is enough to run Part 6. Part 5 sharpens the situation for the
simplex identity.

Second, in dimension 1, the sum S is a single probability and Lemma 4.1
says S >= 1, hence S = 1. This is a useful sanity check of the whole
apparatus: everything already works in dimension one where the answer is
obvious.


================================================================
5. EXTRA BOUNDARY HITS ARE NULL
================================================================

For the simplex identity in Part 6 we need a stronger statement: extra
rows do not hit ∂D with probability one — in fact, they do so with
probability zero. This is a consequence of the strict curvature of the
lens boundary.

From now on F, D, lambda are those of Lemma 2.1. We may further assume
the rows b_1, ..., b_m are pairwise NONPROPORTIONAL. Reason: on each
row line, keep the row of largest magnitude; its strip implies the other
strips on that line (because the larger coefficient tightens the strip).
Also discard zero rows (they impose no constraint). Neither operation
changes A.

LEMMA 5.1 (Extra boundary equalities have probability zero). Under the
assumptions above (spanning, pairwise nonproportional rows) with F the
lens map, for every I in B and every j not in I,
    P( b_j Z_I(theta) in ∂D )  =  0.                        (5.1)

Proof. Write b_j B_I^{-1} = (c_i)_{i in I}. At least two coefficients,
say c_a and c_b, are nonzero; otherwise b_j would be proportional to a
basis row, contradicting nonproportionality.

Let gamma(theta) = F(e^{i theta}) be the boundary curve of D. Away from
the two endpoints ±i, ∂D consists of the two smooth regular branches
(±lambda(t), t), -1 < t < 1.

Two local facts on the branches. First, lambda'' < 0 means that the
tangent direction on each branch is strictly monotone in t, so any fixed
unoriented line direction is tangent on a given branch at most finitely
many times. Second, the boundary parameter of gamma has constant speed
2/pi on each branch (Lemma 2.1, Step 4), so the derivative gamma' is
nowhere zero on each branch.

Now fix all phases theta_i with i != a, b. The remaining map
    (theta_a, theta_b)  |->  c_a gamma(theta_a) + c_b gamma(theta_b) + K
(where K is the constant from the other phases) has real Jacobian
determinant
    det( c_a gamma'(theta_a), c_b gamma'(theta_b) ).
For almost every (nonendpoint) theta_a, the function
theta_b |-> det(c_a gamma'(theta_a), c_b gamma'(theta_b))
is nonzero except at finitely many theta_b (this is the "tangency
happens finitely often" fact; gamma'(theta_b) lies on a curve with
monotone tangent direction, so the linear equation det(v, c_b gamma'(theta_b)) = 0
has finitely many solutions whenever v != 0 and c_b != 0). Thus the
zero set of the Jacobian determinant has planar measure zero in
(theta_a, theta_b) by Fubini.

Off this null set, the inverse function theorem gives local
diffeomorphism charts. A countable refinement of these charts covers the
complement of a null set, and in each chart the inverse is locally
Lipschitz, so it sends planar null sets to null sets. The boundary ∂D
is planar-null (a countable union of smooth compact arcs plus two
points). Therefore its inverse image under the map above has measure
zero in the (theta_a, theta_b)-plane. A final Fubini over the remaining
fixed phases proves (5.1). QED.

In dimension one, the reduced row list has one row, so there is nothing
to prove.


================================================================
6. THE REAL SIMPLEX IDENTITY (THE MAIN INEQUALITY)
================================================================

Now we translate the feasibility probabilities into real volumes, and
extract the main inequality.

Keep the nonzero, spanning, pairwise nonproportional rows b_1, ..., b_m
of (4.1). For X in int A, define
    L_X  =  { Y in R^d : |b_j·Y| <= lambda(b_j·X) for every j }.  (6.1)
Widths are strictly positive (X is interior), so L_X contains a
neighborhood of 0; a basis of rows bounds L_X. So L_X is a convex
polytope with nonempty interior.

For each basis I in B and each sign vector epsilon = (epsilon_i)_{i in I}
in {-1, +1}^I, set
    Y_{I, epsilon}(X)  =  B_I^{-1} ( epsilon_i lambda(b_i·X) )_{i in I}.  (6.2)
Call (I, epsilon) FEASIBLE at X when Y_{I, epsilon}(X) lies in L_X.
Next, define the closed simplex
    T_{I, epsilon}  =  conv( 0, { epsilon_i b_i : i in I } ),   (6.3)
    Sigma_X         =  ⋃_{ (I, epsilon) feasible at X } T_{I, epsilon}.  (6.4)
Then Sigma_X is a finite union of closed d-simplices contained in
C = A°.

The definition makes sense at any interior X, including points where
several constraints are simultaneously tight. For integration on ∂A we
declare every pair infeasible (making Sigma_X empty on the boundary);
this affects only an event of measure zero.

GEOMETRIC PICTURE. A feasible pair (I, epsilon) is a "vertex witness"
of L_X: the d signed constraints corresponding to the rows in I are all
tight at the same point Y_{I, epsilon}(X). The simplex T_{I, epsilon}
records "which d signed rows were active at this vertex". Summing over
feasible pairs gives a kind of footprint of L_X on the polar body.
The footprint is always at least 4^d/d! in integrated volume (up to a
constant), which is precisely the volume-product inequality.

PROPOSITION 6.1 (Feasible-simplex identity).
Let b_1, ..., b_m be nonzero, pairwise nonproportional real rows
spanning (R^d)*, and let F, D, lambda be the lens of Lemma 2.1. With
A, S, Sigma_X defined in (4.1), (4.5), (6.4),
    1  <=  S  =  (d! / 4^d) · ∫_A |Sigma_X| dX
              <=  (d! / 4^d) · |A| · |A°|.                   (6.5)
In particular |A| · |A°| >= 4^d / d!, and
    0  <=  ∫_A ( |A°| - |Sigma_X| ) dX
        <=  |A| · |A°| - 4^d / d!.                          (6.6)

Proof. The chain (6.5) has three steps: a probability-to-real-integral
step, a disjointness step, and a sandwich step.

Step 1. Probability to integral. By the boundary coordinate law (Lemma
2.1(iv)), each active boundary coordinate on ∂D has the distribution
    epsilon_i lambda(t_i) + i t_i,
with t_i uniform on [-1, 1] and epsilon_i an independent fair sign. So
for a fixed sign choice epsilon, the joint measure is 4^{-d} dt_I on
[-1,1]^d.

Write the inferred complex vector (for a given X) as Y + iX, i.e. solve
b_i(Y + iX) = epsilon_i lambda(t_i) + i t_i for each i in I. Comparing
imaginary parts, t_i = b_i X for i in I; comparing real parts,
Y = Y_{I, epsilon}(X). The constraints "all remaining rows lie in D-bar"
become:
    X in A   and   Y in L_X,
with the caveat that the boundary ∂A has measure zero (contained in
the finitely many hyperplanes b_j X = ±1).

Change variables from t_I to X via t_I = B_I X. The Jacobian is D_I
(absolute determinant). Therefore
    P_I  =  (D_I / 4^d) · ∫_A Σ_{epsilon in {-1,1}^I}
               1{ (I, epsilon) is feasible at X } dX.       (6.7)

Step 2. Disjointness of interiors for almost every X. Fix X in
int A outside a null set N (the set where some extra row hits ∂D). By
Lemma 5.1, N has measure zero. For X outside N:

Distinct feasible pairs have distinct Y-vectors. Suppose instead
Y_{I, epsilon}(X) = Y_{I', epsilon'}(X) with (I, epsilon) != (I', epsilon').
  - If I != I', the shared Y satisfies b_j Y = ±lambda(b_j X) for some
    j in only one of the bases. That j is "extra" for the other basis.
    But X is outside N, so such extra equalities don't happen.
  - If I = I' but epsilon != epsilon', the shared Y satisfies
    epsilon_i b_i Y = lambda(b_i X) = epsilon'_i b_i Y for some i with
    epsilon_i != epsilon'_i. Since lambda(b_i X) > 0 (X is interior), this
    is impossible.

Feasible simplices have disjoint interiors. Let e in int T_{I, epsilon}.
Then e = Σ_{i in I} alpha_i epsilon_i b_i with all alpha_i > 0 and
Σ alpha_i < 1. For any Y in L_X,
    e·Y  <=  Σ_{i in I} alpha_i lambda(b_i·X),                 (6.8)
because b_j Y <= lambda(b_j X) for all j and the epsilon_i absorb signs
(both sides even in signs). Equality in (6.8) forces
epsilon_i b_i Y = lambda(b_i X) for every i in I, i.e. Y = Y_{I, epsilon}(X).

Functionals see one vertex. The functional e·Y achieves its maximum on
L_X uniquely at Y_{I, epsilon}(X). If e also belonged to the interior of
T_{I', epsilon'}, then Y_{I', epsilon'}(X) would also be its unique
maximizer (same e, same L_X), so the two Y's agree. But distinct feasible
pairs have distinct Y's (shown above). Contradiction. So the interiors
are disjoint.

Each simplex T_{I, epsilon} has volume D_I / d! in R^d. So for almost
every X,
    d! · |Sigma_X|  =  Σ_{I in B} Σ_{epsilon in {-1,1}^I}
                          D_I · 1{ (I, epsilon) is feasible at X }.  (6.9)

Combining (6.7) and (6.9): S = Σ_I P_I = (1/4^d) ∫_A d! |Sigma_X| dX,
which is the equality in (6.5).

Step 3. Sandwich. By (4.6), S >= 1, giving the lower bound in (6.5).
Each feasible simplex T_{I, epsilon} has vertices in {0} ∪ C. So
T_{I, epsilon} ⊂ C = A° and |Sigma_X| <= |A°|. Hence
∫_A |Sigma_X| dX <= |A| |A°|, the upper bound.

Step 4. Deficit. From the exact identity,

    ∫_A ( |A°| - |Sigma_X| ) dX  =  |A| |A°|  -  (4^d / d!) · S.

The left-hand side is nonnegative because |Sigma_X| <= |A°|. It is at most
|A| |A°| - 4^d / d! because S >= 1. That gives (6.6) and also identifies
exactly the quantity that vanishes in the equality argument (Part 8).
QED.

Measurability check (a detail used implicitly). The set
    { (X, e) : X in int A, e in Sigma_X }
is a finite union of products of Borel feasibility sets and fixed closed
simplices. So X |-> |Sigma_X| is Borel measurable and bounded by |A°|.
Fubini applies throughout.

A small explicit example (illustration only; no step of the proof depends
on it). Let b_1 = (1,0), b_2 = (1/2, sqrt(3)/2), b_3 = b_2 - b_1, and
X = 0.9·(1, 1/sqrt(3)). Then b_1 X = b_2 X = 0.9 and b_3 X = 0. Writing
a = lambda(0.9), one checks 2a < lambda(0) using the endpoint estimate
and the alternating series for F(1); the third strip is thus redundant in
L_X. So Sigma_X is the union of four triangles with vertices
{ ± b_1, ± b_2 }, which is the full cross-polytope conv{±b_1, ±b_2},
while C = conv{±b_1, ±b_2, ±b_3} has extra area (the two "caps"). This
illustrates the deficit in (6.6). The exact size is not needed here.

Now we have |A| |A°| >= 4^d / d! for any polyhedral strip body A whose
polar is C = conv{±b_i} with pairwise nonproportional spanning rows.



================================================================
7. APPROXIMATION: ARBITRARY CONVEX BODIES
================================================================

Proposition 6.1 gives |A||A°| >= 4^d/d! for polyhedral strip bodies.
We now approximate arbitrary origin-symmetric convex bodies by
polytopes and pass to the limit.

COROLLARY 7.1 (Symmetric volume-product inequality).
For every origin-symmetric convex body K in R^d, d >= 1,
    |K| · |K°|  >=  4^d / d!.                                (7.1)

Proof. Let Q = K°. Because Q has nonempty interior, there is some
constant a > 0 with a·B_2^d ⊂ Q, where B_2^d is the Euclidean unit ball.

Take a sequence epsilon_j -> 0. Let N_j be a finite epsilon_j-net in Q
(cover Q by finitely many closed balls of radius epsilon_j). Adjoin the
negatives of N_j and let Q_j = conv(±N_j). Then Q_j is a symmetric
polytope, Q_j ⊂ Q, and the support functions satisfy, for every
Euclidean unit vector u,
    h_Q(u) - epsilon_j  <=  h_{Q_j}(u)  <=  h_Q(u),      h_Q(u) >= a.
Set delta_j = epsilon_j / a. Since epsilon_j -> 0 and a > 0, delta_j -> 0
and delta_j < 1 for large j. From
    h_{Q_j}(u) >= h_Q(u) - epsilon_j >= (1 - epsilon_j/a) h_Q(u)
           = (1 - delta_j) h_Q(u),
the support-function criterion for containment gives
    (1 - delta_j) Q  ⊂  Q_j  ⊂  Q.
Taking polars, and using (1.5) and ((1-delta)Q)° = (1-delta)^{-1} Q°,
    K  ⊂  A_j  :=  Q_j°  ⊂  (1 - delta_j)^{-1} K.                 (7.2)
In particular Q_j and A_j are full-dimensional symmetric polytopes for
large j (Q_j has interior because epsilon_j eventually beats the
inradius a; A_j is its polar).

For large j, choose one vertex from each antipodal vertex pair of Q_j
as a list of rows b_1, ..., b_m. This list is:
  - nonzero: 0 is interior to Q_j, so no sampled vertex is 0;
  - spanning: Q_j is full-dimensional;
  - pairwise nonproportional: two distinct boundary vertices on the same
    ray from an interior point cannot both be extreme.
The strip body of these rows is exactly A_j (by the standard polarity
description of a polytope as an intersection of signed half-spaces).

Proposition 6.1 applied to A_j gives |A_j| · |Q_j| >= 4^d / d!.

By the homothetic bounds (7.2),
    (1-delta_j)^d |Q| <= |Q_j| <= |Q|,
    |K| <= |A_j| <= (1-delta_j)^{-d} |K|.
So |Q_j| -> |Q| and |A_j| -> |K|, hence |A_j| |Q_j| -> |K| |Q|.
Passing to the limit gives |K| |K°| >= 4^d / d!. QED.

The argument uses no smoothness, no simplicity, and no general-position
assumption on K. These are the only places we ever left the polyhedral
world: for polytopes we already have everything (Prop 6.1), and for
general bodies we approximate.

In dimension 1: |K| |K°| = 2a · 2/a = 4 = 4^1/1! for K = [-a, a].


================================================================
8. THE LIFT AND THE DEFICIT: EQUALITY
================================================================

Assume now that K in R^n is origin-symmetric and P(K) = 4^n / n!.
We will extract strong structural information, culminating in the
classification of equality cases in Part 10. Work in one higher
dimension d = n + 1. Define
    B  =  K ⊕_1 [-1, 1]  =  { (x, s) : p_K(x) + |s| <= 1 },     (8.1)
    C  =  B°             =  Q × [-1, 1],   where Q = K°.         (8.2)
The polar formula follows from Lemma 1.1 applied to the segment
[-1,1] (whose polar is [-1,1]).

Volume of B and C. Any horizontal section of B at height s in [-1,1] is
(1 - |s|) · K (gauges add: p_B(x, s) <= 1 iff p_K(x) <= 1 - |s|). So
    |B|  =  |K| · ∫_{-1}^{1} (1 - |s|)^n ds  =  2 |K| / (n + 1).
    |C|  =  |Q| · |[-1, 1]|  =  2 |Q|.
    |B| |C|  =  [2 |K| / (n + 1)] · [2 |Q|]  =  (4/(n+1)) |K| |Q|
             =  (4/(n+1)) · (4^n / n!)  =  4^{n+1} / (n+1)! = 4^d / d!.
So equality is preserved under the lift.

INNER POLYTOPES FOR Q. Choose full-dimensional symmetric polytopes
Q_j ⊂ Q with t_j Q ⊂ Q_j ⊂ Q for some t_j in (0,1) with t_j -> 1. (The
construction from Corollary 7.1 works.) Set C_j = Q_j × [-1,1] and
B_j = C_j°. By the same polarity computation as before,
    t_j C  ⊂  C_j  ⊂  C           and            B  ⊂  B_j  ⊂  t_j^{-1} B.      (8.3)
In particular |B_j| |C_j| -> |B| |C| = 4^d / d!.

Use one vertex from each antipodal vertex pair of C_j as a row list.
This gives a strip description of B_j; the rows belong to
Q_j × {±1} = vertices of C_j, are nonzero, span, and are pairwise
nonproportional. Let Sigma_{j,X} be the union of feasible signed basis
simplices for this strip description of B_j, as in (6.4). Then by
Prop 6.1 (applied to B_j as strip body),
    D_j  :=  ∫_{B_j} (|C_j| - |Sigma_{j,X}|) dX
         <=  |B_j| |C_j|  -  4^d / d!  ->  0.         (8.4)
Note: |B_j| |C_j| is the SAME expression as before (perturbed by
t_j -> 1), and (4^d/d!) is exactly the constant that B,C attain, so
D_j -> 0 as j -> infinity.

The "leftover 4^d/d! - |B_j||C_j|" gap has the interpretation: as
Q_j -> Q, the missing volume of feasible simplices evaporates. In the
limit we get a sharp witness for every interior point and every
direction.

----------------------------------------------------------------
Step 1: from a vanishing integral to pointwise witnesses.
----------------------------------------------------------------

Fix X in int B and e in ∂C. We construct a sequence j_k -> infinity and
points
    X_k in int B_{j_k},      e_k in Sigma_{j_k, X_k},
    with  (X_k, e_k) -> (X, e).                              (8.5)

For each k, pick a Euclidean ball U_k of positive volume in
int B ∩ EuclideanBall(X, 1/k). Pick a Euclidean ball V_k of positive
volume with closure contained in int C ∩ EuclideanBall(e, 1/k). To find
V_k at the boundary point e: move a small distance from e toward the
interior point 0; the resulting point is interior to C; take a small
ball about it. (This is possible since 0 ∈ int C.)

By (8.3) we have U_k ⊂ int B_j for every j, and V_k ⊂ C_j for all j
large enough (because max_{h in V_k-} p_C(h) < 1 and t_j -> 1). Choose
j_k large enough that all these containments hold and D_{j_k} < |U_k| |V_k|.

If none of the sets Sigma_{j_k, Z}, Z in U_k, met V_k, then for every
Z in U_k we would have |Sigma_{j_k, Z}| <= |C_{j_k}| - |V_k|. Integrate
over Z in U_k:
    ∫_{U_k} (|C_{j_k}| - |Sigma_{j_k, Z}|) dZ  >=  |U_k| |V_k|.
But the integral over the larger region B_{j_k} is by definition D_{j_k},
and U_k ⊂ B_{j_k}, so D_{j_k} >= |U_k| |V_k|, contradicting D_{j_k} < |U_k|
|V_k|. Therefore some X_k in U_k has Sigma_{j_k, X_k} ∩ V_k nonempty.
Pick e_k in that intersection. We get (8.5).

----------------------------------------------------------------
Step 2: subdividing inside the simplex, and passing to the limit.
----------------------------------------------------------------

For each k, pick one feasible simplex of Sigma_{j_k, X_k} containing e_k.
Write its d vertices as c_{1k}, ..., c_{dk} in Q_{j_k} × {±1} (signed
vertices of C_{j_k}; the sign is absorbed). Because e_k lies on the
simplex, there are weights theta_{ik} >= 0 with
    e_k  =  Σ_{i=1}^d theta_{ik} c_{ik},       Σ_i theta_{ik} <= 1.   (8.6)
(If e_k lies in the interior of the simplex, Σ theta < 1; the leftover is
the mass placed at the simplex vertex 0. Both cases are allowed.)

By feasibility of (I_k, epsilon_k), there is a witness Y_k in R^d with
    c_{ik} · Y_k  =  lambda(c_{ik} · X_k)        (i = 1, ..., d),     (8.7)
    |v · Y_k|  <=  lambda(v · X_k)              (v a vertex of C_{j_k}).
The second inequality extends to all h in C_{j_k}: write h = Σ s_l v_l
as a convex combination of vertices v_l, so s_l >= 0, Σ s_l = 1, then
    |h · Y_k|  <=  Σ s_l |v_l · Y_k|
              <=  Σ s_l lambda(v_l · X_k)
              <=  lambda( (Σ s_l v_l) · X_k )  =  lambda(h · X_k),
where the last inequality uses concavity of lambda (Lemma 2.1) and the
fact that both h · X_k and v_l · X_k lie in [-1, 1]. (That inclusion
holds because h in C and X_k in B implies |h · X_k| <= 1 by polarity.)

Consequently Y_k ∈ lambda(0) B_{j_k}. By the polar sandwich (8.3),
B_{j_k} ⊂ t_{j_k}^{-1} B, so Y_k stays in a fixed bounded set regardless
of k. We can pass to a subsequence.

Convergence to a representation. Compactness: Y_k in a bounded set,
c_{ik} ∈ Q × {±1} (compact set of vertices), theta_{ik} ∈ [0,1] (compact).
Pass to a subsequence so that c_{ik} -> c_i, theta_{ik} -> theta_i, and
Y_k -> Y. Then (taking limits in (8.6), (8.7), and the derived inequality)
    c_i ∈ Q × {±1},     theta_i >= 0,       Σ theta_i <= 1,
    e  =  Σ theta_i c_i,
    c_i · Y  =  lambda(c_i · X)    (i = 1, ..., d),
    |h · Y|  <=  lambda(h · X)     (all h in C).                       (8.8)

(For the last "all h in C" inequality, use h_k = t_{j_k} h ∈ C_{j_k} in
the derived inequality and let k -> infinity.)

Total mass = 1. Since e ∈ ∂C, p_C(e) = 1. Then
    1  =  p_C(e)  =  p_C(Σ theta_i c_i)
       <=  Σ theta_i p_C(c_i)  <=  Σ theta_i  <=  1.
The middle p_C(c_i) <= 1 because c_i ∈ C. So Σ theta_i = 1: none of
the limiting mass remains at the simplex vertex 0. All of it sits on the
signed basis rows.

----------------------------------------------------------------
Step 3: from a representation of e to a representation of any xi, and
the optimality.
----------------------------------------------------------------

Now fix X in int B and any nonzero xi = (q, a) in R^n × R. Let
T = p_C(xi) = max(p_Q(q), |a|)  (from (1.3) applied to C = Q × [-1,1]).

Apply the preceding construction to e = xi / T in ∂C. Set alpha_i = T theta_i.
Then alpha_i >= 0, Σ alpha_i = T, and
    xi = Σ_i alpha_i c_i,    c_i ∈ Q × {±1},
    c_i · Y  =  lambda(c_i · X)   (i = 1, ..., r),
    |h · Y|  <=  lambda(h · X)    (all h in C),
where r = number of nonzero alphas, 1 <= r <= d.

For any competing representation xi = Σ_j beta_j h_j (beta_j >= 0,
h_j in C), the bound (8.10) gives h_j · Y <= |h_j · Y| <= lambda(h_j · X).
Multiply by beta_j and sum:
    xi · Y  =  Σ_j beta_j (h_j · Y)   <=   Σ_j beta_j lambda(h_j · X).
On the other hand, from xi = Σ_i alpha_i c_i and c_i · Y = lambda(c_i · X):
    xi · Y  =  Σ_i alpha_i (c_i · Y)  =        Σ_i alpha_i lambda(c_i · X).
So the cost of the chosen representation is at most the cost of any
competitor. That is the minimality assertion of Prop 8.1.

PROPOSITION 8.1 (Optimal representation).
Let K ⊂ R^n be origin-symmetric with P(K) = 4^n/n!. Put Q = K°, d = n+1,
and define B, C by (8.1), (8.2). Then for every X in int B and every
nonzero xi = (q, a) in R^n × R, there exist:
  - r vectors c_i = (b_i, sigma_i) with 1 <= r <= d, b_i in Q, sigma_i
    in {±1};
  - nonnegative weights alpha_i with Σ alpha_i = T = max(p_Q(q), |a|);
  - a vector Y in R^d,
such that
    xi  =  Σ_{i=1}^r alpha_i c_i,                                       (8.9)
    |h · Y|  <=  lambda(h · X)    for every h in C,                    (8.10)
    c_i · Y  =  lambda(c_i · X)   for i = 1, ..., r,                    (8.11)
    Σ_i alpha_i lambda(c_i · X)  <=  Σ_j beta_j lambda(h_j · X)         (8.12)
    for every alternative representation xi = Σ_j beta_j h_j with
    beta_j >= 0 and h_j in C.

PROOF. Steps 1-3 above. The choices may depend on X and xi; we do not
require any compatibility between different X's. This is exactly what
we need in Part 9. The conclusion holds even in the degenerate case
where the limiting directions c_i collapse to dependent rows; there is
no independence assumption on the c_i at the end.

Two words of geometric intuition. We are pushing the "visible footprint"
computation (Part 6) to its limit. If K sits on the equality case, the
footprint fills the whole polar body C up to integrable error, and the
limiting witnesses form a coherent shadow: for each point and direction
we get a representation whose row-cost matches the "hypograph" of the
lens. This is the structure exploited in Part 9.


================================================================
9. FROM OPTIMAL REPRESENTATIONS TO METRIC MEDIANS
================================================================

This section converts the optimal representation (Prop 8.1) into a
geometric property of the polar body: medians for every triple.

DEFINITION. Let (V, ||·||) be a normed real vector space. A metric
median of three points x_0, x_1, x_2 in V is a point m in V satisfying,
for every pair i < j,
    ||x_i - x_j||  =  ||x_i - m||  +  ||m - x_j||.                     (9.1)
Equivalently, m lies on every "geodesic" between x_i and x_j in the
norm. The median need not be unique.

We work with V = R^n, ||·|| = p_Q, Q = K°.

PROPOSITION 9.1 (Median for the equality body).
Let K in R^n be origin-symmetric with P(K) = 4^n / n!, Q = K°. Then every
triple of points in (R^n, p_Q) has a metric median.

PROOF. Translation in R^n (adding a common vector to all three points)
preserves distances and turns any median into a median. So reduce to
the triple {0, x, y}.

If two of {0, x, y} agree, that common point is trivially a median.
Assume 0, x, y are distinct. Set
    p_1 = ||x||,        p_2 = ||y||,        p = ||x - y||,
    s = p_1 + p_2,       a = p_1 - p_2.
The triangle and reverse-triangle inequalities give s >= p >= |a| > 0.

Define
    A_+  =  (p + a) / 2,     A_-  =  (p - a) / 2,     c  =  (s - p) / 2.
All nonnegative. Two simple sums:
    A_+ + A_-  =  p,        c + A_+  =  p_1,       c + A_-  =  p_2.     (9.2)

The compact set:
    D_0  =  { r_+ - r_- : r_+ + r_- = x - y,
                          ||r_+|| <= A_+,  ||r_-|| <= A_- }.          (9.3)
This is the linear image of the intersection of A_+ Q × A_- Q (a compact
convex set in R^n × R^n) with the affine subspace r_+ + r_- = x - y.
So D_0 is compact and convex. It is nonempty because
r_± = (A_± / p)(x - y) satisfy all the constraints, including
r_+ + r_- = (A_+ + A_-)/p · (x - y) = x - y.

MAIN CLAIM to be proved:
    x + y  ∈  D_0  +  (s - p) Q.                                (9.4)
Consequences. Choose r_+, r_- realizing x + y as
x + y = (r_+ - r_-) + (s - p) u for some u in Q. Set
    m  =  x - r_+  =  y + r_-.
(The second equality holds because r_+ + r_- = x - y: x - r_+ equals
y + r_- iff x - y = r_+ + r_-.) Then
    2 m  =  x + y - (r_+ - r_-)  =  (s - p) u,
so ||m|| <= (s - p)/2 = c. Also ||x - m|| = ||r_+|| <= A_+, and
||y - m|| = ||r_-|| <= A_-. Now the triangle inequality forces every
one of these to be an equality:
    p_1  <=  ||m|| + ||x - m||  <=  c + A_+  =  p_1,
    p_2  <=  ||m|| + ||y - m||  <=  c + A_-  =  p_2.
Hence ||m|| = c, ||x - m|| = A_+, ||y - m|| = A_-, and so
    ||x - m|| + ||m - y||  =  A_+ + A_-  =  p  =  ||x - y||.
Together with the two pairs from the triangle equalities, m is a median
of {0, x, y} in the norm p_Q. So it remains to prove (9.4).

Proof of (9.4) by support functions. Let u ∈ int K. Set
    X_delta  =  (delta u, 1 - delta)  ∈  R^n × R,        0 < delta < 1.  (9.5)
Then X_delta ∈ int B because
    p_B(X_delta)  =  delta p_K(u) + 1 - delta  <  1
(using (8.1) and p_K(u) < 1 for u ∈ int K).

Apply Proposition 8.1 with X = X_delta and xi = (x - y, a) in R^n × R.
Its total T = p_C(xi) = max(p_Q(x - y), |a|) = max(p, |a|) = p
(using p >= |a|). We get rows c_i = (b_i, sigma_i), b_i ∈ Q,
sigma_i ∈ {±1}, weights alpha_i >= 0, Σ alpha_i = p, and witness Y_delta.
Define the aggregate splits:
    r_±  =  Σ_{i : sigma_i = ±1} alpha_i b_i.                    (9.6)
Then
    r_+ + r_-  =  Σ_i alpha_i b_i  =  x - y
(the n-dimensional part of xi = Σ alpha_i c_i must be x - y, and c_i's
n-part is b_i). And
    Σ_{i : sigma_i = ±1} alpha_i  =  (p ± a) / 2  =  A_±.
(Here the last coordinate of xi = Σ_i alpha_i c_i reads a = Σ_i sigma_i
alpha_i, and Σ_i alpha_i = p.) In particular,
    ||r_±||  <=  Σ_{sigma_i = ±1} alpha_i ||b_i||  <=  A_±
(using b_i in Q so ||b_i|| = p_Q(b_i) <= 1). Hence
    r_+ - r_-  ∈  D_0                                             (9.7)
for each delta (the r_± may depend on delta).

Now the endpoint comparison. For b in Q and sigma in {±1},
    lambda(<(b, sigma), X_delta>)  =  lambda(1 - delta(1 - sigma<b, u>))
(expand the inner product via (9.5)). The numbers
1 - sigma<b,u> range over a compact subinterval of (0, infinity) as (b,
sigma) ranges over Q × {±1}: their infimum is 1 - p_K(u) > 0 and their
supremum is 1 + p_K(u) < infinity. Lemma 2.2 therefore gives a rate
epsilon_u(delta) -> 0 with
    | lambda(<(b, sigma), X_delta>) / lambda(1 - delta) - (1 - sigma<b, u>) |
        <=  epsilon_u(delta)                                    (9.8)
uniformly over b in Q and sigma in {±1}.

Lower bound on the normalized cost. Apply (8.11) and the definition of
optimality. From the endpoint error (9.8), for each i,
    lambda(c_i · X_delta)  >=  lambda(1 - delta)(1 - sigma_i<b_i, u> - epsilon).
Multiply by alpha_i and sum:
    Σ alpha_i lambda(c_i · X_delta)
        >=  lambda(1 - delta) [ Σ alpha_i (1 - sigma_i <b_i, u>) - p epsilon ]
        =  lambda(1 - delta) [ Σ alpha_i - <Σ sigma_i alpha_i b_i, u> - p epsilon ]
        =  lambda(1 - delta) [ p - <r_+ - r_-, u> - p epsilon ]
        =  lambda(1 - delta) [ p - h_{r_+ - r_-}(u) - p epsilon ].
Here I set h_V(u) = V·u for a point V (support of a singleton).

Upper bound on the normalized cost. Compare with the "two-term"
representation
    (x - y, a)  =  p_1 (x/p_1, +1)  +  p_2 (-y/p_2, -1).
Both rows belong to Q × {±1}: x/p_1 has ||x/p_1|| = 1 exactly, so it
lies on ∂Q ⊂ Q, and similarly for -y/p_2. The cost |·| is the sum of the
two coefficients, p_1 + p_2 = s. Let me compute the normalized cost of
this alternative representation. Apply the endpoint error (9.8) with
the two supporting rows:
    row 1:   (x/p_1, +1)  ·  X_delta  =  1 - delta(1 - <x/p_1, u>),
    row 2:   (-y/p_2, -1)  ·  X_delta  =  -(1 - delta(1 - <y/p_2, u>)).
By evenness of lambda,
    lambda(<(-y/p_2, -1), X_delta>)  =  lambda(1 - delta(1 - <y/p_2, u>)).
So the alternative cost divided by lambda(1 - delta) equals
    p_1 (1 - <x/p_1, u> + O(epsilon_u))  +  p_2 (1 - <y/p_2, u> + O(epsilon_u))
(long form), which tends to
    p_1 (1 - <x/p_1, u>)  +  p_2 (1 - <y/p_2, u>)  =  s - <x + y, u>.      (9.9)

By the optimality (8.12) of the chosen representation, the chosen
normalized cost is at most the alternative normalized cost. Combine
with the lower bound:
    p - <r_+ - r_-, u> - p epsilon_u(delta)  <=  (chosen cost) / lambda(1-delta)
                                              <=  (alternative cost) / lambda(1-delta)
                                              =   s - <x + y, u> + O(1/L),
where L = log(1/delta), and O(1/L) -> 0 uniformly over (b, sigma) in the
compact set.

Now pass to the limit delta -> 0. The pairs (r_+, r_-) live in a compact
set (the linear image of a compact convex set) so have a convergent
subsequence with limit (r_+^*, r_-^*) and d_0 := r_+^* - r_-^* in D_0.
The errors epsilon_u(delta) and O(1/L) vanish in the limit. We get
    p - <d_0, u>  <=  s - <x + y, u>,
equivalently
    <x + y, u>  <=  <d_0, u>  +  (s - p)  <=  h_{D_0}(u) + (s - p).      (9.10)
This holds for every u ∈ int K.

Extend to all u ∈ K by continuity of all the maps. For nonzero
v ∈ R^n, put u = v / h_Q(v) ∈ ∂K. By homogeneity of support functions,
(9.10) at this u gives
    <x + y, v>  <=  h_{D_0}(v)  +  (s - p) h_Q(v).
At v = 0 the same inequality holds trivially. So
    <x + y, v>  <=  h_{D_0 + (s-p)Q}(v)          for all v in R^n.
Convex separation (or the separating-hyperplane theorem for compact
convex sets) then gives
    x + y  ∈  D_0 + (s - p) Q.                              (9.11)
That is (9.4). We have already shown (9.4) implies the median property.
Done. QED.


================================================================
10. THREE BALLS AND THE EQUALITY CLASSIFICATION
================================================================

DEFINITION. A normed real vector space V has the THREE-BALL INTERSECTION
PROPERTY (also called the 3.2 intersection property) if any three closed
balls that intersect pairwise have a common point. Radii may differ, may
be zero, and may be infinite.

LEMMA 10.1 (Medians imply 3.2 IP).
Suppose every triple of points in a real normed space V has a metric
median. Then V has the three-ball intersection property.

PROOF. Consider pairwise-intersecting closed balls
    cl(Ball(x_1, r_1)),    cl(Ball(x_2, r_2)),    cl(Ball(x_3, r_3)),
r_i >= 0. Let m be a metric median of the centers x_1, x_2, x_3, and
set d_i = ||m - x_i||. Pairwise intersection gives ||x_i - x_j|| <= r_i +
r_j. By the median property,
    d_i + d_j  =  ||x_i - x_j||  <=  r_i + r_j             (i != j).    (10.1)

If every d_i <= r_i, then m itself lies in all three balls. Suppose
otherwise: after relabeling, t := d_1 - r_1 > 0. For j = 2, 3, (10.1)
reads d_j + t <= r_j, so the ball about x_j excludes m at distance at
most r_j - t from it (m is at distance d_j <= r_j - t < r_j from x_j).
Since 0 < t <= d_1, define
    z  =  m + (t / d_1)(x_1 - m),
a point on the segment from m to x_1 at distance t from m and
distance d_1 - t = r_1 from x_1. So ||z - x_1|| = r_1. And for j = 2, 3,
    ||z - x_j||  <=  ||z - m|| + ||m - x_j||  =  t + d_j  <=  r_j.
So z lies in all three balls. When r_1 = 0 we have t = d_1 and z = x_1,
included in the same argument. QED.

We now use the following deep classification from the literature.

THEOREM 10.2 (Hansen-Lima). Every nonzero finite-dimensional real Banach
space with the 3.2 intersection property is linearly isometric to a
space obtained from R by finitely many ℓ_1 and ℓ_∞ direct sums.

This is Hansen-Lima, Acta Math. 146 (1981), Corollary 7.4. The unit
ball of any such space is, by definition, a Hanner polytope (Part 1).
The two direct-sum norms are exactly those of (1.2), (1.3).

PROPOSITION 10.3 (Equality implies Hanner).
If K ⊂ R^n is origin-symmetric with P(K) = 4^n / n!, then K is a linear
Hanner body.

PROOF. Put Q = K°. Prop 9.1 gives medians for every triple in (R^n, p_Q).
Lemma 10.1 gives the 3.2 IP for (R^n, p_Q). Every finite-dimensional
normed real space is a Banach space (complete as a topological vector
space: any Cauchy sequence in R^n converges). Theorem 10.2 therefore
gives an invertible linear map T : R^n -> R^n and a Hanner polytope H in
R^n with Q = TH. Then by (1.4) of Lemma 1.1 and (1.5) of Lemma 1.2,
    K  =  Q°  =  (TH)°  =  T^{-T} H°,
and H° is a Hanner polytope. So K is a linear Hanner body. QED.

COMPLETION OF THE MAIN THEOREM. Combine the parts.
  - Lemma 1.2 says every linear Hanner body attains P = 4^n/n!.
  - Corollary 7.1 gives P(K) >= 4^n/n! for every origin-symmetric K.
  - Proposition 10.3 says equality forces linear Hanner.
Together: P(K) >= 4^n/n!, with equality if and only if K is a linear
Hanner body. This is the Main Theorem stated in Part 0. QED.


================================================================
11. TWO COROLLARIES: FUNCTIONAL AND ENTROPY
================================================================

The Main Theorem implies two sharp functional inequalities. Both are
already in the literature; here they appear as corollaries of the new
geometric input. Both proofs reduce to pre-existing theorems that hold
CONDITIONALLY on the all-dimensional symmetric Mahler inequality, which
we now have unconditionally.

----------------------------------------------------------------
11a. Even functional Mahler inequality.
----------------------------------------------------------------

For a proper lower-semicontinuous convex function phi : R^n -> R ∪ {+inf}
(the effective domain { phi < +inf } has nonempty interior), its
Fenchel-Legendre transform is
    phi*(y)  =  sup_{x} ( x·y - phi(x) ).
By convention e^{-inf} = 0.

COROLLARY 11.1 (Even functional Mahler).
For every n >= 1 and every even proper lower-semicontinuous convex
phi : R^n -> R ∪ {+inf} with 0 < ∫ e^{-phi} dx < inf,
    ( ∫ e^{-phi(x)} dx ) · ( ∫ e^{-phi*(y)} dy )  >=  4^n.          (11.1)
The second integral is allowed to be +inf, in which case the inequality
is immediate.

PROOF. Set f = e^{-phi}: nonzero integrable log-concave function (a
standard fact about log of e^{-phi} = -phi). Fradelizi-Meyer introduce
the polar function
    f^z(y)  =  inf_{x : f(x) > 0} ( e^{-(x-z)·(y-z)} / f(x) )      (11.2)
and the translation-minimized functional volume product
    P(f)   =  ( ∫ f(x) dx ) · inf_{z in R^n} ∫ f^z(y) dy.        (11.3)
Their Proposition 1(a) states: if the symmetric geometric Mahler
inequality P(K) >= 4^n/n! holds in EVERY dimension n, then P(f) >= 4^n for
every even log-concave f : R^n -> R with 0 < ∫ f < inf. (Reference:
Fradelizi-Meyer, "Some functional inverse Santalo inequalities",
Adv. Math. 218 (2008), 1430-1452.)

Theorem of Part 10 supplies this all-dimensional hypothesis. Then
    ( ∫ e^{-phi} dx ) · ( ∫ e^{-phi*} dy )   =   ( ∫ f dx ) · ( ∫ f^0 dy )   >=   P(f)   >=   4^n.
The middle inequality uses z = 0 in the infimum defining P(f), and
    f^0(y)  =  inf_{x : f(x) > 0} e^{-x·y}/f(x)
           =  inf_x exp(-x·y + phi(x))
           =  exp( - sup_x (x·y - phi(x)) )
           =  e^{-phi*(y)}
whenever the infimum is over a positive set. Since phi is proper lsc
convex, the sup defining phi* may take the value +inf; then f^0 = 0 in
the appropriate sense. So the corollary follows. QED.

REMARK. The corollary's constant 4^n is sharp: take phi(x) = Σ|x_i|.
Then phi* is 0 on [-1,1]^n and +inf outside. Both integrals equal 2^n.
Product = 4^n = the bound.

The corollary does NOT classify equality on the functional side: the
limiting implication (11.3) uses auxiliary bodies of dimension n + m
with m -> inf and does not actually reduce to a single (n)-dimensional
geometric equality case. For potentials WITHOUT evenness the correct
sharp constant is e^n (companion paper on general convex bodies).

----------------------------------------------------------------
11b. Symmetric entropy-transport inequality.
----------------------------------------------------------------

For a log-concave probability measure eta with a density, define the
entropy relative to Lebesgue measure:
    H(eta)  =  ∫ log(d eta/dx) d eta,
the negative of the differential Shannon entropy.

For probability measures mu_1, mu_2 in R^n with finite first moments,
set the (Kantorovich-style convex-transport) cost
    T(mu_1, mu_2)  =  inf_{psi} ( ∫ psi dmu_1 + ∫ psi* dmu_2 ),
where psi ranges over proper lower-semicontinuous convex functions
R^n -> R ∪ {+inf} and psi* is the Fenchel-Legendre transform. The cost
may be +inf.

COROLLARY 11.2 (Symmetric entropy-transport inequality).
For every n >= 1, let eta_i(dx) = e^{-V_i(x)} dx, i = 1, 2, be full-
dimensional log-concave probability measures on R^n, both symmetric
about the origin, with proper lower-semicontinuous convex potentials
V_i. Assume also that the densities are essentially continuous: that is,
e^{-V_i} = 0 at H^{n-1}-almost every point of ∂supp(eta_i) (the
density vanishes at almost all boundary points of its support, in the
H^{n-1}-dimensional sense). Then:
    * the moment measures nu_i = (∇ V_i)_# eta_i have finite first
      moments;
    * H(eta_i) = -∫ V_i d eta_i is finite;
    * and
         H(eta_1) + H(eta_2)  <=  -n log(4 e^2) + T(nu_1, nu_2).     (11.4)

PROOF. For rho = e^{-V} the gradient identity
    |∇rho| = |∇V| e^{-V}
holds almost everywhere on the interior of the support. Lemma 4 and the
proof of Proposition 7 of Cordero-Erausquin-Klartag (J. Funct. Anal. 268
(2015)) give ∫ |∇rho| < +inf and V ∈ L^1(eta) respectively. The
pushforward nu = (∇V)_# eta therefore has finite first moment, and the
entropy H(eta) = -∫ V d eta is finite.

Gozlan's equivalence (as recorded in Fradelizi-Gozlan-Zugmeyer,
arXiv:2109.00871, Theorem 1.3) connects the symmetric functional inverse
Santaló inequality to the symmetric entropy-transport inequality. Apply
that equivalence to Corollary 11.1 with the sharp constant c = 4. We
obtain (11.4). QED.

Both corollaries are downstream conveniences: they follow from the
Main Theorem but do not feed back into it.


================================================================
REFERENCES AND PROVENANCE
================================================================

Each ingredient is labeled by what part of the proof depends on it.

CLASSICAL LITERATURE (cited in the proof).
  - Hansen, A. B.; Lima, A. "The structure of finite dimensional Banach
    spaces with the 3.2 intersection property." Acta Math. 146 (1981),
    1-23. Corollary 7.4 is Theorem 10.2 above.
  - Lima, A. "Intersection properties of balls in spaces of compact
    operators." Ann. Inst. Fourier 28 (1978), 35-65. Contains the norm-
    additive decomposition (median vs. 3.2 IP) criterion.
  - Fradelizi, M.; Meyer, M. "Some functional inverse Santalo
    inequalities." Adv. Math. 218 (2008), 1430-1452. Proposition 1(a)
    is used in Cor. 11.1.
  - Cordero-Erausquin, D.; Klartag, B. "Moment measures." J. Funct.
    Anal. 268 (2015), 3834-3866. Lemma 4 and Proposition 7 in Cor. 11.2.
  - Fradelizi, M.; Gozlan, N.; Zugmeyer, S. "Transport proofs of some
    functional inverse Santalo inequalities." arXiv:2109.00871v3.
    Theorem 1.3 in Cor. 11.2.

LENS AND MASS LEMMA.
  - Gross, R. "A conformal Skorokhod embedding." Electron. Commun. Probab.
    24 (2019), article 68. Section 3.2: our F is a rotation of the
    uniform case; all required properties are re-proved here
    (Lemma 2.1) to keep the argument self-contained.
  - Demailly, J.-P. "Monge-Ampere operators, Lelong numbers and
    intersection theory" (1993), sections 3 and 5. Standard reference
    for the mass lemma; we give a self-contained Stokes proof
    (Lemma 3.1).

HISTORICAL CONTEXT (background, not prerequisites).
  - Mahler, K. "Ein Ubertragungsprinzip fur konvexe Korper." Casopis
    Pest. Mat. Fys. 68 (1939), 93-102. The volume-product problem.
  - Mahler, K. "Ein Minimalproblem fur konvexe Polygone." Mathematica
    (Zutphen) B7 (1938), 118-127. Planar case.
  - Reisner, S. "Zonoids with minimal volume-product." Math. Z. 192
    (1986), 339-346. Equality in the zonoid class.
  - Iriyeh, H.; Shibata, M. "Symmetric Mahler's conjecture for the
    volume product in the 3-dimensional case." Duke Math. J. 169
    (2020), 1077-1134. Complete 3-D symmetric case.
  - Fradelizi, M.; Hubard, A.; Meyer, M.; Roldan-Pensado, E.; Zvavitch,
    A. "Equipartitions and Mahler volumes of symmetric convex bodies."
    Amer. J. Math. 144 (2022), 1201-1219. Shorter 3-D proof via
    equipartitions plus stability.
  - Chen, S.; Li, Y.; Xi, D.; Xu, Z.-F. "The Mahler Conjecture in Three
    Dimensions." arXiv:2605.09334. Shadow-flow proof; also treats the
    nonsymmetric 3-D case.
  - Saint-Raymond, J. "Sur le volume des corps convexes symetriques."
    Seminaire d'initiation a l'analyse (1980-1981), exp. 11. Sharp
    inequality for unconditional bodies.
  - Meyer, M. "Une caracterisation volumique de certains espaces normes
    de dimension finie." Israel J. Math. 55 (1986), 317-326. Hanner
    equality cases in the unconditional class.
  - Reisner, S. "Minimal volume-product in Banach spaces with a
    1-unconditional basis." J. London Math. Soc. 36 (1987), 126-136.
    Conditional statement connecting minimal volume product and ball-
    intersection structure.
  - Gordon, Y.; Meyer, M.; Reisner, S. "Zonoids with minimal volume-
    product - a new proof." Proc. Amer. Math. Soc. 104 (1988), 273-276.
  - Nazarov, F.; Petrov, F.; Ryabogin, D.; Zvavitch, A. "A remark on
    the Mahler conjecture: local minimality of the unit cube." Duke
    Math. J. 154 (2010), 419-430.
  - Kim, J. "Minimal volume product near Hanner polytopes." J. Funct.
    Anal. 266 (2014), 2360-2402.
  - Kim, J.; Zvavitch, A. "Stability of the reverse Blaschke-Santalo
    inequality for unconditional convex bodies." Proc. Amer. Math.
    Soc. 143 (2015), 1705-1717.
  - Bourgain, J.; Milman, V. D. "New volume ratio properties for convex
    symmetric bodies in R^n." Invent. Math. 88 (1987), 319-340.
  - Kuperberg, G. "From the Mahler conjecture to Gauss linking
    integrals." Geom. Funct. Anal. 18 (2008), 870-892.
  - Nazarov, F. "The Hormander proof of the Bourgain-Milman theorem."
    Geometric Aspects of Functional Analysis, Springer LNM 2050 (2012),
    335-343.
  - Berndtsson, B. "Complex integrals and Kuperberg's proof of the
    Bourgain-Milman theorem." Adv. Math. 388 (2021), 107927.
  - Karasev, R. "Mahler's conjecture for some hyperplane sections."
    Israel J. Math. 241 (2021), 795-815.
  - Lundin, M. "The extremal PSH for the complement of convex, symmetric
    subsets of R^N." Michigan Math. J. 32 (1985), 197-201.
  - Bos, L.; Calvi, J.-P.; Levenberg, N. "On the Siciak extremal function
    for real compact convex sets." Ark. Mat. 39 (2001), 245-262.

COMPANION PAPER (context, not a prerequisite).
  - OpenAI. "The Mahler Conjecture for General Convex Bodies."
    Preprint (September 2026). Sharp bound e^n for the nonsymmetric case.
    Not used here; the symmetric argument is independent.

END OF PROOF.

================================================================