diff --git a/global_solvably_closed_galois_v2.txt b/global_solvably_closed_galois_v2.txt
index 2004261..da6b006 100644
--- a/global_solvably_closed_galois_v2.txt
+++ b/global_solvably_closed_galois_v2.txt
@@ -10,114 +10,6 @@ A complete, self-contained proof of Uchida's conjecture.
     hypothesis is required.
 
 
-CONTENTS
---------
- 0.  What this paper is about, in plain words
- 1.  Conventions, solvably closed fields, and the five black boxes
- 2.  Additive characters and Frobenius detection
- 3.  Extension to the normalizer, and generation by Frobenius
- 4.  Matching residue characteristics
- 5.  Identifying the homomorphism, and the main theorem
- 6.  References
-
-
-=====================================================================
-0.  WHAT THIS PAPER IS ABOUT, IN PLAIN WORDS
-=====================================================================
-
-A number field is a field you get by adjoining finitely many roots
-of polynomials to the rational numbers Q; for example Q(i), where
-i^2 = -1. Attach to a number field F all of its algebraic extensions
-at once. The symmetries of that giant object form the absolute
-Galois group G_F. Its finite quotients are exactly the Galois groups
-of the finite Galois extensions of F.
-
-A famous theme of arithmetic geometry ("anabelian geometry", due to
-Neukirch, Iwasawa, Uchida and others) says: G_F remembers F, and in
-fact remembers maps between fields. Two prototype theorems drive
-this paper:
-
-  (a) ISOMORPHISM THEOREM. If two such absolute Galois groups are
-      abstractly isomorphic, the number fields are isomorphic. More
-      precisely (Uchida 1979), an isomorphism of Galois groups of
-      "solvably closed" extensions comes from a field isomorphism.
-
-  (b) THE QUESTION OF THIS PAPER. What happens for HOMOMORPHISMS
-      that are not isomorphisms but still "open" (their image is an
-      open, hence large, subgroup)? Uchida conjectured in 1981 that
-      every such open homomorphism is again induced by a field
-      embedding. We prove this in full, with no hypothesis on the
-      kernel.
-
-"Solvably closed" is a technical convenience. A field extension E/F
-is solvably closed if E has no nontrivial abelian extension. The
-algebraic closure Q-bar is the leading example; the maximal
-prosolvable extension Q^s of Q (the union of all finite solvable
-Galois extensions of Q) is another. Every solvably closed field
-contains Q^s. Because of this, the whole problem reduces to a single
-statement about one object:
-
-    P = Gal(Q^s / Q),
-
-the absolute Galois group of the maximal prosolvable extension. The
-central technical theorem (Theorem 5.3 below) says: every continuous
-open homomorphism G_F -> P is conjugate, inside P, to ordinary
-restriction. Everything else is bookkeeping that passes from P down
-to a general pair of solvably closed fields.
-
-WHY IT IS HARD, AND THE STRATEGY.
-    Uchida already knew that an open homomorphism phi : G_F -> P
-    behaves arithmetically "most of the time": for any fixed auxiliary
-    prime l, at almost every prime where a pro-l piece of local
-    inertia survives, phi matches source primes to target primes
-    (the "partial local correspondence"). The trouble is that WHICH
-    primes match, and which are missed, depends on l. Different l
-    give different, incompatible-looking partial pictures. The task
-    is to extract one clean global statement (equality of cyclotomic
-    characters) out of these l-dependent shadows.
-
-    Three ideas make this work.
-
-    (1) CHARACTER TESTS. Continuous additive Q_l-valued characters
-        x of a Galois group are determined by their values at
-        Frobenius elements: if x vanishes at infinitely many primes
-        of residue degree one, then x is zero. This rests on a
-        logarithm-rank lemma (a special case of the l-adic
-        Waldschmidt-Masser theorem), which we prove in full. Variants
-        for averaged and corestricted characters handle primes of
-        any residue degree.
-
-    (2) GENERATION. Restricting to an open normal subgroup and
-        extending to its normalizer, we enlarge finite quotients of
-        P using many copies of a regular module (a Kummer trick from
-        Uchida 1979). This produces enough characters to show that
-        images of source Frobenius elements generate entire target
-        cyclic subgroups. Consequences: the extended map is
-        SURJECTIVE, and its cyclotomic logarithms agree with the
-        source for every prime l in an infinite congruence class.
-
-    (3) MATCHING AND UNIFORMITY. After ascending to Q(i) and a
-        quadratic preimage K, one Kummer estimate bounds the number
-        of target primes that the partial correspondence can miss
-        for a fixed l by a number depending only on K, not on l.
-        A simultaneous power-residue construction then picks one l
-        that excludes all the "wrong characteristic" partners at
-        once, forcing a genuine same-characteristic partner for
-        almost every split target prime. Splitting completely in a
-        suitable finite extension finally aligns the two character
-        pullbacks, and a faithful representation identifies the maps
-        modulo every finite quotient. Compactness produces a single
-        conjugation.
-
-The proof below makes each of these ideas precise. Part 1 fixes
-notation and lists the five external inputs (Uchida isomorphism,
-centralizer lemma, Uchida local correspondence, Hoshi cyclotomic
-criterion, and the fact that Q^s is solvably closed). The remaining
-parts are self-contained, with the log-rank lemma and every other
-substantive step proved in full.
-
-
-=====================================================================
 1.  CONVENTIONS, SOLVABLY CLOSED FIELDS, AND THE BLACK BOXES
 =====================================================================