Core definitions + the count numerator (Mathlib)

Positions are ZMod N (N = d*m); level i = i.val / m, fiber i = i.val % m. A (d−1)-subset is level-canonical iff #{i ∈ S : level i ≤ j} ≤ j for all j < d.

Proved here (sorry-free): the count numerator #{(d−1)-subsets of Z_N} = C(N, d−1), via Mathlib's Fintype.card_finset_len + ZMod.card.

theorem CriticalPortraits.card_kSubsets (N k : ℕ) [NeZero N] : Fintype.card { S : Finset (ZMod N) // S.card = k } = N.choose k

The k-subsets of Z_N number C(N, k) (the count numerator).

def CriticalPortraits.level {N : ℕ} (m : ℕ) (i : ZMod N) : ℕ

level i = ⌊i / m⌋ for a position i ∈ Z_N (intended N = d*m).

Equations

• CriticalPortraits.level m i = i.val / m

def CriticalPortraits.fiber {N : ℕ} (m : ℕ) (i : ZMod N) : ℕ

fiber i = i mod m.

Equations

• CriticalPortraits.fiber m i = i.val % m

def CriticalPortraits.LevelCanonical (d m : ℕ) (S : Finset (ZMod (d * m))) : Prop

S ⊆ Z_{d*m} is level-canonical iff #{i ∈ S : level i ≤ j} ≤ j for every j < d.

Equations

• CriticalPortraits.LevelCanonical d m S = ∀ j < d, {i ∈ S | i.val / m ≤ j}.card ≤ j

@[implicit_reducible]

instance CriticalPortraits.instDecidableLevelCanonical (d m : ℕ) (S : Finset (ZMod (d * m))) : Decidable (LevelCanonical d m S)

Equations

• CriticalPortraits.instDecidableLevelCanonical d m S = id inferInstance