diff --git a/content/essays/index-period-normal-forms/index.md b/content/essays/index-period-normal-forms/index.md
new file mode 100644
index 0000000..46c3aa4
--- /dev/null
+++ b/content/essays/index-period-normal-forms/index.md
@@ -0,0 +1,1963 @@
+---
+title: "Index-Period Normal Forms for Monoid-Aggregated Recursive Summaries"
+subtitle: "Exact Pumping, Canonical Representatives, and Computable Test Families"
+date: 2026-05-16
+abstract: >
+ A monoid-aggregated summary evaluates a finite rooted cop-labeled tree
+ bottom-up through a finite state set and a finite commutative
+ child-aggregation monoid. Once the multiplicity observation map and the
+ monoid are fixed, context equivalence has finite index and is exactly
+ equality of a finite behavior vector. This note sharpens the resulting
+ pumping and normal-form theory: the crude pigeonhole bound in the product
+ monoid is replaced by an exact index–period bound on each behavior type's
+ child contribution, isolating support, modular, and saturation counting in
+ the Boolean, cyclic, and threshold families. Combining exact sibling
+ pumping with a size-minimality argument — no behavior vector may repeat
+ along a root-to-leaf path — yields a finite universe of normal
+ representatives, and an external tie-break selects one canonical
+ representative per class. Worked computations for one-node trees, stars,
+ unary chains, and split-versus-concentrated examples make the bounds
+ concrete.
+tags:
+ - research
+ - research/mathematics
+ - research/algebra
+ - research/graph-theory
+authors:
+ - "Levi Neuwirth | /me.html"
+affiliation:
+ - "Brown University | https://www.brown.edu"
+no-collapse: true
+status: "Working model"
+confidence: 80
+evidence: 4
+peer-status: unreviewed
+result-shape: positive
+history:
+ - date: 2026-05-16
+---
+
+## Purpose and executive diagnosis
+
+The fixed-resource monoid-aggregated model gives a genuine finite-index
+theory, but the first normal-form bound is far too coarse if stated only as a
+pigeonhole bound in a huge product monoid. The correct next move is to
+analyze, for each behavior type, the cyclic submonoid generated by its child
+contribution. This gives an exact index-period pumping rule.
+
+The result is a more useful theory. Sibling multiplicities reduce by
+explicit index–period normal forms; the Boolean, cyclic, and threshold
+monoids acquire transparent pumping signatures; fixed-resource equivalence
+classes gain finite normal representatives; canonical representatives exist
+after a harmless external tie-break; and the example computations become
+concrete rather than schematic.
+
+There is also an important algebraic correction. One should not assume that
+every finite commutative monoid is a semilattice of abelian groups. That
+statement holds for special regular/Clifford-type commutative monoids, not
+for arbitrary finite commutative monoids. Threshold monoids already contain
+aperiodic saturation behavior that is not group-like. The universal
+finite-monoid fact needed here is simpler: for each element $g$ of a finite
+monoid, the sequence
+
+$$
+0,\; g,\; 2g,\; 3g,\; \ldots
+$$
+
+is ultimately periodic.
+
+**Main principle.** For fixed resources, the relevant algebra is not a global
+decomposition of the whole monoid. It is the index-period decomposition of
+the cyclic submonoid generated by each realized child-contribution element.
+
+## The fixed-resource model, recalled
+
+This section repeats the definitions needed for the present note. The
+conventions are unchanged from the finite-resource foundations note.
+
+::: {.annotation .annotation--static #def-rooted-tree}
+
+Definition 2.1
+Rooted cop-labeled tree
+
+
+
+A *rooted cop-labeled tree* is a finite rooted unordered tree $T$ with root
+$\rho_T$ together with a multiplicity function
+
+$$
+m_T : V(T) \to \mathbb{N}.
+$$
+
+Sibling order is not part of the structure.
+
+
+
+A *rooted one-hole context* $K[\square]$ is a finite rooted cop-labeled tree
+with one distinguished subtree slot. If $X$ is a rooted cop-labeled tree, then
+$K[X]$ is obtained by plugging $X$ into the slot. Contexts compose, and the
+empty context is $E[\square] = \square$.
+
+
+
+A *finite resource datum* is a tuple
+
+$$
+\mathcal{R} = (A, \mu, S, M, \oplus, 0_M)
+$$
+
+where:
+
+1. $A$ is a finite multiplicity alphabet;
+2. $\mu : \mathbb{N} \to A$ is a fixed multiplicity observation map;
+3. $S$ is a finite state set;
+4. $(M, \oplus, 0_M)$ is a finite commutative monoid.
+
+
+Warning 2.4
+Actual resources, not just cardinalities
+
+
+
+For the clean fixed-resource theory, $\mu$ and $(M, \oplus, 0_M)$ are part of
+the resource datum. Fixing only $|A|$ would allow infinitely many exact
+multiplicity tests by varying $\mu$. Fixing only $|M|$ still leaves only
+finitely many monoid structures on a fixed finite set, but the pumping
+constants depend on the actual operation. Therefore all sharp statements
+below are parametrized by the actual resource datum $\mathcal{R}$.
+
+
+
+A *monoid-aggregated summary* over $\mathcal{R}$ is a pair
+
+$$
+P = (\alpha_P, f_P)
+$$
+
+with
+
+$$
+\alpha_P : S \to M, \qquad f_P : A \times M \to S.
+$$
+
+It evaluates a rooted tree bottom-up by
+
+$$
+P(T_v) = f_P\!\left( \mu(m_T(v)),\; \bigoplus_{u \text{ child of } v} \alpha_P(P(T_u)) \right),
+$$
+
+where the empty sum is $0_M$. The root value is denoted $P(T)$.
+
+
+Lemma 2.7
+Crude cardinality of the summary class
+
+
+
+The number of syntactic summaries over $\mathcal{R}$ is
+
+$$
+|D(\mathcal{R})| = |M|^{|S|} \cdot |S|^{|A||M|},
+$$
+
+where equality means syntactic equality of pairs $(\alpha, f)$. The number of
+extensionally distinct summaries is at most this quantity.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Crude cardinality of the summary class" data-exhibit-type="proof" data-exhibit-caption="Count the choices of α : S → M and f : A × M → S independently."}
+
+:::: exhibit-body
+There are $|M|^{|S|}$ choices of $\alpha : S \to M$ and $|S|^{|A||M|}$ choices
+of $f : A \times M \to S$. [□]{.proof-qed}
+::::
+
+:::
+
+## Behavior vectors and fixed-resource equivalence
+
+::: {.annotation .annotation--static #def-behavior-vector}
+
+Definition 3.1
+Behavior vector
+
+
+
+The *$\mathcal{R}$-behavior vector* of a tree $T$ is
+
+$$
+\beta_{\mathcal{R}}(T) = (P(T))_{P \in D(\mathcal{R})} \in S^{D(\mathcal{R})}.
+$$
+
+We write
+
+$$
+B_{\mathcal{R}} := S^{D(\mathcal{R})}
+$$
+
+for the finite set of *formal* behavior vectors. A vector $b \in
+B_{\mathcal{R}}$ is *realizable* if $b = \beta_{\mathcal{R}}(T)$ for some tree
+$T$.
+
+
+Theorem 3.3
+Fixed-resource equivalence is behavior-vector equality
+
+
+
+For all rooted cop-labeled trees $X, Y$,
+
+$$
+X \sim_{\mathcal{R}} Y \iff \beta_{\mathcal{R}}(X) = \beta_{\mathcal{R}}(Y).
+$$
+
+Consequently $\sim_{\mathcal{R}}$ has finite index, with at most
+$|S|^{|D(\mathcal{R})|}$ classes.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Fixed-resource equivalence is behavior-vector equality" data-exhibit-type="proof" data-exhibit-caption="Single-summary context equivalence is root-state equality; intersect over all summaries."}
+
+:::: exhibit-body
+For a single fixed summary $P$, context equivalence is exactly equality of
+root state: if two inserted trees have the same root state, the computation
+above the hole is identical; conversely, the empty context detects root-state
+inequality. Intersecting over all $P \in D(\mathcal{R})$ gives precisely
+equality of all coordinates of $\beta_{\mathcal{R}}$. Since $B_{\mathcal{R}} =
+S^{D(\mathcal{R})}$ is finite, the finite-index bound follows.
+[□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-behavior-type}
+
+Remark 3.4
+Behavior type
+
+
+
+In this note a *behavior type* means an element of $B_{\mathcal{R}}$, usually
+a realizable one. Two trees have the same behavior type exactly when they are
+$\sim_{\mathcal{R}}$-equivalent.
+
+
+
+If $X \sim_{\mathcal{R}} Y$, then for every rooted one-hole context
+$K[\square]$,
+
+$$
+K[X] \sim_{\mathcal{R}} K[Y].
+$$
+
+Equivalently, replacing a subtree by another subtree with the same
+$\mathcal{R}$-behavior vector preserves the $\mathcal{R}$-behavior vector of
+the whole tree.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Fixed-resource congruence" data-exhibit-type="proof" data-exhibit-caption="The inserted subtree is seen above the hole only through its single root state, which agrees for every summary."}
+
+:::: exhibit-body
+By [Theorem 3.3](#thm-behavior-vector), $X \sim_{\mathcal{R}} Y$ means
+$\beta_{\mathcal{R}}(X) = \beta_{\mathcal{R}}(Y)$. In the bottom-up evaluation
+of any summary $P \in D(\mathcal{R})$ on $K[X]$ or $K[Y]$, the inserted
+subtree is seen above the hole only through the single state $P(X)$ or
+$P(Y)$. These states agree for every $P$, so the computation above the hole
+agrees for every $P$. Applying [Theorem 3.3](#thm-behavior-vector) again gives
+$K[X] \sim_{\mathcal{R}} K[Y]$. [□]{.proof-qed}
+::::
+
+:::
+
+## The product contribution monoid
+
+Sibling pumping is most naturally stated in a product monoid that tracks all
+summaries simultaneously.
+
+::: {.annotation .annotation--static #def-product-monoid}
+
+Definition 4.1
+Product monoid
+
+
+
+Let $M^{D(\mathcal{R})}$ denote the product monoid of $D(\mathcal{R})$ copies
+of $M$ — equivalently, the set of functions $D(\mathcal{R}) \to M$ — with
+coordinatewise operation, also denoted $\oplus$, and zero element $(0_M)_{P
+\in D(\mathcal{R})}$.
+
+
+Definition 4.2
+Contribution element of a behavior type
+
+
+
+For a formal behavior vector
+
+$$
+b = (b_P)_{P \in D(\mathcal{R})} \in B_{\mathcal{R}},
+$$
+
+define its *product contribution element*
+
+$$
+\gamma_b \in M^{D(\mathcal{R})}
+$$
+
+by
+
+$$
+(\gamma_b)_P := \alpha_P(b_P).
+$$
+
+Thus $\gamma_b$ is the simultaneous child contribution made by a child
+subtree of behavior type $b$ to every summary $P \in D(\mathcal{R})$. This
+definition also makes sense for formal, non-realizable behavior vectors; only
+realizable vectors occur as actual child types in trees.
+
+
+
+The symbols used below are as follows: $B_{\mathcal{R}} = S^{D(\mathcal{R})}$
+is the set of formal behavior vectors; $M^{D(\mathcal{R})}$ is the product
+contribution monoid; $\gamma_b \in M^{D(\mathcal{R})}$ is the contribution
+element of a behavior type $b$; $\operatorname{ind}(\gamma_b)$ and
+$\operatorname{per}(\gamma_b)$ are computed inside $M^{D(\mathcal{R})}$; and
+$N_{\mathcal{R}}(b) = \operatorname{ind}(\gamma_b) +
+\operatorname{per}(\gamma_b) - 1$ is the exact per-type sibling bound.
+
+
+Lemma 4.4
+Sibling aggregate as a product-monoid sum
+
+
+
+Let a node have child behavior-type multiplicities
+
+$$
+(n_b)_{b \in B_{\mathcal{R}}},
+$$
+
+with all but finitely many $n_b$ zero. Then the simultaneous child aggregate
+seen by all summaries is
+
+$$
+\Gamma := \bigoplus_{b \in B_{\mathcal{R}}} n_b \gamma_b \in M^{D(\mathcal{R})}.
+$$
+
+The $P$-coordinate of $\Gamma$ is exactly
+
+$$
+\bigoplus_{u \text{ child}} \alpha_P(P(T_u)),
+$$
+
+the aggregate used by $P$ at the parent.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Sibling aggregate as a product-monoid sum" data-exhibit-type="proof" data-exhibit-caption="Group children by behavior vector; each contributes α_P(b_P) in coordinate P."}
+
+:::: exhibit-body
+Group the children according to their behavior vector $b$. For each child $u$
+of type $b$, the $P$-coordinate contribution is $\alpha_P(b_P)$. Summing over
+all children and all behavior types gives the stated product-monoid
+expression. Coordinate $P$ is exactly the ordinary child aggregate for the
+summary $P$. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-right-object}
+
+Remark 4.5
+Why this is the right object
+
+
+
+The old bound used only the size of $M^{D(\mathcal{R})}$. That is enough to
+prove eventual pumping, but it ignores the actual contribution elements
+$\gamma_b$. The exact bound for a child type $b$ is controlled by the cyclic
+submonoid generated by $\gamma_b$, not by the whole product monoid.
+
+
+:::
+
+## Index-period decomposition in a finite monoid
+
+We now isolate the elementary finite-monoid fact used throughout the note.
+Additive notation means repeated use of the monoid operation: $ng = g \oplus
+\cdots \oplus g$ with $n$ copies, and $0g = 0_N$.
+
+::: {.annotation .annotation--static #def-index-period}
+
+Definition 5.1
+Index and period of an element
+
+
+
+Let $(N, +, 0_N)$ be a finite monoid and let $g \in N$. The sequence
+
+$$
+0g,\; 1g,\; 2g,\; 3g,\; \ldots
+$$
+
+is eventually periodic. Define $\operatorname{ind}_N(g)$ to be the least $i
+\geq 0$ for which there exists a $p \geq 1$ such that
+
+$$
+(n+p)g = ng \quad \text{for all } n \geq i.
+$$
+
+Given this least index, define $\operatorname{per}_N(g)$ to be the least such
+positive period $p$. When $N$ is clear, write simply $\operatorname{ind}(g)$
+and $\operatorname{per}(g)$. This is the least-index-then-least-period
+convention; other equivalent conventions are possible, but this one is fixed
+throughout the note.
+
+
+
+For every element $g$ of a finite monoid $N$, $\operatorname{ind}(g)$ and
+$\operatorname{per}(g)$ exist. Moreover
+
+$$
+\operatorname{ind}(g) + \operatorname{per}(g) \leq |N|.
+$$
+
+Equivalently, the exact contribution bound satisfies
+$\operatorname{ind}(g) + \operatorname{per}(g) - 1 \leq |N| - 1$.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Existence of index and period" data-exhibit-type="proof" data-exhibit-caption="Pigeonhole on the |N|+1 elements 0g,…,|N|g, then associativity gives eventual periodicity."}
+
+:::: exhibit-body
+Among the $|N|+1$ elements
+
+$$
+0g,\; 1g,\; \ldots,\; |N|g
+$$
+
+two are equal, say $ig = jg$ with $0 \leq i < j \leq |N|$. Let $p = j - i$.
+Then for every $n \geq i$, write $n = i + r$. Associativity gives
+
+$$
+(n+p)g = (i + r + p)g = (j + r)g = (i + r)g = ng.
+$$
+
+Thus eventual periodicity holds with $i + p = j \leq |N|$. The
+least-index-then-least-period pair can only improve this sum, so
+$\operatorname{ind}(g) + \operatorname{per}(g) \leq |N|$. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #def-canon-reduction}
+
+Definition 5.3
+Canonical reduction of a coefficient
+
+
+
+Let $g \in N$, and put
+
+$$
+i = \operatorname{ind}(g), \quad p = \operatorname{per}(g).
+$$
+
+Define
+
+$$
+\operatorname{red}_g(n) = \begin{cases} n, & n < i, \\ i + ((n-i) \bmod p), & n \geq i. \end{cases}
+$$
+
+Then $0 \leq \operatorname{red}_g(n) \leq i + p - 1$.
+
+
+
+For every $n \geq 0$,
+
+$$
+ng = \operatorname{red}_g(n)\, g.
+$$
+
+Moreover $\operatorname{red}_g(n) \leq n$, and if $n > \operatorname{ind}(g) +
+\operatorname{per}(g) - 1$, then $\operatorname{red}_g(n) < n$.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Exact unary pumping" data-exhibit-type="proof" data-exhibit-caption="Reduce n modulo the period beyond the index; a strict drop occurs once n exceeds ind+per−1."}
+
+:::: exhibit-body
+If $n < i$, the claim is immediate. If $n \geq i$, write
+
+$$
+n = i + qp + r
+$$
+
+with $q \geq 0$ and $0 \leq r < p$. By eventual periodicity in steps of $p$
+beyond $i$,
+
+$$
+ng = (i + qp + r)g = (i + r)g = \operatorname{red}_g(n)\, g.
+$$
+
+The inequality $\operatorname{red}_g(n) \leq n$ is clear from the formula. If
+$n > i + p - 1$, then $q \geq 1$, hence $\operatorname{red}_g(n) = i + r < n$.
+[□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #def-contribution-bound}
+
+Definition 5.5
+Contribution bound
+
+
+
+For $g \in N$, define
+
+$$
+N(g) := \operatorname{ind}(g) + \operatorname{per}(g) - 1.
+$$
+
+The exact pumping lemma says every coefficient of $g$ can be reduced to at
+most $N(g)$ without changing the monoid value.
+
+
+:::
+
+## Exact sibling pumping
+
+We now apply the index-period decomposition to behavior-type contributions.
+
+::: {.annotation .annotation--static #def-sibling-signature}
+
+Definition 6.1
+Sibling signature
+
+
+
+For a behavior type $b \in B_{\mathcal{R}}$, its *sibling signature* is
+
+$$
+\sigma_{\mathcal{R}}(b) := \bigl(\operatorname{ind}(\gamma_b), \operatorname{per}(\gamma_b)\bigr),
+$$
+
+computed inside the product monoid $M^{D(\mathcal{R})}$. Its *exact sibling
+bound* is
+
+$$
+N_{\mathcal{R}}(b) := \operatorname{ind}(\gamma_b) + \operatorname{per}(\gamma_b) - 1.
+$$
+
+A uniform exact sibling bound is
+
+$$
+N^{\max}_{\mathcal{R}} := \max_{b \in B_{\mathcal{R}}} N_{\mathcal{R}}(b).
+$$
+
+
+
+Let a node have child behavior-type multiplicities $(n_b)_{b \in
+B_{\mathcal{R}}}$. For each $b$, set
+
+$$
+n'_b := \operatorname{red}_{\gamma_b}(n_b).
+$$
+
+Replace the child multiset by one having exactly $n'_b$ children of behavior
+type $b$ for every $b$, using any available representatives of those behavior
+types. Then the simultaneous child aggregate in $M^{D(\mathcal{R})}$ is
+unchanged. Consequently, if the node's observed multiplicity label is
+unchanged, then its parent behavior vector is unchanged.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Exact sibling pumping at one node" data-exhibit-type="proof" data-exhibit-caption="Per-type unary pumping leaves each n_b γ_b unchanged, hence the whole product aggregate."}
+
+:::: exhibit-body
+By [Lemma 4.4](#lem-aggregate), the original simultaneous child aggregate is
+
+$$
+\Gamma = \bigoplus_b n_b \gamma_b.
+$$
+
+The new aggregate is
+
+$$
+\Gamma' = \bigoplus_b n'_b \gamma_b.
+$$
+
+By [Lemma 5.4](#lem-unary-pumping), $n_b \gamma_b = n'_b \gamma_b$ for each
+$b$. Therefore $\Gamma = \Gamma'$. Coordinatewise, every summary $P \in
+D(\mathcal{R})$ receives the same child aggregate at the node. Since the
+observed multiplicity label is also unchanged, every $P$ assigns the same
+parent state as before. Hence the whole behavior vector at the node is
+unchanged. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #cor-sibling-normal-form}
+
+Corollary 6.3
+Exact sibling normal form
+
+
+
+Every sibling multiset is equivalent, as seen by all summaries in
+$D(\mathcal{R})$, to one in which each behavior type $b$ occurs at most
+
+$$
+N_{\mathcal{R}}(b) = \operatorname{ind}(\gamma_b) + \operatorname{per}(\gamma_b) - 1
+$$
+
+times. In particular, the total number of children after exact sibling
+normalization is at most
+
+$$
+C_{\mathcal{R}} := \sum_{b \in B_{\mathcal{R}}} N_{\mathcal{R}}(b) \leq |B_{\mathcal{R}}| \cdot N^{\max}_{\mathcal{R}}.
+$$
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Exact sibling normal form" data-exhibit-type="proof" data-exhibit-caption="Apply the one-node pumping theorem per behavior type."}
+
+:::: exhibit-body
+Apply [Theorem 6.2](#thm-sibling-pumping) to each behavior type. The
+resulting count $n'_b$ satisfies $n'_b \leq N_{\mathcal{R}}(b)$.
+[□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-realizable-formal}
+
+Remark 6.4
+Realizable versus formal behavior types
+
+
+
+The bounds may be sharpened by taking $b$ only over realizable behavior
+vectors. The present statement uses all formal $b \in B_{\mathcal{R}}$ to
+avoid introducing a separate realizability analysis. Note that realizability
+of behavior vectors is defined existentially over all trees and is not in
+general algorithmically transparent, so the formal-version bounds are also
+the practically computable ones.
+
+
+:::
+
+## Canonical monoid families
+
+The index-period form makes the standard monoid families transparent.
+
+### Boolean semilattices
+
+::: {.annotation .annotation--static #prop-boolean}
+
+Proposition 7.1
+Boolean support pumping
+
+
+
+Let $M = (\{0, 1\}, \vee, 0)$. Then for $g = 0$,
+
+$$
+\operatorname{ind}(g) = 0, \quad \operatorname{per}(g) = 1, \quad N(g) = 0,
+$$
+
+and for $g = 1$,
+
+$$
+\operatorname{ind}(g) = 1, \quad \operatorname{per}(g) = 1, \quad N(g) = 1.
+$$
+
+Thus a nonzero child contribution is remembered only by presence or absence.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Boolean support pumping" data-exhibit-type="proof" data-exhibit-caption="g = 0 is periodic from index 0; g = 1 stabilizes at 1 from index 1."}
+
+:::: exhibit-body
+If $g = 0$, then $ng = 0$ for all $n$, so the sequence is periodic from index
+$0$ with period $1$. If $g = 1$, then $0g = 0$ and $ng = 1$ for all $n \geq
+1$, so the sequence has index $1$ and period $1$. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #cor-boolean-product}
+
+Corollary 7.2
+Boolean product bound
+
+
+
+If $M$ is a finite Boolean semilattice, for example a finite power of $(\{0,
+1\}, \vee, 0)$, every element is idempotent. Hence every behavior type has
+bound $0$ if its contribution is zero and bound $1$ otherwise.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Cyclic group pumping" data-exhibit-type="proof" data-exhibit-caption="ng is periodic from the start with least period the additive order of g."}
+
+:::: exhibit-body
+The sequence $ng$ is periodic from the beginning. Its least positive period
+is the additive order of $g$ in the cyclic group. The displayed formula for
+the order in $\mathbb{Z}/q\mathbb{Z}$ is standard. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #cor-cyclic-product}
+
+Corollary 7.4
+Product of cyclic groups
+
+
+
+If $M$ is a finite abelian group and $g \in M$, then
+
+$$
+\operatorname{ind}(g) = 0, \quad \operatorname{per}(g) = \operatorname{ord}(g), \quad N(g) = \operatorname{ord}(g) - 1.
+$$
+
+For a product element $g = (g_i)$, $\operatorname{ord}(g)$ is the least
+common multiple of the coordinate orders.
+
+
+
+Let $M = \Theta_T$. If $g = 0$, then $\operatorname{ind}(g) = 0$,
+$\operatorname{per}(g) = 1$, and $N(g) = 0$. If $1 \leq g \leq T$, then
+
+$$
+\operatorname{ind}(g) = \lceil T/g \rceil, \quad \operatorname{per}(g) = 1, \quad N(g) = \lceil T/g \rceil.
+$$
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Threshold pumping" data-exhibit-type="proof" data-exhibit-caption="The sequence climbs until it saturates at T after ⌈T/g⌉ steps, then is constant."}
+
+:::: exhibit-body
+For $g = 0$ the sequence is constantly zero. If $T = 0$, this is the only
+case. For $g > 0$,
+
+$$
+ng = \min(T, ng)
+$$
+
+in ordinary integer notation. The first $n$ for which $ng$ reaches $T$ is
+$\lceil T/g \rceil$. From that index onward the sequence is constantly $T$,
+hence the period is $1$. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-aperiodic}
+
+Remark 7.7
+Aperiodic saturation
+
+
+
+Threshold monoids show why arbitrary finite commutative monoids cannot be
+treated as semilattices of abelian groups. In $\Theta_2$, the element $1$ has
+the sequence $0, 1, 2, 2, 2, \ldots$; this has a genuine preperiod and no
+group-like cycle before saturation.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Hybrid threshold-residue pumping" data-exhibit-type="proof" data-exhibit-caption="The threshold coordinate fixes the index; the cyclic coordinate fixes the period."}
+
+:::: exhibit-body
+If $g_{\text{thr}} = 0$, the threshold coordinate is constantly $0$ and the
+product period is exactly the cyclic order. If $g_{\text{thr}} > 0$, the
+threshold coordinate strictly changes until the first index
+
+$$
+i = \lceil T/g_{\text{thr}} \rceil,
+$$
+
+at which it reaches $T$ and remains constant. Thus no smaller index can work.
+From index $i$ onward, the threshold coordinate contributes period $1$, while
+the cyclic coordinate has least period $\operatorname{ord}(g_{\text{cyc}})$.
+Therefore the product has least period $\operatorname{ord}(g_{\text{cyc}})$
+from the least possible index $i$. [□]{.proof-qed}
+::::
+
+:::
+
+### Product bounds in general
+
+::: {.annotation .annotation--static #prop-coord-product}
+
+Proposition 7.9
+Coordinatewise product bound
+
+
+
+Let $N = N_1 \times \cdots \times N_r$ be a product of finite monoids and let
+$g = (g_1, \ldots, g_r)$. If $i_j = \operatorname{ind}(g_j)$ and $p_j =
+\operatorname{per}(g_j)$, then a valid index-period pair for $g$ is
+
+$$
+i = \max_j i_j, \quad p = \operatorname{lcm}_j p_j.
+$$
+
+Thus
+
+$$
+N(g) \leq \max_j i_j + \operatorname{lcm}_j p_j - 1.
+$$
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Coordinatewise product bound" data-exhibit-type="proof" data-exhibit-caption="Beyond the max index, adding the lcm of periods preserves every coordinate."}
+
+:::: exhibit-body
+For every coordinate $j$, the sequence $n g_j$ is periodic with period $p_j$
+from index $i_j$ onward. Once $n \geq \max_j i_j$, adding $p =
+\operatorname{lcm}_j p_j$ preserves every coordinate. Hence it preserves the
+product element. [□]{.proof-qed}
+::::
+
+:::
+
+## Examples: exact computations
+
+This section records concrete test families. These are not yet
+pursuit-evasion applications; they are calibration examples for the summary
+model.
+
+### One-node trees
+
+Let $A_n$ be the one-node tree whose root multiplicity is $n$.
+
+::: {.annotation .annotation--static #prop-one-node}
+
+Proposition 8.1
+One-node criterion
+
+
+
+For fixed $\mathcal{R}$, if
+
+$$
+\mu(n) = \mu(m),
+$$
+
+then
+
+$$
+A_n \sim_{\mathcal{R}} A_m.
+$$
+
+Conversely, if $\mu(n) \neq \mu(m)$ and $|S| \geq 2$, then $A_n$ and $A_m$
+are separated by some summary in $D(\mathcal{R})$.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="One-node criterion" data-exhibit-type="proof" data-exhibit-caption="A one-node tree has empty child aggregate, so its state depends only on μ(n)."}
+
+:::: exhibit-body
+A one-node tree has empty child aggregate. Hence for every $P = (\alpha_P,
+f_P)$,
+
+$$
+P(A_n) = f_P(\mu(n), 0_M).
+$$
+
+If $\mu(n) = \mu(m)$, these values are equal for all $P$, so [Theorem
+3.3](#thm-behavior-vector) gives equivalence.
+
+If $\mu(n) \neq \mu(m)$ and $|S| \geq 2$, choose two distinct states $s_0,
+s_1 \in S$. Define $f$ so that $f(\mu(n), 0_M) = s_0$ and $f(\mu(m), 0_M) =
+s_1$, extending $f$ arbitrarily elsewhere. Choose any $\alpha : S \to M$. The
+resulting summary separates $A_n$ and $A_m$. [□]{.proof-qed}
+::::
+
+:::
+
+### Stars
+
+Fix a rooted tree $Q$ with behavior vector $b = \beta_{\mathcal{R}}(Q)$. Let
+$\mathrm{Star}_n(a; Q)$ be the tree with root observed multiplicity label $a
+\in A$ and $n$ children, each isomorphic to $Q$. More precisely, choose any
+root multiplicity $r$ with $\mu(r) = a$.
+
+::: {.annotation .annotation--static #prop-stars}
+
+Proposition 8.2
+Star aggregate criterion
+
+
+
+For fixed $a$ and $Q$, if
+
+$$
+n \gamma_b = m \gamma_b
+$$
+
+in the product monoid $M^{D(\mathcal{R})}$, then
+
+$$
+\mathrm{Star}_n(a; Q) \sim_{\mathcal{R}} \mathrm{Star}_m(a; Q).
+$$
+
+More generally, the two stars have the same behavior vector exactly when, for
+every summary $P \in D(\mathcal{R})$,
+
+$$
+f_P(a, n \alpha_P(b_P)) = f_P(a, m \alpha_P(b_P)).
+$$
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Star aggregate criterion" data-exhibit-type="proof" data-exhibit-caption="Root state is f_P(a, n α_P(b_P)); product-aggregate equality forces coordinatewise equality."}
+
+:::: exhibit-body
+For every summary $P$, the root state is $f_P(a, n \alpha_P(b_P))$ for the
+first star and $f_P(a, m \alpha_P(b_P))$ for the second. The coordinatewise
+equality displayed in the proposition is therefore exactly behavior-vector
+equality. The product-monoid identity $n \gamma_b = m \gamma_b$ implies that
+equality, since its $P$-coordinate is precisely
+
+$$
+n \alpha_P(b_P) = m \alpha_P(b_P)
+$$
+
+for every $P$. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-aggregate-sufficient}
+
+Remark 8.3
+Why aggregate equality is sufficient, not necessary
+
+
+
+The implication from product-aggregate equality to star equivalence is the
+one needed for pumping and normal forms. It is not generally necessary: two
+different aggregates may be identified by all root update maps at the
+observed label $a$ for the summaries under discussion. In particular examples
+one can often force separation by choosing a summary whose update map
+distinguishes the two aggregates, but the exact statement is the displayed
+coordinatewise criterion.
+
+
+
+Assume unit contribution $\gamma_b = g$.
+
+1. Boolean support: all positive $n$ are equivalent; $n = 0$ is separate from
+ $n > 0$ if $g \neq 0$.
+2. Cyclic $\mathbb{Z}/q\mathbb{Z}$: $n$ and $m$ are equivalent exactly modulo
+ $\operatorname{ord}(g)$.
+3. Threshold $\Theta_T$ with $g = 1$: $n$ and $m$ are equivalent iff either
+ $n = m < T$ or both $n, m \geq T$.
+
+
+:::
+
+### Unary chains
+
+Unary-chain behavior is controlled by finite transformations on behavior
+vectors, not directly by the horizontal child-aggregation monoid.
+
+::: {.annotation .annotation--static #def-unary-map}
+
+Definition 8.5
+Unary extension map
+
+
+
+For each observed multiplicity label $a \in A$, define
+
+$$
+U_a : B_{\mathcal{R}} \to B_{\mathcal{R}}
+$$
+
+by declaring $U_a(b)$ to be the behavior vector of a new root with observed
+label $a$ and exactly one child of behavior type $b$. Coordinatewise,
+
+$$
+(U_a(b))_P = f_P(a, \alpha_P(b_P)).
+$$
+
+
+Proposition 8.6
+Unary chains are eventually periodic
+
+
+
+Fix $a \in A$ and $b \in B_{\mathcal{R}}$. The sequence
+
+$$
+b,\; U_a(b),\; U_a^2(b),\; U_a^3(b),\; \ldots
+$$
+
+is eventually periodic. In particular, among the first $|B_{\mathcal{R}}| +
+1$ terms two are equal.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Unary chains are eventually periodic" data-exhibit-type="proof" data-exhibit-caption="U_a is a self-map of the finite set B_R; every finite-set orbit is eventually periodic."}
+
+:::: exhibit-body
+The map $U_a$ is a self-map of the finite set $B_{\mathcal{R}}$. Every orbit
+of a self-map on a finite set is eventually periodic, and the pigeonhole
+principle gives a repetition among the first $|B_{\mathcal{R}}| + 1$ terms.
+[□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #cor-unary-pumping}
+
+Corollary 8.7
+Unary chain pumping
+
+
+
+Any sufficiently long constant-label unary chain contains a proper subchain
+whose deletion preserves the behavior vector at the top of the chain. A crude
+bound is $|B_{\mathcal{R}}| + 1$ vertices for a repeated behavior vector.
+
+
+
+If labels vary along a unary path, one obtains the finite transformation
+semigroup generated by the maps $U_a$ for $a \in A$: this is the subsemigroup,
+under composition, of the finite monoid of all self-maps of $B_{\mathcal{R}}$
+generated by the maps $U_a$. Long labeled unary words can be pumped using
+repetitions in this finite transformation semigroup, but the
+minimal-representative argument in [Section
+9](#global-normal-representatives) gives a simpler global height bound for
+entire trees.
+
+
+:::
+
+### Split versus concentrated examples
+
+Let $Q$ be a tree of behavior type $b$. A simple split tree has a root with
+two children of type $b$, hence horizontal contribution
+
+$$
+2 \gamma_b.
+$$
+
+A concentrated competitor has a root with one child $R$ of behavior type $c$,
+where the internal construction of $R$ may have encoded some information that
+resembles two copies of $b$ at a lower level.
+
+::: {.annotation .annotation--static #prop-split-concentrated}
+
+Proposition 8.9
+Diagnostic criterion
+
+
+
+Suppose two trees have the same observed root label $a$. One has child
+multiset consisting of two children of behavior type $b$, and the other has
+one child of behavior type $c$. Their root behavior vectors are equal exactly
+when, for every $P \in D(\mathcal{R})$,
+
+$$
+f_P(a, 2\alpha_P(b_P)) = f_P(a, \alpha_P(c_P)).
+$$
+
+Equivalently, equality follows from the stronger aggregate identity
+
+$$
+2 \gamma_b = \gamma_c
+$$
+
+in $M^{D(\mathcal{R})}$, but may also occur accidentally because all update
+maps in question identify the two aggregates at label $a$.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Diagnostic criterion" data-exhibit-type="proof" data-exhibit-caption="Immediate from coordinatewise root evaluation; aggregate equality is sufficient but not necessary."}
+
+:::: exhibit-body
+This is immediate from the coordinatewise evaluation formula at the root.
+Aggregate equality is sufficient. It is not necessary for an arbitrary fixed
+subfamily of updates because two different aggregates may be mapped to the
+same state by every relevant $f_P$ at the label $a$. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-no-converse}
+
+Remark 8.10
+No automatic converse from aggregate inequality
+
+
+
+The stronger aggregate identity $2\gamma_b = \gamma_c$ is a clean sufficient
+condition for equality of the two root behavior vectors. Its failure is not,
+by itself, a clean separation theorem. The behavior coordinates $b_P, c_P$ of
+the child subtrees are fixed properties of those subtrees, indexed by every
+$P \in D(\mathcal{R})$. If a particular coordinate $P^*$ witnesses aggregate
+inequality in $M^{D(\mathcal{R})}$, the summary $P^*$ itself may still fail to
+separate the parents because $f_{P^*}$ may identify the two aggregates. One
+cannot remedy this by "switching to a different $f$" while holding the child
+contributions fixed: choosing a different summary $P'$ means looking at a
+different coordinate $P'$ of the child behavior vectors, with potentially
+different aggregate values. Thus separation should be checked by the exact
+coordinatewise criterion in [Proposition 8.2](#prop-stars) and [Proposition
+8.9](#prop-split-concentrated), not by aggregate inequality alone. This is
+precisely why split-versus-concentrated examples are diagnostically
+interesting rather than trivial.
+
+
+
+This is the first family where horizontal aggregation interacts with vertical
+recursion. It is a natural bridge to later pursuit-evasion questions about
+whether support is split across branches or concentrated inside one branch.
+
+
+:::
+
+## Global normal representatives
+
+Exact sibling pumping bounds branching. To obtain a finite universe of
+representatives, one also needs a height bound. The cleanest argument is not a
+unary-chain analysis; it is minimality.
+
+::: {.annotation .annotation--static #def-label-rep}
+
+Definition 9.1
+Observed-label representative
+
+
+
+Choose once and for all a representative integer $r(a) \in \mathbb{N}$ for
+each $a \in A$ with $\mu(r(a)) = a$, for every $a$ in the image of $\mu$. No
+representative is needed for $a \notin \operatorname{im}(\mu)$, since no
+vertex of any tree has observed label $a$. A tree is *label-normalized* if
+every vertex with observed label $a$ has actual multiplicity $r(a)$.
+
+
+
+Every tree $T$ is $\sim_{\mathcal{R}}$-equivalent to a label-normalized tree
+$T^{\ell}$ with the same underlying rooted unordered tree and the same
+observed labels.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Label normalization preserves behavior" data-exhibit-type="proof" data-exhibit-caption="Summaries use multiplicities only through μ, so replacing m by r(μ(m)) changes nothing."}
+
+:::: exhibit-body
+Replace each vertex multiplicity $m$ by $r(\mu(m))$. Every summary in
+$D(\mathcal{R})$ uses multiplicities only through $\mu$, so every bottom-up
+computation is unchanged. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #def-size-minimal}
+
+Definition 9.3
+Size-minimal representative
+
+
+
+A tree $T$ is *size-minimal* for its behavior vector if among all trees $T'$
+with $\beta_{\mathcal{R}}(T') = \beta_{\mathcal{R}}(T)$, the number of
+vertices of $T'$ is minimized. It is *normalized size-minimal* if it is also
+label-normalized.
+
+
+
+Every realizable behavior vector has a normalized size-minimal
+representative.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Size-minimal representatives exist" data-exhibit-type="proof" data-exhibit-caption="Pick a fewest-vertex realizer, then label-normalize it without changing vertex count."}
+
+:::: exhibit-body
+The behavior vector is realizable, so at least one tree realizes it. Among
+all realizing trees, choose one with the fewest vertices. Apply [Lemma
+9.2](#lem-label-normalization) to normalize labels without changing the
+number of vertices or the behavior vector. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #thm-minimal-sibling-bounded}
+
+Theorem 9.5
+Minimal representatives are sibling-bounded
+
+
+
+Let $T$ be a normalized size-minimal representative. At every node $v$ of
+$T$, each child behavior type $b$ occurs at most
+
+$$
+N_{\mathcal{R}}(b) = \operatorname{ind}(\gamma_b) + \operatorname{per}(\gamma_b) - 1
+$$
+
+times.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Minimal representatives are sibling-bounded" data-exhibit-type="proof" data-exhibit-caption="An over-full sibling type could be pumped down, contradicting size-minimality."}
+
+:::: exhibit-body
+Suppose some node $v$ has $n_b > N_{\mathcal{R}}(b)$ children of behavior
+type $b$. By [Lemma 5.4](#lem-unary-pumping), replacing $n_b$ by
+$\operatorname{red}_{\gamma_b}(n_b)$ preserves the contribution of type $b$,
+and by the same lemma this reduced number satisfies
+$\operatorname{red}_{\gamma_b}(n_b) < n_b$. Delete enough children of type
+$b$ to leave exactly $\operatorname{red}_{\gamma_b}(n_b)$ such children,
+leaving all other child types unchanged. The simultaneous child aggregate at
+$v$ is unchanged, so the behavior vector of the subtree rooted at $v$ is
+unchanged. By [Corollary 3.5](#cor-congruence), the behavior vector of the
+whole tree is unchanged. But the number of vertices strictly decreases,
+contradicting size-minimality. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #thm-no-repeat}
+
+Theorem 9.6
+Minimal representatives have no repeated behavior along a path
+
+
+
+Let $T$ be a normalized size-minimal representative. No root-to-leaf path of
+$T$ contains two distinct vertices $u$ and $v$, with $v$ a proper descendant
+of $u$, such that
+
+$$
+\beta_{\mathcal{R}}(T_u) = \beta_{\mathcal{R}}(T_v).
+$$
+
+Consequently every root-to-leaf path has at most $|B_{\mathcal{R}}|$
+vertices.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Minimal representatives have no repeated behavior along a path" data-exhibit-type="proof" data-exhibit-caption="A repeated behavior vector lets the upper subtree be replaced by the lower one, shrinking the tree."}
+
+:::: exhibit-body
+Suppose $v$ is a proper descendant of $u$ and the rooted subtrees $T_u$ and
+$T_v$ have the same behavior vector. Replace the subtree $T_u$ by the proper
+descendant subtree $T_v$. Since the two subtrees are
+$\sim_{\mathcal{R}}$-equivalent by [Theorem 3.3](#thm-behavior-vector),
+[Corollary 3.5](#cor-congruence) implies that the behavior vector of the
+whole tree is unchanged. The replacement strictly decreases the number of
+vertices, contradicting size-minimality. Therefore no behavior vector
+repeats along a path. Since an actual path encounters only realizable
+behavior vectors, every path has at most the number of realizable behavior
+vectors, and in particular at most $|B_{\mathcal{R}}|$ vertices.
+[□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #def-normal-universe}
+
+Definition 9.7
+Normal universe
+
+
+
+Let $U_{\mathcal{R}}$ be the finite set of all label-normalized rooted
+cop-labeled trees satisfying:
+
+1. every root-to-leaf path has at most $|B_{\mathcal{R}}|$ vertices;
+2. at every node, behavior type $b$ occurs among the children at most
+ $N_{\mathcal{R}}(b)$ times, for every $b \in B_{\mathcal{R}}$.
+
+
+
+One may replace $|B_{\mathcal{R}}|$ and the sum over all formal $b \in
+B_{\mathcal{R}}$ by the corresponding quantities for realizable behavior
+vectors. The formal version is cruder but avoids a separate realizability
+computation. Since realizability is defined existentially over all trees and
+is not in general algorithmically transparent, the formal version is also the
+version most directly usable in computations.
+
+
+Theorem 9.9
+Finite global normal representatives
+
+
+
+Every $\sim_{\mathcal{R}}$-equivalence class has a representative in the
+finite universe $U_{\mathcal{R}}$.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Finite global normal representatives" data-exhibit-type="proof" data-exhibit-caption="A normalized size-minimal representative satisfies both universe constraints; the universe is finite."}
+
+:::: exhibit-body
+Let $b$ be a realizable behavior vector. By [Lemma
+9.4](#lem-minimal-exists), choose a normalized size-minimal representative
+$T$ realizing $b$. By [Theorem 9.5](#thm-minimal-sibling-bounded), $T$
+satisfies the exact sibling bounds. By [Theorem 9.6](#thm-no-repeat), its
+root-to-leaf paths have at most $|B_{\mathcal{R}}|$ vertices. Thus $T \in
+U_{\mathcal{R}}$.
+
+The set $U_{\mathcal{R}}$ is finite because labels come from the finite image
+of $\mu$, height is bounded, and at each node the number of children is
+bounded by
+
+$$
+C_{\mathcal{R}} = \sum_{b \in B_{\mathcal{R}}} N_{\mathcal{R}}(b).
+$$
+
+There are only finitely many finite unordered rooted trees with bounded
+height, bounded branching, and labels from a finite alphabet.
+[□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #cor-size-bound}
+
+Corollary 9.10
+Crude size bound
+
+
+
+Let
+
+$$
+H_{\mathcal{R}} := |B_{\mathcal{R}}|, \quad C_{\mathcal{R}} := \sum_{b \in B_{\mathcal{R}}} N_{\mathcal{R}}(b).
+$$
+
+Then every class has a representative with at most
+
+$$
+1 + C_{\mathcal{R}} + C_{\mathcal{R}}^2 + \cdots + C_{\mathcal{R}}^{H_{\mathcal{R}} - 1}
+$$
+
+vertices, with the usual interpretation as $H_{\mathcal{R}}$ when
+$C_{\mathcal{R}} = 1$.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Crude size bound" data-exhibit-type="proof" data-exhibit-caption="Sum the geometric series for ≤ H_R levels with branching ≤ C_R."}
+
+:::: exhibit-body
+Here $H_{\mathcal{R}}$ bounds the number of vertices on a root-to-leaf path,
+so the tree has at most $H_{\mathcal{R}}$ levels, indexed $0, 1, \ldots,
+H_{\mathcal{R}} - 1$. With branching at most $C_{\mathcal{R}}$, level $d$ has
+at most $C_{\mathcal{R}}^d$ vertices. Summing over the levels gives the
+displayed bound; when $C_{\mathcal{R}} = 1$ the geometric sum has
+$H_{\mathcal{R}}$ terms each equal to $1$, giving $H_{\mathcal{R}}$.
+[□]{.proof-qed}
+::::
+
+:::
+
+## Canonical representatives
+
+A finite normal universe gives canonical representatives once one imposes an
+external tie-break. This is safer than claiming that minimal representatives
+are intrinsically unique, which is generally false.
+
+::: {.annotation .annotation--static #def-external-order}
+
+Definition 10.1
+External ordering
+
+
+
+Fix a total order $\preceq$ on the finite universe $U_{\mathcal{R}}$. For
+example, order first by number of vertices, then by height, then recursively
+by sorted child lists and vertex labels.
+
+
+
+For a realizable behavior vector $b$, define
+
+$$
+\operatorname{Can}_{\mathcal{R}}(b)
+$$
+
+to be the $\preceq$-least tree in $U_{\mathcal{R}}$ with behavior vector $b$.
+
+
+
+After choosing the external order $\preceq$, every
+$\sim_{\mathcal{R}}$-equivalence class has a unique selected canonical
+representative.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Canonical representative theorem" data-exhibit-type="proof" data-exhibit-caption="Each class meets the finite totally ordered universe in a nonempty set with a unique least element."}
+
+:::: exhibit-body
+By [Theorem 9.9](#thm-normal-universe), every class has at least one
+representative in $U_{\mathcal{R}}$. Since $U_{\mathcal{R}}$ is finite and
+totally ordered by $\preceq$, each nonempty subset has a unique least
+element. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-no-uniqueness}
+
+Remark 10.4
+No intrinsic uniqueness claimed
+
+
+
+The theorem does not claim that each class has a unique minimal tree in any
+intrinsic sense. Different non-isomorphic trees of the same size may realize
+the same behavior vector. The uniqueness is selected uniqueness after a
+chosen tie-breaking order.
+
+
+:::
+
+## What has been proved and what has not
+
+- *Proved:* fixed-resource equivalence equals behavior-vector equality.
+- *Proved:* exact sibling pumping is governed by the index and period of each
+ product contribution element $\gamma_b$.
+- *Proved:* Boolean, cyclic, threshold, and hybrid threshold-residue monoids
+ have explicit pumping bounds.
+- *Proved:* every fixed-resource class has a finite normal representative,
+ and an externally selected canonical representative.
+- *Not proved:* any global decomposition theorem for arbitrary finite
+ commutative monoids.
+- *Not claimed:* intrinsic uniqueness of minimal representatives.
+- *Not proved:* comparison with order-$r$ profiles.
+- *Not proved:* nondefinability or definability of pursuit-evasion
+ properties.
+
+## Conclusion
+
+The fixed-resource monoid-aggregated model now has a sharper structural core.
+The essential invariant for sibling multiplicities is the index-period pair
+of the product contribution element $\gamma_b$. This converts the original
+crude finite-product pumping lemma into an exact normal-form statement. It
+also clarifies the qualitative meanings of the standard monoid families:
+Boolean semilattices track support, cyclic groups track residue, threshold
+monoids track saturation, and hybrids combine these effects.
+
+The global canonical-form theory is also cleaner than expected. Sibling
+pumping bounds branching; size-minimality bounds height, because a repeated
+behavior vector along a path could be contracted. Therefore every
+fixed-resource equivalence class has a representative in a finite universe,
+and canonical representatives exist after external tie-breaking.
+
+The next mathematical frontier is no longer fixed-resource equivalence
+itself. That relation is fully finite and behavior-vector controlled. The
+hard questions concern how separation cost grows as one varies the allowed
+multiplicity observations, state sets, and monoids, and whether
+pursuit-evasion properties cut across the resulting bounded-resource
+theories.
+
+::::: aftermatter
+
+## Appendix A — Algorithmic consequences
+
+The theory is constructive, although often computationally enormous.
+
+::: {.annotation .annotation--static #prop-decidability}
+
+Proposition A.1
+Decidability for fixed resources
+
+
+
+For fixed finite resource data $\mathcal{R}$ and finite rooted cop-labeled
+trees $X, Y$, it is decidable whether
+
+$$
+X \sim_{\mathcal{R}} Y.
+$$
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Decidability for fixed resources" data-exhibit-type="proof" data-exhibit-caption="Enumerate the finite class D(R), evaluate both trees bottom-up, compare all coordinates."}
+
+:::: exhibit-body
+The class $D(\mathcal{R})$ is finite by [Lemma 2.7](#lem-cardinality). One
+may enumerate all summaries $P \in D(\mathcal{R})$, compute $P(X)$ and $P(Y)$
+bottom-up, and compare all coordinates. By [Theorem
+3.3](#thm-behavior-vector), the trees are equivalent iff all coordinates
+agree. [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #prop-computable-canonical}
+
+Proposition A.2
+Computable canonical representative, in principle
+
+
+
+For fixed $\mathcal{R}$, a chosen external order $\preceq$ on
+$U_{\mathcal{R}}$, and an input tree $T$, the canonical representative of the
+class of $T$ is computable by finite search.
+
+
+:::
+
+::: {.exhibit .exhibit--proof data-exhibit-name="Computable canonical representative, in principle" data-exhibit-type="proof" data-exhibit-caption="Compute β_R(T), then scan U_R in ≼-order for the first tree with the same behavior vector."}
+
+:::: exhibit-body
+Compute $b = \beta_{\mathcal{R}}(T)$ by enumerating $D(\mathcal{R})$. Then
+enumerate the finite universe $U_{\mathcal{R}}$ in $\preceq$-order and return
+the first tree $U$ with $\beta_{\mathcal{R}}(U) = b$. Termination follows from
+[Theorem 9.9](#thm-normal-universe). [□]{.proof-qed}
+::::
+
+:::
+
+::: {.annotation .annotation--static #rem-practical}
+
+Remark A.3
+Practical versus theoretical computation
+
+
+
+The bounds involving $|D(\mathcal{R})|$ are generally huge. The point of the
+theorem is structural finiteness and conceptual normalization, not immediate
+efficient implementation. For special monoid families, the exact
+index-period bounds above are the first route toward usable computations.
+
+
+:::
+
+## Appendix B — Resource-growth separation complexity
+
+For fixed $\mathcal{R}$, equivalence is completely characterized by the
+behavior vector. The more interesting long-term invariant appears when
+resources vary.
+
+::: {.annotation .annotation--static #def-resource-family}
+
+Definition B.1
+Resource family
+
+
+
+A *resource family* $\mathcal{F}$ is a collection of finite resource data
+$\mathcal{R}$. Examples include:
+
+1. support-only resources with bounded $|S|$;
+2. threshold resources with threshold $T \leq t$ and $|S| \leq s$;
+3. cyclic resources with modulus $q \leq Q$ and $|S| \leq s$;
+4. hybrid threshold-residue resources with bounded thresholds, moduli, and
+ state counts.
+
+
+Definition B.2
+Separation over a resource family
+
+
+
+Given a resource family $\mathcal{F}$, say that $X$ and $Y$ are *separated by
+$\mathcal{F}$* if there exists $\mathcal{R} \in \mathcal{F}$ and $P \in
+D(\mathcal{R})$ such that
+
+$$
+P(X) \neq P(Y).
+$$
+
+Equivalently, $\beta_{\mathcal{R}}(X) \neq \beta_{\mathcal{R}}(Y)$ for some
+$\mathcal{R} \in \mathcal{F}$.
+
+
+
+Let $\kappa(\mathcal{R})$ be a chosen cost of a resource datum, for example a
+tuple involving $|A|$, $|S|$, $|M|$, the threshold parameter, the modulus, or
+the description length of $\mu$ and $\oplus$. Define
+
+$$
+\operatorname{sep}_{\mathcal{F}}(X, Y)
+$$
+
+to be the least cost of a resource datum $\mathcal{R} \in \mathcal{F}$
+separating $X$ and $Y$, and set $\operatorname{sep}_{\mathcal{F}}(X, Y) =
+\infty$ if no $\mathcal{R} \in \mathcal{F}$ separates them.
+
+
+
+For fixed $\mathcal{R}$, a game characterization is nearly tautological:
+Spoiler can choose a differing coordinate $P \in D(\mathcal{R})$ if one
+exists, and otherwise Duplicator wins because behavior vectors agree. A
+nontrivial game should therefore characterize resource growth, restricted
+resource families, or bounded access to coordinates, not merely the
+fixed-$\mathcal{R}$ relation. In particular, the interesting game will need to
+encode a budget on which coordinates $P$ Spoiler is permitted to access at
+each round, with cost tied to $\kappa$.
+
+
+:::
+
+## Appendix C — Near-term theorem targets
+
+The present note proves the first three targets below and sets up the rest.
+
+- **T1. Exact sibling pumping.** Child counts of behavior type $b$ reduce by
+ the index-period pair of $\gamma_b$. Proved in [Theorem
+ 6.2](#thm-sibling-pumping).
+- **T2. Canonical family bounds.** Boolean, cyclic, threshold, and hybrid
+ monoids have explicit pumping signatures. Proved in [Section
+ 7](#canonical-monoid-families).
+- **T3. Finite normal representatives.** Every fixed-resource class has a
+ representative in a finite normal universe. Proved in [Theorem
+ 9.9](#thm-normal-universe).
+- **T4. Efficient special-case canonicalization.** For concrete resource
+ families, replace the huge all-summary behavior vector by smaller
+ sufficient invariants.
+- **T5. Separation complexity examples.** Compute exact or asymptotic costs
+ for one-node, star, unary-chain, and split/concentrated families under
+ support, threshold, cyclic, and hybrid resources.
+- **T6. Resource-growth games.** Design a game that characterizes bounded
+ resource families rather than fixed-$\mathcal{R}$ equality of behavior
+ vectors.
+- **T7. Pursuit-evasion tests.** Only after the previous items, ask whether
+ local pursuit properties are definable or separable in specific resource
+ families.
+
+:::::
diff --git a/content/essays/index-period-normal-forms/mark.svg b/content/essays/index-period-normal-forms/mark.svg
new file mode 100644
index 0000000..ddbf638
--- /dev/null
+++ b/content/essays/index-period-normal-forms/mark.svg
@@ -0,0 +1,70 @@
+