Marginality Scales

@cite{dinis-jacinto-2026}

ML theory enriches a linear order with a primitive "marginally smaller than" relation M. From R (= <) and M one derives L (largely smaller than): L(x,y) := x < y ∧ ¬ M x y. Five axioms govern M; Theorem 2.2 derives M-TRANSITIVITY and M-BOUNDEDNESS as consequences.

This sits alongside DirectedMeasure (in Core.Scale): a DirectedMeasure determines licensing from boundedness, while an MLScale adds granularity structure (marginal vs. large difference) on the same LinearOrder.

• Dinis, B. & Jacinto, B. (2026). Marginality scales for gradable adjectives. Linguistics and Philosophy 49:101–131.

structure Semantics.Lexical.Adjective.MLScale (α : Type u_1) [LinearOrder α] : Type u_1

ML theory (@cite{dinis-jacinto-2026}, Fig. 1): a linear order enriched with a primitive "marginally smaller than" relation M satisfying five axioms. The strict order < from LinearOrder is the paper's R; L (largely smaller) is derived as R ∧ ¬M.

• M : α → α → Prop

  x is marginally smaller than y (primitive)

• exists_large : ∃ (x : α), ∃ (y : α), x < y ∧ ¬self.M x y

  Axiom 1: ∃ x y, L(x,y) — largely different elements exist

• m_implies_lt (x y : α) : self.M x y → x < y

  Axiom 2: M(x,y) → R(x,y)

• m_irrelevance (x y z : α) : self.M x y → (z < y ∧ ¬self.M z y → z < x ∧ ¬self.M z x) ∧ (x < z ∧ ¬self.M x z → y < z ∧ ¬self.M y z)

  Axiom 3 (M-IRRELEVANCE): marginal steps preserve large-gap structure

• r_extends_l (x y z : α) : x < y → (y < z ∧ ¬self.M y z → x < z ∧ ¬self.M x z) ∧ (z < x ∧ ¬self.M z x → z < y ∧ ¬self.M z y)

  Axiom 4: R extends along L — smaller-than propagates through large gaps

• decomposition (x y : α) : x < y ∧ ¬self.M x y → (∃ (z : α), self.M x z ∧ z < y ∧ ¬self.M z y) ∧ ∃ (w : α), self.M w y ∧ x < w ∧ ¬self.M x w

  Axiom 5 (DECOMPOSITION): every large gap decomposes via a marginal step

def Semantics.Lexical.Adjective.MLScale.L {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

Largely smaller than (Def 2.1): R(x,y) ∧ ¬M(x,y).

Equations

• ml.L x y = (x < y ∧ ¬ml.M x y)

def Semantics.Lexical.Adjective.MLScale.MarginalDiff {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

Marginal difference (Def 2.3): M(x,y) ∨ M(y,x).

Equations

• ml.MarginalDiff x y = (ml.M x y ∨ ml.M y x)

def Semantics.Lexical.Adjective.MLScale.AtMostMarginal {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

At most marginal difference: x = y ∨ MarginalDiff(x,y). The equivalence relation on degrees induced by M.

Equations

• ml.AtMostMarginal x y = (x = y ∨ ml.MarginalDiff x y)

def Semantics.Lexical.Adjective.MLScale.LargeDiff {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y : α) : Prop

Large difference: L(x,y) ∨ L(y,x).

Equations

• ml.LargeDiff x y = (ml.L x y ∨ ml.L y x)

theorem Semantics.Lexical.Adjective.MLScale.m_transitive {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y z : α) (hxy : ml.M x y) (hyz : ml.M y z) : ml.M x z

Theorem 2.2, part 1 (M-TRANSITIVITY): M is transitive. If x is marginally smaller than y and y marginally smaller than z, then x is marginally smaller than z. Proof: ¬L(y,z) since M(y,z); Axiom 3 contrapositive gives ¬L(x,z); since R(x,z), this forces M(x,z).

theorem Semantics.Lexical.Adjective.MLScale.m_bounded {α : Type u_1} [LinearOrder α] (ml : MLScale α) (x y z : α) (hxz : ml.M x z) (hxy : x < y) (hyz : y < z) : ml.M x y ∧ ml.M y z

Theorem 2.2, part 2 (M-BOUNDEDNESS): if x is marginally smaller than z and y is between them (x < y < z), then both gaps are marginal.