Core/Scales/Bounds.lean — bounded-scale theorems + maxOnScale

@cite{rett-2026}

Two clusters of theorems:

1. Typeclass-driven licensing (§4 of legacy Scale.lean): 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 (§6b of legacy Scale.lean): maxOnScale R X, IsMaxDetermined, isAmbidirectional — Rett 2026's relation-parameterized MAX operator + ambidirectionality scaffolding.

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

theorem Core.Scale.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 = false: 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 Core.Scale.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 Core.Scale.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 Core.Scale.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.

Scale-sensitive maximality operator

@cite{rett-2026}: MAX_R(X) picks the element(s) of X that R-dominate all other members. For the < scale this is the GLB (earliest / smallest), for > 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.Scale.maxOnScale {α : Type u_2} (R : α → α → Prop) (X : Set α) : Set α

Order-sensitive maximality (@cite{rett-2026}, def. 1): MAX_R(X) = { x ∈ X | ∀ x' ∈ X, x' ≠ x → R x x' }. Domain-general over any relation R and set X.

Equations

• Core.Scale.maxOnScale R X = {x : α | x ∈ X ∧ ∀ x' ∈ X, x' ≠ x → R x x'}

theorem Core.Scale.maxOnScale_singleton {α : Type u_2} (R : α → α → Prop) (x : α) : maxOnScale R {x} = {x}

MAX on a singleton is that singleton: MAX_R({x}) = {x}. The universal quantifier is vacuously satisfied.

theorem Core.Scale.maxOnScale_lt_closedInterval {α : Type u_2} [LinearOrder α] (s f : α) (hsf : s ≤ f) : maxOnScale (fun (x1 x2 : α) => x1 < x2) {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.Scale.maxOnScale_gt_closedInterval {α : Type u_2} [LinearOrder α] (s f : α) (hsf : s ≤ f) : maxOnScale (fun (x1 x2 : α) => x1 > x2) {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.Scale.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

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

def Core.Scale.IsMaxDetermined {α : Type u_2} (R : α → α → Prop) (f : Set α → Prop) : Prop

A predicate f is MAX_R-determined iff its value depends only on maxOnScale R of its argument: any two sets with the same MAX_R yield the same f-verdict. The before/until/comparative theorems all establish exactly this: before relates A to MAX₍<₎ of B, the comparative than-clause to MAX₍≥₎ of the degree set, etc.

Equations

• Core.Scale.IsMaxDetermined R f = ∀ (B₁ B₂ : Set α), Core.Scale.maxOnScale R B₁ = Core.Scale.maxOnScale R B₂ → (f B₁ ↔ f B₂)

theorem Core.Scale.ambidirectional_of_shared_max {α : Type u_2} {R : α → α → Prop} (f : Set α → Prop) (hf : IsMaxDetermined R f) (B : Set α) (hshared : maxOnScale R B = maxOnScale R Bᶜ) : isAmbidirectional f B

Shared informative bound ⇒ ambidirectionality. The general template behind Rett's typology: if a construction is MAX_R-determined and B and Bᶜ share their MAX_R-bound, then the construction is truth-conditionally insensitive to negation of B.

Each per-construction ambidirectionality theorem in the library is an instance of this template — they prove the shared-bound side condition for a specific f and a class of B's, then this lemma packages the result. See Semantics.Tense.TemporalConnectives.before_preEvent_ambidirectional for the canonical instance.

theorem Core.Scale.not_ambidirectional_of_distinct_max_separated {α : Type u_2} {R : α → α → Prop} (f : Set α → Prop) (B : Set α) (hsep : ∀ (B₁ B₂ : Set α), maxOnScale R B₁ ≠ maxOnScale R B₂ → ¬(f B₁ ↔ f B₂)) (hdiff : maxOnScale R B ≠ maxOnScale R Bᶜ) : ¬isAmbidirectional f B

Converse: an ambidirectional construction must share its MAX_R bound between B and Bᶜ — but only when MAX_R alone witnesses the distinction. Stated as a contrapositive to make the empirical content explicit: if MAX_R differs between B and Bᶜ but the construction cannot tell them apart by any other means (i.e. MAX_R-determined), then the construction is non-ambidirectional. The full converse requires assuming f separates sets with distinct MAX_R values, so we instead expose this as a derived fact only under that assumption.

theorem Core.Scale.maxOnScale_atLeast_singleton {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (w : W) : maxOnScale (fun (x1 x2 : α) => x1 ≥ x2) {d : α | d ≤ μ w} = {μ w}

Bridge: maxOnScale (· ≥ ·) 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 R X picks elements x ∈ X with R x x' for all other x'. With R = (· ≥ ·), this picks elements ≥ all others, i.e., the maximum.

theorem Core.Scale.maxOnScale_ge_atMost {α : Type u_1} [LinearOrder α] (b : α) : maxOnScale (fun (x1 x2 : α) => x1 ≥ x2) {d : α | d ≤ b} = {b}

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