Comparative Recognition Dynamics — Failure Ledger

Updated: 2026-08-23 10:00 MDT

CRD-F-1 — Arbitrary automaton states as tree-context parameters

Proposed route: Identify genuine one-hole tree contexts with all unary polynomial operations of the full automaton state algebra (Q), without first trimming the automaton or restricting constants.
Intended conclusion: Characterize ground-tree behavioral equivalence by testing all full-state polynomial contexts.
Precise failure: In the three-state automaton (Q={p,q,r}), (F={r}), with reachable set (R={p,q}), every actual tree context rejects both (p) and (q). The polynomial $f(\square,r)$ , however, accepts from (p) and rejects from (q). Its sibling parameter (r) has no ground-tree witness.
Scope: Representation/definition obstruction. It does not refute the tree-context theorem, minimization, or polynomial methods on the reachable subalgebra.
Surviving result: Actual contexts coincide exactly with unary polynomials whose constant parameters lie in the reachable subalgebra.
Revival condition: Trim to reachable states, or type every polynomial parameter with a reachability witness.
Successful replacement: CRD-TA-1 uses $R=\widehat\delta(T_\Sigma)$ and proves the exact context-polynomial correspondence there.
Status: Refuted as stated; repaired theorem proved.

CRD-F-2 — Counting residual CNF syntax as future behavior

Proposed route: Use “the number of residual formulas after a prefix” as an intrinsic count of future-equivalence classes.
Intended conclusion: Compare raw SAT branching and folded residual behavior without separately fixing semantic equality and representation.
Precise failure: For $\Phi_m=\bigwedge_i(x_i\vee z\vee w)$ at prefix depth (k), the same residual computation has (2^k) origin-labelled encodings, (k+1) duplicate-preserving multiset encodings, and (2) duplicate-deleted encodings. Yet there are exactly two residual Boolean functions.
Scope: Representation obstruction. It does not refute residual-function equivalence, reduced OBDDs, or any SAT algorithm.
Surviving result: Semantic residual equality gives an exact two-class quotient with multiplicities (1) and (2^k-1); the named fixed-order ROBDD realizes exactly that quotient at the cut.
Revival condition: State whether residuals are Boolean functions, clause sets, clause multisets, proof-carrying formulas, or provenance-labelled occurrences, and state the permitted normalization operations.
Successful replacement: CRD-SAT-1 fixes semantic residual functions and an explicit reduced ordered-BDD representation before counting.
Status: Representation-invariance claim refuted; repaired exact theorem proved.

CRD-F-3 — Erasing grade from ordered assignment dynamics

Proposed route: Treat residual Boolean behavior alone, possibly stored as a reduced OBDD node, as a uniform state for consuming the next unlabelled assignment bit, even when equivalent residuals occur at different prefix lengths.
Intended conclusion: Obtain a single-sorted congruence and update function without retaining the prefix position or next variable.
Precise failure: For (f(x_1,x_2)=x_2), the empty prefix and prefix (0) have equal lifted residuals, but appending (0) yields residuals (x_2) and (0). In the Run 2 ROBDD family, the same node (Z) is reached at grades (1) and (m), yet the same next bit must either skip an (x)-variable or branch on (z).
Scope: Definition and representation obstruction. It does not refute same-grade residual equivalence, ROBDD canonicity, variable-labelled traversal, or a state augmented with an explicit schedule.
Surviving result: Same-grade future-equivalence is the greatest observation-saturating congruence in the graded prefix system.
Revival condition: Include prefix grade in the state, label updates by variable identity, or explicitly supply and account for an external clock.
Successful replacement: CRD-SAT-2 uses carriers (H_k={0,1}^k) and typed extensions $e_{k,b}:H_k\to H_{k+1}$ .
Status: Grade-free route refuted; graded theorem proved.

CRD-F-4 — Inferring uniform state from per-cut quotient width

Proposed route: Bound the size of a stationary one-pass stream processor by the maximum number of future-equivalence classes appearing at any one prefix length.
Intended conclusion: If every cut has constant behavioral width, then one constant-size clock-free processor can realize all cuts coherently.
Precise failure: For $G_j(u)=\bot$ when (|u|<j) and (G_j(u)=u_j) thereafter, every fixed cut has width one or two, but the single-sorted suffix quotient has the (j+2) distinct states $P_0,\ldots,P_{j-1},Z,O$ . Pre-clock states at different lengths have different time-to-target behavior under common suffixes.
Scope: Exact representation/resource obstruction in the stationary deterministic Moore model with every-prefix observation. It is not a lower bound for terminal-only, timestamped, externally clocked, query-indexed, randomized, or richer-memory streaming models.
Surviving result: The uniform suffix quotient is single-sorted, but it internalizes the clock as ordinary residual state. Its exact state cost is (j+2), despite layer width at most two.
Revival condition: Include the grade as an explicitly charged interface coordinate, label symbols by position, or restrict comparison to one fixed grade. Then the layer-local width statement is valid, but it no longer measures total stationary state.
Successful replacement: CRD-STR-1 uses the global right congruence over all common suffixes; CRD-STR-2 computes its exact uniformization cost.
Status: Width-to-uniform-state inference refuted; exact replacement theorem proved.

CRD-F-5 — Disjoint commuting squares as a complete history calculus

Proposed route: Identify every pair of complete derivations with the same source and normal-form endpoint using only swaps of consecutive disjoint redex contractions.
Intended conclusion: In a terminating confluent system, independent-step squares generate all complete-history endpoint equivalences.
Precise failure: In the one-rule system $aa\to a$ , the two complete reductions of (a^3) contract the left or right (aa) first. Their initial redexes overlap, neither path admits a disjoint swap, and the two histories lie in distinct square classes despite sharing source (a^3) and endpoint (a). More generally, (a^n) has (C_{n-1}) square classes.
Scope: Refutation for occurrence-labelled complete reductions. The (a^3) witness is minimal by source length within this fixed system, not among all possible rewrite presentations.
Surviving result: Disjoint squares remove scheduling order inside one planar merge tree exactly; each class is the linear-extension graph of that tree's internal-node dependency order.
Revival condition: Add overlap-derived relations rather than only independent squares.
Successful replacement: The symmetric contextual length-two relation $((AB)C)\leftrightarrow(A(BC))$ connects all complete reductions, while retaining the distinction between partial histories.
Status: Square completeness refuted; exact Catalan classification and connectedness repair proved.

CRD-F-6 — Word sequences as derivation histories

Proposed route: Represent a rewrite derivation only by its sequence of underlying words and infer redex independence and overlap from that sequence.
Intended conclusion: Avoid occurrence or provenance labels without losing the history geometry.
Precise failure: Every complete occurrence-labelled reduction of (a^n) projects to the identical word chain $a^n\to a^{n-1}\to\cdots\to a$ . At (a^3), even the two overlapping histories project to the same three vertices.
Scope: Representation obstruction. It does not say that term-sequence derivations are wrong for term-level reachability or confluence; they are too coarse for this independence question.
Surviving result: Current redex position plus residual provenance is sufficient. Provenance remains a history annotation; including it in the semantic endpoint would make the compared endpoints unequal by definition.
Revival condition: Ask only term-level reachability or normal-form questions, or enrich edges by rule occurrence and redex position.
Successful replacement: CRD-RW-1 uses occurrence-labelled contractions and contiguous original-support intervals.
Status: Representation doctrine rejected for history classification.

CRD-F-7 — Connectivity as coherence

Proposed route: Treat the connectedness of complete histories under disjoint-square and contextual overlap moves as sufficient evidence that the resulting history calculus is coherent.
Intended conclusion: Once every pair of complete normalizing histories is connected, no further relation between transformations is needed.
Precise failure: For source (a^4), the raw transformation graph on the six complete histories is (C_6), with one disjoint edge and five overlap edges. Its disjoint-scheduling quotient is the rotation pentagon (C_5). Both are connected but have fundamental group and first homology $\mathbb Z$ .
Scope: Exact higher-dimensional obstruction in the complete occurrence-labelled $aa\to a$ system. It does not assert incoherence after adding pentagon cells or in arbitrary rewriting presentations.
Surviving result: The first missing relation is isolated exactly. One arity-four 3-cell fills the raw hexagon, equivalently the quotient pentagon.
Revival condition: Replace mere connectedness by simple connectedness or an explicit higher-dimensional coherence criterion.
Successful replacement: CRD-RW-2 computes the loop and proves one higher cell necessary and sufficient for the (a^4) component.
Status: Connectedness-to-coherence inference refuted.

CRD-F-8 — Calling the raw (a^4) boundary a pentagon

Proposed route: Describe the first higher loop directly as a pentagon on occurrence-labelled histories.
Intended conclusion: Use the five bracketings without separately tracking schedule representatives.
Precise failure: There are six raw histories. The balanced bracketing has two histories, related by the unique disjoint square. Therefore the raw boundary is a hexagon; it becomes a pentagon only after contracting that disjoint-scheduling edge.
Scope: Presentation distinction, not a refutation of the pentagon equation on square classes.
Surviving result: The raw hexagon and quotient pentagon present the same arity-four higher relation, with the disjoint square explicitly visible in the former.
Revival condition: State that derivations have first been quotiented by disjoint scheduling, or retain the hexagonal boundary in the raw calculus.
Successful replacement: Equation (RW.5) records the raw hexagon and (RW.6) its pentagon quotient.
Status: Representation shortcut rejected; repaired distinction proved.

CRD-F-9 — Disjoint leaf support as the rotation-interchange test

Proposed route: Call two contextual associativity rotations independent exactly when their leaf intervals are disjoint.
Intended conclusion: Generate all interchange squares by checking disjoint leaf supports.
Precise failure: At five leaves, start from ((((AB)C)D)E)). Rotate the inner (((AB)C)) and rotate the outer $((X D)E)\to X(DE)$ , treating (X) as an opaque metavariable. The two orders both produce ((A(BC))(DE)), although the inner leaf support is strictly contained in the outer support. Exhaustive enumeration finds three four-cycles in the five-leaf rotation graph and zero coinitial pairs with disjoint leaf support.
Scope: Definition obstruction for rotation interchange. It does not affect the (a^4) pentagon theorem: the four-leaf graph is (C_5) and has no four-cycle.
Surviving result: A rotation's active support is its two matched binary constructor occurrences, while metavariable subtrees are opaque. Disjoint active support, equivalently verified residual commutation in the finite graph, captures the nested interchange missed by leaf intervals.
Revival condition: Leaf-disjointness remains a sufficient special case, but cannot be used as a complete test.
Successful replacement: CRD-RW-2 excludes arity-four interchange by the graph's lack of a four-cycle and by the three-internal-node bound. The next (a^5) run must enumerate active-support or residual-commutation squares.
Status: General leaf-support criterion refuted; arity-four conclusion preserved by a stronger argument.

CRD-F-10 — Inferring simple connectedness from (H_1=0)

Proposed route: Compute the cellular boundary matrices for the five-leaf square–pentagon complex and promote (H_1=0) directly to $\pi_1=0$ .
Intended conclusion: Prove higher coherence by linear algebra alone.
Precise failure: First homology records only the abelianization of the fundamental group. The rank calculation $21-\operatorname{rank}\partial_1-\operatorname{rank}\partial_2=0$ cannot exclude a nontrivial perfect fundamental group.
Scope: Proof-method obstruction, not a counterexample to simple connectedness of the fixed complex.
Surviving result: The exact ranks $\operatorname{rank}\partial_1=13$ and $\operatorname{rank}\partial_2=8$ correctly give (H_1=0) and $H_2\cong\mathbb Z$ .
Revival condition: Homology may corroborate a separate van Kampen, contraction, shelling, or elementary-collapse proof.
Successful replacement: Remove pentagon (F_{[1,2]}), collapse the other eight faces along explicit free edges, and observe that the remaining 14-vertex, 13-edge connected graph is a tree.
Status: Withdrawn as a simple-connectedness proof; repaired by an explicit collapse certificate.

CRD-F-11 — Disjoint write targets imply update commutation

Proposed route: Declare two tree-cache updates independent whenever they write to incomparable subtree roots.
Intended conclusion: Obtain a commuting square without restricting how update payloads are computed.
Precise failure: From ((L,R)=(0,0)), let (U) write (L:=R) and (V) write $R:=\neg L$ . Targets are disjoint, but (U;V=(0,1)) and (V;U=(1,1)).
Scope: Definition obstruction; fixed pre-evaluated replacements survive.
Surviving result: Incomparable fixed replacements commute, and shared eager work is exactly the intersection of their ancestor paths.
Revival condition: Fix payloads or require noninterfering read/write footprints.
Successful replacement: CRD-TA-3a.
Status: Refuted as stated; repaired theorem proved.

CRD-F-12 — Promoting eager ancestor-union work to a lower bound

Proposed route: Treat $|A(u)\cup A(v)|$ as an intrinsic minimum update cost rather than the cost of a named cache algorithm.
Intended conclusion: Obtain a representation-independent dynamic lower bound from tree geometry alone.
Precise failure: A transition can leave a parent state unchanged, so an early-stopping implementation may avoid higher recomputation; richer stored summaries can also alter the interface.
Scope: Resource-accounting obstruction, not a failure of the eager cost formula.
Surviving result: The LCA formula exactly counts full ancestor-path writes/recomputations and batching savings.
Revival condition: Fix representation and probes and prove sensitivity of every claimed ancestor on a witness family.
Successful replacement: CRD-TA-3b is explicitly algorithm-relative.
Status: Intrinsic-lower-bound promotion rejected.

CRD-F-13 — Endpoint commutation as resource symmetry

Proposed route: Once two fixed subtree replacements form a commuting semantic square, assign the same total update work to its two directed paths, especially when their externally observed root traces also agree.
Intended conclusion: Treat semantic commutation as a sufficient criterion for order-invariant early-stopping maintenance.
Precise failure: For every $h\ge1$ , take sibling leaves initially ((0,0)), replace both by one, use parent transition $m(x,y)=\neg x\land y$ , place (h-1) identity carriers above it, and end in a constant-zero root. Left-then-right stops twice at the unchanged parent and costs (4). Right-then-left propagates a $0\to1\to0$ excursion through the entire chain and costs (2h+4). Both paths end at the same labelled tree and complete cache and have root trace ((0,0)).
Scope: Resource-valuation refutation in the named deterministic cache model. It does not refute semantic commutation, nor does it establish a lower bound for every dynamic representation.
Surviving result: A semantic square can be retained while its edges carry non-flat weights. The exact maximum path-sum difference for sibling leaves with (h) strict ancestors is (2h).
Revival condition: Require a path-independent potential valuation, use full ancestor-path charging, or impose an exact state-sensitivity condition that makes the propagated-change lengths balance on the two paths.
Successful replacement: CRD-TA-4 proves the sharp weighted-square separation and records the accounting model explicitly.
Status: Resource-invariance inference refuted; sharp replacement theorem proved.

CRD-F-14 — Cross-level cancellation of ancestor-chain order bias

Proposed route: Construct a resource-flat early-stopping square by making one update order more expensive at a low ancestor level and the other order more expensive at a higher level, so the signed biases cancel in total.
Intended conclusion: Show that equality of total work need not be visible level by level and that only the aggregate path-cost equation is available.
Precise failure: Prefixes of a deterministic ancestor chain induce nested kernel equivalences. In the discrete quotient at one level, a positive bias means the intermediate corner on one route lies in an endpoint class while the other lies outside. Coarsening can merge the outside corner into an endpoint class and erase the bias, but it cannot remove the first corner from an endpoint class. The sign therefore cannot reverse. The negative case is symmetric.
Scope: Failed counterexample route inside the fixed deterministic, current-state, early-stopping ancestor-chain model. Arbitrary weighted transition systems or history-dependent cache policies need not have nested kernels and are not covered.
Surviving result: The total absolute order gap is the sum of the absolute per-level biases. Total resource-flatness holds exactly when every level is flat, equivalently when both intermediate corners agree on membership in the two endpoint classes at every level.
Revival condition: Permit a higher update to depend on history, mutable siblings, nondeterministic choices, or another mechanism that can split or reorder earlier equivalence classes.
Successful replacement: CRD-TA-5 proves the nested-kernel ultrametric and no-cancellation theorem.
Status: Cancellation route refuted in the stated model; stronger exact criterion proved.

CRD-F-15 — LCA geometry and arrival bits determine resource flatness

Proposed route: Classify early-stopping order dependence for arbitrary incomparable updates using only branch depths, branch-local costs, LCA depth, and whether each change reaches the LCA.
Intended conclusion: Obtain a purely spatial extension of Run 8's LCA formula without retaining the automaton states at the merge.
Precise failure: Use identical direct branch summaries $(B,p_0,p_1,\epsilon)=(1,0,1,1)$ and one strict ancestor. With XOR at the LCA, corners ((0,1,1,0)) give equal route work. With $m(x,y)=\neg x\land y$ , corners ((0,0,1,0)) give order gap two. Every spatial and branch-arrival parameter is unchanged.
Scope: Refutes a state-free resource criterion in the fixed tree-cache model; it does not refute the exact branch/LCA factorization.
Surviving result: Branch-local costs factor additively, but the common contribution requires the four LCA corner states and their nested ancestor quotient images.
Revival condition: Retain the LCA transition algebra or an equivalent complete corner/quotient signature.
Successful replacement: CRD-TA-6 gives the exact factorization and imports Run 10's levelwise criterion above the LCA.
Status: Purely spatial/arrival criterion refuted; algebra-enriched composition theorem proved.

CRD-F-16 — Any shared descendant destroys branch/LCA factorization

Proposed route: Treat the move from a tree to a persistent DAG as an automatic counterexample to Run 11 whenever two incomparable occurrence addresses resolve to a shared cached node.
Intended conclusion: Isolate aliasing itself as a new cross-branch work term or as a universal obstruction to update commutation.
Precise failure: In an immutable DAG, occurrence-addressed path copying allocates a fresh spine and never mutates the shared node. The other incomparable branch retains its exact old pointer and cached state. An address induction shows that unfolding, transition evaluations, and the Run 11 branch summaries are identical to those of the unshared occurrence tree. No alias correction term appears.
Scope: This failed route concerns pure immutable path copying without global hash-consing, GC, or pointer-identity observation. It does not make arbitrary DAG implementations safe.
Surviving result: Sharing reduces retained representation size while fresh allocation/navigation remain exactly (d(u)+d(v)), and transition evaluation retains the Run 11 factorization.
Revival condition: Make node identity operational. Destructive writes to an aliased node give a minimal two-state noncommuting witness; global canonical reuse already invalidates the exact allocation count.
Successful replacement: CRD-TA-7 distinguishes occurrence semantics from identity semantics and proves the resource-preserving path-copy translation.
Status: Blanket alias obstruction refuted; exact operational boundary proved, with destructive and canonicalization obstructions preserved.

CRD-F-17 — Final canonical root makes allocation path-independent

Proposed route: Treat global hash-consing as making two commuting update histories allocation-equivalent whenever they finish at the same canonical root.
Intended conclusion: Recover a closed, resource-flat canonical update square merely from equality of its final interned node.
Precise failure: Let (z) be nullary, let the current root be (a=f(z,z)), and retain (b=f(a,z)). Use the old immutable root (a) as both fixed payloads. Replacing left then right reuses (b) and allocates only (f(a,a)), for cost one. Reversing the order allocates (f(z,a)) and then (f(a,a)), for cost two. Both paths finish at the same current root but at different retained tables. The initial table has only three nodes; four are required if payloads must be nullary.
Scope: Exact representation obstruction for two genuine direct-child replacements in an immutable retained binary hash-cons table. It is not a failure of semantic update commutation and does not bound arbitrary-height canonical DAG maintenance.
Surviving result: Allocation is the cardinality growth of the retained table. For genuine sibling updates, it is order-flat exactly when the two intermediate roots have balanced initial membership, and its order gap is sharply at most one.
Revival condition: If both intermediate roots already exist, the enriched representation endpoints and allocation agree. If only equal allocation is required, it suffices that both intermediate roots are either present or absent; in the absent case the retained endpoint sets still differ.
Successful replacement: CRD-TA-8 keeps the current canonical root and retained table as separate state coordinates and derives the exact two-order indicator formulas.
Status: Canonical-root-to-allocation inference refuted; exact local criterion and minimal witness proved.

CRD-F-18 — Initial-table membership remains the height-two flatness test

Proposed route: Extend Run 13 by comparing only whether the two one-update common-root candidates (r_{10},r_{01}) belong to the initial retained table (H), even after each update also interns a local parent.
Intended conclusion: Preserve the criterion $r_{10}\in H\iff r_{01}\in H$ unchanged at height two and treat the two local allocation decisions as independent additive terms.
Precise failure: Cross-level canonical equality can make an exclusive root coincide with a node requested in both orders. In the four-node acyclic witness (H={z,p_1=f(z,z),p_0=f(p_1,z),r_{00}=f(p_0,p_0)}), two occurrence updates give (r_{10}=q_1=f(p_1,p_0)), while (r_{01}=f(p_0,q_1)). Both exclusive roots are absent initially, but (r_{10}) is covered by the mandatory local candidate (q_1). The two costs are (2) and (3), not equal.
Scope: Representation obstruction in an immutable, monotone, structurally canonical height-two DAG with compound payloads and aliasing. It does not invalidate the initial-membership test when levels are separated by sorts, constructor symbols, or structural-height constraints.
Surviving result: Both orders request the common set (C={p_1,q_1,r_{11}}). After closing the initial table to $D=H\cup C$ , flatness holds exactly when $r_{10}\in D\iff r_{01}\in D$ . The common allocation term cancels, so the sharp gap remains one rather than growing to two.
Revival condition: Prove that neither exclusive common-root candidate can coincide with a local candidate or final root; then (D)-membership reduces to initial (H)-membership.
Successful replacement: CRD-TA-9 uses the set of all candidates mandatory in both orders before comparing the two exclusive candidates.
Status: Initial-membership criterion refuted at height two; corrected common-set coverage theorem proved.

CRD-F-19 — Opposite height-three membership biases cancel structurally

Proposed route: Model the two exclusive height-three spine candidates on each route as unrelated keys. Cover (x_2,y_1) but not (x_1,y_2), giving level biases (+1,-1) and equal total allocation by cancellation.
Intended conclusion: Show that arbitrary cross-level identity destroys the height-two sign discipline and that an arbitrary-height spine law needs independent per-level terms.
Precise failure: A canonical node on the copied spine structurally contains its predecessor. A valid retained table is descendant-closed, so $x_2\in D$ forces $x_1\in D$ . The proposed coverage pattern is not a finite acyclic structural hash-cons state. More generally, each exclusive chain meets (D) in a prefix, making all nonzero normalized level biases have one sign.
Scope: Refutes the cancellation construction only for strict structural dependency chains under monotone retention. It does not rule out cancellation for unrestricted key stores, garbage-collected tables, or forked exclusive dependency DAGs.
Surviving result: The unrestricted profile is a useful hostile witness showing that monotone set union alone is insufficient; descendant closure is the load-bearing invariant.
Revival condition: Replace the exclusive spine by a dependency poset with incomparable nodes, or remove structural closure. Then opposite uncovered ideals may coexist and cancellation must be tested anew.
Successful replacement: CRD-TA-10 gives exact arbitrary-height costs from the two covered-prefix lengths and a sharp gap equal to spine length.
Status: Structural cancellation route refuted; precise boundary and arbitrary-height replacement theorem proved.

CRD-F-20 — Descendant closure prevents cancellation on every dependency DAG

Proposed route: Promote Run 15's no-cancellation theorem from exclusive chains to arbitrary finite structural dependency posets, using only the fact that retained tables are descendant-closed.
Intended conclusion: Treat sign coherence as a general invariant of monotone structural hash-cons allocation.
Precise failure: Descendant closure says that covered candidates form an order ideal, but ideals of a non-chain need not be nested. For the two-element antichain, (I_X={a}) and (I_Y={b}) are both valid ideals. They produce local biases ((-1,+1)), equal total allocation, and different retained tables. A finite term DAG with four independent unary nodes over one retained leaf realizes the pattern without cycles or missing descendants.
Scope: Refutes global sign coherence for genuinely forked exclusive request regions. It does not refute Run 15, because single-occurrence path copying generates a chain rather than a fork.
Surviving result: The exact replacement theorem uses the ideal lattice: opposite biases occur iff the two coverage ideals are incomparable, and cancelled imbalance is $(|I_X\triangle I_Y|-||I_Y|-|I_X||)/2$ .
Revival condition: Require the ideal lattice to be totally ordered; equivalently, require the exclusive dependency poset itself to be a chain.
Successful replacement: CRD-TA-11 classifies all finite dependency posets and proves that the original two-update path-copy model remains in the chain case.
Status: Blanket descendant-closure generalization refuted; exact chain/non-chain boundary proved.

CRD-F-21 — Forked cancellation extends the original path-copy update model

Proposed route: Treat the two-element-antichain witness as a new counterexample inside the same two fixed single-occurrence update model used in Runs 12--15.
Intended conclusion: Reopen the native tree-update branch around forked allocation cancellation.
Precise failure: One occurrence replacement rebuilds exactly the unique address-to-root prefix path. After separating order-common local and final candidates, every order-exclusive intermediate node lies on that one path. The exclusive dependency order is therefore necessarily a chain.
Scope: Applies to immutable occurrence-addressed path copying with fixed pre-evaluated payloads and two incomparable single-site updates. Multi-site commands, speculation, or multiple-parent copy regions are different models.
Surviving result: Forked cancellation is real for expanded request-poset models, and CRD-TA-11 gives their exact rank law.
Revival condition: Explicitly adopt an update primitive or maintenance strategy that natively materializes incomparable path-exclusive nodes.
Successful replacement: Close the stated tree/hash-cons subcampaign and pivot to SAT/branching/proof dynamics.
Status: Native-extension route blocked; pivot required by the focus gate.

CRD-F-22 — Begin with the four-clause forced-literal gadget

Proposed route: Use the four clauses $(z\vee a\vee b)$ , $(z\vee a\vee\neg b)$ , $(z\vee\neg a\vee b)$ , and $(z\vee\neg a\vee\neg b)$ , which jointly force (z), as the smallest strict-3CNF learned-clause separation.
Intended conclusion: Treat adding learned unit ((z)) as the first and minimal example of semantic equality with stronger propagation.
Precise failure: Minimality fails once the comparison is correctly made at a residual prefix. Two clauses already suffice: $(u\vee a\vee b)$ and $(u\vee a\vee\neg b)$ resolve to $(u\vee a)$ ; under (u=0), adding that resolvent changes UP and removes one decision while preserving residual function (a).
Surviving result: The four-clause gadget may still be useful when the learned receipt must be a root-level forced unit, but no such constrained minimality theorem was proved.
Successful replacement: CRD-SAT-3 gives a clause-minimal two-clause witness and an analytic one-clause impossibility proof.
Status: Refuted as the unrestricted smallest candidate; narrower role preserved.

CRD-F-23 — Semantic residual equality determines propagation work

Proposed route: Quotient residual clause databases immediately by their Boolean functions and perform unit-propagation or branching accounting on the quotient classes.
Intended conclusion: Treat semantic residual state as sufficient for both correctness and local solver-resource analysis.
Precise failure: The databases (D_0) and $D_0\cup{u\vee a}$ are semantically identical, including under prefix (u=0), but only the second contains the unit receipt needed for root UP. Their exact minimum successful-decision costs are one and zero.
Scope: Refutes factorization of UP and the named DPLL cost through the semantic quotient. It does not refute semantic residuals for behavior or a stronger inference engine that derives the resolvent dynamically.
Revival condition: Enrich the quotient state with an inference basis or charge the cost of reconstructing the missing implicate.
Successful replacement: Keep semantic residual, clause/proof state, and resource valuation as separate coordinates.
Status: Refuted; explicit representation coordinate required.

CRD-F-24 — Semantic product structure implies resource additivity

Proposed route: Once a residual Boolean function factors as $f_1\wedge\cdots\wedge f_k$ on disjoint variables, sum the solver costs of the factors without inspecting the retained clause database.
Intended conclusion: Treat additivity as a semantic property of the residual function.
Precise failure: The base product and the cross-chain presentation have the same function $\bigwedge_i a_i$ under the fixed prefix. The base clause hypergraph has (k) components and exact cost (k); sound redundant cross clauses connect it into one chain and reduce exact cost to one.
Revival condition: Require the retained database and allowed propagation rules to decompose by variable-clause incidence components.
Successful replacement: CRD-SAT-4a proves additivity from presentation separation; CRD-SAT-4b gives its sharp semantic counterexample.
Status: Semantic inference refuted; representation-level theorem proved.

CRD-F-25 — Use the cross-chain clauses as an ordinary CDCL witness

Proposed route: Present $M_i=(\neg a_i\vee u_{i+1}\vee a_{i+1})$ as clauses naturally learned by standard conflict analysis from the disconnected product.
Intended conclusion: Attribute the nonlocal collapse directly to native CDCL learning.
Precise failure: Pure resolution from a variable-disjoint union remains inside one component. (M_i) is obtained by weakening the local implicate $u_{i+1}\vee a_{i+1}$ with the irrelevant literal $\neg a_i$ ; it is sound but not produced by the stated pure-resolution interface.
Surviving result: Arbitrary entailed-clause retention or resolution plus weakening can create the collapse, exposing a proof-system boundary.
Revival condition: Supply a connected source formula and an explicit conflict-relevant resolution derivation of the cross clause.
Successful replacement: Keep the cross chain as a hostile representation obstruction and make a connected pure-resolution witness the next target.
Status: Native-CDCL interpretation blocked; broader sound-clause result preserved.

CRD-F-26 — Pure resolution cannot create nonlocal propagation savings

Proposed route: Generalize Run 18's locality obstruction and conclude that a learned clause affecting propagation outside its parent pair must use weakening or arbitrary entailed-clause insertion.
Intended conclusion: Treat pure resolution as inherently local for the resource separation under study.
Precise failure: Locality in Run 18 followed from a disconnected source. In the connected three-clause source $T=(u\vee v\vee a_0)$ , $P=(\neg a_0\vee a_1\vee b)$ , and $Q=(\neg a_0\vee a_1\vee\neg b)$ , the outside clause (T) activates the pure resolvent $L=(\neg a_0\vee a_1)$ . Retaining (L) removes one future decision, and a conflict after deciding (a_1=0) derives exactly (L).
Scope: This refutes a global pure-resolution obstruction, not the proven component-locality theorem for disconnected databases.
Successful replacement: Clause-incidence connectivity plus an explicit conflict dependency path permits genuinely nonlocal reuse; the exact guarded chain law is CRD-SAT-5b.
Status: Refuted outside disconnected components; Run 18 locality theorem retained with its hypothesis.

CRD-F-27 — A learned receipt is automatically resource-beneficial

Proposed route: Count the one future decision removed by Run 19's learned clause and declare learning an unconditional improvement.
Intended conclusion: Collapse acquisition and reuse into one scalar “decision saved” statement.
Precise failure: Across (r) identical episodes, never learning has resource vector ((r,0,0)), while immediate conflict-driven learning and retention has ((1,1,1)). Neither vector dominates the other for (r>1). With weights ((d,c,s)), learning pays exactly when $(r-1)d\ge c+s$ . If the receipt is forgotten after every episode, the conflicting strategy has ((r,r,0)) and is strictly worse.
Scope: The result uses one-time clause storage and identical repeated demands. Other valuations and demand families require their own threshold.
Successful replacement: Keep acquisition work, retained proof state, and future demand coverage as separate coordinates; compare them by a Pareto or explicitly weighted law.
Status: Weight-free scalar inference refuted; exact conditional law proved.

CRD-F-28 — Every covered demand contributes one online saved decision

Proposed route: If a receipt benefits (H) demands, assign it gross decision benefit (H) and use $Hd\ge c+s$ as the acquisition threshold.
Intended conclusion: Treat demand coverage as reusable benefit without accounting for where the receipt comes from.
Precise failure: In the four-prefix family, acquiring the receipt on a covered demand consumes one decision and one of the (H) opportunities. Optimal acquisition therefore has (r-H+1) decisions versus (r) without learning: the net saving is (H-1), and the correct threshold is $(H-1)d\ge c+s$ .
Additional hostile result: Waiting for the first covered demand is not uniquely optimal. Acquiring earlier on an uncovered demand costs one extra decision but captures the first later covered saving, so the two policies tie.
Scope: Specific to the stated conflict trace and demand family. Offline or preprocessed receipts have a different acquisition term.
Successful replacement: Separate gross coverage from acquisition premium; use (D_j=r+p_j-H_{>j}) before optimizing over acquisition time.
Status: Gross-coverage shortcut refuted; exact order-independent law proved.

CRD-F-29 — Bounded semantic width bounds persistent proof-state multiplicity

Proposed route: Use a small fixed-order semantic residual quotient or reduced-OBDD width as an upper bound on the number of retained resolution states relevant at the same SAT cut.
Intended conclusion: Treat semantic branching width as a proxy for the size of the solver's persistent proof-state space.
Precise failure: In the connected guarded chain, every subset $S\subseteq[k]$ of the pure-resolution receipts $L_i=(\neg a_{i-1}\vee a_i)$ yields the same residual function $\bigwedge_i a_i$ . Its reduced OBDD has nonterminal width one, yet the exact retained-receipt fiber has (2^k) states. Even quotienting by the scalar minimum-decision cost leaves (k+1) classes, with cost-(q) multiplicity $\binom{k}{q}$ .
Additional hostile result: Bounded learned-clause width does not repair the inference: all optional receipts have width two. The exponential count comes from independent retained-presence coordinates, not wide clauses.
Scope: Representation obstruction in the monotone set-of-receipts model. Full resolution closure, deletion, subsumption replacement, duplicate or provenance tracking, and richer future demands define different fibers.
Successful replacement: Treat semantic residual state, scalar resource quotient, and exact proof-state representation as three distinct levels: $2^k\to k+1\to1$ . State explicitly which observation performs each quotient.
Status: Width-based state bound refuted; exact fiber and quotient laws proved.

CRD-F-30 — The scalar decision-cost quotient preserves all useful demands

Proposed route: Compress a retained receipt subset (S) to its size (|S|), equivalently to Run 22's minimum-decision value (k-|S|), and use the resulting (k+1)-state quotient as the proof-state representation.
Intended conclusion: Treat equal total future decision cost as sufficient operational equivalence between learned databases.
Precise failure: At (k=2), (S={1}) and (S'={2}) both have minimum successful-decision cost one. But the two stage-readiness answer vectors are ((1,0)) and ((0,1)). The cost quotient forgets which stage is prepared.
General obstruction: For demands indexed by $T\subseteq[k]$ , the exact observable is $S\cap T$ . There are (2^{|T|}) demand classes, requiring (|T|) retained bits. With all stages demanded, no two receipt subsets can be identified.
Scope: The demands ask what the current database's unit-propagation closure produces. Asking semantic entailment, permitting query-time receipt derivation, or charging reconstruction work defines another interface.
Successful replacement: Index the quotient by the declared demand family: semantic observation gives one class, scalar cost gives (k+1), and stage set (T) gives (2^{|T|}).
Status: Scalar-cost sufficiency refuted; exact demand-indexed quotient and information law proved.

CRD-F-31 — Singleton UP signatures determine fixed-policy branching work

Proposed route: Compare clause databases under every root and single-literal unit-propagation closure, then promote signature equality to operational equivalence for deterministic DPLL.
Intended conclusion: Treat first-order propagation readiness as a sufficient summary of future branching behavior.
Precise failure: The connected strict-3CNF $D=(x\vee\neg z\vee\neg p)\wedge(y\vee\neg z\vee p)$ and the equivalent pure-resolvent extension $D^+=D\wedge(x\vee y\vee\neg z)$ have identical singleton signatures. Under false-first order (x<y<z<p), however, (D) needs decisions (x=0,y=0,z=0), while (D^+) propagates (z=0) after the first two decisions.
Why the route was especially weak: Any strict 3CNF has trivial singleton UP behavior: one assignment leaves at least two unset literals in every unsatisfied clause. The signature ignores the first possible interaction order by construction.
Scope: The separation disappears under some branching orders and is visible to the two-literal signature. It does not refute stronger signatures or establish heuristic-independent runtime separation.
Successful replacement: Use the interaction-depth filtration $\sigma_t$ of UP behavior under seeds of size at most (t), and state the branching policy and stopping convention explicitly.
Status: First-order sufficiency refuted; minimal second-order witness and strict-width vacuity lemma proved.

CRD-F-32 — One fixed local UP depth controls branching across all widths

Proposed route: Choose a constant seed depth (t), compare every UP closure through that depth, and treat equality as a width-independent operational summary for fixed-policy DPLL.
Intended conclusion: Obtain a finite local observation radius that controls future branching work across arbitrary CNF clause widths.
Precise failure: For each $t\ge1$ , set (r=t+2) in Run 25's family. The semantically equivalent databases (D_r,D_r^+) agree on all UP seeds of size at most (t=r-2), yet the fixed false-first policy uses (r) decisions on (D_r) and (r-1) on (D_r^+).
Mechanism: A strict width-(r) learned clause cannot activate before (r-1) of its literals have been falsified. Width is therefore an activation codimension that escapes every fixed lower-order signature.
Scope: The counterfamily increases width with (t). It does not establish unbounded escape depth for fixed strict 3CNF, nor heuristic-independent work.
Successful replacement: Index UP observations by interaction depth and clause width together. Treat the fixed-width auxiliary-gadget question as a separate unresolved boundary.
Status: Width-independent bounded-depth sufficiency refuted; sharp arbitrary-width theorem proved.

CRD-F-33 — Auxiliary strict-3CNF chains evade every finite UP depth

Proposed route: Add auxiliary strict-3CNF clauses so the base database simulates a learned 3-clause on every two-literal boundary seed, but arrange for deeper assignments to disable that simulation while the retained clause remains unit.
Intended conclusion: Construct unbounded interaction depth at fixed strict width three despite equality of complete depth-two UP signatures.
Precise failure: Unit derivations persist under seed extension: every extension either reproduces the derived literal or causes conflict. Equality on the at-most-two-literal boundary seeds therefore makes every added width-three clause UP-absorbed by the base. Absorbed additions cannot supply a first new unit or conflict under any larger seed.
Scope: Refutes the escape only for complete UP closure/conflict observation and additions of width at most three. It does not cover formula-sensitive heuristics, proof provenance, scan/watch cost, conflict-analysis graphs, deletion, or wider learned clauses.
Surviving result: More generally, additions of width at most (w) are completely controlled at seed depth (w-1), and Run 25 makes this exact.
Revival condition: Change the observer/resource so it is not determined by UP closure, or permit learned clauses whose width grows with the desired interaction depth.
Successful replacement: CRD-SAT-12a--c, the exact fixed-width absorption and DPLL-trace theorem.
Status: Fixed-3CNF auxiliary-chain route refuted; exact boundary proved.

CRD-F-34 — Complete UP closure determines conflict-analysis work

Proposed route: After Run 26 proved equality of UP closure on every seed, treat that closure operator as a sufficient state for deterministic CDCL conflict analysis.
Intended conclusion: Infer equal learned clauses and equal analysis work whenever two databases are semantically and all-seed-UP equivalent.
Precise failure: For every (m), the connected strict-3CNF pair (F_m,G_m) has the same semantic function and complete UP operator. Under the fixed earliest-clause reason policy, however, (F_m)'s conflict reason passes through $a_1,\ldots,a_m,b$ , while the retained clause $x\vee y\vee b$ gives (G_m) a direct reason edge. First-UIP analysis learns the same clause $x\vee y$ in (m+1) versus one resolution pivots.
Scope: The obstruction is provenance- and policy-sensitive. Reordering clauses, replacing reasons, or using a different analysis cost can erase or alter the gap. It is not a minimum resolution-proof lower bound or a heuristic-independent runtime result.
Surviving useful result: Complete UP equivalence still controls the formula-blind fixed-order DPLL traces covered by Run 26. What it does not control is the retained justification graph for those consequences.
Revival condition: Enrich the state with propagation reasons, or prove that a named canonical reason-selection/minimization policy factors through a stronger quotient.
Successful replacement: CRD-SAT-13 gives an exact arbitrary-(m) reason-path compression law with common learned clause and width.
Status: Closure-sufficiency claim refuted; precise representation boundary and exact resource law proved.

CRD-F-35 — A retained reason shortcut guarantees realized analysis savings

Proposed route: Remove Run 27's clause-priority qualification by arguing that every legal propagation schedule in (G_m) must use the retained shortcut (L) as the reason for (b).
Intended conclusion: Promote the one-pivot trace from an available proof to a schedule-independent runtime guarantee.
Precise failure: A legal schedule may postpone both (L) and the opposite endpoint clause, propagate $a_1,\ldots,a_m,b$ along the original chain, and then analyze the old conflict in (m+1) pivots. Thus ${c(\tau):\tau\in\mathcal T(G_m)}={1,m+1}$ .
Additional hostile finding: Run 27's fixed all-(X) trace has width three, but arbitrary mixed (X/Y) reasons in (F_m) can create a width-four intermediate resolvent for every $m\ge2$ .
Scope: The shortcut still changes the minimum available first-UIP cost from (m+1) to one. The failure concerns guaranteed or arbitrarily scheduled realized cost, not proof availability.
Surviving useful result: Every (F_m) trace costs exactly (m+1); therefore the minimum gap (m) is genuinely priority-independent.
Revival condition: Specify a reason-minimizing policy or prove that the online scheduler selects a shortest available reason. Charge the cost of finding that reason separately.
Successful replacement: CRD-SAT-14 gives the complete cost spectrum, exact minimum and maximum laws, and all-schedule width audit.
Status: Guaranteed-speedup route refuted; priority-independent optimum separation proved.