diff --git a/symmetric_mahler_equality_v2.txt b/symmetric_mahler_equality_v2.txt
index a0d3e29..e182d61 100644
--- a/symmetric_mahler_equality_v2.txt
+++ b/symmetric_mahler_equality_v2.txt
@@ -15,97 +15,6 @@ CONTENTS
     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
 ================================================================