Bounded-scale theorems + maxOnScale

[Ret26]

Two clusters of theorems:

1. Typeclass-driven licensing: open_no_upward_ceiling, upperBound_admits_optimum, etc. — show how Mathlib boundedness typeclasses (NoMaxOrder, OrderTop, OrderBot, NoMinOrder) interact with monotonicity to admit/block optima.

2. Order-sensitive maximality: maxOnScale c X, isAmbidirectional — Rett 2026's MAX operator (the dominance direction is the reified Comparison) + ambidirectionality predicate.

theorem Degree.open_no_upward_ceiling {α : Type u_1} [LinearOrder α] [NoMaxOrder α] (P : α → Prop) (hMono : ∀ (x y : α), x ≤ y → P x → P y) (x : α) (hx : P x) : ∃ (y : α), x < y ∧ P y

On a scale with no maximum (NoMaxOrder), any upward monotone family that is nontrivial (i.e., some value yields a different set of worlds than another) cannot have a ceiling: for any candidate optimum, a strictly larger value exists.

This is the typeclass-level counterpart of the data-level prediction ¬ Boundedness.open_.IsLicensed: open scales block degree modification and TIA licensing because no element is maximal.

Proof sketch: For any x, NoMaxOrder gives y > x. If P is upward monotone, P x w → P y w, so x is never the unique optimum.

theorem Degree.upperBound_admits_optimum {α : Type u_1} [LinearOrder α] [OrderTop α] (h_nontrivial : ∃ (x : α), x ≠ ⊤) : ∃ (P : α → Prop), (∀ (x y : α), x ≤ y → P x → P y) ∧ ¬∀ (x y : α), P x ↔ P y

On a scale with a top element (OrderTop), the predicate · = ⊤ is upward monotone (vacuously — only ⊤ satisfies it) and nonconstant (on nontrivial types). This witnesses that upper-bounded scales admit an optimum.

Proof sketch: ⊤ satisfies · = ⊤, and for any x < ⊤, x does not. So the family is not constant → AdmitsOptimum holds.

theorem Degree.lowerBound_admits_optimum {α : Type u_1} [LinearOrder α] [OrderBot α] (h_nontrivial : ∃ (x : α), x ≠ ⊥) : ∃ (P : α → Prop), (∀ (x y : α), x ≤ y → P y → P x) ∧ ¬∀ (x y : α), P x ↔ P y

On a scale with a bottom element (OrderBot), the predicate · = ⊥ is downward monotone and nonconstant (on nontrivial types). This witnesses that lower-bounded scales admit an optimum.

theorem Degree.open_scale_unlicensable {α : Type u_1} [LinearOrder α] [NoMaxOrder α] [NoMinOrder α] (h : ∃ (x : α) (y : α), x ≠ y) : ∃ (P : α → Prop), (∀ (x y : α), x ≤ y → P x → P y) ∧ (¬∀ (x y : α), P x ↔ P y) ∧ ∀ (x : α), P x → ∃ (y : α), x < y ∧ P y

Boundedness is necessary for licensing: on a scale with no upper bound and no lower bound, there exists a monotone family with no optimum. Contrapositive: if every monotone family admits an optimum, the scale has a bound.

Order-theoretic boundedness primitives

Whether a scale has a greatest degree, stated structurally via mathlib's OrderTop / NoMaxOrder mixins rather than as stored data — the order-theoretic facts that telicity and licensing derive from (see Semantics/Gradability/Dimension.lean and Studies/KennedyLevin2008.lean).

def Degree.HasGreatest (β : Type u_2) [LE β] : Prop

"Has a greatest element", as a proposition — usable when an OrderTop instance is not in hand (e.g. under a quantifier).

Equations

• Degree.HasGreatest β = ∃ (m : β), ∀ (x : β), x ≤ m

theorem Degree.hasGreatest_of_orderTop {β : Type u_2} [LE β] [OrderTop β] : HasGreatest β

theorem Degree.not_hasGreatest_of_noMaxOrder {β : Type u_2} [Preorder β] [NoMaxOrder β] : ¬HasGreatest β

theorem Degree.not_noMaxOrder_of_orderTop {β : Type u_2} [Preorder β] [OrderTop β] : ¬NoMaxOrder β

OrderTop and NoMaxOrder are mutually exclusive — the rigorous sense in which a scale either has a greatest degree or does not. (Not in Mathlib.)

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 Degree.maxOnScale {α : Type u_2} [Preorder α] (c : Core.Order.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

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

theorem Degree.maxOnScale_singleton {α : Type u_2} [Preorder α] (c : Core.Order.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 Degree.maxOnScale_lt_closedInterval {α : Type u_2} [LinearOrder α] (s f : α) (hsf : s ≤ f) : maxOnScale Core.Order.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 Degree.maxOnScale_gt_closedInterval {α : Type u_2} [LinearOrder α] (s f : α) (hsf : s ≤ f) : maxOnScale Core.Order.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 Degree.isAmbidirectional {α : Type u_2} (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

• Degree.isAmbidirectional f B = (f B ↔ f Bᶜ)

theorem Degree.maxOnScale_atLeast_singleton {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (w : W) : maxOnScale Core.Order.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 Degree.maxOnScale_ge_atMost {α : Type u_1} [LinearOrder α] (b : α) : maxOnScale Core.Order.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.