The auxiliary words (1)–(3) and the admissibility predicate

This file makes the paper's presentation data completely concrete for finite groups, which is all the surjection-count form of Theorem 1.2 ever needs (paper §2, App. A–B).

Conventions match the paper exactly:

• x ^ g = g⁻¹ * x * g (conjP)
• [x, y] = x⁻¹ * y⁻¹ * x * y (commP)
• x ^ ω₂ = the 2-primary part of x (powOmega2)

ω₂ ∈ ℤ̂ is the idempotent that is 1 on the 2-adic factor and 0 on every odd factor. On a single element x of finite order d = 2^a · m (m odd), x ^ ω₂ is the projection of x to the 2-primary part of ⟨x⟩, i.e. x ^ e for any integer e ≡ 1 (mod 2^a), e ≡ 0 (mod m). We realise such an e concretely as omega2Exp d. Because orderOf x ∣ Monoid.exponent G, using orderOf x per element agrees with a single global integer exponent on the whole finite group, so this is faithful to the profinite ω₂.

The ω₂ exponent

def GQ2.omega2Exp (n : ℕ) : ℕ

A concrete nonnegative-integer representative of the profinite idempotent ω₂ modulo n: the unique e ∈ [0, n) with e ≡ 1 (mod 2^{v₂ n}) and e ≡ 0 (mod oddpart n). Realised as (oddpart n) ^ (2^{v₂ n - 1}) (Euler: m^{φ(2^a)} ≡ 1 mod 2^a, and it is ≡ 0 mod m).

Equations

• GQ2.omega2Exp n = if n.factorization 2 = 0 then 0 else (n / 2 ^ n.factorization 2) ^ 2 ^ (n.factorization 2 - 1) % n

noncomputable def GQ2.powOmega2 {G : Type u_1} [Monoid G] (x : G) : G

x ^ ω₂: the 2-primary part of a finite-order element. Noncomputable because it uses orderOf; a computable variant parametrized by an explicit exponent (a multiple of Monoid.exponent G) is a follow-up for the App. B cross-check.

Equations

• GQ2.powOmega2 x = x ^ GQ2.omega2Exp (orderOf x)

def GQ2.«term_^ω₂» : Lean.TrailingParserDescr

x ^ ω₂: the 2-primary part of a finite-order element. Noncomputable because it uses orderOf; a computable variant parametrized by an explicit exponent (a multiple of Monoid.exponent G) is a follow-up for the App. B cross-check.

Equations

• GQ2.«term_^ω₂» = Lean.ParserDescr.trailingNode `GQ2.«term_^ω₂» 1024 0 (Lean.ParserDescr.symbol "^ω₂")

The paper's conventions for conjugation and commutator

def GQ2.conjP {G : Type u_1} [Group G] (x g : G) : G

Right conjugation x ^ g = g⁻¹ x g (paper's convention).

Equations

• GQ2.conjP x g = g⁻¹ * x * g

def GQ2.commP {G : Type u_1} [Group G] (x y : G) : G

Commutator [x, y] = x⁻¹ y⁻¹ x y (paper's convention).

Equations

• GQ2.commP x y = x⁻¹ * y⁻¹ * x * y

def GQ2.«term_^c_» : Lean.TrailingParserDescr

Right conjugation x ^ g = g⁻¹ x g (paper's convention).

Equations

• GQ2.«term_^c_» = Lean.ParserDescr.trailingNode `GQ2.«term_^c_» 1024 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^c ") (Lean.ParserDescr.cat `term 0))

A marked generating tuple (σ, τ, x₀, x₁)

structure GQ2.Marking (G : Type u_1) : Type u_1

A "marking": an ordered quadruple of group elements (σ, τ, x₀, x₁).

• σ : G
• τ : G
• x₀ : G
• x₁ : G

@[implicit_reducible]

instance GQ2.instDecidableEqMarking {G✝ : Type u_1} [DecidableEq G✝] : DecidableEq (Marking G✝)

Equations

• GQ2.instDecidableEqMarking = GQ2.instDecidableEqMarking.decEq

def GQ2.instDecidableEqMarking.decEq {G✝ : Type u_1} [DecidableEq G✝] (x✝ x✝¹ : Marking G✝) : Decidable (x✝ = x✝¹)

Equations

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

The auxiliary words, transcribed from the machine-readable block (App. B) and eqs. (1)–(3).

sigma2 = sigma^ω₂            g0 = sigma2^2
u0 = (x0*tau)^ω₂             u1 = (x1*tau)^ω₂
d0 = u0*x0⁻¹                 z0 = x0^sigma2
c0 = [d0, z0]               dg = d0^g0
hcomm = [dg, d0]            h0 = (x0^g0)*x0*dg*d0*d0^2*hcomm

noncomputable def GQ2.Marking.sigma2 {G : Type u_1} [Group G] (t : Marking G) : G

σ₂ = σ ^ ω₂.

Equations

• t.sigma2 = GQ2.powOmega2 t.σ

noncomputable def GQ2.Marking.u {G : Type u_1} [Group G] (t : Marking G) (xi : G) : G

u i = (xᵢ τ) ^ ω₂, with u 0 and u 1 the two used in the paper.

Equations

• t.u xi = GQ2.powOmega2 (xi * t.τ)

noncomputable def GQ2.Marking.u0 {G : Type u_1} [Group G] (t : Marking G) : G

u₀ = (x₀ τ) ^ ω₂.

Equations

• t.u0 = t.u t.x₀

noncomputable def GQ2.Marking.u1 {G : Type u_1} [Group G] (t : Marking G) : G

u₁ = (x₁ τ) ^ ω₂.

Equations

• t.u1 = t.u t.x₁

noncomputable def GQ2.Marking.d0 {G : Type u_1} [Group G] (t : Marking G) : G

d₀ = u₀ x₀⁻¹.

Equations

• t.d0 = t.u0 * t.x₀⁻¹

noncomputable def GQ2.Marking.z0 {G : Type u_1} [Group G] (t : Marking G) : G

z₀ = x₀ ^ σ₂.

Equations

• t.z0 = GQ2.conjP t.x₀ t.sigma2

noncomputable def GQ2.Marking.c0 {G : Type u_1} [Group G] (t : Marking G) : G

c₀ = [d₀, z₀].

Equations

• t.c0 = GQ2.commP t.d0 t.z0

noncomputable def GQ2.Marking.g0 {G : Type u_1} [Group G] (t : Marking G) : G

g₀ = σ₂².

Equations

• t.g0 = t.sigma2 ^ 2

noncomputable def GQ2.Marking.dg {G : Type u_1} [Group G] (t : Marking G) : G

d_g = d₀ ^ g₀.

Equations

• t.dg = GQ2.conjP t.d0 t.g0

noncomputable def GQ2.Marking.hc {G : Type u_1} [Group G] (t : Marking G) : G

h_c = [d_g, d₀].

Equations

• t.hc = GQ2.commP t.dg t.d0

noncomputable def GQ2.Marking.h0 {G : Type u_1} [Group G] (t : Marking G) : G

h₀ = (x₀ ^ g₀) · x₀ · d_g · d₀ · d₀² · h_c. (Note the bare d₀ between d_g and d₀² — paper eq. (3) and the App. B machine block agree on dg*d0*d0^2; it is what makes h₀ an instance of the class-two word h_ϕ(X,D) = ϕ(X)·X·ϕ(D)·D·D²·[ϕ(D),D] of paper Lemma 5.2. A step-1 transcription dropped it; see docs/erratum-h0-transcription.md.)

Equations

• t.h0 = GQ2.conjP t.x₀ t.g0 * t.x₀ * t.dg * t.d0 * t.d0 ^ 2 * t.hc

The two relations

def GQ2.Marking.TameRel {G : Type u_1} [Group G] (t : Marking G) : Prop

The tame relation τ^σ = τ² (eq. 5).

Equations

• t.TameRel = (GQ2.conjP t.τ t.σ = t.τ ^ 2)

def GQ2.Marking.WildRel {G : Type u_1} [Group G] (t : Marking G) : Prop

The wild relation h₀ u₁⁻¹ x₁^σ c₀ = 1 (eq. 6).

Equations

• t.WildRel = (t.h0 * t.u1⁻¹ * GQ2.conjP t.x₁ t.σ * t.c0 = 1)

def GQ2.Marking.Generates {G : Type u_1} [Group G] (t : Marking G) : Prop

The marking generates the whole group.

Equations

• t.Generates = (Subgroup.closure {t.σ, t.τ, t.x₀, t.x₁} = ⊤)

def GQ2.Marking.Pro2Core {G : Type u_1} [Group G] (t : Marking G) : Prop

The 2-core condition: the normal closure of {x₀, x₁} is a 2-group (paper Prop. 2.3: equivalent to x₀, x₁ ∈ O₂(G)).

Equations

• t.Pro2Core = IsPGroup 2 ↥(Subgroup.normalClosure {t.x₀, t.x₁})

def GQ2.Marking.Admissible {G : Type u_1} [Group G] (t : Marking G) : Prop

A marking is admissible if it generates, satisfies both relations, and its wild generators have 2-group normal closure (paper §2, "admissible marked generating quadruple").

Equations

• t.Admissible = (t.Generates ∧ t.TameRel ∧ t.WildRel ∧ t.Pro2Core)

noncomputable def GQ2.admissibleCount (G : Type u_1) [Group G] : ℕ

The finite count N(G) of admissible markings — the right-hand side of the surjection-count form of Theorem 1.2 (equals |Sur(Γ_A, G)|, paper Prop. 2.3). Well-defined (finite) for any finite group since Marking G ≃ G⁴.

Equations

• GQ2.admissibleCount G = Nat.card { t : GQ2.Marking G // t.Admissible }

theorem GQ2.odd_nsmul_eq_self {A : Type u_1} [AddCommGroup A] (htor : ∀ (a : A), a + a = 0) {n : ℕ} (hn : Odd n) (x : A) : n • x = x

In a 2-torsion additive group, an odd multiple is the identity — the module-side face of "ω₂ ≡ 0 on the odd part" (odd averaging with no division, cf. inflationVanishes_of_oddNormal and regular_summand_of_subgroup_summand).

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

• eq. (1) = ⟦eq-defwords⟧
• eq. (3) = ⟦eq-defwords3⟧
• Lemma 5.2 = ⟦lem-class2square⟧
• Prop 2.3 = ⟦prop-epi-semantics⟧
• Theorem 1.2 = ⟦thm-main⟧