Moon 2026: Countability and Measured Parts in Mixed Drink Nouns

[Moo26] [Fil12] [CV99] [Kri21]

Mixed drink nouns (martini, cappuccino) are count despite denoting liquids. Moon proposes that their countability derives from a MEASURED PART — an ingredient part (the shot of liquor/espresso) that provides a unit for individuation. This contrasts with standard mass drink nouns (wine, coffee) which lack such a part.

Connection to Filip 2012's three-way classification

Mixed drink predicates instantiate the ¬CUM ∧ ¬QUA middle ground that [Fil12] identifies as a third class beyond CUM (atelic) and QUA (telic). The topological non-cumulativity proved here (not_cum_of_disconnected) plus the algebraic non-quantization (mixedDrink_not_qua) jointly witness Filip's middle ground at the NP level. The propositional substrate for the gap propagating to VPs under SINC + UP + CumTheta verbs lives in Studies/Filip2012.lean as the typeclass-form public API not_cum_vp_of_witnesses and middle_ground_stable (both [IsSincVerb θ]-parametric per mathlib discipline); the bridge in §12 below invokes them directly. Moon's mixed-drink case is the concrete topological witness that Filip's algebraic propagation machinery is designed to consume.

Core Proposal (formula 28)

⟦mixed drink⟧ = λx ∃ȳ₀ⁿ ∃P̄₀ⁿ [x = ⊕ȳ ∧ ∀yᵢ∀Pᵢ[Pᵢ(yᵢ)] ∧ ∃r̄₀ⁿ ∀ȳ₀ⁿ [μ(yᵢ)/rᵢ = μ(yⱼ)/rⱼ] ∧ MEASURED PART(y₀) ∧ CONNECTED LIQUID(x)]

This is built from:

1. Parts in mereological sum — SemilatticeSup (⊔)
2. Ratio constraint — ExtMeasure.μ (extensive measure)
3. Measured part — a distinguished countable ingredient
4. Connected liquid — IsConnected from Mathlib topology

Grounding

Moon concept	Linglib/Mathlib
⊕ (sum)	⊔ (SemilatticeSup)
O (overlap)	Mereology.Overlap
μ (measure)	ExtMeasure.μ
SC (self-connection)	SelfConnected (§ 0) = IsConnected (Set.Iic x)
CONNECTED LIQUID	ConnectedLiquid (§ 0)
QUA/CUM	Mereology.QUA / Mereology.CUM

Key Empirical Claims

1. Mixed drink nouns are syntactically count: pluralize, take numerals, combine with many (not much), accept distributive predicates
2. This is NOT Universal Packager coercion: countability persists in pitcher of martinis, bottomless mimosas (Moon §3.5)
3. Multiplier double targets the MEASURED PART (double americano = double espresso, not double volume), following [Wag21]
4. Quantity judgments are ambiguous between volume, number of portions, and number of measured parts (Moon §4.3.2)

Mereotopological substrate

[CV99] take connection as a mereotopological primitive. Here spatial structure is instead a TopologicalSpace independent of the parthood order (contra OrderTopology), respecting their position that spatial arrangement is irreducible to parthood: entities may share parts without being adjacent, and may touch without sharing parts. Self-connection is IsConnected of the principal downset Set.Iic x — the parts of x, viewed as the region x occupies.

The payoff is a category invisible to pure mereology. In a bare SemilatticeSup, ¬CUM for non-singleton predicates comes from QUA (qua_cum_incompatible). With independent topology the two decouple: join can disconnect two connected entities placed apart (connectivity_breaks_cum), while proper parts can stay connected, so ¬CUM ∧ ¬QUA predicates exist (connectivity_middle_ground). Mixed drink nouns live in exactly this gap: disconnected margaritas are not a margarita (¬CUM), but half a margarita with preserved ratios still is one (¬QUA).

def Moon2026.SelfConnected {α : Type u_1} [Preorder α] [TopologicalSpace α] (x : α) : Prop

Self-connected ([CV99] def 20b): the parts of x — the principal downset Set.Iic x — form a topologically connected set. An atom is trivially self-connected; a scattered aggregate (separate shots of tequila and lime juice at a bar) is not.

Equations

• Moon2026.SelfConnected x = IsConnected (Set.Iic x)

inductive Moon2026.Phase : Type

Phase of matter, [Kri21]'s trichotomy: solids retain shape, granulars are aggregates of discrete solid pieces (rice, sand), liquids have parts in constant internal motion. The distinction drives count/mass behavior of substance nouns: solids and granulars individuate by shape or grain boundaries; liquids lack internal boundaries except via ingredient structure (mixed drinks).

• solid : Phase
• granular : Phase
• liquid : Phase

@[implicit_reducible]

instance Moon2026.instDecidableEqPhase : DecidableEq Phase

Equations

• Moon2026.instDecidableEqPhase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Moon2026.instReprPhase : Repr Phase

Equations

• Moon2026.instReprPhase = { reprPrec := Moon2026.instReprPhase.repr }

def Moon2026.instReprPhase.repr : Phase → ℕ → Std.Format

Equations

• Moon2026.instReprPhase.repr Moon2026.Phase.solid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Moon2026.Phase.solid")).group prec✝
• Moon2026.instReprPhase.repr Moon2026.Phase.granular prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Moon2026.Phase.granular")).group prec✝
• Moon2026.instReprPhase.repr Moon2026.Phase.liquid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Moon2026.Phase.liquid")).group prec✝

@[implicit_reducible]

instance Moon2026.instBEqPhase : BEq Phase

Equations

• Moon2026.instBEqPhase = { beq := Moon2026.instBEqPhase.beq }

def Moon2026.instBEqPhase.beq : Phase → Phase → Bool

Equations

• Moon2026.instBEqPhase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Moon2026.ConnectedLiquid {α : Type u_1} [PartialOrder α] [TopologicalSpace α] (phase : α → Phase) (x : α) : Prop

Connected liquid (Moon's def 23, following [Kri21]): self-connected with every part in liquid phase. The temporal parameter of the paper's definition is omitted (static mereotopology).

Equations

• Moon2026.ConnectedLiquid phase x = (Moon2026.SelfConnected x ∧ ∀ y ≤ x, phase y = Moon2026.Phase.liquid)

theorem Moon2026.ConnectedLiquid.selfConnected {α : Type u_1} [PartialOrder α] [TopologicalSpace α] {phase : α → Phase} {x : α} (h : ConnectedLiquid phase x) : SelfConnected x

theorem Moon2026.connectivity_breaks_cum {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {P : α → Prop} (hConn : ∀ (x : α), P x → SelfConnected x) {x y : α} (hx : P x) (hy : P y) (hDisc : ¬SelfConnected (x ⊔ y)) : ¬Mereology.CUM P

Any predicate entailing self-connectivity fails CUM when two instances have a disconnected join — the topological source of non-cumulativity, orthogonal to the algebraic one (QUA, qua_cum_incompatible).

theorem Moon2026.connectivity_middle_ground {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {P : α → Prop} (hConn : ∀ (x : α), P x → SelfConnected x) {a b : α} (ha : P a) (hb : P b) (hDisc : ¬SelfConnected (a ⊔ b)) {x y : α} (hx : P x) (hy : P y) (hlt : y < x) : ¬Mereology.CUM P ∧ ¬Mereology.QUA P

¬CUM ∧ ¬QUA from connectivity: the middle ground between mass and standard count that pure mereology cannot express.

structure Moon2026.Recipe (α : Type u_2) (n : ℕ) : Type u_2

A mixed drink recipe: ingredient predicates, ratio constants, and an index identifying which ingredient is the MEASURED PART.

Example: a margarita has 3 ingredients (tequila, triple sec, lime juice) in ratio 5:2:1.5, and the measured part is the tequila (index 0).

• ingredients : Fin n → α → Prop

  Ingredient predicates (e.g., TEQUILA, TRIPLE_SEC, LIME_JUICE)

• ratios : Fin n → ℚ

  Ratio constants (e.g., 5, 2, 3/2 for a margarita). All positive.

• ratios_pos (i : Fin n) : 0 < self.ratios i

  All ratio constants are positive.

• measuredPart : Fin n

  Index of the measured part (the individuating ingredient).

def Moon2026.RatioHolds {α : Type u_1} {n : ℕ} (μ : α → ℚ) (recipe : Recipe α n) (parts : Fin n → α) : Prop

The ratio constraint between parts of a mixed drink: μ(yᵢ)/rᵢ = μ(yⱼ)/rⱼ for all pairs of parts.

This captures that it is the ratio between ingredients that defines the drink, not the absolute measurements. A margarita is 5:2:1.5 whether made with 50ml, 20ml, 15ml or with 100ml, 40ml, 30ml of the respective ingredients.

Uses ExtMeasure.μ from Semantics/Mereology.lean.

Equations

• Moon2026.RatioHolds μ recipe parts = ∀ (i j : Fin n), μ (parts i) * recipe.ratios j = μ (parts j) * recipe.ratios i

structure Moon2026.MixedDrinkWitness {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α n) (μ : α → ℚ) (phase : α → Phase) (x : α) : Type u_1

Witness structure for a mixed drink: the ingredient parts that compose the drink, satisfying all constraints.

• assign : Fin n → α

  Assignment of entities to ingredient slots

• part_le (i : Fin n) : self.assign i ≤ x

  Each part is a part of the whole

• satisfies (i : Fin n) : recipe.ingredients i (self.assign i)

  Each part satisfies its ingredient predicate

• ratio : RatioHolds μ recipe self.assign

  Ratio constraint holds between all parts

• disjoint (i j : Fin n) : i ≠ j → ¬Mereology.Overlap (self.assign i) (self.assign j)

  Parts don't overlap pairwise (they are distinct ingredients)

• covers (z : α) : z ≤ x → ∃ (i : Fin n), Mereology.Overlap z (self.assign i)

  The parts exhaust the whole: every part of x overlaps some ingredient. Moon's x = ⊕ȳ requires the ingredients to cover x completely — no extra material beyond the recipe components.

• connected : ConnectedLiquid phase x

  The whole is a connected liquid

def Moon2026.mixedDrinkDen {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α n) (μ : α → ℚ) (phase : α → Phase) (x : α) : Prop

The denotation of a mixed drink noun, following Moon's formula (28).

An entity x is a mixed drink if:

1. It has ingredient parts satisfying the recipe predicates
2. The parts stand in the correct ratio (via μ)
3. The parts are pairwise non-overlapping
4. The whole is a connected liquid (self-connected, all parts liquid)

The MEASURED PART is the ingredient at recipe.measuredPart — it provides the unit for individuation and is what double targets ([Wag21]).

TODO: formula (28)'s MEASURED PART(y₀) conjunct is not imposed as a truth condition — recipe.measuredPart only records which index is the measured part (consumed by doubleRecipe); no MixedDrinkWitness field asserts it is individuable. So this denotation is Moon's earlier formula (19) plus CONNECTED LIQUID, and [Moo26] notes (19) over-generates to ratio-structured mass mixtures like lemonade. The ¬CUM and ¬QUA results below are unaffected (they use only connectivity and the witness), but the denotation does not yet separate a margarita from ratioed lemonade. Encoding it needs truth conditions for MEASURED PART, which [Moo26] leaves informal.

Equations

• Moon2026.mixedDrinkDen recipe μ phase x = Nonempty (Moon2026.MixedDrinkWitness recipe μ phase x)

theorem Moon2026.not_cum_of_disconnected {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α n) (μ : α → ℚ) (phase : α → Phase) {m₁ m₂ : α} (_hm₁ : mixedDrinkDen recipe μ phase m₁) (_hm₂ : mixedDrinkDen recipe μ phase m₂) (hDisc : ¬SelfConnected (m₁ ⊔ m₂)) : ¬mixedDrinkDen recipe μ phase (m₁ ⊔ m₂)

CUM fails for mixed drink denotations because the join of two disconnected mixed drinks is not a connected liquid.

If m₁ and m₂ are two separate margaritas (in different glasses), their mereological sum m₁ ⊔ m₂ is not self-connected: the set {y | y ≤ m₁ ⊔ m₂} has a non-trivial open partition separating the two glasses. Therefore ConnectedLiquid phase (m₁ ⊔ m₂) fails, so m₁ ⊔ m₂ does not satisfy the mixed drink denotation.

This is the key asymmetry with mass nouns like wine: wine does not require self-connection, so pouring two wines together yields more wine (CUM holds).

theorem Moon2026.single_ingredient_not_mixed_drink {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α (n + 2)) (μ : α → ℚ) (phase : α → Phase) {y : α} (i : Fin (n + 2)) (_hIngr : recipe.ingredients i y) (hExcl : ∀ (j : Fin (n + 2)), j ≠ i → ∀ z ≤ y, ¬recipe.ingredients j z) : ¬mixedDrinkDen recipe μ phase y

DIV fails for mixed drink denotations because a single ingredient part does not satisfy the full recipe (it lacks the other ingredients).

For example, just the tequila in a margarita is not itself a margarita: it satisfies TEQUILA but not TRIPLE_SEC or LIME_JUICE. With n ≥ 2 ingredients, no single part can fill all ingredient slots.

This is why mixed drinks are count: proper parts fail the predicate (QUA-like behavior).

def Moon2026.doubleRecipe {α : Type u_1} {n : ℕ} (recipe : Recipe α n) : Recipe α n

The multiplier reading of double: scales the measured part.

Double americano = an americano with 2× the measured part (espresso). The multiplier targets recipe.measuredPart, not the whole drink. Following [Wag21]'s subatomic quantification: multipliers access semantically salient parts of an entity.

A double mixed drink has the same recipe but with the measured part's ratio constant doubled — changing the ratio between parts while keeping the recipe structure.

Equations

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

def Moon2026.modifyRatio {α : Type u_1} {n : ℕ} (recipe : Recipe α n) (target : Fin n) (factor : ℚ) (hPos : 0 < factor) : Recipe α n

Dry martini: reduces the non-measured-part ratio (vermouth). Moon (27b): a modifier that changes the ratio relationship between parts. This is a recipe-level operation, not an entity-level one.

Equations

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

inductive Moon2026.CountabilityContext : Type

Countability diagnostic contexts for nouns. Moon §3: mixed drink nouns pattern with count nouns across all tests. Table 1 (Appendix A): COCA corpus percentages.

• bareSg : CountabilityContext

  Bare singular (*a margarita, *milk)

• barePl : CountabilityContext

  Bare plural (margaritas, *milks)

• unit : CountabilityContext

  With unit/numeral (two martinis, *two milks)

• containerSg : CountabilityContext

  Container/measure singular (a glass of wine, a bottle of beer)

• containerPl : CountabilityContext

  Container/measure plural

@[implicit_reducible]

instance Moon2026.instDecidableEqCountabilityContext : DecidableEq CountabilityContext

Equations

• Moon2026.instDecidableEqCountabilityContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Moon2026.instReprCountabilityContext.repr : CountabilityContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Moon2026.instReprCountabilityContext : Repr CountabilityContext

Equations

• Moon2026.instReprCountabilityContext = { reprPrec := Moon2026.instReprCountabilityContext.repr }

structure Moon2026.CorpusDistribution : Type

Corpus distribution for a noun across countability contexts. Percentages from Moon 2026, Table 1 (COCA data).

• noun : String
• bareSg : Float
• barePl : Float
• unit : Float
• containerSg : Float
• containerPl : Float

def Moon2026.instReprCorpusDistribution.repr : CorpusDistribution → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Moon2026.instReprCorpusDistribution : Repr CorpusDistribution

Equations

• Moon2026.instReprCorpusDistribution = { reprPrec := Moon2026.instReprCorpusDistribution.repr }

def Moon2026.cocktailAvg : CorpusDistribution

Cocktail noun group averages (Moon Table 1).

Equations

• Moon2026.cocktailAvg = { noun := "cocktail_avg", bareSg := 2.17, barePl := 31.65, unit := 31.97, containerSg := 0.22, containerPl := 1.25 }

def Moon2026.nonCountDrinkAvg : CorpusDistribution

Non-count drink noun group averages (Moon Table 1).

Equations

• Moon2026.nonCountDrinkAvg = { noun := "noncount_drink_avg", bareSg := 45.73, barePl := 1.94, unit := 5.15, containerSg := 14.96, containerPl := 0.0 }

def Moon2026.distributionalAsymmetry : Prop

The key distributional asymmetry: cocktails have high bare-plural and unit/numeral rates (count behavior), while non-count drinks have high bare-singular and container rates (mass behavior). χ²(3, N = 1361) = 858.29, p < .001, V = .79

Equations

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

inductive Moon2026.QuantityDimension : Type

Dimensions along which "who has more margaritas?" can be judged.

Moon §4.3.2: Traditional quantity judgment tests assume two dimensions (number vs volume). Mixed drink nouns reveal a third: number of measured parts (shots of alcohol/espresso).

• volume : QuantityDimension

  Total volume of liquid

• portions : QuantityDimension

  Number of standard portions (glasses)

• measuredParts : QuantityDimension

  Number of measured parts (shots of base spirit/espresso)

@[implicit_reducible]

instance Moon2026.instDecidableEqQuantityDimension : DecidableEq QuantityDimension

Equations

• Moon2026.instDecidableEqQuantityDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Moon2026.instReprQuantityDimension : Repr QuantityDimension

Equations

• Moon2026.instReprQuantityDimension = { reprPrec := Moon2026.instReprQuantityDimension.repr }

def Moon2026.instReprQuantityDimension.repr : QuantityDimension → ℕ → Std.Format

Equations

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

structure Moon2026.AmericanoScenario : Type

Moon's scenario: person A drinks two single-shot 16oz americanos, person B drinks two quadruple-shot 12oz americanos.

• By volume: A drank more (32oz > 24oz)
• By portions: tied (2 each)
• By measured parts: B drank more (8 shots > 2 shots)

"Who drank more americanos?" is genuinely ambiguous.

• personA_portions : ℕ
• personA_shots_per : ℕ
• personA_oz_per : ℕ
• personB_portions : ℕ
• personB_shots_per : ℕ
• personB_oz_per : ℕ

def Moon2026.americanoExample : AmericanoScenario

Equations

• Moon2026.americanoExample = { }

theorem Moon2026.americano_volume_A_more : americanoExample.personA_portions * americanoExample.personA_oz_per > americanoExample.personB_portions * americanoExample.personB_oz_per

theorem Moon2026.americano_portions_tied : americanoExample.personA_portions = americanoExample.personB_portions

theorem Moon2026.americano_shots_B_more : americanoExample.personB_portions * americanoExample.personB_shots_per > americanoExample.personA_portions * americanoExample.personA_shots_per

def Moon2026.margaritaRecipe (α : Type u_2) (tequila tripleSec limeJuice : α → Prop) : Recipe α 3

Margarita recipe: tequila (ratio 5), triple sec (ratio 2), lime juice (ratio 3/2). Measured part = tequila (index 0). IBA specification: 50ml tequila, 20ml triple sec, 15ml lime juice.

Equations

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

@[reducible, inline]

abbrev Moon2026.substanceNounDen {α : Type u_1} (substancePred : α → Prop) : α → Prop

Substance noun denotation (wine, coffee, water): the predicate holds of any portion of the substance, with no recipe, ratio, or connectivity constraint.

This is the key contrast with mixed drink nouns. Wine-stuff satisfies WINE regardless of shape, contiguity, or internal structure. Two disconnected puddles of wine are still wine. This makes the denotation cumulative: combining wine with wine gives wine.

Equations

• Moon2026.substanceNounDen substancePred = substancePred

theorem Moon2026.substanceNoun_cum {β : Type u_2} [SemilatticeSup β] (substancePred : β → Prop) (hCum : Mereology.CUM substancePred) : Mereology.CUM (substanceNounDen substancePred)

Substance noun denotations are CUM when the underlying substance predicate is CUM. This is trivially true because the denotation IS the substance predicate — no additional constraints to break closure.

Contrast with not_cum_of_disconnected: mixed drink denotations fail CUM because ConnectedLiquid rejects disconnected sums.

Since [Chi98]'s IsMass implies CUM (via isMass_cum in Semantics/Lexical/Noun/Kind/NMP.lean), this means substance nouns can be mass. Mixed drink nouns cannot — their denotation fails CUM, hence fails IsMass.

theorem Moon2026.mass_count_asymmetry {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] (substancePred : α → Prop) (hCum : Mereology.CUM substancePred) {n : ℕ} (recipe : Recipe α n) (μ : α → ℚ) (phase : α → Phase) {m₁ m₂ : α} (_hm₁ : mixedDrinkDen recipe μ phase m₁) (_hm₂ : mixedDrinkDen recipe μ phase m₂) (hDisc : ¬SelfConnected (m₁ ⊔ m₂)) : Mereology.CUM (substanceNounDen substancePred) ∧ ¬mixedDrinkDen recipe μ phase (m₁ ⊔ m₂)

The core mass/count asymmetry from Moon 2026:

• Substance nouns (wine, coffee): CUM holds, QUA fails → mass behavior (bare singular OK, *two wines needs coercion)
• Mixed drink nouns (martini, americano): CUM fails (via ConnectedLiquid), QUA-like behavior → count (pluralizes, takes numerals, *much martini)

The only structural difference is the ConnectedLiquid + recipe constraint. Both denote liquids. The measured part provides the individuation unit that makes mixed drinks countable.

Why Div fails for mixed drinks

[Bor05]'s individuation operator Div(P) = {x ∈ P | Atom(x)} produces count readings by restricting a cumulative root to mereological atoms — entities with no proper parts. This works for standard count nouns: "a beer" is an atomic portion of beer-stuff, "a cat" is an atomic cat-individual.

Mixed drink nouns break this pattern. A margarita is NOT a mereological atom: it has proper parts (the tequila, the triple sec, the lime juice). These ingredient parts are strictly below the whole in the parthood ordering, so Atom x fails. Borer's standard Div therefore excludes mixed drinks from the individuated extension.

Moon's recipe semantics provides an alternative individuation mechanism that fills the same structural role (Borer's Q head) but operates through topological connectivity rather than mereological atomicity:

Mechanism	Q-head content	Source of ¬CUM
Borer Div	P ∧ Atom	Atoms have no proper parts → QUA
Moon recipe	MixedDrinkWitness	ConnectedLiquid rejects disconnected sums

Both break cumulativity of the root predicate (the universal semantic role of Q), but through orthogonal properties of the parthood lattice: the algebraic (atomicity) versus the topological (connectivity).

theorem Moon2026.mixedDrink_not_atom {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α (n + 2)) (μ : α → ℚ) (phase : α → Phase) {x : α} (hx : mixedDrinkDen recipe μ phase x) : ¬Mereology.Atom x

Mixed drinks are not mereological atoms: they have proper parts (their ingredient components).

A MixedDrinkWitness for a recipe with n + 2 ≥ 2 ingredients assigns at least two disjoint parts (assign 0, assign 1) below x. If x were an atom, both would equal x — but then they would overlap, contradicting disjoint.

theorem Moon2026.div_excludes_mixed_drinks {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α (n + 2)) (μ : α → ℚ) (phase : α → Phase) (DRINK : α → Prop) {x : α} (hx : mixedDrinkDen recipe μ phase x) : ¬Borer2005.Div DRINK x

Borer's standard Div excludes mixed drinks from the individuated extension. Since mixed drinks are not atoms (mixedDrink_not_atom), no mixed drink entity satisfies Div(DRINK) for any predicate DRINK.

This is not a bug in Borer's theory — it reveals that the Q head for mixed drink nouns must be filled with a DIFFERENT individuation mechanism than standard Div. Moon's recipe structure provides this.

theorem Moon2026.both_break_cum {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α n) (μ : α → ℚ) (phase : α → Phase) (P : α → Prop) : Mereology.QUA (Borer2005.Div P) ∧ ∀ (m₁ m₂ : α), mixedDrinkDen recipe μ phase m₁ → mixedDrinkDen recipe μ phase m₂ → ¬SelfConnected (m₁ ⊔ m₂) → ¬mixedDrinkDen recipe μ phase (m₁ ⊔ m₂)

Both Borer's Div and Moon's recipe semantics break cumulativity of the root predicate — the universal semantic role of Borer's Q head.

• Div(P) is QUA (stronger: no proper part satisfies the predicate)
• mixedDrinkDen fails CUM (weaker: disconnected sums are rejected)

The asymmetry in strength reflects the different mechanisms: atomicity is a STRONGER individuation than connectivity. Atoms have no proper parts at all; connected liquids can have proper parts (the ingredients) but cannot be merged across spatial gaps.

This means mixed drink nouns are "less quantized" than standard count nouns — a prediction that aligns with Moon's observation that quantity judgments for mixed drinks are genuinely ambiguous across volume, portions, and measured parts (§4.3.2). Standard count nouns like "cat" admit no such ambiguity.

theorem Moon2026.mixedDrink_not_qua {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α (n + 2)) (μ : α → ℚ) (phase : α → Phase) {x y : α} (hx : mixedDrinkDen recipe μ phase x) (hy : mixedDrinkDen recipe μ phase y) (hlt : y < x) : ¬Mereology.QUA (mixedDrinkDen recipe μ phase)

Mixed drinks are divisible: a proper part of a mixed drink can itself be a mixed drink (half a margarita is still a margarita, if the ratios and connectivity are preserved).

This means mixed drink predicates are NOT QUA — unlike Div-based count nouns, which are QUA by div_qua. Mixed drinks occupy a middle ground: ¬CUM (from ConnectedLiquid) but also ¬QUA (from divisibility). This is the formal content of Moon's claim that mixed drinks require a novel individuation mechanism beyond standard mereological atomicity.

Compare Borer's same_root_mass_and_count: the root √BEER is CUM ∧ Div(√BEER) is QUA. For mixed drinks: the recipe denotation is ¬CUM ∧ ¬QUA — neither mass nor count in Borer's strict sense, but count in DISTRIBUTIONAL behavior (pluralizes, takes numerals).

Mixed drinks as an instance of topological non-cumulativity

The general principle (connectivity_middle_ground, § 0) states that ANY predicate entailing self-connectivity occupies the ¬CUM ∧ ¬QUA middle ground given appropriate witnesses. Mixed drink denotations are an instance: ConnectedLiquid entails SelfConnected, providing the connectivity constraint.

This shows Moon's result is not ad hoc — it follows from a structural theorem about the interaction of semilattice join and topological connectivity. Any predicate that requires spatial contiguity of its instances will exhibit the same pattern: non-cumulativity from topology rather than atomicity.

theorem Moon2026.mixedDrinkDen_selfConnected {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α n) (μ : α → ℚ) (phase : α → Phase) (x : α) (hx : mixedDrinkDen recipe μ phase x) : SelfConnected x

The connectivity constraint on mixed drink denotations: any mixed drink is self-connected (extracted from ConnectedLiquid in the witness). This is the hypothesis that feeds the general connectivity_breaks_cum principle.

theorem Moon2026.mixedDrink_middle_ground {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {n : ℕ} (recipe : Recipe α (n + 2)) (μ : α → ℚ) (phase : α → Phase) {a b : α} (ha : mixedDrinkDen recipe μ phase a) (hb : mixedDrinkDen recipe μ phase b) (hDisc : ¬SelfConnected (a ⊔ b)) {x y : α} (hx : mixedDrinkDen recipe μ phase x) (hy : mixedDrinkDen recipe μ phase y) (hlt : y < x) : ¬Mereology.CUM (mixedDrinkDen recipe μ phase) ∧ ¬Mereology.QUA (mixedDrinkDen recipe μ phase)

Mixed drinks are in the ¬CUM ∧ ¬QUA middle ground: an instance of the general connectivity_middle_ground theorem.

The general principle requires:

1. A connectivity constraint (mixedDrinkDen_selfConnected)
2. Two instances with a disconnected join (CUM failure witnesses)
3. An instance with a proper part also satisfying P (QUA failure)

Moon's empirical contribution is establishing that mixed drinks satisfy all three conditions. The formal contribution of connectivity_middle_ground is showing this pattern is necessary — not contingent on the specific recipe structure but a consequence of ANY predicate that requires topological connectivity.

From NP-level gap to VP-level gap

Sections 4 and 10–11 establish that mixed-drink predicates occupy the NP-level ¬CUM ∧ ¬QUA middle ground that [Fil12] identifies. [Kri98]'s CUM/QUA propagation machinery (§3.3, formalised in Studies/Filip2012.lean's middle_ground_stable) shows the gap propagates to VPs under SINC + UP + CumTheta verbs.

The bridge below directly invokes Filip2012's typeclass-form middle_ground_stable on mixed-drink denotations. The ¬CUM and ¬QUA witnesses on OBJ are exactly what not_cum_of_disconnected and mixedDrink_not_qua produce in this file — Moon's empirical contribution feeds Filip's algebraic machinery in a single Lean term.

theorem Moon2026.mixedDrink_VP_propagation_gap {α : Type u_1} [SemilatticeSup α] [TopologicalSpace α] {β : Type u_2} [SemilatticeSup β] {n : ℕ} (recipe : Recipe α n) (μ : α → ℚ) (phase : α → Phase) (drinkTheme : α → β → Prop) [Semantics.Aspect.Incremental.IsSincVerb drinkTheme] {a b : α} {e_a e_b : β} (ha : mixedDrinkDen recipe μ phase a) (hb : mixedDrinkDen recipe μ phase b) (hθ_a : drinkTheme a e_a) (hθ_b : drinkTheme b e_b) (hSum : ¬mixedDrinkDen recipe μ phase (a ⊔ b)) {x y : α} {e_x : β} (hx : mixedDrinkDen recipe μ phase x) (hy : mixedDrinkDen recipe μ phase y) (hlt : y < x) (hθ_x : drinkTheme x e_x) : ¬Mereology.CUM (Semantics.Aspect.Cumulativity.VP drinkTheme (mixedDrinkDen recipe μ phase)) ∧ ¬Mereology.QUA (Semantics.Aspect.Cumulativity.VP drinkTheme (mixedDrinkDen recipe μ phase))

Mixed-drink denotations (Moon 2026) instantiate the ¬CUM ∧ ¬QUA middle ground that [Fil12] identifies. When a SINC drinking verb (typeclass IsSincVerb) takes a mixed-drink object, the resulting drinking-mixed-drink VP inherits the gap.

The α-side witnesses (ha, hb, hSum, hx, hy, hlt) are produced by not_cum_of_disconnected and mixedDrink_not_qua together with Moon's recipe semantics. The β-side hypotheses (hθ_a, hθ_b, hθ_x) are existential closures of the verb's incremental theme over concrete drinking events.

Direct invocation of substrate's typeclass-form middle_ground_stable.