Marginality Scales

[DJ26]

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 PolarMeasure (in Degree): a PolarMeasure determines licensing from boundedness, while an MLScale adds granularity structure (marginal vs. large difference) on the same LinearOrder.

structure DinisJacinto2026.MLScale (α : Type u_1) [LinearOrder α] : Type u_1

ML theory ([DJ26], 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 DinisJacinto2026.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 DinisJacinto2026.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 DinisJacinto2026.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 DinisJacinto2026.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 DinisJacinto2026.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 DinisJacinto2026.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.

Marginality scales ([DJ26])

structure DinisJacinto2026.GradableMLScale (α : Type u_1) [LinearOrder α] (W : Type u_2) extends Degree.PolarMeasure α W : Type (max u_1 u_2)

• boundedness : Boundedness
• μ : W → α
• direction : Core.Order.ScalePolarity
• ml : MLScale α

def DinisJacinto2026.marginalityPositive {α : Type u_1} [LinearOrder α] (ml : MLScale α) (norm degree : α) : Prop

Equations

• DinisJacinto2026.marginalityPositive ml norm degree = ml.L norm degree

theorem DinisJacinto2026.marginality_entails_standard {α : Type u_1} [LinearOrder α] (ml : MLScale α) (norm degree : α) (h : marginalityPositive ml norm degree) : norm < degree