Markedness cutoffs on a scale

The order-theoretic core of differential-marking cutoffs, generic over any scale (any [Preorder S]). A cutoff marks one end of the scale; the marked region is an Set.Ici/Set.Iic, hence an upper/lower set — the "staircase" monotonicity ([Ais03]) that every prominence scale (animacy, definiteness, person, …) shares. Stated once here over the order mixin, so each scale instantiates it rather than re-proving by decide.

Main declarations

• Core.Order.atOrAbove / atOrBelow — the cutoff predicates (c ≤ · / · ≤ c)
• Core.Order.atOrAbove_isUpperSet / atOrBelow_isLowerSet — monotonicity, for any scale

def Core.Order.atOrAbove {S : Type u_1} [Preorder S] (c s : S) : Prop

The "marked above a cutoff" predicate on a scale: at or above c. The prominent-end cutoff shared by every differential-marking scale.

Equations

• Core.Order.atOrAbove c s = (c ≤ s)

def Core.Order.atOrBelow {S : Type u_1} [Preorder S] (c s : S) : Prop

The "marked below a cutoff" predicate: at or below c (the anti-monotone cutoff, for high-default roles).

Equations

• Core.Order.atOrBelow c s = (s ≤ c)

theorem Core.Order.atOrAbove_isUpperSet {S : Type u_1} [Preorder S] (c : S) : IsUpperSet {s : S | atOrAbove c s}

Marking the prominent end is monotone: the marked region of an atOrAbove cutoff is an upper set, for ANY scale. Replaces per-scale decide proofs of the staircase property.

theorem Core.Order.atOrBelow_isLowerSet {S : Type u_1} [Preorder S] (c : S) : IsLowerSet {s : S | atOrBelow c s}

Marking the non-prominent end is anti-monotone: a lower set, any scale.