Sharp heights of all one-dimensional upper-set representations

theorem MagnitudeConjecture.PosetSpace.line_level_eq_card_of_sharp_grading {k T : Type u} [Field k] [PartialOrder T] [Fintype T] {L : ℕ} (G : PositiveGrading (Obj k T) (IsSchur k T) L) (hL : L ≤ Fintype.card T) (U : Finset T) (hU : IsUpperSet ↑U) : G.level (line k T (↑U) hU) = U.card

In a sharp positive grading every upper-set line has its support size as height, independently of any chosen reverse enumeration.