LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule

Statement

Let $(M, +, 0)$ be a commutative monoid and let all index sets below be finite.

If $h : T \to S$ is a bijection and $a : S \to M$ , then $\sum_{t \in T} a_{h (t)} = \sum_{s \in S} a_{s}$ .
If $S$ and $T$ are disjoint and $a : S \cup T \to M$ , then $\sum_{u \in S \cup T} a_{u} = \sum_{s \in S} a_{s} + \sum_{t \in T} a_{t}$ .
If $a : S \times T \to M$ , then $\sum_{(s, t) \in S \times T} a_{s, t} = \sum_{s \in S} (\sum_{t \in T} a_{s, t}) = \sum_{t \in T} (\sum_{s \in S} a_{s, t}) .$

Facts & Assumptions

Given: A commutative monoid $(M, +, 0)$ , finite sets $S, T$ , and functions and a bijection as in the Statement.

[F1]

A finite commutative-monoid sum is obtained from any enumeration of its finite index set, and its value is independent of that enumeration (A finite sum in a commutative monoid indexed by an arbitrary finite set).

[L1]

A finite monoid product splits at a cut, may be regrouped into consecutive blocks, and in a commutative monoid is invariant under permutations (Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either).

[L2]

A finite family of pairwise disjoint finite sets has finite union, and its cardinality is the sum of the cardinalities; in particular, $∣ S \cup T ∣ = ∣ S ∣ + ∣ T ∣$ when $S$ and $T$ are disjoint (The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition).

[L3]

A Cartesian product of finite sets is finite with $∣ S \times T ∣ = ∣ S ∣ ∣ T ∣$ (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ ).

[F2]

Composites and inverses of bijections are bijections (Injection, surjection, bijection).

Proof

technique · direct

1.1F1F2

For clause 1, choose an enumeration $ϕ : ∣ T ∣ \to T$ . Then $h \circ ϕ$ enumerates $S$ , and [F1] gives $\sum_{t \in T} a_{h (t)} = \sum_{k < ∣ T ∣} a_{h (ϕ (k))} = \sum_{s \in S} a_{s}$ .

1.2F1L1L2

For clause 2, choose enumerations of $S$ and $T$ and concatenate them. By [L2] this gives an enumeration of $S \cup T$ of length $∣ S ∣ + ∣ T ∣$ , and the splitting law in [L1] turns the resulting finite sum into the sum over $S$ followed by the sum over $T$ .

1.3F1L1L2L3

For clause 3, choose enumerations $ϕ : ∣ S ∣ \to S$ and $ψ : ∣ T ∣ \to T$ . The disjoint slices ${ϕ (i)} \times T$ cover $S \times T$ ; concatenate their $ψ$ -enumerations in the order of $i$ . By [L2] and [L3] this is an enumeration of $S \times T$ , and regrouping it into the $∣ S ∣$ consecutive slices gives $\sum_{(s, t) \in S \times T} a_{s, t} = \sum_{s \in S} (\sum_{t \in T} a_{s, t})$ .

2.1step 1.3F1L1L3

The column-major list also enumerates $S \times T$ , and permutation invariance followed by regrouping into columns gives $\sum_{(s, t) \in S \times T} a_{s, t} = \sum_{t \in T} (\sum_{s \in S} a_{s, t})$ .

3.1step 1.1step 1.2step 1.3step 2.1∎

Steps 1.1, 1.2, 1.3 and 2.1 prove reindexing, disjoint splitting and both finite Fubini equalities.

Depends on

Dependency tree · 2 levels

Sources

Andrade–da Cruz, Finite products in commutative monoids