NormalCorePower

Abstract

Noncommutative algebra for the power-subgroup route to strong completeness.

Theorem 1.1 (Normality without commutativity).

$$\forall (m:\mathbb{N}),\mathrm{Normal}(\mathrm{powerSubgroup}(G,m))$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup_normal (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conjugation carries each mth power to another mth power. The subgroup generated by all such powers is therefore normal in any group.

Definition 1.2 (Power-generated subgroup).

$$\mathrm{powerSubgroup}(G,m)=\mathrm{SubgroupClosure}(\mathrm{Range}(g\mapsto g^m))$$

Formalization. D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup (✓ std3).

Source. Repository-derived.

Commentary.

The subgroup is generated algebraically by all mth powers in an arbitrary group. No commutativity or topology is assumed.

Theorem 1.3 (Each power belongs to the subgroup).

$$\forall (m:\mathbb{N}),\forall (g:G),g^m\in \mathrm{powerSubgroup}(G,m)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/NormalCorePower.pow_mem_powerSubgroup (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural m and group element g, the element g to the mth power belongs to the generated subgroup.

Theorem 1.4 (Exponent quotient criterion).

$$\forall (m:\mathbb{N}),\forall (N:\mathrm{NormalSubgroup}(G)),\mathrm{powerSubgroup}(G,m)\le N⟺\forall (q:\mathrm{Quotient}(G,N)),q^m=1$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup_le_iff (✓ std3). ∎

Source. Repository-derived.

Commentary.

For any normal subgroup N, containment of the power subgroup in N is equivalent to every element of G modulo N having mth power one. The criterion also includes m equal to zero.

Theorem 1.5 (Powers in a finite-index normal core).

$$\forall (H:\mathrm{Subgroup}(G)),\mathrm{FiniteIndex}(H)\Rightarrow \forall (g:G),g^{\mathrm{Index}(\mathrm{NormalCore}(H))}\in \mathrm{NormalCore}(H)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/NormalCorePower.pow_normalCore_index_mem (✓ std3). ∎

Source. Repository-derived.

Commentary.

If H has finite index, its normal core also has finite index. Lagrange in that abstract quotient puts the normal-core-index power of every group element in the core. No normality of H or continuity of this quotient is needed.

Theorem 1.6 (Containment in the normal core).

$$\forall (H:\mathrm{Subgroup}(G)),\mathrm{FiniteIndex}(H)\Rightarrow \mathrm{powerSubgroup}(G,\mathrm{Index}(\mathrm{NormalCore}(H)))\le \mathrm{NormalCore}(H)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup_le_normalCore (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every finite-index subgroup H contains the power subgroup at the positive index of its normal core, through the containment of that power subgroup in the core.

References

• Truth anchor: D5/S3/Factorization/Galois/NormalCorePower.pow_mem_powerSubgroup
• Truth anchor: D5/S3/Factorization/Galois/NormalCorePower.pow_normalCore_index_mem
• Truth anchor: D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup
• Truth anchor: D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup_le_iff
• Truth anchor: D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup_le_normalCore
• Truth anchor: D5/S3/Factorization/Galois/NormalCorePower.powerSubgroup_normal