Separate spatial and material budgets for actual Leibniz subwords.

theorem AVenhance.Infra.Section4.amnrMixedWord_count_none (α : List (Fin 2)) (n : ℕ) : List.count none (amnrMixedWord α n) = n

A canonical mixed word contains exactly its prescribed material count.

theorem AVenhance.Infra.Section4.amnrMixedWord_subword_normalForm {α : List (Fin 2)} {n : ℕ} {v : List (Option (Fin 2))} (hv : v.Sublist (amnrMixedWord α n)) : ∃ (η : List (Fin 2)) (r : ℕ), v = amnrMixedWord η r ∧ r ≤ n ∧ η.length + 2 * r ≤ α.length + 2 * n

A Leibniz subword is canonical and never gains spatial or material budget. The material count is controlled separately for strong induction.