YoungRule.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Saxl.rowWeights line 12

Source comment

Horizontal-strip chains recording the exact ordered strip sizes.

def rowWeights (θ : YoungDiagram) : ℕ → List ℕ
  | 0 => []
  | k+1 => rowWeights θ k ++ [θ.rowLen k]

lemma OAI.Saxl.rowWeights_congr line 16
lemma OAI.Saxl.card_zero_iff_bot line 23
theorem OAI.Saxl.sizedStripChain_of_dominates line 32
Source comment
The actual constructive sufficiency step in Young's rule. No tableau, Pieri, or representation hypothesis is assumed by this combinatorial theorem.
```
theorem sizedStripChain_of_dominates (θ τ : YoungDiagram) (k : ℕ)
    (hh : θ.colLen 0 ≤ k) (hc : τ.card = θ.card) (hd : Dominates τ θ) :
    SizedStripChain (rowWeights θ k) ⊥ τ := by
…
```
Mentions: OAI.Saxl.Dominates, OAI.Saxl.SizedStripChain, OAI.Saxl.rowWeights
lemma OAI.Saxl.rowWeights_length line 61
lemma OAI.Saxl.rowWeights_getElem line 66
lemma OAI.Saxl.perm_of_equal_content line 79
lemma OAI.Saxl.vector_of_invariant_functional line 92

theorem OAI.Saxl.young_invariant_functional line 117

Source comment

Young's sufficiency in the exact form needed for the repeated-row quotient: a dominant Specht has a nonzero invariant functional for a word of the prescribed content.

theorem young_invariant_functional (θ τ : YoungDiagram)
    (hc : τ.card = θ.card) (hd : Dominates τ θ) :
    ∃ (a : Fin τ.card → Fin (θ.colLen 0)) (l : Module.Dual ℂ (Specht (shapeTableau τ))),
      l ≠ 0 ∧
      (∀ j, (Finset.univ.filter (fun i => a i = j)).card = θ.rowLen j) ∧
      (∀ g : Equiv.Perm (Fin τ.card), a ∘ g = a →
        ∀ x, l (spechtRep (shapeTableau τ) g x) = l x) := by
…

Mentions: OAI.Saxl.Dominates, OAI.Saxl.Specht, OAI.Saxl.shapeTableau, OAI.Saxl.spechtRep