Dimensional aggregation

A multidimensional predicate applies to an object, or ranks two objects, according to how the objects stand on several underlying dimensions. Two aggregation vocabularies share this file.

Rules, in the value-function framework of [sen-1970] as [DAH24] transposes it to dimensions: a profile assigns each object its vector of dimensional values, and a rule sends profiles to an overall relation on the objects, read x ⪰ y. Sen's informational requirements are invariance under a class of transformation vectors (strictly increasing maps, common-unit positive affine maps, similarities). Arrow's conditions ([arrow-1950]) and the strong Pareto, Pareto-indifference and anonymity conditions are predicates on rules. Four classical rules are stated with the conditions they meet or fail: majority ([may-1952]) meets every Arrow condition but weak-ordering outputs, which Condorcet's cycle refutes; the Pareto rule ([weymark-1984]) is a quasi-ordering that leaves every trade-off incomparable; the utilitarian rule meets every Arrow condition but ordinal invariance, failing even ratio-scale invariance; the Cobb–Douglas rule ([tsui-weymark-1997]) is ratio-scale invariant on non-negative profiles.

Scores for the positive form: a weighted sum of dimensional measures ([waldon-etal-2023]), its normalisation by the host's spatial extent ([tham-2025], [solt-2018-proportional]), and the multiplicative composition of [sassoon-fadlon-2017].

Implementation notes

• A rule is total on profiles, so Arrow's unrestricted-domain condition is built in; a domain restriction, such as the non-negative profiles the Cobb–Douglas rule needs, is a hypothesis of the statement.
• Outputs are bare relations, because majority rule is not transitive; a weak-ordering-valued rule bundles into Core.Order.TotalPreorder. AsymmRel is the strict part of a relation and mathlib's AntisymmRel its indifference part.

TODO

• The scores index dimensions by lists. Restating them over ι → K, so that the utilitarian rule compares weightedScores, awaits the cleanse of their consumers.

References

• [K. J. Arrow, A difficulty in the concept of social welfare (1951)][arrow-1950]
• J. D'Ambrosio and B. Hedden, Multidimensional adjectives (2024)
• [K. O. May, A set of independent necessary and sufficient conditions for simple majority decision (1952)][may-1952]
• [G. W. Sassoon and J. Fadlon, The role of dimensions in classification under predicates predicts their status in degree constructions (2017)][sassoon-fadlon-2017]
• [A. K. Sen, Collective choice and social welfare (1970)][sen-1970]
• [S. Solt, Proportional comparatives and relative scales (2018)][solt-2018-proportional]
• [S. W. Tham, Multidimensionality and the scalar components of physical disturbance predicates (2025)][tham-2025]
• [K.-Y. Tsui and J. A. Weymark, Social welfare orderings for ratio-scale measurable utilities (1997)][tsui-weymark-1997]
• [B. Waldon, C. Condoravdi, B. Levin and J. Degen, On the context dependence of artifact noun interpretation (2023)][waldon-etal-2023]
• [J. A. Weymark, Arrow's theorem with social quasi-orderings (1984)][weymark-1984]

def AsymmRel {α : Type u_1} (r : α → α → Prop) (a b : α) : Prop

The asymmetric part of a relation: r a b and not r b a. Mathlib's AntisymmRel r is the symmetric part.

Equations

• AsymmRel r a b = (r a b ∧ ¬r b a)

@[instance_reducible]

instance instDecidableAsymmRelOfDecidableRel {α : Type u_1} (r : α → α → Prop) [DecidableRel r] (a b : α) : Decidable (AsymmRel r a b)

Equations

• instDecidableAsymmRelOfDecidableRel r a b = instDecidableAsymmRelOfDecidableRel._aux_1 r a b

theorem AsymmRel.trans_le {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {a b c : α} (h : AsymmRel r a b) (h' : r b c) : AsymmRel r a c

theorem AsymmRel.le_trans {α : Type u_1} {r : α → α → Prop} [IsTrans α r] {a b c : α} (h : r a b) (h' : AsymmRel r b c) : AsymmRel r a c

@[reducible, inline]

abbrev Degree.Aggregation.Profile (ι : Type u_4) (α : Type u_5) (K : Type u_6) : Type (max (max u_4 u_5) u_6)

A profile: each object's vector of values, one per dimension.

Equations

• Degree.Aggregation.Profile ι α K = (α → ι → K)

@[reducible, inline]

abbrev Degree.Aggregation.Rule (ι : Type u_4) (α : Type u_5) (K : Type u_6) : Type (max (max u_5 u_6) u_4)

An aggregation rule: a relation on the objects, read x ⪰ y, for each profile.

Equations

• Degree.Aggregation.Rule ι α K = (Degree.Aggregation.Profile ι α K → α → α → Prop)

def Degree.Aggregation.Profile.transform {ι : Type u_1} {α : Type u_2} {K : Type u_3} (f : ι → K → K) (v : Profile ι α K) : Profile ι α K

Apply a vector of transformations, one per dimension, to a profile.

Equations

• Degree.Aggregation.Profile.transform f v x i = f i (v x i)

Informational invariance

def Degree.Aggregation.Invariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} (T : Set (ι → K → K)) (a : Rule ι α K) : Prop

Invariance of a rule under a class of transformation vectors.

Equations

• Degree.Aggregation.Invariant T a = ∀ f ∈ T, ∀ (v : Degree.Aggregation.Profile ι α K), a (Degree.Aggregation.Profile.transform f v) = a v

theorem Degree.Aggregation.Invariant.mono {ι : Type u_1} {α : Type u_2} {K : Type u_3} {S T : Set (ι → K → K)} (h : S ⊆ T) {a : Rule ι α K} (ha : Invariant T a) : Invariant S a

def Degree.Aggregation.ordinal {ι : Type u_1} {K : Type u_3} [Preorder K] : Set (ι → K → K)

Vectors of strictly increasing transformations; invariance under them is ordinal non-comparability.

Equations

• Degree.Aggregation.ordinal = {f : ι → K → K | ∀ (i : ι), StrictMono (f i)}

def Degree.Aggregation.cardinalUnit {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : Set (ι → K → K)

Common-unit positive affine transformation vectors; invariance under them is cardinal unit comparability.

Equations

• Degree.Aggregation.cardinalUnit = {f : ι → K → K | ∃ (a : K), 0 < a ∧ ∃ (b : ι → K), ∀ (i : ι) (t : K), f i t = a * t + b i}

def Degree.Aggregation.ratio {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] : Set (ι → K → K)

Similarity transformation vectors; invariance under them is ratio-scale non-comparability.

Equations

• Degree.Aggregation.ratio = {f : ι → K → K | ∃ (a : ι → K), (∀ (i : ι), 0 < a i) ∧ ∀ (i : ι) (t : K), f i t = a i * t}

theorem Degree.Aggregation.cardinalUnit_subset_ordinal {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] [IsStrictOrderedRing K] : cardinalUnit ⊆ ordinal

theorem Degree.Aggregation.ratio_subset_ordinal {ι : Type u_1} {K : Type u_3} [Semiring K] [PartialOrder K] [IsStrictOrderedRing K] : ratio ⊆ ordinal

Conditions on rules

def Degree.Aggregation.ParetoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Pareto indifference: objects with the same vector of values are indifferent.

Equations

• Degree.Aggregation.ParetoIndifferent a = ∀ (v : Degree.Aggregation.Profile ι α K) (x y : α), v x = v y → AntisymmRel (a v) x y

def Degree.Aggregation.Independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Independence of irrelevant alternatives: the verdict on a pair depends only on the vectors of that pair.

Equations

• Degree.Aggregation.Independent a = ∀ (v w : Degree.Aggregation.Profile ι α K) (x y : α), v x = w x → v y = w y → (a v x y ↔ a w x y)

def Degree.Aggregation.Transitive {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is transitive.

Equations

• Degree.Aggregation.Transitive a = ∀ (v : Degree.Aggregation.Profile ι α K), IsTrans α (a v)

def Degree.Aggregation.Complete {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is complete.

Equations

• Degree.Aggregation.Complete a = ∀ (v : Degree.Aggregation.Profile ι α K), Std.Total (a v)

def Degree.Aggregation.WeakOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is a weak ordering, a complete preorder.

Equations

• Degree.Aggregation.WeakOrderValued a = (Degree.Aggregation.Transitive a ∧ Degree.Aggregation.Complete a)

def Degree.Aggregation.QuasiOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Every output is a quasi-ordering, a preorder.

Equations

• Degree.Aggregation.QuasiOrderValued a = ∀ (v : Degree.Aggregation.Profile ι α K), IsPreorder α (a v)

def Degree.Aggregation.Anonymous {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) : Prop

Anonymity: permuting the dimensions leaves the output unchanged.

Equations

• Degree.Aggregation.Anonymous a = ∀ (σ : Equiv.Perm ι) (v : Degree.Aggregation.Profile ι α K), (a fun (x : α) => v x ∘ ⇑σ) = a v

def Degree.Aggregation.WeakOrderValued.toTotalPreorder {ι : Type u_1} {α : Type u_2} {K : Type u_3} {a : Rule ι α K} (h : WeakOrderValued a) (v : Profile ι α K) : Core.Order.TotalPreorder α

The output of a weak-ordering-valued rule at a profile, as a bundled total preorder.

Equations

• h.toTotalPreorder v = { le := a v, isPreorder := ⋯, total := ⋯ }

theorem Degree.Aggregation.WeakOrderValued.lt_toTotalPreorder {ι : Type u_1} {α : Type u_2} {K : Type u_3} {a : Rule ι α K} (h : WeakOrderValued a) (v : Profile ι α K) : (h.toTotalPreorder v).lt = AsymmRel (a v)

theorem Degree.Aggregation.WeakOrderValued.quasiOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} {a : Rule ι α K} (h : WeakOrderValued a) : QuasiOrderValued a

def Degree.Aggregation.WeakPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] : Prop

Weak Pareto: an object ranked strictly above another on every dimension is strictly preferred.

Equations

• Degree.Aggregation.WeakPareto a = ∀ (v : Degree.Aggregation.Profile ι α K) (x y : α), (∀ (i : ι), v y i < v x i) → AsymmRel (a v) x y

def Degree.Aggregation.StrongPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] : Prop

Strong Pareto: an object ranked weakly above another on every dimension is weakly preferred, and strictly so if some dimension ranks it strictly above.

Equations

• Degree.Aggregation.StrongPareto a = ∀ (v : Degree.Aggregation.Profile ι α K) (x y : α), v y ≤ v x → a v x y ∧ ((∃ (i : ι), v y i < v x i) → AsymmRel (a v) x y)

def Degree.Aggregation.IsDictator {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] (i : ι) : Prop

Dimension i is a dictator: its strict rankings are the strict overall rankings.

Equations

• Degree.Aggregation.IsDictator a i = ∀ (v : Degree.Aggregation.Profile ι α K) (x y : α), v y i < v x i → AsymmRel (a v) x y

def Degree.Aggregation.NonDictatorial {ι : Type u_1} {α : Type u_2} {K : Type u_3} (a : Rule ι α K) [Preorder K] : Prop

No dimension is a dictator.

Equations

• Degree.Aggregation.NonDictatorial a = ∀ (i : ι), ¬Degree.Aggregation.IsDictator a i

Majority rule

def Degree.Aggregation.majority {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] : Rule ι α K

Majority rule: x ⪰ y iff at least as many dimensions rank x weakly above y as rank y weakly above x.

Equations

• Degree.Aggregation.majority v x y = ({i : ι | v x i ≤ v y i}.card ≤ {i : ι | v y i ≤ v x i}.card)

@[instance_reducible]

instance Degree.Aggregation.instDecidableRelMajority {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] (v : Profile ι α K) : DecidableRel (majority v)

Equations

• Degree.Aggregation.instDecidableRelMajority v x✝¹ x✝ = id inferInstance

theorem Degree.Aggregation.majority_weakPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] [Nonempty ι] : WeakPareto majority

theorem Degree.Aggregation.majority_independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] : Independent majority

theorem Degree.Aggregation.majority_ordinalInvariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] : Invariant ordinal majority

theorem Degree.Aggregation.majority_anonymous {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] : Anonymous majority

theorem Degree.Aggregation.majority_paretoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] : ParetoIndifferent majority

theorem Degree.Aggregation.majority_nonDictatorial {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [LinearOrder K] [Nontrivial ι] [Nontrivial α] [Nontrivial K] : NonDictatorial majority

def Degree.Aggregation.condorcet : Profile (Fin 3) (Fin 3) ℕ

Condorcet's profile: three dimensions ranking three objects cyclically.

Equations

• Degree.Aggregation.condorcet = ![![2, 0, 1], ![1, 2, 0], ![0, 1, 2]]

theorem Degree.Aggregation.majority_condorcet : AsymmRel (majority condorcet) 0 1 ∧ AsymmRel (majority condorcet) 1 2 ∧ AsymmRel (majority condorcet) 2 0

Condorcet's paradox: majority rule ranks the three objects in a strict cycle.

theorem Degree.Aggregation.not_transitive_majority : ¬Transitive majority

Majority rule does not output transitive relations.

The Pareto rule

def Degree.Aggregation.paretoRule {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] : Rule ι α K

The Pareto rule: x ⪰ y iff every dimension ranks x weakly above y.

Equations

• Degree.Aggregation.paretoRule v x y = (v y ≤ v x)

theorem Degree.Aggregation.paretoRule_quasiOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] : QuasiOrderValued paretoRule

theorem Degree.Aggregation.paretoRule_strongPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] : StrongPareto paretoRule

theorem Degree.Aggregation.paretoRule_paretoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] : ParetoIndifferent paretoRule

theorem Degree.Aggregation.paretoRule_independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] : Independent paretoRule

theorem Degree.Aggregation.paretoRule_anonymous {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] : Anonymous paretoRule

theorem Degree.Aggregation.paretoRule_incomparable {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Preorder K] {v : Profile ι α K} {x y : α} {i j : ι} (hi : v y i < v x i) (hj : v x j < v y j) : ¬paretoRule v x y ∧ ¬paretoRule v y x

A trade-off, one dimension ranking x strictly above y and another y above x, is incomparable under the Pareto rule.

theorem Degree.Aggregation.paretoRule_ordinalInvariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] : Invariant ordinal paretoRule

The utilitarian rule

def Degree.Aggregation.utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) : Rule ι α K

The utilitarian rule with weights c: x ⪰ y iff the weighted sum of values favours x.

Equations

• Degree.Aggregation.utilitarian c v x y = (c ⬝ᵥ v y ≤ c ⬝ᵥ v x)

theorem Degree.Aggregation.utilitarian_weakOrderValued {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) : WeakOrderValued (utilitarian c)

theorem Degree.Aggregation.utilitarian_paretoIndifferent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) : ParetoIndifferent (utilitarian c)

theorem Degree.Aggregation.utilitarian_independent {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) : Independent (utilitarian c)

theorem Degree.Aggregation.utilitarian_weakPareto {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] (hc : ∀ (i : ι), 0 ≤ c i) (hpos : ∃ (i : ι), 0 < c i) : WeakPareto (utilitarian c)

theorem Degree.Aggregation.utilitarian_cardinalUnitInvariant {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] : Invariant cardinalUnit (utilitarian c)

theorem Degree.Aggregation.utilitarian_nonDictatorial {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] [Nontrivial α] (h₂ : ∀ (i : ι), ∃ (j : ι), j ≠ i ∧ 0 < c j) : NonDictatorial (utilitarian c)

theorem Degree.Aggregation.not_ratioInvariant_utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] [Nontrivial α] {i j : ι} (hij : i ≠ j) (hi : 0 < c i) (hj : 0 < c j) : ¬Invariant ratio (utilitarian c)

With two positive weights the utilitarian rule is not even ratio-scale invariant: rescaling one dimension breaks a tie.

theorem Degree.Aggregation.not_ordinalInvariant_utilitarian {ι : Type u_1} {α : Type u_2} {K : Type u_3} [Fintype ι] [Field K] [LinearOrder K] (c : ι → K) [IsStrictOrderedRing K] [Nontrivial α] {i j : ι} (hij : i ≠ j) (hi : 0 < c i) (hj : 0 < c j) : ¬Invariant ordinal (utilitarian c)

The Cobb–Douglas rule

def Degree.Aggregation.cobbDouglas {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) : Rule ι α ℝ

The Cobb–Douglas rule with exponents c: x ⪰ y iff the weighted geometric product of values favours x.

Equations

• Degree.Aggregation.cobbDouglas c v x y = (∏ i : ι, v y i ^ c i ≤ ∏ i : ι, v x i ^ c i)

theorem Degree.Aggregation.cobbDouglas_weakOrderValued {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) : WeakOrderValued (cobbDouglas c)

theorem Degree.Aggregation.cobbDouglas_paretoIndifferent {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) : ParetoIndifferent (cobbDouglas c)

theorem Degree.Aggregation.cobbDouglas_independent {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) : Independent (cobbDouglas c)

theorem Degree.Aggregation.cobbDouglas_transform_of_nonneg {ι : Type u_1} {α : Type u_2} [Fintype ι] (c : ι → ℝ) {f : ι → ℝ → ℝ} (hf : f ∈ ratio) {v : Profile ι α ℝ} (hv : ∀ (x : α) (i : ι), 0 ≤ v x i) : cobbDouglas c (Profile.transform f v) = cobbDouglas c v

On non-negative profiles the Cobb–Douglas rule is ratio-scale invariant.

Arrow's theorem

def Degree.Aggregation.Decisive {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] (a : Rule ι α K) (G : Finset ι) : Prop

G is decisive: whenever every dimension in G ranks x strictly above y, the rule ranks x strictly above y.

Equations

• Degree.Aggregation.Decisive a G = ∀ (v : Degree.Aggregation.Profile ι α K) (x y : α), (∀ i ∈ G, v y i < v x i) → AsymmRel (a v) x y

def Degree.Aggregation.DecisiveOn {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] (a : Rule ι α K) (G : Finset ι) (x y : α) : Prop

G is decisive for the pair x, y.

Equations

• Degree.Aggregation.DecisiveOn a G x y = ∀ (v : Degree.Aggregation.Profile ι α K), (∀ i ∈ G, v y i < v x i) → AsymmRel (a v) x y

def Degree.Aggregation.AlmostDecisiveOn {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] (a : Rule ι α K) (G : Finset ι) (x y : α) : Prop

G is almost decisive for the pair x, y: it prevails when every dimension outside G ranks y strictly above x.

Equations

• Degree.Aggregation.AlmostDecisiveOn a G x y = ∀ (v : Degree.Aggregation.Profile ι α K), (∀ i ∈ G, v y i < v x i) → (∀ i ∉ G, v x i < v y i) → AsymmRel (a v) x y

theorem Degree.Aggregation.DecisiveOn.almost {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} {G : Finset ι} {x y : α} (h : DecisiveOn a G x y) : AlmostDecisiveOn a G x y

theorem Degree.Aggregation.decisive_of_decisiveOn {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} {G : Finset ι} (hne : G.Nonempty) (h : ∀ (x y : α), x ≠ y → DecisiveOn a G x y) : Decisive a G

theorem Degree.Aggregation.iff_of_pattern {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] (hO : Invariant ordinal a) (hI : Independent a) {v w : Profile ι α K} {x y : α} (h : ∀ (i : ι), (v x i < v y i ↔ w x i < w y i) ∧ (v y i < v x i ↔ w y i < w x i)) : a v x y ↔ a w x y

Under ordinal invariance and independence, the verdict on a pair depends only on how each dimension orders the pair.

theorem Degree.Aggregation.decisiveOn_of_almost {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) {G : Finset ι} {x y : α} (hxy : x ≠ y) (h : AlmostDecisiveOn a G x y) {z : α} (hzy : z ≠ y) : DecisiveOn a G x z

Field expansion, first half: a group almost decisive for x, y is decisive for x, z.

theorem Degree.Aggregation.decisiveOn_of_almost' {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) {G : Finset ι} {x y : α} (hxy : x ≠ y) (h : AlmostDecisiveOn a G x y) {z : α} (hzx : z ≠ x) : DecisiveOn a G z y

Field expansion, second half: a group almost decisive for x, y is decisive for z, y.

theorem Degree.Aggregation.decisiveOn_of_almost_of_ne {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] [Fintype α] (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) (h₃ : 3 ≤ Fintype.card α) {G : Finset ι} {x y : α} (hxy : x ≠ y) (h : AlmostDecisiveOn a G x y) {u w : α} (huw : u ≠ w) : DecisiveOn a G u w

Field expansion: with three or more objects, a group almost decisive for one pair is decisive for every pair.

theorem Degree.Aggregation.exists_decisive_ssubset {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] [Fintype α] (hO : Invariant ordinal a) (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) (h₃ : 3 ≤ Fintype.card α) {G : Finset ι} (hG : Decisive a G) (h₂ : 2 ≤ G.card) : ∃ G' ⊂ G, Decisive a G'

Group contraction: a decisive group with two or more dimensions has a decisive proper subgroup.

theorem Degree.Aggregation.exists_isDictator {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] {a : Rule ι α K} [Field K] [IsStrictOrderedRing K] [Fintype α] [Fintype ι] (hO : Invariant ordinal a) (hW : WeakOrderValued a) (hP : WeakPareto a) (hI : Independent a) (h₃ : 3 ≤ Fintype.card α) : ∃ (i : ι), IsDictator a i

Arrow's theorem: with three or more objects, a rule that is ordinally invariant, outputs weak orderings, respects weak Pareto and is independent has a dictator.

theorem Degree.Aggregation.arrow {ι : Type u_1} {α : Type u_2} {K : Type u_3} [LinearOrder K] [Field K] [IsStrictOrderedRing K] [Fintype α] [Fintype ι] (h₃ : 3 ≤ Fintype.card α) (a : Rule ι α K) : ¬(Invariant ordinal a ∧ WeakOrderValued a ∧ WeakPareto a ∧ Independent a ∧ NonDictatorial a)

Arrow's theorem as an impossibility: no rule meets all of Arrow's conditions.

Scores for the positive form

def Degree.Aggregation.boolMeasures {α : Type u_2} {K : Type u_3} [Field K] (dims : List (α → Bool)) : List (α → K)

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

Equations

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

def Degree.Aggregation.weightedScore {α : Type u_2} {K : Type u_3} [Field K] (weights : List K) (measures : List (α → K)) (x : α) : K

Weighted score: Σᵢ wᵢ · fᵢ(x), where each fᵢ : α → K is a measure function along one dimension ([waldon-etal-2023]'s eq. (8)).

Equations

• Degree.Aggregation.weightedScore weights measures x = List.foldl (fun (acc : K) (x_1 : K × (α → K)) => match x_1 with | (w, f) => acc + w * f x) 0 (weights.zip measures)

def Degree.Aggregation.spatialNormalizedScore {α : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] (weights : List K) (measures : List (α → K)) (spatial : α → K) (x : α) : K

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

[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

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

def Degree.Aggregation.spatialNormalizedBinding {α : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] (weights : List K) (θ : K) (dims : List (α → Bool)) (spatial : α → K) (x : α) : Bool

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

Equations

• Degree.Aggregation.spatialNormalizedBinding weights θ dims spatial x = decide (Degree.Aggregation.spatialNormalizedScore weights (Degree.Aggregation.boolMeasures dims) spatial x ≥ θ)

@[simp]

theorem Degree.Aggregation.spatialNormalizedScore_unit {α : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (weights : List K) (measures : List (α → K)) (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 Degree.Aggregation.spatialNormalizedScore_zero {α : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] (weights : List K) (measures : List (α → K)) (spatial : α → K) (x : α) (h : spatial x = 0) : spatialNormalizedScore weights measures spatial x = 0

Spatial normalisation at a zero-extent host returns 0: a host with no spatial extent exhibits no disturbance.

theorem Degree.Aggregation.spatialNormalizedScore_le_one {α : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (weights : List K) (measures : List (α → K)) (spatial : α → K) (x : α) (hsum : weightedScore weights measures x ≤ spatial x) (hpos : 0 < spatial x) : spatialNormalizedScore weights measures spatial x ≤ 1

A weighted score bounded by the host's spatial extent normalises to at most 1: [tham-2025]'s boundedness from spatial extent.

theorem Degree.Aggregation.spatialNormalizedScore_nonneg {α : Type u_2} {K : Type u_3} [Field K] [LinearOrder K] [IsStrictOrderedRing K] (weights : List K) (measures : List (α → K)) (spatial : α → K) (x : α) (hnum : 0 ≤ weightedScore weights measures x) (hspatial : 0 ≤ spatial x) : 0 ≤ spatialNormalizedScore weights measures spatial x

A nonnegative weighted score over a nonnegative extent normalises to a nonnegative score; with spatialNormalizedScore_le_one it lies in [0, 1], the fraction of the totality of [tham-2025] and [solt-2018-proportional].

def Degree.Aggregation.multiplicativeScore {α : Type u_2} {K : Type u_3} [Field K] (measures : List (α → K)) (x : α) : K

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

Equations

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