Directed measurement primitive

[Ken07] [Ken15] [LG17] [KLST71]

A DirectedMeasure D E packages a degree type, entity type, measure function, boundedness classification, and direction. The common algebraic core of the degree-domain constructors and epistemic threshold semantics.

Main declarations

• DirectedMeasure: the bundled measure structure.
• DirectedMeasure.IsLicensed: endpoint-based licensing via Boundedness.IsLicensed.
• DirectedMeasure.degreeProperty: the degree property derived from direction (Comparison.ge.over positive, Comparison.le.over negative); its maximal informativity is characterized in Semantics/Entailment/Extremum.lean.
• DirectedMeasure.numeral, DirectedMeasure.adjective: Kennedy-style numeral and gradable-adjective domains.

Scale types as Mathlib typeclass combinations

For theorems about concrete scales — proving facts about a particular type — use Mathlib typeclasses directly:

• Measurement scale: [LinearOrder α]
• Dense measurement scale ([FH06b] UDM): [LinearOrder α] [DenselyOrdered α]
• Upper-bounded scale: [LinearOrder α] [OrderTop α]
• Lower-bounded scale: [LinearOrder α] [OrderBot α]
• Open scale: [LinearOrder α] [NoMaxOrder α] [NoMinOrder α]

For lexical-data tagging, use the Boundedness enum from Defs.lean. Mathlib typeclass instances cannot be stored in record fields; the enum and the typeclass system serve different roles and both are real.

DirectedMeasure

structure Degree.DirectedMeasure (D : Type u_1) [LinearOrder D] (E : Type u_2) extends Core.Order.ComparativeScale D : Type (max u_1 u_2)

A directed measurement on a bounded scale: a degree type D (the scale), an entity type E, a measure function μ : E → D, boundedness (from ComparativeScale), and a direction.

Common algebraic core of the numeral/adjective domain constructors and epistemic thresholds (epistemicAsDirectedMeasure, on DirectedMeasure ℚ (E × (W → Bool))). The degree property (Comparison.ge.over for positive, Comparison.le.over for negative) is derived from direction, not stored — per [LG17], the binary direction choice is the fundamental parameter.

• boundedness : Boundedness
• μ : E → D

  Measure function: maps entities to degrees on the scale

• direction : Core.Order.ScalePolarity

  Scale direction: positive (μ(x) ≥ θ) or negative (μ(x) ≤ θ). Determines which side of a threshold counts as satisfying the predicate. Positive: tall, likely, full. Negative: short, unlikely, empty.

def Degree.DirectedMeasure.IsLicensed {D : Type u_1} [LinearOrder D] {E : Type u_2} (dm : DirectedMeasure D E) : Prop

Licensing: licensed iff the bounded scale admits an optimum. See Boundedness.IsLicensed for the caveat — this checks "any endpoint exists", not [Ken07]'s full modifier-class licensing matrix.

Equations

• dm.IsLicensed = dm.boundedness.IsLicensed

@[implicit_reducible]

instance Degree.DirectedMeasure.instDecidableIsLicensed {D : Type u_1} [LinearOrder D] {E : Type u_2} (dm : DirectedMeasure D E) : Decidable dm.IsLicensed

Equations

• dm.instDecidableIsLicensed = Degree.DirectedMeasure.instDecidableIsLicensed._aux_1 dm

def Degree.DirectedMeasure.degreeProperty {D : Type u_1} [LinearOrder D] {E : Type u_2} (dm : DirectedMeasure D E) : D → Set E

The degree property derived from the measure's direction: Comparison.ge.over for positive scales (tall, likely), Comparison.le.over for negative ones (short, unlikely). The derivation the structure docstring promises: direction is the stored parameter, the property follows.

Equations

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

Numeral and adjective domains

Constructors for [Ken15]'s numeral domains (de-Fregean type-shift over cardinality) and [Ken07]'s gradable-adjective domains. The licensing theorems below only pin the Boundedness → licensed map; the substantive maximal-informativity results (exactness of the maximally informative degree) live in Semantics/Entailment/Extremum.lean (isMaxInf_atLeast_iff_eq, isMaxInf_atMost_iff_eq) and are discharged over real numeral meanings in Studies/FoxHackl2006Numerals.lean.

def Degree.DirectedMeasure.numeral {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : DirectedMeasure α W

[Ken15] numeral domain: "at least n" over cardinality. Closed scale (ℕ well-ordered) → always licensed. Type-shift to exact = MIP applied to Comparison.ge.over.

Equations

• Degree.DirectedMeasure.numeral μ = { boundedness := Core.Order.Boundedness.closed, μ := μ }

def Degree.DirectedMeasure.adjective {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) (b : Core.Order.Boundedness) : DirectedMeasure α W

[Ken07] gradable adjective domain. Boundedness varies by adjective class (tall: open, full: closed).

Equations

• Degree.DirectedMeasure.adjective μ b = { boundedness := b, μ := μ }

Licensing theorems

theorem Degree.DirectedMeasure.numeral_licensed {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : (numeral μ).IsLicensed

Numeral domains are always licensed (closed scale).

theorem Degree.DirectedMeasure.classB_licensed {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : (adjective μ Core.Order.Boundedness.closed).IsLicensed

Class B adjectives (closed scale) are licensed.

theorem Degree.DirectedMeasure.classA_blocked {α : Type u_1} [LinearOrder α] {W : Type u_2} (μ : W → α) : ¬(adjective μ Core.Order.Boundedness.open_).IsLicensed

Class A adjectives (open scale) are blocked.