Core/Scales/Comparison.lean — reified degree comparison

Comparison reifies the five ways a measured value relates to a threshold — =, ≥, >, ≤, < — as data (cf. core Ordering, reified for compare). It is the shared, theory-neutral primitive behind numeral modifiers, measure phrases, and (the measure-derived case of) gradable comparatives, per the joint degree-semantic treatment of [Ken15] and [Ret14].

It interprets two ways, both bottoming out in mathlib's order API so downstream proofs reduce into Set.mem_Ici & friends rather than a bespoke lemma set:

• Comparison.rel — the order relation ([kennedy-2015]'s REL).
• Comparison.interval — the order-interval (Set.Ici/Ioi/Iic/Iio/{·}).
• Comparison.over μ n — the predication μ ⁻¹' (c.interval n): the entities whose measure lands in the interval. Bare cardinals are over .eq id, measure phrases over c μ for a DimensionedMeasure, classifier counting over .eq (atom-count).
• Comparison.overSet μ Δ — the set-standard generalization μ ⁻¹' (c.bounds Δ): the entities whose measure bounds the whole standard set Δ. The point predication over is the singleton case (overSet_singleton); this is the order-theoretic core of [Hoe83]'s S-comparative, with the binary NP-comparative its singleton face.

Main declarations

• Core.Order.Comparison — the reified comparison.
• Comparison.isStrict — Class A (>,<) vs. non-strict (=,≥,≤).
• Comparison.over / Comparison.overSet — point- and set-standard predications.
• Comparison.boundary_mem — Class A/B as interval-endpoint membership.

inductive Core.Order.Comparison : Type

[Ken15]'s REL reified: the relation a degree modifier draws between a measured value and a threshold.

• eq : Comparison

  Exact / bare: μ x = n.

• ge : Comparison

  "At least n": μ x ≥ n.

• gt : Comparison

  "More than n": μ x > n.

• le : Comparison

  "At most n": μ x ≤ n.

• lt : Comparison

  "Fewer than n": μ x < n.

@[implicit_reducible]

instance Core.Order.instDecidableEqComparison : DecidableEq Comparison

Equations

• Core.Order.instDecidableEqComparison x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Order.instReprComparison : Repr Comparison

Equations

• Core.Order.instReprComparison = { reprPrec := Core.Order.instReprComparison.repr }

def Core.Order.instReprComparison.repr : Comparison → ℕ → Std.Format

Equations

• Core.Order.instReprComparison.repr Core.Order.Comparison.eq prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.eq")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.ge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.ge")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.gt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.gt")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.le prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.le")).group prec✝
• Core.Order.instReprComparison.repr Core.Order.Comparison.lt prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Order.Comparison.lt")).group prec✝

@[implicit_reducible]

instance Core.Order.instInhabitedComparison : Inhabited Comparison

Equations

• Core.Order.instInhabitedComparison = { default := Core.Order.instInhabitedComparison.default }

def Core.Order.Comparison.isStrict : Comparison → Prop

Strict (Class A: >, <) vs. non-strict (bare =, Class B ≥, ≤). The modifier-level Class A/B split ([GN07], [Nou10]) is isStrict restricted to the four modified forms.

Equations

• Core.Order.Comparison.gt.isStrict = True
• Core.Order.Comparison.lt.isStrict = True
• x✝.isStrict = False

@[implicit_reducible]

instance Core.Order.instDecidablePredComparisonIsStrict : DecidablePred Comparison.isStrict

Equations

• One or more equations did not get rendered due to their size.

def Core.Order.Comparison.rel {α : Type u_1} [Preorder α] : Comparison → α → α → Prop

The order relation a Comparison stands for.

Equations

• Core.Order.Comparison.eq.rel = fun (x1 x2 : α) => x1 = x2
• Core.Order.Comparison.ge.rel = fun (x1 x2 : α) => x1 ≥ x2
• Core.Order.Comparison.gt.rel = fun (x1 x2 : α) => x1 > x2
• Core.Order.Comparison.le.rel = fun (x1 x2 : α) => x1 ≤ x2
• Core.Order.Comparison.lt.rel = fun (x1 x2 : α) => x1 < x2

def Core.Order.Comparison.interval {α : Type u_1} [Preorder α] : Comparison → α → Set α

The order-interval a comparison selects, in mathlib terms: {n} / [n,∞) / (n,∞) / (-∞,n] / (-∞,n).

Equations

• Core.Order.Comparison.eq.interval = fun (n : α) => {n}
• Core.Order.Comparison.ge.interval = Set.Ici
• Core.Order.Comparison.gt.interval = Set.Ioi
• Core.Order.Comparison.le.interval = Set.Iic
• Core.Order.Comparison.lt.interval = Set.Iio

def Core.Order.Comparison.over {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (n : α) : Set E

The unifying predication: the entities whose measure μ lands in the comparison's interval. The measure varies — id for bare cardinals, a dimensional DimensionedMeasure for measure phrases, an atom-count for classifiers.

Equations

• c.over μ n = μ ⁻¹' c.interval n

@[simp]

theorem Core.Order.Comparison.mem_interval {α : Type u_1} [Preorder α] (c : Comparison) (a n : α) : a ∈ c.interval n ↔ c.rel a n

@[simp]

theorem Core.Order.Comparison.mem_over {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (n : α) (x : E) : x ∈ c.over μ n ↔ c.rel (μ x) n

@[implicit_reducible]

instance Core.Order.Comparison.relDecidable {α : Type u_1} [Preorder α] [DecidableEq α] [DecidableLE α] [DecidableLT α] (c : Comparison) (a n : α) : Decidable (c.rel a n)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Order.Comparison.overDecidable {E : Type u_1} {α : Type u_2} [Preorder α] [DecidableEq α] [DecidableLE α] [DecidableLT α] (c : Comparison) (μ : E → α) (n : α) (x : E) : Decidable (x ∈ c.over μ n)

Equations

• c.overDecidable μ n x = decidable_of_iff (c.rel (μ x) n) ⋯

@[simp]

theorem Core.Order.Comparison.boundary_mem {α : Type u_1} [Preorder α] (c : Comparison) (n : α) : n ∈ c.interval n ↔ ¬c.isStrict

Class A/B is interval-endpoint membership. A non-strict comparison (bare =, Class B ≥/≤) keeps the boundary n; a strict one (Class A >/<) drops it — the whole Class A/B distinction ([GN07], [Nou10]) in one lemma.

Set-standard comparison

The than-clause of a comparative supplies not a point but a set of degrees. Comparison.bounds lifts Comparison.interval from a point n to a standard set Δ — the (strict) upper/lower bounds matching the comparison's relation — and Comparison.overSet is the corresponding measure-pullback predication. The point predication over is exactly the singleton case (overSet_singleton).

def Core.Order.Comparison.bounds {α : Type u_1} [Preorder α] : Comparison → Set α → Set α

The standard-set a comparison imposes: the bounds of Δ matching the comparison's relation (upperBounds/strictUpperBounds/… per case). Generalizes Comparison.interval from a point n (≡ {n}) to a standard set Δ.

Equations

• Core.Order.Comparison.eq.bounds = fun (Δ : Set α) => {x : α | ∀ a ∈ Δ, x = a}
• Core.Order.Comparison.ge.bounds = upperBounds
• Core.Order.Comparison.gt.bounds = strictUpperBounds
• Core.Order.Comparison.le.bounds = lowerBounds
• Core.Order.Comparison.lt.bounds = strictLowerBounds

def Core.Order.Comparison.overSet {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (Δ : Set α) : Set E

Set-standard predication: the entities whose measure bounds the whole standard set Δ. The set-standard generalization of Comparison.over and the order-theoretic core of [Hoe83]'s S-comparative; the binary NP-comparative is the singleton case (overSet_singleton).

Equations

• c.overSet μ Δ = μ ⁻¹' c.bounds Δ

theorem Core.Order.Comparison.bounds_singleton {α : Type u_1} [Preorder α] (c : Comparison) (n : α) : c.bounds {n} = c.interval n

bounds at a singleton standard collapses to the point interval.

@[simp]

theorem Core.Order.Comparison.mem_overSet {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (Δ : Set α) (x : E) : x ∈ c.overSet μ Δ ↔ μ x ∈ c.bounds Δ

@[simp]

theorem Core.Order.Comparison.overSet_singleton {E : Type u_1} {α : Type u_2} [Preorder α] (c : Comparison) (μ : E → α) (n : α) : c.overSet μ {n} = c.over μ n

The NP ⊂ S bridge: the set-standard predication at a singleton standard is the point predication. Makes [Hoe83]'s NP↔S equivalence definitional.

Threshold and measure monotonicity

The shared content of every threshold-semantics face (Kennedy positive form, CSW positive region, credence thresholds): raising a non-strict lower threshold shrinks the extension, raising the measure preserves membership, and on a linear order the positive/negative poles are complementary and comparison reduces to a separating threshold (Klein).

theorem Core.Order.Comparison.antitone_ge_over {E : Type u_1} {α : Type u_2} [Preorder α] (μ : E → α) : Antitone (ge.over μ)

Raising an at least threshold shrinks the extension.

theorem Core.Order.Comparison.antitone_gt_over {E : Type u_1} {α : Type u_2} [Preorder α] (μ : E → α) : Antitone (gt.over μ)

Raising a more than threshold shrinks the extension.

theorem Core.Order.Comparison.monotone_le_over {E : Type u_1} {α : Type u_2} [Preorder α] (μ : E → α) : Monotone (le.over μ)

Raising an at most threshold grows the extension.

theorem Core.Order.Comparison.monotone_lt_over {E : Type u_1} {α : Type u_2} [Preorder α] (μ : E → α) : Monotone (lt.over μ)

Raising a less than threshold grows the extension.

theorem Core.Order.Comparison.mem_ge_over_of_le {E : Type u_1} {α : Type u_2} [Preorder α] (μ : E → α) {θ : α} {x y : E} (hx : x ∈ ge.over μ θ) (hxy : μ x ≤ μ y) : y ∈ ge.over μ θ

Membership in an at least extension transports up the measure.

theorem Core.Order.Comparison.mem_ge_over_iff_not_mem_lt_over {E : Type u_1} {α : Type u_2} [LinearOrder α] (μ : E → α) {θ : α} {x : E} : x ∈ ge.over μ θ ↔ x ∉ lt.over μ θ

Polarity duality: clearing the threshold is exactly not falling below it.

theorem Core.Order.Comparison.lt_iff_separating_threshold {E : Type u_1} {α : Type u_2} [LinearOrder α] (μ : E → α) {x y : E} : μ y < μ x ↔ ∃ (θ : α), x ∈ ge.over μ θ ∧ y ∉ ge.over μ θ

The Klein reduction: strict comparison holds iff some threshold separates the two measures.

Order-Sensitive MAX ([Ret26])

Scale-sensitive maximality operator

[Ret26]: MAX_c(X) picks the element(s) of X that c-dominate all other members. For the < scale (.lt) this is the GLB (earliest / smallest), for > (.gt) the LUB (latest / largest). The same operator underlies both temporal connectives (before/after) and degree comparatives.

• Rett, J. (2026). Semantic ambivalence and expletive negation. Ms.

def Core.Order.maxOnScale {α : Type u_1} [Preorder α] (c : Comparison) (X : Set α) : Set α

Order-sensitive maximality ([Ret26], def. 1): MAX_c(X) = { x ∈ X | ∀ x' ∈ X, x' ≠ x → c.rel x x' }. The dominance relation is the reified Core.Order.Comparison rather than a lawless R : α → α → Prop — removing the "fake generality" of an unconstrained relation parameter. Each concrete c (.lt, .gt, .ge, …) names an order relation via Comparison.rel.

Equations

• Core.Order.maxOnScale c X = {x : α | x ∈ X ∧ ∀ x' ∈ X, x' ≠ x → c.rel x x'}

theorem Core.Order.maxOnScale_singleton {α : Type u_1} [Preorder α] (c : Comparison) (x : α) : maxOnScale c {x} = {x}

MAX on a singleton is that singleton: MAX_c({x}) = {x}. The universal quantifier is vacuously satisfied, so this holds for any c.

theorem Core.Order.maxOnScale_lt_closedInterval {α : Type u_1} [LinearOrder α] (s f : α) (hsf : s ≤ f) : maxOnScale Comparison.lt {x : α | s ≤ x ∧ x ≤ f} = {s}

MAX₍<₎ on a closed interval {x | s ≤ x ∧ x ≤ f} is the singleton {s}. The minimum element s R-dominates all others on the < scale. Dual: MAX₍>₎ on the same interval is {f}.

theorem Core.Order.maxOnScale_gt_closedInterval {α : Type u_1} [LinearOrder α] (s f : α) (hsf : s ≤ f) : maxOnScale Comparison.gt {x : α | s ≤ x ∧ x ≤ f} = {f}

MAX₍>₎ on a closed interval {x | s ≤ x ∧ x ≤ f} is the singleton {f}. The maximum element R-dominates all others on the > scale.

def Core.Order.isAmbidirectional {α : Type u_1} (f : Set α → Prop) (B : Set α) : Prop

A scalar construction f is ambidirectional iff applying f to a set B and to its complement Bᶜ yields the same result, because MAX picks the same informative boundary from both. This is the mechanism behind expletive negation licensing: when f(B) ↔ f(Bᶜ), negating B is truth-conditionally vacuous.

Equations

• Core.Order.isAmbidirectional f B = (f B ↔ f Bᶜ)

theorem Core.Order.maxOnScale_atLeast_singleton {W : Type u_1} {α : Type u_2} [LinearOrder α] (μ : W → α) (w : W) : maxOnScale Comparison.ge {d : α | d ≤ μ w} = {μ w}

Bridge: maxOnScale .ge applied to the "at least" degree set {d | d ≤ μ(w)} yields {μ(w)} — the singleton containing the true value. This connects the relational MAX to IsMaxInf.

The convention: maxOnScale c X picks elements x ∈ X with c.rel x x' for all other x'. With c = .ge, this picks elements ≥ all others, i.e., the maximum.

theorem Core.Order.maxOnScale_ge_atMost {α : Type u_1} [LinearOrder α] (b : α) : maxOnScale Comparison.ge {d : α | d ≤ b} = {b}

MAX₍≥₎ on {d | d ≤ b} is {b}. Corollary of maxOnScale_atLeast_singleton with μ = id. Used by the comparative boundary theorems.

theorem Core.Order.maxOnScale_ge_eq {α : Type u_1} [Preorder α] (X : Set α) : maxOnScale Comparison.ge X = {x : α | IsGreatest X x}

Grounding: MAX₍≥₎ is mathlib's IsGreatest (the x' = x case of the dominance quantifier holds by reflexivity).