The headline census theorem: #{portraits} = C(N, d−1) / d for all d

This module assembles the four proved, sorry-free ingredients into the final count. With positions in ZMod N (N = d*m) and the delete-min map T:

• Forward (T_levelCanonical) + weight (T_card): T maps each portrait to a level-canonical (d−1)-subset, i.e. Set.MapsTo T {P | Portrait} {U | U.card = d−1 ∧ …}.
• Injectivity (T_injOn) and Surjectivity (T_surjOn) upgrade this to Set.BijOn.
• Set.BijOn.equiv then gives an equivalence of the two subtypes, so their Fintype.cards agree; composing with the denominator count card_levelCanonical_mul yields the result.

theorem CriticalPortraits.card_portraits_mul {d m : ℕ} (hd : 0 < d) (hm : 0 < m) : d * Fintype.card { P : Finset (Finset (ZMod (d * m))) // Portrait d m P } = (d * m).choose (d - 1)

PRIMARY (multiplicative form). d · #{portraits} = C(d*m, d-1).

The cleanest statement: the count of portraits times d equals the binomial numerator. Proved by the T-bijection onto level-canonical (d−1)-subsets composed with card_levelCanonical_mul.

theorem CriticalPortraits.card_portraits {d m : ℕ} (hd : 0 < d) (hm : 0 < m) : Fintype.card { P : Finset (Finset (ZMod (d * m))) // Portrait d m P } = (d * m).choose (d - 1) / d

HEADLINE CENSUS THEOREM. #{portraits} = C(d*m, d-1) / d for all d (and all m).

The number of degree-d portraits at level m equals C(d·m, d−1) / d. Follows from the multiplicative form by Nat.div_eq_of_eq_mul_right (exact ℕ-division, no remainder).

theorem CriticalPortraits.d_dvd_choose {d m : ℕ} (hd : 0 < d) (hm : 0 < m) : d ∣ (d * m).choose (d - 1)

Exactness of the / d. The denominator divides the numerator: d ∣ C(d*m, d-1). Hence the / d in card_portraits is exact ℕ-division (the count is a genuine integer), not floor rounding — the witness is the portrait count itself, read off card_portraits_mul.