Dimensional Aggregation for Multidimensional Predicates

@cite{dambrosio-hedden-2024} @cite{sassoon-2013} @cite{waldon-etal-2023} @cite{sassoon-fadlon-2017} @cite{tham-2025} @cite{solt-2018-proportional}

General mechanisms for combining dimensional assessments into overall predicate application. These apply to any multi-dimensional predicate — gradable adjectives (Sassoon, D'Ambrosio-Hedden), artifact nouns (Waldon, Sassoon-Fadlon), disturbance predicates (Tham), and proportional measures for vague quantity expressions (Solt).

Aggregation is analogous to preference aggregation in social choice theory. Arrow's impossibility theorem and its escape routes characterize the available aggregation functions:

• Counting (§1): x is F iff ≥k dimensions are satisfied. Subsumes Sassoon's conjunctive (k=n) and disjunctive (k=1).
• Majority (§1): x is F iff a strict majority of dimensions are satisfied.
• Weighted (§2): x is F iff Σᵢ wᵢ·fᵢ(x) ≥ θ (utilitarian aggregation). Subsumes Waldon et al.'s eq. 8.
• Spatially-normalized weighted (§2): x is F iff (Σᵢ wᵢ·fᵢ(x)) / s(x) ≥ θ, where s : α → ℚ is a host-extent measure. Tham 2025's eq. 47b for physical disturbance adjectives.
• Multiplicative (§4): x is F iff Πᵢ fᵢ(x) ≥ θ (Cobb-Douglas aggregation). Sassoon-Fadlon argue natural kinds compose multiplicatively.

Plus §6 Sassoon 2013 subsumption theorems showing all binding types reduce to counting aggregation.

This file consolidates the previous Theories/Semantics/Degree/Aggregation.lean

• Theories/Semantics/Gradability/Aggregation.lean (shim) per master plan v4 Phase C.4 (no-backcompat fix).

def Semantics.Gradability.Aggregation.countBinding {α : Type} (k : ℕ) (dims : List (α → Bool)) (x : α) : Bool

Counting aggregation: x satisfies the predicate iff at least k of the dimension predicates in dims return true for x.

Generalizes @cite{sassoon-2013}'s binding types:

• k = dims.length → conjunctive (∀ dims)
• k = 1 → disjunctive (∃ dim)
• intermediate k → mixed / "dimension counting"

Equations

• Semantics.Gradability.Aggregation.countBinding k dims x = decide ((List.filter (fun (d : α → Bool) => d x) dims).length ≥ k)

def Semantics.Gradability.Aggregation.majorityBinding {α : Type} (dims : List (α → Bool)) (x : α) : Bool

Majority binding: x satisfies the predicate iff a strict majority of dimensions are satisfied. May's theorem (1952) characterizes this as the unique aggregation rule satisfying neutrality, anonymity, and positive responsiveness.

Equations

• Semantics.Gradability.Aggregation.majorityBinding dims x = decide (2 * (List.filter (fun (d : α → Bool) => d x) dims).length > dims.length)

def Semantics.Gradability.Aggregation.boolMeasures {α : Type} (dims : List (α → Bool)) : List (α → ℚ)

Lift Bool dimension predicates to ℚ-valued measure functions. Each d : α → Bool becomes fun x => if d x then 1 else 0.

Equations

• Semantics.Gradability.Aggregation.boolMeasures dims = List.map (fun (d : α → Bool) (x : α) => if d x = true then 1 else 0) dims

def Semantics.Gradability.Aggregation.weightedScore {α : Type} (weights : List ℚ) (measures : List (α → ℚ)) (x : α) : ℚ

Weighted score: Σᵢ wᵢ · fᵢ(x), where each fᵢ : α → ℚ is a measure function along one dimension.

This is the unified core: @cite{waldon-etal-2023}'s eq. (8) uses ℚ-valued measures directly; @cite{dambrosio-hedden-2024}'s Bool dimensions are the special case via boolMeasures.

Equations

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

def Semantics.Gradability.Aggregation.weightedBinding {α : Type} (weights : List ℚ) (θ : ℚ) (dims : List (α → Bool)) (x : α) : Bool

Weighted binding (Bool dimensions): x is F iff its weighted score over Bool-lifted measures exceeds threshold θ.

Equations

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

def Semantics.Gradability.Aggregation.weightedBindingQ {α : Type} (weights : List ℚ) (θ : ℚ) (measures : List (α → ℚ)) (x : α) : Bool

Weighted binding over continuous ℚ-valued measures.

Equations

• Semantics.Gradability.Aggregation.weightedBindingQ weights θ measures x = decide (Semantics.Gradability.Aggregation.weightedScore weights measures x ≥ θ)

def Semantics.Gradability.Aggregation.spatialNormalizedScore {α : Type} (weights : List ℚ) (measures : List (α → ℚ)) (spatial : α → ℚ) (x : α) : ℚ

Spatially-normalized weighted score: (Σᵢ wᵢ·fᵢ(x)) / s(x).

@cite{tham-2025} eq. 47b for physical disturbance adjectives. The measures track per-dimension EXTENT of disturbance (e.g., total crack length, depth-weighted area); the spatial measure tracks the host entity's SPATIAL EXTENT. A small disturbance on a small host can score the same as a large disturbance on a large host — boundedness of the scale comes from the denominator, not from any single dimension. Returns 0 when spatial x = 0 (avoiding division by zero); callers should ensure spatial x ≠ 0 for meaningful results.

Equations

• Semantics.Gradability.Aggregation.spatialNormalizedScore weights measures spatial x = if spatial x = 0 then 0 else Semantics.Gradability.Aggregation.weightedScore weights measures x / spatial x

def Semantics.Gradability.Aggregation.spatialNormalizedBinding {α : Type} (weights : List ℚ) (θ : ℚ) (dims : List (α → Bool)) (spatial : α → ℚ) (x : α) : Bool

Spatially-normalized weighted binding (Bool dimensions): x is F iff its spatially-normalized weighted score over Bool-lifted measures exceeds threshold θ.

Equations

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

theorem Semantics.Gradability.Aggregation.countBinding_zero {α : Type} (dims : List (α → Bool)) (x : α) : countBinding 0 dims x = true

Counting with threshold 0 is always satisfied (vacuously true).

@[simp]

theorem Semantics.Gradability.Aggregation.spatialNormalizedScore_unit {α : Type} (weights : List ℚ) (measures : List (α → ℚ)) (x : α) : spatialNormalizedScore weights measures (fun (x : α) => 1) x = weightedScore weights measures x

The spatial-normalization reduces to plain weighted score when spatial x = 1 (constant unit host extent).

@[simp]

theorem Semantics.Gradability.Aggregation.spatialNormalizedScore_zero {α : Type} (weights : List ℚ) (measures : List (α → ℚ)) (spatial : α → ℚ) (x : α) (h : spatial x = 0) : spatialNormalizedScore weights measures spatial x = 0

Spatial normalization at a zero-extent host returns 0. Documents the edge-case convention: a host with no spatial extent cannot exhibit a physical disturbance, so the predicate is vacuously not satisfied.

theorem Semantics.Gradability.Aggregation.spatialNormalizedScore_le_one {α : Type} (weights : List ℚ) (measures : List (α → ℚ)) (spatial : α → ℚ) (x : α) (hsum : weightedScore weights measures x ≤ spatial x) (hpos : 0 < spatial x) : spatialNormalizedScore weights measures spatial x ≤ 1

Bounded-by-one normalization (mathlib-style structural property). When the weighted-score numerator is bounded by the spatial-extent denominator, the normalized score is at most 1. This makes Tham 2025's "boundedness from spatial extent" claim (§3.4) into a structural theorem rather than a stipulation.

theorem Semantics.Gradability.Aggregation.spatialNormalizedScore_nonneg {α : Type} (weights : List ℚ) (measures : List (α → ℚ)) (spatial : α → ℚ) (x : α) (hnum : 0 ≤ weightedScore weights measures x) (hspatial : 0 ≤ spatial x) : 0 ≤ spatialNormalizedScore weights measures spatial x

Nonnegativity of normalized score. When the weighted score is nonnegative and the spatial extent is nonnegative, the normalized score is nonnegative. Combined with spatialNormalizedScore_le_one, this places the score in [0, 1] — the "fraction of the totality" intuition Tham 2025 §3.4 and Solt 2018 eq. 21 both require.

def Semantics.Gradability.Aggregation.multiplicativeScore {α : Type} (measures : List (α → ℚ)) (x : α) : ℚ

Multiplicative (Cobb-Douglas) score: Πᵢ fᵢ(x). @cite{sassoon-fadlon-2017} argue natural kind nouns compose multiplicatively: failure on ANY single dimension kills membership. Contrast with additive weightedScore for artifact nouns.

Equations

• Semantics.Gradability.Aggregation.multiplicativeScore measures x = List.foldl (fun (acc : ℚ) (f : α → ℚ) => acc * f x) 1 measures

inductive Semantics.Gradability.Aggregation.AggregationType : Type

Classification of dimensional aggregation mechanisms. Each type corresponds to an escape route from Arrow's impossibility.

• counting : AggregationType

  Threshold counting (rejects WO via non-transitivity or incompleteness).

• utilitarian : AggregationType

  Weighted sum / utilitarian (rejects ONC, accepts interval scale IUC).

• cobbDouglas : AggregationType

  Weighted product / Cobb-Douglas (rejects ONC, accepts ratio scale RNC).

def Semantics.Gradability.Aggregation.instReprAggregationType.repr : AggregationType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.Aggregation.instReprAggregationType : Repr AggregationType

Equations

• Semantics.Gradability.Aggregation.instReprAggregationType = { reprPrec := Semantics.Gradability.Aggregation.instReprAggregationType.repr }

@[implicit_reducible]

instance Semantics.Gradability.Aggregation.instDecidableEqAggregationType : DecidableEq AggregationType

Equations

• Semantics.Gradability.Aggregation.instDecidableEqAggregationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

theorem Semantics.Gradability.Aggregation.conjunctive_is_countAll {α : Type} (dims : List (α → Bool)) (x : α) : conjunctiveBinding dims x = countBinding dims.length dims x

Conjunctive binding = counting with threshold k = dims.length. @cite{sassoon-2013}'s ∀-binding is a special case of counting.

theorem Semantics.Gradability.Aggregation.disjunctive_is_countOne {α : Type} (dims : List (α → Bool)) (x : α) : disjunctiveBinding dims x = countBinding 1 dims x

Disjunctive binding = counting with threshold k = 1. @cite{sassoon-2013}'s ∃-binding is a special case of counting.

def Semantics.Gradability.Aggregation.toAggregationType : DimensionBindingType → AggregationType

@cite{sassoon-2013}'s binding types all map to counting aggregation. The key gap: Sassoon has no utilitarian or Cobb-Douglas mechanism.

Equations

• Semantics.Gradability.Aggregation.toAggregationType Semantics.Gradability.DimensionBindingType.conjunctive = Semantics.Gradability.Aggregation.AggregationType.counting
• Semantics.Gradability.Aggregation.toAggregationType Semantics.Gradability.DimensionBindingType.disjunctive = Semantics.Gradability.Aggregation.AggregationType.counting
• Semantics.Gradability.Aggregation.toAggregationType Semantics.Gradability.DimensionBindingType.mixed = Semantics.Gradability.Aggregation.AggregationType.counting

theorem Semantics.Gradability.Aggregation.sassoon_all_counting (b : DimensionBindingType) : toAggregationType b = AggregationType.counting

All of Sassoon 2013's binding types are counting aggregation.