Tits.lean`

190 declarations, 0 contain sorry, 0 declared as axioms

Actual Bruhat graph labels, Tits realizations and extended root spaces, cotangent coordinates and standard parabolic support.

def OAI.KLInvariance.BruhatGraph.Edge line 22
Source documentation
Actual finite directed moment-graph edges, including the non-cover reflection edges. No reconstruction from the abstract poset is assumed.
```
def Edge := {p : Interval cs u b × Interval cs u b // BruhatStep cs p.1.val p.2.val}
```
Mentions: OAI.KLInvariance.Interval, OAI.KLInvariance.BruhatStep
instance OAI.KLInvariance.BruhatGraph.(instance at line 24) line 24
def OAI.KLInvariance.BruhatGraph.source line 29
def OAI.KLInvariance.BruhatGraph.target line 30
def OAI.KLInvariance.BruhatGraph.graph line 32
def OAI.KLInvariance.BruhatGraph.label line 41
Source documentation
Genuine left reflection label; uniquely determined by the endpoints.
```
def label (e : Edge cs u b) : W := (target cs u b e).val * (source cs u b e).val⁻¹
```
Mentions: OAI.KLInvariance.BruhatGraph.Edge, OAI.KLInvariance.BruhatGraph.target, OAI.KLInvariance.BruhatGraph.source
theorem OAI.KLInvariance.BruhatGraph.label_isReflection line 43
theorem OAI.KLInvariance.BruhatGraph.label_mul_source line 47
theorem OAI.KLInvariance.BruhatGraph.label_mul_target line 51
theorem OAI.KLInvariance.BruhatGraph.eq_of_label_source_eq line 56
theorem OAI.KLInvariance.BruhatGraph.eq_of_label_target_eq line 65
theorem OAI.KLInvariance.BruhatGraph.source_ne_target_of_label_eq line 73
theorem OAI.KLInvariance.BruhatGraph.endpoints_disjoint_of_label_eq line 88

theorem OAI.KLInvariance.Realization.orthogonal_rank_one_form line 111

Source documentation

An actual rank-one perturbation that preserves a nondegenerate symmetric form is an orthogonal reflection, not a unipotent transvection.

theorem orthogonal_rank_one_form
    (B : LinearMap.BilinForm ℝ V) (hs : B.IsSymm) (hn : B.Nondegenerate)
    (u : V) (hu : u ≠ 0) (f : Module.Dual ℝ V) (hf : f ≠ 0)
    (hg : ∀ v w, B (v + f v • u) (w + f w • u) = B v w) :
    f u = -2 ∧ B u u ≠ 0 ∧
      ∀ v, v + f v • u = Module.preReflection u ((2 / B u u) • B u) v := by
…

theorem OAI.KLInvariance.Realization.orthogonal_finrank_one line 153

Source documentation

This is the rank-one assertion in bg:realization stated without a chosen rank-one normal form. Its conclusion uses the library's actual reflection.

theorem orthogonal_finrank_one
    (B : LinearMap.BilinForm ℝ V) (hs : B.IsSymm) (hn : B.Nondegenerate)
    (g : V ≃ₗ[ℝ] V) (hg : ∀ v w, B (g v) (g w) = B v w)
    (hr : Module.finrank ℝ (LinearMap.range (g.toLinearMap - LinearMap.id)) = 1) :
    ∃ u : V, B u u ≠ 0 ∧
      ∀ v, g v = Module.preReflection u ((2 / B u u) • B u) v := by
…

theorem OAI.KLInvariance.Realization.reflection_pow_even_eq_one line 196
theorem OAI.KLInvariance.Realization.reflection_pow_odd_eq_one line 207

theorem OAI.KLInvariance.Realization.geometric_reflection_relation line 225

Source documentation

If the two simple roots have the exact Tits pairing, the corresponding linear equivalences satisfy their finite Coxeter relation on the entire ambient space, not just on the root plane.

theorem geometric_reflection_relation
    {α β : V} {f g : Module.Dual ℝ V} (hf : f α = 2) (hg : g β = 2)
    (m : ℕ) (hm : 2 ≤ m)
    (hfg : f β = -2 * Real.cos (Real.pi / m))
    (hgf : g α = -2 * Real.cos (Real.pi / m)) :
    (Module.reflection hf * Module.reflection hg) ^ m = 1 := by
…

lemma OAI.KLInvariance.Realization.simple_normal_value line 307
def OAI.KLInvariance.Realization.geometricSimple line 311
theorem OAI.KLInvariance.Realization.geometricSimple_liftable line 314
def OAI.KLInvariance.Realization.geometricAction line 332
Source documentation
The genuine geometric reflection action. Each relation has been proved; this definition does not presuppose a faithful representation.
```
noncomputable def geometricAction : W →* (V ≃ₗ[ℝ] V) :=
…
```
theorem OAI.KLInvariance.Realization.geometricAction_simple line 335
theorem OAI.KLInvariance.Realization.geometricSimple_preserves line 339
theorem OAI.KLInvariance.Realization.geometricAction_preserves line 346
def OAI.KLInvariance.TitsSpace.gram line 365
def OAI.KLInvariance.TitsSpace.root line 367
def OAI.KLInvariance.TitsSpace.normal line 371
def OAI.KLInvariance.TitsSpace.form line 374
theorem OAI.KLInvariance.TitsSpace.normal_root line 377
theorem OAI.KLInvariance.TitsSpace.form_root line 387
theorem OAI.KLInvariance.TitsSpace.form_symm line 391
theorem OAI.KLInvariance.TitsSpace.form_roots line 405
theorem OAI.KLInvariance.TitsSpace.root_linearIndependent line 408
def OAI.KLInvariance.TitsSpace.action line 418
Source documentation
A concrete action on the ordinary geometric root space over ℝ. Its faithfulness and the root-sign theorem are still required for the main proof.
```
def action {W : Type v} [Group W] (cs : CoxeterSystem M W) :
    W →* ((I → ℝ) ≃ₗ[ℝ] (I → ℝ)) :=
…
```
theorem OAI.KLInvariance.TitsSpace.action_simple line 422
theorem OAI.KLInvariance.TitsSpace.action_preserves line 428
abbrev OAI.KLInvariance.Realization.Extension line 439
def OAI.KLInvariance.Realization.extensionForm line 441
theorem OAI.KLInvariance.Realization.extensionForm_apply line 462
theorem OAI.KLInvariance.Realization.extensionForm_inl line 466
theorem OAI.KLInvariance.Realization.extensionForm_symm line 470
theorem OAI.KLInvariance.Realization.extensionForm_nondegenerate line 478
theorem OAI.KLInvariance.Realization.exists_minimal_nondegenerate_extension line 507
theorem OAI.KLInvariance.Realization.extension_finrank line 517
theorem OAI.KLInvariance.Realization.extension_dimension_minimal line 522
abbrev OAI.KLInvariance.TitsSpace.Extended line 553
def OAI.KLInvariance.TitsSpace.extendedForm line 555
theorem OAI.KLInvariance.TitsSpace.extendedForm_spec line 558
def OAI.KLInvariance.TitsSpace.extendedRoot line 562
theorem OAI.KLInvariance.TitsSpace.extendedForm_roots line 564
theorem OAI.KLInvariance.TitsSpace.extendedRoot_linearIndependent line 569
theorem OAI.KLInvariance.TitsSpace.extendedNormal_linearIndependent line 575
Source documentation
Both roots and coroots are independent in the actual minimal extension.
```
theorem extendedNormal_linearIndependent :
    LinearIndependent ℝ (fun i => extendedForm M (extendedRoot M i)) :=
…
```
Mentions: OAI.KLInvariance.TitsSpace.extendedForm, OAI.KLInvariance.TitsSpace.extendedRoot
def OAI.KLInvariance.TitsSpace.extendedAction line 579
theorem OAI.KLInvariance.TitsSpace.extendedAction_preserves line 583
theorem OAI.KLInvariance.TitsSpace.extendedAction_simple line 589
theorem OAI.KLInvariance.TitsSpace.extendedAction_restrict line 599
Source documentation
The extended action genuinely restricts to the ordinary geometric action. Injectivity of that latter action is an outstanding obligation, not a hypothesis hidden in the construction of this extension.
```
theorem extendedAction_restrict {W : Type v} [Group W] (cs : CoxeterSystem M W)
    (w : W) (v : I → ℝ) :
    extendedAction M cs w (v, 0) = (action M cs w v, 0) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.extendedAction, OAI.KLInvariance.TitsSpace.action
theorem OAI.KLInvariance.TitsSpace.extended_finrank line 613
def OAI.KLInvariance.TitsSpace.dominant line 618
theorem OAI.KLInvariance.TitsSpace.dominant_root line 622
def OAI.KLInvariance.ParabolicSupport.subgroup line 639
Source documentation
The genuine subgroup generated by a subset of simple reflections.
```
def subgroup : Subgroup W := Subgroup.closure (cs.simple '' J)
```
theorem OAI.KLInvariance.ParabolicSupport.word_mem line 641
theorem OAI.KLInvariance.ParabolicSupport.exists_word line 651
theorem OAI.KLInvariance.ParabolicSupport.exists_reduced_word line 667

theorem OAI.KLInvariance.ParabolicSupport.reduced_append_of_minimal line 675

Source documentation

A minimal right-coset representative concatenates with every reduced word in the parabolic generators without cancellations.

theorem reduced_append_of_minimal {u : W}
    (hmin : ∀ v ∈ subgroup cs J, cs.length u ≤ cs.length (u * v))
    {ω ν : List B} (hω : cs.IsReduced ω) (hu : cs.wordProd ω = u)
    (hν : cs.IsReduced ν) (hJ : ∀ i ∈ ν, i ∈ J) :
    cs.IsReduced (ω ++ ν) := by
…

Mentions: OAI.KLInvariance.ParabolicSupport.subgroup

theorem OAI.KLInvariance.ParabolicSupport.length_mul_of_minimal line 705
theorem OAI.KLInvariance.ParabolicSupport.exists_minimal line 714
Source documentation
Every right parabolic coset has a minimal representative.
```
theorem exists_minimal (w : W) :
    ∃ u v : W, v ∈ subgroup cs J ∧ w = u * v ∧
      ∀ z ∈ subgroup cs J, cs.length u ≤ cs.length (u * z) := by
…
```
Mentions: OAI.KLInvariance.ParabolicSupport.subgroup
theorem OAI.KLInvariance.ParabolicSupport.minimal_simple_ascent line 727

theorem OAI.KLInvariance.ParabolicSupport.exists_length_additive_decomposition line 735

Source documentation

The decomposition is length-additive, including after multiplying by any of the chosen simple generators. This is used in the root-sign induction.

theorem exists_length_additive_decomposition (w : W) :
    ∃ u v : W, v ∈ subgroup cs J ∧ w = u * v ∧
      cs.length w = cs.length u + cs.length v ∧
      (∀ i ∈ J, cs.length (u * cs.simple i) = cs.length u + 1) ∧
      (∀ i ∈ J, cs.length (w * cs.simple i) = cs.length u + cs.length (v * cs.simple i)) := by
…

Mentions: OAI.KLInvariance.ParabolicSupport.subgroup

theorem OAI.KLInvariance.ParabolicSupport.reduced_of_append line 759

theorem OAI.KLInvariance.ParabolicSupport.reduced_pair_eq_alternating line 764

Source documentation

A reduced two-letter word followed by i must alternate and end in j.

theorem reduced_pair_eq_alternating {ω : List B} {i j : B} (hij : i ≠ j)
    (hJ : ∀ k ∈ ω, k = i ∨ k = j) (hred : cs.IsReduced (ω ++ [i])) :
    ω = alternatingWord i j ω.length := by
…

theorem OAI.KLInvariance.ParabolicSupport.alternating_length_bound line 790
Source documentation
The coefficients in the root formula are controlled by genuine reducedness, not by a separate rank-two length assumption.
```
theorem alternating_length_bound {ω : List B} {i j : B} (hij : i ≠ j)
    (hJ : ∀ k ∈ ω, k = i ∨ k = j) (hred : cs.IsReduced (ω ++ [i])) :
    M i j = 0 ∨ ω.length + 1 ≤ M i j := by
…
```
def OAI.KLInvariance.TitsSpace.rootCoeff line 813
theorem OAI.KLInvariance.TitsSpace.rootCoeff_zero line 817
theorem OAI.KLInvariance.TitsSpace.rootCoeff_neg_one line 821
theorem OAI.KLInvariance.TitsSpace.rootCoeff_succ line 826
theorem OAI.KLInvariance.TitsSpace.gram_diag line 833

theorem OAI.KLInvariance.TitsSpace.alternating_root line 838

Source documentation

Exact rank-two root formula, including the infinite pairing.

theorem alternating_root (i j : I) (n : ℕ) :
    action M cs (cs.wordProd (alternatingWord i j n)) (root i) =
      if Even n then
        rootCoeff M i j n • root i + rootCoeff M i j ((n : ℤ)-1) • root j
      else rootCoeff M i j ((n : ℤ)-1) • root i + rootCoeff M i j n • root j := by
…

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

theorem OAI.KLInvariance.TitsSpace.rootCoeff_nonneg line 867
Source documentation
For a reduced alternating word followed by the other generator, both rank-two coefficients are nonnegative.
```
theorem rootCoeff_nonneg (i j : I) {n : ℤ} (hn : -1 ≤ n)
    (hm : M i j = 0 ∨ n + 1 ≤ (M i j : ℤ)) (hij : i ≠ j) :
    0 ≤ rootCoeff M i j n := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.rootCoeff
theorem OAI.KLInvariance.TitsSpace.root_nonneg line 912

theorem OAI.KLInvariance.TitsSpace.pair_image_nonneg line 919

Source documentation

Positivity of a rank-two reduced tail after an already positive prefix.

theorem pair_image_nonneg (u : W) {i j : I} (hij : i ≠ j)
    (hi : ∀ k, 0 ≤ action M cs u (root i) k)
    (hj : ∀ k, 0 ≤ action M cs u (root j) k)
    {ω : List I} (hJ : ∀ k ∈ ω, k = i ∨ k = j)
    (hred : cs.IsReduced (ω ++ [i])) :
    ∀ k, 0 ≤ action M cs (u * cs.wordProd ω) (root i) k := by
…

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

theorem OAI.KLInvariance.TitsSpace.action_root_nonneg_of_ascent line 941
Source documentation
The genuine Tits root-sign theorem for ascents, proved from exchange, minimal parabolic cosets and the rank-two trigonometric formulas.
```
theorem action_root_nonneg_of_ascent (w : W) (i : I)
    (hasc : cs.length (w * cs.simple i) = cs.length w + 1) :
    ∀ k, 0 ≤ action M cs w (root i) k := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.action, OAI.KLInvariance.TitsSpace.root
theorem OAI.KLInvariance.TitsSpace.action_simple_root line 980
theorem OAI.KLInvariance.TitsSpace.action_root_nonpos_of_descent line 985
Source documentation
Descents carry a simple root into the negative cone.
```
theorem action_root_nonpos_of_descent (w : W) (i : I)
    (hdesc : cs.length (w * cs.simple i) < cs.length w) :
    ∀ k, action M cs w (root i) k ≤ 0 := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.action, OAI.KLInvariance.TitsSpace.root
theorem OAI.KLInvariance.TitsSpace.action_injective line 997
Source documentation
Faithfulness of the actual ordinary Tits action, not an added axiom.
```
theorem action_injective : Function.Injective (action M cs) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.action

theorem OAI.KLInvariance.Realization.finrank_moving_conj line 1015

Source documentation

Rank of the moving subspace is unchanged by conjugacy.

theorem finrank_moving_conj (g h : V ≃ₗ[ℝ] V) :
    Module.finrank ℝ (LinearMap.range ((h * g * h⁻¹).toLinearMap - LinearMap.id)) =
      Module.finrank ℝ (LinearMap.range (g.toLinearMap - LinearMap.id)) := by
…

theorem OAI.KLInvariance.Realization.rank_one_eq_reflection_of_negates line 1026

Source documentation

An orthogonal rank-one map negating a norm-two vector is its exact reflection.

theorem rank_one_eq_reflection_of_negates [FiniteDimensional ℝ V]
    (B : LinearMap.BilinForm ℝ V) (g : V ≃ₗ[ℝ] V)
    (hg : ∀ v w, B (g v) (g w) = B v w)
    (hr : Module.finrank ℝ (LinearMap.range (g.toLinearMap - LinearMap.id)) = 1)
    (e : V) (he : B e e = 2) (hge : g e = -e) :
    ∀ v, g v = Module.preReflection e (B e) v := by
…

theorem OAI.KLInvariance.Realization.negates_of_commutes_nonpos line 1059

Source documentation

Commutation with a reflection makes its negative eigenspace invariant; a nonpositive coordinate selects the negative, rather than positive, sign.

theorem negates_of_commutes_nonpos
    (B : LinearMap.BilinForm ℝ V) (g : V ≃ₗ[ℝ] V)
    (hg : ∀ v w, B (g v) (g w) = B v w)
    (e : V) (he : B e e = 2)
    (hcomm : g * Module.reflection he = Module.reflection he * g)
    (f : Module.Dual ℝ V) (hfe : f e = 1) (hfg : f (g e) ≤ 0) :
    g e = -e := by
…

theorem OAI.KLInvariance.Realization.range_reflection_sub_id line 1080

Source documentation

The moving subspace of a genuine reflection is exactly its root line.

theorem range_reflection_sub_id (e : V) (f : Module.Dual ℝ V) (h : f e = 2) :
    LinearMap.range ((Module.reflection h).toLinearMap - LinearMap.id) =
      Submodule.span ℝ {e} := by
…

theorem OAI.KLInvariance.Realization.finrank_reflection_sub_id line 1099
theorem OAI.KLInvariance.TitsSpace.extendedAction_injective line 1117
Source documentation
Faithfulness persists in the actual nondegenerate extension.
```
theorem extendedAction_injective : Function.Injective (extendedAction M cs) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.extendedAction
theorem OAI.KLInvariance.TitsSpace.extendedForm_root_self line 1124
theorem OAI.KLInvariance.TitsSpace.extendedAction_simple_eq line 1129
theorem OAI.KLInvariance.TitsSpace.involution_of_moving_rank_one line 1136
Source documentation
A rank-one element of the actual extended action is an involution.
```
theorem involution_of_moving_rank_one (w : W)
    (hr : Module.finrank ℝ (LinearMap.range
      ((extendedAction M cs w).toLinearMap - LinearMap.id)) = 1) : w⁻¹ = w := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.extendedAction
theorem OAI.KLInvariance.TitsSpace.isReflection_of_moving_rank_one line 1156
Source documentation
Reflection faithfulness, the difficult converse, proved by length descent. This avoids assuming the finite-subgroup theorem cited in the manuscript.
```
theorem isReflection_of_moving_rank_one (w : W)
    (hr : Module.finrank ℝ (LinearMap.range
      ((extendedAction M cs w).toLinearMap - LinearMap.id)) = 1) :
    cs.IsReflection w := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.extendedAction
theorem OAI.KLInvariance.TitsSpace.moving_rank_one_of_isReflection line 1243
Source documentation
The other direction of reflection faithfulness for the actual action.
```
theorem moving_rank_one_of_isReflection (w : W) (hw : cs.IsReflection w) :
    Module.finrank ℝ (LinearMap.range
      ((extendedAction M cs w).toLinearMap - LinearMap.id)) = 1 := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.extendedAction
theorem OAI.KLInvariance.TitsSpace.reflectionFaithful line 1255
theorem OAI.KLInvariance.TitsSpace.dominant_action_root line 1260
theorem OAI.KLInvariance.TitsSpace.dominant_pos_iff_ascent line 1266
Source documentation
Strict dominant sign, not merely closed-cone positivity.
```
theorem dominant_pos_iff_ascent (w : W) (i : I) :
    0 < dominant M (extendedAction M cs w (extendedRoot M i)) ↔
      cs.length w < cs.length (w * cs.simple i) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.dominant, OAI.KLInvariance.TitsSpace.extendedAction, OAI.KLInvariance.TitsSpace.extendedRoot
theorem OAI.KLInvariance.TitsSpace.dominant_dual_pos_iff_left_ascent line 1294
Source documentation
The strictly dominant linear form in the convention (w ρ)(αᵢ)=ρ(w⁻¹αᵢ) has exactly the source manuscript's left-ascent sign.
```
theorem dominant_dual_pos_iff_left_ascent (w : W) (i : I) :
    0 < dominant M (extendedAction M cs w⁻¹ (extendedRoot M i)) ↔
      cs.length w < cs.length (cs.simple i * w) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.dominant, OAI.KLInvariance.TitsSpace.extendedAction, OAI.KLInvariance.TitsSpace.extendedRoot
def OAI.KLInvariance.Cotangent.root line 1314
lemma OAI.KLInvariance.Cotangent.normal_root line 1316
def OAI.KLInvariance.Cotangent.simple line 1319
theorem OAI.KLInvariance.Cotangent.simple_liftable line 1321
def OAI.KLInvariance.Cotangent.action line 1339
theorem OAI.KLInvariance.Cotangent.action_simple line 1342
lemma OAI.KLInvariance.Cotangent.dot_root line 1351
lemma OAI.KLInvariance.Cotangent.root_dot line 1355
lemma OAI.KLInvariance.Cotangent.simple_pairing line 1359
theorem OAI.KLInvariance.Cotangent.pairing line 1370
theorem OAI.KLInvariance.Cotangent.action_injective line 1379
def OAI.KLInvariance.StandardParabolic.matrix line 1402
abbrev OAI.KLInvariance.StandardParabolic.system line 1408
def OAI.KLInvariance.StandardParabolic.inclusion line 1411
theorem OAI.KLInvariance.StandardParabolic.inclusion_simple line 1415
lemma OAI.KLInvariance.StandardParabolic.inclusion_word line 1419
def OAI.KLInvariance.StandardParabolic.restrictVec line 1426
lemma OAI.KLInvariance.StandardParabolic.simple_restrict line 1428
theorem OAI.KLInvariance.StandardParabolic.action_restrict line 1436
theorem OAI.KLInvariance.StandardParabolic.inclusion_injective line 1446
lemma OAI.KLInvariance.StandardParabolic.lift_word line 1462
theorem OAI.KLInvariance.StandardParabolic.inclusion_mem line 1470
theorem OAI.KLInvariance.StandardParabolic.inclusion_range line 1479
theorem OAI.KLInvariance.StandardParabolic.length_inclusion line 1488
lemma OAI.KLInvariance.StandardParabolic.reduced_map_iff line 1505
theorem OAI.KLInvariance.StandardParabolic.bruhat_inclusion_iff line 1519
theorem OAI.KLInvariance.StandardParabolic.lower_range line 1538
def OAI.KLInvariance.StandardParabolic.intervalMap line 1548
lemma OAI.KLInvariance.StandardParabolic.intervalMap_bijective line 1554
def OAI.KLInvariance.StandardParabolic.intervalIso line 1571
Source documentation
The exact unlabelled interval identification used in the finite-rank reduction; it arises from a proved embedding, not an added main hypothesis.
```
def intervalIso (x y : (matrix (M := M) J).Group) :
…
```
Mentions: OAI.KLInvariance.StandardParabolic.matrix
theorem OAI.KLInvariance.StandardParabolic.intervalIso_val line 1579
lemma OAI.KLInvariance.StandardParabolic.rankDifference_inclusion line 1583
theorem OAI.KLInvariance.StandardParabolic.normalized_restriction line 1590
Source documentation
Restriction of the actual normalized families satisfies their exact recurrence, degree bound and interval reciprocity in the standard parabolic.
```
theorem normalized_restriction {RP : PolynomialFamilies W} (hRP : NormalizedKL cs RP) :
    NormalizedKL (system (M := M) J)
…
```
Mentions: OAI.KLInvariance.PolynomialFamilies, OAI.KLInvariance.NormalizedKL, OAI.KLInvariance.StandardParabolic.system
theorem OAI.KLInvariance.StandardParabolic.klFamilies_inclusion line 1629
theorem OAI.KLInvariance.StandardParabolic.klPolynomial_inclusion line 1636
theorem OAI.KLInvariance.StandardParabolic.rPolynomial_inclusion line 1641
def OAI.KLInvariance.TitsSpace.IsRoot line 1657
Source documentation
A genuine real root, obtained from a simple root by the Tits action.
```
def IsRoot (a : I → ℝ) : Prop := ∃ w : W, ∃ i : I, a = action M cs w (root i)
```
Mentions: OAI.KLInvariance.TitsSpace.action, OAI.KLInvariance.TitsSpace.root
def OAI.KLInvariance.TitsSpace.Represents line 1660
Source documentation
A normalized real root representing a genuine Coxeter reflection.
```
def Represents (t : W) (a : I → ℝ) : Prop :=
…
```
abbrev OAI.KLInvariance.TitsSpace.embed line 1663
theorem OAI.KLInvariance.TitsSpace.form_root_self line 1665
theorem OAI.KLInvariance.TitsSpace.IsRoot.norm line 1670
theorem OAI.KLInvariance.TitsSpace.IsRoot.ne_zero line 1674
theorem OAI.KLInvariance.TitsSpace.IsRoot.sign line 1679
theorem OAI.KLInvariance.TitsSpace.IsRoot.neg line 1687
theorem OAI.KLInvariance.TitsSpace.IsRoot.act line 1692
theorem OAI.KLInvariance.TitsSpace.Represents.isRoot line 1697
theorem OAI.KLInvariance.TitsSpace.Represents.isReflection line 1702
theorem OAI.KLInvariance.TitsSpace.Represents.neg line 1707
theorem OAI.KLInvariance.TitsSpace.Represents.act line 1714
theorem OAI.KLInvariance.TitsSpace.Represents.formula line 1723
Source documentation
The actual reflection formula for every conjugate root in the minimal nondegenerate extension, not merely for simple roots.
```
theorem Represents.formula {t : W} {a : I → ℝ} (ha : Represents M cs t a)
    (v : Extended M) :
    extendedAction M cs t v = v - extendedForm M (embed M a) v • embed M a := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.Represents, OAI.KLInvariance.TitsSpace.Extended, OAI.KLInvariance.TitsSpace.extendedAction, OAI.KLInvariance.TitsSpace.extendedForm, OAI.KLInvariance.TitsSpace.embed
theorem OAI.KLInvariance.TitsSpace.Represents.action_formula line 1737
theorem OAI.KLInvariance.TitsSpace.Represents.unique_up_to_sign line 1743
theorem OAI.KLInvariance.TitsSpace.Represents.reflection_unique line 1765
theorem OAI.KLInvariance.TitsSpace.Represents.unique_positive line 1772
theorem OAI.KLInvariance.TitsSpace.exists_positive_root line 1789
def OAI.KLInvariance.TitsSpace.PositiveRoot line 1799
Source documentation
Genuine positive roots, with their actual coordinate sign.
```
def PositiveRoot := {a : I → ℝ // IsRoot M cs a ∧ ∀ i, 0 ≤ a i}
```
Mentions: OAI.KLInvariance.TitsSpace.IsRoot
def OAI.KLInvariance.TitsSpace.positiveRoot line 1801
theorem OAI.KLInvariance.TitsSpace.positiveRoot_represents line 1806
def OAI.KLInvariance.TitsSpace.rootReflection line 1810
theorem OAI.KLInvariance.TitsSpace.rootReflection_represents line 1815
def OAI.KLInvariance.TitsSpace.positiveRootEquiv line 1821
theorem OAI.KLInvariance.TitsSpace.IsRoot.not_both line 1839
theorem OAI.KLInvariance.TitsSpace.IsRoot.eq_simple_of_nonpos line 1847
Source documentation
A simple reflection can turn a positive real root negative only on its own root. This uses actual Tits coordinates and normalization.
```
theorem IsRoot.eq_simple_of_nonpos {a : I → ℝ} (ha : IsRoot M cs a)
    (hp : ∀ k, 0 ≤ a k) (i : I)
    (hn : ∀ k, action M cs (cs.simple i) a k ≤ 0) : a = root i := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.IsRoot, OAI.KLInvariance.TitsSpace.action, OAI.KLInvariance.TitsSpace.root
theorem OAI.KLInvariance.TitsSpace.Represents.simple_sign line 1867
def OAI.KLInvariance.TitsSpace.SignedRepresents line 1891
Source documentation
The signed combinatorial reflection action is the actual root sign under the faithful Tits representation.
```
def SignedRepresents (p : W × ZMod 2) (a : I → ℝ) : Prop :=
…
```
theorem OAI.KLInvariance.TitsSpace.SignedRepresents.simple line 1895
theorem OAI.KLInvariance.TitsSpace.SignedRepresents.act line 1916
theorem OAI.KLInvariance.TitsSpace.Represents.inversion_iff line 1928
theorem OAI.KLInvariance.TitsSpace.Represents.independent_of_ne line 1983
theorem OAI.KLInvariance.TitsSpace.Represents.extended_independent_of_ne line 1998
theorem OAI.KLInvariance.TitsSpace.Represents.extendedAction_eq line 2010
theorem OAI.KLInvariance.TitsSpace.Represents.plane_eq_of_product_eq line 2019
def OAI.KLInvariance.TitsSpace.RootInversions line 2039
Source documentation
The actual positive ambient roots inverted by w.
```
def RootInversions (w : W) :=
…
```
def OAI.KLInvariance.TitsSpace.rootInversionEquiv line 2042
def OAI.KLInvariance.TitsSpace.leftInversionListEquiv line 2057
theorem OAI.KLInvariance.TitsSpace.rootInversions_finite line 2065
Source documentation
Full ambient inversion count, not a cardinality assumption.
```
theorem rootInversions_finite (w : W) : Finite (RootInversions M cs w) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.RootInversions
theorem OAI.KLInvariance.TitsSpace.card_rootInversions line 2073
def OAI.KLInvariance.TitsSpace.movingSubgroup line 2093
Source documentation
Elements whose actual linear displacement lies in P. This is a subgroup even when the invariant bilinear form restricted to P is singular.
```
def movingSubgroup (P : Submodule ℝ (I → ℝ)) : Subgroup W where
…
```
def OAI.KLInvariance.TitsSpace.planeSubgroup line 2110
Source documentation
The manuscript's maximal plane reflection subgroup, defined using actual normalized roots, not by assuming a rank-two presentation.
```
def planeSubgroup (P : Submodule ℝ (I → ℝ)) : Subgroup W :=
…
```
theorem OAI.KLInvariance.TitsSpace.planeSubgroup_le_moving line 2113
theorem OAI.KLInvariance.TitsSpace.Represents.mem_of_moving line 2122
theorem OAI.KLInvariance.TitsSpace.Represents.planeSubgroup_mem_iff line 2134
theorem OAI.KLInvariance.TitsSpace.reflection_between_coset_mem line 2144
Source documentation
Two ambient vertices in a left coset of this plane subgroup can have no reflection edge except one whose actual root is in the plane.
```
theorem reflection_between_coset_mem {P : Submodule ℝ (I → ℝ)} {t g h a : W}
    (hg : g ∈ planeSubgroup M cs P) (hh : h ∈ planeSubgroup M cs P)
    (heq : h*a=t*(g*a)) {r : I → ℝ} (ht : Represents M cs t r) : r ∈ P := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.Represents
theorem OAI.KLInvariance.TitsSpace.planeCoset_exists_minimal line 2166
Source documentation
Least ambient length in each actual left plane-subgroup coset. No uniqueness or rank-two Coxeter presentation is smuggled into this definition.
```
theorem planeCoset_exists_minimal (P : Submodule ℝ (I → ℝ)) (a : W) :
    ∃ a₀ g : W, g ∈ planeSubgroup M cs P ∧ a = g*a₀ ∧
      ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀) := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup
theorem OAI.KLInvariance.TitsSpace.planeSubgroup_preserves line 2183
theorem OAI.KLInvariance.TitsSpace.root_nonneg_of_coset_minimal line 2191
Source documentation
A least coset representative sends every positive plane root to a positive ambient root under its inverse, by the proved inversion criterion.
```
theorem root_nonneg_of_coset_minimal {P : Submodule ℝ (I → ℝ)} {a₀ : W}
    (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
    {a : I → ℝ} (ha : IsRoot M cs a) (hp : ∀ i, 0 ≤ a i) (haP : a ∈ P) :
    ∀ i, 0 ≤ action M cs a₀⁻¹ a i := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.TitsSpace.IsRoot, OAI.KLInvariance.TitsSpace.action
theorem OAI.KLInvariance.TitsSpace.root_nonpos_coset_minimal_iff line 2204
theorem OAI.KLInvariance.TitsSpace.root_inversion_coset_iff line 2218
theorem OAI.KLInvariance.TitsSpace.leftInversion_coset_iff line 2229
theorem OAI.KLInvariance.TitsSpace.bruhatStep_coset_iff line 2244
Source documentation
The directed ambient reflection graph on any plane-subgroup coset is exactly transported from that on the subgroup by a least coset representative. Identifying this graph with a dihedral Coxeter graph still requires the canonical rank-two reflection-subgroup theorem.
```
theorem bruhatStep_coset_iff {P : Submodule ℝ (I → ℝ)} {a₀ g h : W}
    (hmin : ∀ z ∈ planeSubgroup M cs P, cs.length a₀ ≤ cs.length (z*a₀))
    (hg : g ∈ planeSubgroup M cs P) (hh : h ∈ planeSubgroup M cs P) :
    BruhatStep cs (g*a₀) (h*a₀) ↔ BruhatStep cs g h := by
…
```
Mentions: OAI.KLInvariance.TitsSpace.planeSubgroup, OAI.KLInvariance.BruhatStep