The main theorem for every torsion-free Abelian group of cardinality continuum

This module closes the scope gap between the canonical rational construction and the exact main theorem stated in the paper. The rational character package is pulled back along the coordinatization embedding from Section 2. Its prescribed basis limits lie in the embedded group by construction, so no new fusion or set-theoretic hypothesis is needed.

noncomputable def Wallace.RationalCoordinatization.fullCharacterPackage {G : Type} [AddCommGroup G] (K : RationalCoordinatization G) : FullCharacterPackage G

Pull the fully constructed rational character package back to a coordinatized group.

Equations

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

theorem Wallace.RationalCoordinatization.hasMainGroupTopology {G : Type} [AddCommGroup G] (K : RationalCoordinatization G) : HasMainGroupTopology G

Every group with the paper's rational coordinatization inherits the complete topology conclusion from the unconditional rational construction.

theorem Wallace.torsionFreeAbelianGroup_mainTheorem (G : Type) [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : HasMainGroupTopology G

Formal counterpart of the paper's main theorem. Every torsion-free Abelian group of cardinality continuum admits a Hausdorff countably compact group topology in which every convergent sequence is eventually constant. The formal conclusion additionally records a compatible totally bounded uniform group structure. Wallace.Audit records the standard classical Lean foundations used by the proof.

theorem Wallace.torsionFreeAbelianGroup_mainTheorem_exact (G : Type) [AddCommGroup G] [IsAddTorsionFree G] (hcard : Cardinal.mk G = Cardinal.continuum) : ∃ (topology : TopologicalSpace G), IsTopologicalAddGroup G ∧ T2Space G ∧ CountablyCompactSpace G ∧ ∀ (s : ℕ → G) (x : G), Filter.Tendsto s Filter.atTop (nhds x) → ∀ᶠ (n : ℕ) in Filter.atTop, s n = x

The exact paper-level projection of the main theorem, with only the properties printed in the theorem statement and no additional uniform-space fields exposed.