CanonicalKL.lean`

30 declarations, 0 contain sorry, 0 declared as axioms

Canonical low-part construction, strict halfdegree, reciprocity and uniqueness; certification of the selected polynomials and interval ranks.

def OAI.KLInvariance.CanonicalP.lowPart line 23
Source documentation
The strict lower half of a polynomial, used in the KL recursion.
```
noncomputable def lowPart (d : ℕ) (p : ℤ[X]) : ℤ[X] :=
…
```
theorem OAI.KLInvariance.CanonicalP.coeff_lowPart line 26
theorem OAI.KLInvariance.CanonicalP.lowPart_degree line 34
theorem OAI.KLInvariance.CanonicalP.lowPart_solution line 43
Source documentation
Solve the anti-reciprocal defect with the required strict degree bound.
```
theorem lowPart_solution (d : ℕ) (p : ℤ[X]) (hanti : reflect d p = -p) :
    reflect d (-lowPart d p) = -lowPart d p + p := by
…
```
Mentions: OAI.KLInvariance.CanonicalP.lowPart
def OAI.KLInvariance.CanonicalP.polynomial line 70
Source documentation
The standard lower-half KL recursion, on the actual Bruhat interval. Its reciprocity will be proved from the genuine R-kernel, not stipulated.
```
noncomputable def polynomial (cs : CoxeterSystem M W) (x y : W) : ℤ[X] := by
…
```
theorem OAI.KLInvariance.CanonicalP.polynomial_diagonal line 86
theorem OAI.KLInvariance.CanonicalP.polynomial_zero line 91
def OAI.KLInvariance.CanonicalP.defect line 95
theorem OAI.KLInvariance.CanonicalP.polynomial_recursion line 98
theorem OAI.KLInvariance.CanonicalP.polynomial_strict_degree line 104
theorem OAI.KLInvariance.CanonicalP.polynomial_degree line 113
theorem OAI.KLInvariance.CanonicalP.defect_full_sum line 124
theorem OAI.KLInvariance.CanonicalP.reversed_kernel_on_lower line 133
theorem OAI.KLInvariance.CanonicalP.reversed_kernel_on_proper line 149
theorem OAI.KLInvariance.CanonicalP.polynomial_reciprocity line 162
Source documentation
The reciprocity equation is a theorem of the lower-half construction.
```
theorem polynomial_reciprocity (cs : CoxeterSystem M W) (x y : W)
    (hxy : BruhatLE cs x y) :
    reflect (rankDifference cs x y) (polynomial cs x y) =
      ∑ z ∈ lowerFinset cs y, OrdinaryR.polynomial cs x z * polynomial cs z y := by
…
```
Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.rankDifference, OAI.KLInvariance.CanonicalP.polynomial, OAI.KLInvariance.lowerFinset, OAI.KLInvariance.OrdinaryR.polynomial
theorem OAI.KLInvariance.normalized_interval_sum line 239
Source documentation
Finitely supported interval sums agree with the lower-ideal sums used in our construction; all incomparable summands are literally zero.
```
theorem normalized_interval_sum (cs : CoxeterSystem M W) (x y : W) :
    (∑ᶠ z : Interval cs x y,
      OrdinaryR.polynomial cs x z.val * CanonicalP.polynomial cs z.val y) =
    ∑ z ∈ lowerFinset cs y,
      OrdinaryR.polynomial cs x z * CanonicalP.polynomial cs z y := by
…
```
Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.OrdinaryR.polynomial, OAI.KLInvariance.CanonicalP.polynomial, OAI.KLInvariance.lowerFinset
theorem OAI.KLInvariance.constructed_normalizedKL line 260
Source documentation
The selected polynomials really exist with the classical equal-parameter normalization. This is a construction, not an extra hypothesis.
```
theorem constructed_normalizedKL (cs : CoxeterSystem M W) :
    NormalizedKL cs (OrdinaryR.polynomial cs, CanonicalP.polynomial cs) where
…
```
Mentions: OAI.KLInvariance.NormalizedKL, OAI.KLInvariance.OrdinaryR.polynomial, OAI.KLInvariance.CanonicalP.polynomial
theorem OAI.KLInvariance.normalizedKL_existsUnique line 273
theorem OAI.KLInvariance.klFamilies_spec line 279
theorem OAI.KLInvariance.klFamilies_eq_constructed line 282
theorem OAI.KLInvariance.klPolynomial_eq_constructed line 286
theorem OAI.KLInvariance.rPolynomial_eq_constructed line 290
theorem OAI.KLInvariance.exists_bruhat_successor line 297
Source documentation
Every nontrivial Bruhat interval contains a first step of length one. This is the grading fact needed to transport rank differences without labels.
```
theorem exists_bruhat_successor (cs : CoxeterSystem M W) {x y : W}
    (hxy : BruhatLE cs x y) (hne : x ≠ y) :
    ∃ z, BruhatLE cs x z ∧ BruhatLE cs z y ∧ cs.length z = cs.length x + 1 := by
…
```
Mentions: OAI.KLInvariance.BruhatLE

theorem OAI.KLInvariance.rankDifference_le_of_strictMono line 367

Source documentation

An order embedding between Bruhat intervals cannot shorten rank.

theorem rankDifference_le_of_strictMono
    {B' : Type u'} {W' : Type v'} [Group W'] {M' : CoxeterMatrix B'}
    (cs : CoxeterSystem M W) (cs' : CoxeterSystem M' W')
    {u b : W} {u' b' : W'}
    (f : Interval cs u b → Interval cs' u' b') (hf : StrictMono f)
    {x y : Interval cs u b} (hxy : x ≤ y) :
    rankDifference cs x.val y.val ≤ rankDifference cs' (f x).val (f y).val := by
…

Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.rankDifference

theorem OAI.KLInvariance.intervalIso_rankDifference line 415

Source documentation

Rank is intrinsic to the abstract interval poset, with neither root labels nor simple generators preserved by the isomorphism.

theorem intervalIso_rankDifference
    {B' : Type u'} {W' : Type v'} [Group W'] {M' : CoxeterMatrix B'}
    (cs : CoxeterSystem M W) (cs' : CoxeterSystem M' W')
    {u b : W} {u' b' : W'}
    (ι : Interval cs u b ≃o Interval cs' u' b')
    {x y : Interval cs u b} (hxy : x ≤ y) :
    rankDifference cs x.val y.val = rankDifference cs' (ι x).val (ι y).val := by
…

Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.rankDifference

def OAI.KLInvariance.intervalBottom line 428
Source documentation
Named endpoints for an actual nonempty interval.
```
def intervalBottom (cs : CoxeterSystem M W) {u b : W} (hub : BruhatLE cs u b) :
    Interval cs u b := ⟨u, bruhat_refl cs u, hub⟩
```
Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.Interval, OAI.KLInvariance.bruhat_refl
def OAI.KLInvariance.intervalTop line 431
theorem OAI.KLInvariance.intervalIso_bottom line 434
theorem OAI.KLInvariance.intervalIso_top line 446
theorem OAI.KLInvariance.intervalIso_full_rankDifference line 458