Weight as a finitely additive measure

This file develops the arithmetic of wt, the total-stake functional on validator sets, as a finitely additive measure: monotone under inclusion and obeying inclusion–exclusion over the disjoint-union set algebra of Lemmas/SetTheoryProps.lean.

Monotonicity

wt_inc_leq is the cornerstone: s_1 \subseteq s_2 implies \operatorname{wt}(s_1) \le \operatorname{wt}(s_2). From it follow the intersection bounds wt_meet_leq1, wt_meet_leq2, wt_meet_leq.

Additivity and inclusion–exclusion

Over the disjoint union fUnion and difference fDiff, weight is additive:

\operatorname{wt}(\operatorname{fUnion}(A, B)) = \operatorname{wt}(A) + \operatorname{wt}(\operatorname{fDiff}(B, A))

(wt_fUnion). Splitting A into A \cap B and A \setminus B gives \operatorname{wt}(A) = \operatorname{wt}(A \cap B) + \operatorname{wt}(A \setminus B) (wt_inter_add_fDiff), and together these yield the inclusion–exclusion identity

\operatorname{wt}(A) + \operatorname{wt}(B) = \operatorname{wt}(\operatorname{fUnion}(A, B)) + \operatorname{wt}(A \cap B)

(wt_add_inter_fUnion).

Downstream use

wt_inc_leq underpins quorum_2_upclosed; the inclusion–exclusion and difference laws (wt_add_inter_fUnion, wt_fDiff, wt_fUnion_of_disjointMF) power quorum_intersection_weight_lower and validator_intersection_lower_bound of Theories/SlashableBound.lean.

Basic properties

The weight function \operatorname{wt} is non-negative, vanishes on the empty set, respects set equality, and is monotone under inclusion.

Non-negativity

Weights are non-negative:

0 \le \operatorname{wt}(\mathsf{stake}, s)

Immediate from \mathbb{N}-valuedness (Nat.zero_le). This is rarely invoked explicitly — it holds by the type — but serves as the base case in inductive weight arguments.

Empty weight

The empty set has zero weight:

\operatorname{wt}(\mathsf{stake}, \emptyset) = 0

The sum over the empty Finset is 0 (Finset.­sum_empty). This is the identity element for the additive structure: \operatorname{wt}(\emptyset) plays the role of the zero measure.

Monotonicity under inclusion

Monotonicity of weight:

s_1 \subseteq s_2 \;\implies\; \operatorname{wt}(\mathsf{stake}, s_1) \le \operatorname{wt}(\mathsf{stake}, s_2)

Assumptions

Only the subset hypothesis s_1 \subseteq s_2 hsub, and that the stake codomain \mathbb{N} has non-negative elements.

Proof idea

Write s_2 as the multiset sum of s_1 with a remainder t (from s_1 \subseteq s_2), so the stake-mapped sums satisfy \textstyle\sum_{s_2} = \sum_{s_1} + \sum_{t}; non-negativity of the remainder term (\mathbb{N}-valued, hence \ge 0) gives the inequality.

Non-assumptions

• No [\mathsf{DecidableEq}\ \mathsf{Validator}] — this lemma sits above the variable [DecidableEq Validator] declaration in the file, and the proof goes through the raw multiset remainder rather than a Finset difference. This is a deliberate placement, not an accident: monotonicity is the one weight fact that needs no decidable equality.

• No positivity of \mathsf{stake} — zero stakes are allowed.

• Strictness is not claimed: s_1 \subsetneq s_2 may still give equal weights when the extra elements carry zero stake.

Role in the development

The cornerstone of the measure layer: it yields the intersection bounds wt_meet_leq1/wt_meet_leq2, the quorum up-closure quorum_2_upclosed, and every \subseteq-monotone step in Theories/SlashableBound.lean.

Congruence

Weight respects set equality:

s_1 = s_2 \;\implies\; \operatorname{wt}(s_1) = \operatorname{wt}(s_2)

By congrArg.

Intersection bounds

The weight of an intersection is bounded by the weight of each constituent set. These bounds are immediate corollaries of monotonicity (wt_inc_leq) and the subset relations s_1 \cap s_2 \subseteq s_1 and s_1 \cap s_2 \subseteq s_2.

Left intersection bound

The intersection weighs at most the left set:

\operatorname{wt}(s_1 \cap s_2) \le \operatorname{wt}(s_1)

Immediate from wt_inc_leq and the subset s_1 \cap s_2 \subseteq s_1 (Finset.­inter_subset_left). Together with wt_meet_leq2 this supplies the two-sided bound needed in the quorum-overlap arguments.

Right intersection bound

The intersection weighs at most the right set:

\operatorname{wt}(s_1 \cap s_2) \le \operatorname{wt}(s_2)

The symmetric counterpart of wt_meet_leq1, from s_1 \cap s_2 \subseteq s_2 (Finset.­inter_subset_right).

Sum bound

The intersection weighs at most the sum of the two sets:

\operatorname{wt}(s_1 \cap s_2) \le \operatorname{wt}(s_1) + \operatorname{wt}(s_2)

Obtained by chaining wt_meet_leq1 with \operatorname{wt}(s_1) \le \operatorname{wt}(s_1) + \operatorname{wt}(s_2) (Nat.le_add_right). A coarser bound than either wt_meet_leq1 or wt_meet_leq2 individually, but sometimes the only form needed when both summands are present.

Commutativity of intersection weight

Intersection weight is symmetric:

\operatorname{wt}(s_1 \cap s_2) = \operatorname{wt}(s_2 \cap s_1)

Lifts the set-level commutativity inter_commF through wt by congruence. Used in wt_inter_add_fDiff (to split B's weight along A by commuting the intersection) and in validator_intersection_lower_bound (to swap the two checkpoint validator sets).

Additivity and inclusion–exclusion

The disjoint-union presentation of fUnion makes weight additive: the weight of a union splits as a plain sum (no truncated subtraction). From this additive law the file derives the partition identity, the inclusion–exclusion formula, and its subtractive rearrangements. The derivation chain is:

1. wt_fUnion — additivity of weight over fUnion

2. inter_fDiff_partition — the set-level partition A = (A \cap B) \uplus (A \setminus B)

3. wt_inter_add_fDiff — weighing the partition

4. wt_fDiff — subtractive rearrangement

5. wt_add_inter_fUnion — inclusion–exclusion (additive)

6. wt_fUnion_of_disjointMF — disjoint special case

7. wt_join_partition_fUnion — three-block decomposition

8. wt_join_fUnion — inclusion–exclusion (subtractive)

Additivity over disjoint union

Additivity of weight:

\operatorname{wt}(\operatorname{fUnion}(A, B)) = \operatorname{wt}(A) + \operatorname{wt}(\operatorname{fDiff}(B, A))

Because fUnion is the disjoint sum A \uplus (B \setminus A), the stake-mapped multiset sum splits additively — with no truncated subtraction. This is the additive engine on which the inclusion–exclusion identities below rest.

Proof idea

The carrier of fUnion is the raw multiset sum A.\mathrm{val} + (\operatorname{fDiff}(B, A)).\mathrm{val}. Mapping stake distributes over multiset addition (Multiset.­map_add), and multiset sum distributes over multiset addition (Multiset.­sum_add), giving the \mathbb{N}-level identity. The two Finset.­sum_eq_multiset_sum conversions bridge between the Finset.­sum presentation of wt and the raw multiset sum.

Set partition

Partition of a set into its intersection with B and its difference from B:

A = \operatorname{fUnion}(A \cap B,\, \operatorname{fDiff}(A, B))

Every element of A either lies in B (landing in A \cap B) or not (landing in A \setminus B); the two parts are disjoint. This is the set-level identity (proved by Finset.­ext) underlying the additive weight split wt_inter_add_fDiff.

Additive weight split

Additive split of a set's weight along B:

\operatorname{wt}(A) = \operatorname{wt}(A \cap B) + \operatorname{wt}(\operatorname{fDiff}(A, B))

The weight of A is the weight of its part inside B plus the weight of its part outside B. Together with wt_fUnion it produces the inclusion–exclusion identity wt_add_inter_fUnion, and rearranged it gives the subtractive form wt_fDiff.

Proof idea

First, inter_fDiff_partition gives the set-level partition A = \operatorname{fUnion}(A \cap B,\, \operatorname{fDiff}(A, B)). Weighing this through wt_fUnion would yield \operatorname{wt}(A) = \operatorname{wt}(A \cap B) + \operatorname{wt}(\operatorname{fDiff}(\operatorname{fDiff}(A,B),\, A \cap B)), but the inner fDiff is idempotent: \operatorname{fDiff}(\operatorname{fDiff}(A, B),\, A \cap B) = \operatorname{fDiff}(A, B) (proved by Finset.­ext — an element of A \setminus B cannot lie in A \cap B). This auxiliary fact hfdf simplifies the right side to \operatorname{wt}(\operatorname{fDiff}(A, B)), completing the split.

Difference weight (subtractive form)

Subtractive form of the difference weight:

\operatorname{wt}(\operatorname{fDiff}(A, B)) = \operatorname{wt}(A) - \operatorname{wt}(A \cap B)

The truncated-subtraction rearrangement of wt_inter_add_fDiff; legitimate as a genuine subtraction because A \cap B \subseteq A, so the minuend dominates. Consumed by validator_intersection_lower_bound to express the weight of validators that exited (the part of one checkpoint's set not in the other's).

Inclusion–exclusion (additive form)

Inclusion–exclusion for weight:

\operatorname{wt}(A) + \operatorname{wt}(B) = \operatorname{wt}(\operatorname{fUnion}(A, B)) + \operatorname{wt}(A \cap B)

Assumptions

An arbitrary \mathsf{stake} : V \to \mathbb{N}, and [\mathsf{DecidableEq}\ V] (in scope as a section variable) for the intersection on the right.

Interpretation

Summing the two sets' weights double-counts exactly their intersection; moving that shared weight to the right gives the union weight. The classical |A| + |B| = |A \cup B| + |A \cap B|, weighed by stake.

Proof idea

Split \operatorname{wt}(B) as \operatorname{wt}(A \cap B) + \operatorname{wt}(B \setminus A) (wt_inter_add_fDiff with inter_commF), then recognize \operatorname{wt}(A) + \operatorname{wt}(B \setminus A) = \operatorname{wt}(\operatorname{fUnion}(A, B)) (wt_fUnion).

Non-assumptions

• A and B need not be disjoint — the \operatorname{wt}(A \cap B) term is precisely the correction handling overlap (the disjoint special case, where it vanishes, is wt_fUnion_of_disjointMF).

• No positivity of stake and no quorum hypothesis: the identity is purely algebraic and holds for every pair of finite validator sets.

Role in the development

The algebraic heart of the quorum-overlap arguments: it is the purely additive precursor that wt_quorum_union_bound_fUnion and quorum_intersection_weight_lower (Theories/SlashableBound.lean) instantiate with quorum and validator-set weights to lower-bound the slashed intersection.

Remarks

The identity is stated in its additive (subtraction-free) form. This is a deliberate representation choice, not a cosmetic one: over \mathbb{N} the additive equality is the primitive statement — it holds in any commutative monoid, needing neither subtraction nor an order — whereas the familiar subtractive form \operatorname{wt}(\operatorname{fUnion}(A, B)) = \operatorname{wt}(A) + \operatorname{wt}(B) - \operatorname{wt}(A \cap B) (wt_join_fUnion) is recovered only afterward by truncated rearrangement, and is specific to natural-number arithmetic.

Disjoint union weight

For genuinely disjoint sets the union weight is the plain sum:

\operatorname{disjointMF}(A.\mathrm{val},\, B.\mathrm{val}) \;\implies\; \operatorname{wt}(\operatorname{fUnion}(A, B)) = \operatorname{wt}(A) + \operatorname{wt}(B)

When A and B already share no element, \operatorname{fDiff}(B, A) = B, so the general additive law wt_fUnion collapses to the unqualified sum (no intersection correction). Used in wt_meet_subbound_fUnion of Theories/SlashableBound.lean.

Three-block decomposition

Three-block weight decomposition of the union:

\operatorname{wt}(\operatorname{fUnion}(A, B)) = \operatorname{wt}(\operatorname{fDiff}(A, B)) + \operatorname{wt}(\operatorname{fDiff}(B, A)) + \operatorname{wt}(A \cap B)

The weight of A \cup B split across its three pairwise-disjoint blocks — left-only A \setminus B, right-only B \setminus A, and shared A \cap B — obtained by combining wt_fUnion with the split wt_inter_add_fDiff. The weight image of the set partition setU_parF.

Inclusion–exclusion (subtractive form)

Subtractive inclusion–exclusion for the union weight:

\operatorname{wt}(\operatorname{fUnion}(A, B)) = \operatorname{wt}(A) + \operatorname{wt}(B) - \operatorname{wt}(A \cap B)

The familiar |A \cup B| = |A| + |B| - |A \cap B|, obtained as the truncated-subtraction rearrangement of the additive form wt_add_inter_fUnion (valid since \operatorname{wt}(A \cap B) is dominated by \operatorname{wt}(A) + \operatorname{wt}(B)).

Appendix: weight as a finitely additive measure

This appendix is a non-load-bearing aside. Nothing in the Core development depends on the perspective recorded here; it is collected at the file's end as added context, deliberately separated from the load-bearing docstrings above. It may be read or skipped without affecting any proof.

The lemmas above can be read through a single organising lens: the total-stake functional \operatorname{wt}(\mathsf{stake}, s) = \sum_{v \in s} \mathsf{stake}(v) is the finitely additive measure induced on the finite Boolean algebra \mathcal{P}(V) of validator subsets by the point mass \mathsf{stake} : V \to \mathbb{N}. Reading the file's results in that language:

• Base laws — wt_set0 (\operatorname{wt}(\emptyset) = 0) and wt_fUnion_of_disjointMF (additivity on disjoint pairs) are exactly the two axioms of a finitely additive measure (null empty set, finite additivity).

• Monotonicity — wt_inc_leq is the order-theoretic shadow of additivity: for a measure valued in an ordered monoid with non-negative masses, s_1 \subseteq s_2 \implies \mu(s_2) = \mu(s_1) + \mu(s_2 \setminus s_1) \ge \mu(s_1), the remainder being \mathbb{N}-valued and hence \ge 0.

• Inclusion–exclusion — wt_add_inter_fUnion is the N = 2 additive instance of the classical inclusion–exclusion principle (Poincaré's formula). The file does not state or use the general N-ary signed formula; over \mathbb{N} the additive two-set form is primitive (valid in any commutative monoid) and the subtractive rearrangement (wt_join_fUnion) is a derived convenience specific to natural-number arithmetic.

The value of this lens is taxonomic: it explains why the eight lemmas of the additivity block form a closed family (they are the finite-measure laws plus their truncated-subtraction rearrangements) rather than an ad-hoc list. But the proofs themselves use only \mathbb{N}-arithmetic and the disjoint-union set algebra of Lemmas/SetTheoryProps.lean; no measure-theoretic machinery is imported or required.