Documentation

Linglib.Core.Scales.Comparative

Core/Scales/Comparative.lean — ComparativeScale + AdditiveScale #

@cite{krantz-1971} @cite{holliday-icard-2013}

Root algebraic structures for the category of scales.

ComparativeScale α — a preorder with boundedness classification. All scale-based reasoning factors through this structure.

AdditiveScale α — comparative scale enriched with join and finite additivity (FA). Two independent linglib instances:

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

source
structure Core.Scale.ComparativeScale (α : Type u_1) [Preorder α] :
Type

A comparative scale: a boundedness classification on a preorder. This is the root object in the category of scales. All scale-based reasoning in linglib (degree semantics, mereological measurement, epistemic comparison) factors through this structure.

The ordering comes from the ambient [Preorder α] — no redundant le/le_refl/le_trans fields. Morphisms are Mathlib's Monotone.

@cite{krantz-1971}: a comparative scale is an ordered set with enough structure to support qualitative comparison.

  • boundedness : Boundedness

    Scale boundedness classification

Instances For
    source
    structure Core.Scale.AdditiveScale (α : Type u_1) [SemilatticeSup α] extends Core.Scale.ComparativeScale α :
    Type u_1

    An additive scale: a comparative scale enriched with join and finite additivity (FA). Two independent instances exist in linglib:

    • Mereological: ExtMeasure.additive
    • Epistemic: probability FA

    The FA axiom says disjoint augmentation preserves order: if z is disjoint from both x and y, then x ≤ y ↔ x ⊔ z ≤ y ⊔ z. This is the qualitative content of additive representation.

    • boundedness : Boundedness
    • disjoint : α → α → Prop

      Disjointness predicate

    • fa (x y z : α) : self.disjoint x z → self.disjoint y z → (x ≤ y ↔ x ⊔ z ≤ y ⊔ z)

      Finite additivity: disjoint augmentation preserves order. Both ≤ and ⊔ come from the ambient SemilatticeSup.

    Instances For
      source
      def Core.Scale.ComparativeScale.isLicensed {α : Type u_1} [Preorder α] (S : ComparativeScale α) :
      Bool

      Licensing prediction from the underlying boundedness.

      Equations
      Instances For