Admissible measures and dimensional restriction

The monotonicity requirement on measure functions, and the order-theoretic content of dimension availability.

Main declarations

• admissibleMeasure — the multi-tradition monotonicity condition on a measure function: mathlib's StrictMono, named once.
• DimensionallyRestricted — any two admissible measures agree on the comparative ordering; holds exactly on linear orders (linearOrder_dimensionallyRestricted / prod_not_dimensionallyRestricted).

@[reducible, inline]

abbrev Degree.admissibleMeasure {S : Type u_1} {D : Type u_2} [Preorder S] [Preorder D] (μ : S → D) : Prop

The monotonicity-preservation requirement on measure functions used in monotonicity-requiring constructions: μ is admissible for a background ordering iff s₁ ≺ s₂ entails μ(s₁) < μ(s₂). This is Mathlib's StrictMono.

Single-name canonical Prop for a multi-tradition convergence. This one Prop names the same condition that appears under different labels across the literature; linglib hosts it once here and lets every consumer credit its own source:

• [Sch02] [Sch06] — Monotonicity Constraint on the measure function in nominal pseudopartitives.
• [Kri89] — extensive measure functions on quantized objects.
• [Wel15] — μ admissibility for much-comparatives; admissibleMeasure_of_mereoDim bridges to the bundled MereoDim typeclass.
• [CSW24] (eq. 21) — CSW use this exact formulation for confidence orderings.
• [Pas19b] (def 4) — μ_int monotonicity on the part-whole structure of mental states.
• [YZXW+25] — EpistemicThreshold.isProbabilistic is a strengthening of this (Monotone, not StrictMono).

The bundled-typeclass form is MereoDim in Semantics/Mereology.lean (with [PartialOrder] carriers); the unbundled-Prop form is here (with [Preorder], more permissive). Use MereoDim when typeclass inference is desired; use admissibleMeasure when the witness is passed explicitly.

Equations

• Degree.admissibleMeasure μ = StrictMono μ

theorem Degree.admissibleMeasure_of_mereoDim {A : Type u_1} {D : Type u_2} [PartialOrder A] [PartialOrder D] {μ : A → D} (h : Mereology.MereoDim μ) : admissibleMeasure μ

Every MereoDim witness yields the unbundled admissibleMeasure Prop (MereoDim bundles StrictMono with [PartialOrder] carriers).

Dimensional restriction

def Degree.DimensionallyRestricted (α : Type u_1) [Preorder α] : Prop

A domain is dimensionally restricted when any two admissible measure functions (StrictMono maps to ℚ) agree on the comparative ordering of all elements: the comparative is determined by the background ordering alone, not by the choice of measure.

Dimensional restriction holds iff the ambient preorder is total: the forward direction is linearOrder_dimensionallyRestricted; the converse is witnessed by incomparable elements with disagreeing measures (prod_not_dimensionallyRestricted).

Equations

• Degree.DimensionallyRestricted α = ∀ (μ₁ μ₂ : α → ℚ), StrictMono μ₁ → StrictMono μ₂ → ∀ (a b : α), μ₁ a < μ₁ b ↔ μ₂ a < μ₂ b

theorem Degree.linearOrder_dimensionallyRestricted {α : Type u_1} [LinearOrder α] : DimensionallyRestricted α

Linear orders are dimensionally restricted: the comparative ordering is uniquely determined by the ambient order, regardless of which admissible measure function is chosen.

theorem Degree.not_restricted_of_disagreement {α : Type u_1} [Preorder α] {μ₁ μ₂ : α → ℚ} (hμ₁ : StrictMono μ₁) (hμ₂ : StrictMono μ₂) {a b : α} (h₁ : μ₁ a < μ₁ b) (h₂ : ¬μ₂ a < μ₂ b) : ¬DimensionallyRestricted α

If two admissible measures disagree on some pair, the domain is NOT dimensionally restricted.

theorem Degree.prod_not_dimensionallyRestricted : ¬DimensionallyRestricted (ℚ × ℚ)

The converse witness: on the componentwise-ordered ℚ × ℚ (weight × volume), the admissible measures 2·w + v and w + v order the incomparable elements (0, 1) and (1, 0) differently — the multi-dimensional signature of entity/event domains.