Category of Comparative Scales

Objects are bundled types with a preorder and ComparativeScale metadata (boundedness classification). Morphisms are OrderHom (bundled monotone maps from Mathlib).

The boundedness tag is metadata attached to objects — morphisms are order-preserving but do not need to preserve boundedness. This mirrors the relationship between MereoDim (injective monotone = StrictMono) and Monotone: MereoCat requires strict monotonicity, while ScaleCat uses the weaker Monotone.

Mathlib's Preord (category of preorders) is the underlying category; ScaleCat adds the ComparativeScale annotation.

structure Core.Categorical.ScaleObj : Type (u + 1)

Bundled comparative scale: a preordered type with boundedness metadata.

• α : Type u

  The carrier type.

• preord : Preorder self.α

  The preorder on the carrier.

• scale : Scale.ComparativeScale self.α

  The comparative scale metadata.

instance Core.Categorical.instCategoryScaleObj : CategoryTheory.Category.{u, u + 1} ScaleObj

Equations

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

def Core.Categorical.ScaleObj.boundedness (S : ScaleObj) : Scale.Boundedness

Extract the boundedness classification of a scale object.

Equations

• S.boundedness = S.scale.boundedness

def Core.Categorical.ScaleObj.isLicensed (S : ScaleObj) : Bool

The licensing prediction for a scale object.

Equations

• S.isLicensed = S.scale.isLicensed

theorem Core.Categorical.ScaleObj.licensing_invariant (A : ScaleObj) (B : ScaleObj) (h : A.boundedness = B.boundedness) : A.isLicensed = B.isLicensed

A morphism between scales with the same boundedness preserves licensing.