Dinis and Jacinto (2025): A Theory of Marginal and Large Difference

Dinis and Jacinto propose ML theory, eleven axioms on marginally and largely smaller than along a strict weak order, and give it a measurement theory. Every model is infinite, since a large difference decomposes into a marginal step and a further large difference, and the theory has no model on the naturals or the reals, but it has models in nonstandard analysis, where a marginal difference is an infinitesimal one. Every countable, finitely marginal model maps homomorphically into the representative model of rational-indexed blocks of integer-indexed locations, and any two such maps differ by a transformation that rescales blocks and locations within blocks. In a Sorites whose series is infinite, being bald as not being largely less bald than the last member makes the premises jointly satisfiable.

Main statements

• instIsEmptyMarginalScale: no conditionally complete order, such as the naturals or the reals, carries an ML scale.
• exists_isHom_lex_rat_int: every countable, finitely marginal ML scale maps homomorphically into the representative model ℚ ×ₗ ℤ.
• heap_iff_bald: Itzhaki's heaps are exactly what is not largely smaller than a clear case.
• not_transGen_marginallyLT: no finite chain of marginal steps leads from someone not bald to the last member of a Sorites series.

Implementation notes

• The project's ML scales are those of [DJ26], over a linear order with marginally smaller than primitive, and the results after the axioms are stated for them; a homomorphism then preserves and reflects smaller than and marginally smaller than, and is injective.
• The nonstandard models are mathlib's hyperreals, built from the infinitesimal and the finite numbers of [Itz21]. The finite-difference reading of Dean and Itzhaki (§5, §6), stated for nonstandard integers, is taken on the hyperreals.

TODO

• The arithmetical model ℑ1 of §3.2 and the model ℜ with an initial block of §4.3 need a nonstandard model of arithmetic, which mathlib lacks.

References

• [DJ25]
• [DJ26]
• [Dea18]
• [Itz21]

The theory

structure DinisJacinto2025.IsMLModel {β : Type u_2} (R M L : β → β → Prop) : Prop

The eleven axioms of §2 on marginally and largely smaller than, M and L, along a strict weak order R, both relations primitive.

• isStrictWeakOrder : IsStrictWeakOrder β R
• exists_l : ∃ (x : β) (y : β), L x y
• r_of_m ⦃x y : β⦄ : M x y → R x y
• r_of_l ⦃x y : β⦄ : L x y → R x y
• m_trans ⦃x y z : β⦄ : M x y → M y z → M x z
• not_l_of_m ⦃x y : β⦄ : M x y → ¬L x y
• irrelevance ⦃x y : β⦄ (z : β) : M x y → (L z y → L z x) ∧ (L x z → L y z)
• l_of_r_of_l ⦃x y z : β⦄ : R x y → L y z → L x z
• l_of_l_of_r ⦃x y z : β⦄ : L x y → R y z → L x z
• m_or_l_of_r ⦃x y : β⦄ : R x y → M x y ∨ L x y
• decomposition ⦃x y : β⦄ : L x y → (∃ (z : β), M x z ∧ L z y) ∧ ∃ (w : β), M w y ∧ L x w
• m_bounded ⦃x y z : β⦄ : M x z → R x y → R y z → M x y ∧ M y z

theorem DinisJacinto2025.IsMLModel.l_iff {α : Type u_1} [LinearOrder α] {x y : α} {M L : α → α → Prop} (h : IsMLModel (fun (x1 x2 : α) => x1 < x2) M L) : L x y ↔ x < y ∧ ¬M x y

Along a linear order, largely smaller than is smaller than but not marginally smaller than.

instance DinisJacinto2025.instIsEmptyMarginalScale {α : Type u_2} [ConditionallyCompleteLinearOrder α] : IsEmpty (Degree.MarginalScale α)

No conditionally complete linear order carries an ML scale (Theorem 2.12). The supremum of the degrees above x and largely below y would lie in the block of y, and a degree marginally below it would be a smaller upper bound.

theorem DinisJacinto2025.infinite_of_marginalScale {α : Type u_1} [LinearOrder α] (ml : Degree.MarginalScale α) : Infinite α

Every ML scale is infinite (p. 521).

Nonstandard models

noncomputable def DinisJacinto2025.infinitesimal : Degree.MarginalScale ℝ*

The hyperreals with infinitesimal differences marginal, the model ℑ2 of Theorem 3.1.

Equations

• DinisJacinto2025.infinitesimal = Degree.MarginalScale.ofAddSubgroup Itzhaki2021.infinitesimals DinisJacinto2025.infinitesimal._proof_4 ⋯ ⋯

theorem DinisJacinto2025.infinitesimal_marginallyLT_iff {x y : ℝ*} : infinitesimal.MarginallyLT x y ↔ x < y ∧ 0 < ArchimedeanClass.mk (y - x)

noncomputable def DinisJacinto2025.finite : Degree.MarginalScale ℝ*

The hyperreals with finite differences marginal, the reading of Dean (§5) and of Itzhaki (§6).

Equations

• DinisJacinto2025.finite = Degree.MarginalScale.ofAddSubgroup Itzhaki2021.finites DinisJacinto2025.finite._proof_3 ⋯ ⋯

theorem DinisJacinto2025.finite_marginallyLT_iff {x y : ℝ*} : finite.MarginallyLT x y ↔ x < y ∧ 0 ≤ ArchimedeanClass.mk (y - x)

Representation

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

y is a weakly marginal successor of x when x is marginally smaller than y and no degree marginally above x is marginally below y (Definition 4.4).

Equations

• DinisJacinto2025.MarginalSucc ml x y = (ml.MarginallyLT x y ∧ ∀ (z : α), ml.MarginallyLT x z → ¬ml.MarginallyLT z y)

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

An ML scale is finitely marginal when finitely many weakly marginal successions lead from any degree to any marginally greater one (Definition 4.5).

Equations

• DinisJacinto2025.FinitelyMarginal ml = ∀ ⦃x y : α⦄, ml.MarginallyLT x y → Relation.TransGen (DinisJacinto2025.MarginalSucc ml) x y

theorem DinisJacinto2025.MarginalSucc.Icc_subset {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {x y : α} (h : MarginalSucc ml x y) : Set.Icc x y ⊆ {x, y}

theorem DinisJacinto2025.FinitelyMarginal.finite_Icc {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {x y : α} (hf : FinitelyMarginal ml) (h : ml.AtMostMarginal x y) : (Set.Icc x y).Finite

In a finitely marginal ML scale, the closed interval between at most marginally different degrees is finite.

theorem DinisJacinto2025.FinitelyMarginal.finite_Icc_block {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} (hf : FinitelyMarginal ml) (q : Quotient ml.atMostMarginalSetoid) (a b : { y : α // ⟦y⟧ = q }) : (Set.Icc a b).Finite

In a finitely marginal ML scale, every block is locally finite.

theorem DinisJacinto2025.exists_lt_of_marginallyLT {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {γ : Type u_2} [Preorder γ] (h : ∀ (q : Quotient ml.atMostMarginalSetoid), ∃ (g : { y : α // ⟦y⟧ = q } → γ), StrictMono g) : ∃ (G : α → γ), ∀ ⦃x y : α⦄, ml.MarginallyLT x y → G x < G y

When every block embeds in γ, the degrees can be given locations in γ that grow along marginal steps.

theorem DinisJacinto2025.exists_isHom_lex_rat_int {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} [Countable α] (hf : FinitelyMarginal ml) : ∃ (f : α → Lex (ℚ × ℤ)), ml.IsHom (Degree.MarginalScale.lex ℚ ℤ) f

Every countable, finitely marginal ML scale maps homomorphically into the representative model (Theorem 4.7).

theorem DinisJacinto2025.exists_isHom_lex_rat_rat {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} [Countable α] : ∃ (f : α → Lex (ℚ × ℚ)), ml.IsHom (Degree.MarginalScale.lex ℚ ℚ) f

Every countable ML scale maps homomorphically into rational-indexed blocks of rational-indexed locations (§4.4).

Uniqueness

def DinisJacinto2025.CautiouslyMonotone {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] (X : Set (Lex (β × γ))) (τ : Lex (β × γ) → Lex (β × γ)) : Prop

A transformation of a set of pairs is cautiously monotone-increasing when it maps blocks by one strictly increasing map and the locations within each block by strictly increasing maps (Definition 4.8).

Equations

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

theorem DinisJacinto2025.IsHom.comp_cautiouslyMonotone {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] [Nontrivial β] [Nonempty γ] [NoMaxOrder γ] [NoMinOrder γ] {h : α → Lex (β × γ)} (hh : ml.IsHom (Degree.MarginalScale.lex β γ) h) {τ : Lex (β × γ) → Lex (β × γ)} (hτ : CautiouslyMonotone (Set.range h) τ) : ml.IsHom (Degree.MarginalScale.lex β γ) (τ ∘ h)

A representation composed with a cautiously monotone-increasing transformation is a representation (Theorem 4.9).

theorem DinisJacinto2025.IsHom.exists_cautiouslyMonotone {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {β : Type u_2} {γ : Type u_3} [LinearOrder β] [LinearOrder γ] [Nontrivial β] [Nonempty γ] [NoMaxOrder γ] [NoMinOrder γ] {h u : α → Lex (β × γ)} (hh : ml.IsHom (Degree.MarginalScale.lex β γ) h) (hu : ml.IsHom (Degree.MarginalScale.lex β γ) u) : ∃ (τ : Lex (β × γ) → Lex (β × γ)), CautiouslyMonotone (Set.range h) τ ∧ u = τ ∘ h

Any two representations differ by a cautiously monotone-increasing transformation (Theorem 4.9).

The Sorites

def DinisJacinto2025.Bald {α : Type u_1} [LinearOrder α] (ml : Degree.MarginalScale α) (e x : α) : Prop

In the Sorites of §5, to be bald is not to be largely less bald than the last member e of the series.

Equations

• DinisJacinto2025.Bald ml e x = ¬ml.LargelyLT x e

theorem DinisJacinto2025.bald_of_le {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {x e : α} (h : e ≤ x) : Bald ml e x

Whatever is balder than the last member is bald.

theorem DinisJacinto2025.Bald.tolerance {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {x y e : α} : (¬Bald ml e x → ml.MarginallyLT x y → ¬Bald ml e y) ∧ (Bald ml e x → ml.MarginallyLT y x → Bald ml e y)

Baldness is tolerant. What is marginally balder than someone not bald is not bald, and what is marginally less bald than someone bald is bald.

theorem DinisJacinto2025.not_transGen_marginallyLT {α : Type u_1} [LinearOrder α] {ml : Degree.MarginalScale α} {x e : α} (hx : ¬Bald ml e x) : ¬Relation.TransGen ml.MarginallyLT x e

No finite chain of marginal steps leads from someone not bald to the last member, so a series in which each member is marginally balder than the one before satisfies the premises of the Sorites only if it is infinite.

Itzhaki's nonstandard heuristics

theorem DinisJacinto2025.infinitesimal_atMostMarginal_iff {x y : ℝ*} : infinitesimal.AtMostMarginal x y ↔ Itzhaki2021.InfinitesimallyClose x y

Itzhaki's indistinguishability is at most marginal difference on the infinitesimal scale.

theorem DinisJacinto2025.finite_atMostMarginal_iff {x y : ℝ*} : finite.AtMostMarginal x y ↔ Itzhaki2021.FinitelyClose x y

Itzhaki's finite closeness is at most marginal difference on the finite scale (§6).

theorem DinisJacinto2025.finite_largelyLT_iff {x y : ℝ*} : finite.LargelyLT x y ↔ Itzhaki2021.InfinitelyLess x y

Being infinitely less, in Itzhaki's sense, is being largely smaller on the finite scale (§6).

theorem DinisJacinto2025.heap_iff_bald {De : Type u_2} {heap known : De → Prop} [DecidablePred heap] [DecidablePred known] {size : De → ℕ} {H : ℝ*} (hH : ArchimedeanClass.mk H < 0) (hpos : 0 < H) {e x : De} (he : heap e) : heap x ↔ Bald finite (Itzhaki2021.qualSize heap known size H e) (Itzhaki2021.qualSize heap known size H x)

Under Itzhaki's qualitative size, the heaps are exactly what is not largely smaller than a clear case on the finite scale, the baldness of §5 (§6).