Triangular coding and block preprocessing

This file supplies the unconditional set-theoretic bookkeeping that precedes the character construction. The index set is the canonical well-order of cardinality continuum. All injective sequences in the corresponding free Abelian group are coded, and their codes are assigned distinct indices strictly above every coordinate in the sequence. The second half of the file constructs a genuine subsequence whose prescribed finite blocks are bounded-independent.

The continuum initial ordinal and its free group

@[reducible, inline]

abbrev Wallace.TriangularPreprocess.ContinuumIndex : Type

The canonical well-ordered index type of cardinality continuum.

Equations

• Wallace.TriangularPreprocess.ContinuumIndex = Cardinal.continuum.ord.ToType

@[reducible, inline]

abbrev Wallace.TriangularPreprocess.ContinuumFreeGroup : Type

The free Abelian group on the canonical continuum index.

Equations

• Wallace.TriangularPreprocess.ContinuumFreeGroup = (Wallace.TriangularPreprocess.ContinuumIndex →₀ ℤ)

@[reducible, inline]

abbrev Wallace.TriangularPreprocess.InjectiveSequences : Type

The type of all injective sequences in the free group.

Equations

• Wallace.TriangularPreprocess.InjectiveSequences = { s : ℕ → Wallace.TriangularPreprocess.ContinuumFreeGroup // Function.Injective s }

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

theorem Wallace.TriangularPreprocess.continuumIndex_infinite : Infinite ContinuumIndex

theorem Wallace.TriangularPreprocess.mk_continuumFreeGroup : Cardinal.mk ContinuumFreeGroup = Cardinal.continuum

theorem Wallace.TriangularPreprocess.mk_continuumFreeGroup_sequences : Cardinal.mk (ℕ → ContinuumFreeGroup) = Cardinal.continuum

noncomputable def Wallace.TriangularPreprocess.basisRay (i : ContinuumIndex) (n : ℕ) : ContinuumFreeGroup

An injective ray along one basis vector.

Equations

• Wallace.TriangularPreprocess.basisRay i n = Finsupp.single i ↑n

theorem Wallace.TriangularPreprocess.basisRay_injective (i : ContinuumIndex) : Function.Injective (basisRay i)

theorem Wallace.TriangularPreprocess.basisRay_family_injective : Function.Injective fun (i : ContinuumIndex) => ⟨basisRay i, ⋯⟩

theorem Wallace.TriangularPreprocess.mk_injectiveSequences : Cardinal.mk InjectiveSequences = Cardinal.continuum

noncomputable def Wallace.TriangularPreprocess.sequenceCodeEquiv : ContinuumIndex ≃ InjectiveSequences

A fixed equivalence between the canonical continuum index and all injective sequences.

Equations

• Wallace.TriangularPreprocess.sequenceCodeEquiv = Classical.choice Wallace.TriangularPreprocess.sequenceCodeEquiv._proof_1

noncomputable def Wallace.TriangularPreprocess.codedSequence (a : ContinuumIndex) : ℕ → ContinuumFreeGroup

The sequence represented by a code.

Equations

• Wallace.TriangularPreprocess.codedSequence a = ↑(Wallace.TriangularPreprocess.sequenceCodeEquiv a)

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

Countable supports have strict upper bounds

def Wallace.TriangularPreprocess.sequenceSupport (s : ℕ → ContinuumFreeGroup) : Set ContinuumIndex

All coordinates that occur in a sequence.

Equations

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

theorem Wallace.TriangularPreprocess.sequenceSupport_countable (s : ℕ → ContinuumFreeGroup) : (sequenceSupport s).Countable

theorem Wallace.TriangularPreprocess.exists_strict_upperBound_of_countable {S : Set ContinuumIndex} (hS : S.Countable) : ∃ (i : ContinuumIndex), ∀ j ∈ S, j < i

Every countable set of continuum indices is strictly bounded.

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

A chosen strict upper bound for the support of each coded sequence.

Equations

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

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

Fresh indices above all supports

theorem Wallace.TriangularPreprocess.exists_fresh_above (bound : ContinuumIndex → ContinuumIndex) (a : ContinuumIndex) (previous : (b : ContinuumIndex) → b < a → ContinuumIndex) : ∃ (i : ContinuumIndex), bound a < i ∧ ∀ (b : ContinuumIndex) (h : b < a), previous b h ≠ i

noncomputable def Wallace.TriangularPreprocess.freshIndex (bound : ContinuumIndex → ContinuumIndex) : ContinuumIndex → ContinuumIndex

Transfinite fresh-index assignment. At stage a, it avoids all values assigned below a and lies strictly above bound a.

Equations

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

theorem Wallace.TriangularPreprocess.freshIndex_spec (bound : ContinuumIndex → ContinuumIndex) (a : ContinuumIndex) : bound a < freshIndex bound a ∧ ∀ b < a, freshIndex bound b ≠ freshIndex bound a

theorem Wallace.TriangularPreprocess.freshIndex_injective (bound : ContinuumIndex → ContinuumIndex) : Function.Injective (freshIndex bound)

noncomputable def Wallace.TriangularPreprocess.codeIndex : ContinuumIndex ↪ ContinuumIndex

The injective index assigned to every sequence code.

Equations

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

theorem Wallace.TriangularPreprocess.codedSequence_supportedBelow (a : ContinuumIndex) : FiniteCombinatorics.SupportedBelow (codedSequence a) (codeIndex a)

Blockwise bounded-independence selection

theorem Wallace.TriangularPreprocess.boundedIndependent_mono {G : Type u_1} [AddCommGroup G] {M : ℕ} {X Y : Finset G} (hY : FiniteCombinatorics.BoundedIndependent M Y) (hXY : X ⊆ Y) : FiniteCombinatorics.BoundedIndependent M X

Bounded independence is inherited by finite subsets.

theorem Wallace.TriangularPreprocess.exists_index_gt_avoiding_finset {G : Type u_1} {u : ℕ → G} (hu : Function.Injective u) (B : Finset G) (k : ℕ) : ∃ (m : ℕ), k < m ∧ u m ∉ B

An injective sequence has arbitrarily late terms outside any fixed finite set.

structure Wallace.TriangularPreprocess.BlockSelectionState (G : Type u_1) : Type u_1

State of the recursive block selector. values l contains the values already selected in block l; last is the last source index used.

• last : ℕ

  The most recently selected block index.

• values : ℕ → Finset G

  The finite set selected at each block index.

def Wallace.TriangularPreprocess.initialBlockSelectionState (G : Type u_1) : BlockSelectionState G

The block-selection state with no selected values.

Equations

• Wallace.TriangularPreprocess.initialBlockSelectionState G = { last := 0, values := fun (x : ℕ) => ∅ }

noncomputable def Wallace.TriangularPreprocess.excludedAt {G : Type u_1} [AddCommGroup G] (M block : ℕ → ℕ) (n : ℕ) (st : BlockSelectionState G) : Finset G

The finite set of values excluded at the next block-selection stage.

Equations

• Wallace.TriangularPreprocess.excludedAt M block n st = st.values (block n) ∪ Wallace.FiniteCombinatorics.forbiddenFinset (M (block n)) (st.values (block n))

noncomputable def Wallace.TriangularPreprocess.nextBlockIndex {G : Type u_1} [AddCommGroup G] (u : ℕ → G) (hu : Function.Injective u) (M block : ℕ → ℕ) (n : ℕ) (st : BlockSelectionState G) : ℕ

The next source index: strictly later than the previous one and outside both the values already used in this block and every bounded forbidden equation over them.

Equations

• Wallace.TriangularPreprocess.nextBlockIndex u hu M block n st = Classical.choose ⋯

noncomputable def Wallace.TriangularPreprocess.blockSelectionStep {G : Type u_1} [AddCommGroup G] (u : ℕ → G) (hu : Function.Injective u) (M block : ℕ → ℕ) (n : ℕ) (st : BlockSelectionState G) : BlockSelectionState G

Advance block selection by choosing values outside the excluded set.

Equations

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

def Wallace.TriangularPreprocess.blockSelectionStates {G : Type u_1} [AddCommGroup G] (u : ℕ → G) (hu : Function.Injective u) (M block : ℕ → ℕ) : ℕ → BlockSelectionState G

States after the first n positions of the new sequence have been selected.

Equations

• One or more equations did not get rendered due to their size.
• Wallace.TriangularPreprocess.blockSelectionStates u hu M block 0 = Wallace.TriangularPreprocess.initialBlockSelectionState G

noncomputable def Wallace.TriangularPreprocess.blockSubsequenceIndex {G : Type u_1} [AddCommGroup G] (u : ℕ → G) (hu : Function.Injective u) (M block : ℕ → ℕ) (n : ℕ) : ℕ

The actual source-index subsequence selected by the state recursion.

Equations

• Wallace.TriangularPreprocess.blockSubsequenceIndex u hu M block n = (Wallace.TriangularPreprocess.blockSelectionStates u hu M block (n + 1)).last

theorem Wallace.TriangularPreprocess.blockSubsequenceIndex_strictMono {G : Type u_1} [AddCommGroup G] (u : ℕ → G) (hu : Function.Injective u) (M block : ℕ → ℕ) : StrictMono (blockSubsequenceIndex u hu M block)

def Wallace.TriangularPreprocess.finsetCutoff (B : Finset ℕ) : ℕ

A cutoff beyond every position in a finite set.

Equations

• Wallace.TriangularPreprocess.finsetCutoff B = B.sup fun (n : ℕ) => n + 1

theorem Wallace.TriangularPreprocess.add_one_le_finsetCutoff {B : Finset ℕ} {n : ℕ} (hn : n ∈ B) : n + 1 ≤ finsetCutoff B

theorem Wallace.TriangularPreprocess.exists_blockwise_boundedIndependent_subsequence {G : Type u_1} [AddCommGroup G] [IsAddTorsionFree G] [DecidableEq G] (u : ℕ → G) (hu : Function.Injective u) (block M : ℕ → ℕ) (hfinite : ∀ (l : ℕ), {n : ℕ | block n = l}.Finite) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (l : ℕ), FiniteCombinatorics.BoundedIndependent (M l) (Finset.image (fun (n : ℕ) => u (φ n)) ⋯.toFinset)

Generic block preprocessing. block n specifies which finite block contains output position n. Each block may have any prescribed positive finite size; only finiteness is needed by the selection argument.

The consecutive block partition used in the paper

def Wallace.TriangularPreprocess.blockStart (N : ℕ → ℕ) (l : ℕ) : ℕ

The first position of block l, namely ∑ j < l, N j. This is the paper's S_l.

Equations

• Wallace.TriangularPreprocess.blockStart N l = ∑ j ∈ Finset.range l, N j

@[simp]

theorem Wallace.TriangularPreprocess.blockStart_zero (N : ℕ → ℕ) : blockStart N 0 = 0

theorem Wallace.TriangularPreprocess.blockStart_succ (N : ℕ → ℕ) (l : ℕ) : blockStart N (l + 1) = blockStart N l + N l

theorem Wallace.TriangularPreprocess.blockStart_strictMono (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) : StrictMono (blockStart N)

theorem Wallace.TriangularPreprocess.index_le_blockStart (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (l : ℕ) : l ≤ blockStart N l

def Wallace.TriangularPreprocess.blockOf (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (n : ℕ) : ℕ

The unique block label whose consecutive half-open interval contains n.

Equations

• Wallace.TriangularPreprocess.blockOf N hN n = Nat.find ⋯

theorem Wallace.TriangularPreprocess.blockOf_spec (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (n : ℕ) : blockStart N (blockOf N hN n) ≤ n ∧ n < blockStart N (blockOf N hN n + 1)

def Wallace.TriangularPreprocess.blockPositions (N : ℕ → ℕ) (_hN : ∀ (l : ℕ), 0 < N l) (l : ℕ) : Finset ℕ

The finite interval I_l = [S_l, S_l + N_l) used in the paper.

Equations

• Wallace.TriangularPreprocess.blockPositions N _hN l = Finset.Ico (Wallace.TriangularPreprocess.blockStart N l) (Wallace.TriangularPreprocess.blockStart N (l + 1))

theorem Wallace.TriangularPreprocess.mem_blockPositions_iff (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) {l n : ℕ} : n ∈ blockPositions N hN l ↔ blockOf N hN n = l

theorem Wallace.TriangularPreprocess.blockPositions_card (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (l : ℕ) : (blockPositions N hN l).card = N l

theorem Wallace.TriangularPreprocess.blockFiber_finite (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (l : ℕ) : {n : ℕ | blockOf N hN n = l}.Finite

theorem Wallace.TriangularPreprocess.exists_boundedIndependent_subsequence_for_sizes {G : Type u_1} [AddCommGroup G] [IsAddTorsionFree G] [DecidableEq G] (u : ℕ → G) (hu : Function.Injective u) (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) : ∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (l : ℕ), (blockPositions N hN l).card = N l ∧ FiniteCombinatorics.BoundedIndependent (M l) (Finset.image (fun (n : ℕ) => u (φ n)) (blockPositions N hN l))

Block preprocessing for any prescribed sequence of positive finite sizes.

The paper's shifted coded sequences

noncomputable def Wallace.TriangularPreprocess.codeBasisVector (a : ContinuumIndex) : ContinuumFreeGroup

The basis vector attached to a code's fresh index.

Equations

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

noncomputable def Wallace.TriangularPreprocess.codedDifference (a : ContinuumIndex) (n : ℕ) : ContinuumFreeGroup

The sequence to which finite bounded-independence extraction is applied.

Equations

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

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

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

Full block preprocessing. For every triangular code and every prescribed positive block size sequence N and coefficient-bound sequence M, a genuine subsequence is chosen so that the shifted values in each block have exactly size N l and are M l-independent. The original strict support bound is preserved by passage to the subsequence.