Documentation

Linglib.Core.Order.ComparativeScale

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

[KLST71] [HI13]

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.Order.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.

[KLST71]: a comparative scale is an ordered set with enough structure to support qualitative comparison.

  • boundedness : Boundedness

    Scale boundedness classification

Instances For
    source
    structure Core.Order.AdditiveScale (α : Type u_1) [SemilatticeSup α] extends Core.Order.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.Order.ComparativeScale.IsLicensed {α : Type u_1} [Preorder α] (S : ComparativeScale α) :
      Prop

      Licensing prediction from the underlying boundedness.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Core.Order.ComparativeScale.instDecidableIsLicensed {α : Type u_1} [Preorder α] (S : ComparativeScale α) :
        Decidable S.IsLicensed
        Equations