From the local fusions to the Wallace counterexample

This module performs the final global assembly. Its only input is the output of the countable fusion: for each nonzero vector, a character on its concrete countable dependency closure which detects that vector and satisfies the prescribed ultrafilter limits for all codes internal to the closure. The transfinite recursion extends each such character to the whole free group and makes it admissible at every code. The resulting characters form a separating family, so the minimal construction interface yields the Wallace semigroup.

def Wallace.GlobalAssembly.HasLocalSeparatingCharacters (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) : Prop

The exact local output required from the countable fusion.

Equations

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

noncomputable def Wallace.GlobalAssembly.localCharacter (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : HasLocalSeparatingCharacters N hN M) (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : (↑(ConcreteClosure.closure N hN M ↑x) →₀ ℤ) →+ UnitAddCircle

The chosen local character for a nonzero vector.

Equations

• Wallace.GlobalAssembly.localCharacter N hN M H x = Classical.choose ⋯

theorem Wallace.GlobalAssembly.localCharacter_self_ne_zero (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : HasLocalSeparatingCharacters N hN M) (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : (localCharacter N hN M H x) (Finsupp.subtypeDomain (ConcreteClosure.closure N hN M ↑x) ↑x) ≠ 0

theorem Wallace.GlobalAssembly.localCharacter_admissible (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : HasLocalSeparatingCharacters N hN M) (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : TransfiniteExtension.LocallyAdmissible (ConcreteData.transfiniteData N hN M) (ConcreteClosure.closure N hN M ↑x) (localCharacter N hN M H x)

noncomputable def Wallace.GlobalAssembly.globalCharacter (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : HasLocalSeparatingCharacters N hN M) (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : TriangularPreprocess.ContinuumFreeGroup →+ UnitAddCircle

Extend the chosen local character by the well-founded triangular recursion.

Equations

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

theorem Wallace.GlobalAssembly.globalCharacter_self_ne_zero (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : HasLocalSeparatingCharacters N hN M) (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) : (globalCharacter N hN M H x) ↑x ≠ 0

theorem Wallace.GlobalAssembly.globalCharacter_admissible (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : HasLocalSeparatingCharacters N hN M) (x : { x : TriangularPreprocess.ContinuumFreeGroup // x ≠ 0 }) (a : TriangularPreprocess.ContinuumIndex) : Filter.Tendsto (fun (n : ℕ) => (globalCharacter N hN M H x) (ConcreteData.prepared N hN M a n)) (↑(BlockData.ultrafilter N hN a)) (nhds ((globalCharacter N hN M H x) (TriangularPreprocess.codeBasisVector a)))

noncomputable def Wallace.GlobalAssembly.separationPackage (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (H : HasLocalSeparatingCharacters N hN M) : SeparationPackage TriangularPreprocess.ContinuumIndex

The completely concrete separating package obtained from the local fusion theorem.

Equations

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