OAI/RepresentationTheory/KazhdanLusztig/DyerPaths.lean

GitHub source file

165 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.KLInvariance.finite_character_cancellation line 15
2. theorem OAI.KLInvariance.BruhatGraph.stalkCharacter_reciprocity line 62
3. theorem OAI.KLInvariance.StandardParabolic.leftInvSeq_inclusion line 119
4. theorem OAI.KLInvariance.StandardParabolic.reflection_inclusion line 134
5. theorem OAI.KLInvariance.StandardParabolic.bruhatStep_inclusion_iff line 140
6. theorem OAI.KLInvariance.diamondEdges_of_bruhatStep_general line 175

   Source documentation

   The graph reconstruction input in its source scope: the Coxeter system can have infinitely many generators. The interval determines every reflection edge without being supplied the reflection labels.

   theorem diamondEdges_of_bruhatStep_general (cs : CoxeterSystem M W)
       {u b : W} {x y : Interval cs u b} (hxy : BruhatStep cs x.val y.val) :
       DiamondEdges x y := by
   …

   Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.DiamondEdges

7. theorem OAI.KLInvariance.diamondEdges_bruhatStep_general line 204
8. theorem OAI.KLInvariance.intervalIso_bruhatStep_iff_general line 234

   Source documentation

   Exact unlabelled directed graph invariance, also for arbitrary infinite Coxeter systems. This is not yet KL polynomial invariance.

   theorem intervalIso_bruhatStep_iff_general
       {I' : Type u'} {W' : Type v'} [Group W'] {M' : CoxeterMatrix I'}
       (cs : CoxeterSystem M W) (cs' : CoxeterSystem M' W')
       {u b : W} {u' b' : W'} (e : Interval cs u b ≃o Interval cs' u' b')
       (x y : Interval cs u b) :
       BruhatStep cs' (e x).val (e y).val ↔ BruhatStep cs x.val y.val := by
   …

   Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep

9. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.graphRoot_mem line 265
10. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.graphRoot_path_plane line 274

    Source documentation

    The two labels on a composable coset path span the whole actual plane.

    theorem graphRoot_path_plane {a₀ : W} {g h k : planeSubgroup M cs P}
        (he : BruhatStep cs ((g : W) * a₀) ((h : W) * a₀))
        (hf : BruhatStep cs ((h : W) * a₀) ((k : W) * a₀)) :
        rootPlane (graphRoot he) (graphRoot hf) = P := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.rootPlane, OAI.KLInvariance.TitsSpace.graphRoot

11. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.twoStep_mem_coset line 283
12. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.ambient_two_step_rank_two line 302

    Source documentation

    A relative rank-two interval has exactly its two ambient two-edge paths, with no assumption that the two ambient and relative orders coincide.

    theorem ambient_two_step_rank_two {a₀ : W}
        (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z * a₀))
        {g k : planeSubgroup M cs P} (hlen : B.system.length k = B.system.length g + 2) :
        ∃ a b : W, a ≠ b ∧ ∀ z : W,
          (BruhatStep cs ((g : W) * a₀) z ∧ BruhatStep cs z ((k : W) * a₀)) ↔
            z = a ∨ z = b := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep

13. theorem OAI.KLInvariance.Dihedral.rank_two_of_two_step_bound line 341

    Source documentation

    Exactly two intermediate vertices characterize relative rank two as soon as one two-edge path exists. Used to rule out skipped ranks after transport.

    theorem rank_two_of_two_step_bound (ds : CoxeterSystem N G) {x y a b : G}
        (ha : BruhatStep ds x a) (hay : BruhatStep ds a y)
        (hbound : ∀ z, BruhatStep ds x z → BruhatStep ds z y → z = a ∨ z = b) :
        ds.length y = ds.length x + 2 := by
    …

    Mentions: OAI.KLInvariance.BruhatStep

14. theorem OAI.KLInvariance.TitsSpace.graphRoot_mem_of_coset line 381
15. theorem OAI.KLInvariance.TitsSpace.mem_coset_of_graphRoot line 388
16. theorem OAI.KLInvariance.TitsSpace.dihedral_image_in_plane line 400

    Source documentation

    The image of a full relative dihedral interval lies in one maximal plane coset. This is derived just from the directed graph and distinct vertices.

    theorem dihedral_image_in_plane
        (f : Interval ds l r → W) (hinj : Function.Injective f)
        (hgraph : ∀ a b : Interval ds l r,
          BruhatStep ds a.val b.val → BruhatStep cs (f a) (f b))
        (hlr : BruhatLE ds l r) (hrank : ds.length l + 2 ≤ ds.length r) :
        ∃ a b : PositiveRoot M cs, a ≠ b ∧
          ∀ z : Interval ds l r,
            f z * (f ⟨l,bruhat_refl ds l,hlr⟩)⁻¹ ∈ planeSubgroup M cs (rootPlane a b) := by
    …

    Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.bruhat_refl, OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.rootPlane

17. theorem OAI.KLInvariance.Dihedral.exists_interval_length line 488
18. theorem OAI.KLInvariance.Dihedral.map_cover_length line 504
19. theorem OAI.KLInvariance.Dihedral.map_length_affine line 536

    Source documentation

    A directed dihedral-interval graph injection which does not stretch any rank-two interval preserves all relative ranks.

    theorem map_length_affine
        (f : Interval ds l r → D')
        (hgraph : ∀ x y : Interval ds l r, BruhatStep ds x.val y.val →
          BruhatStep ds' (f x) (f y))
        (htwo : ∀ x y : Interval ds l r, ds.length y.val = ds.length x.val+2 →
          ds'.length (f y) = ds'.length (f x)+2)
        (hlr : BruhatLE ds l r) (hrank : ds.length l+2 ≤ ds.length r)
        (z : Interval ds l r) :
        ds'.length (f z) + ds.length l =
          ds'.length (f ⟨l,bruhat_refl ds l,hlr⟩) + ds.length z.val := by
    …

    Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.bruhat_refl

20. theorem OAI.KLInvariance.Dihedral.range_eq_interval_of_rank_two line 567

    Source documentation

    Once relative covers are recovered, the image exhausts rather than merely embeds in the target dihedral interval.

    theorem range_eq_interval_of_rank_two
        (f : Interval ds l r → D') (hinj : Function.Injective f)
        (hgraph : ∀ x y : Interval ds l r, BruhatStep ds x.val y.val →
          BruhatStep ds' (f x) (f y))
        (htwo : ∀ x y : Interval ds l r, ds.length y.val = ds.length x.val+2 →
          ds'.length (f y) = ds'.length (f x)+2)
        (hlr : BruhatLE ds l r) (hrank : ds.length l+2 ≤ ds.length r) :
        Set.range f = {z | BruhatLE ds' (f ⟨l,bruhat_refl ds l,hlr⟩) z ∧
          BruhatLE ds' z (f ⟨r,hlr,bruhat_refl ds r⟩)} := by
    …

    Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.bruhat_refl

21. theorem OAI.KLInvariance.intervalIso_twoStep_iff line 634

    Source documentation

    An interval graph isomorphism preserves the exact two-edge intermediate set, including ambient intermediates not specified as interval data.

    theorem intervalIso_twoStep_iff
        (e : Interval cs u b ≃o Interval cs' u' b') (x y a c : Interval cs u b)
        (hpaths : ∀ z : W, (BruhatStep cs x.val z ∧ BruhatStep cs z y.val) ↔
          z=a.val ∨ z=c.val) (z : W') :
        (BruhatStep cs' (e x).val z ∧ BruhatStep cs' z (e y).val) ↔
          z=(e a).val ∨ z=(e c).val := by
    …

    Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep

22. def OAI.KLInvariance.TitsSpace.PlaneBasis.cosetIntervalMap line 676
23. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.twoStep_interval_iff line 687
24. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.transport_interval line 736
25. theorem OAI.KLInvariance.TitsSpace.inverted_of_positive_combination line 844
26. theorem OAI.KLInvariance.TitsSpace.graphRoot_inverted_target line 855

    Source documentation

    Incoming graph labels are actual inversions at their upper vertex.

    theorem graphRoot_inverted_target {x y : W} (h : BruhatStep cs x y) :
        rootInverted y (graphRoot h) := by
    …

    Mentions: OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.graphRoot

27. theorem OAI.KLInvariance.TitsSpace.graphRoot_not_inverted_source line 866

    Source documentation

    Outgoing graph labels are actual noninversions at their lower vertex.

    theorem graphRoot_not_inverted_source {x y : W} (h : BruhatStep cs x y) :
        ¬ rootInverted x (graphRoot h) := by
    …

    Mentions: OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.graphRoot

28. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.slope_lt_of_inverted_left line 881

    Source documentation

    In a plane with its first simple root inverted, every noninverted root is later than every inverted root. This uses convexity, not a signed-index formula for a particular realization.

    theorem slope_lt_of_inverted_left (w : W) (hl : rootInverted w B.left)
        (a b : PositiveRoot M cs) (haP : a.val ∈ P) (hbP : b.val ∈ P)
        (ha : rootInverted w a) (hb : ¬ rootInverted w b) :
        geometricSlope a < geometricSlope b := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.geometricSlope

29. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.slope_lt_of_inverted_right line 899

    Source documentation

    The other angular cut, when the last simple root is inverted.

    theorem slope_lt_of_inverted_right (w : W) (hr : rootInverted w B.right)
        (a b : PositiveRoot M cs) (haP : a.val ∈ P) (hbP : b.val ∈ P)
        (ha : rootInverted w a) (hb : ¬ rootInverted w b) :
        geometricSlope b < geometricSlope a := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.geometricSlope

30. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.slope_lt_iff_inverted_left line 923

    Source documentation

    In the mixed-sign case the angular cut is determined by the first canonical simple root. In particular the comparison of consecutive path labels depends only on their middle vertex.

    theorem slope_lt_iff_inverted_left (w : W)
        (a b : PositiveRoot M cs) (haP : a.val ∈ P) (hbP : b.val ∈ P)
        (ha : rootInverted w a) (hb : ¬ rootInverted w b) :
        geometricSlope a < geometricSlope b ↔ rootInverted w B.left := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.rootInverted, OAI.KLInvariance.TitsSpace.geometricSlope

31. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.consecutive_slopes_iff line 940

    Source documentation

    The exact middle-vertex test for two ascending graph arrows with both labels in this root plane.

    theorem consecutive_slopes_iff {x y z : W}
        (hxy : BruhatStep cs x y) (hyz : BruhatStep cs y z)
        (ha : (graphRoot hxy).val ∈ P) (hb : (graphRoot hyz).val ∈ P) :
        geometricSlope (graphRoot hxy) < geometricSlope (graphRoot hyz) ↔
          rootInverted y B.left :=
    …

    Mentions: OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.graphRoot, OAI.KLInvariance.TitsSpace.geometricSlope, OAI.KLInvariance.TitsSpace.rootInverted

32. def OAI.KLInvariance.Dihedral.swapHom line 958

    Source documentation

    The genuine diagram automorphism of an arbitrary rank-two Coxeter system, including the infinite one.

    def swapHom (cs : CoxeterSystem M W) : W →* W :=
    …

33. theorem OAI.KLInvariance.Dihedral.swapHom_simple line 970
34. theorem OAI.KLInvariance.Dihedral.swapHom_involutive line 973
35. def OAI.KLInvariance.Dihedral.swap line 983
36. theorem OAI.KLInvariance.Dihedral.swap_simple line 990
37. theorem OAI.KLInvariance.Dihedral.swap_swap line 993
38. theorem OAI.KLInvariance.Dihedral.swap_wordProd line 996
39. theorem OAI.KLInvariance.Dihedral.length_swap line 1003
40. theorem OAI.KLInvariance.Dihedral.descent_swap line 1011
41. theorem OAI.KLInvariance.Dihedral.unique_leftDescent line 1019

    Source documentation

    A nonzero length below an existing greater length has exactly one left simple descent. This is not asserted for a finite dihedral longest element.

    theorem unique_leftDescent (cs : CoxeterSystem M W) {w z : W}
        (hw : 0 < cs.length w) (hz : cs.length w < cs.length z) :
        ∃! i : Bool, cs.IsLeftDescent w i := by
    …

42. theorem OAI.KLInvariance.Dihedral.descent_swap_false_iff_not line 1048

    Source documentation

    Internally, the diagram involution interchanges the two unique-descent vertices of each rank.

    theorem descent_swap_false_iff_not (cs : CoxeterSystem M W) {w z : W}
        (hw : 0 < cs.length w) (hz : cs.length w < cs.length z) :
        cs.IsLeftDescent (swap cs w) false ↔ ¬ cs.IsLeftDescent w false := by
    …

    Mentions: OAI.KLInvariance.Dihedral.swap

43. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.simpleRoot_inverted_coset_iff line 1079

    Source documentation

    The ambient sign of a canonical plane root in a minimal coset is the intrinsic simple-descent sign, with the original left labels.

    theorem simpleRoot_inverted_coset_iff {a₀ : W}
        (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
        (w : planeSubgroup M cs P) (i : Bool) :
        rootInverted ((w : W)*a₀) (B.simpleRoot i) ↔ B.system.IsLeftDescent w i := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.rootInverted

44. def OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot line 1094

    Source documentation

    Geometric label of an intrinsic graph edge, taken in the actual ambient root plane rather than an abstract alternate representation.

    def edgeRoot {x y : planeSubgroup M cs P} (h : BruhatStep B.system x y) :
        PositiveRoot M cs := graphRoot ((B.bruhatStep_iff x y).mpr h)

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.PositiveRoot, OAI.KLInvariance.TitsSpace.graphRoot

45. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_plane line 1097
46. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_slopes_iff line 1106

    Source documentation

    In the intrinsic system, the middle-vertex test uses its actual left simple generator; it therefore applies to any induced dihedral realization.

    theorem edgeRoot_slopes_iff {x y z : planeSubgroup M cs P}
        (hxy : BruhatStep B.system x y) (hyz : BruhatStep B.system y z) :
        geometricSlope (B.edgeRoot hxy) < geometricSlope (B.edgeRoot hyz) ↔
          B.system.IsLeftDescent y false := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep, OAI.KLInvariance.TitsSpace.geometricSlope

47. def OAI.KLInvariance.TitsSpace.simplePositive line 1138
48. theorem OAI.KLInvariance.TitsSpace.simplePositive_val line 1141
49. theorem OAI.KLInvariance.TitsSpace.rootRef_simplePositive line 1144
50. theorem OAI.KLInvariance.TitsSpace.simplePositive_injective line 1148
51. theorem OAI.KLInvariance.TitsSpace.coordinate_sum line 1154
52. theorem OAI.KLInvariance.TitsSpace.dual_coordinate_sum line 1158
53. def OAI.KLInvariance.TitsSpace.PositiveFunctional line 1163
54. theorem OAI.KLInvariance.TitsSpace.PositiveFunctional.root_pos line 1165
55. theorem OAI.KLInvariance.TitsSpace.height_positive line 1175
56. structure OAI.KLInvariance.TitsSpace.RatioOrder line 1181

    Source documentation

    Both functionals are actual dual vectors; the root order is not a label-carrying addition to the interval isomorphism.

    structure RatioOrder where
    …

57. def OAI.KLInvariance.TitsSpace.RatioOrder.slope line 1190
58. theorem OAI.KLInvariance.TitsSpace.RatioOrder.denominator_pos line 1192
59. theorem OAI.KLInvariance.TitsSpace.RatioOrder.slope_injective line 1195
60. def OAI.KLInvariance.TitsSpace.RatioOrder.Adapted line 1198

    Source documentation

    The cut at zero is the genuine inversion set of the upper vertex.

    def Adapted (y : W) : Prop := ∀ a : PositiveRoot M cs,
    …

    Mentions: OAI.KLInvariance.TitsSpace.PositiveRoot

61. theorem OAI.KLInvariance.TitsSpace.RatioOrder.simple_lower_bound line 1201
62. theorem OAI.KLInvariance.TitsSpace.RatioOrder.exists_least_simple line 1214
63. theorem OAI.KLInvariance.TitsSpace.RatioOrder.least_simple_descent line 1220
64. def OAI.KLInvariance.TitsSpace.RatioOrder.Chamber line 1240

    Source documentation

    A functional in the chamber indexed by y has exactly Inv(y) as its negative roots. This is stronger data used only to construct the order.

    def Chamber (y : W) : Prop := ∀ i, 0 < O.numerator (action M cs y (root i))

    Mentions: OAI.KLInvariance.TitsSpace.action, OAI.KLInvariance.TitsSpace.root

65. theorem OAI.KLInvariance.TitsSpace.RatioOrder.adapted_of_chamber line 1242
66. theorem OAI.KLInvariance.TitsSpace.exists_ratioOrder_chamber_height line 1266

    Source documentation

    The generic functional can be chosen in any prescribed Coxeter chamber, not just outside the countably many equality hyperplanes. The explicit polynomial perturbation makes both requirements simultaneous.

    theorem exists_ratioOrder_chamber_height (y : W) :
        ∃ O : RatioOrder (M := M) (cs := cs), O.Chamber y ∧ O.denominator=height := by
    …

    Mentions: OAI.KLInvariance.TitsSpace.RatioOrder, OAI.KLInvariance.TitsSpace.height

67. theorem OAI.KLInvariance.TitsSpace.exists_ratioOrder_chamber line 1322
68. theorem OAI.KLInvariance.TitsSpace.positiveAction_simplePositive line 1327
69. theorem OAI.KLInvariance.TitsSpace.simple_action_nonneg line 1334
70. theorem OAI.KLInvariance.TitsSpace.simple_positiveAction_val line 1340
71. theorem OAI.KLInvariance.TitsSpace.simple_positiveAction_ne line 1345
72. theorem OAI.KLInvariance.TitsSpace.exists_uniform_pos_lt line 1351
73. def OAI.KLInvariance.TitsSpace.RatioOrder.turnNumerator line 1369
74. def OAI.KLInvariance.TitsSpace.RatioOrder.turnDenominator line 1372
75. theorem OAI.KLInvariance.TitsSpace.RatioOrder.exists_turn_parameter line 1375
76. theorem OAI.KLInvariance.TitsSpace.RatioOrder.turn_ratio_injective line 1413
77. def OAI.KLInvariance.TitsSpace.RatioOrder.turn line 1454
78. theorem OAI.KLInvariance.TitsSpace.RatioOrder.turn_chamber line 1459
79. theorem OAI.KLInvariance.TitsSpace.RatioOrder.turn_simple_greatest line 1468
80. theorem OAI.KLInvariance.TitsSpace.RatioOrder.turn_slope_lt_iff line 1489
81. theorem OAI.KLInvariance.TitsSpace.RatioOrder.exists_rotation line 1527

    Source documentation

    The actual geometric rotation needed for the Hecke recursion. It moves the least simple root to last and preserves all other root comparisons.

    theorem exists_rotation {y : W} (hy : y ≠ 1) (hc : O.Chamber y) :
        ∃ (i : I) (O' : RatioOrder (M := M) (cs := cs)),
    …

    Mentions: OAI.KLInvariance.TitsSpace.RatioOrder

82. def OAI.KLInvariance.Dihedral.rankFlip line 1563

    Source documentation

    Switch the two vertices at every strictly internal rank, leaving all other ranks fixed. The diagram involution supplies the intrinsic switch.

    def rankFlip (cs : CoxeterSystem M W) (L H : ℕ) (w : W) : W :=
    …

83. theorem OAI.KLInvariance.Dihedral.length_rankFlip line 1566
84. theorem OAI.KLInvariance.Dihedral.rankFlip_involutive line 1571
85. theorem OAI.KLInvariance.Dihedral.rankFlip_lower line 1577
86. theorem OAI.KLInvariance.Dihedral.rankFlip_upper line 1580
87. theorem OAI.KLInvariance.Dihedral.rankFlip_bruhat_iff line 1583
88. theorem OAI.KLInvariance.Dihedral.rankFlip_step_iff line 1588
89. def OAI.KLInvariance.Dihedral.intervalFlip line 1594

    Source documentation

    An automorphism of the unlabelled full dihedral interval, fixing its ends. It need not arise from a Coxeter-system automorphism at those ends.

    def intervalFlip (cs : CoxeterSystem M W) (lo hi : W) :
        Interval cs lo hi ≃o Interval cs lo hi where
    …

    Mentions: OAI.KLInvariance.Interval

90. theorem OAI.KLInvariance.Dihedral.intervalFlip_val line 1612
91. theorem OAI.KLInvariance.Dihedral.intervalFlip_involutive line 1616
92. def OAI.KLInvariance.Dihedral.edgeFlip line 1620
93. theorem OAI.KLInvariance.Dihedral.edgeFlip_source line 1633
94. theorem OAI.KLInvariance.Dihedral.edgeFlip_target line 1638
95. theorem OAI.KLInvariance.Dihedral.edgeFlip_involutive line 1643
96. theorem OAI.KLInvariance.SchedulePaths.IsPath.map line 1659

    Source documentation

    Relabelling graph vertices and edges preserves the actual path predicate.

    theorem IsPath.map {x y : V} {p : List E}
        (hp : IsPath source target x y p) (f : V → V') (g : E → E')
        (hs : ∀ e, source' (g e) = f (source e))
        (ht : ∀ e, target' (g e) = f (target e)) :
        IsPath source' target' (f x) (f y) (p.map g) := by
    …

    Mentions: OAI.KLInvariance.SchedulePaths.IsPath

97. theorem OAI.KLInvariance.SchedulePaths.IsPath.isChain line 1670

    Source documentation

    Every adjacent pair in a genuine path is composable.

    theorem IsPath.isChain {x y : V} {p : List E} (hp : IsPath source target x y p) :
        p.IsChain (fun e f => target e = source f) := by
    …

    Mentions: OAI.KLInvariance.SchedulePaths.IsPath

98. theorem OAI.KLInvariance.SchedulePaths.IsPath.pairwise_map_of_local line 1684

    Source documentation

    A path's adjacent comparisons suffice for a transitive label order. The statement allows the comparison to change under an edge map, provided the local relation is checked only on composable edges.

    theorem IsPath.pairwise_map_of_local {Λ Λ' : Type*} [LinearOrder Λ] [LinearOrder Λ']
        {x y : V} {p : List E} (hp : IsPath source target x y p)
        (label : E → Λ) (label' : E' → Λ') (g : E → E')
        (hlocal : ∀ e f, target e = source f →
          label e < label f → label' (g e) < label' (g f))
        (horder : p.Pairwise (fun e f => label e < label f)) :
        (p.map g).Pairwise (fun e f => label' e < label' f) := by
    …

    Mentions: OAI.KLInvariance.SchedulePaths.IsPath

99. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_ne_of_path line 1715
100. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.edgeRoot_slopes_rankFlip line 1722

     Source documentation

     At every internal vertex, the cut switches side under the path involution. This is the local relation behind rank-two path-product reversal.

     theorem edgeRoot_slopes_rankFlip {x y z top : planeSubgroup M cs P} {L : ℕ}
         (hxy : BruhatStep B.system x y) (hyz : BruhatStep B.system y z)
         (hL : L < B.system.length y) (hH : B.system.length y < B.system.length top) :
         let hx := (rankFlip_step_iff B.system L (B.system.length top) x y).mpr hxy
     …

     Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep

101. def OAI.KLInvariance.TitsSpace.PlaneBasis.intervalEdgeSlope line 1752

     Source documentation

     Restriction of the actual geometric root slope to a full plane interval.

     def intervalEdgeSlope (lo hi : planeSubgroup M cs P) (e : Edge B.system lo hi) : ℝ :=
     …

     Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup

102. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.intervalEdgeSlope_flip line 1757

     Source documentation

     The global edge map reverses the comparison for every composable pair. No statement is asserted for disjoint edge labels, which can share ties.

     theorem intervalEdgeSlope_flip {lo hi : planeSubgroup M cs P}
         (e f : Edge B.system lo hi)
         (hjoin : target B.system lo hi e = source B.system lo hi f) :
         B.intervalEdgeSlope lo hi e < B.intervalEdgeSlope lo hi f ↔
           B.intervalEdgeSlope lo hi (edgeFlip B.system lo hi f) <
             B.intervalEdgeSlope lo hi (edgeFlip B.system lo hi e) := by
     …

     Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup

103. def OAI.KLInvariance.SchedulePaths.subpaths line 1784

     Source documentation

     The finite set of genuine directed paths selected by an edge schedule.

     def subpaths (schedule : List E) (x y : V) : Finset (List E) :=
     …

104. theorem OAI.KLInvariance.SchedulePaths.mem_subpaths line 1787
105. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_subpaths_sum line 1794
106. theorem OAI.KLInvariance.SchedulePaths.dispatch_eq_of_path_involution line 1803

     Source documentation

     A length-preserving involution on the actual schedule-path sets proves an operator-entry relation, with no Hecke polynomial used in the assumptions.

     theorem dispatch_eq_of_path_involution (T : R) (schedule schedule' : List E)
         (hnd : schedule.Nodup) (hnd' : schedule'.Nodup) (x y : V) (g : E → E)
         (hg : Function.Involutive g)
         (hforward : ∀ p ∈ subpaths source target schedule x y,
           p.map g ∈ subpaths source target schedule' x y)
         (hbackward : ∀ p ∈ subpaths source target schedule' x y,
           p.map g ∈ subpaths source target schedule x y) :
         dispatch source target T (fun z => if z=y then 1 else 0) schedule x =
           dispatch source target T (fun z => if z=y then 1 else 0) schedule' x := by
     …

     Mentions: OAI.KLInvariance.SchedulePaths.subpaths, OAI.KLInvariance.SchedulePaths.dispatch

107. theorem OAI.KLInvariance.SchedulePaths.subpaths_map_of_sorted line 1828

     Source documentation

     Sorted full schedules select precisely their strictly monotone paths; an actual graph map satisfying the adjacent comparison test transports them.

     theorem subpaths_map_of_sorted (label label' : E → ℝ)
         (schedule schedule' : List E) (x y : V)
         (hs : schedule.Pairwise (fun e f => label f ≤ label e))
         (hs' : schedule'.Pairwise (fun e f => label' f ≤ label' e))
         (hfull' : ∀ e, e ∈ schedule')
         (hties : ∀ e f, label e = label f → target e ≠ source f)
         (f : V → V) (g : E → E)
         (hsource : ∀ e, source (g e) = f (source e))
         (htarget : ∀ e, target (g e) = f (target e))
         (hx : f x=x) (hy : f y=y)
         (hlocal : ∀ e f, target e=source f → label f<label e → label' (g f)<label' (g e))
         (p : List E) (hp : p ∈ subpaths source target schedule x y) :
     …

     Mentions: OAI.KLInvariance.SchedulePaths.subpaths

108. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.intervalEdgeSlope_ties line 1865
109. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.intervalEdgeSlope_flip_reverse line 1875
110. theorem OAI.KLInvariance.TitsSpace.PlaneBasis.dispatch_reverse_endpoints line 1889

     Source documentation

     Rank-two reversal of the genuine path-product entry between the two ends of any full interval. The order is the actual induced angular order.

     theorem dispatch_reverse_endpoints {R : Type*} [Semiring R]
         {lo hi : planeSubgroup M cs P} (hlohi : BruhatLE B.system lo hi)
         (schedule : List (Edge B.system lo hi)) (hnd : schedule.Nodup)
         (hfull : ∀ e, e ∈ schedule)
         (hs : schedule.Pairwise (fun e f => B.intervalEdgeSlope lo hi f ≤ B.intervalEdgeSlope lo hi e))
         (T : R) :
         let x : Interval B.system lo hi := ⟨lo,bruhat_refl B.system lo,hlohi⟩
     …

     Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatLE, OAI.KLInvariance.Interval, OAI.KLInvariance.bruhat_refl

111. abbrev OAI.KLInvariance.AdaptedDyer.Edge line 1948
112. def OAI.KLInvariance.AdaptedDyer.source line 1949
113. def OAI.KLInvariance.AdaptedDyer.target line 1950
114. def OAI.KLInvariance.AdaptedDyer.rootLabel line 1951
115. theorem OAI.KLInvariance.AdaptedDyer.rootRef_rootLabel line 1953
116. theorem OAI.KLInvariance.AdaptedDyer.target_eq_root line 1958
117. theorem OAI.KLInvariance.AdaptedDyer.rootLabel_ne_of_join line 1963
118. def OAI.KLInvariance.AdaptedDyer.score line 1972
119. theorem OAI.KLInvariance.AdaptedDyer.score_ties line 1975
120. def OAI.KLInvariance.AdaptedDyer.edgeFinset line 1980
121. theorem OAI.KLInvariance.AdaptedDyer.mem_edgeFinset line 1987
122. def OAI.KLInvariance.AdaptedDyer.schedule line 2005
123. theorem OAI.KLInvariance.AdaptedDyer.mem_schedule line 2008
124. theorem OAI.KLInvariance.AdaptedDyer.schedule_nodup line 2012
125. theorem OAI.KLInvariance.AdaptedDyer.schedule_increasing line 2016
126. theorem OAI.KLInvariance.AdaptedDyer.path_le line 2023
127. theorem OAI.KLInvariance.AdaptedDyer.path_targets_le line 2031
128. def OAI.KLInvariance.AdaptedDyer.paths line 2043
129. theorem OAI.KLInvariance.AdaptedDyer.mem_paths line 2046
130. def OAI.KLInvariance.AdaptedDyer.polynomial line 2063
131. theorem OAI.KLInvariance.AdaptedDyer.polynomial_dispatch line 2066
132. theorem OAI.KLInvariance.AdaptedDyer.rootRef_injective line 2073
133. theorem OAI.KLInvariance.AdaptedDyer.rootLabel_simple_iff line 2078
134. def OAI.KLInvariance.AdaptedDyer.rotateEdge line 2091

     Source documentation

     On a non-simple-labelled edge this is actual left multiplication by s. Simple-labelled edges are fixed merely to make the extension a total involution; all path uses below exclude them before applying this map.

     def rotateEdge (i : I) (e : Edge cs) : Edge cs :=
     …

     Mentions: OAI.KLInvariance.AdaptedDyer.Edge

135. theorem OAI.KLInvariance.AdaptedDyer.rotateEdge_val line 2096
136. theorem OAI.KLInvariance.AdaptedDyer.rotateEdge_root line 2100
137. theorem OAI.KLInvariance.AdaptedDyer.rotateEdge_nonsimple line 2112
138. theorem OAI.KLInvariance.AdaptedDyer.rotateEdge_involutive line 2117
139. theorem OAI.KLInvariance.AdaptedDyer.path_map_of_mem line 2132
140. theorem OAI.KLInvariance.AdaptedDyer.path_rotate line 2144
141. theorem OAI.KLInvariance.AdaptedDyer.rotateEdge_twice line 2156
142. def OAI.KLInvariance.AdaptedDyer.Nonsimple line 2160
143. theorem OAI.KLInvariance.AdaptedDyer.nonsimple_map line 2163
144. theorem OAI.KLInvariance.AdaptedDyer.path_map_twice line 2169
145. theorem OAI.KLInvariance.AdaptedDyer.path_rotate_iff line 2174
146. theorem OAI.KLInvariance.AdaptedDyer.paths_rotate_iff line 2184
147. theorem OAI.KLInvariance.AdaptedDyer.nonsimple_of_greatest line 2198
148. theorem OAI.KLInvariance.AdaptedDyer.nonsimple_tail_of_least line 2233
149. theorem OAI.KLInvariance.AdaptedDyer.nonsimple_of_least_descent line 2247
150. def OAI.KLInvariance.AdaptedDyer.nonsimplePaths line 2268
151. theorem OAI.KLInvariance.AdaptedDyer.mem_nonsimplePaths line 2271
152. theorem OAI.KLInvariance.AdaptedDyer.sum_nonsimple_rotate line 2276
153. def OAI.KLInvariance.AdaptedDyer.simpleEdge line 2309
154. theorem OAI.KLInvariance.AdaptedDyer.simpleEdge_source line 2313
155. theorem OAI.KLInvariance.AdaptedDyer.simpleEdge_target line 2317
156. theorem OAI.KLInvariance.AdaptedDyer.simpleEdge_root line 2320
157. theorem OAI.KLInvariance.AdaptedDyer.cons_simple_mem line 2325
158. theorem OAI.KLInvariance.AdaptedDyer.not_nonsimple_iff_cons line 2340
159. theorem OAI.KLInvariance.AdaptedDyer.polynomial_split line 2376
160. theorem OAI.KLInvariance.AdaptedDyer.polynomial_recursion line 2402

     Source documentation

     The path expansion satisfies exactly the genuine normalized Hecke recursion, because the chosen geometric order can be rotated at a descent.

     theorem polynomial_recursion (O O' : RatioOrder (M := M) (cs := cs)) (i : I)
     …

161. theorem OAI.KLInvariance.AdaptedDyer.paths_diagonal line 2431
162. theorem OAI.KLInvariance.AdaptedDyer.polynomial_diagonal line 2447
163. theorem OAI.KLInvariance.AdaptedDyer.polynomial_zero line 2451
164. theorem OAI.KLInvariance.AdaptedDyer.polynomial_eq_rTilde line 2462

     Source documentation

     Dyer's increasing-path formula for a genuine generic geometric order whose numerator is in the top chamber. The target is the Hecke-defined normalized R-polynomial, not a renamed path polynomial.

     theorem polynomial_eq_rTilde (O : RatioOrder (M := M) (cs := cs)) (x y : W)
     …

165. theorem OAI.KLInvariance.AdaptedDyer.exists_dyer_schedule line 2488

     Source documentation

     An adapted geometric order exists for every top, without adding labels or geometric data to the given interval isomorphism.

     theorem exists_dyer_schedule (y : W) :
         ∃ O : RatioOrder (M := M) (cs := cs), O.Chamber y ∧
     …