Sparse periodic masks

The bookkeeping in this file is purely combinatorial. In particular it does not use a matrix-mortality theorem: that theorem will be a hypothesis of the sequence construction.

We use the integral invariant 4 * assigned < period. If a compatible word has length l, repeating the old mask 4*l+1 times before installing the word preserves this invariant. Thus no limiting density or geometric-series calculation is needed.

def KoetheCounterexample.MaskSequence.Extends {k : Type u_1} [Field k] (N M : PeriodicMask k) : Prop

All assignments, at all sites, of M persist in N.

Equations

• KoetheCounterexample.MaskSequence.Extends N M = ∀ (n : ℕ) (z : KoetheCounterexample.Triple k), M.lookup n = some z → N.lookup n = some z

theorem KoetheCounterexample.MaskSequence.Extends.refl {k : Type u_1} [Field k] (M : PeriodicMask k) : Extends M M

theorem KoetheCounterexample.MaskSequence.Extends.trans {k : Type u_1} [Field k] {L M N : PeriodicMask k} (hNM : Extends N M) (hML : Extends M L) : Extends N L

theorem KoetheCounterexample.MaskSequence.lookup_nonzero {k : Type u_1} [Field k] (M : PeriodicMask k) {n : ℕ} {z : Triple k} (h : M.lookup n = some z) : z ≠ 0

@[simp]

theorem KoetheCounterexample.MaskSequence.lookup_fin {k : Type u_1} [Field k] (M : PeriodicMask k) (i : Fin M.period) : M.lookup ↑i = M.value i

theorem KoetheCounterexample.MaskSequence.lookup_mod_of_dvd {k : Type u_1} [Field k] (M : PeriodicMask k) {p : ℕ} (hp : M.period ∣ p) (n : ℕ) : M.lookup (n % p) = M.lookup n

theorem KoetheCounterexample.MaskSequence.lookup_add_of_mod_eq_zero {k : Type u_1} [Field k] (M : PeriodicMask k) {b : ℕ} (hb : b % M.period = 0) (i : ℕ) : M.lookup (b + i) = M.lookup i

theorem KoetheCounterexample.MaskSequence.holes_add_assigned {k : Type u_1} [Field k] (M : PeriodicMask k) : M.holes + M.assigned = M.period

theorem KoetheCounterexample.MaskSequence.enough_holes {k : Type u_1} [Field k] (M : PeriodicMask k) (h : 4 * M.assigned < M.period) : M.period < 2 * M.holes

def KoetheCounterexample.MaskSequence.emptyMask {k : Type u_1} [Field k] : PeriodicMask k

The unassigned mask of period one.

Equations

• KoetheCounterexample.MaskSequence.emptyMask = { period := 1, period_pos := KoetheCounterexample.MaskSequence.emptyMask._proof_1, value := fun (x : Fin 1) => none, nonzero := ⋯ }

@[simp]

theorem KoetheCounterexample.MaskSequence.emptyMask_assigned {k : Type u_1} [Field k] : emptyMask.assigned = 0

theorem KoetheCounterexample.MaskSequence.lifted_assigned_card {k : Type u_1} [Field k] (M : PeriodicMask k) (c : ℕ) : {i : Fin (c * M.period) | M.lookup ↑i ≠ none}.card = c * M.assigned

Exact cardinal count for lifting all old assignments to c periods.

def KoetheCounterexample.MaskSequence.install {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) : PeriodicMask k

Refine a mask by installing a nonzero compatible word in its first block. Outside that block every previous assignment is retained.

Equations

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

@[simp]

theorem KoetheCounterexample.MaskSequence.install_period {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) : (install M w hw).period = (4 * w.length + 1) * M.period

theorem KoetheCounterexample.MaskSequence.period_dvd_install {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) : M.period ∣ (install M w hw).period

theorem KoetheCounterexample.MaskSequence.length_le_install_period {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) : w.length ≤ (install M w hw).period

theorem KoetheCounterexample.MaskSequence.install_extends {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) (hc : M.Compatible w) : Extends (install M w hw) M

theorem KoetheCounterexample.MaskSequence.install_word {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) (i : Fin w.length) : (install M w hw).lookup ↑i = some (w.get i)

theorem KoetheCounterexample.MaskSequence.install_assigned_le {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) : (install M w hw).assigned ≤ (4 * w.length + 1) * M.assigned + w.length

Installing the word adds at most its length to the lifted assigned set.

theorem KoetheCounterexample.MaskSequence.install_sparse {k : Type u_1} [Field k] (M : PeriodicMask k) (w : List (Triple k)) (hw : ∀ z ∈ w, z ≠ 0) (hM : 4 * M.assigned < M.period) : 4 * (install M w hw).assigned < (install M w hw).period

An adaptive integral density budget: the positive old slack is amplified by 4 * length + 1, whereas the cost of the new block is at most 4 * length. The new slack is therefore still at least one.