FoldingGcdInput.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Published gcd input for an admissible folding

Castella, Admissible submonoids of Artin--Tits monoids (2008), Proposition 41(2), states that an admissible folding preserves left and right gcds. Source: https://arxiv.org/pdf/0804.0704, p. 15. The field below is exactly its common-left-atom consequence: if two expanded positive words have a common left atom, their original words have a common left atom. The folding here is the color partition. Its required Coxeter admissibility is already established by unfoldedHom_right_ascent (constant ascent sign on every color).

The field involves positive words and braid relations only. It contains no tests, family action, height, stabilizer, or intersection assertion.

structure OAI.HarmonicArtin.ParabolicIntersections.PublishedFoldingGcd line 34
Source documentation
The precise part of published gcd preservation needed below. The sphericity proof is retained in the type to identify the admissible finite-type folding to which the source theorem is applied.
```
structure PublishedFoldingGcd (Y : Set S) (_hY : IsSpherical M Y) : Prop where
…
```
Mentions: OAI.HarmonicArtin.IsSpherical
theorem OAI.HarmonicArtin.ParabolicIntersections.unfolded_color_admissible line 45
Source documentation
The Coxeter admissibility condition is proved, rather than included as a categorical assumption: all vertices of a color have the same right-ascent behavior on every element of the folded Coxeter group.
```
theorem unfolded_color_admissible (Y : Set S) (hY : IsSpherical M Y)
    (w : (restrictedMatrix M Y).Group) (i : Y) (L H : FusionLabel m) :
    let N := (unfoldedMatrix M Y).toCoxeterSystem
…
```
Mentions: OAI.HarmonicArtin.IsSpherical, OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.unfoldedMatrix