The concrete countable block schedule around one nonzero vector

For one nonzero vector x, only codes whose fresh coordinates lie in its dependency closure matter to the local fusion. They form a countable type. This module disjointizes their fixed almost-disjoint labels, selects the unique active code at each block label, and defines the finite independent set presented to bounded deletion at that stage.

@[reducible, inline]

abbrev Wallace.ConcreteLocalSetup.RelevantCode (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : Type

Codes whose prescribed basis coordinate belongs to the local dependency closure of x.

Equations

• Wallace.ConcreteLocalSetup.RelevantCode N hN M x = Wallace.LocalCodeSchedule.RelevantCode Wallace.TriangularPreprocess.codeIndex (Wallace.ConcreteClosure.closure N hN M x)

def Wallace.ConcreteLocalSetup.refinedLabel (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : RelevantCode N hN M x → Set ℕ

Pairwise disjoint labels obtained by deleting finitely many points from each relevant almost-disjoint label.

Equations

• Wallace.ConcreteLocalSetup.refinedLabel N hN M x = Wallace.LocalCodeSchedule.refinedLabel Wallace.TriangularPreprocess.codeIndex (Wallace.ConcreteClosure.closure N hN M x) ⋯

theorem Wallace.ConcreteLocalSetup.label_diff_refinedLabel_finite (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) : (BlockData.label ↑a \ refinedLabel N hN M x a).Finite

noncomputable def Wallace.ConcreteLocalSetup.activeCode (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (l : ℕ) : Option (RelevantCode N hN M x)

The unique relevant code scheduled at label l, if there is one.

Equations

• Wallace.ConcreteLocalSetup.activeCode N hN M x l = Wallace.LocalCodeSchedule.activeCode Wallace.TriangularPreprocess.codeIndex (Wallace.ConcreteClosure.closure N hN M x) ⋯ l

theorem Wallace.ConcreteLocalSetup.activeCode_eq_some_of_mem (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (l : ℕ) (a : RelevantCode N hN M x) (ha : l ∈ refinedLabel N hN M x a) : activeCode N hN M x l = some a

Restriction to the countable local free group

noncomputable def Wallace.ConcreteLocalSetup.closureInclusion (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : (↑(ConcreteClosure.closure N hN M x) →₀ ℤ) →+ TriangularPreprocess.ContinuumFreeGroup

Inclusion of the free group on the closure coordinates into the ambient free group.

Equations

• Wallace.ConcreteLocalSetup.closureInclusion N hN M x = Finsupp.embDomain.addMonoidHom (Function.Embedding.subtype (Wallace.ConcreteClosure.closure N hN M x))

theorem Wallace.ConcreteLocalSetup.closureInclusion_apply (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (z : ↑(ConcreteClosure.closure N hN M x) →₀ ℤ) : (closureInclusion N hN M x) z = Finsupp.embDomain (Function.Embedding.subtype (ConcreteClosure.closure N hN M x)) z

theorem Wallace.ConcreteLocalSetup.closureInclusion_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) : Function.Injective ⇑(closureInclusion N hN M x)

noncomputable def Wallace.ConcreteLocalSetup.localDifference (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) (n : ℕ) : ↑(ConcreteClosure.closure N hN M x) →₀ ℤ

The shifted prepared value, restricted to the local closure.

Equations

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

theorem Wallace.ConcreteLocalSetup.closureInclusion_localDifference (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) (n : ℕ) : (closureInclusion N hN M x) (localDifference N hN M x a n) = ConcreteData.prepared N hN M (↑a) n - TriangularPreprocess.codeBasisVector ↑a

theorem Wallace.ConcreteLocalSetup.localDifference_injective (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) : Function.Injective (localDifference N hN M x a)

noncomputable def Wallace.ConcreteLocalSetup.localDifferenceBlock (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) (l : ℕ) : Finset (↑(ConcreteClosure.closure N hN M x) →₀ ℤ)

The independent shifted set in one block, now inside the countable local group.

Equations

• Wallace.ConcreteLocalSetup.localDifferenceBlock N hN M x a l = Finset.image (Wallace.ConcreteLocalSetup.localDifference N hN M x a) (Wallace.TriangularPreprocess.blockPositions N hN l)

theorem Wallace.ConcreteLocalSetup.localDifferenceBlock_card (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) (l : ℕ) : (localDifferenceBlock N hN M x a l).card = N l

theorem Wallace.ConcreteLocalSetup.localDifferenceBlock_image_inclusion (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) (l : ℕ) : Finset.image (⇑(closureInclusion N hN M x)) (localDifferenceBlock N hN M x a l) = ConcreteData.differenceBlock N hN M (↑a) l

theorem Wallace.ConcreteLocalSetup.localDifferenceBlock_boundedIndependent (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (a : RelevantCode N hN M x) (l : ℕ) : FiniteCombinatorics.BoundedIndependent (M l) (localDifferenceBlock N hN M x a l)

noncomputable def Wallace.ConcreteLocalSetup.localActiveBlock (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (l : ℕ) : Finset (↑(ConcreteClosure.closure N hN M x) →₀ ℤ)

The active finite set inside the local free group.

Equations

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

theorem Wallace.ConcreteLocalSetup.localActiveBlock_eq_of_mem (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (l : ℕ) (a : RelevantCode N hN M x) (ha : l ∈ refinedLabel N hN M x a) : localActiveBlock N hN M x l = localDifferenceBlock N hN M x a l

theorem Wallace.ConcreteLocalSetup.localActiveBlock_boundedIndependent (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (l : ℕ) : FiniteCombinatorics.BoundedIndependent (M l) (localActiveBlock N hN M x l)

theorem Wallace.ConcreteLocalSetup.localActiveBlock_card_le (N : ℕ → ℕ) (hN : ∀ (l : ℕ), 0 < N l) (M : ℕ → ℕ) (x : TriangularPreprocess.ContinuumFreeGroup) (l : ℕ) : (localActiveBlock N hN M x l).card ≤ N l