Comparative Recognition Dynamics — Cumulative Checkpoint

Updated: 2026-08-23 10:00 MDT
Completed runs: 28
Authoritative scope: Short-horizon comparative program; no publication or GitLab work.

Run 1 target

For a deterministic bottom-up finite tree automaton, determine exactly when two ground trees or reachable states are indistinguishable by all one-hole tree contexts. Prove a finite distinguishing-depth bound and hostilely test the tempting replacement of genuine tree contexts by polynomial contexts carrying arbitrary automaton-state constants.

Native definitions

Let $\Sigma=(\Sigma_k)_{k\ge 0}$ be a finite ranked alphabet and

$$A=(Q,(\delta_f)_{f\in\Sigma},F)$$

a complete deterministic bottom-up finite tree automaton, where $\delta_f:Q^k\to Q$ for $f\in\Sigma_k$. Write $\widehat\delta:T_\Sigma\to Q$ for bottom-up evaluation and

$$R=\widehat\delta(T_\Sigma)$$

for the reachable state set. It is a $\Sigma$-subalgebra of (Q).

A one-hole tree context is a ranked tree over $\Sigma\cup{\square}$ containing exactly one nullary hole. Plugging a ground tree (t) into (C) is written (C[t]). If $p\in R$, choose any ground tree (t) with $\widehat\delta(t)=p$ and put

$$C^A(p)=\widehat\delta(C[t]).$$

Determinism makes this independent of the witness (t).

Let $\operatorname{UP}(R)$ be the unary polynomial transformations generated from the identity by repeatedly placing the current unary polynomial in one argument of some $f\in\Sigma_k$ and filling every other argument with a constant from (R). Define

$$p\equiv_A q \iff \forall P\in\operatorname{UP}(R),\quad P(p)\in F\Longleftrightarrow P(q)\in F.$$

For ground trees define the language-context relation

$$s\equiv_L t \iff \forall C,\quad C[s]\in L(A)\Longleftrightarrow C[t]\in L(A).$$

The hole-depth of a context is the number of ranked-symbol nodes on the path from its root to its hole.

CRD-TA-1: reachable context theorem

Statement

For every deterministic bottom-up finite tree automaton (A):

1. the transformations $C^A:R\to R$ induced by genuine one-hole tree contexts are exactly $\operatorname{UP}(R)$;

2. $\equiv_A$ is the largest $\Sigma$-congruence on (R) that saturates $F\cap R$;

3. for all ground trees (s,t),

   $$s\equiv_L t \iff \widehat\delta(s)\equiv_A\widehat\delta(t);$$

4. the map

   $$[t]_{\equiv_L}\longmapsto [\widehat\delta(t)]_{\equiv_A}$$

   is an isomorphism of ranked algebras $T_\Sigma/{\equiv_L}\cong R/{\equiv_A}$.

Proof

The substitution identity

$$\widehat\delta(C[t])=C^A(\widehat\delta(t))$$

follows by induction on the unique root-to-hole spine of (C).

For a genuine context, evaluate each ground sibling subtree on that spine. Every resulting sibling state lies in (R), so the induced map belongs to $\operatorname{UP}(R)$. Conversely, for each reachable state parameter used by a unary polynomial, choose a ground witness tree evaluating to that state and insert those witnesses as the sibling subtrees. This constructs a genuine tree context with the same transformation. Hence the two transformation sets are equal.

The identity polynomial shows that $\equiv_A$ saturates $F\cap R$. To show congruence, suppose $p_i\equiv_A q_i$ for $1\le i\le k$. For an arbitrary outer unary polynomial (P), replace the coordinates of $P(\delta_f(p_1,\ldots,p_k))$ one at a time. At coordinate (i), the map

$$x\longmapsto P(\delta_f(q_1,\ldots,q_{i-1},x,p_{i+1},\ldots,p_k))$$

is a unary polynomial over (R), so the replacement preserves final-state membership. Thus $\delta_f(p_1,\ldots,p_k)\equiv_A\delta_f(q_1,\ldots,q_k)$.

If $\theta$ is any congruence on (R) saturating $F\cap R$, then $p\mathrel\theta q$ implies $P(p)\mathrel\theta P(q)$ for every unary polynomial (P), and saturation forces equal final-state membership. Therefore $\theta\subseteq\equiv_A$, proving maximality.

Part 3 now follows immediately from the substitution identity and equality of the two context families. The evaluation map is a surjective homomorphism onto (R), and Part 3 says exactly that the inverse image of $\equiv_A$ is $\equiv_L$. The induced quotient map is therefore a bijective homomorphism, proving Part 4. $\square$

CRD-TA-2: sharp finite distinguishing-depth bound

Statement

Let $n=|R|\ge 2$. If two reachable states are not $\equiv_A$-equivalent, then a genuine one-hole tree context of hole-depth at most (n-2) distinguishes them. The bound is attained for every $n\ge 2$.

Proof of the upper bound

Let (E_h) identify states receiving the same final/nonfinal observation under every context of hole-depth at most (h). Thus (E_0) is the partition by membership in $F\cap R$. Let an elementary translation be one parent operation with the hole in one coordinate and reachable constants in all other coordinates. Then

[ E_{h+1}

E_h\cap \bigcap_u u^{-1}(E_h), ]

where (u) ranges over elementary translations. If (E_{h+1}=E_h), the relation is stable under every elementary translation, hence under every unary polynomial, so $E_h=\equiv_A$.

If all reachable states have the same finality, no context distinguishes any pair. Otherwise (E_0) has two blocks. Every nonstable round strictly increases the number of blocks, which can never exceed (n). Hence stability is reached by round (n-2), and every inequivalent pair has a distinguishing context of depth at most (n-2). $\square$

Sharpness family

For $n\ge2$, take constants $c_0,\ldots,c_{n-1}$, one unary symbol (u), states $R={0,\ldots,n-1}$, transitions

$$\delta(c_i)=i, \qquad \delta_u(i)=\min(i+1,n-1),$$

and final set ({n-1}). The states (0) and (1) agree under $u^h(\square)$ for every (h<n-2), while $u^{n-2}(\square)$ sends (1) to the final state (n-1) and (0) to the nonfinal state (n-2). Their least distinguishing depth is exactly (n-2).

Hostile audit: unreachable parameters are not tree contexts

The theorem fails if $\operatorname{UP}(R)$ is silently replaced by unary polynomials carrying arbitrary constants from all of (Q).

Take $\Sigma_0={a,b}$, $\Sigma_2={f}$, (Q={p,q,r}), and (F={r}). Put

$$\delta(a)=p,\qquad \delta(b)=q,$$

and define every binary transition to be (p), except

$$\delta_f(p,r)=r.$$

Then (R={p,q}), so every ground tree and every genuine context applied to a reachable hole value evaluates inside (R) and is rejected. Thus $p\equiv_A q$ under genuine tree contexts. But the arbitrary-state polynomial

$$P(x)=\delta_f(x,r)$$

sends (p) to the final state (r) and (q) to the nonfinal state (p). It therefore distinguishes two reachable states using an unrealizable sibling parameter. Three states are minimal for this particular discrepancy because it requires two distinct reachable states and at least one unreachable parameter.

This is a representation/definition obstruction, not a limitation of tree automata. The exact repair is to trim to the reachable subalgebra or explicitly restrict polynomial parameters to reachable states.

Evidence and status audit

• Internal correctness: CRD-TA-1 and CRD-TA-2 have complete written proofs in the stated deterministic, complete, bottom-up model.
• Finite corroboration: tree_context_baseline_check.py verifies the sharpness family for $2\le n\le12$ and the three-state hostile witness.
• External dependency: None; the promoted claims do not depend on an external theorem, implementation, or paper.
• Representation obstruction: The hostile witness refutes only the use of arbitrary unreachable state parameters as substitutes for genuine tree contexts.
• Novelty: Not assessed. These are standard-style syntactic-algebra and minimization facts plus an elementary boundary witness; no novelty claim is made.

Run 1 handoff obligations — resolved by Run 2

1. The independent SAT choice baseline has now been completed.
2. The fixed variable order, explicit 3CNF family, semantic residuals, and reduced ordered-BDD states are specified below with exact size statements.
3. Do not infer that context families in other models must be generated by their reachable runtime states; the reachability repair is model-specific until independently reproduced.

Run 2 target

For one explicit 3CNF family and one fixed variable order, compare exactly:

1. raw prefix-assignment histories;
2. future-equivalence classes defined by residual Boolean functions; and
3. states in the reduced ordered binary decision diagram.

Then test whether the count of residual CNF formulas is an intrinsic substitute for the semantic residual count.

Native SAT definitions

For $m\ge1$, let

[ \Phi_m$x_1,\ldots,x_m,z,w$

\bigwedge_{i=1}^m $x_i\vee z\vee w$. ]

Every clause has exactly three distinct literals, and the fixed variable order is

$$x_1<\cdots<x_m<z<w.$$

For a prefix assignment $\alpha\in{0,1}^k$, $0\le k\le m$, define its semantic residual function by

[ \rho_\alpha$x_{k+1},\ldots,x_m,z,w$

\Phi_m$\alpha_1,\ldots,\alpha_k, x_{k+1},\ldots,x_m,z,w$. ]

Two length-(k) histories are future-equivalent when their residual Boolean functions are equal on every assignment to the remaining variables.

The raw history object is the full binary prefix-assignment tree. The canonical decision representation is the reduced ordered BDD (ROBDD) for the displayed variable order, with the usual two reductions: merge isomorphic nodes and delete a test whose low and high successors agree.

CRD-SAT-1: exact prefix-fold theorem

Statement

For every $m\ge1$ and every cut $1\le k\le m$:

1. there are exactly (2^k) raw length-(k) assignment histories;
2. those histories induce exactly two semantic residual functions;
3. one residual class contains the unique history (1^k), and the other contains the remaining (2^k-1) histories;
4. the ROBDD has exactly two states reachable after consuming a length-(k) (x)-prefix, with the same multiplicities.

The entire raw (x)-prefix history tree through depth (m) has (2^{m+1}-1) nodes. The full ROBDD has exactly (m+2) nonterminal nodes and (m+4) nodes including its two terminals. Across all (x)-prefix cuts, the set of reached ROBDD roots has exactly (m+2) members.

Residual proof

The formula has the Boolean identity

[ \Phi_m

z\vee w\vee\bigwedge_{i=1}^m x_i. ]

Indeed, if $z\vee w$ is true then every clause is true; if it is false, all clauses are true exactly when every (x_i) is true.

For a length-(k) prefix, define

[ A_k

z\vee w\vee\bigwedge_{i=k+1}^m x_i, \qquad B=z\vee w, ]

using the empty-conjunction convention (A_m=1). If $\alpha=1^k$, then $\rho_\alpha=A_k$. If any assigned (x_i) is zero, one clause reduces to $z\vee w$, which implies every remaining clause, so $\rho_\alpha=B$. Thus there are at most two residuals with the stated multiplicities.

They are distinct. For (k<m), set (z=w=0) and every unassigned (x_i=1): then (A_k=1) but (B=0). For (k=m), (A_m=1) while (B(0,0)=0). This proves Parts 1–3. $\square$

ROBDD proof and exact size

Construct nodes $X_1,\ldots,X_m,Z,W$. Node (X_i) tests (x_i), has low successor (Z), and high successor (X_{i+1}), where (X_{m+1}) denotes terminal (1). Node (Z) tests (z), with low successor (W) and high successor (1). Node (W) tests (w), with low successor (0) and high successor (1).

Induction from (X_m) upward shows that (X_i) computes

$$z\vee w\vee\bigwedge_{j=i}^m x_j,$$

so (X_1) computes $\Phi_m$. Every edge respects the fixed order. No node has identical low and high successors, and nodes with different tested variables cannot be merged. Hence the graph is reduced and has exactly (m+2) nonterminals, or (m+4) nodes with terminals.

After an (x)-prefix $\alpha$, the unique all-one history reaches (X_{k+1}) (or terminal (1) when (k=m)); every other history takes a low edge at its first zero and reaches (Z), skipping the remaining (x)-tests. This gives exactly two cut states and the same (1) versus (2^k-1) multiplicity profile as the semantic residuals.

The raw binary prefix tree has $\sum_{k=0}^m2^k=2^{m+1}-1$ nodes. The ROBDD roots reached over all these cuts are precisely

$${X_1,\ldots,X_m,Z,1},$$

which has (m+2) members. $\square$

CRD-SAT-F1: syntactic residual count is representation-dependent

At a fixed cut (k), direct substitution into the CNF yields different exact counts under three ordinary representation conventions:

1. Origin-labelled clause occurrences: each zero position leaves a provenance-distinct copy of $(z\vee w)$, so all (2^k) histories have distinct residual encodings.
2. Unlabelled duplicate-preserving multisets: only the number $t\in{0,\ldots,k}$ of zero assignments matters, giving (k+1) encodings.
3. Duplicate deletion: the residual records only whether at least one copy of $(z\vee w)$ exists, giving two encodings for $k\ge1$.

All non-all-one histories nevertheless denote the same Boolean function $B=z\vee w$. Therefore “the number of residual formulas” is not intrinsic until syntax, duplicate policy, provenance, and semantic quotient are fixed. The ROBDD theorem concerns semantic residual functions and a named canonical representation; it does not license switching among these syntactic counts.

Run 2 evidence and status audit

• Internal correctness: CRD-SAT-1 has a complete all-(m) proof in the stated monotone 3CNF family and fixed order.
• Finite corroboration: sat_residual_obdd_check.py exhaustively checks $1\le m\le10$, including truth-table residual equality, ROBDD reduction, node counts, cut multiplicities, and all three syntactic conventions.
• External dependency: None; neither theorem nor audit relies on an external paper or implementation.
• Representation obstruction: CRD-SAT-F1 refutes only an unspecified syntactic residual-count doctrine. It does not refute semantic residuals, ROBDD canonicity under a fixed order, or SAT algorithms.
• Refutation: The claim that “residual formula count” is representation invariant is false on this family.
• Novelty: Not assessed; the construction is an elementary calibration family and no novelty claim is made.

Run 2 handoff obligations — resolved by Run 3

1. The bounded comparison of tree-context equivalence and ordered SAT-prefix future-equivalence has now been completed below.
2. Assignment extension supplies a congruence law only in a graded/many-sorted prefix system. Erasing prefix grade is not sound.
3. Do not promote the exponential raw-history collapse into a SAT hardness, DPLL, CDCL, proof-size, or complexity lower bound; this family is easy, monotone, symmetric, and chosen for exact calibration.

Run 3 target

For an arbitrary Boolean function with a fixed variable order, determine whether future-equivalence of ordered prefix assignments is the largest terminal-observation-saturating congruence under next-bit assignment. Then hostilely test whether prefix length (equivalently, the identity of the next variable) can be erased from the runtime state or hidden inside a reduced OBDD node.

Native ordered-prefix definitions

Fix $f:{0,1}^n\to{0,1}$ and the order $x_1<\cdots<x_n$. For each $0\le k\le n$, let

[ H_k={0,1}^k. ]

These are distinct grades. For $b\in{0,1}$, the typed next-variable extension is

$$e_{k,b}:H_k\to H_{k+1},\qquad e_{k,b}(\alpha)=\alpha b.$$

Only (H_n) carries the terminal observation

$$\operatorname{Obs}(\alpha)=f(\alpha).$$

For same-grade prefixes define

$$\alpha\equiv_k\beta \iff \forall\gamma\in{0,1}^{n-k},\quad f(\alpha\gamma)=f(\beta\gamma).$$

A terminal-observation-saturating graded congruence is a family $\theta=(\theta_k)_{k=0}^n$, with each $\theta_k$ an equivalence relation on (H_k), such that

$$\alpha\mathrel{\theta_k}\beta \Longrightarrow \alpha b\mathrel{\theta_{k+1}}\beta b \quad(b=0,1),$$

and

$$\alpha\mathrel{\theta_n}\beta \Longrightarrow f(\alpha)=f(\beta).$$

CRD-SAT-2: greatest graded-congruence theorem

Statement

For every Boolean function (f) and fixed variable order:

1. $\equiv=(\equiv_k)_{k=0}^n$ is the largest, by relation inclusion, terminal-observation-saturating graded congruence on the ordered prefix system.

2. It is characterized backward by

   $$\alpha\equiv_n\beta\iff f(\alpha)=f(\beta),$$

   and, for (k<n),

   $$\alpha\equiv_k\beta \iff \bigl(\alpha0\equiv_{k+1}\beta0\bigr) \land \bigl(\alpha1\equiv_{k+1}\beta1\bigr).$$

3. The quotient transitions

   $$[\alpha]_{\equiv_k}\xrightarrow{b} [\alpha b]_{\equiv_{k+1}}$$

   are well-defined. Backward refinement by the ordered pair of child classes constructs the canonical layered residual quotient.

Proof

Suppose $\alpha\equiv_k\beta$. For either bit (b) and every $\gamma\in{0,1}^{n-k-1}$,

$$f(\alpha b\gamma)=f(\beta b\gamma),$$

because $b\gamma$ is a completion quantified over in the definition of $\equiv_k$. Hence extension compatibility holds. At grade (n), the only completion is the empty word, so $\equiv_n$ is exactly equality of terminal observation.

For maximality, let $\theta$ be any terminal-observation-saturating graded congruence and assume $\alpha\mathrel{\theta_k}\beta$. Repeated compatibility with the successive bits of an arbitrary completion $\gamma$ gives

$$\alpha\gamma\mathrel{\theta_n}\beta\gamma.$$

Terminal saturation then yields $f(\alpha\gamma)=f(\beta\gamma)$. Since this holds for every completion, $\alpha\equiv_k\beta$, and therefore $\theta_k\subseteq\equiv_k$ at every grade.

For the backward recursion, every nonempty completion is uniquely $0\gamma$ or $1\gamma$. Equality on all completions is therefore equivalent to equality after both one-bit extensions on every remaining suffix. This also makes quotient transitions well-defined and gives the stated backward partition-refinement construction. $\square$

CRD-SAT-F2: grade erasure destroys append compatibility

One might compare prefixes of different lengths by lifting every residual to the full (n)-cube:

$$\bar\rho_\alpha(v_1,\ldots,v_n) =f(\alpha_1,\ldots,\alpha_k,v_{k+1},\ldots,v_n),$$

ignoring the first (k) coordinates of the argument. This equality is not a congruence for an untyped append-bit operation.

For the two-variable function (f(x_1,x_2)=x_2),

$$\bar\rho_\epsilon= x_2=\bar\rho_0.$$

But appending (0) to both prefixes gives

$$\bar\rho_{\epsilon0}=x_2, \qquad \bar\rho_{00}=0.$$

The same bit label assigns (x_1) at grade (0) and (x_2) at grade (1). Thus prefix grade, a typed next-variable label, or an equivalent external schedule is essential.

CRD-SAT-F3: ROBDD node identity is not a uniform next-bit state

The Run 2 family gives a representation-level form of the same obstruction. For $m\ge2$, its ROBDD node (Z), computing $z\vee w$, is reached both after (x_1=0) at grade (1) and after a full (x)-prefix containing a zero at grade (m). At grade (1), the next bit assigns (x_2), which is skipped below (Z), so either bit leaves the root at (Z). At grade (m), the next bit assigns (z), so bit (0) moves to the (w)-node and bit (1) moves to terminal (1).

Consequently no grade-free update function

$$U(\text{ROBDD node},b)$$

can simulate ordered sequential assignments in both situations. A correct runtime state must include the grade/schedule, receive variable-labelled updates, or obtain the position from an explicit external clock. ROBDD node identity captures future Boolean behavior but not, by itself, which variable the next unlabelled bit assigns.

Run 3 evidence and status audit

• Internal correctness: CRD-SAT-2 has a complete self-contained proof for every Boolean function and fixed variable order.
• Finite corroboration: sat_graded_congruence_check.py exhaustively checks all 65,812 Boolean functions of arity one through four, including 5,576,020 recursive prefix-pair tests and 3,905,720 compatible-extension tests.
• External dependency: None.
• Representation obstruction: CRD-SAT-F3 applies to a node-only, unlabelled-bit update interface. It does not challenge ROBDD canonicity or ordinary variable-labelled ROBDD traversal.
• Refutation: CRD-SAT-F2 refutes cross-grade lifted-residual equality as an untyped append congruence.
• Novelty: Not assessed; no novelty claim is made.

Current obligations after Run 3

1. The tree and SAT cases now share a precise kernel/maximal-congruence pattern, but the tree case is single-sorted while the SAT prefix system is graded. Do not erase that difference or promote a universal abstraction yet.
2. Fix one deterministic one-pass streaming model and determine whether its suffix-continuation equivalence is single-sorted or length-graded, including the exact status and cost of any clock/position coordinate.
3. Do not infer a SAT lower bound, an OBDD update lower bound for richer interfaces, or a general theorem about all branching programs.

Run 4 target

Fix one deterministic one-pass streaming model and determine whether its suffix-continuation quotient is genuinely single-sorted or secretly graded by prefix length. Account explicitly for the state cost of any position/clock coordinate, and hostilely test the inference that constant quotient width at every individual cut implies a constant-size uniform stream processor.

Native uniform streaming model

A deterministic Moore stream processor is a tuple

$$M=(Q,q_0,\delta,\lambda),$$

where (Q) is a finite state set, $q_0\in Q$, $\delta:Q\times\Sigma\to Q$ is a stationary one-symbol update, and $\lambda:Q\to O$ is an output map. The current output is observable after every finite prefix. Extend $\delta$ to words in the usual way and put

$$q(u)=\delta^*(q_0,u), \qquad M(u)=\lambda(q(u)).$$

For reachable states define suffix-continuation equivalence by

$$p\equiv_M q \iff \forall w\in\Sigma^*,\quad \lambda(\delta^*(p,w))=\lambda(\delta^*(q,w)). \tag{STR.1}$$

Equivalently, histories $u,v\in\Sigma^*$ are equivalent when (M(uw)=M(vw)) for every common suffix (w). A transition congruence is an equivalence relation $\theta$ on reachable states satisfying

$$p\mathrel\theta q \Longrightarrow \delta(p,a)\mathrel\theta\delta(q,a) \quad(a\in\Sigma).$$

It saturates output when $p\mathrel\theta q$ implies $\lambda(p)=\lambda(q)$.

CRD-STR-1: uniform streaming quotient theorem

Statement

For every deterministic Moore stream processor:

1. $\equiv_M$ is the largest output-saturating transition congruence on the reachable states;

2. the history relation

   $$u\equiv v \iff \forall w\in\Sigma^*,\ M(uw)=M(vw)$$

   is a single-sorted right congruence on $\Sigma^*$; and

3. the reachable quotient by this relation is the unique minimal Moore stream processor up to isomorphism.

Proof

If $p\equiv_M q$, then taking $w=\epsilon$ gives $\lambda(p)=\lambda(q)$. For every input symbol (a) and suffix (w),

$$\lambda(\delta^*(\delta(p,a),w))=\lambda(\delta^*(p,aw))=\lambda(\delta^*(q,aw))=\lambda(\delta^*(\delta(q,a),w)).$$

so $\delta(p,a)\equiv_M\delta(q,a)$. Thus $\equiv_M$ is an output-saturating transition congruence.

Conversely, let $\theta$ be any such congruence and suppose $p\mathrel\theta q$. Repeated transition compatibility gives $\delta^*(p,w)\mathrel\theta\delta^*(q,w)$ for every (w). Output saturation then makes their outputs equal, so $p\equiv_M q$. Hence $\theta\subseteq\equiv_M$, proving maximality. The same calculation on histories proves right-congruence.

The quotient is a reachable Moore processor with one state per distinct suffix behavior. Every exact reachable implementation maps histories with the same reached implementation state to the same suffix behavior, so it has at least as many states. The quotient itself attains that number, proving minimality and uniqueness by the residual-state correspondence. $\square$

The quotient is single-sorted for a substantive reason: every letter has the same update meaning at every time, every suffix is legal after every state, and output can be demanded after every prefix. No external position schedule appears in the definition.

CRD-STR-2: exact cost of internalizing a positional clock

For $j\ge1$, define the binary streaming task

$$G_j(u)= \begin{cases} \bot, & |u|<j,\ u_j, & |u|\ge j, \end{cases} \tag{STR.2}$$

where positions are one-indexed and $\bot$ means that the requested bit has not yet arrived. Thus the processor reports $\bot$ before position (j) and thereafter retains and reports the bit observed at position (j).

Statement

For every $j\ge1$:

1. at each fixed prefix length, the future-equivalence quotient has width one before position (j) and width two from position (j) onward;

2. across all prefix lengths, (G_j) has exactly (j+2) single-sorted suffix residuals;

3. every exact stationary Moore stream processor for (G_j) needs at least (j+2) reachable states, and a (j+2)-state processor exists;

4. consequently the exact finite-state memory lower bound is

   $$\left\lceil\log_2(j+2)\right\rceil$$

   bits under ordinary state counting; and

5. for pre-clock residuals at lengths $0\le i<\ell<j$, the shortest distinguishing suffix has length exactly $j-\ell$. The maximum shortest distinguishing length is (j-1).

Proof

If (|u|=i<j), the value of every continuation depends only on (i), not on the symbols already seen: the (j)-th symbol has not arrived. Call this residual (P_i). If $|u|\ge j$, every continuation preserves the stored value (u_j), giving residuals (Z) and (O). Hence there are at most

$$P_0,P_1,\ldots,P_{j-1},Z,O,$$

or (j+2), global residuals. At one fixed grade there is only one (P_i), or the two stored-bit residuals, proving the width statement.

All global residuals are distinct. The empty suffix separates every (P_i) from (Z) and (O), and separates (Z) from (O), because their current outputs are $\bot,0,1$. For $i<\ell<j$, use

$$w=0^{j-\ell}.$$

Starting from $P_\ell$, this suffix reaches position (j) and produces output (0). Starting from (P_i), the total length is $i+j-\ell<j$, so the output remains $\bot$. No shorter suffix can distinguish them because both computations still have length below (j). This proves both exact residual count and exact distinguishing length.

The residual transition graph itself supplies the upper bound:

$$P_i\xrightarrow{0,1}P_{i+1}\quad(i<j-1),$$

$$P_{j-1}\xrightarrow{0}Z, \qquad P_{j-1}\xrightarrow{1}O,$$

with (Z) and (O) absorbing under both inputs. It has (j+2) states and computes (G_j). CRD-STR-1 says no exact implementation can have fewer than the number of residuals, proving the lower bound. The bit bound follows by encoding (j+2) distinguishable states. $\square$

Hostile audit: constant per-cut width does not give constant uniform state

The family (G_j) refutes the inference

$$\sup_k{\text{number of behavioral classes at cut }k}=O(1) \Longrightarrow \text{one }O(1)\text{-state stationary stream processor}.$$

Every cut has width at most two, but sewing those cuts into one stationary processor requires exactly (j+2) states. A layer-local representation can use one bit after the target and no data bit before it only because the grade is supplied externally. The single-sorted processor must internalize time-to-target, producing the chain $P_0\to\cdots\to P_{j-1}$.

This is an exact uniformization cost, not a claim that all clocks require linear states. It also depends on the fixed model boundary:

• output is observable after every prefix, including the $\bot$ value;
• input letters are unlabelled bits with stationary meaning;
• the position (j) is fixed in the machine, not supplied as a query;
• an external counter is charged rather than declared free.

If output is inspected only at one prescribed terminal horizon, histories of different lengths no longer share the same continuation domain and the problem becomes graded again. If timestamped symbols or a free position counter are supplied, the clock cost has been moved into the interface rather than eliminated.

Algebraic, geometric, and comparative content

The quotient carries the canonical right action of the free monoid ({0,1}^*). For (G_j), its directed geometry is a length-(j) clock chain that forks into two absorbing stored-value states. The suffix metric is intrinsic to the stream interface: the distance between two residuals is the least suffix length that separates their outputs. On pre-clock states $P_i,P_\ell$ with $i<\ell$, it is exactly $j-\ell$, and the maximum over all pairs is (j-1).

The comparison with the prior cases is now exact:

The SAT and streaming results are therefore not contradictory. In SAT, the same unlabelled bit denotes different variables at different grades. In the uniform stream model, every input symbol always denotes the same update. A positional dependency is consequently visible in the residual behavior and becomes ordinary state rather than an external type.

Run 4 evidence and status audit

• Internal correctness: CRD-STR-1 and CRD-STR-2 have complete self-contained proofs in the stated Moore streaming model.
• Finite corroboration: 'streaming_position_quotient_check.py' independently minimizes the explicit processors for $1\le j\le64$, checks all 47,904 unordered state pairs, and verifies the exact distinguishing-depth profile.
• External dependency: None.
• Representation obstruction: Constant layer width does not imply constant uniform stationary state when the layer/clock is not free.
• Refutation: The grade-width-to-uniform-state inference is false on (G_j).
• Novelty: Not assessed; no novelty claim is made. CRD-STR-1 is a standard Moore/Myhill--Nerode-style fact; the positional family is used as an exact comparative calibration.

Current obligations after Run 4

1. Do not transfer the (j+2) lower bound to terminal-only, timestamped, query-indexed, randomized, or non-finite-state streaming models.
2. The three completed cases now force a precise distinction between an intrinsic single-sorted continuation action and a graded system whose operation meanings vary with position. This is evidence for a comparative criterion, not yet a universal abstraction.
3. The next bounded primary case should be a finite terminating rewriting system: test whether disjoint-redex commuting squares account for endpoint- equal derivations, and isolate the smallest overlapping critical pair when they do not.

Run 5 target

In one finite terminating rewriting system, determine exactly how much derivation branching is removed by commuting independent redex contractions. Test whether disjoint-redex squares generate all identifications between complete derivations with the same source and normal-form endpoint. If not, isolate the first overlap obstruction and the additional local relation that repairs path connectedness.

Native finite string-rewriting model

Let the alphabet be ({a}) and take the one-rule semi-Thue system

$$R={aa\to a}. \tag{RW.1}$$

Every step strictly decreases word length, so (R) terminates. Every nonempty word (a^n) reduces to the unique normal form (a), so the system is confluent at the level of terms.

A rewrite step is occurrence-labelled: from (a^k), it records which adjacent positions (i,i+1), $1\le i<k$, are contracted. The semantic state remains the underlying word; occurrence and provenance information belongs to the derivation history.

Initially label the occurrences $1,\ldots,n$. During a history, each current (a) represents a contiguous interval of original occurrences. A contraction merges two adjacent intervals.

Let $\mathcal D_n$ be the complete occurrence-labelled derivations

$$a^n\Rightarrow a^{n-1}\Rightarrow\cdots\Rightarrow a.$$

Define $\sim_\square$ on $\mathcal D_n$ to be generated by swapping two consecutive contractions when, immediately before the first contraction, both redexes are simultaneously present and have disjoint provenance intervals. The two orders then form the usual commuting diamond, with residual positions adjusted after the first length decrease.

Explicitly, if the first contraction has position (p) in (a^m) and the second has position (q) in (a^{m-1}), the contractions are disjoint exactly when

$$q\le p-2 \qquad\text{or}\qquad q\ge p+1.$$

Their swaps are

$$(p,q)\longleftrightarrow(q,p-1) \quad(q\le p-2),$$

and

$$(p,q)\longleftrightarrow(q+1,p) \quad(q\ge p+1).$$

The cases (q=p-1) and (q=p) consume the block created by the first contraction and are overlapping rather than independent.

CRD-RW-1: exact three-level history classification

Statement

For every $n\ge1$:

1. the number of raw complete derivations is

   $$|\mathcal D_n|=(n-1)!;$$

2. mapping a contraction to an ordered binary node whose children are the two merged blocks induces a bijection

   $$\mathcal D_n/{\sim_\square} ;\cong; {\text{planar full binary trees with (n) ordered leaves}};$$

3. consequently,

   $$|\mathcal D_n/{\sim_\square}|=C_{n-1}=\frac1n\binom{2n-2}{n-1}.$$

4. disjoint squares fail to generate equality of complete-derivation endpoints first at (n=3); and

5. if the symmetric length-two overlap relation

   $$((AB)C);\longleftrightarrow;(A(BC)) \tag{RW.2}$$

   is closed under prehistory and posthistory composition and under word and derivation contexts, then it joins all (C_{n-1}) square classes of complete reductions. Thus the exact hierarchy of counts is

   $$(n-1)! \quad\longrightarrow\quad C_{n-1} \quad\longrightarrow\quad 1,$$

   for raw histories, disjoint-square classes, and complete-history classes after the contextual overlap relation, respectively.

Proof: raw histories

At word length (k), there are exactly (k-1) adjacent occurrences of (aa). Every complete derivation makes one choice at each length $k=n,n-1,\ldots,2$. Therefore

$$|\mathcal D_n|=\prod_{k=2}^n(k-1)=(n-1)!.$$

Equivalently, label the (n-1) original gaps between occurrences. Every contraction deletes exactly one surviving gap, and every order of deleting the gaps is legal. Thus complete histories are in bijection with (S_{n-1}).

Proof: merge trees and disjoint squares

Given a complete history, represent each original occurrence by a leaf. When two adjacent current blocks are contracted, add a parent whose ordered children are those blocks. The final result is a planar full binary tree (T) with leaves $1,\ldots,n$ in their original order.

Fix such a tree (T). Order its internal vertices by dependency: (u<v) when (u) is a proper descendant of (v). A history produces (T) exactly when its chronological contraction order is a linear extension of this poset. Indeed, both child blocks must be completed before their parent can be contracted. Conversely, in any linear extension, when an internal vertex is scheduled its two child intervals have already collapsed and remain adjacent, so the contraction is legal.

Any two linear extensions of a finite poset are connected by swaps of adjacent incomparable elements. For completeness, take the first element of a target extension, locate it in another extension, and bubble it leftward. Every crossed element must be incomparable with it; then continue inductively on the remaining poset.

In a planar binary tree, incomparable internal vertices have disjoint leaf intervals. Thus the adjacent incomparable swaps are exactly the legal disjoint-redex squares. Conversely, a disjoint swap changes only the schedule, not the parent-child merge tree. Therefore the fibres of the history-to-tree map are precisely the $\sim_\square$-classes.

Every planar full binary tree is executable by contracting its internal vertices bottom-up, so the map is onto. Such trees satisfy the recurrence

$$T_1=1, \qquad T_n=\sum_{i=1}^{n-1}T_iT_{n-i},$$

whose values are the Catalan numbers $T_n=C_{n-1}=\frac1n\binom{2n-2}{n-1}$. This proves Parts 2 and 3. $\square$

Proof: smallest overlap and contextual repair

For (n=1,2), there is only one complete derivation. At (n=3), the two histories are

$$((a_1a_2)a_3) \qquad\text{and}\qquad (a_1(a_2a_3)).$$

Their first redexes overlap at (a_2), so neither path contains a pair of consecutive disjoint contractions and no square move applies. Both underlying paths nevertheless end at the same normal form (a). Hence (n=3) is the smallest source length in this system at which disjoint-square completeness fails.

Relation (RW.2) is specifically the equality between the two length-two normalizing paths from (aaa) to (a), not an equality between their length-one prefixes from (aaa) to (aa). Its contextual closure acts on any three already-collapsed adjacent nonempty blocks (A,B,C) and changes

$$((AB)C)\longleftrightarrow(A(BC)).$$

This is exactly one local rotation of a planar binary tree. These rotations connect all such trees: whenever the root's left subtree is composite, rotate (((A,B),C)) to ((A,(B,C))), strictly decreasing the number of leaves in the root's left subtree. Once that subtree is a leaf, apply the same procedure recursively to the right subtree. Every tree is thereby connected to the right comb. Combining rotations between tree shapes with disjoint swaps between schedules proves Part 5.

The gap-permutation view gives the same conclusion. Two consecutive gap deletions are either disjoint, in which case their adjacent transposition is a square, or share one current block, in which case their transposition is an instance of (RW.2). Hence the augmented move graph on histories is the adjacent-transposition graph of (S_{n-1}), and is connected. $\square$

Hostile audit

Occurrence erasure

If a derivation is represented only as a sequence of underlying words, then every complete history projects to

$$a^n\to a^{n-1}\to\cdots\to a.$$

In particular, the two (a^3) histories become the same term sequence. That representation cannot express redex independence, overlap, the factorial raw count, or the Catalan quotient. Occurrence labels are therefore essential to this history theorem. Provenance must remain a history annotation rather than part of the semantic endpoint; otherwise different trees would cease to have equal endpoints by definition.

Exact boundary of the overlap relation

A direct one-step cell identifying the two parallel contractions $aaa\Rightarrow aa$ would be stronger than (RW.2) and would also identify partial histories. CRD-RW-1 instead uses the length-two normalizing-path cell, which generates tree rotations for complete reductions but does not identify the two one-step partial paths. The connectivity conclusion is therefore restricted to complete reductions $a^n\Rightarrow^*a$.

Connectivity also uses the symmetric relation generated by (RW.2). If only the rightward orientation $((AB)C)\to(A(BC))$ is allowed, every tree reaches the right comb but the directed graph is not strongly connected.

Confluence is weaker than history coherence

The self-overlap at (aaa) is trivial from the ordinary term-level confluence view: either first contraction produces the same word (aa). It is nontrivial only after derivation occurrences are retained. Thus CRD-RW-1 does not challenge standard confluence of (R); it separates endpoint confluence from generation of history equivalence by independent commutations.

Connectedness is not higher coherence

Adding the contextual overlap relation proves only that the space of complete histories is connected. It does not prove uniqueness of connections or contractibility. Already at (n=4), the five Catalan tree classes and their local rotations form a pentagon loop. A higher relation would be needed to fill that loop; no such relation is established here.

Algebraic, geometric, and comparative content

The result exposes a genuine combinatorial path geometry:

• rewrite steps are occurrence-labelled edges;
• independent consecutive steps support commuting square 2-cells;
• square-homotopy classes retain a planar binary merge tree;
• the overlapping normalizing-path relation induces local tree rotations;
• the augmented history graph is the adjacent-transposition graph of (S_{n-1});
• the first unaddressed higher relation is the (n=4) pentagon.

This adds a layer absent from the earlier behavioral quotients. In the tree, SAT, and streaming cases, the promoted quotient identified presentations with the same permitted future observations. Here all complete paths already share one normal-form observation, yet the independence calculus retains (C_{n-1}) history classes. Endpoint behavior, causal scheduling, and overlap shape are therefore distinct quotients.

Run 5 evidence and status audit

• Internal correctness: CRD-RW-1 has a complete self-contained proof in the occurrence-labelled unary string-rewriting model.
• Finite corroboration: rewriting_disjoint_square_check.py enumerates all 46,234 complete histories for $1\le n\le9$, verifies the factorial raw counts, Catalan square-component counts, exact merge-tree fibres, direct augmented-history connectivity, and connectivity of the tree-rotation graph.
• External dependency: None.
• Representation obstruction: Word-sequence-only paths erase redex occurrences and make the history distinction invisible.
• Refutation: Disjoint-redex commuting squares do not generate all endpoint-equal complete derivations; (a^3) is the first witness within this fixed system.
• Novelty: Not assessed; no novelty claim is made. Catalan bracketings, adjacent swaps of linear extensions, gap permutations, and binary-tree rotations are standard-style combinatorics used here as an exact calibration.

Current obligations after Run 5

1. Do not identify term confluence, square-connected scheduling, and overlap-relation connectedness; they are three different equivalence levels.
2. Do not call the contextual overlap relation coherent merely because it connects all complete histories.
3. The sharpest next bounded target is the (a^4) pentagon: determine exactly whether its loop survives all disjoint-square relations among 2-cell moves, and state the minimal higher relation needed to fill it.

Run 6 — The first higher coherence obstruction is exactly the (a^4) pentagon

Run time: 2026-08-22 17:15 MDT
Selected model: occurrence-labelled unary string rewriting
Single bounded target: determine whether the (a^4) rotation pentagon is already null under the relations admitted in Run 5, and if not, identify the minimal higher relation required to fill it.

Native dimensional convention

Continue with $R={aa\to a}$. Rewrite contractions are 1-cells. A disjoint-redex commuting square or a contextual length-two overlap comparison is a 2-cell between complete derivations. A relation between composites of such 2-cells is therefore a 3-cell.

For finite checking and path geometry, form a transformation graph whose vertices are complete derivations and whose edges are the symmetric generating 2-cell moves. A 3-cell is represented there by a two-dimensional face attached along a loop. This dimension shift is only a way to visualize transformations between derivations; it does not turn rewrite steps themselves into vertices.

Exact six-history graph

Label the three original gaps in (a_1a_2a_3a_4) by (1,2,3). A complete history is the order in which these gaps are deleted, hence a permutation in (S_3). Let $h_\sigma$ denote the history with deletion order $\sigma$. Swapping two consecutive deletions gives either a disjoint-square move or an overlap move. The complete transformation graph is

$$h_{123}-h_{132}-h_{312}-h_{321}-h_{231}-h_{213}-h_{123}. \tag{RW.3}$$

Exactly one edge is disjoint:

[ h_{132}-h_{312}. ]

It exchanges the independent formation of blocks ((12)) and ((34)). The other five edges are contextual instances of the (aaa) overlap relation. Thus the raw graph is exactly the Cayley graph of (S_3) under adjacent transpositions, namely the six-cycle (C_6).

Square quotient and the pentagon

The merge trees of the six histories are

$$\begin{array}{c|c} \text{history} & \text{merge tree}\\ \hline h_{123} & (((12)3)4)\\ h_{132},h_{312} & ((12)(34))\\ h_{321} & (1(2(34)))\\ h_{231} & (1((23)4))\\ h_{213} & ((1(23))4). \end{array}$$

Contracting the unique disjoint edge identifies the two schedules of the balanced tree and turns (RW.3) into the five-cycle

$$(((12)3)4) ;--;((12)(34)) ;--;(1(2(34))) ;--;(1((23)4)) ;--;((1(23))4) ;--;(((12)3)4). \tag{RW.4}$$

This is the rotation pentagon on the five planar binary trees with four ordered leaves.

For the coherence audit, let $K_n^{\mathrm{int}}$ be the derived interchange complex. Its vertices are complete histories modulo disjoint rewrite squares, and its undirected edges are contextual overlap rotations. Attach a square 2-cell only when two distinct coinitial rotations are residually independent: each has a residual after the other, both application orders are legal, and the composites reach the same fourth tree without a critical overlap of their active constructor occurrences. This includes a rotation nested inside an opaque metavariable block of another; it does not attach a face merely because two longer paths share endpoints. In this dimension-shifted complex, a square 2-cell represents a 3-dimensional interchange relation in the original rewrite hierarchy.

Theorem CRD-RW-2

For complete occurrence-labelled reductions of (a^4) in $R={aa\to a}$:

1. the graph generated by disjoint and overlap 2-cell moves is (C_6);

2. quotienting by disjoint-square scheduling gives (C_5);

3. $K_4^{\mathrm{int}}$ has no 2-cells, so the loop survives cancellation of inverse moves and all residually independent-move interchange relations;

4. before any new pentagon filler, the raw shifted graph and $K_4^{\mathrm{int}}$ have infinite-cyclic fundamental group and first integral homology:

   $$\pi_1(C_6)\cong H_1(C_6;\mathbb Z)\cong\mathbb Z, \qquad \pi_1(K_4^{\mathrm{int}}) =\pi_1(C_5) \cong H_1(C_5;\mathbb Z) \cong\mathbb Z;$$

5. one arity-four 3-cell equating the two directed rotation composites from ((((AB)C)D)) to (A(B(CD))) is necessary and sufficient to make this component simply connected;

6. (a^4) is the smallest source in this system with a higher loop.

Proof

There are (3!=6) histories. A transformation edge swaps two adjacent entries of the gap permutation. The adjacent-transposition Cayley graph of (S_3) is connected, every vertex has degree two, and has six edges, so it is (C_6). Direct residual-support inspection gives the edge classification above: only the swap between (132) and (312) forms the left and right pairs in the opposite order without causal overlap.

Run 5 proved that disjoint-square classes are merge-tree fibres. At arity four, four trees have one history and the balanced tree has the two histories (h_{132},h_{312}). Contracting that single graph edge produces a connected graph with five vertices and five edges, all of degree two, hence (C_5).

Backtracking contributes only the usual cancellation of an edge followed by its inverse and cannot contract the simple cycle. An interchange relation between two residually independent generating 2-cell moves would appear as a nondegenerate four-cycle: apply the two moves in either order and compare the common fourth vertex. Neither (C_6) nor its quotient (C_5) contains a four-cycle.

There is also a structural arity bound. A tree rotation changes two active binary-constructor occurrences; its three metavariable subtrees are opaque. Two independent rotations have disjoint active-constructor sets. If their sites are in disjoint subtrees, they require at least six leaves. If one lies inside an opaque metavariable of the other, it requires three leaves for the inner site plus two other nonempty outer blocks, hence at least five leaves. At four leaves there are only three internal constructors, so two two-node active sets cannot be disjoint. Therefore none of the already-admitted interchanges supplies a face whose boundary can reduce (RW.3).

A connected graph with (V) vertices and (E) edges has free fundamental group of rank (E-V+1). Both (C_6) and (C_5) have rank one. With the displayed 1-skeleton fixed and no new vertices or edges, zero new higher cells cannot kill this generator. Attaching one disk once around the primitive simple cycle has degree $\pm1$, makes the component a disk, and kills both $\pi_1$ and (H_1). Thus one cell is necessary and sufficient in this fixed presentation. This is minimality by number of new cells, not uniqueness under changes of generators or Tietze-style presentation changes.

For $n\le3$, the augmented history graphs are respectively a point, a point, and one edge. They contain no loop. Thus arity four is minimal. $\square$

The higher relation in raw and quotient form

Write

$$\alpha_{A,B,C}:((AB)C)\Longrightarrow(A(BC))$$

for the overlap 2-cell, with contextual whiskering understood, and write $\chi$ for the disjoint square exchanging the order of forming (AB) and (CD). In the raw occurrence-history presentation, the required 3-cell has hexagonal boundary and equates two three-move composites:

$$\alpha_{AB,C,D}\ ;\ \chi_{AB,CD}\ ;\ \alpha_{A,B,CD} \quad=\quad (\alpha_{A,B,C},D)\ ;\ \alpha_{A,BC,D}\ ; (A,\alpha_{B,C,D}). \tag{RW.5}$$

After quotienting the independent scheduling edge $\chi$, (RW.5) becomes the pentagon equation

$$\alpha_{AB,C,D}\ ;\ \alpha_{A,B,CD} \quad=\quad (\alpha_{A,B,C},D)\ ;\ \alpha_{A,BC,D}\ ; (A,\alpha_{B,C,D}). \tag{RW.6}$$

Thus the raw hexagon and quotient pentagon are two presentations of the same first higher obstruction. The disjoint square is not itself the pentagon filler; it is one boundary edge that disappears in the schedule quotient.

Hostile audit

1. Connectivity is not coherence. Run 5's overlap cells make the history graph connected, but Run 6 computes $\pi_1\cong\mathbb Z$. Existence of a transformation between histories does not imply uniqueness up to the existing relations.
2. Raw and quotient boundaries differ. Calling the raw loop a pentagon silently treats one disjoint scheduling move as equality. Before that quotient the correct boundary is a hexagon.
3. Disjoint leaf support is not the general interchange criterion. With five leaves, rotate the inner (((AB)C)) inside ((((AB)C)D)E)), and independently rotate the outer (((X D)E)) while treating (X) as opaque. Both orders yield ((A(BC))(DE)), although the leaf supports are nested rather than disjoint. Independence must be expressed by residual commutation or disjoint active-constructor occurrences. This does not revive an arity-four square: (C_5) has no four-cycle.
4. A one-way orientation does not supply the filler. Both directed paths in (RW.6) point from the left comb to the right comb, but merely having two normalizing paths does not identify them, and the pentagon is not a directed cycle. Their equality is new data.
5. Homology is sufficient here only because the underlying space is a graph with one cycle. In more complicated dimensions, killing (H_1) need not prove simple connectedness.
6. No general coherence theorem is claimed. Contextual instances of one pentagon may or may not suffice for all (a^n); that is a separate target.

Structure exposed

This run establishes a genuine low-dimensional combinatorial structure:

$$\text{raw histories }C_6 \xrightarrow{\text{contract independent schedule}} \text{four-factor associahedral 1-skeleton }C_5 \xrightarrow{\text{attach one higher cell}} D^2.$$

The algebraic content is associativity at the level of transformations; the geometric content is the pentagonal 1-skeleton associated with four-factor associativity. The face is not assumed as part of that identification: its absence is the obstruction, and attaching it is the new higher relation. The result is model-native because every vertex and edge was derived from occurrence-labelled contractions and residual moves before the associahedral comparison was made.

Run 6 evidence and status audit

• Internal correctness: CRD-RW-2 has a complete finite classification and graph-theoretic proof in the stated (a^4) component.
• Finite corroboration: rewriting_pentagon_coherence_check.py verifies the (C_6) raw graph, unique disjoint edge, (C_5) quotient, Betti number one, disappearance of (H_1) after one face, and absence of smaller loops. As a hostile definition check, it also finds three commuting rotation squares at five leaves while a disjoint-leaf-support test finds none.
• External dependency: None.
• Representation obstruction: The tree quotient hides the disjoint edge; the raw boundary is hexagonal even though its schedule quotient is pentagonal. Leaf-support disjointness also undercounts nested interchange.
• Refutation: Connectedness under overlap rotations does not imply history coherence; disjoint leaf support does not characterize all independent rotations.
• Novelty: Not assessed; no novelty claim. The pentagon and associahedron are standard-style structures; the contribution here is their exact role in the fixed CRD calibration.

Current obligations after Run 6

1. Do not promote the arity-four filler to a global coherence theorem.
2. Distinguish raw occurrence-history coherence from coherence after the disjoint-scheduling quotient.
3. At (a^5), use residual commutation or active-constructor support rather than leaf-support disjointness; the latter already misses three squares.
4. The sharpest next bounded target is (a^5): enumerate the 14 tree vertices, square and pentagon faces, prove that inventory complete, and test whether those faces make the rotation complex simply connected without importing a general associahedron theorem.

Run 7 — The five-leaf square–pentagon complex is a 2-sphere

Run time: 2026-08-22 17:57 MDT
Selected model: occurrence-labelled unary string rewriting after the disjoint-scheduling quotient
Single bounded target: enumerate the native residual-interchange squares and contextual pentagons on five-leaf merge trees, prove that this face inventory is complete, and determine simple connectedness directly.

Native complex

Let (K_5) have one vertex for each planar full binary merge tree on ordered leaves (1,2,3,4,5), one edge for each contextual overlap rotation $((AB)C)\leftrightarrow(A(BC))$, one square face for each pair of residually commuting rotations, and one pentagon face for each contextual instance of the primitive arity-four coherence cell proved in Run 6. The vertices already represent complete reductions modulo disjoint scheduling; (K_5) is not the raw 24-history graph.

For a tree (T), a proper cluster is the leaf interval ([i,j]), $2\le j-i+1\le4$, occurring as the leaf set of a non-root internal subtree. There are nine possible proper intervals:

$$\begin{aligned} &[1,2],[2,3],[3,4],[4,5],\ &[1,3],[2,4],[3,5],\ &[1,4],[2,5]. \end{aligned}$$

For each interval (I), let (F_I) be the subgraph of rotations preserving that cluster.

Exact face inventory

If (|I|=r), a tree containing (I) decomposes uniquely into a binary tree on the (r) leaves inside (I), and a binary outer tree on the (6-r) blocks obtained by collapsing (I) to one opaque leaf. Hence

$$|V(F_I)|=C_{r-1}C_{5-r}=\begin{cases}5,&r=2,\\4,&r=3,\\5,&r=4.\end{cases}$$

For (r=2), the inner factor is fixed and the outer four-block trees rotate around the Run 6 pentagon. For (r=4), the outer factor is fixed and the inner four-leaf trees rotate around a pentagon. These give six pentagons:

[ F_{[1,2]},F_{[2,3]},F_{[3,4]},F_{[4,5]},F_{[1,4]},F_{[2,5]}. ]

For (r=3), both factors have two bracketings. The inner rotation and outer rotation commute because the inner triple is treated as an opaque metavariable by the outer move. Their product is a square. These give exactly

[ F_{[1,3]},F_{[2,4]},F_{[3,5]}. ]

This inventory is complete. A contextual arity-four pentagon on five leaves either has one two-leaf metavariable and acts on all five leaves, giving a unique size-two interval, or lies inside a four-leaf context with one leaf outside, giving a unique size-four interval. Two residually independent rotations use disjoint pairs of active binary-constructor occurrences. Five leaves have four binary constructors, so the pairs exhaust them and leave a unique three-leaf subtree treated internally by one move and opaquely by the other. Thus every native interchange is one of the three size-three faces.

Theorem CRD-RW-3

The five-leaf complex (K_5) has

[ (V,E,F)=(14,21,9), ]

with six pentagons and three squares. Every rotation edge lies in exactly two faces, and

$$\chi(K_5)=14-21+9=2.$$

Moreover, (K_5) is simply connected and, more strongly,

$$K_5\simeq S^2.$$

Its cellular homology is

$$H_0(K_5;\mathbb Z)\cong\mathbb Z, \qquad H_1(K_5;\mathbb Z)=0, \qquad H_2(K_5;\mathbb Z)\cong\mathbb Z.$$

Edge incidence

A five-leaf binary tree has three proper internal clusters. One rotation changes exactly one cluster and preserves the other two. Consequently its two endpoint trees share exactly two proper intervals. The corresponding edge lies in precisely the two faces indexed by those intervals.

Direct collapse proof

Remove the interior of pentagon (F_{[1,2]}). In the remaining complex, perform elementary face–free-edge collapses in this order:

$$F_{[1,3]},F_{[1,4]},F_{[2,3]},F_{[2,4]},F_{[2,5]}, F_{[3,4]},F_{[3,5]},F_{[4,5]}. \tag{RW.7}$$

At each stage the named face contains an edge incident to no other remaining face. An explicit certificate is:

After these eight collapses, 14 vertices and 13 edges remain, and the remaining graph is connected. It is therefore a tree and collapses to a point. Hence

$$K_5\setminus\operatorname{int}F_{[1,2]}$$

is collapsible. Restoring the omitted pentagonal 2-cell attaches one disk along a loop in a contractible CW complex. The result is homotopy equivalent to (S^2), proving simple connectedness.

Cellular corroboration

With arbitrary consistent orientations, the cellular boundary matrices have

$$\operatorname{rank}\partial_1=13, \qquad \operatorname{rank}\partial_2=8.$$

Therefore

$$\operatorname{rank}H_1=21-13-8=0, \qquad \operatorname{rank}H_2=9-8=1.$$

These ranks corroborate the collapse proof but do not replace it.

Hostile audit

1. (H_1=0) does not by itself prove $\pi_1=0$. Cellular boundary ranks see only the abelianization of the fundamental group. The explicit collapse certificate is the simple-connectedness proof.
2. Leaf-disjointness remains false as an interchange criterion. The three square faces are nested-context commutations: the inner triple lies inside the leaf support of the outer rotation but is opaque to its pattern. Active constructor occurrences are the correct support.
3. The 14 vertices are schedule quotients. The raw complete-history count is (4!=24), not 14. No raw-complex conclusion is promoted.
4. Every short graph cycle is not automatically a semantic face. Faces were derived from residual interchange and contextual arity-four coherence, then enumerated by clusters.
5. This remains a fixed finite theorem. It does not prove all-arity coherence or that analogous (K_n) are associahedral spheres.

Algebraic and geometric content

Run 6 found one unfilled associativity loop. Run 7 shows how two kinds of higher relation interact one arity later: contextual pentagons express compatibility among overlapping associativity transformations, while squares express interchange of residually independent transformations. Together they close the entire five-leaf transformation surface.

The nine faces are forced by retained contiguous clusters, not added after recognizing a familiar polytope. Only after this native derivation may (K_5) be identified with the two-dimensional boundary of the three-dimensional associahedron.

Run 7 evidence and status audit

• Internal correctness: complete finite combinatorial proof and explicit collapse certificate for the stated (K_5).
• Finite corroboration: rewriting_a5_cell_complex_check.py verifies all 14 vertices, 21 edges, six pentagons, three squares, two-face edge incidence, boundary ranks, and every step of (RW.7).
• External dependency: none.
• Representation obstruction: the tree-level complex does not retain the 24 raw schedules; no raw-complex conclusion is promoted.
• Refutation / failed route: inference of simple connectedness from (H_1=0) was rejected as insufficient and replaced by collapse.
• Novelty: not assessed; no claim. The associahedral structure is standard; its role here is an exact native calibration.

Current obligations after Run 7

1. Do not infer an all-arity coherence theorem from (n=4,5).
2. Keep the raw occurrence-history complex separate from its disjoint-schedule quotient.
3. The sharpest next bounded target is to leave this rewriting family and test whether an independently defined primary model—preferably tree automata under two disjoint local subtree updates—naturally produces commuting squares, or whether the apparent cubical analogy fails.

Run 8 — Dynamic tree-automaton target

Fix a deterministic bottom-up tree automaton whose implementation retains the canonical state of every node. An update (U=(u,s)) replaces the subtree at address (u) by a fixed, pre-evaluated tree (s), then writes or recomputes the cache at (u) and every ancestor through the root. One node operation costs one unit, and this eager algorithm does not stop early.

Write (A(u)) for the inclusive ancestor path and (d(u)) for depth, so (|A(u)|=d(u)+1).

CRD-TA-3: disjoint-update square and exact LCA geometry

Let (U=(u,s)) and (V=(v,r)), where (u,v) are incomparable addresses. Then [ V(U(t))=U(V(t)). ] After eager recomputation, the complete node caches are equal, so every root and enclosing-context observation agrees. Either sequential order costs $$S_{\rm seq}=|A(u)|+|A(v)|=d(u)+d(v)+2.$$ Installing both replacements and recomputing the affected union once in bottom-up order costs $$S_{\rm batch}=|A(u)\cup A(v)| =d(u)+d(v)-d(\operatorname{lca}(u,v))+1.$$ The exact saved work is $$S_{\rm seq}-S_{\rm batch} =|A(u)\cap A(v)| =d(\operatorname{lca}(u,v))+1.$$ Equivalently, using tree distance, $$|A(u)\cap A(v)| =\frac{d(u)+d(v)-d_T(u,v)}2+1.$$

Proof

Incomparable addresses denote disjoint subtrees. Replacing at (u) neither changes the address nor the content at (v), and conversely. Both composites therefore produce the same labelled tree with (s) at (u) and (r) at (v). Deterministic bottom-up evaluation gives that tree one unique canonical cache, proving endpoint and contextual equality. The two traces remain different histories.

Sequential eager maintenance touches (A(u)) and then (A(v)), counting the common ancestors twice. In the batch, every node outside the union retains its correct cache, while processing the union in decreasing depth order makes each child state available before its parent. Each union node is touched once. Finally, $$A(u)\cap A(v)=A(\operatorname{lca}(u,v)),$$ and inclusion--exclusion proves the formulas. $\square$

For equal-depth leaves (h) with least-common-ancestor depth $\ell$, $$S_{\rm seq}=2h+2, \qquad S_{\rm batch}=2h-\ell+1.$$ For siblings, the batching factor is $$\frac{2h+2}{h+2}\longrightarrow2.$$ This is genuine dependency-cone geometry: the LCA controls exactly how much upward recomputation can be shared.

Hostile audit

• Disjoint write targets do not suffice for state-dependent payloads. From cached bits ((L,R)=(0,0)), let (U) write (L:=R) and (V) write $R:=\neg L$. Then (U;V=(0,1)) but (V;U=(1,1)).
• Fixed replacements at overlapping positions need not commute. Let (U) replace the whole root by ((1,1)), while (V) replaces its left leaf by zero. Then (U;V=(0,1)), while (V;U=(1,1)).
• Early stopping can change the work because an unchanged state need not propagate upward. The displayed costs are exact for the named full-path algorithm, not representation-independent lower bounds.

tree_automaton_disjoint_update_check.py exhaustively verifies 6,144 complete Boolean cache squares, 43,435 structural ancestor-pair identities through depth eight, and both counterexamples. This corroborates but does not replace the proof. External dependency: none. Novelty: not assessed; no claim.

Current obligations after Run 8

1. Do not promote write-target disjointness to a general independence notion; account for read footprints or fix payloads in advance.
2. Keep endpoint commutation distinct from trace equality and higher coherence.
3. The sharpest next bounded target is to find the smallest exact order asymmetry for two behaviorally commuting fixed leaf updates under early-stopping cache recomputation, or prove invariance under a precise sufficient condition.

Run 9 — Early-stopping work is path-dependent on a semantic square

Native early-stopping model

Retain the deterministic bottom-up state at every tree node. A fixed leaf replacement first writes the pre-evaluated new leaf state, costing one unit. Then recompute ancestors upward, charging one unit for every transition evaluation. Stop immediately after the first recomputed node whose new state equals its old cached state. The unchanged-node evaluation is charged because it is what certifies that no higher cache can change.

For $h\ge1$, use states (Q={0,1}), nullary symbols (z,o) with states 0 and 1, a binary symbol (m) with

$$\delta_m(x,y)=\neg x\land y, \qquad (\delta_m(0,0),\delta_m(0,1),\delta_m(1,0),\delta_m(1,1)) =(0,1,0,0),$$

(h-1) unary identity carriers (c), and one unary constant-zero root (r). The initial tree is

[ t_h=r(c^{h-1}(m(z,z))). ]

Thus the binary parent has exactly (h) strict ancestors. Let (U) replace the left (z) by (o), and let (V) replace the right (z) by (o). Their addresses are sibling leaves and their payloads are fixed.

CRD-TA-4: sharp order-asymmetry theorem

The two replacements commute as labelled-tree substitutions, produce the same complete final cache, and have the same root-observation trace ((0,0)) in both orders. Nevertheless their early-stopping work is

$$W(U;V)=4, \qquad W(V;U)=2h+4.$$

Consequently

$$W(V;U)-W(U;V)=2h, \qquad \frac{W(V;U)}{W(U;V)}=1+\frac h2.$$

The additive gap (2h) is the largest possible for two fixed sibling-leaf replacements whose parent has (h) strict ancestors. The ratio is therefore unbounded as the tree height grows. Two states and (h=1), hence tree depth two, are minimal for any such asymmetry in this model.

Proof

Initially the parent has state (m(0,0)=0). In order (U;V), the first update changes the left input and gives (m(1,0)=0). The parent is unchanged, so the update stops after the leaf write and parent evaluation, at cost two. The second update gives (m(1,1)=0), again unchanged at the parent and again cost two. Hence (W(U;V)=4).

In order (V;U), the first update gives (m(0,1)=1). The parent changes; the change propagates through all (h-1) identity carriers. The constant root must then be evaluated, but remains zero and stops propagation. The charged work is one leaf write, one parent evaluation, and (h) evaluations above the parent:

[ 1+1+h=h+2. ]

The second update changes the parent from (m(0,1)=1) to (m(1,1)=0). The reverse change again passes through every identity carrier and stops only after the constant root is evaluated unchanged. Its cost is also (h+2), so (W(V;U)=2h+4). In both orders the root remains zero after each update. Since the final leaf pair is ((1,1)), deterministic evaluation gives the same complete final cache.

For sharpness, every update necessarily charges its leaf and the common parent, contributing four order-independent units across the two updates. Only the (h) strict ancestors can contribute differently between orders, and each can be evaluated at most once per update. Thus

$$|W(U;V)-W(V;U)|\le 2h.$$

The family attains equality. If (h=0), the parent is the root and every update costs exactly leaf plus parent, so no order asymmetry is possible. With one state, every recomputed state is unchanged, so propagation always stops at the parent; two states are necessary. The (h=1), two-state instance realizes the gap, proving these two minimality statements. $\square$

Hostile audit

1. Semantic commutation is not resource symmetry. The square commutes at the labelled-tree endpoint and at the complete-cache endpoint; even the two root-observation traces agree. Its two directed paths nevertheless have different weights.
2. The bound is algorithm-relative. It counts transition evaluations, including the first unchanged node. Charging only changed cache writes, or using different summaries or batching, changes the resource measure.
3. No intrinsic dynamic lower bound follows. This is a worst-case exact separation inside the named representation and update algorithm, not a lower bound for all dynamic tree-language recognizers.
4. Minimality is limited. Two states and depth two are minimal in the fixed sibling-leaf early-stopping model. No minimality claim is made for alphabet size, transition-description size, or broader update models.
5. Endpoint and root observations are deliberately coarse. Internal cache traces differ. The result does not say the histories are identical under every enriched observer.

Structure exposed

The two substitutions form a genuine commuting square in the state space of labelled trees and canonical caches. Early-stopping work equips its edges with history-dependent weights. The unequal path sums show that this valuation is not a potential difference and does not descend to semantic endpoints. The mechanism is a sensitivity cone: the intermediate parent state (1) activates the entire ancestor chain, while the other path stays on parent state (0) and terminates locally.

This differs from Run 8's full-path LCA geometry. There, the charged support is fixed by addresses, so either sequential order has the same cost. Here, the active support depends on the intermediate automaton state, and a semantic square becomes a non-flat weighted square.

Run 9 evidence and status audit

• Proof: complete for the all-(h) family, the sharp (2h) upper bound, and the state/depth minimality statements in the fixed model.
• Finite corroboration: tree_automaton_early_stop_order_check.py checks the family through (h=128) and exhaustively checks all 16 Boolean binary transitions and four Boolean starting corners for $0\le h\le8$, 576 cases in total. It finds maximum gap (2h) at every checked height.
• External dependency: none.
• Representation obstruction: the work count is tied to the specified cache and early-stopping accounting.
• Refutation: endpoint commutation, and even equal root-observation traces, do not imply order-invariant update work.
• Novelty: not assessed; no claim.

Current obligations after Run 9

1. Do not treat a semantically commuting square as resource-flat without auditing its edge weights.
2. Keep recomputation attempts distinct from changed writes and from optimal dynamic complexity.
3. The sharpest next bounded target is to derive a necessary-and-sufficient criterion for order-invariant early-stopping work along a fixed unary ancestor chain, stated using the four parent-corner states and their propagated-change prefix lengths.

Run 10 — Exact ultrametric flatness criterion for early stopping

Native setup

Fix two pre-evaluated child-state replacements at distinct child positions of one parent. Let the four possible parent states be

$$a=q_{00},\qquad b=q_{10},\qquad c=q_{01},\qquad d=q_{11},$$

where the first bit records whether update (U) has occurred and the second whether update (V) has occurred. The semantic update square is

$$\begin{array}{ccc} a & \xrightarrow{U} & b\\ \big\downarrow V && \big\downarrow V\\ c & \xrightarrow{U} & d. \end{array}$$

There are $h\ge1$ strict ancestors above this parent. At the (i)-th ancestor, every sibling argument outside the changing child path is fixed, so the ranked transition induces a unary map $g_i:Q\to Q$. Thus this setup allows ancestors of arbitrary rank; “unary chain” describes their induced action on the one changing path, not a restriction to unary tree symbols.

Put

$$\Phi_0=\operatorname{id}_Q, \qquad \Phi_i=g_i\circ\cdots\circ g_1\quad(1\le i\le h),$$

and define nested kernel equivalences

$$x,E_i,y \iff \Phi_i(x)=\Phi_i(y).$$

Determinism gives

$$E_0\subseteq E_1\subseteq\cdots\subseteq E_h:$$

once two propagated states agree, no higher deterministic ancestor can split them again.

For $0\le i<h$, let

$$d_i(x,y)= \begin{cases} 0,&x,E_i,y,\ 1,&\text{otherwise}, \end{cases}$$

and define the propagation length

$$\lambda(x,y)=\sum_{i=0}^{h-1}d_i(x,y). \tag{TA.10}$$

This is exactly the number of strict ancestors evaluated after the parent changes from state (x) to state (y). The term (d_i(x,y)) charges ancestor (i+1) precisely when the two propagated states are still unequal just below it. If equality first appears at that ancestor, its evaluation is included and then propagation stops.

CRD-TA-5a: exact path-cost and ultrametric theorem

The propagation length $\lambda$ is an ultrametric on (Q), truncated at height (h):

$$\lambda(x,z)\le \max{\lambda(x,y),\lambda(y,z)}. \tag{TA.11}$$

Under the Run 9 accounting—one unit for the child-state write, one for the parent evaluation, and one for each attempted strict-ancestor evaluation—the two order costs are exactly

$$W(U;V)=4+\lambda(a,b)+\lambda(b,d), \tag{TA.12}$$

$$W(V;U)=4+\lambda(a,c)+\lambda(c,d). \tag{TA.13}$$

Proof

Because the equivalences (E_i) are nested, $\lambda(x,y)$ is the first level at which (x,y) coalesce, capped at (h). If

$$r=\max{\lambda(x,y),\lambda(y,z)}<h,$$

then (xE_r y) and (yE_r z). Transitivity gives (xE_r z), so $\lambda(x,z)\le r$. If (r=h), (TA.11) is automatic.

For the boundary case (h=0), $\lambda$ is the identically zero pseudometric and both orders pay only the four local operations.

For one child replacement changing the parent from (x) to (y), the child write and parent transition cost two. Ancestor (i+1) is evaluated exactly when $\Phi_i(x)\ne\Phi_i(y)$, so the remaining cost is (TA.10). Applying this to the parent-state paths $a\to b\to d$ and $a\to c\to d$ proves (TA.12)–(TA.13). $\square$

CRD-TA-5b: no-cancellation and exact resource-flatness criterion

For each level define its signed order bias

$$\delta_i= d_i(a,c)+d_i(c,d)-d_i(a,b)-d_i(b,d). \tag{TA.14}$$

Then all nonzero $\delta_i$ have the same sign. Consequently

$$|W(V;U)-W(U;V)| =\sum_{i=0}^{h-1}|\delta_i| \le 2h. \tag{TA.15}$$

In particular, the square is resource-flat if and only if it is balanced at every counted ancestor level:

$$W(U;V)=W(V;U) \iff \forall i<h, \quad d_i(a,b)+d_i(b,d) =d_i(a,c)+d_i(c,d). \tag{TA.16}$$

Equivalently, writing $a_i=\Phi_i(a)$, and similarly for the other corners, the criterion is

$$b_i\in{a_i,d_i} \iff c_i\in{a_i,d_i} \qquad(0\le i<h). \tag{TA.17}$$

Thus total equality cannot be produced by a positive order bias at one level and a negative bias at another.

Proof

For one equivalence relation (E), use its quotient's discrete metric (d_E) and put

[ L_E(x)=d_E(a,x)+d_E(x,d). ]

If (aEd), then (L_E(x)=0) when (xEa), and (L_E(x)=2) otherwise. If $a\not E d$, then (L_E(x)=1) when the class of (x) is one of the two endpoint classes, and (L_E(x)=2) otherwise. Hence

$$L_E(b)=L_E(c) \iff \Bigl( [b]_E\in{[a]_E,[d]_E} \Longleftrightarrow [c]_E\in{[a]_E,[d]_E} \Bigr),$$

This proves the equivalence of (TA.16) and (TA.17) at one level.

It remains to exclude cancellation. Suppose (L_E(c)-L_E(b)>0). If the endpoint classes are distinct, (b) lies in one of them while (c) lies in neither. Under any coarser equivalence (F), the class of (b) remains an endpoint class. If the endpoints remain distinct, then $L_F(b)=1\le L_F(c)$; if they merge, then $L_F(b)=0\le L_F(c)$. If the endpoints were already equal under (E), then (b) lies in their common class and the same conclusion follows. Therefore a positive bias can become zero under coarsening but never negative. The negative case is symmetric.

Since $E_0\subseteq\cdots\subseteq E_{h-1}$, all nonzero $\delta_i$ have one sign. Equations (TA.12)–(TA.14) now give (TA.15), and their sum vanishes exactly when every summand vanishes, proving (TA.16). Each $\delta_i$ has absolute value at most two, giving the bound (2h). $\square$

Sharpness and examples

Run 9 is the extremal case. Its corners are

[ (a,b,c,d)=(0,0,1,0), ]

and the first (h) levels keep (0) and (1) separate. At every level, the route through (b) has discrete length zero and the route through (c) has length two. Thus $|\delta_i|=2$ for all (i<h), and (TA.15) gives the sharp gap (2h).

Resource-flatness is only equality of total work. For example, if

[ (a,b,c,d)=(0,0,1,1) ]

and the chain keeps (0,1) separate for (h) levels, then one order pays its full propagation on the second update and the other pays it on the first:

[ (0+h)=(h+0). ]

The total costs agree although the per-update timing and intermediate caches do not.

Hostile audit

1. The metric is representation-relative. $\lambda$ measures attempted recomputations in the fixed complete-cache early-stopping algorithm. It is not contextual distance, tree-edit distance, or an optimal dynamic lower bound.
2. Nestedness is the decisive hypothesis. It follows from deterministic composition of current child state through fixed ancestor contexts. A history-dependent ancestor update, mutable sibling payload, or nondeterministic cache policy need not generate nested kernel equivalences; the no-cancellation proof would then fail.
3. Flat total work is not trace equality. Equation (TA.16) does not make the two per-update costs, intermediate caches, or observation traces equal.
4. The corner square must be fixed. State-dependent replacement payloads and overlapping update positions remain outside the theorem.
5. The height truncation is real. States that do not coalesce before the root all have propagation length (h); the algorithm has no higher cache levels with which to distinguish them.
6. No cross-level cancellation counterexample exists in this model. A deliberate search for one failed for the structural reason proved above; this is not extrapolated to arbitrary weighted transition systems.

Structure exposed

The kernels of the prefix maps $\Phi_i$ form a chain in the lattice of equivalence relations. That laminar order induces a coalescence ultrametric on parent states. Early-stopping work is path length in this ultrametric, plus a fixed local cost. The order gap around a semantic square has an exact multiscale decomposition (TA.15), and nestedness makes its orientation sign-coherent across scales.

This is stronger than Run 9's extremal counterexample and more specific than Run 8's LCA geometry. Run 8's support was fixed spatially by addresses. Run 10 shows that state-sensitive support along one dependency path is governed by a hierarchy of kernel partitions. The two geometries coexist but are not the same: LCA measures overlap of possible dependency cones, while $\lambda$ measures how far a particular state change survives inside one cone.

Run 10 evidence and status audit

• Proof: complete for the exact path-cost formula, ultrametric property, sign-coherence lemma, sharp (2h) decomposition, and necessary-and-sufficient flatness criterion in the fixed deterministic ancestor-chain model.
• Finite corroboration: tree_automaton_unary_chain_flatness_check.py exhaustively checks all 5,384 multichains of partitions of four labelled corners through height eight. It verifies the strong triangle inequality, sign coherence, both flatness equivalences, and maximum gap (2h).
• External dependency: none.
• Representation obstruction: $\lambda$ depends on the retained cache, fixed ancestor contexts, early-stopping rule, and transition-attempt cost.
• Refutation / failed route: opposite-signed per-level biases cannot cancel in a deterministic unary ancestor chain.
• Novelty: not assessed; no claim. Nested-partition ultrametrics are standard-style structure; their exact role here is internally derived.

Current obligations after Run 10

1. Do not promote $\lambda$ to an intrinsic language or dynamic-complexity metric.
2. Keep total resource-flatness separate from trace and latency equality.
3. The sharpest next bounded target is to place two fixed replacements at arbitrary incomparable addresses, derive whether their two branch-local propagation chains plus the common LCA chain admit an exact compositional cost formula, and isolate the smallest obstruction if they do not.

Run 11 — Arbitrary incomparable updates factor through the LCA square

Target and model

Extend the Run 10 shared-parent theorem to fixed replacements at arbitrary incomparable addresses under the same complete-cache early-stopping algorithm. Determine whether their work decomposes into order-invariant branch-local terms plus the four-corner metric above their least common ancestor.

Let $w=\operatorname{lca}(u,v)$, and let (x) and (y) be the distinct children of (w) leading to update positions (u) and (v). For update (U), define:

• (B_U): its exact early-stopping work inside the subtree rooted at (x), including the replacement write and every attempted recomputation through (x), but excluding (w);
• (p_0,p_1): the cached state at (x) before and after (U);
• $\epsilon_U=\mathbf{1}[p_0\ne p_1]$, which is exactly whether (U) reaches and recomputes (w).

Define $B_V,q_0,q_1,\epsilon_V$ symmetrically in the (y)-branch. Fixing all other child states of (w), let its transition produce the corner states

$$a=\delta_w(p_0,q_0),\quad b=\delta_w(p_1,q_0),\quad c=\delta_w(p_0,q_1),\quad d=\delta_w(p_1,q_1). \tag{TA.18}$$

The (h) strict ancestors above (w), with unaffected sibling states fixed, induce unary maps $g_1,\ldots,g_h$, prefix maps $\Phi_i$, and the Run 10 propagation ultrametric

$$\lambda(x,y)=\sum_{i=0}^{h-1} \mathbf{1}[\Phi_i(x)\ne\Phi_i(y)]. \tag{TA.19}$$

CRD-TA-6: exact LCA factorization theorem

For arbitrary incomparable fixed replacements,

$$\boxed{ W(U;V)=C+\lambda(a,b)+\lambda(b,d) } \tag{TA.20}$$

and

$$\boxed{ W(V;U)=C+\lambda(a,c)+\lambda(c,d), } \tag{TA.21}$$

where the order-invariant branch/LCA base is

$$C=B_U+B_V+\epsilon_U+\epsilon_V. \tag{TA.22}$$

Consequently:

1. every order-dependent unit of work occurs strictly above the LCA;
2. the absolute order gap is at most (2h), independently of the two branch depths, and the bound is sharp;
3. the no-cancellation and levelwise flatness theorem from Run 10 applies unchanged to the corner states (TA.18);
4. total work is equal in both orders iff, for every (i<h), $$\Phi_i(b)\in{\Phi_i(a),\Phi_i(d)} \iff \Phi_i(c)\in{\Phi_i(a),\Phi_i(d)}. \tag{TA.23}$$

Proof

The path from (u) to (x) lies wholly inside one child subtree of (w), while the path from (v) to (y) lies wholly inside the other. Replacing at (v) changes no cached state, transition symbol, or fixed sibling argument on the (u)-to-(x) path. Therefore (U)'s local old/new state sequence, stopping point, cost (B_U), and boundary states (p_0,p_1) are identical in both orders. The symmetric statement holds for (V). Hence the entire branch-local contribution is (B_U+B_V), independent of order.

Early stopping invokes (w)'s transition after (U) exactly when the state at (x) changes, namely $\epsilon_U=1$, and after (V) exactly when $\epsilon_V=1$. These two LCA-attempt charges are also order-independent. If an update dies below (w), its epsilon is zero and its corresponding corner edge degenerates: for example (p_0=p_1) implies (a=b) and (c=d).

What remains is propagation strictly above (w). In order (U;V), the LCA state follows $a\to b\to d$; in order (V;U), it follows $a\to c\to d$. The exact numbers of strict-ancestor attempts are therefore the two sums of $\lambda$-lengths in (TA.20)--(TA.21). This proves the factorization. Subtracting cancels (C), so Run 10's sign-coherence, flatness criterion, and sharp (2h) bound apply verbatim. The sibling witness of Run 9 attains equality and is a special case of arbitrary incomparable addresses. $\square$

Hostile audit: spatial arrival data is insufficient

Branch depth, local work, and the two arrival bits do not determine order flatness. Take two direct child replacements with identical summaries

$$(B,p_0,p_1,\epsilon)=(1,0,1,1)$$

and one strict ancestor above (w). If the LCA transition is XOR, then

[ (a,b,c,d)=(0,1,1,0) ]

and both routes have common-chain length two. If instead $m(x,y)=\neg x\land y$, then

[ (a,b,c,d)=(0,0,1,0), ]

so one route has length zero and the other length two. All spatial and branch arrival data agree; only the LCA transition algebra differs. Thus an LCA-depth/arrival-only resource criterion is refuted.

The theorem also requires fixed payloads, a deterministic complete cache, unchanged off-path sibling contexts, and the stated early-stopping accounting. State-reading payloads, overlapping updates, mutable contexts, nondeterminism, or shared-DAG aliases can couple the supposedly local branches and invalidate the factorization.

Finite corroboration and status

tree_automaton_lca_composition_check.py generates every distinct two-state branch summary induced by unary paths of length at most four, every Boolean LCA transition, and every common unary chain of height at most four. It checks 2,182,400 combinations. All satisfy (TA.20)--(TA.23), sign coherence, and the (2h) bound; maxima are (0,2,4,6,8). The XOR/biased pair confirms the arrival-only obstruction. This is finite corroboration, not the general proof. External dependency: none. Novelty: not assessed; no claim.

Current obligations after Run 11

1. Do not treat LCA depth or branch-arrival bits as sufficient resource data; the four LCA corner states and their common-chain quotient images matter.
2. Do not extend the factorization to shared DAGs: incomparable tree addresses can denote aliased storage, so branch-locality may fail operationally.
3. The sharpest next bounded target is a hostile persistent-DAG test: determine whether two syntactically incomparable tree positions that share a cached descendant still admit any corrected branch/LCA factorization, or isolate the smallest aliasing obstruction.

Run 12 — Immutable occurrence path copying is alias-transparent

Bounded target and native persistent-DAG model

Test the warning after Run 11 rather than assuming it: does sharing a cached descendant by itself destroy the branch/LCA factorization for two incomparable tree-occurrence updates?

An immutable state-annotated ranked DAG node has the form

$$v=(f,v_1,\ldots,v_k,q_v), \qquad q_v=\delta_f(q_{v_1},\ldots,q_{v_k}).$$

A distinguished root (r) unfolds to a ranked tree $\operatorname{Unf}(r)$. An occurrence address is a word of child indices in that unfolding. Distinct addresses may resolve to the same DAG node.

For a pre-evaluated payload root (s), the occurrence update $\operatorname{pcopy}(r,u,s)$ follows address (u), replaces only that occurrence, allocates a fresh immutable node for every strict prefix of (u), and reuses all off-path child pointers. It performs no global hash-consing or canonical lookup. Every old version root is retained.

At a copied ancestor, the cached transition is evaluated exactly when the new state of the child on the copied path differs from its old state. Once those states agree, the complete parent input-state tuple is unchanged, so the old cached parent state may be copied without evaluating the transition; the same holds at every higher copied node.

Keep three resource coordinates separate:

• (A): fresh DAG-node allocations;
• (N): child-edge navigation steps used to follow occurrence addresses;
• (E): bottom-up automaton-transition evaluations.

Payload construction and global address indexing are excluded. For an address (u), write (d(u)=|u|).

CRD-TA-7: alias-transparent persistent translation

Let (U=(u,s)) and (V=(v,t)) be fixed pre-evaluated replacements at incomparable occurrence addresses of an immutable cached DAG, even when the two addresses or portions of their spines resolve to shared node identities. Then:

1. $$\operatorname{Unf}(\operatorname{pcopy}(r,u,s))=\operatorname{Unf}(r)[u\leftarrow\operatorname{Unf}(s)]; \tag{TA.24}$$

2. the two updates commute at the unfolded-tree endpoint and agree on the cached state at every unfolded occurrence; the fresh DAG identities need only be isomorphic after identities are erased;
3. sharing causes no change in the sequence or number of transition evaluations relative to the fully unshared occurrence tree;
4. in either sequential order, $$A=N=d(u)+d(v); \tag{TA.25}$$
5. if $w=\operatorname{lca}(u,v)$, (B_U,B_V) are the transition-evaluation counts strictly inside the two branches below (w), and $\epsilon_U,\epsilon_V$ record whether the branch-boundary state changes, then the evaluation component retains the Run 11 formulas $$E(U;V)=B_U+B_V+\epsilon_U+\epsilon_V +\lambda(a,b)+\lambda(b,d), \tag{TA.26}$$ $$E(V;U)=B_U+B_V+\epsilon_U+\epsilon_V +\lambda(a,c)+\lambda(c,d). \tag{TA.27}$$