The anabelian bridge: B8 ⟹ Lemma 3.7

The paper's Lemma 3.7 constructs, for each u ∈ ℤ₂ˣ, an automorphism Ψ_u of D₀ acting on the abelianization by Ā ↦ uĀ, S̄ ↦ uS̄, out of B8's cyclotomic action φ_u on Δ = ⟨P,T⟩_pro-2. This file proves it (GQ2.lemma_3_7, statement verbatim SectionThree.lemma_3_7).

The proof, reorganized (deviation note)

The paper (proof of Lemma 3.7) runs through the one-relator group E□ = ⟨P,T,A | PTA²⟩_pro-2 ≅ ⟨P,A⟩_pro-2, a Tietze elimination, and a cube-root comparison. We inline this scaffolding:

• B8's three conjugation identities combine (via φ_u being a homomorphism and PTC = 1) into the single Δ-identity peripheral_identity (*) below.
• The words P ↦ s³, T ↦ s⁻³a⁻² define a continuous hom λ : Δ → D₀ (lambdaHom; freeness of Δ — no relator check). Pushing (*) along λ gives exactly the conjugation identity that makes the marking A ↦ (a^u)^{κ_C}, S ↦ (s^u)^{κ_P}, Y ↦ κ_P⁻¹ y κ_T respect the Demushkin relator in its HNN form y⁻¹sy = s⁻³a⁻² (paper (16)) — so Ψ_u exists by the universal property of the presentation (d0Lift).
• Surjectivity is the pro-2 Frattini criterion: in every index-2 quotient the u-powers act trivially (u is odd) and the conjugators die, so Ψ_u's generator-images have the same images as the generators. Hopficity (profinite_hopfian) upgrades to bijectivity.
• The cube-root comparison and the intermediate automorphism θ_u of the paper are not needed: their only role was to transit the identities from Δ-coordinates to E-coordinates, which the direct λ-push does. (The E□ ≅ ⟨P,A⟩ Tietze step is likewise absorbed.)

The u-th powers are B8's x ^ᶻ ι u; by the bundle's hι_proj pinning (see the GQ2/PeripheralAction.lean docstring) these are the 2-adic powers zpowZtwo x u on every pro-2 group (zpowHat_iota). The compatibility of that pinning with the original hι_one : ι 1 = ω₂ is proved here: zhatProjTwo_omega2 : zhatProjTwo ω₂ = ofAdd 1, via zpowHat_omega2_eq_self (x ^ᶻ ω₂ = x on pro-2 groups — the idempotent acts as the identity precisely on the pro-2 part).

Everything is at the standard three axioms plus (where marked) the B8 bundle argument.

File organisation. The proof is split into Construction (the bridge, automorphisms, and lifting half) and Classification (the converse classification argument). This umbrella preserves the original import path and public declaration names.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (11) = ⟦eq-Bsplit⟧
• Lemma 3.6 = ⟦lem-peripheralpower⟧ (= lemma 3.7 in current tex)
• Lemma 3.7 = ⟦lem-squarerootHNN⟧ (= lemma 3.8 in current tex)
• Proposition 3.8 = ⟦prop-orientationlift⟧ (= proposition 3.9 in current tex)