Dihedral.lean`

44 declarations, 0 contain sorry, 0 declared as axioms

Interval restrictions, dihedral Coxeter and Hecke calculations, and the genuine square-parameter R normalization.

def OAI.KLInvariance.intervalIso_restrict line 19

Source documentation

Restriction of the actual interval isomorphism to any subinterval. This is the same unlabeled map, not a new isomorphism with extra structure.

def intervalIso_restrict (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) :
    Interval cs x.val y.val ≃o Interval cs' (ι x).val (ι y).val where
…

Mentions: OAI.KLInvariance.Interval

theorem OAI.KLInvariance.intervalIso_restrict_val line 58
def OAI.KLInvariance.Dihedral.alt line 74
Source documentation
The alternating expression starting with i, unlike Mathlib's alternatingWord, which specifies the final letter.
```
def alt (i : Bool) : ℕ → List Bool
  | 0 => []
  | n + 1 => i :: alt (!i) n
```
theorem OAI.KLInvariance.Dihedral.alt_zero line 78
theorem OAI.KLInvariance.Dihedral.alt_succ line 79
theorem OAI.KLInvariance.Dihedral.length_alt line 80
theorem OAI.KLInvariance.Dihedral.take_alt line 85
theorem OAI.KLInvariance.Dihedral.reduced_cons_cons_ne line 93
theorem OAI.KLInvariance.Dihedral.reduced_cons_eq_alt line 101
theorem OAI.KLInvariance.Dihedral.reduced_eq_alt line 114
theorem OAI.KLInvariance.Dihedral.exists_alt line 120
theorem OAI.KLInvariance.Dihedral.reduced_alt_take line 127
theorem OAI.KLInvariance.Dihedral.alt_sublist line 131
theorem OAI.KLInvariance.Dihedral.shorter_bruhat line 144
Source documentation
In a rank-two Coxeter system, every strictly shorter element lies below every longer element. This uses the actual Bruhat subword theorem.
```
theorem shorter_bruhat (cs : CoxeterSystem M W) {x w : W}
    (h : cs.length x < cs.length w) : BruhatLE cs x w := by
…
```
Mentions: OAI.KLInvariance.BruhatLE
theorem OAI.KLInvariance.Dihedral.bruhat_iff_length_lt_or_eq line 162
theorem OAI.KLInvariance.Dihedral.eq_alt_of_descent line 173
def OAI.KLInvariance.Dihedral.lowerSum line 197
theorem OAI.KLInvariance.Dihedral.lowerSum_coeff line 200
theorem OAI.KLInvariance.Dihedral.lowerSum_one line 205

theorem OAI.KLInvariance.Dihedral.double_string line 217

Source documentation

The two members of an s-string enter a lower ideal together precisely on the common lower interval appearing in the source's rank-two product.

theorem double_string (cs : CoxeterSystem M W) (i : Bool) (n : ℕ)
    (hr : cs.IsReduced (alt i (n+2))) (x : W) :
    (BruhatLE cs x (cs.wordProd (alt (!i) (n+1))) ∧
      BruhatLE cs (cs.simple i * x) (cs.wordProd (alt (!i) (n+1)))) ↔
    (0 < n ∧ BruhatLE cs x (cs.wordProd (alt i n))) := by
…

Mentions: OAI.KLInvariance.Dihedral.alt, OAI.KLInvariance.BruhatLE

theorem OAI.KLInvariance.Dihedral.left_plus_coeff line 287
theorem OAI.KLInvariance.Dihedral.union_string line 303
def OAI.KLInvariance.Dihedral.correction line 322
theorem OAI.KLInvariance.Dihedral.correction_coeff line 325
theorem OAI.KLInvariance.Dihedral.lowerSum_product line 336
Source documentation
The Hecke sum identity loc:dihedral-product, before normalization by q to a half-integer power. Every interval here is genuine strong Bruhat.
```
theorem lowerSum_product (cs : CoxeterSystem M W) (q : Cˣ) (i : Bool) (n : ℕ)
    (hr : cs.IsReduced (alt i (n+2))) :
    lowerSum cs (cs.wordProd (alt (!i) (n+1))) +
      HeckeQ.left cs (q : C) i (lowerSum cs (cs.wordProd (alt (!i) (n+1)))) =
    lowerSum cs (cs.wordProd (alt i (n+2))) + (q : C) • correction cs i n := by
…
```
Mentions: OAI.KLInvariance.Dihedral.alt, OAI.KLInvariance.Dihedral.lowerSum, OAI.KLInvariance.HeckeQ.left, OAI.KLInvariance.Dihedral.correction
def OAI.KLInvariance.HeckeQ.dualR line 387
theorem OAI.KLInvariance.HeckeQ.dualR_diagonal line 390
theorem OAI.KLInvariance.HeckeQ.dualR_zero line 395
theorem OAI.KLInvariance.HeckeQ.dualR_recursion line 399
theorem OAI.KLInvariance.HeckeQ.rValue_eq_dualR line 440
Source documentation
Signed inversion symmetry of actual equal-parameter R-values, proved from all-descent recurrence, not imposed as an additional normalization.
```
theorem rValue_eq_dualR (cs : CoxeterSystem M W) (q : Cˣ) (x y : W) :
    rValue cs q x y = dualR cs q x y := by
…
```
Mentions: OAI.KLInvariance.HeckeQ.rValue, OAI.KLInvariance.HeckeQ.dualR
theorem OAI.KLInvariance.HeckeQ.rValue_inverse_eq_barBasis line 467
Source documentation
R at the inverse parameter is exactly the corresponding bar coefficient with the bottom q-power. This is the coefficient form used below.
```
theorem rValue_inverse_eq_barBasis (cs : CoxeterSystem M W) (q : Cˣ) (x y : W) :
    rValue cs q⁻¹ x y = (q:C) ^ cs.length x * barBasis cs q y x := by
…
```
Mentions: OAI.KLInvariance.HeckeQ.rValue, OAI.KLInvariance.HeckeQ.barBasis
theorem OAI.KLInvariance.Dihedral.lowerSum_simple line 490
theorem OAI.KLInvariance.Dihedral.plus_leftInv line 509

theorem OAI.KLInvariance.Dihedral.bar_lowerSum_alt line 517

Source documentation

Unnormalized form of bar invariance of the dihedral constant sums.

theorem bar_lowerSum_alt (cs : CoxeterSystem M W) (q : Cˣ) (i : Bool) (n : ℕ)
    (hr : cs.IsReduced (alt i n)) :
    HeckeQ.barLinear cs q (lowerSum cs (cs.wordProd (alt i n))) =
      (↑q⁻¹:C)^n • lowerSum cs (cs.wordProd (alt i n)) := by
…

Mentions: OAI.KLInvariance.Dihedral.alt, OAI.KLInvariance.HeckeQ.barLinear, OAI.KLInvariance.Dihedral.lowerSum

theorem OAI.KLInvariance.Dihedral.bar_lowerSum line 557
theorem OAI.KLInvariance.Dihedral.rValue_sum line 576
theorem OAI.KLInvariance.Dihedral.rPolynomial_sum line 605
def OAI.KLInvariance.Dihedral.constantP line 612
theorem OAI.KLInvariance.Dihedral.constant_normalizedKL line 615
theorem OAI.KLInvariance.Dihedral.klPolynomial_eq_one line 656
Source documentation
The manuscript's necessary dihedral calculation (loc:dihedral-kl), for the actual KL family, with the exact standard normalization. This is support for localization, not a substitute for general invariance.
```
theorem klPolynomial_eq_one (cs : CoxeterSystem M W) (x y : W)
    (hxy : BruhatLE cs x y) : klPolynomial cs x y = 1 := by
…
```
Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.klPolynomial
theorem OAI.KLInvariance.rPolynomial_normalization line 676
Source documentation
The exact square-parameter normalization, proved from the two genuine Hecke recurrences. Integer exponents let the formula include incomparable pairs without silently changing the R-polynomial definition.
```
theorem rPolynomial_normalization {C : Type*} [Field C]
    (cs : CoxeterSystem M W) (v : C) (hv : v ≠ 0) (x y : W) :
    eval₂ (Int.castRingHom C) (v^2) (rPolynomial cs x y) =
      v ^ ((cs.length y : ℤ) - cs.length x) *
        eval₂ (Int.castRingHom C) (v-v⁻¹) (Hecke.rTilde cs x y) := by
…
```
Mentions: OAI.KLInvariance.rPolynomial, OAI.KLInvariance.Hecke.rTilde
def OAI.KLInvariance.scaledKL line 730
Source documentation
The manuscript's q^{-d/2} P(q), written with t^2=q so no square-root branch is hidden. This is an evaluation of the already constructed genuine KL polynomial, not a new combinatorial invariant.
```
noncomputable def scaledKL {C : Type*} [Field C]
    (cs : CoxeterSystem M W) (t : C) (x b : W) : C :=
…
```
theorem OAI.KLInvariance.scaledKL_reciprocity_inverse line 737
Source documentation
Exact normalized reciprocity in the direction useful for reversing the parameter. No path formula and no moment-graph assumption occurs here.
```
theorem scaledKL_reciprocity_inverse {C : Type*} [Field C]
    (cs : CoxeterSystem M W) (v : C) (hv : v ≠ 0)
    (x b : W) (hxb : BruhatLE cs x b) :
    scaledKL cs v⁻¹ x b = ∑ᶠ z : Interval cs x b,
      eval₂ (Int.castRingHom C) (v-v⁻¹) (Hecke.rTilde cs x z.val) *
        scaledKL cs v z.val b := by
…
```
Mentions: OAI.KLInvariance.BruhatLE, OAI.KLInvariance.scaledKL, OAI.KLInvariance.Interval, OAI.KLInvariance.Hecke.rTilde
theorem OAI.KLInvariance.scaledKL_reciprocity line 790