§4: the common boundary and Theorem 4.2 #

The paper's §4 fixes, once and for all, a common finite-headed boundary shared by the two source groups Γ_A and G_ℚ₂, and states the boundary-framed exact-image theorem (Thm 4.2) — the technical heart of the proof of eq. (154), proved in §9 by strong induction on |L_Y|. This file provides the §4 objects; the statement of Theorem 4.2 (thm_4_2) lives in GQ2/ThmFourTwo.lean, because its §9 proof machinery imports this file, with the explicit hE2 hypothesis required by the encoded frame.

The paper's objects and their encodings #

Ttame (§3 opening display): the "finite-quotient tame group" ⟨σ, τ ∣ τ^σ = τ²⟩_prof — profinitePresentation {tameWord} with tameWord = conjP τ σ * (τ²)⁻¹ on σ, τ = of 0, of 1 (paper conventions x^g = g⁻¹xg, GQ2/Words.lean).
PiBd (paper Π, Prop 3.10 eq. (20)): the pro-2 group ⟨σ, x₀, x₁ ∣ x₀^{σ²} x₀ [x₁,σ] = 1⟩_pro-2, encoded as maxProPQuotient 2 (profinitePresentation {piRelator}) — a pro-2 presentation is the maximal pro-2 quotient of the profinite presentation (same universal property on pro-2 targets; this is the repo's standing encoding, cf. Δ in GQ2/PeripheralAction.lean). Generator order σ, x₀, x₁ = of 0, of 1, of 2; the relator's conjugation is by σ² (eq. (24) — note the superscript, easily lost: x₀^{σ²}, not x₀^σ).
Ztwo (paper Z₂): the additive 2-adics as a profinite group, encoded maxProPQuotient 2 Zhat (the pro-2 completion of ℤ; GQ2/Zhat.lean). ztwoOne is the image of 1 ∈ ℤ.
nuT, nuTwo (Prop 3.14's ν_t and eq. (21)'s ν₂): the unramified markings, pinned by ν_t(σ) = 1, ν_t(τ) = 0 and ν₂(σ) = 1, ν₂(x₀) = ν₂(x₁) = 0, built by presentationLift (kill the relator, descend) and — for nuTwo — the universal property of maxProP (proPKernel_le_ker; the target Ztwo is pro-2 by isProP_maxProPQuotient). The generator values are proved below (nuT_tameSigma, …) — they are this file's stress tests.
boundarySubgroup / Boundary (eq. (26)): ∂bd = Ttame ×_{Z₂} Π, encoded as the equalizer subgroup {x : Ttame × Π ∣ ν_t x.1 = ν₂ x.2} — closed (T2 target), hence profinite.
BoundaryFrame (eq. (28)): the fixed frame data — a finite tame quotient α : Ttame ↠ H, an elementary abelian 2-group E ([CommGroup E] + exponent_two), and ψ̄ : Π → E; frameMap is β(t, p) = (α t, ψ̄ p).
MarkedTarget (Definition 4.1): 𝒴 = (Y, L_Y, π_Y, θ_Y) with L_Y ◁ Y a finite 2-group, π_Y : Y ↠ H with kernel L_Y, θ_Y : Y → E. [Finite Y] is carried as a parameter (the paper implies it: L_Y finite + H finite); IsPGroup 2 L_Y then says exactly "finite 2-group". stratum is the sub-target 𝒥 = (J, J ∩ L_Y, π_Y|_J, θ_Y|_J) for J ≤ Y projecting onto H.
IsBoundaryLift / BoundaryLifts / exactImageCount (eq. (29)): the boundary equation q_Y ∘ f = β ∘ b_Γ (pointwise, as one H × E-valued equation), the set of continuous epimorphisms satisfying it, and e^β_Γ(𝒴) = Nat.card of it. Nat.card is 0 on infinite sets — same convention as contSurjCount/admissibleCount; under topological finite generation the set is genuinely finite (finite_boundaryLifts). §5's "ρ : Γ ↠ C satisfies the boundary equation" and §8's X_Γ(C) (Def 8.1) are BoundaryLifts verbatim.

`BoundaryMaps`: the epimorphisms of (27) as an interface bundle #

Theorem 4.2 is stated relative to the maps b_Γ : Γ ↠ ∂bd of eq. (27). The structure BoundaryMaps carries the tame and pro-2 components of both maps together with exactly the properties Proposition 3.14 asserts; GQ2/BoundaryMapsWitness.lean constructs the concrete witness used by the final assembly.

Γ_A-side: pinned rigidly by generator values — tameA : σ ↦ σ, τ ↦ τ, x₀, x₁ ↦ 1 and pro2A : σ ↦ σ, τ ↦ 1, xᵢ ↦ xᵢ (Prop 3.10 and Prop 3.14's proof). A continuous hom out of Γ_A is determined by its values on the four topological generators, so these eight equations determine tameA/pro2A uniquely.
G_ℚ₂-side: pinned intrinsically — tameF is surjective with kernel the characteristic 2-core (Lemma 3.3's characterization of wild inertia W_F = O₂(G_ℚ₂): the kernel is pro-2 normal and contains every closed normal pro-2 subgroup), and pro2F is surjective with kernel exactly proPKernel 2 AbsGalQ2 (i.e. the maximal pro-2 quotient map).
both sides: the ν-compatibility (compatA/compatF — Prop 3.14's conclusion; this is what makes the pairs land in ∂bd) and joint surjectivity onto ∂bd (eq. (27); the paper derives it by profinite Goursat, so instantiators may prove rather than assume it).

thm_4_2 quantifies over all BoundaryMaps witnesses. This is the faithful reading: Prop 3.14 says the quotient maps "may be chosen so that" the compatibility holds, and §4 fixes such a choice "once and for all" — nothing after §4 uses more about the choice than the properties above. In particular, the full marking from Remark 3.15 is represented by the ν-compatibility fields rather than reconstructed later.

Axioms: none — the statement layer is axiom-free. The literature inputs listed for Theorem 4.2 in Appendix D enter only through the §§5–9 proof.

Descending homs from a profinite presentation #

A continuous hom out of the free profinite group killing every relator kills their closed normal closure (the kernel is closed and normal), hence descends to the presented group. Stated here for the ν-maps used below.

§4: the common boundary and Theorem 4.2 #

The paper's objects and their encodings #

BoundaryMaps: the epimorphisms of (27) as an interface bundle #

Descending homs from a profinite presentation #

The three boundary constituents: Ttame, Π, Z₂ #

The unramified markings ν_t and ν₂ (Prop 3.14, eq. (21)) #

The common boundary ∂bd = Ttame ×_{Z₂} Π (eq. (26)) #

The frame (eq. (28)) #

Boundary-framed marked targets (Definition 4.1) #

The exact-image counts (eq. (29)) #

The Prop 3.14 interface: the epimorphisms b_Γ (eq. (27)) #

Theorem 4.2 #

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

`BoundaryMaps`: the epimorphisms of (27) as an interface bundle #

The three boundary constituents: `Ttame`, `Π`, `Z₂` #

The unramified markings `ν_t` and `ν₂` (Prop 3.14, eq. (21)) #

The common boundary `∂bd = Ttame ×_{Z₂} Π` (eq. (26)) #

The Prop 3.14 interface: the epimorphisms `b_Γ` (eq. (27)) #