FPRD LabShare an approach

Research program

Comparative Recognition Dynamics

Mathematical models of computation that preserve enough structure to compare not only outcomes, but also the histories and resources that produce them.

Further reading

DocumentRole
OverviewIntroduction, scope, and reading guide
ResultsStatements and connections across the models
ModelsFormal specifications and comparisons
Counterexamples and failed approachesNegative results and corrected formulations
Computational checksFinite verification reports

Rewriting histories

Enumeration, connectedness, and coherence

These results study complete reductions in the rule aa→aaa\to a while retaining which occurrence is contracted at each step. They distinguish concrete histories, changes in the scheduling of independent steps, and higher relations between transformations.

CRD-RW-1a · Theorem · exact enumeration

Complete reductions are counted by permutations and binary trees

In the occurrence-labelled rewriting system R={aa→a}R=\{aa\to a\}, the complete reductions an⇒∗aa^n\Rightarrow^*a are in bijection with the (n−1)!(n-1)! orders in which the original gaps are deleted. After identifying consecutive contractions with disjoint residual supports, the equivalence classes are the Cn−1C_{n-1} planar full binary trees on nn leaves.

Result
Proved in the stated occurrence-labelled model
Proof
A contraction deletes exactly one surviving original gap, and every ordering of the n−1n-1 gaps is legal, giving (n−1)!(n-1)! histories. Each history also determines a planar full binary merge tree. The histories producing a fixed tree are the linear extensions of its internal-vertex dependency order. Adjacent swaps of incomparable internal vertices are exactly swaps of contractions on disjoint leaf intervals, so the square classes are precisely the merge trees. The Catalan recurrence then gives Cn−1C_{n-1} classes.
Scope
The result concerns complete reductions and retains occurrence identity.

Sources and detailed status →

CRD-RW-1b · Theorem · connectedness

Associativity rotations connect all complete reductions

After adjoining the contextual overlap move ((AB)C)↔(A(BC))((AB)C)\leftrightarrow(A(BC)) to the disjoint-square moves, every pair of complete occurrence-labelled reductions an⇒∗aa^n\Rightarrow^*a is connected.

Result
Proved for complete reductions in the stated model
Proof
By CRD-RW-1a, disjoint squares connect all histories with the same merge tree. The overlap move induces an ordinary rotation of planar full binary trees. Repeated rotations take every such tree to the right comb, so the augmented transformation graph is connected.
Scope
Connectedness does not imply simple connectedness or higher coherence.

Sources and detailed status →

CRD-RW-2a · Proposition · finite classification

The four-letter history graph is a hexagon

For complete occurrence-labelled reductions of a4a^4, the graph generated by disjoint and overlap moves is the six-cycle C6C_6. Contracting its unique disjoint-scheduling edge gives the five-cycle C5C_5, the rotation graph of the five planar binary trees on four leaves.

Result
Proved by complete enumeration and edge classification
Proof
The six orders of the three original gaps give the six histories. Adjacent transpositions give a Cayley cycle C6C_6. Exactly one edge represents disjoint scheduling; its contraction identifies the two histories with the same merge tree and leaves the five-tree associahedral cycle C5C_5.
Scope
This is a fixed arity-four calculation.

Sources and detailed status →

CRD-RW-2b · Proposition · coherence cell

One higher cell fills the arity-four loop

The unique loop in the arity-four transformation graph survives backtrack cancellation and residual-interchange squares. In the fixed presentation, attaching one 3-cell along the raw hexagon—or equivalently along the quotient pentagon—is necessary and sufficient to fill it.

Result
Proved for the fixed arity-four component
Proof
The graph has cycle rank E−V+1=1E-V+1=1. At four leaves there is no pair of independent rotations and hence no residual-interchange 4-cycle to fill the generator. A single disk attached with degree ±1\pm1 along the primitive cycle kills the loop; without a new 2-dimensional filler the loop remains.
Scope
Necessity and sufficiency are relative to this fixed one-skeleton.

Sources and detailed status →

CRD-RW-3a · Theorem · cell-complex classification

The five-leaf rotation complex has nine native faces

The five-leaf binary-tree rotation complex K5K_5 has 14 vertices, 21 edges, six contextual pentagons, and three residual-interchange squares. Its nine faces are indexed by the proper contiguous clusters of the five leaves.

Result
Proved for the schedule-quotient five-leaf complex
Proof
There are C4=14C_4=14 trees and 21 rotation edges. A cluster of size rr supports Cr−1C5−rC_{r-1}C_{5-r} vertices: five for r=2r=2 or 44, and four for r=3r=3. The six size-two and size-four intervals give pentagons; the three size-three intervals give squares. The active-constructor classification shows that these exhaust the native elementary faces.
Scope
This is the tree-level schedule quotient, not the raw 24-history complex.

Sources and detailed status →

CRD-RW-3b · Theorem · homotopy type

The five-leaf rotation complex is a sphere

Every edge of K5K_5 lies in exactly two native faces. Removing one pentagon leaves a collapsible complex; consequently K5≃S2K_5\simeq S^2, with H1(K5)=0H_1(K_5)=0 and H2(K5)≅ZH_2(K_5)\cong\mathbb Z.

Result
Proved by an explicit elementary-collapse certificate
Proof
Each rotation edge preserves exactly two proper clusters, so it is incident to exactly two listed faces. Remove the interior of one pentagon and collapse the other eight faces along explicit free edges. The remaining graph has 14 vertices and 13 edges and is connected, hence is a tree and collapses to a point. Restoring the removed disk gives a 2-sphere. Independently, rank⁡∂1=13\operatorname{rank}\partial_1=13 and rank⁡∂2=8\operatorname{rank}\partial_2=8 yield H1=0H_1=0 and H2≅ZH_2\cong\mathbb Z.
Scope
The proof concerns the fixed five-leaf complex.

Sources and detailed status →

Rewriting histories

Counterexamples and limitations

These examples show where natural simplifications lose essential information and where additional structure is needed.

CRD-RW-F1 · Counterexample · failed completeness claim

Disjoint squares do not classify overlapping histories

In the terminating confluent system aa→aaa\to a, swapping consecutive disjoint redex contractions does not connect all complete reductions with the same source and normal-form endpoint: the two reductions of a3a^3 begin at overlapping redexes and lie in different square classes.

Status
Refuted in the stated occurrence-labelled model; repaired by adding contextual overlap moves
Evidence
From a3a^3, contracting the left aaaa first and contracting the right aaaa first produce two complete histories with the same endpoints. Their initial redexes overlap, so neither history contains a disjoint adjacent pair to swap; hence they are distinct square classes. The source further classifies ana^n into Cn−1C_{n-1} such classes and reconnects them with ((AB)C)↔(A(BC))((AB)C)\leftrightarrow(A(BC)).
Scope
The a3a^3 witness is minimal by source length only inside this fixed rewriting system.

Sources and detailed status →

CRD-RW-F2 · Representation obstruction

Word sequences erase redex identity

For aa→aaa\to a, the sequence of underlying words is too coarse to recover redex independence or overlap: every complete occurrence-labelled reduction of ana^n projects to the same chain an→an−1→⋯→aa^n\to a^{n-1}\to\cdots\to a.

Status
Representation doctrine refuted for history classification
Evidence
Every step shortens aka^k to ak−1a^{k-1}, regardless of which adjacent pair is contracted. Thus all complete histories project to the identical word chain. Already at a3a^3, the two overlapping first choices become indistinguishable after projection.
Scope
Word sequences remain adequate for ordinary term-level reachability and confluence questions.

Sources and detailed status →

CRD-RW-F3 · Negative result · coherence obstruction

Connected history graphs need not be coherent

For complete occurrence-labelled reductions of a4a^4 under aa→aaa\to a, the graph generated by disjoint-square and contextual-overlap moves is connected but has π1≅H1≅Z\pi_1\cong H_1\cong\mathbb Z; connectedness therefore does not establish coherence.

Status
Connectedness-to-coherence inference refuted; one higher cell repairs the fixed component
Evidence
The six raw histories form a cycle C6C_6; contracting the single disjoint edge gives the five-vertex rotation cycle C5C_5. Both are connected and both have fundamental group and first homology Z\mathbb Z. Attaching one arity-four 3-cell along the raw hexagon, equivalently the quotient pentagon, fills the unique loop.
Scope
The result concerns the fixed arity-four component, not every rewriting presentation.

Sources and detailed status →

CRD-RW-F4 · Counterexample · definition obstruction

Leaf-disjointness misses nested interchange

Disjoint leaf intervals are not a complete test for independent contextual rotations: at five leaves, an inner rotation on ((AB)C)((AB)C) commutes with an outer rotation ((XD)E)→X(DE)((XD)E)\to X(DE) even though the inner leaf support is strictly contained in the outer support.

Status
Leaf-support criterion refuted; active-constructor support survives
Evidence
Starting at (((AB)C)D)E)(((AB)C)D)E), perform the inner rotation ((AB)C)→(A(BC))((AB)C)\to(A(BC)) and the outer rotation ((XD)E)→X(DE)((XD)E)\to X(DE) in either order. Both paths end at (A(BC))(DE)(A(BC))(DE), although one leaf interval is nested in the other. The preserved exhaustive enumeration finds three four-cycles and no coinitial rotation pair with disjoint leaf intervals.
Scope
Leaf-disjointness remains a sufficient special case; it is not necessary.

Sources and detailed status →

CRD-RW-F5 · Failed proof method

Vanishing first homology does not prove simple connectedness

For the five-leaf square–pentagon complex, the calculation H1=0H_1=0 cannot by itself establish π1=0\pi_1=0, because first homology records only the abelianization of the fundamental group.

Status
Homology-only proof withdrawn; conclusion recovered by an explicit collapse certificate
Evidence
The boundary ranks rank⁡∂1=13\operatorname{rank}\partial_1=13 and rank⁡∂2=8\operatorname{rank}\partial_2=8 correctly yield H1=0H_1=0 and H2≅ZH_2\cong\mathbb Z, but a nontrivial perfect fundamental group would have the same first homology. The repaired proof removes one pentagon, collapses the other eight faces along recorded free edges, and leaves a connected graph with 14 vertices and 13 edges, hence a tree.
Scope
The homology ranks remain valid and useful corroboration.

Sources and detailed status →

SAT and proof dynamics

Interaction depth, absorption, and retained reasons

Clause width controls when a retained consequence can first become visible to unit propagation. Absorption determines when it preserves every unit-propagation consequence. Even then, two databases can retain different reasons for those consequences and support conflict proofs of very different lengths.

Interaction depth

The signature σt(D)\sigma_t(D) records unit-propagation closure and conflict status for every consistent seed assigning at most tt variables. A strict rr-clause cannot become unit or false before r−1r-1 of its variables have been assigned.

The arbitrary-width family

For r≥3r\ge3, putAr=z1∨⋯∨zr−3∨¬zr−2A_r=z_1\vee\cdots\vee z_{r-3}\vee\neg z_{r-2}, where the positive prefix is empty at r=3r=3. The source clauses areCr−=(Ar∨x∨¬p)C_r^-=(A_r\vee x\vee\neg p) andCr+=(Ar∨y∨p)C_r^+=(A_r\vee y\vee p). Their resolvent is Lr=(Ar∨x∨y)L_r=(A_r\vee x\vee y). Write Dr=Cr−∧Cr+D_r=C_r^-\wedge C_r^+ andDr+=Dr∧LrD_r^+=D_r\wedge L_r.

Absorption

For a literal ℓ∈C\ell\in C, the boundary seed B(C,ℓ)B(C,\ell) falsifies every other literal of CC. The clause is UP-absorbed by FF when unit propagation from every such seed either conflicts or derives ℓ\ell.

The clause family

For m≥1m\ge1, the base database uses variables x,y,a1,…,am,bx,y,a_1,\ldots,a_m,b. It contains

  • C0=(x∨y∨a1)C_0=(x\vee y\vee a_1);
  • Xi=(x∨¬ai∨ai+1)X_i=(x\vee\neg a_i\vee a_{i+1}) and Yi=(y∨¬ai∨ai+1)Y_i=(y\vee\neg a_i\vee a_{i+1}) along the chain, with am+1=ba_{m+1}=b;
  • the conflict clause K=(x∨y∨¬b)K=(x\vee y\vee\neg b).

Write FmF_m for this database and Gm=Fm∪{L}G_m=F_m\cup\{L\}, where the retained shortcut is L=(x∨y∨b)L=(x\vee y\vee b). Under the decision prefix x=0,y=0x=0,y=0, first-UIP work is measured by the number of resolution pivots.

CRD-SAT-10a · Lemma · interaction-depth bound

Strict width bounds the first possible unit propagation

If every clause in a strict rr-CNF has rr distinct literals, then every consistent seed assigning fewer than r−1r-1 variables has trivial unit-propagation closure: no clause can yet be unit or false.

Result
Proved for strict finite r-CNF databases
Proof
After fewer than r−1r-1 seed assignments, every unsatisfied strict rr-clause retains at least two unset literals. Therefore no unit clause or falsified clause exists from which propagation or conflict could begin.
Scope
Shorter clauses, repeated literals, or auxiliary clauses can make propagation begin earlier.

Sources and detailed status →

CRD-SAT-10b · Theorem · exact separating example

A smallest second-order branching separation

For D=(x∨¬z∨¬p)∧(y∨¬z∨p)D=(x\vee\neg z\vee\neg p)\wedge(y\vee\neg z\vee p) and D+=D∧(x∨y∨¬z)D^+=D\wedge(x\vee y\vee\neg z), the databases are semantically equivalent and have the same singleton unit-propagation signature, yet fixed false-first DPLL in the order x<y<z<px<y<z<p uses three decisions on DD and two on D+D^+, with no conflicts.

Result
Proved for the displayed databases and fixed DPLL policy
Proof
Resolution proves semantic equivalence. By CRD-SAT-10a, both strict-3CNFs have trivial singleton closure. Under x=y=0x=y=0, the base reduces to (¬z∨¬p)∧(¬z∨p)(\neg z\vee\neg p)\wedge(\neg z\vee p) and stalls, whereas the resolvent becomes the unit ¬z\neg z. The fixed traces therefore have costs (3,0)(3,0) and (2,0)(2,0).
Scope
Choosing zz first and trying false erases the decision gap.

Sources and detailed status →

CRD-SAT-10c · Proposition · analytic minimality

Four variables and two clauses are minimal

A satisfiable strict-3CNF needs at least four variables and at least two source clauses to entail a distinct strict width-three addition; the databases in CRD-SAT-10b attain both lower bounds.

Result
Proved for distinct entailed strict-3 clauses
Proof
On three variables, each strict 3-clause excludes exactly one complete assignment, so entailing a missing strict 3-clause requires already containing the unique clause that excludes its falsifying assignment. A single clause entails another clause exactly by literal-set inclusion; equal widths then force equality. Thus four variables and two source clauses are necessary, and CRD-SAT-10b supplies them.
Scope
The claim does not cover shorter learned clauses, unsatisfiable databases, weakening, or other proof systems.

Sources and detailed status →

CRD-SAT-11a · Theorem · sharp parameterized family

Clause width gives a sharp propagation depth

For every r≥3r\ge3, there are connected, semantically equivalent strict-rr-CNF databases DrD_r and Dr+D_r^+ whose unit-propagation signatures agree through seed size r−2r-2 and first differ at seed size r−1r-1. The added clause is a pure resolvent and a reverse-unit-propagating consequence.

Result
Proved for every clause width r at least three
Proof
Resolving the two parents on pp gives the addition, hence semantic equivalence. CRD-SAT-10a gives agreement through depth r−2r-2. The seed x=y=z1=⋯=zr−3=0x=y=z_1=\cdots=z_{r-3}=0 has size r−1r-1: the parents reduce to (¬zr−2∨¬p)∧(¬zr−2∨p)(\neg z_{r-2}\vee\neg p)\wedge(\neg z_{r-2}\vee p) and stall, while the resolvent propagates zr−2=0z_{r-2}=0. Negating the resolvent makes the parents propagate opposite values of pp, establishing the RUP witness.
Scope
The growing interaction depth is carried by growing clause width.

Sources and detailed status →

CRD-SAT-11b · Theorem · exact decision law

The retained resolvent saves one fixed-policy decision

Under false-first DPLL order x<y<z1<⋯<zr−2<px<y<z_1<\cdots<z_{r-2}<p, exhaustive unit propagation, and stopping when every stored clause is satisfied, DrD_r uses rr decisions and Dr+D_r^+ uses r−1r-1, with no conflicts on either successful trace.

Result
Proved for the stated family and fixed DPLL interface
Proof
The base solver decides false for x,y,z1,…,zr−3x,y,z_1,\ldots,z_{r-3} and must also decide zr−2=0z_{r-2}=0, totaling rr. In the augmented database, the retained resolvent becomes unit after the first r−1r-1 decisions and propagates that last value. Both traces then satisfy every stored clause without conflict.
Scope
Choosing zr−2z_{r-2} earlier can erase the saving.

Sources and detailed status →

CRD-SAT-11c · Corollary · fixed-depth obstruction

No fixed seed depth determines this branching cost

Across unbounded clause width, no fixed finite unit-propagation seed depth determines the fixed-policy DPLL decision count: for any t≥1t\ge1, choosing r=t+2r=t+2 gives semantically equivalent databases with equal signatures through depth tt but different decision counts.

Result
Proved from the arbitrary-width family
Proof
Given tt, take r=t+2r=t+2. CRD-SAT-11a gives semantic equivalence and signature equality through r−2=tr-2=t, while CRD-SAT-11b gives decision counts rr and r−1r-1.
Scope
Unbounded width is essential to this construction.

Sources and detailed status →

CRD-SAT-12a · Theorem · exact equivalence

Absorption characterizes bounded-width UP equivalence

Let G=F∪AG=F\cup A, where every added clause has width at most ww. Equality of the complete unit-propagation signatures through seed size w−1w-1, UP-absorption of every clause in AA by FF, and equality of UP closure and conflict outcomes on every consistent seed are equivalent.

Result
Proved for arbitrary CNF bases and finite bounded-width additions
Proof
Signature equality through depth w−1w-1 handles every boundary seed and therefore implies absorption. A propagation-persistence lemma shows that consequences from a boundary seed survive every consistent extension unless a conflict appears. Hence an absorbed addition can never supply the first new unit or conflict beyond the base closure. This proves all-seed equality; restriction gives the reverse implication. The packet reports 110,397 finite configurations as corroboration.
Scope
The theorem concerns exhaustive unit-propagation closure and conflict outcomes.

Sources and detailed status →

CRD-SAT-12b · Corollary · sharp bound

The UP completeness radius w−1 is sharp

The exact unit-propagation completeness radius for additions of width at most ww is w−1w-1: depth w−1w-1 always suffices, while for every w≥3w\ge3 there are semantically equivalent pairs agreeing through depth w−2w-2 and separating at a seed of size w−1w-1.

Result
Proved from the absorption theorem and the preserved width-w family
Proof
CRD-SAT-12a gives the upper bound w−1w-1. The preserved Run 25 family has a width-ww addition that is inactive on every smaller seed and becomes unit on an explicit seed of size w−1w-1, giving the matching lower bound. Widths three through eight were rerun as finite corroboration.
Scope
The width bound applies to the added clauses, not necessarily every clause in the base.

Sources and detailed status →

CRD-SAT-12c · Corollary · trace preservation

Absorbed additions preserve a fixed DPLL trace

For a fixed variable order and polarity, exhaustive unit propagation, and stopping when every stored clause is syntactically satisfied, the equivalent conditions of CRD-SAT-12a imply that FF and F∪AF\cup A have identical complete DPLL traces: the same closures, decisions, conflicts, and stopping points.

Result
Proved for the stated fixed-policy DPLL interface
Proof
All-seed UP equality gives identical closures, conflicts, and subsequent fixed decisions. Absorption also gives semantic entailment. If a partial assignment satisfies every base clause, every total extension is a base model and therefore satisfies every added clause; an added clause cannot remain merely unset at the stopping point. The complete traces coincide.
Scope
Formula-inspecting heuristics, scans, watches, clause activity, provenance, learning, deletion, and proof cost are excluded.

Sources and detailed status →

CRD-SAT-13a · Theorem · closure equivalence

An absorbed clause preserves every unit-propagation closure

For every m≥1m\ge1, the connected strict-3CNF databases FmF_m and Gm=Fm∪{x∨y∨b}G_m=F_m\cup\{x\vee y\vee b\} are semantically equivalent and have identical unit-propagation closure and conflict outcomes on every consistent seed. The added clause is UP-absorbed and has the displayed mm-step pure-resolution derivation.

Result
Proved in the stated connected strict-3CNF family
Proof
The three boundary assignments for LL are handled by forward or backward propagation along the displayed chains. The earlier absorption theorem then gives equality of every UP closure. Resolving C0C_0 successively with the XiX_i chain produces LL in exactly mm displayed steps. The packet also reports 88,533 all-seed instances, 177,066 paired closures, 16,368 truth rows, and 2,080 derivation steps as finite corroboration.
Scope
The displayed mm-step derivation is not claimed globally shortest.

Sources and detailed status →

CRD-SAT-13b · Theorem · exact resource separation

Reason-path compression changes fixed first-UIP work

Under the fixed earliest-clause propagation policy, immutable first reasons, decisions x=0x=0 then y=0y=0, and latest-trail first-UIP analysis, FmF_m requires exactly m+1m+1 resolution pivots while GmG_m requires one. Both traces learn x∨yx\vee y, make two decisions, and encounter one conflict.

Result
Proved for the stated deterministic solver interface
Proof
In FmF_m, the reason chain is C0,X1,…,XmC_0,X_1,\ldots,X_m, so resolving the conflict clause eliminates b,am,…,a1b,a_m,\ldots,a_1 in m+1m+1 pivots. In GmG_m, the retained clause LL supplies bb directly and resolves with the conflict clause in one pivot. The packet reports 128 deterministic traces through m=64m=64.
Scope
This is not a heuristic-independent CDCL runtime lower bound.

Sources and detailed status →

CRD-SAT-F13 · Counterexample · representation obstruction

Unit-propagation closure does not determine conflict-analysis work

Semantic equality together with equality of complete all-seed unit-propagation closure does not determine first-UIP resolution work for a reason-sensitive solver interface.

Result
Refuted by the CRD-SAT-13 family
Proof
CRD-SAT-13a proves that FmF_m and GmG_m have identical semantics and every UP closure. CRD-SAT-13b gives exact costs m+1m+1 and one. The gap grows with mm, so no function of semantics plus the closure operator alone can recover this resource.
Scope
The refutation is relative to a declared provenance-sensitive observer.

Sources and detailed status →

CRD-SAT-14a · Theorem · all-schedule classification

The all-schedule first-UIP cost spectrum is exact

For every legal sequential unit-propagation schedule, reason choice, and detected conflict under x=y=0x=y=0, the first-UIP cost spectrum of FmF_m is {m+1}\{m+1\}, while the spectrum of GmG_m is {1,m+1}\{1,m+1\}. Every trace learns x∨yx\vee y.

Result
Proved for the stated sequential-UP/first-UIP model
Proof
In FmF_m, true assignments form a prefix and false assignments a suffix of the residual path. When the frontiers meet, first-UIP must eliminate all m+1m+1 path variables. In GmG_m, choosing either endpoint unit early yields a one-pivot conflict, while postponing both added endpoint opportunities reproduces the long m+1m+1-pivot path. The packet exhaustively generated 176,800 traces through m=8m=8.
Scope
The theorem is not about unrestricted resolution proof size.

Sources and detailed status →

CRD-SAT-14b · Corollary · exact extremal costs

The best legal first-UIP gap is exactly m

The priority-independent minimum first-UIP costs are cmin⁡(Fm)=m+1c_{\min}(F_m)=m+1 and cmin⁡(Gm)=1c_{\min}(G_m)=1, giving exact gap mm; the maximum costs are equal: cmax⁡(Fm)=cmax⁡(Gm)=m+1c_{\max}(F_m)=c_{\max}(G_m)=m+1.

Result
Proved from the all-schedule classification
Proof
Taking minima and maxima of the two exact spectra in CRD-SAT-14a gives the formulas immediately.
Scope
A smaller minimum does not guarantee that an online solver realizes it.

Sources and detailed status →

CRD-SAT-14c · Proposition · exact width spectrum

All legal base analyses have width three or four

Across all legal reason choices, F1F_1 has maximum analysis width three; for m≥2m\ge2, the attainable maximum widths for FmF_m are exactly {3,4}\{3,4\}; every trace of GmG_m has maximum width three.

Result
Proved in the stated all-schedule model
Proof
Every intermediate resolvent contains at most the guards x,yx,y and two adjacent path literals, giving width at most four. A mixed-guard reason and conflict at m=2m=2 attains width four. The shortcut in GmG_m keeps all legal traces within width three. The all-trace checker corroborates the spectrum through m=8m=8.
Scope
This is not a general resolution-width separation.

Sources and detailed status →

CRD-SAT-F14 · Counterexample · scheduling obstruction

An available shortcut need not be used

Retaining the absorbed shortcut LL does not guarantee that every legal propagation and reason schedule realizes the one-pivot conflict analysis.

Result
Refuted by a legal long trace in the augmented family
Proof
A legal schedule can postpone both endpoint clauses, propagate v0,v1,…,vmv_0,v_1,\ldots,v_m along the original forward chain, and then select the old conflict. This produces the same m+1m+1-pivot analysis available in FmF_m, even though one-pivot traces also exist.
Scope
The result does not say that practical heuristics usually ignore the shortcut.

Sources and detailed status →