FoldingHead.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Greedy heads, and hence left atoms, are preserved by folding.

lemma OAI.HarmonicArtin.ParabolicIntersections.positive_nil line 18
lemma OAI.HarmonicArtin.ParabolicIntersections.positive_cons line 21
Distinct definitions of this name: OAI/Topology/ArtinGroups/ParabolicIntersections/BraidRestriction.lean:15 (different declaration text). Qualify references as OAI.HarmonicArtin.ParabolicIntersections.positive_cons@path.

theorem OAI.HarmonicArtin.ParabolicIntersections.folded_positive_head line 25

Source documentation

The original and folded positive elements have corresponding greedy heads.

theorem folded_positive_head (b : PositiveArtin R) :
    ∃ h : (R).Group,
      PositivePrefix R (P h) b ∧
      (∀ w, PositivePrefix R (P w) b → PositivePrefix R (P w) (P h)) ∧
      PositivePrefix N (Φ (P h)) (Φ b) ∧
      (∀ w, PositivePrefix N (positiveSimpleLift N w) (Φ b) →
        PositivePrefix N (positiveSimpleLift N w) (Φ (P h))) := by
…

Mentions: OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.PositivePrefix, OAI.HarmonicArtin.positiveSimpleLift

theorem OAI.HarmonicArtin.ParabolicIntersections.folded_atom_reflect line 91
Source documentation
Every atom dividing an expanded positive word has its entire color as a left divisor. This is the exact divisibility consequence needed downstream.
```
theorem folded_atom_reflect (b : PositiveArtin R)
    (α : Y × FusionLabel (fusionLabelSize M))
    (hα : PositivePrefix N (positiveGenerator N α) (Φ b)) :
    PositivePrefix R (positiveGenerator R α.1) b := by
…
```
Mentions: OAI.HarmonicArtin.PositiveArtin, OAI.HarmonicArtin.FusionLabel, OAI.HarmonicArtin.fusionLabelSize, OAI.HarmonicArtin.PositivePrefix, OAI.HarmonicArtin.positiveGenerator