Finite tame quotients (Stage C, Lemma 3.1 lem:tamefinite)

Pure finite group theory, independent of Stages A/B and of the profinite machinery. This file formalises the manuscript's Lemma 3.1 (reference/q2_manuscript.tex, lines 405–419):

In every finite quotient generated by s, t with tˢ = t², the element t has odd order, and the quotient has the form Cₑ ⋊ Cₙ (e odd, s⁻¹ t s = t²). Every normal 2-subgroup of such a quotient is central and lies in the unramified cyclic direction.

We use the manuscript's right-conjugation convention rconj x g = g⁻¹ * x * g (Foundation/RightConj).

theorem Q2Presentation.finite_tame_tau_odd {G : Type u_1} [Group G] [Finite G] {s t : G} (h : rconj t s = t ^ 2) : Odd (orderOf t)

Lemma 3.1, oddness part. In a finite group, if t satisfies the tame relation tˢ = t² (i.e. rconj t s = t ^ 2), then t has odd order.

Proof (manuscript l.416): conjugation preserves order, so orderOf (rconj t s) = orderOf t; on the other hand orderOf (t²) = orderOf t / gcd (orderOf t) 2. Combining forces gcd (orderOf t) 2 = 1, i.e. Odd (orderOf t).

theorem Q2Presentation.finite_tame_normal_two_subgroup_unramified {G : Type u_1} [Group G] [Finite G] {s t : G} (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) (N : Subgroup G) [N.Normal] (hN2 : IsPGroup 2 ↥N) : N ≤ Subgroup.center G ∧ N ⊓ Subgroup.zpowers t = ⊥

Lemma 3.1, normal 2-subgroup part. Let G be a finite group generated by s, t with the tame relation tˢ = t². Then every normal 2-subgroup N of G is central (N ≤ center G) and lies in the unramified cyclic direction, formalised as having trivial intersection with the tame inertia I = ⟨t⟩ (so N injects into the procyclic unramified quotient G/⟨t⟩).

This matches the manuscript (reference/q2_manuscript.tex, l.412 & l.418): "every normal 2-subgroup of such a quotient is central and lies in the unramified cyclic direction"; the proof there shows N ∩ I = 1 and [N, I] ≤ N ∩ I = 1.

Proof: I = ⟨t⟩ has odd order (finite_tame_tau_odd); being a 2-group, N meets I trivially (N ⊓ I = ⊥). The relation makes I normal with cyclic — hence abelian — quotient G/I, so for every g and n ∈ N the commutator g n g⁻¹ n⁻¹ lies in both N and I, i.e. in N ⊓ I = ⊥; thus every g commutes with every n ∈ N, i.e. N ≤ center G.