Degree predicates + monotonicity

[FH06b] [Ken15] [GN07] [Nou10] [Par87]

Predicate transformers over a measure function μ : W → α:

• IsUpwardMonotone / IsDownwardMonotone / IsConstant / AdmitsOptimum
• typeLower (Partee 1987 existential lowering)
• monotonicity / anti-Horn-scale lemmas about the Core.Order.Comparison.over degree predicates (general)

The five degree predicates ("exactly", "at least", "more than", "at most", "less than") are Core.Order.Comparison.{eq,ge,gt,le,lt}.over μ directly: the reified Core.Order.Comparison IS the canonical scale-comparison primitive, so there is no separate named family. c.over μ n is a Set W; w ∈ c.over μ n ↔ c.rel (μ w) n (Comparison.mem_over), and c.rel unfolds to the order relation per case.

This file is part of the Phase A decomposition of the legacy Core/Scales/Scale.lean dumping ground (master plan v4).

def Degree.IsUpwardMonotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) : Prop

A family of propositions indexed by scale values is upward monotone (entailments go from smaller to larger values). Kennedy: "tall" — if x is tall, x is tall-or-more. Rouillard: E-TIA with telic VP — if event fits in n days, it fits in m ≥ n days.

Equations

• Degree.IsUpwardMonotone P = ∀ (x y : α), x ≤ y → ∀ (w : W), P x w → P y w

def Degree.IsDownwardMonotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) : Prop

A family is downward monotone: entailments go from larger to smaller. Rouillard: E-TIA with atelic VP — if sick during n-day time, sick during m ≤ n day time.

Equations

• Degree.IsDownwardMonotone P = ∀ (x y : α), x ≤ y → ∀ (w : W), P y w → P x w

def Degree.IsConstant {α : Type u_1} {W : Type u_2} (P : α → W → Prop) : Prop

A family is constant: every value yields the same proposition. This is information collapse — no value is more informative than another. Occurs when a family is both upward and downward monotone.

Equations

• Degree.IsConstant P = ∀ (x y : α) (w : W), P x w ↔ P y w

theorem Degree.bimonotone_constant {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) (hUp : IsUpwardMonotone P) (hDown : IsDownwardMonotone P) : IsConstant P

If P is both upward and downward monotone, it is constant.

def Degree.AdmitsOptimum {α : Type u_1} {W : Type u_2} (P : α → W → Prop) : Prop

Informativity licensing: a scale admits a well-defined optimum iff it is NOT constant. When the family is constant (information collapse), no grammatical element operating on that scale is felicitous.

This is the abstract pattern shared by:

• Kennedy's Interpretive Economy: degree modifiers require non-trivial scale contribution
• Rouillard's MIP: TIA numerals require maximally informative values

Equations

• Degree.AdmitsOptimum P = ¬Degree.IsConstant P

theorem Degree.bimonotone_no_optimum {α : Type u_1} [LinearOrder α] {W : Type u_2} (P : α → W → Prop) (hUp : IsUpwardMonotone P) (hDown : IsDownwardMonotone P) : ¬AdmitsOptimum P

Bimonotone families do not admit an optimum: if a family is both upward and downward monotone, it collapses to a constant and no element is maximally informative. This is the abstract core of why open-scale degree modification and atelic-VP E-TIAs are both blocked.

The cross-world entailment-based IsMaxInf (Fox 2007 / vFFI 2014 / Beck-Rullmann 1999 / Rouillard 2026) is linguistic substrate, not pure order theory — it lives in Semantics/Entailment/Extremum.lean. The per-world specialization is just IsLeast {y | P y w} x from mathlib (Mathlib.Order.Bounds.Defs); the per-world↔cross-world bridge under monotonicity is mathlib's MonotoneOn.map_isLeast family (Mathlib.Order.Bounds.Image).

theorem Degree.closed_isLicensed : Core.Order.Boundedness.closed.IsLicensed

Closed scales predict licensing (Kennedy: "completely full" ✓; Rouillard: telic VP E-TIA ✓).

theorem Degree.open_notLicensed : ¬Core.Order.Boundedness.open_.IsLicensed

Open scales predict blocking (Kennedy: "??completely tall"; Rouillard: atelic VP E-TIA ✗).

Degree properties as Comparison.over

The five degree predicates covering all comparison relations are Core.Order.Comparison.{eq,ge,gt,le,lt}.over μ directly — there is no separate named family. c.over μ d : Set W, with w ∈ c.over μ d ↔ c.rel (μ w) d (Comparison.mem_over). These are the building blocks for the named numeral meanings (Semantics.Numerals.atLeastMeaning etc.) and degree question semantics.

• Comparison.ge.over μ: closed ≥, always has max⊨
• Comparison.gt.over μ: open >, fails on dense scales
• Comparison.eq.over μ: equality =, trivially has max⊨
• Comparison.le.over μ: closed ≤
• Comparison.lt.over μ: open <

The key divergence: on ℕ, > collapses to ≥ with successor, so both have HasMaxInf. On dense scales, > yields an open set with no max⊨. This is the UDM prediction ([FH06b]).

theorem Degree.geOver_downMono {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : IsDownwardMonotone (Core.Order.Comparison.ge.over μ)

"At least" is downward monotone: weaker thresholds are easier to satisfy.

theorem Degree.gtOver_downMono {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : IsDownwardMonotone (Core.Order.Comparison.gt.over μ)

"More than" is downward monotone: weaker thresholds are easier to satisfy.

theorem Degree.gtOver_eq_geOver_succ {W : Type u_2} (μ : W → ℕ) (m : ℕ) (w : W) : w ∈ Core.Order.Comparison.gt.over μ m ↔ w ∈ Core.Order.Comparison.ge.over μ (m + 1)

On ℕ, > collapses to ≥ with successor: "more than m" ↔ "at least m+1". This is the discrete equivalence that density breaks.

IsMaxInf-flavored consequences of these degree predicates (atLeast_hasMaxInf, moreThan_noMaxInf, isMaxInf_atLeast_iff_eq, moreThan_nat_hasMaxInf) live in Semantics/Entailment/Extremum.lean since they depend on the linguistic-substrate IsMaxInf predicate.

Existential lowering: exact → "at least"

[Par87]'s BE + iota + existential closure, applied to a degree property: from an exact reading exact d w ("the measure equals d"), existentially close to ∃ d' ≥ d, exact d' w. On any reflexive linear order this collapses to Comparison.ge.over μ d w — witness d' := μ w.

This is the formal content of [Ken15]'s "de-Fregean" derivation of the lower-bound numeral reading from the exact reading. The collapse generalizes Numeral type-shifting to arbitrary scales.

def Degree.typeLower {α : Type u_1} [LinearOrder α] {W : Type u_2} (exact : α → W → Prop) (d : α) (w : W) : Prop

Existentially lower an exact-style degree property to its lower-bound counterpart: there exists some d' ≥ d such that the exact property holds at d'.

Equations

• Degree.typeLower exact d w = ∃ d' ≥ d, exact d' w

theorem Degree.typeLower_eqOver_iff {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) : typeLower (fun (d' : α) (w : W) => w ∈ Core.Order.Comparison.eq.over μ d') d w ↔ w ∈ Core.Order.Comparison.ge.over μ d

Type-shift collapse: existentially lowering the exact property Comparison.eq.over μ yields the lower-bound property Comparison.ge.over μ.

A unified GQ denotation via Core.Order.Comparison

[Ken15] proposes a single denotation for modified and unmodified numerals: λP. max{d | #P ≥ d} REL m, where the only parameter distinguishing surface forms is the relation REL ∈ {=, ≥, >, ≤, <}.

Specialised to a property of the form Comparison.ge.over μ, the maximum degree satisfying Comparison.ge.over μ d w is μ w itself, so Kennedy's denotation collapses to c.rel (μ w) m — i.e. w ∈ c.over μ m (Comparison.mem_over). The reified Core.Order.Comparison (in Comparison.lean) IS this canonical comparison primitive; it selects which rel/interval to use, and the Class A vs Class B distinction ([GN07], [Nou10]) is its Comparison.boundary_mem (non-strict comparisons keep the endpoint).

Why exact bare numerals are not part of a Horn scale

[Ken15] argues that bare numerals (under their exact reading) are not monotone in their numerical argument — neither upward nor downward — so they fail the Horn-scale criterion. The classic Horn scale ⟨1, 2, 3, …⟩ presupposes upward monotonicity; the dual scale ⟨…, 3, 2, 1⟩ presupposes downward monotonicity. Kennedy's unified GQ accommodates both modifier directions without needing a Horn scale at all.

The lemmas below state the failure-of-monotonicity and weakness-vs-exact results purely in terms of Comparison.{eq,ge,gt}.over — independent of any specific scale. The Nat-specific results in Semantics/Numerals/Basic.lean are immediate corollaries.

theorem Degree.gtOver_disjoint_eqOver {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) : ¬(w ∈ Core.Order.Comparison.eq.over μ d ∧ w ∈ Core.Order.Comparison.gt.over μ d)

"More than d" and "exactly d" are disjoint (general).

theorem Degree.ltOver_disjoint_eqOver {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) : ¬(w ∈ Core.Order.Comparison.eq.over μ d ∧ w ∈ Core.Order.Comparison.lt.over μ d)

"Less than d" and "exactly d" are disjoint (general).

theorem Degree.eqOver_imp_geOver {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) : w ∈ Core.Order.Comparison.eq.over μ d → w ∈ Core.Order.Comparison.ge.over μ d

Bare exact meaning entails "at least" (general half of Class B inclusion).

theorem Degree.eqOver_imp_leOver {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (d : α) (w : W) : w ∈ Core.Order.Comparison.eq.over μ d → w ∈ Core.Order.Comparison.le.over μ d

Bare exact meaning entails "at most" (general; symmetric to above).

theorem Degree.geOver_strictly_weaker_than_eqOver {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) {d d' : α} (hlt : d < d') {w : W} (hμ : μ w = d') : w ∈ Core.Order.Comparison.ge.over μ d ∧ w ∉ Core.Order.Comparison.eq.over μ d

"At least d" is strictly weaker than "exactly d" (general). Given a witness world w with μ w = d' where d < d', "at least d" holds but "exactly d" fails.

theorem Degree.eqOver_not_upward_monotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) {d d' : α} (hne : d ≠ d') (hle : d ≤ d') {w : W} (hμ : μ w = d) : ¬∀ (x y : α), x ≤ y → w ∈ Core.Order.Comparison.eq.over μ x → w ∈ Core.Order.Comparison.eq.over μ y

Exact equality is not upward-monotone (general). Given two distinct boundary values d ≤ d' and a witness world with μ w = d, the universal "if exact at d then exact at d'" fails — μ w cannot equal both.

theorem Degree.eqOver_not_downward_monotone {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) {d d' : α} (hne : d ≠ d') (hle : d' ≤ d) {w : W} (hμ : μ w = d) : ¬∀ (x y : α), y ≤ x → w ∈ Core.Order.Comparison.eq.over μ x → w ∈ Core.Order.Comparison.eq.over μ y

Exact equality is not downward-monotone (general). Symmetric to above.

theorem Degree.distinct_no_universal_witness {α : Type u_2} (k₁ k₂ : α) (hne : k₁ ≠ k₂) : ¬∃ (x : α), ∀ (k : α), k = k₁ ∨ k = k₂ → x = k

Universal closure (the alternative to existential closure) is unsatisfiable when the closure range contains two distinct values: no single x can equal two different ks. This rules out the universal-closure reading of Partee's iota generally.

theorem Degree.leOver_upMono {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : IsUpwardMonotone (Core.Order.Comparison.le.over μ)

"At most" is upward monotone: larger thresholds are easier to satisfy.

IsMaxInf-flavored consequences of "at most" (atMost_hasMaxInf, isMaxInf_atMost_iff_eq) live in Semantics/Entailment/Extremum.lean.