Mereology ↔ Scale Bridge

@cite{champollion-2017} @cite{kennedy-2007} @cite{krifka-1989} @cite{krifka-1998} @cite{rouillard-2026}

Cross-pillar connection between Core/Mereology.lean (CUM/QUA/ExtMeasure) and Core/Scale.lean (ComparativeScale/Boundedness/MIP/degree properties).

The two pillars are independently motivated:

• Mereology: algebraic part-whole structure (@cite{krifka-1989}/1998, @cite{champollion-2017})
• Scale: comparative/additive scale structure

This file bridges them at four levels:

• Annotation bridge (§1): QUA ↔ Boundedness.closed, CUM ↔ Boundedness.open_
• Constructor bridge (§2): ExtMeasure → DirectedMeasure
• Structural bridge (§3–4): singleton_qua ↔ .closed, CUM sum extensibility
• Categorical bridge (§11): MereoDim → Monotone, ExtMeasure → Monotone μ

The lax measure square

The @cite{krifka-1989} linking theory involves two dimension chains:

Events →θ Entities →μ ℚ (object dimension)
Events →τ Times →dur ℚ (temporal dimension)

These form a square that commutes laxly: the two paths Events → ℚ need not agree pointwise, but they are related by a proportionality constant (the "rate" of gradual change). This is captured by MeasureProportional (§9) and LaxMeasureSquare (§10) below.

def Mereology.quaBoundedness : Core.Scale.Boundedness

QUA predicates correspond to closed/bounded scales.

Krifka: QUA(P) means P-elements have no P-proper-parts, so measurement reaches a definite value at each P-element — the scale has an inherent endpoint. @cite{kennedy-2007}: closed scales license degree modifiers. @cite{rouillard-2026}: closed scales license temporal in-adverbials.

This is the mereological root of the Kennedy–Rouillard isomorphism: QUA → telic → closed → licensed.

Equations

• Mereology.quaBoundedness = Core.Scale.Boundedness.closed

def Mereology.cumBoundedness : Core.Scale.Boundedness

CUM predicates correspond to open/unbounded scales.

Krifka: CUM(P) means P is closed under ⊔, so measurement can always be extended upward — the scale has no inherent endpoint. @cite{kennedy-2007}: open scales block degree modifiers. @cite{rouillard-2026}: open scales cause information collapse for TIAs.

This is the mereological root: CUM → atelic → open → blocked.

Equations

• Mereology.cumBoundedness = Core.Scale.Boundedness.open_

theorem Mereology.qua_boundedness_licensed : quaBoundedness.isLicensed = true

QUA → licensed: closed scales admit maximally informative elements.

theorem Mereology.cum_boundedness_blocked : cumBoundedness.isLicensed = false

CUM → blocked: open scales have information collapse.

def Mereology.extMeasure_kennedy {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} (_hμ : ExtMeasure α μ) (b : Core.Scale.Boundedness) : Core.Scale.DirectedMeasure ℚ α

An extensive measure induces a Kennedy-style directed measure.

The measure function μ : α → ℚ from ExtMeasure becomes the measure function of a DirectedMeasure (positive direction), with atLeastDeg as the derived degree property (@cite{kennedy-2007}/2015: "at least n" with type-shift to exact). The boundedness annotation comes from the mereological property of the source predicate: QUA → .closed, CUM → .open_.

See also extMeasure_rouillard for the @cite{rouillard-2026} direction (negative → atMostDeg).

Equations

• Mereology.extMeasure_kennedy _hμ b = { boundedness := b, μ := μ }

def Mereology.extMeasure_rouillard {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} (_hμ : ExtMeasure α μ) (b : Core.Scale.Boundedness) : Core.Scale.DirectedMeasure ℚ α

An extensive measure induces a Rouillard-style directed measure.

Same measure function, but with negative direction (deriving atMostDeg as the degree property). @cite{rouillard-2026}: E-TIA semantics uses "at most n" for runtime bounds. Boundedness again from the mereological source predicate.

Equations

• Mereology.extMeasure_rouillard _hμ b = { boundedness := b, μ := μ, direction := Core.Scale.ScalePolarity.negative }

theorem Mereology.qua_kennedy_licensed {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} (hμ : ExtMeasure α μ) : (extMeasure_kennedy hμ quaBoundedness).licensed = true

QUA predicates yield licensed Kennedy directed measures.

theorem Mereology.cum_kennedy_blocked {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} (hμ : ExtMeasure α μ) : (extMeasure_kennedy hμ cumBoundedness).licensed = false

CUM predicates yield blocked Kennedy directed measures.

theorem Mereology.qua_direction_invariant {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} (hμ : ExtMeasure α μ) : (extMeasure_kennedy hμ quaBoundedness).licensed = (extMeasure_rouillard hμ quaBoundedness).licensed

The Kennedy–Rouillard direction invariance for mereological domains: a QUA-induced directed measure is licensed regardless of whether we use Kennedy's atLeastDeg or Rouillard's atMostDeg.

theorem Mereology.singleton_qua_closed (n : ℚ) : (QUA fun (x : ℚ) => x = n) ∧ quaBoundedness = Core.Scale.Boundedness.closed

Singletons are both QUA (mereologically) and closed (scale-theoretically).

singleton_qua n proves {x | x = n} is quantized. A singleton set {n} has both a maximum and minimum (namely n itself), so its scale boundedness is .closed.

This is the base case of the QUA ↔ Boundedness correspondence: the simplest QUA predicate (a singleton) maps to the simplest closed scale (a point). The connection is non-trivial: singleton_qua is proved from lt_irrefl (mereological), while .closed is a scale-theoretic classification — two independent proofs arriving at the same conclusion.

theorem Mereology.extMeasure_singleton_closed {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] (n : ℚ) : (QUA fun (x : α) => μ x = n) ∧ quaBoundedness = Core.Scale.Boundedness.closed

ExtMeasure singletons {x | μ(x) = n} are QUA and correspond to closed scales. Combines extMeasure_qua' (mereological) with the boundedness annotation (scale-theoretic).

This is the measure-theoretic version of singleton_qua_closed: measuring a QUA predicate by an extensive measure yields a singleton on the scale (exactly one measure value), which is closed.

theorem Mereology.cum_sum_exceeds {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] {P : α → Prop} (hCum : CUM P) {x y : α} (hx : P x) (hy : P y) (h_not_le : ¬x ≤ y) : P (x ⊔ y) ∧ μ (x ⊔ y) > μ y

CUM predicates with incomparable elements can always produce larger measure values via sum.

If P is CUM and has elements x, y where x ≤ y fails (they are incomparable), then x ⊔ y satisfies P (by CUM) and μ(x ⊔ y) > μ(y) (because y < x ⊔ y and μ is StrictMono).

This is the structural mechanism behind open/unbounded scales for CUM predicates: given fresh material, CUM can always produce a larger measurement. The incomparability condition is satisfied whenever two P-elements have non-overlapping parts (e.g., two distinct portions of rice, two non-overlapping running events).

theorem Mereology.cum_sum_exceeds_both {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] {P : α → Prop} (hCum : CUM P) {x y : α} (hx : P x) (hy : P y) (hxy : ¬x ≤ y) (hyx : ¬y ≤ x) : P (x ⊔ y) ∧ μ (x ⊔ y) > μ x ∧ μ (x ⊔ y) > μ y

CUM predicates with incomparable elements yield measure values strictly exceeding both inputs.

Symmetric version of cum_sum_exceeds: μ(x ⊔ y) > μ(x) AND μ(x ⊔ y) > μ(y) when x and y are incomparable.

class Mereology.MereoDim {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (d : α → β) : Prop

Morphism class of Mereo^op: the category of partially ordered types with strictly monotone maps. A MereoDim d instance witnesses that d is a mereological dimension — a map along which QUA pulls back.

Unifies three sources of StrictMono:

• ExtMeasure (via extMeasure_strictMono)
• IsSumHom + Injective (via strictMono_of_injective)
• Compositions of the above (Krifka dimension chains)

• toStrictMono : StrictMono d

  The underlying strict monotonicity proof.

instance Mereology.instMereoDimOfExtMeasure {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] : MereoDim μ

Any ExtMeasure is automatically a MereoDim: extensive measures are strictly monotone by extMeasure_strictMono.

def Mereology.MereoDim.ofInjSumHom {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} [hf : IsSumHom f] (hinj : Function.Injective f) : MereoDim f

An injective sum homomorphism is a MereoDim. Not an instance because Function.Injective is not inferrable by typeclass search.

Equations

• ⋯ = ⋯

theorem Mereology.MereoDim.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : β → γ} {g : α → β} (hf : MereoDim f) (hg : MereoDim g) : MereoDim (f ∘ g)

Composition of MereoDim morphisms. Captures Krifka's dimension chains: Events →θ Entities →μ ℚ gives MereoDim (μ ∘ θ) when both components are MereoDim.

Stated as a theorem (not an instance) to avoid typeclass inference loops from decomposing arbitrary composed functions.

theorem Mereology.qua_pullback_mereoDim {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {d : α → β} [hd : MereoDim d] {P : β → Prop} (hP : QUA P) : QUA (P ∘ d)

QUA pullback via MereoDim: typeclass-dispatched version of qua_pullback. When [MereoDim d] is available (automatically for any ExtMeasure), QUA pulls back without manual StrictMono threading.

theorem Mereology.qua_pullback_mereoDim_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {d₁ : α → β} {d₂ : β → γ} (hd₁ : MereoDim d₁) (hd₂ : MereoDim d₂) {P : γ → Prop} (hP : QUA P) : QUA (P ∘ d₂ ∘ d₁)

QUA pullback along a composed dimension chain. Given two MereoDim morphisms d₁ : α → β and d₂ : β → γ, QUA on γ pulls back to QUA on α through the chain d₂ ∘ d₁.

structure Mereology.MeasureProportional {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] (R : α → β → Prop) (μ₁ : α → ℚ) (μ₂ : β → ℚ) : Type

Measure proportionality: two measure functions are proportional on pairs related by a relation R. For any R-pair (x,e), μ₂(e) = rate * μ₁(x) for some positive constant rate.

This captures the idealized "constant rate" linking two dimensions: measuring x is proportional to measuring e whenever R relates them. For instance, in @cite{krifka-1989}'s telicity theory, eating twice as much food takes twice as long, so the object measure and event duration are proportional on θ-related pairs.

• rate : ℚ

  The proportionality constant (rate).

• rate_pos : 0 < self.rate

  The rate is positive.

• proportional (x : α) (e : β) : R x e → μ₂ e = self.rate * μ₁ x

  For any R-pair, μ₂(e) = rate × μ₁(x).

structure Mereology.LaxMeasureSquare {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup γ] (R : α → γ → Prop) (μ₁ : α → ℚ) (f : γ → β) (μ₂ : β → ℚ) : Type

A lax commutative square of mereological dimensions:

α →R γ →f β →μ₂ ℚ (composed path: μ₂ ∘ f)
α →──── μ₁ ────→ ℚ (direct path)

The two paths α → ℚ commute laxly: they don't agree pointwise, but are proportional on R-related pairs (via MeasureProportional). Both paths are required to be extensive measures (ExtMeasure), making them MereoDim morphisms that support QUA pullback.

This is the general mereological square.

• laxComm : MeasureProportional R μ₁ (μ₂ ∘ f)

  Lax commutativity: μ₂(f(e)) = rate * μ₁(x) for R-pairs.

• ext₁ : ExtMeasure α μ₁

  First arm is an extensive measure.

• ext₂ : ExtMeasure γ (μ₂ ∘ f)

  Second arm (composed path) is an extensive measure.

theorem Mereology.LaxMeasureSquare.laxCommutativity {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup γ] {R : α → γ → Prop} {μ₁ : α → ℚ} {f : γ → β} {μ₂ : β → ℚ} (sq : LaxMeasureSquare R μ₁ f μ₂) {x : α} {e : γ} (hR : R x e) : μ₂ (f e) = sq.laxComm.rate * μ₁ x

The defining equation of the lax measure square: for any R-pair (x,e), μ₂(f(e)) = rate * μ₁(x).

theorem Mereology.LaxMeasureSquare.mereoDim₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup γ] {R : α → γ → Prop} {μ₁ : α → ℚ} {f : γ → β} {μ₂ : β → ℚ} (sq : LaxMeasureSquare R μ₁ f μ₂) : MereoDim μ₁

The first arm (direct path) is a MereoDim (via ExtMeasure).

theorem Mereology.LaxMeasureSquare.mereoDim₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup γ] {R : α → γ → Prop} {μ₁ : α → ℚ} {f : γ → β} {μ₂ : β → ℚ} (sq : LaxMeasureSquare R μ₁ f μ₂) : MereoDim (μ₂ ∘ f)

The second arm (composed path) is a MereoDim (via ExtMeasure).

theorem Mereology.LaxMeasureSquare.qua_pullback₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SemilatticeSup α] [SemilatticeSup γ] {R : α → γ → Prop} {μ₁ : α → ℚ} {f : γ → β} {μ₂ : β → ℚ} (sq : LaxMeasureSquare R μ₁ f μ₂) {P : ℚ → Prop} (hP : QUA P) : QUA (P ∘ μ₂ ∘ f)

QUA pullback through the composed path: QUA on ℚ pulls back to QUA on γ via the composed measure μ₂ ∘ f.

The categorical connection

MereoDim is a strengthened morphism: it requires StrictMono (injective monotone map between partial orders), while the categorical morphism of comparative scales is Monotone (between preorders).

Monotone ⊇ MereoDim = injective Monotone (on partial orders)

The bridge theorems below make this precise:

1. Every MereoDim is Monotone (mereoDim_monotone)
2. Every ExtMeasure μ gives Monotone μ (extMeasure_monotone)
3. IsSumHom f → Monotone f (IsSumHom.monotone, already in Mereology.lean)

The forgetful functor from AdditiveScale morphisms (IsSumHom) to ComparativeScale morphisms (Monotone) is just IsSumHom.monotone.

Together with the boundedness annotations (§1: QUA → .closed, CUM → .open_) and the DirectedMeasure constructors (§2), the entire mereological pipeline factors through ComparativeScale:

  (α, ≤) ——MereoDim d——→ (β, ≤) ——ExtMeasure μ——→ (ℚ, ≤)
     ↓ ↓ ↓
ComparativeScale b₁ ComparativeScale b₂ ComparativeScale.closed
     └─────── Monotone ───────┘ │
                └──────────── Monotone ──────────────────┘

theorem Mereology.mereoDim_monotone {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] {d : α → β} (hd : MereoDim d) : Monotone d

Every MereoDim d is Monotone: the forgetful map from the category of partial orders with strict monotone maps to the category of preorders with monotone maps.

theorem Mereology.extMeasure_monotone {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} (hμ : ExtMeasure α μ) : Monotone μ

Every ExtMeasure μ gives a monotone map to (ℚ, ≤).

theorem Mereology.qua_cum_boundedness_coherence : quaBoundedness = Core.Scale.Boundedness.closed ∧ cumBoundedness = Core.Scale.Boundedness.open_

Boundedness coherence: the mereological classification (QUA → .closed, CUM → .open_) is definitional — ComparativeScale is now just a boundedness tag on an ambient preorder, so the classification is stored directly as the boundedness field.

structure Mereology.DimensionChain {Source : Type u_1} {Inter : Type u_2} {Measure : Type u_3} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] (f : Source → Inter) (μ : Inter → Measure) : Prop

A mereological dimension chain: a two-leg pipeline Source →f Inter →μ Measure where both legs are MereoDim. The three canonical instances:

• Temporal: Events →τ Intervals →dur ℚ
• Spatial: Events →σ Paths →dist ℚ
• Object: Events →θ Entities →μ ℚ

• leg₁ : MereoDim f
• leg₂ : MereoDim μ

def Mereology.DimensionChain.composed {Source : Type u_1} {Inter : Type u_2} {Measure : Type u_3} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) : MereoDim (μ ∘ f)

The composed map is a MereoDim.

Equations

• ⋯ = ⋯

theorem Mereology.DimensionChain.qua_transfer {Source : Type u_1} {Inter : Type u_2} {Measure : Type u_3} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) {P : Measure → Prop} (hP : QUA P) : QUA (P ∘ μ ∘ f)

QUA on Measure pulls back to QUA on Source through the full chain.

theorem Mereology.DimensionChain.qua_transfer_leg₁ {Source : Type u_1} {Inter : Type u_2} {Measure : Type u_3} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) {P : Inter → Prop} (hP : QUA P) : QUA (P ∘ f)

QUA on Inter pulls back to QUA on Source through the first leg.

theorem Mereology.DimensionChain.qua_transfer_leg₂ {Source : Type u_1} {Inter : Type u_2} {Measure : Type u_3} [PartialOrder Source] [PartialOrder Inter] [PartialOrder Measure] {f : Source → Inter} {μ : Inter → Measure} (dc : DimensionChain f μ) {P : Measure → Prop} (hP : QUA P) : QUA (P ∘ μ)

QUA on Measure pulls back to QUA on Inter through the second leg.

theorem Mereology.cum_exceeds_source {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] {P : α → Prop} (hCum : CUM P) {x y : α} (hx : P x) (hy : P y) (hyx : ¬y ≤ x) : P (x ⊔ y) ∧ μ (x ⊔ y) > μ x

CUM + fresh incomparable element → exists P-element with strictly larger measure. The structural content of "CUM → open scale."

Given P(x) and fresh y with P(y) and ¬ y ≤ x, then x ⊔ y satisfies P (by CUM) and μ(x ⊔ y) > μ(x) (by StrictMono, since x < x ⊔ y).

theorem Mereology.cum_measure_unbounded {α : Type u_1} [SemilatticeSup α] {μ : α → ℚ} [hμ : ExtMeasure α μ] {P : α → Prop} (hCum : CUM P) {δ : ℚ} (hδ : 0 < δ) (hSupply : ∀ (x : α), P x → ∃ (y : α), P y ∧ ¬Overlap x y ∧ δ ≤ μ y) (x₀ : α) (hx₀ : P x₀) (M : ℚ) : ∃ (z : α), P z ∧ μ z > M

CUM + disjoint fresh supply with minimum measure → measurement unbounded.

If P is CUM and for every P-element x there exists a disjoint P-element y with μ(y) ≥ δ > 0, then P-elements achieve arbitrarily large measure. This is the structural content of information collapse: CUM predicates with enough disjoint material have no inherent measurement ceiling.

The hypothesis requires ¬ Overlap x y (not merely ¬ y ≤ x) because overlap allows the increment μ(x ⊔ y) - μ(x) to shrink to zero, making the series of increments convergent. With ¬ Overlap, additivity gives μ(x ⊔ y) = μ(x) + μ(y) ≥ μ(x) + δ, guaranteeing linear growth.

The proof iterates k disjoint extensions from x₀, each adding at least δ to the measure. By the Archimedean property of ℚ, choosing k > (M - μ(x₀)) / δ suffices.

theorem Mereology.sumHom_qua_pullback_pattern {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} [hf : IsSumHom f] (hinj : Function.Injective f) {P : β → Prop} (hP : QUA P) : QUA (P ∘ f)

The three dimension chains all instantiate the same pattern: IsSumHom + Injective → MereoDim → QUA pullback. This theorem states the pattern for any sum homomorphism.

theorem Mereology.sumHom_cum_pullback_pattern {α : Type u_1} {β : Type u_2} [SemilatticeSup α] [SemilatticeSup β] {f : α → β} [hf : IsSumHom f] {P : β → Prop} (hP : CUM P) : CUM (P ∘ f)

CUM always pulls back through any sum homomorphism (no injectivity needed). All three dimension chains preserve atelicity/cumulativity.

theorem Mereology.krifka_qua_licensed : quaBoundedness.isLicensed = true

Krifka: QUA → closed → licensed.

theorem Mereology.krifka_cum_blocked : cumBoundedness.isLicensed = false

Krifka: CUM → open → blocked.