Global assembly for the rational vector group

The local fusion around each nonzero vector is extended by the rational transfinite recursion. The resulting compatible characters separate points and realize the nonzero ultrafilter limit attached to every injective rational sequence.

@[reducible, inline]

abbrev Wallace.RationalAssembly.N : ℕ → ℕ

The block-size schedule used by the assembled rational construction.

Equations

• Wallace.RationalAssembly.N = Wallace.RationalFusionRun.blockSize

theorem Wallace.RationalAssembly.hN (l : ℕ) : 0 < N l

@[reducible, inline]

noncomputable abbrev Wallace.RationalAssembly.M : ℕ → ℕ

The bounded-independence schedule used by the assembled rational construction.

Equations

• Wallace.RationalAssembly.M = Wallace.RationalFusionRun.independenceBound

noncomputable def Wallace.RationalAssembly.localCharacter (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : (↑(RationalClosure.closure N hN M ↑x) →₀ ℚ) →+ UnitAddCircle

The local limiting character supplied by the concrete fusion.

Equations

• Wallace.RationalAssembly.localCharacter x = (Wallace.RationalFusionRun.localRunCertificate x).run.limitCharacter

theorem Wallace.RationalAssembly.localCharacter_self_ne_zero (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : (localCharacter x) (Finsupp.subtypeDomain (RationalClosure.closure N hN M ↑x) ↑x) ≠ 0

theorem Wallace.RationalAssembly.localCharacter_admissible (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : RationalTransfiniteExtension.LocallyAdmissible (RationalData.transfiniteData N hN M) (RationalClosure.closure N hN M ↑x) (localCharacter x)

noncomputable def Wallace.RationalAssembly.globalCharacter (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : RationalTriangularPreprocess.ContinuumRationalGroup →+ UnitAddCircle

Extend the local character to all continuum coordinates.

Equations

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

theorem Wallace.RationalAssembly.globalCharacter_self_ne_zero (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) : (globalCharacter x) ↑x ≠ 0

theorem Wallace.RationalAssembly.globalCharacter_admissible (x : { x : RationalTriangularPreprocess.ContinuumRationalGroup // x ≠ 0 }) (a : RationalTriangularPreprocess.ContinuumIndex) : Filter.Tendsto (fun (n : ℕ) => (globalCharacter x) (RationalData.prepared N hN M a n)) (↑(BlockData.ultrafilter N hN a)) (nhds ((globalCharacter x) (RationalTriangularPreprocess.codeBasisVector a)))

noncomputable def Wallace.RationalAssembly.fullCharacterPackage : FullCharacterPackage RationalTriangularPreprocess.ContinuumRationalGroup

The complete character package for the rational direct sum of rank continuum.

Equations

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

theorem Wallace.RationalAssembly.continuumRationalGroup_mainTheorem : RationalVectorGroupConclusion RationalTriangularPreprocess.ContinuumIndex

The rational vector group of continuum rank has the full constructed topology: Hausdorff, countably compact, totally bounded, and with only eventually constant convergent sequences.