Counting vertex maps: the birthday bound and injective-map counts (#94, shared infrastructure)

Pure finite combinatorics about maps Fin k → Fin n, extracted from the mixture-existence collision estimate so the t/t_inj/t_ind subgraph-density interlude (#94) can share it:

• Graphon.card_not_injective_le — the union (birthday) bound: at most k² · n^(k−1) maps are non-injective;
• Graphon.card_noninjective_div_card_le — the proportion form, ≤ k²/(n + 1);
• Graphon.inv_pow_eq_card_inv — the inverse-power sampling weight is the reciprocal vertex-map count;
• Graphon.card_filter_injective_eq_descFactorial — the injective-map count is the descending factorial n.descFactorial k (the normalizer of t_inj/t_ind).

theorem Graphon.card_not_injective_le (k m : ℕ) : ↑{f : Fin k → Fin m | ¬Function.Injective f}.card ≤ ↑k * ↑k * ↑m ^ (k - 1)

The union (birthday) bound: at most a k²/m proportion of vertex maps Fin k → Fin m are non-injective.

theorem Graphon.inv_pow_eq_card_inv (n k : ℕ) : (↑(n + 1))⁻¹ ^ k = (↑(Fintype.card (Fin k → Fin (n + 1))))⁻¹

The inverse-power sampling weight is the reciprocal vertex-map count.

theorem Graphon.card_noninjective_div_card_le (n k : ℕ) : ↑{f : Fin k → Fin (n + 1) | ¬Function.Injective f}.card / ↑(Fintype.card (Fin k → Fin (n + 1))) ≤ ↑k * ↑k / (↑n + 1)

The non-injective proportion of vertex maps is at most k²/(n + 1) (birthday bound plus arithmetic).

theorem Graphon.card_filter_injective_eq_descFactorial (k n : ℕ) : {f : Fin k → Fin n | Function.Injective f}.card = n.descFactorial k

The injective-map count is the descending factorial: there are exactly n.descFactorial k injective maps Fin k → Fin n — the normalizer of the injective and induced subgraph densities.

theorem Graphon.card_filter_not_injective_eq (k n : ℕ) : {f : Fin k → Fin n | ¬Function.Injective f}.card = n ^ k - n.descFactorial k

The non-injective map count is the complement of the descending factorial.