Periodic masks and independent connector holes

Free positions are enumerated as a finite subtype of occurrences, not as residue classes. In particular a connector of length m * period has m * holes distinct projective blocks.

theorem KoetheCounterexample.Mortality.lookup_add_of_dvd {k : Type u_1} [Field k] (M : PeriodicMask k) (a b : ℕ) (ha : M.period ∣ a) : M.lookup (a + b) = M.lookup b

theorem KoetheCounterexample.Mortality.compatible_append {k : Type u_1} [Field k] (M : PeriodicMask k) {u v : List (Triple k)} (hu : M.Compatible u) (hv : M.Compatible v) (hlen : M.period ∣ u.length) : M.Compatible (u ++ v)

theorem KoetheCounterexample.Mortality.compatible_ofFn {k : Type u_1} [Field k] (M : PeriodicMask k) {L : ℕ} (f : Fin L → Triple k) (hf : ∀ (i : Fin L) (z : Triple k), M.lookup ↑i = some z → f i = z) : M.Compatible (List.ofFn f)

@[reducible, inline]

abbrev KoetheCounterexample.Mortality.FreePos {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) : Type

Actual unassigned occurrences in a finite interval.

Equations

• KoetheCounterexample.Mortality.FreePos M L = { i : Fin L // M.lookup ↑i = none }

@[instance_reducible]

instance KoetheCounterexample.Mortality.freePosFintype {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) : Fintype (FreePos M L)

Equations

• KoetheCounterexample.Mortality.freePosFintype M L = Subtype.fintype fun (i : Fin L) => M.lookup ↑i = none

def KoetheCounterexample.Mortality.freeCount {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) : ℕ

The number of free positions in the initial interval of length L.

Equations

• KoetheCounterexample.Mortality.freeCount M L = Fintype.card (KoetheCounterexample.Mortality.FreePos M L)

noncomputable def KoetheCounterexample.Mortality.freeIndex {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) : FreePos M L ≃ Fin (freeCount M L)

An enumeration of the free positions in the initial interval of length L.

Equations

• KoetheCounterexample.Mortality.freeIndex M L = Fintype.equivFin (KoetheCounterexample.Mortality.FreePos M L)

theorem KoetheCounterexample.Mortality.lookup_finProd {k : Type u_1} [Field k] (M : PeriodicMask k) {m : ℕ} (a : Fin m) (b : Fin M.period) : M.lookup ↑(finProdFinEquiv (a, b)) = M.value b

theorem KoetheCounterexample.Mortality.freeCount_mul_period {k : Type u_1} [Field k] (M : PeriodicMask k) (m : ℕ) : freeCount M (m * M.period) = m * M.holes

Exact independent-hole count, including zero repetitions.

noncomputable def KoetheCounterexample.Mortality.connectorLetter {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) (i : Fin L) : FormalLetter k (freeCount M L)

A fixed letter at assigned positions; a distinct variable block at each hole.

Equations

• KoetheCounterexample.Mortality.connectorLetter M L i = match h : M.lookup ↑i with | none => Sum.inr ((KoetheCounterexample.Mortality.freeIndex M L) ⟨i, h⟩) | some z => Sum.inl z

noncomputable def KoetheCounterexample.Mortality.formalConnector {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) : List (FormalLetter k (freeCount M L))

The formal word of length L reading the mask: its fixed letter at each assigned position and a distinct hole at each free position.

Equations

• KoetheCounterexample.Mortality.formalConnector M L = List.ofFn (KoetheCounterexample.Mortality.connectorLetter M L)

@[simp]

theorem KoetheCounterexample.Mortality.formalConnector_length {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) : (formalConnector M L).length = L

theorem KoetheCounterexample.Mortality.connectorLetter_of_none {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) (i : Fin L) (h : M.lookup ↑i = none) : connectorLetter M L i = Sum.inr ((freeIndex M L) ⟨i, h⟩)

theorem KoetheCounterexample.Mortality.connectorLetter_of_some {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) (i : Fin L) (z : Triple k) (h : M.lookup ↑i = some z) : connectorLetter M L i = Sum.inl z

theorem KoetheCounterexample.Mortality.formalConnector_degree {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) : (List.map letterDegree (formalConnector M L)).sum = fun (x : Fin (freeCount M L)) => 1

Each enumerated hole contributes exactly one copy of its block degree.

theorem KoetheCounterexample.Mortality.specialized_connector_nonzero {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) (x : Fin (freeCount M L) × Fin 3 → k) (hx : ∀ (b : Fin (freeCount M L)), (fun (j : Fin 3) => x (b, j)) ≠ 0) (z : Triple k) : z ∈ List.map (specializeLetter x) (formalConnector M L) → z ≠ 0

theorem KoetheCounterexample.Mortality.specialized_connector_compatible {k : Type u_1} [Field k] (M : PeriodicMask k) (L : ℕ) (x : Fin (freeCount M L) × Fin 3 → k) : M.Compatible (List.map (specializeLetter x) (formalConnector M L))

theorem KoetheCounterexample.Mortality.exists_compatible_block {k : Type u_1} [Field k] (M : PeriodicMask k) : ∃ (w : List (Triple k)), w.length = M.period ∧ (∀ z ∈ w, z ≠ 0) ∧ M.Compatible w

There is an initial compatible, nonzero word of exactly one mask period.