Marginal and large differences

Dinis and Jacinto's ML theory orders degrees by smaller than together with a relation of being marginally smaller. A degree is largely smaller than another when it is smaller but not marginally so. A marginal scale, the theory's ML scale, is a linear order with a marginally-smaller-than relation obeying the five axioms of their 2026 paper, which simplify the original theory of 2025.

Largely smaller than is a strict weak order, and its incomparability relation is at most marginal difference. The degrees therefore fall into order-connected blocks of marginally different degrees, no block having an endpoint that faces another block, and every such partition of a linear order is a marginal scale. Two families of examples are lexicographic pairs of a block and a location within it, among them the representative model ℚ ×ₗ ℤ, and the differences lying in an order-connected subgroup of an ordered group, such as the infinitesimals among the hyperreals.

Main definitions

• Degree.MarginalScale: a marginal scale, with MarginallyLT marginally smaller than, LargelyLT largely smaller than, and AtMostMarginal at most marginal difference.
• Degree.MarginalScale.ofSetoid, Degree.MarginalScale.lex, Degree.MarginalScale.ofAddSubgroup: marginal scales from order-connected partitions, lexicographic pairs, and order-connected subgroups.
• Degree.MarginalScale.IsHom: a homomorphism of marginal scales.

Main statements

• Degree.MarginalScale.atMostMarginal_iff_incompRel: largely smaller than is a strict weak order whose incomparability is at most marginal difference.
• Degree.MarginalScale.ofSetoid_atMostMarginalSetoid: marginal scales correspond to their partitions into blocks.
• Degree.MarginalScale.isHom_lex_iff: a map into a lexicographic marginal scale is a homomorphism exactly when its block coordinate pulls back largely smaller than and its location coordinate grows along marginal steps.

References

• [DJ25]
• [DJ26]

structure Degree.MarginalScale (α : Type u_1) [LinearOrder α] : Type u_1

A marginal scale is a linear order with a relation of being marginally smaller, subject to the five axioms of ML theory. A degree is largely smaller than another when it is smaller but not marginally smaller.

• MarginallyLT : α → α → Prop

  x is marginally smaller than y.

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

  Axiom 1 says that some element is largely smaller than another.

• lt_of_marginallyLT ⦃x y : α⦄ : self.MarginallyLT x y → x < y

  Axiom 2 says that marginally smaller than implies smaller than.

• irrelevance ⦃x y : α⦄ (z : α) : self.MarginallyLT x y → (z < y ∧ ¬self.MarginallyLT z y → z < x ∧ ¬self.MarginallyLT z x) ∧ (x < z ∧ ¬self.MarginallyLT x z → y < z ∧ ¬self.MarginallyLT y z)

  Axiom 3, M-irrelevance, says that when x is marginally smaller than y, whatever is largely smaller than y is largely smaller than x, and y is largely smaller than whatever x is largely smaller than.

• extends_lt ⦃x y : α⦄ (z : α) : x < y → (y < z ∧ ¬self.MarginallyLT y z → x < z ∧ ¬self.MarginallyLT x z) ∧ (z < x ∧ ¬self.MarginallyLT z x → z < y ∧ ¬self.MarginallyLT z y)

  Axiom 4 says that whatever is smaller than something largely smaller than z is largely smaller than z, and whatever is largely smaller than something smaller than z is largely smaller than z.

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

  Axiom 5, Decomposition, says that a large difference is a marginal step followed by a large one, and a large one followed by a marginal step.

def Degree.MarginalScale.LargelyLT {α : Type u_1} [LinearOrder α] (ml : MarginalScale α) (x y : α) : Prop

x is largely smaller than y when it is smaller but not marginally smaller.

Equations

• ml.LargelyLT x y = (x < y ∧ ¬ml.MarginallyLT x y)

def Degree.MarginalScale.AtMostMarginal {α : Type u_1} [LinearOrder α] (ml : MarginalScale α) : α → α → Prop

Two degrees differ at most marginally when they are equal or one is marginally smaller than the other.

Equations

• ml.AtMostMarginal = Relation.ReflGen (Relation.SymmGen ml.MarginallyLT)

theorem Degree.MarginalScale.atMostMarginal_iff {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} : ml.AtMostMarginal x y ↔ x = y ∨ ml.MarginallyLT x y ∨ ml.MarginallyLT y x

theorem Degree.MarginalScale.MarginallyLT.lt {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} (h : ml.MarginallyLT x y) : x < y

theorem Degree.MarginalScale.LargelyLT.lt {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} (h : ml.LargelyLT x y) : x < y

theorem Degree.MarginalScale.MarginallyLT.not_largelyLT {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} (h : ml.MarginallyLT x y) : ¬ml.LargelyLT x y

theorem Degree.MarginalScale.marginallyLT_or_largelyLT_of_lt {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} (h : x < y) : ml.MarginallyLT x y ∨ ml.LargelyLT x y

theorem Degree.MarginalScale.LargelyLT.of_lt_of_largelyLT {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (hxy : x < y) (h : ml.LargelyLT y z) : ml.LargelyLT x z

theorem Degree.MarginalScale.LargelyLT.trans_lt {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (h : ml.LargelyLT x y) (hyz : y < z) : ml.LargelyLT x z

theorem Degree.MarginalScale.LargelyLT.trans {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (hxy : ml.LargelyLT x y) (hyz : ml.LargelyLT y z) : ml.LargelyLT x z

theorem Degree.MarginalScale.MarginallyLT.trans {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (hxy : ml.MarginallyLT x y) (hyz : ml.MarginallyLT y z) : ml.MarginallyLT x z

Marginal steps do not accrue to a large difference.

theorem Degree.MarginalScale.MarginallyLT.bounded {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (hxz : ml.MarginallyLT x z) (hxy : x < y) (hyz : y < z) : ml.MarginallyLT x y ∧ ml.MarginallyLT y z

What lies between marginally different degrees is marginally different from each.

instance Degree.MarginalScale.instIsTransMarginallyLT {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} : IsTrans α ml.MarginallyLT

instance Degree.MarginalScale.instAsymmLargelyLT {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} : Std.Asymm ml.LargelyLT

instance Degree.MarginalScale.instIsOrderConnectedLargelyLT {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} : IsOrderConnected α ml.LargelyLT

Largely smaller than is negatively transitive. When one degree is largely smaller than another, any third degree is largely greater than the first or largely smaller than the second.

instance Degree.MarginalScale.instIsStrictWeakOrderLargelyLT {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} : IsStrictWeakOrder α ml.LargelyLT

theorem Degree.MarginalScale.atMostMarginal_iff_incompRel {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} : ml.AtMostMarginal x y ↔ IncompRel ml.LargelyLT x y

At most marginal difference is incomparability under largely smaller than.

theorem Degree.MarginalScale.AtMostMarginal.refl {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} (x : α) : ml.AtMostMarginal x x

theorem Degree.MarginalScale.AtMostMarginal.symm {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} (h : ml.AtMostMarginal x y) : ml.AtMostMarginal y x

theorem Degree.MarginalScale.AtMostMarginal.trans {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (hxy : ml.AtMostMarginal x y) (hyz : ml.AtMostMarginal y z) : ml.AtMostMarginal x z

def Degree.MarginalScale.atMostMarginalSetoid {α : Type u_1} [LinearOrder α] (ml : MarginalScale α) : Setoid α

At most marginal difference is an equivalence relation, sameness for present purposes.

Equations

• ml.atMostMarginalSetoid = { r := ml.AtMostMarginal, iseqv := ⋯ }

theorem Degree.MarginalScale.AtMostMarginal.largelyLT_congr_left {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (h : ml.AtMostMarginal x y) : ml.LargelyLT x z ↔ ml.LargelyLT y z

theorem Degree.MarginalScale.AtMostMarginal.largelyLT_congr_right {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y z : α} (h : ml.AtMostMarginal y z) : ml.LargelyLT x y ↔ ml.LargelyLT x z

theorem Degree.MarginalScale.marginallyLT_iff_lt_and_atMostMarginal {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} : ml.MarginallyLT x y ↔ x < y ∧ ml.AtMostMarginal x y

Marginally smaller than is smaller than within a block.

theorem Degree.MarginalScale.ordConnected_setOf_atMostMarginal {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} (x : α) : {y : α | ml.AtMostMarginal x y}.OrdConnected

A block of at most marginally different degrees is order-connected.

theorem Degree.MarginalScale.LargelyLT.infinite_setOf {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} (h : ml.LargelyLT x y) : {z : α | ml.MarginallyLT x z ∧ ml.LargelyLT z y}.Infinite

When x is largely smaller than y, infinitely many degrees lie marginally above x and largely below y, since Decomposition gives each such degree a marginally greater one.

theorem Degree.MarginalScale.LargelyLT.infinite_Ioo {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} (h : ml.LargelyLT x y) : (Set.Ioo x y).Infinite

Largely different degrees are infinitely far apart.

theorem Degree.MarginalScale.isUpperSet_setOf_largelyLT {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} (x : α) : IsUpperSet {y : α | ml.LargelyLT x y}

The degrees largely greater than a given one form an upper set.

Constructions

def Degree.MarginalScale.ofSetoid {α : Type u_1} [LinearOrder α] (s : Setoid α) (hconv : ∀ (x : α), {y : α | s x y}.OrdConnected) (hne : ∃ (x : α) (y : α), ¬s x y) (hgt : ∀ ⦃x y : α⦄, x < y → ¬s x y → ∃ (z : α), x < z ∧ s x z) (hlt : ∀ ⦃x y : α⦄, x < y → ¬s x y → ∃ w < y, s w y) : MarginalScale α

A partition of a linear order into order-connected blocks, at least two of them and none with an endpoint facing another block, is a marginal scale whose marginal differences are the differences within a block.

Equations

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

theorem Degree.MarginalScale.ext {α : Type u_1} [LinearOrder α] {ml ml' : MarginalScale α} (h : ∀ (x y : α), ml.MarginallyLT x y ↔ ml'.MarginallyLT x y) : ml = ml'

theorem Degree.MarginalScale.ext_iff {α : Type u_1} [LinearOrder α] {ml ml' : MarginalScale α} : ml = ml' ↔ ∀ (x y : α), ml.MarginallyLT x y ↔ ml'.MarginallyLT x y

theorem Degree.MarginalScale.ofSetoid_atMostMarginalSetoid {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} : ofSetoid ml.atMostMarginalSetoid ⋯ ⋯ ⋯ ⋯ = ml

Every marginal scale is the scale of its partition into blocks of at most marginally different degrees.

theorem Degree.MarginalScale.atMostMarginalSetoid_ofSetoid {α : Type u_1} [LinearOrder α] {s : Setoid α} {hconv : ∀ (x : α), {y : α | s x y}.OrdConnected} {hne : ∃ (x : α) (y : α), ¬s x y} {hgt : ∀ ⦃x y : α⦄, x < y → ¬s x y → ∃ (z : α), x < z ∧ s x z} {hlt : ∀ ⦃x y : α⦄, x < y → ¬s x y → ∃ w < y, s w y} : (ofSetoid s hconv hne hgt hlt).atMostMarginalSetoid = s

The blocks of the scale built from a partition are the cells of the partition.

def Degree.MarginalScale.lex (β : Type u_2) (γ : Type u_3) [LinearOrder β] [LinearOrder γ] [Nontrivial β] [Nonempty γ] [NoMaxOrder γ] [NoMinOrder γ] : MarginalScale (Lex (β × γ))

Lexicographic pairs of a block and a location form a marginal scale in which one pair is marginally smaller than another when they share a block and its location is smaller.

Equations

• Degree.MarginalScale.lex β γ = Degree.MarginalScale.ofSetoid (Setoid.ker fun (p : Lex (β × γ)) => (ofLex p).1) ⋯ ⋯ ⋯ ⋯

theorem Degree.MarginalScale.lex_marginallyLT_iff {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] [Nontrivial β] [Nonempty γ] [NoMaxOrder γ] [NoMinOrder γ] {x y : Lex (β × γ)} : (lex β γ).MarginallyLT x y ↔ (ofLex x).1 = (ofLex y).1 ∧ (ofLex x).2 < (ofLex y).2

theorem Degree.MarginalScale.lex_largelyLT_iff {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] [Nontrivial β] [Nonempty γ] [NoMaxOrder γ] [NoMinOrder γ] {x y : Lex (β × γ)} : (lex β γ).LargelyLT x y ↔ (ofLex x).1 < (ofLex y).1

def Degree.MarginalScale.ofAddSubgroup {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (H : AddSubgroup G) (hconv : (↑H).OrdConnected) (hbot : H ≠ ⊥) (htop : H ≠ ⊤) : MarginalScale G

The differences lying in an order-connected subgroup that is neither trivial nor everything are the marginal differences of a marginal scale.

Equations

• Degree.MarginalScale.ofAddSubgroup H hconv hbot htop = Degree.MarginalScale.ofSetoid (QuotientAddGroup.leftRel H) ⋯ ⋯ ⋯ ⋯

theorem Degree.MarginalScale.ofAddSubgroup_marginallyLT_iff {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} {hconv : (↑H).OrdConnected} {hbot : H ≠ ⊥} {htop : H ≠ ⊤} {x y : G} : (ofAddSubgroup H hconv hbot htop).MarginallyLT x y ↔ x < y ∧ y - x ∈ H

theorem Degree.MarginalScale.atMostMarginalSetoid_ofAddSubgroup {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} {hconv : (↑H).OrdConnected} {hbot : H ≠ ⊥} {htop : H ≠ ⊤} : (ofAddSubgroup H hconv hbot htop).atMostMarginalSetoid = QuotientAddGroup.leftRel H

The blocks of the scale built from a subgroup are its cosets.

theorem Degree.MarginalScale.ofAddSubgroup_atMostMarginal_iff {G : Type u_2} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] {H : AddSubgroup G} {hconv : (↑H).OrdConnected} {hbot : H ≠ ⊥} {htop : H ≠ ⊤} {x y : G} : (ofAddSubgroup H hconv hbot htop).AtMostMarginal x y ↔ y - x ∈ H

Homomorphisms

structure Degree.MarginalScale.IsHom {α : Type u_1} [LinearOrder α] {β : Type u_2} [LinearOrder β] (ml : MarginalScale α) (ml' : MarginalScale β) (f : α → β) : Prop

A homomorphism of marginal scales preserves and reflects smaller than and marginally smaller than.

• strictMono : StrictMono f
• marginallyLT_iff (x y : α) : ml'.MarginallyLT (f x) (f y) ↔ ml.MarginallyLT x y

theorem Degree.MarginalScale.IsHom.largelyLT_iff {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} {β : Type u_2} [LinearOrder β] {ml' : MarginalScale β} {f : α → β} (hf : ml.IsHom ml' f) : ml'.LargelyLT (f x) (f y) ↔ ml.LargelyLT x y

theorem Degree.MarginalScale.isHom_lex_iff {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] [Nontrivial β] [Nonempty γ] [NoMaxOrder γ] [NoMinOrder γ] {f : α → Lex (β × γ)} : ml.IsHom (lex β γ) f ↔ (∀ (x y : α), ml.LargelyLT x y ↔ (ofLex (f x)).1 < (ofLex (f y)).1) ∧ ∀ ⦃x y : α⦄, ml.MarginallyLT x y → (ofLex (f x)).2 < (ofLex (f y)).2

A map into a lexicographic marginal scale is a homomorphism exactly when its block coordinate pulls back largely smaller than and its location coordinate grows along marginal steps.

theorem Degree.MarginalScale.IsHom.fst_eq_fst_iff {α : Type u_1} [LinearOrder α] {ml : MarginalScale α} {x y : α} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] [Nontrivial β] [Nonempty γ] [NoMaxOrder γ] [NoMinOrder γ] {f : α → Lex (β × γ)} (hf : ml.IsHom (lex β γ) f) : (ofLex (f x)).1 = (ofLex (f y)).1 ↔ ml.AtMostMarginal x y