Core/Scales/HasComparison.lean — primitive comparison typeclass

HasComparison α provides a binary comparison primitive comparativeGreater : α → α → Prop — "a is more-Adj than b". Lawless: anyone instantiates (Klein delineation, Kennedy measure-derived, Charlow-Sutton-Wechsler states, Lassiter-Goodman expected-value, Tversky-Fishburn intransitive majority).

Lawfulness is opt-in via LawfulComparison mixin in LawfulComparison.lean.

Mathlib analog: class LT (α : Type*) where lt : α → α → Prop.

This file is part of the Phase A.7 atomic typeclass landing per master plan v4.

Smart constructor (NOT auto-instance)

HasComparison.ofMeasure is a def, not an auto-instance. Frameworks opt-in via attribute [instance] HasComparison.ofMeasure per their carrier. This avoids typeclass-synthesis ambiguity from the deliberate absence of outParam on HasMeasure δ (multi-dim same-carrier support).

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

A type carries a binary comparison: "a is more-Adj than b".

• comparativeGreater : α → α → Prop

@[reducible]

def Core.Scale.HasComparison.ofMeasure {α δ : Type} [Preorder δ] (m : HasMeasure α δ) : HasComparison α

Smart constructor: any type with a measure into an ordered codomain has comparison. NOT an auto-instance (synthesis ambiguity from no outParam on δ). Frameworks opt-in via attribute [instance].

Example use: attribute [instance] HasComparison.ofMeasure inside a Kennedy-framework file scoped where δ is determinate.

Named instance argument m to avoid typeclass-synthesis ambiguity in the body (we'd otherwise need to specify (α := δ) for HasMeasure.measure). @[reducible] is required for class-type defs (Lean elaboration hygiene).

Equations

• Core.Scale.HasComparison.ofMeasure m = { comparativeGreater := fun (a b : α) => Core.Scale.HasMeasure.degree a > Core.Scale.HasMeasure.degree b }