levineuwirth.org/content/essays/index-period-normal-forms/index.md

---
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}
<div class="annotation-header">
<span class="annotation-label">Definition 2.1</span>
<span class="annotation-name">Rooted cop-labeled tree</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #def-context}
<div class="annotation-header">
<span class="annotation-label">Definition 2.2</span>
<span class="annotation-name">Rooted one-hole context</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.annotation .annotation--static #def-resource-datum}
<div class="annotation-header">
<span class="annotation-label">Definition 2.3</span>
<span class="annotation-name">Finite resource datum</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #warn-actual-resources}
<div class="annotation-header">
<span class="annotation-label">Warning 2.4</span>
<span class="annotation-name">Actual resources, not just cardinalities</span>
</div>
<div class="annotation-body">

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}$.

</div>
:::

::: {.annotation .annotation--static #def-summary}
<div class="annotation-header">
<span class="annotation-label">Definition 2.5</span>
<span class="annotation-name">Monoid-aggregated summary</span>
</div>
<div class="annotation-body">

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)$.

</div>
:::

::: {.annotation .annotation--static #def-fixed-class}
<div class="annotation-header">
<span class="annotation-label">Definition 2.6</span>
<span class="annotation-name">The fixed-resource class</span>
</div>
<div class="annotation-body">

Let $D(\mathcal{R})$ be the finite class of all monoid-aggregated summaries
over $\mathcal{R}$.

</div>
:::

::: {.annotation .annotation--static #lem-cardinality}
<div class="annotation-header">
<span class="annotation-label">Lemma 2.7</span>
<span class="annotation-name">Crude cardinality of the summary class</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Definition 3.1</span>
<span class="annotation-name">Behavior vector</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.annotation .annotation--static #def-context-equiv}
<div class="annotation-header">
<span class="annotation-label">Definition 3.2</span>
<span class="annotation-name">Fixed-resource context equivalence</span>
</div>
<div class="annotation-body">

For rooted cop-labeled trees $X, Y$, define

$$
X \sim_{\mathcal{R}} Y
$$

if for every rooted one-hole context $K[\square]$ and every summary $P \in
D(\mathcal{R})$,

$$
P(K[X]) = P(K[Y]).
$$

</div>
:::

::: {.annotation .annotation--static #thm-behavior-vector}
<div class="annotation-header">
<span class="annotation-label">Theorem 3.3</span>
<span class="annotation-name">Fixed-resource equivalence is behavior-vector equality</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark 3.4</span>
<span class="annotation-name">Behavior type</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #cor-congruence}
<div class="annotation-header">
<span class="annotation-label">Corollary 3.5</span>
<span class="annotation-name">Fixed-resource congruence</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Definition 4.1</span>
<span class="annotation-name">Product monoid</span>
</div>
<div class="annotation-body">

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})}$.

</div>
:::

::: {.annotation .annotation--static #def-contribution}
<div class="annotation-header">
<span class="annotation-label">Definition 4.2</span>
<span class="annotation-name">Contribution element of a behavior type</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #rem-notation}
<div class="annotation-header">
<span class="annotation-label">Remark 4.3</span>
<span class="annotation-name">Notation checkpoint</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #lem-aggregate}
<div class="annotation-header">
<span class="annotation-label">Lemma 4.4</span>
<span class="annotation-name">Sibling aggregate as a product-monoid sum</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark 4.5</span>
<span class="annotation-name">Why this is the right object</span>
</div>
<div class="annotation-body">

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.

</div>
:::

## 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}
<div class="annotation-header">
<span class="annotation-label">Definition 5.1</span>
<span class="annotation-name">Index and period of an element</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #lem-existence}
<div class="annotation-header">
<span class="annotation-label">Lemma 5.2</span>
<span class="annotation-name">Existence of index and period</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Definition 5.3</span>
<span class="annotation-name">Canonical reduction of a coefficient</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.annotation .annotation--static #lem-unary-pumping}
<div class="annotation-header">
<span class="annotation-label">Lemma 5.4</span>
<span class="annotation-name">Exact unary pumping</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Definition 5.5</span>
<span class="annotation-name">Contribution bound</span>
</div>
<div class="annotation-body">

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.

</div>
:::

## Exact sibling pumping

We now apply the index-period decomposition to behavior-type contributions.

::: {.annotation .annotation--static #def-sibling-signature}
<div class="annotation-header">
<span class="annotation-label">Definition 6.1</span>
<span class="annotation-name">Sibling signature</span>
</div>
<div class="annotation-body">

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).
$$

</div>
:::

::: {.annotation .annotation--static #thm-sibling-pumping}
<div class="annotation-header">
<span class="annotation-label">Theorem 6.2</span>
<span class="annotation-name">Exact sibling pumping at one node</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Corollary 6.3</span>
<span class="annotation-name">Exact sibling normal form</span>
</div>
<div class="annotation-body">

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}}.
$$

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark 6.4</span>
<span class="annotation-name">Realizable versus formal behavior types</span>
</div>
<div class="annotation-body">

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.

</div>
:::

## Canonical monoid families

The index-period form makes the standard monoid families transparent.

### Boolean semilattices

::: {.annotation .annotation--static #prop-boolean}
<div class="annotation-header">
<span class="annotation-label">Proposition 7.1</span>
<span class="annotation-name">Boolean support pumping</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Corollary 7.2</span>
<span class="annotation-name">Boolean product bound</span>
</div>
<div class="annotation-body">

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.

</div>
:::

### Finite cyclic groups

::: {.annotation .annotation--static #prop-cyclic}
<div class="annotation-header">
<span class="annotation-label">Proposition 7.3</span>
<span class="annotation-name">Cyclic group pumping</span>
</div>
<div class="annotation-body">

Let $M = \mathbb{Z}/q\mathbb{Z}$ under addition. For $g \in M$,

$$
\operatorname{ind}(g) = 0, \quad \operatorname{per}(g) = \operatorname{ord}(g) = \frac{q}{\gcd(q, g)},
$$

with the convention that $\operatorname{ord}(0) = 1$. Thus

$$
N(g) = \operatorname{ord}(g) - 1.
$$

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Corollary 7.4</span>
<span class="annotation-name">Product of cyclic groups</span>
</div>
<div class="annotation-body">

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.

</div>
:::

### Threshold monoids

::: {.annotation .annotation--static #def-threshold}
<div class="annotation-header">
<span class="annotation-label">Definition 7.5</span>
<span class="annotation-name">Threshold monoid</span>
</div>
<div class="annotation-body">

For $T \geq 0$, let

$$
\Theta_T := \{0, 1, \ldots, T\}
$$

with operation

$$
x \oplus y := \min(T, x + y)
$$

and identity $0$.

</div>
:::

::: {.annotation .annotation--static #prop-threshold}
<div class="annotation-header">
<span class="annotation-label">Proposition 7.6</span>
<span class="annotation-name">Threshold pumping</span>
</div>
<div class="annotation-body">

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.
$$

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark 7.7</span>
<span class="annotation-name">Aperiodic saturation</span>
</div>
<div class="annotation-body">

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.

</div>
:::

### Threshold-times-cyclic products

::: {.annotation .annotation--static #prop-hybrid}
<div class="annotation-header">
<span class="annotation-label">Proposition 7.8</span>
<span class="annotation-name">Hybrid threshold-residue pumping</span>
</div>
<div class="annotation-body">

Let

$$
M = \Theta_T \times \mathbb{Z}/q\mathbb{Z}
$$

with coordinatewise operation, and let $g = (g_{\text{thr}}, g_{\text{cyc}})$.
Then

$$
\operatorname{ind}(g) = \begin{cases} 0, & g_{\text{thr}} = 0, \\ \lceil T/g_{\text{thr}} \rceil, & g_{\text{thr}} > 0, \end{cases}
$$

and

$$
\operatorname{per}(g) = \operatorname{ord}(g_{\text{cyc}}).
$$

Consequently

$$
N(g) = \operatorname{ind}(g) + \operatorname{per}(g) - 1.
$$

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Proposition 7.9</span>
<span class="annotation-name">Coordinatewise product bound</span>
</div>
<div class="annotation-body">

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.
$$

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Proposition 8.1</span>
<span class="annotation-name">One-node criterion</span>
</div>
<div class="annotation-body">

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})$.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Proposition 8.2</span>
<span class="annotation-name">Star aggregate criterion</span>
</div>
<div class="annotation-body">

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)).
$$

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark 8.3</span>
<span class="annotation-name">Why aggregate equality is sufficient, not necessary</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #ex-stars}
<div class="annotation-header">
<span class="annotation-label">Example 8.4</span>
<span class="annotation-name">Stars in standard monoids</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

### 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}
<div class="annotation-header">
<span class="annotation-label">Definition 8.5</span>
<span class="annotation-name">Unary extension map</span>
</div>
<div class="annotation-body">

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)).
$$

</div>
:::

::: {.annotation .annotation--static #prop-unary-periodic}
<div class="annotation-header">
<span class="annotation-label">Proposition 8.6</span>
<span class="annotation-name">Unary chains are eventually periodic</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Corollary 8.7</span>
<span class="annotation-name">Unary chain pumping</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #rem-variable-labels}
<div class="annotation-header">
<span class="annotation-label">Remark 8.8</span>
<span class="annotation-name">Variable labels</span>
</div>
<div class="annotation-body">

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.

</div>
:::

### 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}
<div class="annotation-header">
<span class="annotation-label">Proposition 8.9</span>
<span class="annotation-name">Diagnostic criterion</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark 8.10</span>
<span class="annotation-name">No automatic converse from aggregate inequality</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #rem-family-matters}
<div class="annotation-header">
<span class="annotation-label">Remark 8.11</span>
<span class="annotation-name">Why this family matters</span>
</div>
<div class="annotation-body">

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.

</div>
:::

## 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}
<div class="annotation-header">
<span class="annotation-label">Definition 9.1</span>
<span class="annotation-name">Observed-label representative</span>
</div>
<div class="annotation-body">

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)$.

</div>
:::

::: {.annotation .annotation--static #lem-label-normalization}
<div class="annotation-header">
<span class="annotation-label">Lemma 9.2</span>
<span class="annotation-name">Label normalization preserves behavior</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Definition 9.3</span>
<span class="annotation-name">Size-minimal representative</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #lem-minimal-exists}
<div class="annotation-header">
<span class="annotation-label">Lemma 9.4</span>
<span class="annotation-name">Size-minimal representatives exist</span>
</div>
<div class="annotation-body">

Every realizable behavior vector has a normalized size-minimal
representative.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Theorem 9.5</span>
<span class="annotation-name">Minimal representatives are sibling-bounded</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Theorem 9.6</span>
<span class="annotation-name">Minimal representatives have no repeated behavior along a path</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Definition 9.7</span>
<span class="annotation-name">Normal universe</span>
</div>
<div class="annotation-body">

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}}$.

</div>
:::

::: {.annotation .annotation--static #rem-sharper-universe}
<div class="annotation-header">
<span class="annotation-label">Remark 9.8</span>
<span class="annotation-name">Sharper realizable normal universe</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #thm-normal-universe}
<div class="annotation-header">
<span class="annotation-label">Theorem 9.9</span>
<span class="annotation-name">Finite global normal representatives</span>
</div>
<div class="annotation-body">

Every $\sim_{\mathcal{R}}$-equivalence class has a representative in the
finite universe $U_{\mathcal{R}}$.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Corollary 9.10</span>
<span class="annotation-name">Crude size bound</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Definition 10.1</span>
<span class="annotation-name">External ordering</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #def-canonical-rep}
<div class="annotation-header">
<span class="annotation-label">Definition 10.2</span>
<span class="annotation-name">Canonical representative</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

::: {.annotation .annotation--static #thm-canonical}
<div class="annotation-header">
<span class="annotation-label">Theorem 10.3</span>
<span class="annotation-name">Canonical representative theorem</span>
</div>
<div class="annotation-body">

After choosing the external order $\preceq$, every
$\sim_{\mathcal{R}}$-equivalence class has a unique selected canonical
representative.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark 10.4</span>
<span class="annotation-name">No intrinsic uniqueness claimed</span>
</div>
<div class="annotation-body">

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.

</div>
:::

## 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}
<div class="annotation-header">
<span class="annotation-label">Proposition A.1</span>
<span class="annotation-name">Decidability for fixed resources</span>
</div>
<div class="annotation-body">

For fixed finite resource data $\mathcal{R}$ and finite rooted cop-labeled
trees $X, Y$, it is decidable whether

$$
X \sim_{\mathcal{R}} Y.
$$

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Proposition A.2</span>
<span class="annotation-name">Computable canonical representative, in principle</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.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}
<div class="annotation-header">
<span class="annotation-label">Remark A.3</span>
<span class="annotation-name">Practical versus theoretical computation</span>
</div>
<div class="annotation-body">

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.

</div>
:::

## 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}
<div class="annotation-header">
<span class="annotation-label">Definition B.1</span>
<span class="annotation-name">Resource family</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #def-separation}
<div class="annotation-header">
<span class="annotation-label">Definition B.2</span>
<span class="annotation-name">Separation over a resource family</span>
</div>
<div class="annotation-body">

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}$.

</div>
:::

::: {.annotation .annotation--static #def-separation-cost}
<div class="annotation-header">
<span class="annotation-label">Definition B.3</span>
<span class="annotation-name">Separation cost, schematic</span>
</div>
<div class="annotation-body">

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.

</div>
:::

::: {.annotation .annotation--static #rem-games-deferred}
<div class="annotation-header">
<span class="annotation-label">Remark B.4</span>
<span class="annotation-name">Why games are deferred</span>
</div>
<div class="annotation-body">

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$.

</div>
:::

## 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.

:::::