Permutation-Subset Combinatorics

@cite{anttila-1997} @cite{zuraw-2010}

A closed-form count of Equiv.Perm (Fin n) filtered by predicates of the form "the highest-ranked constraint in D lies in Y" — the canonical OT factorial-typology pattern.

Main result

perm_filter_head_in_card: for D Y : Finset (Fin n),

(# σ where head of permDList σ D ∈ Y) × |D| = n! × |Y ∩ D|

This reduces O(n!) constraint-ranking enumeration to closed-form arithmetic. Two factorial-typology studies consume it: Phenomena/Phonology/Studies/Zuraw2010.lean and Phenomena/Phonology/Studies/Anttila1997.lean.

Proof technique

For each y ∈ D, the fiber S_y = {σ : head of permDList σ D = y} is in bijection with any other fiber S_y' via left-multiplication by Equiv.swap y y' (which preserves D-membership pointwise and swaps the head element). All fibers thus have equal cardinality. Summing over D (which partitions Finset.univ when D is nonempty) gives |D| × |S_y| = n!, hence |S_y| = n!/|D|.

Scope

Specialized to head-in-Y predicates on Equiv.Perm (Fin n). A more general factoring theorem for arbitrary D-determined predicates is feasible (via orbit-stabilizer on the fixing subgroup of Dᶜ) but currently has no consumer in the OT-variation literature.

def Core.Constraint.PermSubsetCombinatorics.permToList {n : ℕ} (σ : Equiv.Perm (Fin n)) : List (Fin n)

The list [σ 0, σ 1, …, σ (n-1)] of σ's values in increasing index order.

Equations

• Core.Constraint.PermSubsetCombinatorics.permToList σ = List.map (⇑σ) (List.finRange n)

@[simp]

theorem Core.Constraint.PermSubsetCombinatorics.permToList_length {n : ℕ} (σ : Equiv.Perm (Fin n)) : (permToList σ).length = n

theorem Core.Constraint.PermSubsetCombinatorics.permToList_nodup {n : ℕ} (σ : Equiv.Perm (Fin n)) : (permToList σ).Nodup

@[simp]

theorem Core.Constraint.PermSubsetCombinatorics.mem_permToList {n : ℕ} (σ : Equiv.Perm (Fin n)) (x : Fin n) : x ∈ permToList σ

def Core.Constraint.PermSubsetCombinatorics.permDList {n : ℕ} (σ : Equiv.Perm (Fin n)) (D : Finset (Fin n)) : List (Fin n)

Subsequence of permToList σ filtered to elements of D. The head of this list is the σ-image element that lies in D and has the smallest preimage index — i.e., the highest-ranked constraint in the OT interpretation.

Equations

• Core.Constraint.PermSubsetCombinatorics.permDList σ D = List.filter (fun (x : Fin n) => decide (x ∈ D)) (Core.Constraint.PermSubsetCombinatorics.permToList σ)

theorem Core.Constraint.PermSubsetCombinatorics.permDList_nodup {n : ℕ} (σ : Equiv.Perm (Fin n)) (D : Finset (Fin n)) : (permDList σ D).Nodup

@[simp]

theorem Core.Constraint.PermSubsetCombinatorics.mem_permDList {n : ℕ} (σ : Equiv.Perm (Fin n)) (D : Finset (Fin n)) (x : Fin n) : x ∈ permDList σ D ↔ x ∈ D

@[simp]

theorem Core.Constraint.PermSubsetCombinatorics.permDList_toFinset {n : ℕ} (σ : Equiv.Perm (Fin n)) (D : Finset (Fin n)) : (permDList σ D).toFinset = D

@[simp]

theorem Core.Constraint.PermSubsetCombinatorics.permDList_length {n : ℕ} (σ : Equiv.Perm (Fin n)) (D : Finset (Fin n)) : (permDList σ D).length = D.card

theorem Core.Constraint.PermSubsetCombinatorics.permToList_split_at {n : ℕ} (σ : Equiv.Perm (Fin n)) (k : Fin n) : permToList σ = List.map (⇑σ) (List.take (↑k) (List.finRange n)) ++ σ k :: List.map (⇑σ) (List.drop (↑k + 1) (List.finRange n))

Decompose permToList σ at any position: the list factors as (take k).map σ ++ σ k :: (drop (k+1)).map σ.

theorem Core.Constraint.PermSubsetCombinatorics.permToList_eq_append_cons_imp_apply {n : ℕ} (σ : Equiv.Perm (Fin n)) (pre suf : List (Fin n)) (x : Fin n) (h_split : permToList σ = pre ++ x :: suf) (h_pre_lt : pre.length < n) : σ ⟨pre.length, h_pre_lt⟩ = x

Inverse: if permToList σ = pre ++ x :: suf, then σ at the canonical Fin-position pre.length equals x.

theorem Core.Constraint.PermSubsetCombinatorics.permDList_head_eq_some_iff {n : ℕ} (σ : Equiv.Perm (Fin n)) (D : Finset (Fin n)) (x : Fin n) : (permDList σ D).head? = some x ↔ x ∈ D ∧ ∃ (pre : List (Fin n)) (suf : List (Fin n)), permToList σ = pre ++ x :: suf ∧ ∀ y ∈ pre, y ∉ D

The head of permDList σ D characterized via mathlib's List.find?_eq_some_iff_append: head = some x iff x ∈ D and permToList σ decomposes as prefix ++ x :: suffix where every prefix element lies outside D.

theorem Core.Constraint.PermSubsetCombinatorics.permToList_mul {n : ℕ} (τ σ : Equiv.Perm (Fin n)) : permToList (τ * σ) = List.map (⇑τ) (permToList σ)

permToList of a left-multiplied permutation: (τ * σ).permToList equals σ.permToList with τ applied element-wise.

theorem Core.Constraint.PermSubsetCombinatorics.permDList_mul_of_preserves_D {n : ℕ} (D : Finset (Fin n)) (σ τ : Equiv.Perm (Fin n)) (h_pres : ∀ (x : Fin n), x ∈ D ↔ τ x ∈ D) : permDList (τ * σ) D = List.map (⇑τ) (permDList σ D)

When τ preserves D-membership both ways, the D-image of τ * σ is the D-image of σ with τ applied element-wise.

theorem Core.Constraint.PermSubsetCombinatorics.perm_filter_head_in_card {n : ℕ} (D Y : Finset (Fin n)) : {σ : Equiv.Perm (Fin n) | ∃ x ∈ Y, (permDList σ D).head? = some x}.card * D.card = n.factorial * (Y ∩ D).card

The closed-form count: for the predicate "head of permDList σ D lies in Y", the number of permutations satisfying it is n! × |Y ∩ D| / D.card, expressed in multiplied form to avoid ℕ division.

For each consonant in a factorial typology, this gives the per-consonant substitution count from a single application of the underlying head-fiber counting head_eq_card summed over Y ∩ D.

theorem Core.Constraint.PermSubsetCombinatorics.perm_filter_head_in_rate {n : ℕ} (D Y : Finset (Fin n)) : ↑{σ : Equiv.Perm (Fin n) | ∃ x ∈ Y, (permDList σ D).head? = some x}.card / ↑n.factorial = ↑(Y ∩ D).card / ↑D.card

Rational variation rate: the fraction of permutations with permDList-head in Y is |Y ∩ D| / |D| (both as ℚ).

Direct rational form of perm_filter_head_in_card, intended for consumers stating per-context probabilities (e.g. pocPredict … = 1/3). For empty D, both sides are 0/0 = 0 by Lean's convention.

Pure list-filter / head? facts about how (L.filter (· ∈ D)).head? behaves under subset relations between D and D'. Used by factorial-typology studies (e.g., Phenomena/Phonology/Studies/Zuraw2010.lean's structural voicing/place implications) to propagate "first element of L falling in D lies in Y" properties across distinguishing-set / favoring-set pairs.

Originally lived private inside Zuraw2010.lean; lifted here because they are pure list/Finset facts with zero phonology content, and any cross-input implication theorem in a binary-output OT factorial typology needs them.

theorem Core.Constraint.PermSubsetCombinatorics.filter_cons_head_of_mem {α : Type u_1} [DecidableEq α] (D : Finset α) (z : α) (zs : List α) (hzD : z ∈ D) : (List.filter (fun (x : α) => decide (x ∈ D)) (z :: zs)).head? = some z

Filtering z :: zs by (· ∈ D) when z ∈ D puts z first.

theorem Core.Constraint.PermSubsetCombinatorics.filter_cons_head_of_not_mem {α : Type u_1} [DecidableEq α] (D : Finset α) (z : α) (zs : List α) (hzD : z ∉ D) : (List.filter (fun (x : α) => decide (x ∈ D)) (z :: zs)).head? = (List.filter (fun (x : α) => decide (x ∈ D)) zs).head?

Filtering z :: zs by (· ∈ D) when z ∉ D recurses to zs.

theorem Core.Constraint.PermSubsetCombinatorics.head_filter_subset_extends {α : Type u_1} [DecidableEq α] {D D' Y Y' : Finset α} (h_D : D' ⊆ D) (h_Y : Y' ⊆ Y) (h_extra : ∀ x ∈ D, x ∉ D' → x ∈ Y) (L : List α) : (∃ x ∈ Y', (List.filter (fun (x : α) => decide (x ∈ D')) L).head? = some x) → ∃ y ∈ Y, (List.filter (fun (x : α) => decide (x ∈ D)) L).head? = some y

The head of a list filtered by a larger set D ⊇ D' still satisfies a "head-in-Y" property, provided Y' ⊆ Y and any element of the extra region D \ D' is in Y (so it counts as YES-favoring when it appears as the head of L.filter (· ∈ D)).

Used for "voicing-style" implications in factorial typology: if c' has a smaller distinguishing set than c and c's extras all favor YES, then c' subbed ⇒ c subbed.

theorem Core.Constraint.PermSubsetCombinatorics.head_filter_smaller_inherits {α : Type u_1} [DecidableEq α] {D D' Y Y' : Finset α} (h_D : D ⊆ D') (h_Y : Y' ⊆ Y) (h_Y_in_D : Y' ⊆ D) (L : List α) : (∃ x ∈ Y', (List.filter (fun (x : α) => decide (x ∈ D')) L).head? = some x) → ∃ y ∈ Y, (List.filter (fun (x : α) => decide (x ∈ D)) L).head? = some y

The head of a list filtered by a smaller set D ⊆ D' inherits a "head-in-Y" property from the larger filter, provided the YES-favorers Y' of the larger setting are entirely contained in the smaller D (so when the head of L.filter (· ∈ D') lies in Y', it is also in D, hence the head of L.filter (· ∈ D)).

Used for "place-style" implications in factorial typology: if c' has a larger distinguishing set than c but c''s YES-favorers all lie in c's smaller set, then c' subbed ⇒ c subbed.