Triangular preprocessing for the rational direct sum

This module repeats only the coefficient-dependent part of the triangular bookkeeping for ContinuumIndex →₀ ℚ. It enumerates all injective rational sequences, assigns each code a fresh coordinate strictly above the support of its sequence, and applies the generic bounded independence selector from Wallace.TriangularPreprocess.

No topology or character is assumed.

@[reducible, inline]

abbrev Wallace.RationalTriangularPreprocess.ContinuumIndex : Type

The canonical well-ordered index type of cardinality continuum.

Equations

• Wallace.RationalTriangularPreprocess.ContinuumIndex = Wallace.TriangularPreprocess.ContinuumIndex

@[reducible, inline]

abbrev Wallace.RationalTriangularPreprocess.ContinuumRationalGroup : Type

The direct sum of continuum many copies of the additive group of rationals.

Equations

• Wallace.RationalTriangularPreprocess.ContinuumRationalGroup = (Wallace.RationalTriangularPreprocess.ContinuumIndex →₀ ℚ)

@[reducible, inline]

abbrev Wallace.RationalTriangularPreprocess.RationalInjectiveSequences : Type

All injective sequences in the rational direct sum.

Equations

• Wallace.RationalTriangularPreprocess.RationalInjectiveSequences = { s : ℕ → Wallace.RationalTriangularPreprocess.ContinuumRationalGroup // Function.Injective s }

def Wallace.RationalTriangularPreprocess.RationalSupportedBelow (s : ℕ → ContinuumRationalGroup) (i : ContinuumIndex) : Prop

The triangular support condition for rational-valued finitely supported sequences.

Equations

• Wallace.RationalTriangularPreprocess.RationalSupportedBelow s i = ∀ (n : ℕ), ∀ j ∈ (s n).support, j < i

theorem Wallace.RationalTriangularPreprocess.mk_continuumIndex : Cardinal.mk ContinuumIndex = Cardinal.continuum

theorem Wallace.RationalTriangularPreprocess.continuumIndex_infinite : Infinite ContinuumIndex

theorem Wallace.RationalTriangularPreprocess.mk_continuumRationalGroup : Cardinal.mk ContinuumRationalGroup = Cardinal.continuum

theorem Wallace.RationalTriangularPreprocess.mk_continuumRationalGroup_sequences : Cardinal.mk (ℕ → ContinuumRationalGroup) = Cardinal.continuum

noncomputable def Wallace.RationalTriangularPreprocess.rationalBasisRay (i : ContinuumIndex) (n : ℕ) : ContinuumRationalGroup

An injective ray in a rational basis coordinate.

Equations

• Wallace.RationalTriangularPreprocess.rationalBasisRay i n = Finsupp.single i ↑n

theorem Wallace.RationalTriangularPreprocess.rationalBasisRay_injective (i : ContinuumIndex) : Function.Injective (rationalBasisRay i)

theorem Wallace.RationalTriangularPreprocess.rationalBasisRay_family_injective : Function.Injective fun (i : ContinuumIndex) => ⟨rationalBasisRay i, ⋯⟩

theorem Wallace.RationalTriangularPreprocess.mk_rationalInjectiveSequences : Cardinal.mk RationalInjectiveSequences = Cardinal.continuum

noncomputable def Wallace.RationalTriangularPreprocess.rationalSequenceCodeEquiv : ContinuumIndex ≃ RationalInjectiveSequences

A fixed enumeration of every injective rational sequence.

Equations

• Wallace.RationalTriangularPreprocess.rationalSequenceCodeEquiv = Classical.choice Wallace.RationalTriangularPreprocess.rationalSequenceCodeEquiv._proof_1

noncomputable def Wallace.RationalTriangularPreprocess.codedSequence (a : ContinuumIndex) : ℕ → ContinuumRationalGroup

The injective rational sequence represented by the code a.

Equations

• Wallace.RationalTriangularPreprocess.codedSequence a = ↑(Wallace.RationalTriangularPreprocess.rationalSequenceCodeEquiv a)

theorem Wallace.RationalTriangularPreprocess.codedSequence_injective (a : ContinuumIndex) : Function.Injective (codedSequence a)

def Wallace.RationalTriangularPreprocess.sequenceSupport (s : ℕ → ContinuumRationalGroup) : Set ContinuumIndex

The union of the finite supports of a rational sequence.

Equations

• Wallace.RationalTriangularPreprocess.sequenceSupport s = {i : Wallace.RationalTriangularPreprocess.ContinuumIndex | ∃ (n : ℕ), i ∈ (s n).support}

theorem Wallace.RationalTriangularPreprocess.sequenceSupport_countable (s : ℕ → ContinuumRationalGroup) : (sequenceSupport s).Countable

noncomputable def Wallace.RationalTriangularPreprocess.supportBound (a : ContinuumIndex) : ContinuumIndex

A strict bound for every coordinate occurring in the coded sequence.

Equations

• Wallace.RationalTriangularPreprocess.supportBound a = Classical.choose ⋯

theorem Wallace.RationalTriangularPreprocess.support_lt_supportBound (a : ContinuumIndex) {n : ℕ} {i : ContinuumIndex} (hi : i ∈ (codedSequence a n).support) : i < supportBound a

noncomputable def Wallace.RationalTriangularPreprocess.codeIndex : ContinuumIndex ↪ ContinuumIndex

The fresh-coordinate embedding for rational sequence codes.

Equations

• Wallace.RationalTriangularPreprocess.codeIndex = { toFun := Wallace.TriangularPreprocess.freshIndex Wallace.RationalTriangularPreprocess.supportBound, inj' := ⋯ }

theorem Wallace.RationalTriangularPreprocess.codedSequence_supportedBelow (a : ContinuumIndex) : RationalSupportedBelow (codedSequence a) (codeIndex a)

noncomputable def Wallace.RationalTriangularPreprocess.codeBasisVector (a : ContinuumIndex) : ContinuumRationalGroup

The rational basis point assigned to a code.

Equations

• Wallace.RationalTriangularPreprocess.codeBasisVector a = Finsupp.single (Wallace.RationalTriangularPreprocess.codeIndex a) 1

noncomputable def Wallace.RationalTriangularPreprocess.codedDifference (a : ContinuumIndex) (n : ℕ) : ContinuumRationalGroup

The translated sequence used for bounded-independence preprocessing.

Equations

• Wallace.RationalTriangularPreprocess.codedDifference a n = Wallace.RationalTriangularPreprocess.codedSequence a n - Wallace.RationalTriangularPreprocess.codeBasisVector a

theorem Wallace.RationalTriangularPreprocess.codedDifference_injective (a : ContinuumIndex) : Function.Injective (codedDifference a)

theorem Wallace.RationalTriangularPreprocess.triangular_block_preprocess (a : ContinuumIndex) (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ (∀ (l : ℕ), (TriangularPreprocess.blockPositions N hN l).card = N l ∧ FiniteCombinatorics.BoundedIndependent (M l) (Finset.image (fun (n : ℕ) => codedSequence a (φ n) - codeBasisVector a) (TriangularPreprocess.blockPositions N hN l))) ∧ RationalSupportedBelow (codedSequence a ∘ φ) (codeIndex a)

Full block preprocessing for rational sequences.