The candidate boundary package boundaryPackage_GammaA (Stage C, Prop 3.14)

This file assembles the candidate-side Stage-C data of Γ_A into a single BoundaryPackage GammaA, realising the manuscript's Proposition 3.14 (reference/q2_manuscript.tex, prop:compatiblemarking, l.1085–1110) and plan Turn 4 §6: the common tame quotient Γ_A ↠ T_A and the maximal pro-2 quotient Γ_A ↠ Π may be chosen with a common unramified character ν : Γ_A ↠ ℤ₂, compatible after passage to every finite quotient C_{2^m}.

The three ingredients are already built:

• tameMap := gammaTameMap (Boundary/CandidateTame.lean), surjective by gammaTameMap_surjective;
• pro2Map := p (Boundary/CandidatePro2.lean), the canonical pro-2 quotient Γ_A ⟶ Π (its generator-image lemmas p_gammaGen_* make the compatibility immediate), surjective by p_surjective;
• nu := gammaTameMap ≫ nu_t, so the tame compatibility tame_nu is rfl.

The key compatibility pro2_nu

The load-bearing field is pro2_nu : p ≫ nu_2 = gammaTameMap ≫ nu_t. Both sides are continuous homs Γ_A ⟶ ℤ₂; they agree on the four topological generators gammaGen and hence everywhere, by dense generation (gammaGen_hom_ext, the same uniqueness principle EpiSemantics/B5 uses, i.e. Profinite.hom_ext_of_dense

• MonoidHom.eqOn_closure). On generators the manuscript marking σ↦1, τ,x₀,x₁↦0 reads off the existing generator-image lemmas:

gen	p	nu_2 ∘ p	gammaTameMap	nu_t ∘ gammaTameMap
σ	piSigma	z2One (nu_2_piSigma)	tameSigma	z2One (nu_t_tameSigma)
τ	1	1	tameTau	z2Zero (nu_t_tameTau)
x₀	piX0	z2Zero (nu_2_piX0)	1	1
x₁	piX1	z2Zero (nu_2_piX1)	1	1

with z2Zero = 1 (the 2-adic 0 is the multiplicative identity of ℤ₂, z2Zero_eq_one below) closing the τ, x₀, x₁ rows.

theorem Q2Presentation.z2Zero_eq_one : z2Zero = 1

The 2-adic integer 0 is the multiplicative identity of ℤ₂: z2Zero = 1. Checked layerwise — every reduction of z2Zero is ofAdd 0 = 1.

theorem Q2Presentation.gammaA_pro2_nu : CategoryTheory.CategoryStruct.comp p nu_2 = CategoryTheory.CategoryStruct.comp gammaTameMap nu_t

Compatibility of the two markings of Γ_A (manuscript Prop 3.14, prop:compatiblemarking): the pro-2 quotient p : Γ_A ⟶ Π and the tame quotient gammaTameMap : Γ_A ⟶ T_A induce the same unramified character Γ_A ⟶ ℤ₂, i.e. p ≫ ν₂ = gammaTameMap ≫ ν_t.

Both composites are continuous homs Γ_A ⟶ ℤ₂, so it suffices to check equality on the four topological generators gammaGen (gammaGen_hom_ext). There the manuscript marking σ↦1, τ,x₀,x₁↦0 is exactly the recorded generator images: σ ↦ z2One on both sides, while τ, x₀, x₁ ↦ z2Zero = 1.

noncomputable def Q2Presentation.boundaryPackage_GammaA : BoundaryPackage GammaA

The candidate boundary package (manuscript Prop 3.14, prop:compatiblemarking; plan Turn 4 §6). The Stage-C data of Γ_A: the common tame quotient gammaTameMap, the maximal pro-2 quotient p : Γ_A ⟶ Π, and the common unramified character ν = gammaTameMap ≫ ν_t, through which both factor.

Equations

• One or more equations did not get rendered due to their size.

Acceptance checks