The finite pro-2 specialization of the Q₂ words (Stage C, Proposition 3.10)

This file is the finite-2-group avatar of the manuscript's maximal pro-2 quotient statement (reference/q2_manuscript.tex, Proposition 3.10 prop:pro2, lines ~959–995). It is pure finite group theory: independent of Stage B (GammaA) and of all profinite machinery.

The manuscript computes that, in a finite 2-group quotient,

• the tame relation τ^σ = τ² forces τ = 1 (Lemma 3.1, lem:tamefinite);
• the profinite idempotent ω₂ acts as the identity, so u_i = x_i, d₀ = c₀ = 1, g₀ = σ², d_g = h_c = 1, h₀ = x₀^{σ²} x₀, and u₁⁻¹ x₁^σ = [x₁, σ];
• hence the wild relator collapses to x₀^{σ²} x₀ [x₁, σ].

So in a finite 2-group an admissible marking is exactly the data of the presentation Π = ⟨σ, x₀, x₁ ∣ x₀^{σ²} x₀ [x₁,σ] = 1⟩ with τ = 1.

This is the designated place where the abstract word language GExpr.eval (of Foundation/Expr, Foundation/Q2Words) is unfolded explicitly; downstream files consume admissible_twoGroup_iff_piMarked as a black box.

theorem Q2Presentation.admissible_twoGroup_iff_piMarked {G : Type u_1} [Group G] [Finite G] (hG2 : IsPGroup 2 G) (q : Marking G) : Admissible q ↔ q Gen.tau = 1 ∧ Subgroup.closure {q Gen.sigma, q Gen.x0, q Gen.x1} = ⊤ ∧ rconj (q Gen.x0) (q Gen.sigma ^ 2) * q Gen.x0 * commutatorW (q Gen.x1) (q Gen.sigma) = 1

Proposition 3.10 (finite-2-group form). For a finite 2-group G, a marking q is admissible iff τ = 1, the remaining three images σ, x₀, x₁ generate G, and the collapsed wild relator x₀^{σ²} x₀ [x₁, σ] = 1 holds.

The two 2-core side conditions of Admissible are automatic here (O₂(G) = ⊤), the tame relator is equivalent to τ = 1 (via finite_tame_tau_odd together with the 2-power order of every element), and powOmega2 = id collapses the wild word to the displayed relator.