InitialMinimum.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The initial singleton is a minimum of the full relative harmonic height.

lemma OAI.HarmonicArtin.ParabolicIntersections.vector_eq_single_of_sum line 11
lemma OAI.HarmonicArtin.ParabolicIntersections.initial_profile line 26
lemma OAI.HarmonicArtin.ParabolicIntersections.pointedCosetVector_frame_of_relative line 34
lemma OAI.HarmonicArtin.ParabolicIntersections.initial_block_le line 47
theorem OAI.HarmonicArtin.ParabolicIntersections.initial_height_minimum line 97
Source documentation
The minimum-height assertion in the proof of the initial stabilizer, including the full vector and full sign mask.
```
theorem initial_height_minimum (U : Set (S ⊕ Unit)) (cutoff : ℤ) (Y : Set S) (hf : f ∉ Y)
    (P : RelativeVertex M Y 1) :
    relativeHeight M f U cutoff (sourceCoset M ∅ (spherical_empty M) 1) ≤
      relativeHeight M f U cutoff P.val := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.RelativeVertex, OAI.HarmonicArtin.ParabolicIntersections.relativeHeight, OAI.HarmonicArtin.sourceCoset, OAI.HarmonicArtin.spherical_empty