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:

• [schwarzschild-2002] [schwarzschild-2006] — Monotonicity Constraint on the measure function in nominal pseudopartitives.
• [krifka-1989] — extensive measure functions on quantized objects.
• [wellwood-2015] — μ admissibility for much-comparatives.
• [cariani-santorio-wellwood-2024] (eq. 21) — CSW use this exact formulation for confidence orderings.
• [pasternak-2019] (def 4) — μ_int monotonicity on the part-whole structure of mental states.
• [ying-zhi-xuan-wong-mansinghka-tenenbaum-2025] — EpistemicThreshold.IsProbabilistic is a strengthening of this (Monotone, not StrictMono).

Equations

• Degree.admissibleMeasure μ = StrictMono μ

Dimensional restriction

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

A domain is dimensionally restricted when any two admissible measure functions (StrictMono maps into the scale D, default ℝ) 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 α D = ∀ (μ₁ μ₂ : α → D), StrictMono μ₁ → StrictMono μ₂ → ∀ (a b : α), μ₁ a < μ₁ b ↔ μ₂ a < μ₂ b

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

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 α] {D : Type} [Preorder D] {μ₁ μ₂ : α → D} (hμ₁ : StrictMono μ₁) (hμ₂ : StrictMono μ₂) {a b : α} (h₁ : μ₁ a < μ₁ b) (h₂ : ¬μ₂ a < μ₂ b) : ¬DimensionallyRestricted α D

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

theorem Degree.prod_not_dimensionallyRestricted {D : Type} [Field D] [LinearOrder D] [IsStrictOrderedRing D] : ¬DimensionallyRestricted (D × D) D

The converse witness: on the componentwise-ordered D × D (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.