M02 — Weighted partition sums

{"text": "{\n "data": "Theorem M02_tile_sum_reindex. Let $\\\\iota$ be an arbitrary type on which equality of elements is decidable; let $I \\\\subseteq \\\\iota$ be a finite set; let $\\\\mathcal{B} = (B_1, B_2, \\\\dots, B_k)$ be a finite list of finite subsets of $\\\\iota$ (the tiles); let $E$ be a type equipped with the structure of a normed additive commutative group (an abelian group with a norm compatible with addition \u2014 for instance $\\\\mathbb{R}$ or $\\\\mathbb{R}^d$); and let $g : \\\\iota \\\\to E$ be a completely arbitrary function assigning to each index $i$ a summand $g(i) \\\\in E$. The hypothesis $h$ states that $\\\\mathcal{B}$ is a valid tile partition of $I$, which by definition (unfolding IsTilePartition) is the conjunction of two conditions:\n\n- Cover: folding the list $\\\\mathcal{B}$ with the operation of finite-set union, starting from $\\\\varnothing$, yields exactly $I$; equivalently,\n

\nthe union taken without multiplicity.\n- Pairwise disjointness: any two tiles occupying different positions in the list are disjoint, i.e. $B_p \\\\cap B_q = \\\\varnothing$ for all positions $p \\\\neq q$.\n\nUnder this hypothesis, the conclusion is the exact equality (not an inequality) of elements of $E$\n\n

\n\nThe left-hand side is the finite sum of $g$ over the occurrence set $I$. The right-hand side is an ordered sum over the list of tiles: the list $\\\\mathcal{B}$ is first mapped entrywise to the list of per-tile sums $\\\\big(\\\\sum_{i \\\\in B_1} g(i),\\\\ \\\\dots,\\\\ \\\\sum_{i \\\\in B_k} g(i)\\\\big)$, and that list of elements of $E$ is then summed by iterated group addition in list order, starting from the group zero $0$ (an empty list of tiles sums to $0$). Because addition in $E$ is commutative, the value of this list sum does not depend on the order or position of the tiles, but the right-hand side is literally the list-indexed iterated sum, so tiles are counted with their multiplicity as list entries.\n\nEdge cases and fine print silently included by the quantifiers:\n\n- Empty occurrence set, $I = \\\\varnothing$: both sides are $0$, and the hypothesis is still satisfiable \u2014 e.g. by the empty list $\\\\mathcal{B} = ()$, or by any list consisting only of empty tiles.\n- Empty tiles: a tile $B_p = \\\\varnothing$ may appear anywhere in $\\\\mathcal{B}$, several times included; it contributes $\\\\sum_{i \\\\in \\\\varnothing} g(i) = 0$ to the right-hand side, i.e. nothing.\n- Repeated tiles: the same nonempty tile may not occur twice \u2014 a finite set is disjoint from itself only when it is empty, so $\\\\mathcal{B} = (\\\\varnothing, \\\\varnothing)$ is admissible whereas $\\\\mathcal{B} = (B, B)$ with $B \\\\neq \\\\varnothing$ makes the hypothesis false.\n- Uneven tile sizes: nothing in the statement refers to tile cardinality; there is no renormalization by the number of tiles or by the size of any tile on either side.\n- Non-vacuity: the hypothesis is always satisfiable \u2014 for every $I$ the one-tile list $\\\\mathcal{B} = (I)$ satisfies both conjuncts (the union is $I$, and disjointness over a single position is trivial), and for that choice the statement reads $\\\\sum_{i \\\\in I} g(i) = \\\\sum_{i \\\\in I} g(i)$.\n\nRole of the remaining assumptions: decidable equality on $\\\\iota$ is what makes finite-set union and disjointness (hence the hypothesis itself) available as decidable operations on subsets of $\\\\iota$; the normed-additive-commutative-group structure on $E$ supplies, in particular, the abelian addition and zero under which both sums are formed \u2014 the norm itself, and any scalar multiplication, play no role in the assertion. All parameters $\\\\iota$, $I$, $\\\\mathcal{B}$, $E$, and $g$ are universally quantified: the theorem asserts the equality above for every choice of them satisfying the partition hypothesis.",\n "type": "result"\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-M02.md", "contentType": "text/markdown", "totalLines": 4, "displayContent": {"text": "{\n "data": "Theorem M02_tile_sum_reindex. Let $\\\\iota$ be an arbitrary type on which equality of elements is decidable; let $I \\\\subseteq \\\\iota$ be a finite set; let $\\\\mathcal{B} = (B_1, B_2, \\\\dots, B_k)$ be a finite list of finite subsets of $\\\\iota$ (the tiles); let $E$ be a type equipped with the structure of a normed additive commutative group (an abelian group with a norm compatible with addition \u2014 for instance $\\\\mathbb{R}$ or $\\\\mathbb{R}^d$); and let $g : \\\\iota \\\\to E$ be a completely arbitrary function assigning to each index $i$ a summand $g(i) \\\\in E$. The hypothesis $h$ states that $\\\\mathcal{B}$ is a valid tile partition of $I$, which by definition (unfolding IsTilePartition) is the conjunction of two conditions:\n\n- Cover: folding the list $\\\\mathcal{B}$ with the operation of finite-set union, starting from $\\\\varnothing$, yields exactly $I$; equivalently,\n

\nthe union taken without multiplicity.\n- Pairwise disjointness: any two tiles occupying different positions in the list are disjoint, i.e. $B_p \\\\cap B_q = \\\\varnothing$ for all positions $p \\\\neq q$.\n\nUnder this hypothesis, the conclusion is the exact equality (not an inequality) of elements of $E$\n\n

\n\nThe left-hand side is the finite sum of $g$ over the occurrence set $I$. The right-hand side is an ordered sum over the list of tiles: the list $\\\\mathcal{B}$ is first mapped entrywise to the list of per-tile sums $\\\\big(\\\\sum_{i \\\\in B_1} g(i),\\\\ \\\\dots,\\\\ \\\\sum_{i \\\\in B_k} g(i)\\\\big)$, and that list of elements of $E$ is then summed by iterated group addition in list order, starting from the group zero $0$ (an empty list of tiles sums to $0$). Because addition in $E$ is commutative, the value of this list sum does not depend on the order or position of the tiles, but the right-hand side is literally the list-indexed iterated sum, so tiles are counted with their multiplicity as list entries.\n\nEdge cases and fine print silently included by the quantifiers:\n\n- Empty occurrence set, $I = \\\\varnothing$: both sides are $0$, and the hypothesis is still satisfiable \u2014 e.g. by the empty list $\\\\mathcal{B} = ()$, or by any list consisting only of empty tiles.\n- Empty tiles: a tile $B_p = \\\\varnothing$ may appear anywhere in $\\\\mathcal{B}$, several times included; it contributes $\\\\sum_{i \\\\in \\\\varnothing} g(i) = 0$ to the right-hand side, i.e. nothing.\n- Repeated tiles: the same nonempty tile may not occur twice \u2014 a finite set is disjoint from itself only when it is empty, so $\\\\mathcal{B} = (\\\\varnothing, \\\\varnothing)$ is admissible whereas $\\\\mathcal{B} = (B, B)$ with $B \\\\neq \\\\varnothing$ makes the hypothesis false.\n- Uneven tile sizes: nothing in the statement refers to tile cardinality; there is no renormalization by the number of tiles or by the size of any tile on either side.\n- Non-vacuity: the hypothesis is always satisfiable \u2014 for every $I$ the one-tile list $\\\\mathcal{B} = (I)$ satisfies both conjuncts (the union is $I$, and disjointness over a single position is trivial), and for that choice the statement reads $\\\\sum_{i \\\\in I} g(i) = \\\\sum_{i \\\\in I} g(i)$.\n\nRole of the remaining assumptions: decidable equality on $\\\\iota$ is what makes finite-set union and disjointness (hence the hypothesis itself) available as decidable operations on subsets of $\\\\iota$; the normed-additive-commutative-group structure on $E$ supplies, in particular, the abelian addition and zero under which both sums are formed \u2014 the norm itself, and any scalar multiplication, play no role in the assertion. All parameters $\\\\iota$, $I$, $\\\\mathcal{B}$, $E$, and $g$ are universally quantified: the theorem asserts the equality above for every choice of them satisfying the partition hypothesis.",\n "type": "result"\n}", "startLine": 1, "lineNumbers": [1, 2, 3, 4]}, "meta": {"source": {"type": "internal", "value": "agent://RB-M02"}}}}