Core/Scales/HasMeasure.lean — measurement typeclass + finite degree types

HasMeasure E α is the formal-semantics "measure function" μ : E → α, parameterized over both the entity type and the codomain.

Renames the legacy HasDegree typeclass — HasDegree is preserved as a deprecation alias for one version, then removed in a later refactor.

Degree max and Threshold max are discretized scale types for gradable adjective RSA computations; they participate in the DirectedMeasure infrastructure via their LinearOrder/BoundedOrder instances.

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

Multi-dim measurement

No outParam on δ — multi-dim same-carrier (e.g. Entity measured by both height and weight) is supported via distinct (α, δ) instance signatures or newtype wrappers (mathlib Additive/Multiplicative precedent). This is a deliberate design choice per master plan v4.

Degree and Threshold types for finite scales

Degree max wraps Fin (max + 1) with LinearOrder, BoundedOrder, Fintype. Threshold max wraps Fin max with coercion to Degree max.

structure Core.Scale.Degree (max : ℕ) : Type

A degree on a scale from 0 to max. Represents discretized continuous values like height, temperature, etc.

• value : Fin (max + 1)

def Core.Scale.instReprDegree.repr {max✝ : ℕ} : Degree max✝ → ℕ → Std.Format

Equations

• Core.Scale.instReprDegree.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

@[implicit_reducible]

instance Core.Scale.instReprDegree {max✝ : ℕ} : Repr (Degree max✝)

Equations

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

def Core.Scale.instDecidableEqDegree.decEq {max✝ : ℕ} (x✝ x✝¹ : Degree max✝) : Decidable (x✝ = x✝¹)

Equations

• Core.Scale.instDecidableEqDegree.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Scale.instDecidableEqDegree {max✝ : ℕ} : DecidableEq (Degree max✝)

Equations

• Core.Scale.instDecidableEqDegree = Core.Scale.instDecidableEqDegree.decEq

@[implicit_reducible]

instance Core.Scale.instInhabitedDegree {n : ℕ} : Inhabited (Degree n)

Equations

• Core.Scale.instInhabitedDegree = { default := { value := ⟨0, ⋯⟩ } }

@[implicit_reducible]

instance Core.Scale.instLinearOrderDegree {max : ℕ} : LinearOrder (Degree max)

Degree max inherits a linear order from Fin (max + 1).

Equations

• Core.Scale.instLinearOrderDegree = LinearOrder.lift' Core.Scale.Degree.value ⋯

@[implicit_reducible]

instance Core.Scale.instBoundedOrderDegree {max : ℕ} : BoundedOrder (Degree max)

Degree max is bounded: 0 is the minimum, max is the maximum.

Equations

• Core.Scale.instBoundedOrderDegree = { top := { value := Fin.last max }, le_top := ⋯, bot := { value := ⟨0, ⋯⟩ }, bot_le := ⋯ }

def Core.Scale.allDegrees (max : ℕ) : List (Degree max)

All degrees from 0 to max

Equations

• Core.Scale.allDegrees max = List.map (fun (x : Fin (max + 1)) => { value := x }) (List.finRange (max + 1))

def Core.Scale.Degree.ofNat (max n : ℕ) : Degree max

Degree from Nat (clamped)

Equations

• Core.Scale.Degree.ofNat max n = { value := ⟨min n max, ⋯⟩ }

def Core.Scale.Degree.toNat {max : ℕ} (d : Degree max) : ℕ

Get numeric value

Equations

• d.toNat = ↑d.value

structure Core.Scale.Threshold (max : ℕ) : Type

A threshold for a gradable adjective. x is "tall" iff degree(x) > threshold.

• value : Fin max

def Core.Scale.instReprThreshold.repr {max✝ : ℕ} : Threshold max✝ → ℕ → Std.Format

Equations

• Core.Scale.instReprThreshold.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "value" ++ Std.Format.text " := " ++ (Std.Format.nest 9 (repr x✝.value)).group) " }"

@[implicit_reducible]

instance Core.Scale.instReprThreshold {max✝ : ℕ} : Repr (Threshold max✝)

Equations

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

def Core.Scale.instDecidableEqThreshold.decEq {max✝ : ℕ} (x✝ x✝¹ : Threshold max✝) : Decidable (x✝ = x✝¹)

Equations

• Core.Scale.instDecidableEqThreshold.decEq { value := a } { value := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Scale.instDecidableEqThreshold {max✝ : ℕ} : DecidableEq (Threshold max✝)

Equations

• Core.Scale.instDecidableEqThreshold = Core.Scale.instDecidableEqThreshold.decEq

@[implicit_reducible]

instance Core.Scale.instInhabitedThresholdOfAutoParamLtNatOfNat_auto_44 {n : ℕ} (h : 0 < n := by omega) : Inhabited (Threshold n)

Equations

• Core.Scale.instInhabitedThresholdOfAutoParamLtNatOfNat_auto_44 h = { default := { value := ⟨0, h⟩ } }

@[implicit_reducible]

instance Core.Scale.instLinearOrderThreshold {max : ℕ} : LinearOrder (Threshold max)

Threshold max inherits a linear order from Fin max.

Equations

• Core.Scale.instLinearOrderThreshold = LinearOrder.lift' Core.Scale.Threshold.value ⋯

def Core.Scale.allThresholds (max : ℕ) : autoParam (0 < max) allThresholds._auto_1 → List (Threshold max)

All thresholds from 0 to max-1

Equations

• Core.Scale.allThresholds max x✝ = List.map (fun (x : Fin max) => { value := x }) (List.finRange max)

def Core.Scale.Threshold.toNat {max : ℕ} (t : Threshold max) : ℕ

Get numeric value

Equations

• t.toNat = ↑t.value

@[implicit_reducible]

instance Core.Scale.instFintypeDegree {max : ℕ} : Fintype (Degree max)

Equations

• Core.Scale.instFintypeDegree = Fintype.ofEquiv (Fin (max + 1)) { toFun := Core.Scale.Degree.mk, invFun := Core.Scale.Degree.value, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance Core.Scale.instFintypeThresholdOfNeZeroNat {max : ℕ} [NeZero max] : Fintype (Threshold max)

Equations

• Core.Scale.instFintypeThresholdOfNeZeroNat = Fintype.ofEquiv (Fin max) { toFun := Core.Scale.Threshold.mk, invFun := Core.Scale.Threshold.value, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance Core.Scale.instCoeThresholdDegree {max : ℕ} : Coe (Threshold max) (Degree max)

Coercion: Threshold embeds into Degree via Fin.castSucc

Equations

• Core.Scale.instCoeThresholdDegree = { coe := fun (t : Core.Scale.Threshold max) => { value := t.value.castSucc } }

theorem Core.Scale.coe_threshold_toNat {max : ℕ} (t : Threshold max) : { value := t.value.castSucc }.toNat = t.toNat

@[reducible, inline]

abbrev Core.Scale.deg (n : ℕ) {max : ℕ} (h : n ≤ max := by omega) : Degree max

Construct a degree by literal: deg 5 : Degree 10.

Equations

• Core.Scale.deg n h = { value := ⟨n, ⋯⟩ }

@[reducible, inline]

abbrev Core.Scale.thr (n : ℕ) {max : ℕ} (h : n < max := by omega) : Threshold max

Construct a threshold by literal: thr 5 : Threshold 10.

Equations

• Core.Scale.thr n h = { value := ⟨n, h⟩ }

class Core.Scale.HasMeasure (E α : Type) : Type

Typeclass for entities that have a measurement on some scale. The formal semantics "measure function" μ : Entity → α.

The codomain α is polymorphic — heights might use ℚ (cm, exact), physical heights ℝ, durations ℕ (ticks), prices ℚ (USD), etc.

No outParam on α: master plan v4 deliberately drops outParam to support multi-dim same-carrier (e.g., Entity measured by BOTH height and weight). When an Entity has multiple measures, consumers disambiguate via explicit (α := ...) or named instances; mathlib Additive/Multiplicative newtype-wrapping is the canonical pattern for type-level disambiguation.

Renamed from HasDegree (legacy name) per master plan v4 Phase A.7. Field name kept as degree for one-version migration compatibility; HasMeasure.measure is provided as the v4-canonical alias.

• degree : E → α

@[reducible, inline]

abbrev Core.Scale.HasMeasure.measure {E α : Type} [HasMeasure E α] : E → α

v4-canonical name for the measurement function. Aliased to the legacy field name degree for one-version migration.

Equations

• Core.Scale.HasMeasure.measure = Core.Scale.HasMeasure.degree

@[reducible, inline]

abbrev Core.Scale.HasDegree (E α : Type) : Type

Deprecation alias: HasDegree is the legacy name for HasMeasure. One-version migration alias; will be removed in a follow-up refactor.

Equations

• Core.Scale.HasDegree E α = Core.Scale.HasMeasure E α

@[reducible, inline]

abbrev Core.Scale.HasDegree.degree {E α : Type} [HasDegree E α] : E → α

Explicit alias for the legacy field projection HasDegree.degree. Needed because Lean does not auto-derive projection names through abbrevs.

Equations

• Core.Scale.HasDegree.degree = Core.Scale.HasMeasure.degree