Permutation-subset combinatorics

A closed-form count of Equiv.Perm (Fin n) filtered by predicates of the form "the head of a list filtered by D lies in Y".

Main results

For any family S : Finset (Equiv.Perm (Fin n)) closed under left-multiplication by swaps of elements of D:

• filter_head_in_card_of_swaps: (# σ ∈ S where head of permDList σ D ∈ Y) × |D| = |S| × |Y ∩ D|
• filter_head_in_rate_of_swaps: the rational form (count / |S|) = |Y ∩ D| / |D|.

perm_filter_head_in_card / perm_filter_head_in_rate are the S = Finset.univ specializations (|S| = n!), consumed by Studies/Zuraw2010.lean and Studies/CoetzeePater2011.lean. The swap-closed generality serves partially-ordered constraint grammars, whose consistent-linear-extension sets are swap-closed within a freely ranked stratum (winProb_stratified_binary_rate in Phonology/OptimalityTheory/PartiallyOrderedConstraints.lean).

Proof technique

For y, y' ∈ D, left-multiplication by Equiv.swap y y' preserves D-membership pointwise and swaps the head element, so it restricts to a bijection between the head-fibers {σ ∈ S : head of permDList σ D = y} and {σ ∈ S : … = y'} whenever S is closed under it. All fibers thus have equal cardinality; summing over D (which partitions S when D is nonempty) gives |D| × |fiber| = |S|.

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

Subsequence of List.ofFn ⇑σ (σ's values in increasing position order) 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.Optimization.PermSubsetCombinatorics.permDList σ D = List.filter (fun (x : Fin n) => decide (x ∈ D)) (List.ofFn ⇑σ)

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem Core.Optimization.PermSubsetCombinatorics.take_map_eq_of_ofFn_eq_append_cons {n : ℕ} (σ : Equiv.Perm (Fin n)) {pre suf : List (Fin n)} {x : Fin n} (h_split : List.ofFn ⇑σ = pre ++ x :: suf) (h_pre_lt : pre.length < n) : List.map (⇑σ) (List.take pre.length (List.finRange n)) = pre

In a decomposition List.ofFn ⇑σ = pre ++ x :: suf, the prefix is the σ-image of the first pre.length positions.

theorem Core.Optimization.PermSubsetCombinatorics.symm_lt_of_ofFn_eq_append_cons {n : ℕ} (σ : Equiv.Perm (Fin n)) {pre suf : List (Fin n)} {x y : Fin n} (h_split : List.ofFn ⇑σ = pre ++ x :: suf) (hy : y ∈ pre) : (Equiv.symm σ) y < (Equiv.symm σ) x

Elements of the prefix of a List.ofFn ⇑σ decomposition occupy strictly earlier positions than the distinguished element.

theorem Core.Optimization.PermSubsetCombinatorics.mem_pre_of_symm_lt {n : ℕ} (σ : Equiv.Perm (Fin n)) {pre suf : List (Fin n)} {x y : Fin n} (h_split : List.ofFn ⇑σ = pre ++ x :: suf) (hy : (Equiv.symm σ) y < (Equiv.symm σ) x) : y ∈ pre

Converse of symm_lt_of_ofFn_eq_append_cons: a value positioned strictly before x lies in the prefix.

theorem Core.Optimization.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)), List.ofFn ⇑σ = 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 List.ofFn ⇑σ decomposes as prefix ++ x :: suffix where every prefix element lies outside D.

theorem Core.Optimization.PermSubsetCombinatorics.mem_of_permDList_head?_eq_some {n : ℕ} {D : Finset (Fin n)} {σ : Equiv.Perm (Fin n)} {x : Fin n} (h : (permDList σ D).head? = some x) : x ∈ D

If (permDList σ D).head? = some x then x ∈ D (the head of a filtered list lies in the filter set).

theorem Core.Optimization.PermSubsetCombinatorics.exists_permDList_head?_eq_some {n : ℕ} {D : Finset (Fin n)} (h_nonempty : D.Nonempty) (σ : Equiv.Perm (Fin n)) : ∃ y ∈ D, (permDList σ D).head? = some y

For nonempty D, the head of permDList σ D is always defined and lies in D.

theorem Core.Optimization.PermSubsetCombinatorics.permDList_head?_eq_some_iff_min {n : ℕ} (σ : Equiv.Perm (Fin n)) (D : Finset (Fin n)) (x : Fin n) : (permDList σ D).head? = some x ↔ x ∈ D ∧ ∀ y ∈ D, (Equiv.symm σ) x ≤ (Equiv.symm σ) y

The head of permDList σ D is the σ-earliest element of D: head? = some x iff x lies in D and no D-element occupies an earlier position. The position-minimum characterization, complementing the decomposition form permDList_head_eq_some_iff.

theorem Core.Optimization.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. Composes mathlib's List.map_ofFn and List.filter_map.

theorem Core.Optimization.PermSubsetCombinatorics.filter_head_in_card_of_swaps {n : ℕ} (S : Finset (Equiv.Perm (Fin n))) (D Y : Finset (Fin n)) (h_closed : ∀ y₁ ∈ D, ∀ y₂ ∈ D, ∀ σ ∈ S, Equiv.swap y₁ y₂ * σ ∈ S) : {σ ∈ S | ∃ x ∈ Y, (permDList σ D).head? = some x}.card * D.card = S.card * (Y ∩ D).card

The closed-form count over a swap-closed family: for S closed under left-multiplication by swaps of D-elements, the number of σ ∈ S whose permDList σ D head lies in Y is |S| × |Y ∩ D| / |D|, expressed in multiplied form to avoid ℕ division.

theorem Core.Optimization.PermSubsetCombinatorics.filter_head_in_rate_of_swaps {n : ℕ} (S : Finset (Equiv.Perm (Fin n))) (D Y : Finset (Fin n)) (h_S : S.Nonempty) (h_closed : ∀ y₁ ∈ D, ∀ y₂ ∈ D, ∀ σ ∈ S, Equiv.swap y₁ y₂ * σ ∈ S) : ↑{σ ∈ S | ∃ x ∈ Y, (permDList σ D).head? = some x}.card / ↑S.card = ↑(Y ∩ D).card / ↑D.card

Rational rate over a swap-closed family: the fraction of σ ∈ S with permDList-head in Y is |Y ∩ D| / |D| (both as ℚ). For empty D, both sides are 0 by Lean's 0/0 = 0 convention.

theorem Core.Optimization.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 over all permutations: S = Finset.univ specialization of filter_head_in_card_of_swaps (|S| = n!).

theorem Core.Optimization.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 ℚ). S = Finset.univ specialization of filter_head_in_rate_of_swaps, intended for consumers stating per-context probabilities (e.g. winProb … = 1/3).

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., 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.Optimization.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.Optimization.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.Optimization.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.Optimization.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.