§10 — the per-source discharge of Lemma 10.1's hypotheses

SectionTen.card_contSurj_eq (Lemma 10.1, counting form) is stated Γ-generically over the two hypotheses on a boundary map b:

• htame : Function.Surjective (tameCoord b) — the tame coordinate pr₁ ∘ b is onto Ttame;
• hwild : IsProP 2 (tameCoord b).toMonoidHom.ker — its kernel (the wild inertia) is pro-2.

This file discharges both for the two real sources, so eq_154 can invoke card_contSurj_eq twice. Since tameCoord (B.bA) = B.tameA and tameCoord (B.bF) = B.tameF (bA_apply_coe/bF_apply_coe):

• G_ℚ₂ (F-side) — generic, straight from the BoundaryMaps clauses tameF_surjective (surjectivity) and wild_isProP (= W_F = O₂(G_ℚ₂) pro-2, Lemma 3.3).
• Γ_A (A-side) — for the concrete boundaryMapsWitness: tameA := φ_A is surjective (phiA_surjective), and ker φ_A = W_A (the wild core) because the descent φ_A / W_A = ψ_W is injective (tameAEquiv, Prop 3.2's Γ_A-side iso), which is pro-2 by isProP_wildPart. Thus the A-side needs no BoundaryMaps amendment — the witness supplies it.

theorem GQ2.SectionTen.tameCoord_bF (B : BoundaryMaps) : tameCoord B.bF = B.tameF

The tame coordinate of b_{G_ℚ₂} is the boundary bundle's tame component tameF.

theorem GQ2.SectionTen.tameCoord_bA (B : BoundaryMaps) : tameCoord B.bA = B.tameA

The tame coordinate of b_{Γ_A} is the boundary bundle's tame component tameA.

G_ℚ₂ (F-side): from the BoundaryMaps fields

theorem GQ2.SectionTen.tameCoord_bF_surjective (B : BoundaryMaps) : Function.Surjective ⇑(tameCoord B.bF)

htame for G_ℚ₂: tameF is onto (BoundaryMaps.tameF_surjective).

theorem GQ2.SectionTen.tameCoord_bF_ker_isProP (B : BoundaryMaps) : IsProP 2 ↥(tameCoord B.bF).ker

hwild for G_ℚ₂: the wild inertia ker tameF = O₂(G_ℚ₂) is pro-2 (BoundaryMaps.wild_isProP).

Γ_A (A-side): the kernel of φ_A

theorem GQ2.SectionTen.ker_phiA : SectionThree.phiA.ker = SectionThree.wildPartB

ker φ_A = W_A. ⊇ is wildPartB_le_ker_phiA; ⊆ because the descent ψ_W = φ_A / W_A is injective — it is the underlying map of the Prop-3.2 iso tameAEquiv.

theorem GQ2.SectionTen.tameCoord_bA_surjective [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : Function.Surjective ⇑(tameCoord SectionThree.boundaryMapsWitness.bA)

htame for Γ_A (the witness boundaryMapsWitness): tameA = φ_A is onto (phiA_surjective).

theorem GQ2.SectionTen.tameCoord_bA_ker_isProP [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : IsProP 2 ↥(tameCoord SectionThree.boundaryMapsWitness.bA).ker

hwild for Γ_A (the witness): the wild inertia ker tameA = ker φ_A = W_A is pro-2 (isProP_wildPart).

Eq. (154) and the surjection-count theorem

Both live here (not in SectionTen) because eq_154's A-side needs the concrete boundaryMapsWitness (Γ_A's tame surjectivity phiA_surjective is witness-specific), and BoundaryMapsWitness is downstream of SectionTen. The proof then applies the proved thm_4_2 frame by frame.

theorem GQ2.SectionTen.main_surjection_count' [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (G : Type) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] : contSurjCount G = admissibleCount G

Theorem 1.2, surjection-count form (GQ2.main_surjection_count), proved from eq. (154) + Prop 2.3. The original Statement.lean placeholder was resolved by the statement-move pattern (Statement is upstream of the tower); the moved statement carries the tower-standing AbsGalQ2 instance binders.

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

• eq. (154) = ⟦eq-app-cup-convention⟧ [≥ drift window; verify against v428 tex]
• Lemma 10.1 = ⟦lem-tameframeexhaustion⟧
• Lemma 3.3 = ⟦lem-o2tame⟧
• Prop 2.3 = ⟦prop-epi-semantics⟧
• Prop 3.14 = ⟦prop-compatiblemarking⟧
• Prop 3.2 = ⟦prop-tamequotient⟧
• Theorem 1.2 = ⟦thm-main⟧