Bruhat.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Strong Bruhat order, subwords, length, finite lower ideals and arbitrary finite intervals; the selected R family.

theorem OAI.KLInvariance.bruhat_refl line 19
theorem OAI.KLInvariance.bruhat_trans line 22
theorem OAI.KLInvariance.length_le_of_bruhat line 26
theorem OAI.KLInvariance.length_lt_of_bruhat_ne line 32
theorem OAI.KLInvariance.bruhat_antisymm line 38
def OAI.KLInvariance.rPolynomial line 54
theorem OAI.KLInvariance.finite_bruhat_predecessors line 73
Source documentation
A vertex has only finitely many incoming strong Bruhat edges, using strong exchange proved from the Coxeter presentation above.
```
theorem finite_bruhat_predecessors (cs : CoxeterSystem M W) (b : W) :
    {x : W | BruhatStep cs x b}.Finite := by
…
```
Mentions: OAI.KLInvariance.BruhatStep
theorem OAI.KLInvariance.finite_bruhat_lower line 86
Source documentation
Finiteness of all lower Bruhat ideals, with no finite-rank assumption.
```
theorem finite_bruhat_lower (cs : CoxeterSystem M W) (b : W) :
    {x : W | BruhatLE cs x b}.Finite := by
…
```
Mentions: OAI.KLInvariance.BruhatLE
theorem OAI.KLInvariance.interval_finite line 106
Source documentation
The finite-interval obligation in the faithful trusted main target.
```
theorem interval_finite (cs : CoxeterSystem M W) (u b : W) :
    Finite (Interval cs u b) :=
…
```
Mentions: OAI.KLInvariance.Interval
theorem OAI.KLInvariance.normalized_R_unique line 111
Source documentation
The exact R recursion determines at most one R family.
```
theorem normalized_R_unique (cs : CoxeterSystem M W)
    {RP SQ : PolynomialFamilies W} (hRP : NormalizedKL cs RP) (hSQ : NormalizedKL cs SQ) :
    RP.1 = SQ.1 := by
…
```
Mentions: OAI.KLInvariance.PolynomialFamilies, OAI.KLInvariance.NormalizedKL
theorem OAI.KLInvariance.low_degree_reflect_eq_self line 141
Source documentation
The degree/reciprocity rigidity used both by normalization uniqueness and by the final main-theorem induction: no polynomial supported strictly below the midpoint can be self-reciprocal about that midpoint.
```
theorem low_degree_reflect_eq_self (f : ℤ[X]) (d : ℕ)
    (hd : 2 * f.natDegree < d) (hself : reflect d f = f) : f = 0 := by
…
```
theorem OAI.KLInvariance.normalized_P_unique line 151
Source documentation
The polynomial part of the manuscript's normalization is unique; the proof uses the actual finite strong-Bruhat intervals, not extra assumptions.
```
theorem normalized_P_unique (cs : CoxeterSystem M W)
    {RP SQ : PolynomialFamilies W} (hRP : NormalizedKL cs RP) (hSQ : NormalizedKL cs SQ) :
    RP.2 = SQ.2 := by
…
```
Mentions: OAI.KLInvariance.PolynomialFamilies, OAI.KLInvariance.NormalizedKL
theorem OAI.KLInvariance.normalizedKL_unique line 204
Source documentation
Unique existence is still a separate obligation: this proves its uniqueness half only, without postulating a normalized family.
```
theorem normalizedKL_unique (cs : CoxeterSystem M W)
    {RP SQ : PolynomialFamilies W} (hRP : NormalizedKL cs RP) (hSQ : NormalizedKL cs SQ) :
    RP = SQ :=
…
```
Mentions: OAI.KLInvariance.PolynomialFamilies, OAI.KLInvariance.NormalizedKL

theorem OAI.KLInvariance.exists_reduced_subword line 214

Source documentation

Every word contains a reduced subword with the same product.

theorem exists_reduced_subword (cs : CoxeterSystem M W) (ω : List B) :
    ∃ ν : List B, ν.Sublist ω ∧ cs.IsReduced ν ∧ cs.wordProd ν = cs.wordProd ω := by
…

theorem OAI.KLInvariance.subword_of_bruhat_step line 234

Source documentation

A single downward reflection step can be realized inside any reduced word.

theorem subword_of_bruhat_step (cs : CoxeterSystem M W) {x y : W}
    (hxy : BruhatStep cs x y) {ω : List B} (hω : cs.IsReduced ω)
    (hy : cs.wordProd ω = y) :
    ∃ ν : List B, ν.Sublist ω ∧ cs.IsReduced ν ∧ cs.wordProd ν = x := by
…

Mentions: OAI.KLInvariance.BruhatStep

theorem OAI.KLInvariance.reduced_subword_of_bruhat line 248

Source documentation

Forward subword property, for every chosen reduced expression of the top.

theorem reduced_subword_of_bruhat (cs : CoxeterSystem M W) {x y : W}
    (hxy : BruhatLE cs x y) {ω : List B} (hω : cs.IsReduced ω)
    (hy : cs.wordProd ω = y) :
    ∃ ν : List B, ν.Sublist ω ∧ cs.IsReduced ν ∧ cs.wordProd ν = x := by
…

Mentions: OAI.KLInvariance.BruhatLE

theorem OAI.KLInvariance.bruhatStep_simple_mul line 262
Source documentation
Simple left multiplication preserves the orientation of every reflection edge except the edge carrying that simple reflection itself.
```
theorem bruhatStep_simple_mul (cs : CoxeterSystem M W) {x y : W}
    (hxy : BruhatStep cs x y) (i : B) (hne : y ≠ cs.simple i * x) :
    BruhatStep cs (cs.simple i * x) (cs.simple i * y) := by
…
```
Mentions: OAI.KLInvariance.BruhatStep
def OAI.KLInvariance.lowerSimple line 299
Source documentation
The smaller of x and s*x in Bruhat order.
```
noncomputable def lowerSimple (cs : CoxeterSystem M W) (i : B) (x : W) : W :=
…
```
def OAI.KLInvariance.upperSimple line 303
Source documentation
The larger of x and s*x in Bruhat order.
```
noncomputable def upperSimple (cs : CoxeterSystem M W) (i : B) (x : W) : W :=
…
```
theorem OAI.KLInvariance.lowerSimple_le line 306
theorem OAI.KLInvariance.le_upperSimple line 314
theorem OAI.KLInvariance.lowerSimple_mul line 323
theorem OAI.KLInvariance.upperSimple_mul line 331
theorem OAI.KLInvariance.lowerSimple_step_mono line 339
theorem OAI.KLInvariance.upperSimple_step_mono line 363
theorem OAI.KLInvariance.lowerSimple_mono line 387
theorem OAI.KLInvariance.upperSimple_mono line 394

theorem OAI.KLInvariance.bruhat_lifting line 403

Source documentation

The standard lifting property, now for the actual strong order.

theorem bruhat_lifting (cs : CoxeterSystem M W) {x y : W}
    (hxy : BruhatLE cs x y) (i : B)
    (hx : cs.length x < cs.length (cs.simple i * x))
    (hy : cs.length (cs.simple i * y) < cs.length y) :
    BruhatLE cs x (cs.simple i * y) ∧ BruhatLE cs (cs.simple i * x) y := by
…

Mentions: OAI.KLInvariance.BruhatLE

theorem OAI.KLInvariance.bruhat_of_subword line 414

Source documentation

Converse subword property; no labels are added to Bruhat intervals.

theorem bruhat_of_subword (cs : CoxeterSystem M W) {ν ω : List B}
    (hsub : ν.Sublist ω) (hω : cs.IsReduced ω) :
    BruhatLE cs (cs.wordProd ν) (cs.wordProd ω) := by
…

Mentions: OAI.KLInvariance.BruhatLE

theorem OAI.KLInvariance.bruhat_iff_reduced_subword line 439

Source documentation

The subword criterion with an arbitrary fixed reduced word for the top.

theorem bruhat_iff_reduced_subword (cs : CoxeterSystem M W) {x : W} {ω : List B}
    (hω : cs.IsReduced ω) :
    BruhatLE cs x (cs.wordProd ω) ↔
      ∃ ν : List B, ν.Sublist ω ∧ cs.IsReduced ν ∧ cs.wordProd ν = x := by
…

Mentions: OAI.KLInvariance.BruhatLE

theorem OAI.KLInvariance.lower_ideal_finite_generator_support line 452
Source documentation
Precisely the finite-support part used by the manuscript's finite-rank reduction: all lower elements are words in the generators of any reduced top word. Equality of parabolic polynomial normalizations remains a later step.
```
theorem lower_ideal_finite_generator_support (cs : CoxeterSystem M W) (b : W) :
    ∃ J : Set B, J.Finite ∧ ∀ x, BruhatLE cs x b →
      ∃ ν : List B, (∀ i ∈ ν, i ∈ J) ∧ cs.wordProd ν = x := by
…
```
Mentions: OAI.KLInvariance.BruhatLE
theorem OAI.KLInvariance.bruhatStep_inv line 463
Source documentation
Inversion preserves the actual strong Bruhat graph.
```
theorem bruhatStep_inv (cs : CoxeterSystem M W) {x y : W}
    (hxy : BruhatStep cs x y) : BruhatStep cs x⁻¹ y⁻¹ := by
…
```
Mentions: OAI.KLInvariance.BruhatStep
theorem OAI.KLInvariance.bruhatStep_mul_simple line 470

theorem OAI.KLInvariance.left_descent_mul_simple_iff line 483

Source documentation

The noncollapsed left/right simple square has consistent orientations.

theorem left_descent_mul_simple_iff (cs : CoxeterSystem M W) (i j : B) (x : W)
    (hne : cs.simple i * x ≠ x * cs.simple j) :
    cs.length (cs.simple i * (x * cs.simple j)) < cs.length (x * cs.simple j) ↔
      cs.length (cs.simple i * x) < cs.length x := by
…

theorem OAI.KLInvariance.right_descent_simple_mul_iff line 504