Concrete triangular data and block-density ultrafilters

This module makes all global choices which are shared by the local character fusions. For arbitrary positive block sizes and arbitrary bounded-independence thresholds, it chooses the prepared subsequence of every triangularly coded injective sequence. It also transports the standard continuum-sized almost-disjoint family to the canonical continuum index and chooses a free block-density ultrafilter for every code.

The choices here are entirely set-theoretic. No topology on the free group and no character is assumed.

The globally prepared sequences

noncomputable def Wallace.ConcreteData.selector (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) : ℕ → ℕ

The strictly increasing subsequence selector supplied by block preprocessing.

Equations

• Wallace.ConcreteData.selector N hN M a = Classical.choose ⋯

theorem Wallace.ConcreteData.selector_strictMono (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) : StrictMono (selector N hN M a)

noncomputable def Wallace.ConcreteData.prepared (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) (n : ℕ) : TriangularPreprocess.ContinuumFreeGroup

The prepared subsequence coded by a.

Equations

• Wallace.ConcreteData.prepared N hN M a n = Wallace.TriangularPreprocess.codedSequence a (Wallace.ConcreteData.selector N hN M a n)

noncomputable def Wallace.ConcreteData.differenceBlock (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) (l : ℕ) : Finset TriangularPreprocess.ContinuumFreeGroup

The shifted finite set in block l.

Equations

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

theorem Wallace.ConcreteData.differenceBlock_boundedIndependent (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) (l : ℕ) : FiniteCombinatorics.BoundedIndependent (M l) (differenceBlock N hN M a l)

theorem Wallace.ConcreteData.prepared_support_lt (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) (n : ℕ) (i : TriangularPreprocess.ContinuumIndex) (hi : i ∈ (prepared N hN M a n).support) : i < TriangularPreprocess.codeIndex a

theorem Wallace.ConcreteData.prepared_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) : Function.Injective (prepared N hN M a)

theorem Wallace.ConcreteData.preparedDifference_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (a : TriangularPreprocess.ContinuumIndex) : Function.Injective fun (n : ℕ) => prepared N hN M a n - TriangularPreprocess.codeBasisVector a

Translating a prepared sequence by its prescribed basis point preserves injectivity.

Packaging for the transfinite extension

noncomputable def Wallace.ConcreteData.transfiniteData (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) : TransfiniteExtension.ContinuumData

The concrete triangular data used by the transfinite recursion.

Equations

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