The ω₂ exponent: specification and Appendix-B cross-check

GQ2.omega2Exp n is our concrete integer representative of the profinite idempotent ω₂ modulo n. This file proves it satisfies the two congruences that define ω₂ — ≡ 1 on the 2-part and ≡ 0 on the odd part — and cross-checks it against the paper's Appendix B serialization.

theorem GQ2.oddPart_dvd_omega2Exp (n : ℕ) : n / 2 ^ n.factorization 2 ∣ omega2Exp n

The odd part of n divides omega2Exp n (the "ω₂ ≡ 0 on the odd part" condition).

theorem GQ2.omega2Exp_modEq_one {n : ℕ} (hn : n ≠ 0) (ha : n.factorization 2 ≠ 0) : omega2Exp n ≡ 1 [MOD 2 ^ n.factorization 2]

omega2Exp n ≡ 1 modulo the 2-part 2 ^ v₂(n) (the "ω₂ ≡ 1 on the 2-part" condition), for n with a nontrivial 2-part. Uses Euler's theorem: the odd part is a unit mod 2^a, and 2^(a-1) = φ(2^a).

theorem GQ2.omega2Exp_modEq {N M : ℕ} (hdvd : N ∣ M) (hM : M ≠ 0) : omega2Exp M ≡ omega2Exp N [MOD N]

Compatibility of the ω₂ exponents across levels. For N ∣ M (M ≠ 0), the exponents at levels M and N agree modulo N: omega2Exp M ≡ omega2Exp N [MOD N]. This is the coherence making the family (omega2Exp N)_N a well-defined element ω₂ of ℤ̂ = lim ℤ/N (see GQ2.omega2): both sides are ≡ 1 on the 2-part of N and ≡ 0 on its odd part, and CRT combines the two congruences over the coprime factorisation N = 2^{v₂ N} · (N / 2^{v₂ N}).

theorem GQ2.powOmega2_pow_eq {G : Type u_1} [Group G] (x : G) {N : ℕ} (hdvd : orderOf x ∣ N) (hN : N ≠ 0) : x ^ omega2Exp N = powOmega2 x

ω₂ is well-defined via any exponent multiple. For x of finite order dividing N (N ≠ 0), x ^ (omega2Exp N) = powOmega2 x. So powOmega2 really is the 2-primary projection: the choice of modulus orderOf x in its definition is immaterial, as long as the modulus is a multiple of orderOf x. (This is what makes powOmega2 behave coordinatewise on products, cf. powOmega2_prod.)

theorem GQ2.powOmega2_map {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (f : G →* H) (x : G) : f (powOmega2 x) = powOmega2 (f x)

Naturality of ω₂. The 2-primary projection commutes with every group homomorphism (out of a finite group): f (x ^ ω₂) = (f x) ^ ω₂. This is the structural fact underlying the fact that the paper's auxiliary words are preserved by quotient maps (needed for Lemma 2.1).

theorem GQ2.omega2Exp_appendixB_value : omega2Exp 85667662080 = 40491355905

Appendix B, exact match. Our computable representative omega2Exp, evaluated at the paper's modulus M = 85667662080 = 2⁸·3²·5·7·11·13·17·19·23, reproduces the Appendix-B serialization 40491355905 exactly (not merely up to the defining congruences). This certifies that the definition omega2Exp, and not just the hard-coded residue of omega2_appendixB, agrees with the paper. Proved with only the standard axioms: the 2-adic valuation v₂(M) = 8 is pinned by p^k ∣ M bounds, and the remaining 334639305 ^ 2⁷ % M is closed by kernel Nat arithmetic.

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

• Lemma 2.1 = ⟦lem-subdirect⟧