Scale boundedness and the licensing pipeline

[KMcN05] [Ken07] [RW04b] [Rou26]

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

Main declarations

• Boundedness: the four-way endpoint classification, with HasMax / HasMin / IsLicensed predicates.
• MereoTag, EpistemicTag: binary classifications mapping into Boundedness.
• LicensingPipeline: typeclass for types classifiable into Boundedness, with the universal agreement theorem.
• ScalePolarity.

Scale boundedness

inductive Core.Order.Boundedness : Type

Classification of scale boundedness. [KMcN05] eq (1) and [Ken07] §4.2 eq (59): four scale types based on which endpoints exist (independently discovered by [RW04b]). [Rou26]: 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. [Ken07] §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. [Ken07] 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.Order.instDecidableEqBoundedness : DecidableEq Boundedness

Equations

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

@[implicit_reducible]

instance Core.Order.instReprBoundedness : Repr Boundedness

Equations

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

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

Equations

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

def Core.Order.Boundedness.HasMax : Boundedness → Prop

Does this scale have an inherent maximum?

Equations

• Core.Order.Boundedness.upperBounded.HasMax = True
• Core.Order.Boundedness.closed.HasMax = True
• Core.Order.Boundedness.open_.HasMax = False
• Core.Order.Boundedness.lowerBounded.HasMax = False

@[implicit_reducible]

instance Core.Order.instDecidablePredBoundednessHasMax : DecidablePred Boundedness.HasMax

Equations

• Core.Order.instDecidablePredBoundednessHasMax Core.Order.Boundedness.open_ = isFalse Core.Order.instDecidablePredBoundednessHasMax._proof_1
• Core.Order.instDecidablePredBoundednessHasMax Core.Order.Boundedness.lowerBounded = isFalse Core.Order.instDecidablePredBoundednessHasMax._proof_2
• Core.Order.instDecidablePredBoundednessHasMax Core.Order.Boundedness.upperBounded = isTrue trivial
• Core.Order.instDecidablePredBoundednessHasMax Core.Order.Boundedness.closed = isTrue trivial

def Core.Order.Boundedness.HasMin : Boundedness → Prop

Does this scale have an inherent minimum?

Equations

• Core.Order.Boundedness.lowerBounded.HasMin = True
• Core.Order.Boundedness.closed.HasMin = True
• Core.Order.Boundedness.open_.HasMin = False
• Core.Order.Boundedness.upperBounded.HasMin = False

@[implicit_reducible]

instance Core.Order.instDecidablePredBoundednessHasMin : DecidablePred Boundedness.HasMin

Equations

• Core.Order.instDecidablePredBoundednessHasMin Core.Order.Boundedness.open_ = isFalse Core.Order.instDecidablePredBoundednessHasMin._proof_1
• Core.Order.instDecidablePredBoundednessHasMin Core.Order.Boundedness.lowerBounded = isTrue trivial
• Core.Order.instDecidablePredBoundednessHasMin Core.Order.Boundedness.upperBounded = isFalse Core.Order.instDecidablePredBoundednessHasMin._proof_2
• Core.Order.instDecidablePredBoundednessHasMin Core.Order.Boundedness.closed = isTrue trivial

def Core.Order.Boundedness.IsLicensed : Boundedness → Prop

"Any endpoint exists": the scale has at least one bound (max or min); an open scale has none.

NOT [Ken07]'s full licensing prediction. Kennedy's actual prediction is the 4×2 modifier-class matrix in [Ken07] eq (61) (= [KMcN05] eq (15)): maximizers (completely, perfectly) require an UPPER endpoint; minimizers (slightly, partially) require a LOWER endpoint; proportional modifiers (half) require BOTH — for modifier-specific licensing, consult HasMax/HasMin directly. This predicate suffices for callers that only distinguish "open" from "any-endpoint-exists" (Interpretive Economy, [Ken07] §4.3; Rouillard's MIP, [Rou26]).

Equations

• Core.Order.Boundedness.closed.IsLicensed = True
• Core.Order.Boundedness.lowerBounded.IsLicensed = True
• Core.Order.Boundedness.upperBounded.IsLicensed = True
• Core.Order.Boundedness.open_.IsLicensed = False

@[implicit_reducible]

instance Core.Order.instDecidablePredBoundednessIsLicensed : DecidablePred Boundedness.IsLicensed

Equations

• Core.Order.instDecidablePredBoundednessIsLicensed Core.Order.Boundedness.open_ = isFalse Core.Order.instDecidablePredBoundednessIsLicensed._proof_1
• Core.Order.instDecidablePredBoundednessIsLicensed Core.Order.Boundedness.lowerBounded = isTrue trivial
• Core.Order.instDecidablePredBoundednessIsLicensed Core.Order.Boundedness.upperBounded = isTrue trivial
• Core.Order.instDecidablePredBoundednessIsLicensed Core.Order.Boundedness.closed = isTrue trivial

MereoTag and the licensing pipeline

inductive Core.Order.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.Order.instDecidableEqMereoTag : DecidableEq MereoTag

Equations

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

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

Equations

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

@[implicit_reducible]

instance Core.Order.instReprMereoTag : Repr MereoTag

Equations

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

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

Equations

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

class Core.Order.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.Order.LicensingPipeline.IsLicensed {α : Type u_1} [LicensingPipeline α] (a : α) : Prop

A pipeline input is licensed iff its boundedness classification is.

Equations

• Core.Order.LicensingPipeline.IsLicensed a = (Core.Order.LicensingPipeline.toBoundedness a).IsLicensed

@[implicit_reducible]

instance Core.Order.LicensingPipeline.instDecidablePredIsLicensed {α : Type u_1} [LicensingPipeline α] : DecidablePred IsLicensed

Equations

• Core.Order.LicensingPipeline.instDecidablePredIsLicensed a = Core.Order.LicensingPipeline.instDecidablePredIsLicensed._aux_1 a

@[implicit_reducible]

instance Core.Order.LicensingPipeline.instBoundedness : LicensingPipeline Boundedness

Equations

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

@[implicit_reducible]

instance Core.Order.LicensingPipeline.instMereoTag : LicensingPipeline MereoTag

Equations

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

theorem Core.Order.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.Order.EpistemicTag : Type

Binary epistemic classification, parallel to MereoTag: finitely additive scales are closed (endpoint standards licensed), qualitative scales open.

• finitelyAdditive : EpistemicTag
• qualitative : EpistemicTag

@[implicit_reducible]

instance Core.Order.instDecidableEqEpistemicTag : DecidableEq EpistemicTag

Equations

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

@[implicit_reducible]

instance Core.Order.instReprEpistemicTag : Repr EpistemicTag

Equations

• Core.Order.instReprEpistemicTag = { reprPrec := Core.Order.instReprEpistemicTag.repr }

def Core.Order.instReprEpistemicTag.repr : EpistemicTag → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Order.instLicensingPipelineEpistemicTag : LicensingPipeline EpistemicTag

Equations

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

theorem Core.Order.epistemicFA_licensed : LicensingPipeline.IsLicensed EpistemicTag.finitelyAdditive

theorem Core.Order.epistemicQualitative_blocked : ¬LicensingPipeline.IsLicensed EpistemicTag.qualitative

theorem Core.Order.five_frameworks_agree (m : MereoTag) (e : EpistemicTag) (h : LicensingPipeline.toBoundedness m = LicensingPipeline.toBoundedness e) : LicensingPipeline.IsLicensed m ↔ LicensingPipeline.IsLicensed e

theorem Core.Order.epistemicFA_iff_qua : LicensingPipeline.IsLicensed EpistemicTag.finitelyAdditive ↔ LicensingPipeline.IsLicensed MereoTag.qua

theorem Core.Order.epistemicQualitative_iff_cum : LicensingPipeline.IsLicensed EpistemicTag.qualitative ↔ LicensingPipeline.IsLicensed MereoTag.cum

Scale polarity

inductive Core.Order.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.Order.instDecidableEqScalePolarity : DecidableEq ScalePolarity

Equations

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

@[implicit_reducible]

instance Core.Order.instReprScalePolarity : Repr ScalePolarity

Equations

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

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

Equations

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