M01 — Finite occurrence partition

{"text": "{\n "readback": "Declaration M01_partition_flatten (theorem).\n\nFix an arbitrary type $\\\\iota$ (of occurrences/indices, in an arbitrary universe) on which equality is decidable \u2014 this decidability is a genuine assumption on $\\\\iota$ and is what allows a list of $\\\\iota$-values to be converted into a finite set of its elements. Fix further a finite subset $I \\\\subseteq \\\\iota$ (given as a Finset) and a finite list of such finite subsets\n

\n(the \"tiles\"). The type $\\\\iota$, the decidability instance, the set $I$, and the list $\\\\mathcal{B}$ are all implicitly and universally quantified; the sole explicit hypothesis is $h$.\n\nHypothesis $h$ states that $\\\\mathcal{B}$ is a valid tile partition of $I$, which unfolds \u2014 literally, by the definition of IsTilePartition \u2014 into the conjunction of:\n\n

\n\ni.e. the union of all tiles in the list (computed as a right fold of binary union starting from $\\\\varnothing$) equals $I$ exactly; and\n\n

\n\ni.e. the list is pairwise disjoint (the formal relation is \"$B_p$ is disjoint from $B_q$\", which for finite sets means $B_p \\\\cap B_q = \\\\varnothing$; since this condition is symmetric in its two arguments, this is ordinary pairwise disjointness of the tiles). In particular, if one and the same tile $B$ occupies two distinct positions of the list, the hypothesis demands $B \\\\cap B = \\\\varnothing$, i.e. that repeated tile must be $\\\\varnothing$.\n\nConclusion. Let\n\n

\n\ndenote the concatenation, in list order, of the canonical element-lists of the tiles, where $\\\\operatorname{toList}(B)$ is a fixed list containing each element of the finite set $B$ exactly once, in an order determined by the internal construction of $B$ (not necessarily sorted; nothing in the conclusion depends on, or asserts anything about, the order of $L$). The theorem asserts the conjunction:\n\n1. No duplicates. $L$ is Nodup: no value of $\\\\iota$ occurs at two distinct positions of $L$ \u2014 every two entries of the flattened list are distinct.\n2. Exact occurrence set. Converting $L$ to the finite set of values that occur in it (the toFinset conversion, which is where decidable equality on $\\\\iota$ is used) yields exactly $I$: every element of $I$ appears somewhere in $L$, and no value outside $I$ appears in $L$.\n\nTaken together, the two conjuncts say: each element of $I$ appears exactly once in the concatenation of the tile element-lists.\n\nEdge cases the quantifiers silently include:\n\n- Empty tile list ($k = 0$, $\\\\mathcal{B} = []$): the union condition reads $\\\\varnothing = I$, so the hypothesis is satisfiable only when $I = \\\\varnothing$; then $L = []$, which is Nodup, and its element set is $\\\\varnothing = I$. The case is consistent, but it is available only for the empty occurrence set.\n- Empty tiles: a tile $B_p = \\\\varnothing$ may appear anywhere in $\\\\mathcal{B}$ and may even repeat ($\\\\varnothing$ is disjoint from every set, including itself, and contributes nothing to the union); its segment $\\\\operatorname{toList}(\\\\varnothing) = []$ contributes nothing to $L$.\n- Empty occurrence set ($I = \\\\varnothing$) with $k \\\\ge 1$: the union condition forces every tile to be empty, so $L$ is a concatenation of empty segments.\n- Non-vacuity: the hypothesis is satisfiable for every choice of $I$ and $\\\\iota$ with decidable equality \u2014 e.g. $\\\\mathcal{B} = [I]$ is a valid tile partition \u2014 so the theorem is not vacuously true; it makes a substantive claim whenever a valid partition is given.\n"\n}", "details": {"resolvedPath": "/home/ajax/.omp/agent/sessions/-math/2026-09-22T19-31-08-510Z_01a0ca99-be5e-7000-93c6-dac7c74cc004/RB-M01.md", "contentType": "text/markdown", "totalLines": 3, "displayContent": {"text": "{\n "readback": "Declaration M01_partition_flatten (theorem).\n\nFix an arbitrary type $\\\\iota$ (of occurrences/indices, in an arbitrary universe) on which equality is decidable \u2014 this decidability is a genuine assumption on $\\\\iota$ and is what allows a list of $\\\\iota$-values to be converted into a finite set of its elements. Fix further a finite subset $I \\\\subseteq \\\\iota$ (given as a Finset) and a finite list of such finite subsets\n

\n(the \"tiles\"). The type $\\\\iota$, the decidability instance, the set $I$, and the list $\\\\mathcal{B}$ are all implicitly and universally quantified; the sole explicit hypothesis is $h$.\n\nHypothesis $h$ states that $\\\\mathcal{B}$ is a valid tile partition of $I$, which unfolds \u2014 literally, by the definition of IsTilePartition \u2014 into the conjunction of:\n\n

\n\ni.e. the union of all tiles in the list (computed as a right fold of binary union starting from $\\\\varnothing$) equals $I$ exactly; and\n\n

\n\ni.e. the list is pairwise disjoint (the formal relation is \"$B_p$ is disjoint from $B_q$\", which for finite sets means $B_p \\\\cap B_q = \\\\varnothing$; since this condition is symmetric in its two arguments, this is ordinary pairwise disjointness of the tiles). In particular, if one and the same tile $B$ occupies two distinct positions of the list, the hypothesis demands $B \\\\cap B = \\\\varnothing$, i.e. that repeated tile must be $\\\\varnothing$.\n\nConclusion. Let\n\n

\n\ndenote the concatenation, in list order, of the canonical element-lists of the tiles, where $\\\\operatorname{toList}(B)$ is a fixed list containing each element of the finite set $B$ exactly once, in an order determined by the internal construction of $B$ (not necessarily sorted; nothing in the conclusion depends on, or asserts anything about, the order of $L$). The theorem asserts the conjunction:\n\n1. No duplicates. $L$ is Nodup: no value of $\\\\iota$ occurs at two distinct positions of $L$ \u2014 every two entries of the flattened list are distinct.\n2. Exact occurrence set. Converting $L$ to the finite set of values that occur in it (the toFinset conversion, which is where decidable equality on $\\\\iota$ is used) yields exactly $I$: every element of $I$ appears somewhere in $L$, and no value outside $I$ appears in $L$.\n\nTaken together, the two conjuncts say: each element of $I$ appears exactly once in the concatenation of the tile element-lists.\n\nEdge cases the quantifiers silently include:\n\n- Empty tile list ($k = 0$, $\\\\mathcal{B} = []$): the union condition reads $\\\\varnothing = I$, so the hypothesis is satisfiable only when $I = \\\\varnothing$; then $L = []$, which is Nodup, and its element set is $\\\\varnothing = I$. The case is consistent, but it is available only for the empty occurrence set.\n- Empty tiles: a tile $B_p = \\\\varnothing$ may appear anywhere in $\\\\mathcal{B}$ and may even repeat ($\\\\varnothing$ is disjoint from every set, including itself, and contributes nothing to the union); its segment $\\\\operatorname{toList}(\\\\varnothing) = []$ contributes nothing to $L$.\n- Empty occurrence set ($I = \\\\varnothing$) with $k \\\\ge 1$: the union condition forces every tile to be empty, so $L$ is a concatenation of empty segments.\n- Non-vacuity: the hypothesis is satisfiable for every choice of $I$ and $\\\\iota$ with decidable equality \u2014 e.g. $\\\\mathcal{B} = [I]$ is a valid tile partition \u2014 so the theorem is not vacuously true; it makes a substantive claim whenever a valid partition is given.\n"\n}", "startLine": 1, "lineNumbers": [1, 2, 3]}, "meta": {"source": {"type": "internal", "value": "agent://RB-M01"}}}}