The rational proposition on the additive group of real numbers

The paper writes ℚ^(𝔠) ≅ ℝ. This module formalizes that algebraic identification using the rational Hamel dimension of ℝ, then transports the fully constructed character package rather than merely asserting that a suitable topology can be transferred.

theorem Wallace.rank_continuumRationalGroup : Module.rank ℚ RationalTriangularPreprocess.ContinuumRationalGroup = Cardinal.continuum

noncomputable def Wallace.continuumRationalGroupLinearEquivReal : RationalTriangularPreprocess.ContinuumRationalGroup ≃ₗ[ℚ] ℝ

A rational-linear equivalence ℚ^(𝔠) ≃ₗ[ℚ] ℝ.

Equations

• Wallace.continuumRationalGroupLinearEquivReal = Classical.choice Wallace.continuumRationalGroupLinearEquivReal._proof_2

noncomputable def Wallace.continuumRationalGroupAddEquivReal : RationalTriangularPreprocess.ContinuumRationalGroup ≃+ ℝ

The algebraic isomorphism explicitly invoked in the paper's rational proposition.

Equations

• Wallace.continuumRationalGroupAddEquivReal = Wallace.continuumRationalGroupLinearEquivReal.toAddEquiv

noncomputable def Wallace.realFullCharacterPackage : FullCharacterPackage ℝ

The concrete rational character package transported to the additive group of real numbers.

Equations

• Wallace.realFullCharacterPackage = Wallace.RationalAssembly.fullCharacterPackage.comapAddEquiv Wallace.continuumRationalGroupAddEquivReal.symm

theorem Wallace.realAdditiveGroup_mainTheorem : HasMainGroupTopology ℝ

Rational proposition of the paper, in its literal real-group form. The additive group of real numbers admits a Hausdorff countably compact group topology in which every convergent sequence is eventually constant.

theorem Wallace.continuumRationalGroup_and_real_mainTheorem : HasMainGroupTopology RationalTriangularPreprocess.ContinuumRationalGroup ∧ HasMainGroupTopology ℝ

A single declaration recording both presentations used in the paper, ℚ^(𝔠) and the additively isomorphic group ℝ.