Schwarzschild's Interval Semantics

[Sch05] [Sch08f] [SW02a]

[Sch08f] reifies degrees as intervals on a scale rather than points: "tall" is [⊥, μ x], "short" is [μ x, ⊤], and degree morphology manipulates these intervals. Intervals are mathlib's NonemptyInterval (the same type the time-interval substrate uses). The comparative asserts the matrix interval extends past the standard's; subcomparatives compare intervals from commensurable scales; differentials specify the interval gap.

Main declarations

• positiveInterval / negativeInterval — the [⊥, μ x] / [μ x, ⊤] extents.
• intervalComparative — upper-bound comparison; is the consensus comparativeSem (interval_eq_comparativeSem).
• subcomparative — cross-dimensional comparison ([SW02a]).

Intervals as degrees

def Degree.Intervals.positiveInterval {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) : NonemptyInterval D

The positive interval for x: [⊥, μ x] — the extent to which x is tall.

Equations

• Degree.Intervals.positiveInterval μ x = { fst := ⊥, snd := μ x, fst_le_snd := ⋯ }

def Degree.Intervals.negativeInterval {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) : NonemptyInterval D

The negative interval for x: [μ x, ⊤] — the extent to which x is short ([Bur07] §4: ⟦short⟧ = ⟦LITTLE tall⟧, which inverts the positive interval).

Equations

• Degree.Intervals.negativeInterval μ x = { fst := μ x, snd := ⊤, fst_le_snd := ⋯ }

Comparative as interval comparison

def Degree.Intervals.intervalComparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (a b : Entity) : Prop

Schwarzschild's comparative: the matrix interval extends past the standard's, i.e. its upper bound is greater.

Equations

• Degree.Intervals.intervalComparative μ a b = ((Degree.Intervals.positiveInterval μ b).toProd.2 < (Degree.Intervals.positiveInterval μ a).toProd.2)

theorem Degree.Intervals.interval_eq_comparativeSem {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (a b : Entity) : intervalComparative μ a b ↔ comparativeSem μ a b Core.Order.ScalePolarity.positive

Schwarzschild's interval comparative is the consensus point comparative ([Ken99], [Ret26]): for positive intervals [⊥, μ x], comparing upper bounds is comparing degrees.

Differential comparatives

def Degree.Intervals.differentialInterval {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (a b : Entity) (h : μ b ≤ μ a) : NonemptyInterval D

The differential interval [μ b, μ a] — the gap between standard and matrix ("A is d-much taller than B" specifies its extent).

Equations

• Degree.Intervals.differentialInterval μ a b h = { fst := μ b, snd := μ a, fst_le_snd := h }

Subcomparatives

def Degree.Intervals.subcomparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] (μ₁ μ₂ : Entity → D) (a b : Entity) : Prop

Subcomparative ("longer than it is wide"): two commensurable scales compared in shared units ([SW02a]).

Equations

• Degree.Intervals.subcomparative μ₁ μ₂ a b = (μ₁ a > μ₂ b)

Bridge to extent functions

theorem Degree.Intervals.positiveInterval_iff_posExt {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) (d : D) : (positiveInterval μ x).toProd.1 ≤ d ∧ d ≤ (positiveInterval μ x).toProd.2 ↔ d ∈ posExt μ x

The positive interval's membership is exactly posExt: d ∈ [⊥, μ x] iff d ∈ posExt μ x. Connects Schwarzschild's intervals to the extent algebra.

Negative intervals and LITTLE

theorem Degree.Intervals.little_inverts_interval {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) : negativeInterval μ x = { fst := (positiveInterval μ x).toProd.2, snd := ⊤, fst_le_snd := ⋯ }

LITTLE inverts the positive interval [⊥, μ x] into the negative interval [μ x, ⊤] ([Bur07] §4).

theorem Degree.Intervals.negativeInterval_comparative {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (a b : Entity) : (negativeInterval μ a).toProd.1 < (negativeInterval μ b).toProd.1 ↔ μ a < μ b

"Shorter than" via negative intervals: a is shorter than b iff a's negative interval reaches further down, i.e. μ a < μ b.

theorem Degree.Intervals.negativeInterval_membership {Entity : Type u_1} {D : Type u_2} [LinearOrder D] [BoundedOrder D] (μ : Entity → D) (x : Entity) (d : D) : (negativeInterval μ x).toProd.1 ≤ d ↔ μ x ≤ d

The negative interval starts at μ x.