Maximal chains in the Boolean lattice

A permutation σ : Equiv.Perm (Fin m) records the order in which elements are inserted into a maximal chain. The state at level j consists of the first j elements in that order. The lemmas below expose both the ranked chain structure and the exact one-element insertion step needed by the mass transport argument.

def Feige.chainState {m : ℕ} (σ : Equiv.Perm (Fin m)) (j : Fin (m + 1)) : Finset (Fin m)

The level-j state of the maximal Boolean-lattice chain encoded by σ. Here σ k is the element inserted at step k.

Equations

• Feige.chainState σ j = Finset.map (Equiv.toEmbedding σ) {k : Fin m | ↑k < ↑j}

@[simp]

theorem Feige.mem_chainState_iff {m : ℕ} (σ : Equiv.Perm (Fin m)) (j : Fin (m + 1)) (i : Fin m) : i ∈ chainState σ j ↔ ↑((Equiv.symm σ) i) < ↑j

@[simp]

theorem Feige.chainState_zero {m : ℕ} (σ : Equiv.Perm (Fin m)) : chainState σ 0 = ∅

@[simp]

theorem Feige.chainState_last {m : ℕ} (σ : Equiv.Perm (Fin m)) : chainState σ (Fin.last m) = Finset.univ

@[simp]

theorem Feige.card_chainState {m : ℕ} (σ : Equiv.Perm (Fin m)) (j : Fin (m + 1)) : (chainState σ j).card = ↑j

theorem Feige.chainState_mono {m : ℕ} (σ : Equiv.Perm (Fin m)) {j k : Fin (m + 1)} (hjk : j ≤ k) : chainState σ j ⊆ chainState σ k

States are monotone in their level.

theorem Feige.perm_not_mem_chainState_castSucc {m : ℕ} (σ : Equiv.Perm (Fin m)) (j : Fin m) : σ j ∉ chainState σ j.castSucc

The element inserted at step j was not present before that step.

theorem Feige.chainState_succ {m : ℕ} (σ : Equiv.Perm (Fin m)) (j : Fin m) : chainState σ j.succ = insert (σ j) (chainState σ j.castSucc)

Passing from level j to level j+1 inserts exactly σ j.

theorem Feige.chainState_succ_sdiff {m : ℕ} (σ : Equiv.Perm (Fin m)) (j : Fin m) : chainState σ j.succ \ chainState σ j.castSucc = {σ j}

Consecutive states differ by precisely the singleton containing the next permutation element.

theorem Feige.chainState_ssubset {m : ℕ} (σ : Equiv.Perm (Fin m)) {j k : Fin (m + 1)} (hjk : j < k) : chainState σ j ⊂ chainState σ k

Distinct levels are strictly nested.