Measure-phrase modification of degree constructions

[Sch05] [Sol15] [Win05] [Bur07]

Measure-phrase differentials ("3 inches taller") and factor phrases ("twice as tall"): differentialComparative and factorEquative, the interval- and ratio-scale rows of the naturality table in Degree/Hom.lean. Where bare comparatives are invariant under any StrictMono rescaling (comparativeSem_comp), the differential is invariant under translations only (differentialComparative_comp_add, differentialComparative_not_natural) and the factor phrase under scalings only (factorEquative_comp_mul, factorEquative_not_translation_invariant) — the measurement-theoretic scale hierarchy (MeasurementLevel) derived as invariance classes rather than stipulated: a construction is meaningful on a scale type exactly when it is natural under that type's admissible transformations. Hence "3 inches taller" ✓ but "*3 units more beautiful" ✗ (beauty is ordinal), "twice as tall" ✓ but "*twice as hot" in °C ✗ (temperature is interval, no meaningful zero).

Differential and factor semantics

def Degree.differentialComparative {Entity : Type u_1} {D : Type u_2} [Sub D] (μ : Entity → D) (a b : Entity) (diff : D) : Prop

Differential comparative: "A is d-much Adj-er than B" iff μ(A) - μ(B) = d. Requires subtraction structure, not just ordering — what makes measure-phrase differentials more restrictive than bare comparatives.

Equations

• Degree.differentialComparative μ a b diff = (μ a - μ b = diff)

def Degree.factorEquative {Entity : Type u_1} {D : Type u_2} [Mul D] (μ : Entity → D) (a b : Entity) (factor : D) : Prop

Factor phrase equative: "A is n times as tall as B" iff μ(A) = n × μ(B). Requires a meaningful zero (ratio scale).

Equations

• Degree.factorEquative μ a b factor = (μ a = factor * μ b)

theorem Degree.differential_positive_iff {Entity : Type u_1} (μ : Entity → ℚ) (a b : Entity) (diff : ℚ) (hdiff : 0 < diff) : differentialComparative μ a b diff → μ b < μ a

A positive differential entails the bare comparative. Stated on ℚ; generalizing requires ordered-group machinery ([AddCommGroup D] [LinearOrder D] [IsStrictOrderedAddMonoid D]) that mathlib's current taxonomy splits across multiple unbundled classes — see e.g. Mathlib/Algebra/Order/Field/Defs.lean for the analogous LinearOrderedField → Field + LinearOrder + IsStrictOrderedRing migration. Consumers (Intensional, VonStechow1984) instantiate at ℚ.

Invariance: the measurement-theoretic hierarchy derived

Each construction's scale-type requirement is its invariance class (cf. comparativeSem_comp in Degree/Hom.lean for the ordinal row and positive_not_natural for the positive form's failure).

theorem Degree.differentialComparative_comp_add {Entity : Type u_1} (μ : Entity → ℚ) (c : ℚ) (a b : Entity) (diff : ℚ) : differentialComparative (fun (x : Entity) => μ x + c) a b diff ↔ differentialComparative μ a b diff

Differentials are translation-invariant: shifting the scale's zero point preserves gaps — differentials are meaningful on interval scales.

theorem Degree.differentialComparative_not_natural : ∃ (f : ℚ → ℚ), StrictMono f ∧ ∃ (μ : ℚ → ℚ) (a : ℚ) (b : ℚ) (diff : ℚ), differentialComparative μ a b diff ∧ ¬differentialComparative (f ∘ μ) a b diff

Differentials are NOT invariant under arbitrary monotone rescaling: a StrictMono map can destroy the gap. Differentials need interval structure — "*3 units more beautiful" fails because beauty supports only ordinal comparison.

theorem Degree.factorEquative_comp_mul {Entity : Type u_1} (μ : Entity → ℚ) {c : ℚ} (hc : c ≠ 0) (a b : Entity) (factor : ℚ) : factorEquative (fun (x : Entity) => c * μ x) a b factor ↔ factorEquative μ a b factor

Factor phrases are scaling-invariant: changing the unit preserves ratios — factor phrases are meaningful on ratio scales.

theorem Degree.factorEquative_not_translation_invariant : ∃ (μ : ℚ → ℚ) (c : ℚ) (a : ℚ) (b : ℚ) (factor : ℚ), factorEquative μ a b factor ∧ ¬factorEquative (fun (x : ℚ) => μ x + c) a b factor

Factor phrases are NOT translation-invariant: moving the zero point destroys ratios — "*twice as hot" fails in °C because temperature's zero is conventional.

Scale types as a lexical classification

inductive Degree.MeasurementLevel : Type

Measurement level of an adjective's scale, ordered by admissible transformations (each level's constructions are exactly those invariant under its transformation class — the theorems above): ordinal (any monotone map), interval (affine), ratio (scaling), extensive (ratio + cross-dimensional commensurability; spatial extent is [Bur07]'s "only scale ... that has measurements in different dimensions mapped onto it", licensing subcomparatives).

• ordinal : MeasurementLevel
• interval : MeasurementLevel
• ratio : MeasurementLevel
• extensive : MeasurementLevel

@[implicit_reducible]

instance Degree.instDecidableEqMeasurementLevel : DecidableEq MeasurementLevel

Equations

• Degree.instDecidableEqMeasurementLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.instReprMeasurementLevel.repr : MeasurementLevel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Degree.instReprMeasurementLevel : Repr MeasurementLevel

Equations

• Degree.instReprMeasurementLevel = { reprPrec := Degree.instReprMeasurementLevel.repr }

def Degree.MeasurementLevel.AdmitsMeasurePhrase (l : MeasurementLevel) : Prop

Measure-phrase differentials ("10 degrees warmer") require at least interval scale (differentialComparative_comp_add).

Equations

• l.AdmitsMeasurePhrase = (l ≠ Degree.MeasurementLevel.ordinal)

@[implicit_reducible]

instance Degree.instDecidablePredMeasurementLevelAdmitsMeasurePhrase : DecidablePred MeasurementLevel.AdmitsMeasurePhrase

Equations

• Degree.instDecidablePredMeasurementLevelAdmitsMeasurePhrase l = Degree.instDecidablePredMeasurementLevelAdmitsMeasurePhrase._aux_1 l

def Degree.MeasurementLevel.AdmitsFactorPhrase (l : MeasurementLevel) : Prop

Factor phrases ("twice as tall") require a meaningful zero (factorEquative_comp_mul).

Equations

• l.AdmitsFactorPhrase = (l = Degree.MeasurementLevel.ratio ∨ l = Degree.MeasurementLevel.extensive)

@[implicit_reducible]

instance Degree.instDecidablePredMeasurementLevelAdmitsFactorPhrase : DecidablePred MeasurementLevel.AdmitsFactorPhrase

Equations

• Degree.instDecidablePredMeasurementLevelAdmitsFactorPhrase l = Degree.instDecidablePredMeasurementLevelAdmitsFactorPhrase._aux_1 l

def Degree.MeasurementLevel.AdmitsSubcomparative (l : MeasurementLevel) : Prop

Subcomparatives ("shorter than the house is high") require extensive commensurability: two measure functions sharing a unit. Hence "shorter than high" ✓ (both spatial), "??hotter than expensive" ✗.

Equations

• l.AdmitsSubcomparative = (l = Degree.MeasurementLevel.extensive)

@[implicit_reducible]

instance Degree.instDecidablePredMeasurementLevelAdmitsSubcomparative : DecidablePred MeasurementLevel.AdmitsSubcomparative

Equations

• Degree.instDecidablePredMeasurementLevelAdmitsSubcomparative l = Degree.instDecidablePredMeasurementLevelAdmitsSubcomparative._aux_1 l