Core/Scales/Defs.lean — basic types

@cite{kennedy-mcnally-2005} @cite{kennedy-2007} @cite{rotstein-winter-2004} @cite{rouillard-2026}

Foundational scale-classification types used across all gradability/degree substrate. No framework-specific operators here (those live in Theories/Semantics/Gradability/).

Contents:

• Boundedness enum + hasMax/hasMin/isLicensed
• MereoTag + toBoundedness
• LicensingPipeline typeclass + universal theorem
• ScalePolarity enum

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

inductive Core.Scale.Boundedness : Type

Classification of scale boundedness. @cite{kennedy-mcnally-2005} eq (1) and @cite{kennedy-2007} §4.2 eq (59): four scale types based on which endpoints exist (independently discovered by @cite{rotstein-winter-2004}). @cite{rouillard-2026}: temporal domains have similar boundary structure (closed intervals have both bounds, open intervals lack them).

This enum is the lexical data tag for classifying scales in fragment entries and phenomena files — a role mathlib's typeclass instances cannot play (you cannot store an [OrderTop α] instance in a record field). The actual order-theoretic properties of concrete scale types are encoded via Mathlib typeclasses (OrderTop, OrderBot, NoMaxOrder, NoMinOrder); the two encodings serve different roles and both are real.

Standard-type dimension. @cite{kennedy-2007} §4.3 eq (66) (Interpretive Economy) DERIVES standard type (relative / min-absolute / max-absolute) from scale structure for open_, lowerBounded, and upperBounded. For closed, all three interpretations are licensed (see eq 67: opaque, transparent) — this enum doesn't capture that disambiguation. Fragment entries with boundedness = .closed may need a separate standardType slot if downstream theorems care about the distinction.

Open-bounded sub-distinction. @cite{kennedy-2007} fn 28: open scales can be further distinguished by whether they approach a value (e.g. 0 for cost) but don't include it, vs. completely unbounded. Not captured here.

• open_ : Boundedness
• lowerBounded : Boundedness
• upperBounded : Boundedness
• closed : Boundedness

@[implicit_reducible]

instance Core.Scale.instDecidableEqBoundedness : DecidableEq Boundedness

Equations

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

@[implicit_reducible]

instance Core.Scale.instReprBoundedness : Repr Boundedness

Equations

• Core.Scale.instReprBoundedness = { reprPrec := Core.Scale.instReprBoundedness.repr }

def Core.Scale.instReprBoundedness.repr : Boundedness → ℕ → Std.Format

Equations

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

def Core.Scale.Boundedness.hasMax : Boundedness → Bool

Does this scale have an inherent maximum?

Equations

• Core.Scale.Boundedness.upperBounded.hasMax = true
• Core.Scale.Boundedness.closed.hasMax = true
• Core.Scale.Boundedness.open_.hasMax = false
• Core.Scale.Boundedness.lowerBounded.hasMax = false

def Core.Scale.Boundedness.hasMin : Boundedness → Bool

Does this scale have an inherent minimum?

Equations

• Core.Scale.Boundedness.lowerBounded.hasMin = true
• Core.Scale.Boundedness.closed.hasMin = true
• Core.Scale.Boundedness.open_.hasMin = false
• Core.Scale.Boundedness.upperBounded.hasMin = false

def Core.Scale.Boundedness.isLicensed : Boundedness → Bool

"Any endpoint exists" predicate: returns true whenever the scale has at least one bound (max or min). An open scale returns false.

NOT @cite{kennedy-2007}'s full licensing prediction. Kennedy's actual prediction is the 4×2 modifier-class matrix in @cite{kennedy-2007} eq (61) (= @cite{kennedy-mcnally-2005} eq (15)): maximizers (completely, perfectly) require an UPPER endpoint; minimizers (slightly, partially) require a LOWER endpoint; proportional modifiers (half) require BOTH. A single Bool can't encode this — to be faithful, split into licensesMaximizer/licensesMinimizer/licensesProportional.

The current Bool is sufficient for callers that only need to distinguish "open" from "any-endpoint-exists" (e.g. Interpretive Economy gating a relative vs. absolute interpretation, @cite{kennedy-2007} §4.3, or Rouillard's MIP, @cite{rouillard-2026}). For modifier-specific licensing, consumers must consult hasMax/hasMin directly.

Equations

• Core.Scale.Boundedness.closed.isLicensed = true
• Core.Scale.Boundedness.lowerBounded.isLicensed = true
• Core.Scale.Boundedness.upperBounded.isLicensed = true
• Core.Scale.Boundedness.open_.isLicensed = false

inductive Core.Scale.MereoTag : Type

Binary mereological classification: the shared abstraction underlying all four licensing frameworks (Kennedy, Rouillard, Krifka, Zwarts).

• qua : MereoTag
• cum : MereoTag

@[implicit_reducible]

instance Core.Scale.instDecidableEqMereoTag : DecidableEq MereoTag

Equations

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

def Core.Scale.instReprMereoTag.repr : MereoTag → ℕ → Std.Format

Equations

• Core.Scale.instReprMereoTag.repr Core.Scale.MereoTag.qua prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Scale.MereoTag.qua")).group prec✝
• Core.Scale.instReprMereoTag.repr Core.Scale.MereoTag.cum prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Scale.MereoTag.cum")).group prec✝

@[implicit_reducible]

instance Core.Scale.instReprMereoTag : Repr MereoTag

Equations

• Core.Scale.instReprMereoTag = { reprPrec := Core.Scale.instReprMereoTag.repr }

def Core.Scale.MereoTag.toBoundedness : MereoTag → Boundedness

Equations

• Core.Scale.MereoTag.qua.toBoundedness = Core.Scale.Boundedness.closed
• Core.Scale.MereoTag.cum.toBoundedness = Core.Scale.Boundedness.open_

class Core.Scale.LicensingPipeline (α : Type u_1) : Type u_1

A licensing pipeline: any type whose elements can be classified into scale boundedness. Kennedy, Rouillard, Krifka, and Zwarts all instantiate this with different source types but the same target.

Core instances (Boundedness, MereoTag) live here. Domain-specific instances (Telicity, VendlerClass, PathShape, BoundaryType) live in their respective theory/bridge files.

• toBoundedness : α → Boundedness

def Core.Scale.LicensingPipeline.isLicensed {α : Type u_1} [LicensingPipeline α] (a : α) : Bool

Equations

• Core.Scale.LicensingPipeline.isLicensed a = (Core.Scale.LicensingPipeline.toBoundedness a).isLicensed

@[implicit_reducible]

instance Core.Scale.LicensingPipeline.instBoundedness : LicensingPipeline Boundedness

Equations

• Core.Scale.LicensingPipeline.instBoundedness = { toBoundedness := id }

@[implicit_reducible]

instance Core.Scale.LicensingPipeline.instMereoTag : LicensingPipeline MereoTag

Equations

• Core.Scale.LicensingPipeline.instMereoTag = { toBoundedness := Core.Scale.MereoTag.toBoundedness }

theorem Core.Scale.LicensingPipeline.universal {α : Type u_2} {β : Type u_3} [LicensingPipeline α] [LicensingPipeline β] (a : α) (b : β) (h : toBoundedness a = toBoundedness b) : isLicensed a = isLicensed b

The universal licensing theorem: any two pipeline inputs that map to the same Boundedness yield the same licensing prediction, regardless of which framework they come.

inductive Core.Scale.ScalePolarity : Type

Intrinsic polarity of a scale dimension. positive: the unmarked direction (tall, hot, confident). negative: the marked/inverted direction (short, cold, doubtful).

• positive : ScalePolarity
• negative : ScalePolarity

@[implicit_reducible]

instance Core.Scale.instDecidableEqScalePolarity : DecidableEq ScalePolarity

Equations

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

@[implicit_reducible]

instance Core.Scale.instReprScalePolarity : Repr ScalePolarity

Equations

• Core.Scale.instReprScalePolarity = { reprPrec := Core.Scale.instReprScalePolarity.repr }

def Core.Scale.instReprScalePolarity.repr : ScalePolarity → ℕ → Std.Format

Equations

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