bibkey: nikolov2007on authors: Nikolay Nikolov and Dan Segal year: 2007 title: ‘On finitely generated profinite groups, I: strong completeness and uniform bounds’ doi: 10.4007/annals.2007.165.171 url: https://annals.math.princeton.edu/wp-content/uploads/annals-v165-n1-p05.pdf claim: Every topologically finitely generated profinite group is strongly complete; every abstract subgroup of finite index is open. strata_touched:

• D5/S3/Factorization/Galois/GeneralPowerCharacterLayer license: No redistribution license asserted for the paper; citation only triage: anchor

Nikolov–Segal strong completeness and an abelian Lean precursor

Retrieved primary source

Nikolay Nikolov and Dan Segal, On finitely generated profinite groups, I: strong completeness and uniform bounds, Annals of Mathematics 165 (2007), 171–238, DOI https://doi.org/10.4007/annals.2007.165.171. The publisher’s paper was retrieved from https://annals.math.princeton.edu/wp-content/uploads/annals-v165-n1-p05.pdf. Theorem 1.1 on printed page 172 states: “Every finitely generated profinite group is strongly complete.” The immediately following sentence specifies topological finite generation; the preceding definition of strong completeness includes that every subgroup of finite index is open. This full theorem permits nonabelian groups. Its literature statement is not itself a Lean proof.

Immutable reusable source and actual library dependency

The separate public, source-only abelian publication is https://github.com/the-omega-institute/trureturning-lean-eval/tree/c13fc74d2430bf94b25eca6dead266229b7ce9fb. Its exact prerequisite pins and canonical scoped reproduction commands are in https://github.com/the-omega-institute/trureturning-lean-eval/blob/c13fc74d2430bf94b25eca6dead266229b7ce9fb/README.md. The three unchanged reviewed files are AbelianPowerQuotient.lean, Checks.lean, and SharpGeneratorCheck.lean.

They import the existing module D5.S3.Factorization.Galois.GeneralPowerCharacterLayer at trureturing commit 586ff54dc5fba0aaa4eab5b152048e0bc3daec23, with Lean 4.33.0 and Mathlib db584cd6d46c92f209a44c0f1c829460d327499d: https://github.com/the-omega-institute/trureturing/blob/586ff54dc5fba0aaa4eab5b152048e0bc3daec23/D5/S3/Factorization/Galois/GeneralPowerCharacterLayer.lean. The actual reused declarations are powerSubgroup, power_quotient_has_exponent_dividing, and power_subgroup_le_iff_quotient_pow_eq_one in that namespace. The imported finite-character kernel equality is not used to supply the topological proof.

Exact compiled quantitative statement and mechanism

The named theorem LeanEval.NikolovSegalDependency.compact_abelian_power_quotient has a commutative group G with a topological group structure, compactness and Hausdorffness, a finite set S with (Subgroup.closure (S : Set G)).topologicalClosure = ⊤, and n : ℕ with 0 < n. It concludes that the range of powMonoidHom n is open and its subgroup index is at most n ^ S.card. Writing d = S.card, this is openness of Gⁿ together with [G : Gⁿ] ≤ nᵈ. This abelian quantitative precursor is described separately from Theorem 1.1; no novelty is asserted.

Compactness makes the continuous power-map image compact, and Hausdorffness makes it closed. The closed subgroup P = Gⁿ therefore gives a Hausdorff quotient Q = G/P. The reused exponent declaration says that every element of Q has nth power one. The images of the generators define a homomorphism from a product of d cyclic groups of order n into Q. Its finite image is closed and contains the dense subgroup generated by those images, so it is all of Q. Surjectivity gives the index bound; closedness and finite index then make P open.

For any finite-index subgroup H of this abelian G, taking n = H.index and using the reused quotient-power equivalence puts Gⁿ inside H. Openness of the smaller subgroup implies openness of H. The final check uses compactness and total disconnectedness and derives Hausdorffness from the singleton connected component of the identity. It therefore checks the abelian specialization without introducing an extra Hausdorff premise.

The checks establish equality [G : Gⁿ] = nᵈ for G = Fin d → Multiplicative (ZMod n), and construct a generating set of cardinality d when n > 1. Thus the bound is attained by finite products of cyclic groups; n = 1 and the empty generating set are also checked. All three unchanged files passed scoped Lean compilation against the pinned library. Printed axiom closures of their named declarations contain only propext, Classical.choice, and Quot.sound. No Lake package build or full-root rebuild was performed for this source-only publication.

Nonabelian gap and admission boundary

For nonabelian groups the power map need not be a homomorphism and its image need not be a subgroup. The finite cyclic-product surjection above relies on commutativity. It does not establish closedness of general verbal subgroups or the uniform finite-group word-width results used in the paper’s full argument. The abelian files do not prove the arbitrary nonabelian LeanEval nikolov_segal statement and are not an official submission.

This note returns literature context, immutable reusable proof sources and the exact existing dependency to the Library. It adds no D5 formalization, theory chapter, Reg wrapper, atom, deposit or freeze. The new abelian formalized mathematics remains outside trureturing dev; admission of a reference note does not admit that formal code. The publication’s campaign attribution is trureturning, with no acceptance, score or rank claim. The separate Gardam unit-submission branches and legacy issue 1932 remain separate.