The tame 2-quotient factoring + the B10′ orientation package

The nuT-factoring brick of the analytic-hunram derivation (docs/orchestration/p15f2c2c-handoff.md §half-(B) step 4). Three pieces:

• (i) τ-death in 2-groups (pure finite group theory, axiom-free): any group hom φ : Ttame →* Q into a finite 2-group Q kills tameTau — φ tameTau = 1. From the pushed tame relation (φ σ)⁻¹ (φ τ) (φ σ) = (φ τ)², Tame.tame_odd_order gives orderOf (φ τ) odd; in a 2-group it is a power of 2; odd ∧ 2-power ⟹ 1.

• (ii) the factoring (axiom-free): any continuous φ : Ttame → Q into a finite discrete 2-group factors through nuT : Ttame → Ztwo (the pro-2 tame character).

• (iii) TameUnitOrientation (std-3 + B10′): the B10′-clause shape, plus its discharge at the axiom witness boundaryMapsWitness.tameF.

Parts (i) and (ii) are std-3; part (iii) uses B10′.

(i) τ-death in a finite 2-group

theorem GQ2.map_tameTau_eq_one {Q : Type u_1} [Group Q] [Finite Q] (hQ : IsPGroup 2 Q) (φ : ↑Ttame.toProfinite.toTop →* Q) : φ tameTau = 1

τ-death (the Lemma 6.17 vanishing proof(i)): a group hom from T_tame into a finite 2-group kills the tame generator τ. The tame relation σ⁻¹ τ σ = τ² pushes to Q, so Tame.tame_odd_order makes orderOf (φ τ) odd; in the 2-group Q it is a power of 2; the only odd power of 2 is 1, so φ τ = 1. Pure finite group theory — no topology, no axiom.

(ii) the factoring: continuous homs into a pro-2 group factor through nuT

Both nuT and any continuous hom into a pro-2 group factor through the maximal pro-2 quotient T_tame(2); and nuT induces there an isomorphism (its kernel is exactly the pro-2 kernel: ker nuT ≤ proPKernel 2 T_tame). Composing with proPKernel_le_ker gives the factoring.

theorem GQ2.maxProPMk_tameTau : (maxProPMk 2 ↑Ttame.toProfinite.toTop) tameTau = 1

τ dies in the maximal pro-2 quotient T_tame(2): maxProPMk 2 T_tame τ = 1. By part (i) map_tameTau_eq_one, τ lands in every open normal U with a 2-group quotient, hence in the pro-2 kernel.

theorem GQ2.ker_nuT_le_proPKernel : nuT.ker ≤ proPKernel 2 ↑Ttame.toProfinite.toTop

ker ν_t ≤ proPKernel 2 T_tame: maxProPMk : T_tame ↠ T_tame(2) factors through ν_t : T_tame ↠ ℤ₂. Build ρ' : ℤ₂ → T_tame(2) from the ẑ-power hom ẑ ↦ (maxProPMk σ)^ẑ (descended through ℤ₂ = ẑ(2), the target being pro-2), matching maxProPMk on σ and (via maxProPMk_tameTau) on τ; density on {σ, τ} gives maxProPMk = ρ' ∘ ν_t, so ν_t x = 1 ⟹ maxProPMk x = 1 ⟹ x ∈ proPKernel.

theorem GQ2.map_eq_one_of_nuT_eq_one {Q : Type u_1} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q] (hQ : IsProP 2 Q) (φ : ↑Ttame.toProfinite.toTop →ₜ* Q) {x : ↑Ttame.toProfinite.toTop} (hx : nuT x = 1) : φ x = 1

The factoring (the Lemma 6.17 vanishing proof(ii)): a continuous hom φ : T_tame → Q into a pro-2 group kills everything ν_t kills — ν_t x = 1 ⟹ φ x = 1. (ker ν_t ≤ proPKernel 2 T_tame ≤ ker φ, the second inclusion by proPKernel_le_ker.)

theorem GQ2.map_eq_one_of_nuT_eq_one_finite {Q : Type u_1} [Group Q] [Finite Q] [TopologicalSpace Q] [DiscreteTopology Q] (hQ : IsPGroup 2 Q) (φ : ↑Ttame.toProfinite.toTop →ₜ* Q) {x : ↑Ttame.toProfinite.toTop} (hx : nuT x = 1) : φ x = 1

The factoring, finite discrete 2-group form — the shape the c2c4 unit-image argument consumes (Q = the 2-part quotient of Gal(F₀/ℚ₂)).

(iii) the B10′ orientation clause

def GQ2.TameUnitOrientation (R : LocalReciprocity) (tameF : AbsGalQ2 →ₜ* ↑Ttame.toProfinite.toTop) : Prop

TameUnitOrientation (the Lemma 6.17 vanishing proof(iii)): the B10′ orientation clause for an arbitrary tame coordinate tameF : G_ℚ₂ → T_tame — every local-reciprocity image of a 2-adic unit is killed by ν_t ∘ tameF. For the axiom bundle's own tame coordinate this is OrientedTameQuotient's nuT_recip_unit; a general B : BoundaryMaps carries no reciprocity clause, so the moved lemma_6_17_vanish threads TameUnitOrientation localReciprocity B.tameF as one hypothesis (the hc/hV2 precedent), discharged at boundaryMapsWitness.

Equations

• GQ2.TameUnitOrientation R tameF = ∀ (u : ℤ_[2]ˣ) (g : GQ2.AbsGalQ2), GQ2.toAb g = R.recip (GQ2.unitEmbed u) → GQ2.nuT (tameF g) = 1