The /d denominator: #level-canonical = C(N, d-1)/d (all d), Mathlib, sorry-free.

PRIMARY (multiplicative form): d * #{S // S.card = d-1 ∧ LevelCanonical d m S} = (d*m).choose (d-1) COROLLARY (division form), one-liner from the above.

Route: rotation rhoPow t (translate by +(t*m)), the per-level count vector cnt, the cycle-lemma bridge (∃! canonical rotation index per (d-1)-subset), assembled into a bijection {(d-1)-subsets} ≃ {canonical} × Fin d (uniqueness of the canonical index supplies freeness for free), giving card = #canonical * d.

Part 0: a Fintype instance for the target subtype (all d, m).

The TARGET statement uses Fintype.card {S : Finset (ZMod (d*m)) // …} with no [NeZero (d*m)] binder, so we must provide the Fintype instance unconditionally. When d*m ≠ 0 it comes from NeZero; in the degenerate case d*m = 0 the predicate forces every S = ∅ (a singleton), so the subtype is still finite.

instance CriticalPortraits.instFiniteCanonical (d m : ℕ) : Finite { S : Finset (ZMod (d * m)) // S.card = d - 1 ∧ LevelCanonical d m S }

@[implicit_reducible]

noncomputable instance CriticalPortraits.instFintypeCanonical (d m : ℕ) : Fintype { S : Finset (ZMod (d * m)) // S.card = d - 1 ∧ LevelCanonical d m S }

Equations

• CriticalPortraits.instFintypeCanonical d m = Fintype.ofFinite { S : Finset (ZMod (d * m)) // S.card = d - 1 ∧ CriticalPortraits.LevelCanonical d m S }

Part 1: level arithmetic.

theorem CriticalPortraits.level_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (i : ZMod (d * m)) : i.val / m < d

Every level is < d (when N = d*m, m > 0).

theorem CriticalPortraits.shift_cast {d m : ℕ} (t : ℕ) : ↑(t * m) = ↑(t % d * m)

The shift element t*m reduces to (t%d)*m in ZMod (d*m).

theorem CriticalPortraits.shift_val_lt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (t : ℕ) : t % d * m < d * m

(t%d)*m < d*m, so its val is itself.

theorem CriticalPortraits.level_add {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (t : ℕ) (i : ZMod (d * m)) : (i + ↑(t * m)).val / m = (i.val / m + t % d) % d

The fundamental level-shift identity: translating by +(t*m) adds t to the level cyclically.

Part 2: counts and prefix sums.

def CriticalPortraits.cnt {d m : ℕ} (S : Finset (ZMod (d * m))) (j : ℕ) : ℕ

Number of elements of S at level exactly j.

Equations

• CriticalPortraits.cnt S j = {i ∈ S | i.val / m = j}.card

theorem CriticalPortraits.sum_cnt {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) : ∑ j ∈ Finset.range d, cnt S j = S.card

S is partitioned by level into range d: total count is S.card.

theorem CriticalPortraits.prefix_cnt {d m : ℕ} (S : Finset (ZMod (d * m))) (j : ℕ) : {i ∈ S | i.val / m ≤ j}.card = ∑ l ∈ Finset.range (j + 1), cnt S l

Prefix count: #{i ∈ S : level i ≤ j} = ∑_{l ≤ j} cnt S l.

Part 3: the rotation rhoPow and the count-shift.

theorem CriticalPortraits.cyc_round (a b d : ℕ) (_hd : 0 < d) (ha : a < d) (hb : b < d) : ((a + (d - b)) % d + b) % d = a

Cyclic round-trip: for a, b < d, (((a + (d-b)) % d) + b) % d = a.

theorem CriticalPortraits.cyc_inv (a b c d : ℕ) (_hd : 0 < d) (ha : a < d) (hb : b < d) (_hc : c < d) (h : c = (a + b) % d) : a = (c + (d - b)) % d

The inverse cyclic relation.

def CriticalPortraits.rhoPow {d m : ℕ} (t : ℕ) (S : Finset (ZMod (d * m))) : Finset (ZMod (d * m))

t-fold rotation: translate every element by +(t*m).

Equations

• CriticalPortraits.rhoPow t S = Finset.map (Equiv.toEmbedding (Equiv.addRight ↑(t * m))) S

@[simp]

theorem CriticalPortraits.card_rhoPow {d m : ℕ} (t : ℕ) (S : Finset (ZMod (d * m))) : (rhoPow t S).card = S.card

theorem CriticalPortraits.mem_rhoPow {d m : ℕ} (t : ℕ) (S : Finset (ZMod (d * m))) (x : ZMod (d * m)) : x ∈ rhoPow t S ↔ ∃ y ∈ S, y + ↑(t * m) = x

theorem CriticalPortraits.rhoPow_add {d m : ℕ} (t u : ℕ) (S : Finset (ZMod (d * m))) : rhoPow t (rhoPow u S) = rhoPow (t + u) S

Composing rotations: rhoPow t (rhoPow u S) = rhoPow (t + u) S.

@[simp]

theorem CriticalPortraits.rhoPow_zero {d m : ℕ} (S : Finset (ZMod (d * m))) : rhoPow 0 S = S

rhoPow 0 S = S.

theorem CriticalPortraits.rhoPow_period {d m : ℕ} (S : Finset (ZMod (d * m))) : rhoPow d S = S

rhoPow d S = S (a full cycle is the identity).

theorem CriticalPortraits.rhoPow_mod {d m : ℕ} (t : ℕ) (S : Finset (ZMod (d * m))) : rhoPow (t % d) S = rhoPow t S

rhoPow only depends on t % d.

theorem CriticalPortraits.cnt_rhoPow {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (t : ℕ) (S : Finset (ZMod (d * m))) (j : ℕ) (hj : j < d) : cnt (rhoPow t S) j = cnt S ((j + (d - t % d)) % d)

The count-shift: rotating by t shifts the level-count vector cyclically. For j < d, the elements of rhoPow t S at level j biject (via +t'*m) with the elements of S at level (j + (d - t%d)) % d.

Part 4: the period-d count sequence and the cycle-lemma bridge.

def CriticalPortraits.aP {d m : ℕ} (S : Finset (ZMod (d * m))) (l : ℕ) : ℕ

The period-d natural count sequence: aP S l = cnt S (l % d).

Equations

• CriticalPortraits.aP S l = CriticalPortraits.cnt S (l % d)

def CriticalPortraits.bSeq {d m : ℕ} (S : Finset (ZMod (d * m))) (l : ℕ) : ℤ

The integer complement sequence whose partial sums drive the cycle lemma: bSeq S l = 1 - (aP S l : ℤ).

Equations

• CriticalPortraits.bSeq S l = 1 - ↑(CriticalPortraits.aP S l)

theorem CriticalPortraits.aP_lt {d m : ℕ} (S : Finset (ZMod (d * m))) {l : ℕ} (hl : l < d) : aP S l = cnt S l

theorem CriticalPortraits.bSeq_periodic {d m : ℕ} (S : Finset (ZMod (d * m))) (k : ℕ) : bSeq S (k + d) = bSeq S k

theorem CriticalPortraits.sum_aP {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) : ∑ l ∈ Finset.range d, ↑(aP S l) = ↑S.card

Period sum of aP is S.card.

theorem CriticalPortraits.Q_bSeq_d {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) : Cycle.Q (bSeq S) d = ↑d - ↑S.card

Period sum of bSeq over range d is d - S.card.

theorem CriticalPortraits.Q_bSeq_d_one {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) (hcard : S.card = d - 1) : Cycle.Q (bSeq S) d = 1

For a (d-1)-subset, the period sum of bSeq is exactly 1.

theorem CriticalPortraits.Q_bSeq_eq {d m : ℕ} (S : Finset (ZMod (d * m))) (k : ℕ) : Cycle.Q (bSeq S) k = ↑k - ∑ l ∈ Finset.range k, ↑(aP S l)

The integer partial sum Q (bSeq S) k = k - (∑_{l<k} aP S l).

theorem CriticalPortraits.Q_bSeq_period {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) (hcard : S.card = d - 1) (k : ℕ) : Cycle.Q (bSeq S) (k + d) = Cycle.Q (bSeq S) k + 1

Periodicity of the partial sums of bSeq for a (d-1)-subset.

Part 5: the core equivalence LevelCanonical ↔ Good.

theorem CriticalPortraits.prefix_rhoPow {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (t : ℕ) (ht : t < d) (S : Finset (ZMod (d * m))) (j : ℕ) (hj : j < d) : ∑ l ∈ Finset.range (j + 1), ↑(cnt (rhoPow t S) l) = ∑ l ∈ Finset.range (j + 1), ↑(aP S (l + (d - t)))

The prefix sum of the rotated count is a shifted window of aP. For t < d and j < d, with e = d - t.

theorem CriticalPortraits.sum_shift_window (f : ℕ → ℤ) (e j : ℕ) : ∑ l ∈ Finset.range (j + 1), f (l + e) = ∑ l ∈ Finset.range (e + (j + 1)), f l - ∑ l ∈ Finset.range e, f l

Reindex: ∑_{l<j+1} f (l + e) = (∑_{l<e+j+1} f) - (∑_{l<e} f).

theorem CriticalPortraits.lc_index_iff {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (t : ℕ) (ht : t < d) (S : Finset (ZMod (d * m))) (j : ℕ) (hj : j < d) : {i ∈ rhoPow t S | i.val / m ≤ j}.card ≤ j ↔ Cycle.Q (bSeq S) (d - t) < Cycle.Q (bSeq S) (d - t + (j + 1))

The LC prefix inequality (index j) for rhoPow t S, recast via partial sums of bSeq. For t < d, j < d, with e = d - t: (#{i ∈ rhoPow t S : level i ≤ j} ≤ j) ↔ Q b e < Q b (e + (j+1)).

theorem CriticalPortraits.Q_e_c_cross {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) (hcard : S.card = d - 1) (t : ℕ) (ht : t < d) (x : ℕ) : Cycle.Q (bSeq S) (d - t) + Cycle.Q (bSeq S) ((d - t) % d + x) = Cycle.Q (bSeq S) ((d - t) % d) + Cycle.Q (bSeq S) (d - t + x)

Cross-equality relating Q b e to Q b c where c = e % d and e ≤ d (so e = c, or e = d with c = 0).

theorem CriticalPortraits.lc_iff_good {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) (hcard : S.card = d - 1) (t : ℕ) (ht : t < d) : LevelCanonical d m (rhoPow t S) ↔ Cycle.Good d (bSeq S) ((d - t) % d)

The cycle-lemma bridge (single rotation). For t < d and a (d-1)-subset S, LevelCanonical d m (rhoPow t S) ↔ Good d (bSeq S) ((d - t) % d).

Part 7: the unique canonical rotation index.

theorem CriticalPortraits.sigma_lt {d : ℕ} (hd : 0 < d) (t : ℕ) : (d - t) % d < d

σ t = (d - t) % d is < d.

theorem CriticalPortraits.sigma_invol {d : ℕ} (_hd : 0 < d) {t : ℕ} (ht : t < d) : (d - (d - t) % d) % d = t

σ is an involution on [0, d): (d - ((d - t) % d)) % d = t for t < d.

theorem CriticalPortraits.canonical_unique {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) (hcard : S.card = d - 1) : ∃! t : ℕ, t < d ∧ LevelCanonical d m (rhoPow t S)

The unique canonical rotation. For a (d-1)-subset S, exactly one t ∈ [0,d) makes rhoPow t S level-canonical.

Part 8: the bijection {(d-1)-subsets} ≃ {canonical} × Fin d.

noncomputable def CriticalPortraits.canIdx {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) : ℕ

The canonical rotation index of a (d-1)-subset (junk 0 for non-(d-1)-subsets).

Equations

• CriticalPortraits.canIdx hd hm S = if h : S.card = d - 1 then Exists.choose ⋯ else 0

theorem CriticalPortraits.canIdx_spec {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) (hcard : S.card = d - 1) : canIdx hd hm S < d ∧ LevelCanonical d m (rhoPow (canIdx hd hm S) S)

theorem CriticalPortraits.canIdx_eq {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (S : Finset (ZMod (d * m))) (hcard : S.card = d - 1) {t : ℕ} (htd : t < d) (htLC : LevelCanonical d m (rhoPow t S)) : t = canIdx hd hm S

Uniqueness characterization of canIdx.

theorem CriticalPortraits.canIdx_of_canonical {d m : ℕ} (hd : 0 < d) (hm : 0 < m) (c : Finset (ZMod (d * m))) (hcard : c.card = d - 1) (hLC : LevelCanonical d m c) : canIdx hd hm c = 0

For a canonical (d-1)-subset, the canonical index is 0.

theorem CriticalPortraits.rhoPow_round {d m : ℕ} (t : ℕ) (ht : t < d) (S : Finset (ZMod (d * m))) : rhoPow ((d - t) % d) (rhoPow t S) = S

rhoPow is "mod-d periodic with the round-trip cancelling to identity".

@[reducible, inline]

abbrev CriticalPortraits.Asub (d m : ℕ) : Type

The Fintype subtype of (d-1)-subsets.

Equations

• CriticalPortraits.Asub d m = { S : Finset (ZMod (d * m)) // S.card = d - 1 }

@[reducible, inline]

abbrev CriticalPortraits.Csub (d m : ℕ) : Type

The Fintype subtype of canonical (d-1)-subsets (the TARGET).

Equations

• CriticalPortraits.Csub d m = { S : Finset (ZMod (d * m)) // S.card = d - 1 ∧ CriticalPortraits.LevelCanonical d m S }

noncomputable def CriticalPortraits.equivCanFin {d m : ℕ} (hd : 0 < d) (hm : 0 < m) : Asub d m ≃ Csub d m × Fin d

The bijection Asub ≃ Csub × Fin d.

Equations

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

Part 9: the final count.

theorem CriticalPortraits.card_levelCanonical_mul (d m : ℕ) (hd : 0 < d) (hm : 0 < m) : d * Fintype.card { S : Finset (ZMod (d * m)) // S.card = d - 1 ∧ LevelCanonical d m S } = (d * m).choose (d - 1)

PRIMARY. d · #{canonical (d-1)-subsets} = C(d*m, d-1).

theorem CriticalPortraits.card_levelCanonical (d m : ℕ) (hd : 0 < d) (hm : 0 < m) : Fintype.card { S : Finset (ZMod (d * m)) // S.card = d - 1 ∧ LevelCanonical d m S } = (d * m).choose (d - 1) / d

COROLLARY. #{canonical (d-1)-subsets} = C(d*m, d-1) / d.