Moon (2026): countability and measured parts in mixed drink nouns

Mixed drink nouns (martini, cappuccino) are count nouns that denote liquids. Moon derives their countability from their part structure: a mixed drink is a mereological sum of ingredient parts standing in a fixed ratio of measures (Recipe, RatioHolds), one of which — the shot of liquor or espresso, the MEASURED PART — supplies the unit of individuation, and the whole is a connected liquid, self-connected in the mereotopological sense of Casati and Varzi and of Grimm under a connection relation C (ConnectedLiquid, Mereology.SelfConnected). The denotation mixedDrinkDen packages Moon's final formula as the existence of a MixedDrinkWitness.

Two consequences carry the countability argument. The sum of two spatially separate drinks is not a connected liquid, so the denotation is not cumulative (not_mixedDrinkDen_of_not_selfConnected), a mereotopological route to non-cumulativity that a bare semilattice lacks, where it comes only from quantization (connectivity_breaks_cum). And a mixed drink has proper parts, so it is not a mereological atom (mixedDrink_not_atom), and the atomicity on which count theories found countability excludes it (atomsOf_excludes_mixed_drinks), while half a drink with its ratios preserved is still a drink, so the denotation is not quantized either (mixedDrink_not_qua). Mixed drinks thus occupy Filip's ¬CUM ∧ ¬QUA middle ground (mixedDrink_middle_ground), and the gap propagates to drinking VPs through middle_ground_stable (mixedDrink_VP_propagation_gap). Multipliers such as double rescale the measured part's ratio constant rather than the whole (doubleRecipe, Wągiel's subatomic quantification), and dry rescales another ingredient's (modifyRatio).

Moon's corpus and judgment data stay in prose: in her COCA counts (Appendix A) cocktail nouns pattern with count nouns on bare plurals and numerals while non-count drink nouns take bare singulars and containers; countability survives coercion contexts such as pitcher of martinis; and who drank more americanos? is ambiguous between volume, portions, and measured parts.

Implementation notes

Self-connection is Moon's (20b), stated with the library's overlap, which unlike (20a) relates non-null parts only; connected liquid (23) is read with this notion rather than the touch-based self-connection of (22), and without its temporal parameter.

References

• [Moo26]
• [CV99], [Fil12], [Gri12], [Kri21], [Wag21]

Mereotopology

inductive Moon2026.Phase : Type

The phases of matter ([Kri21]) are solids, which retain shape, granulars, which are aggregates of discrete pieces, and liquids, whose parts are in constant internal motion.

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

@[instance_reducible]

instance Moon2026.instDecidableEqPhase : DecidableEq Phase

Equations

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

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✝

@[instance_reducible]

instance Moon2026.instReprPhase : Repr Phase

Equations

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

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

A connected liquid (Moon's definition (23), without its temporal parameter) is self-connected with every part liquid.

Equations

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

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

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

A predicate entailing self-connection is not cumulative once two instances have a disconnected sum, so that non-cumulativity comes from connection rather than from quantization (qua_cum_incompatible).

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

With a proper part that is also an instance, such a predicate is neither cumulative nor quantized.

Recipes and the mixed-drink denotation

structure Moon2026.Recipe (α : Type u_1) (K : Type u_2) [Zero K] [LT K] (n : ℕ) : Type (max u_1 u_2)

A mixed drink recipe lists ingredient predicates, positive ratio constants, and the index of the measured part.

• ingredients : Fin n → α → Prop

  Each slot has an ingredient predicate.

• ratios : Fin n → K

  Each slot has a ratio constant.

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

  The measured part is the ingredient that supplies the unit.

def Moon2026.RatioHolds {α : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {n : ℕ} (μ : α → K) (recipe : Recipe α K n) (parts : Fin n → α) : Prop

Moon's ratio constraint requires μ yᵢ / rᵢ = μ yⱼ / rⱼ for all ingredient parts, here in cross-multiplied form.

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} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} (C : α → α → Prop) (recipe : Recipe α K n) (μ : α → K) (phase : α → Phase) (x : α) : Type u_1

A witness that x is a mixed drink under recipe gives non-null, pairwise non-overlapping ingredient parts of x that exhaust it and satisfy their ingredient predicates and the ratio constraint, with x a connected liquid.

• assign : Fin n → α

  Each ingredient slot is filled by an entity.

• part_le (i : Fin n) : self.assign i ≤ x
• present (i : Fin n) : ¬IsBot (self.assign i)
• satisfies (i : Fin n) : recipe.ingredients i (self.assign i)
• ratio : RatioHolds μ recipe self.assign
• disjoint (i j : Fin n) : i ≠ j → ¬Mereology.Overlap (self.assign i) (self.assign j)
• covers (z : α) : z ≤ x → ∃ (i : Fin n), Mereology.Overlap z (self.assign i)
• connected : ConnectedLiquid C phase x

def Moon2026.mixedDrinkDen {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} (C : α → α → Prop) (recipe : Recipe α K n) (μ : α → K) (phase : α → Phase) (x : α) : Prop

The denotation of a mixed drink noun, Moon's final formula, holds of ratio-related ingredient parts forming a connected liquid. The MEASURED PART conjunct, which Moon leaves informal, is recorded only as the recipe's measuredPart index and not imposed as a truth condition, so this is her ratio formula (19) plus CONNECTED LIQUID; she notes that (19) alone also covers ratio-structured non-count drinks such as lemonade.

Equations

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

theorem Moon2026.selfConnected_of_mixedDrinkDen {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} {C : α → α → Prop} {recipe : Recipe α K n} {μ : α → K} {phase : α → Phase} {x : α} (hx : mixedDrinkDen C recipe μ phase x) : Mereology.SelfConnected C x

theorem Moon2026.not_mixedDrinkDen_of_not_selfConnected {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} {C : α → α → Prop} {recipe : Recipe α K n} {μ : α → K} {phase : α → Phase} {x : α} (hDisc : ¬Mereology.SelfConnected C x) : ¬mixedDrinkDen C recipe μ phase x

Two margaritas in separate glasses do not sum to a margarita, since the sum is not a connected liquid.

theorem Moon2026.not_mixedDrinkDen_of_exclusive {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} {C : α → α → Prop} {μ : α → K} {phase : α → Phase} {recipe : Recipe α K (n + 2)} {y : α} (i : Fin (n + 2)) (hExcl : ∀ (j : Fin (n + 2)), j ≠ i → ∀ z ≤ y, ¬recipe.ingredients j z) : ¬mixedDrinkDen C recipe μ phase y

A single ingredient is not the drink, since with at least two ingredients whose extensions are exclusive of one another's parts, an entity all of whose parts are ingredient i fills no other slot.

theorem Moon2026.mixedDrink_not_atom {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} {C : α → α → Prop} {μ : α → K} {phase : α → Phase} {recipe : Recipe α K (n + 2)} {x : α} (hx : mixedDrinkDen C recipe μ phase x) : ¬Mereology.Atom x

A mixed drink has at least two disjoint non-null parts, so it is not an atom.

theorem Moon2026.atomsOf_excludes_mixed_drinks {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} {C : α → α → Prop} {μ : α → K} {phase : α → Phase} {recipe : Recipe α K (n + 2)} (DRINK : α → Prop) {x : α} (hx : mixedDrinkDen C recipe μ phase x) : ¬Number.atomsOf DRINK x

The atoms restriction, individuation as atom-based count theories construe it, excludes mixed drinks, whose unit of individuation is not atomicity but the measured part.

theorem Moon2026.mixedDrink_not_qua {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} {C : α → α → Prop} {recipe : Recipe α K n} {μ : α → K} {phase : α → Phase} {x y : α} (hx : mixedDrinkDen C recipe μ phase x) (hy : mixedDrinkDen C recipe μ phase y) (hlt : y < x) : ¬Mereology.QUA (mixedDrinkDen C recipe μ phase)

Half a margarita with its ratios and connectivity preserved is a margarita, so the denotation is not quantized.

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

Mixed drinks occupy [Fil12]'s middle ground, neither cumulative nor quantized, as an instance of connectivity_middle_ground.

theorem Moon2026.middle_ground_stable {α : Type u_1} [SemilatticeSup α] {β : Type u_3} [SemilatticeSup β] {θ : α → β → Prop} (h : Aspect.SINC θ) (hU : Mereology.UP θ) (hs : Mereology.SUM θ) {OBJ : α → Prop} {a b : α} {e_a e_b : β} (ha : OBJ a) (hb : OBJ b) (hθ_a : θ a e_a) (hθ_b : θ b e_b) (hSum : ¬OBJ (a ⊔ b)) {x y : α} {e_x : β} (hx : OBJ x) (hy : OBJ y) (hlt : y < x) (hθ_x : θ x e_x) : ¬Mereology.CUM (Aspect.VP θ OBJ) ∧ ¬Mereology.QUA (Aspect.VP θ OBJ)

With a strictly incremental verb, an object neither cumulative nor quantized yields a VP neither cumulative nor quantized, as the sum witnesses refute cumulativity and a proper object part, mapped to a proper subevent, refutes quantization.

theorem Moon2026.mixedDrink_VP_propagation_gap {α : Type u_1} {K : Type u_2} [SemilatticeSup α] [Field K] [LinearOrder K] {n : ℕ} {C : α → α → Prop} {recipe : Recipe α K n} {μ : α → K} {phase : α → Phase} {β : Type u_3} [SemilatticeSup β] {drinkTheme : α → β → Prop} (h : Aspect.SINC drinkTheme) (hU : Mereology.UP drinkTheme) (hs : Mereology.SUM drinkTheme) {a b : α} {e_a e_b : β} (ha : mixedDrinkDen C recipe μ phase a) (hb : mixedDrinkDen C recipe μ phase b) (hθ_a : drinkTheme a e_a) (hθ_b : drinkTheme b e_b) (hSum : ¬mixedDrinkDen C recipe μ phase (a ⊔ b)) {x y : α} {e_x : β} (hx : mixedDrinkDen C recipe μ phase x) (hy : mixedDrinkDen C recipe μ phase y) (hlt : y < x) (hθ_x : drinkTheme x e_x) : ¬Mereology.CUM (Aspect.VP drinkTheme (mixedDrinkDen C recipe μ phase)) ∧ ¬Mereology.QUA (Aspect.VP drinkTheme (mixedDrinkDen C recipe μ phase))

The middle ground propagates to VPs, so a strictly incremental drinking verb with a mixed-drink object is neither cumulative nor quantized (middle_ground_stable).

Modifying the ratios

def Moon2026.modifyRatio {α : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {n : ℕ} [IsStrictOrderedRing K] (recipe : Recipe α K n) (target : Fin n) (factor : K) (hPos : 0 < factor) : Recipe α K n

Rescaling one ingredient's ratio constant gives dry martini (Moon's (27b)), which lowers the vermouth relative to the gin.

Equations

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

def Moon2026.doubleRecipe {α : Type u_1} {K : Type u_2} [Field K] [LinearOrder K] {n : ℕ} [IsStrictOrderedRing K] (recipe : Recipe α K n) : Recipe α K n

The multiplier double targets the measured part ([Wag21]), so a double americano has twice the espresso, not twice the volume.

Equations

• Moon2026.doubleRecipe recipe = Moon2026.modifyRatio recipe recipe.measuredPart 2 ⋯

def Moon2026.margaritaRecipe (α : Type u_3) (K : Type u_4) [Field K] [LinearOrder K] [IsStrictOrderedRing K] (tequila tripleSec limeJuice : α → Prop) : Recipe α K 3

A margarita mixes tequila, triple sec and lime juice in ratio 5 : 2 : 3/2, with the tequila as measured part.

Equations

• Moon2026.margaritaRecipe α K tequila tripleSec limeJuice = { ingredients := ![tequila, tripleSec, limeJuice], ratios := ![5, 2, 3 / 2], ratios_pos := ⋯, measuredPart := 0 }