Surgery on timestamped edge-CSP DAGs #
This formalizes Lemmas 35 and 37, Corollary 36's graph argument, and Lemma 43 of [KKR18], arXiv:1602.03124v6, printed pp. 16–20. The four-coordinate exchange consequences are applied to actual positional tuples to prove preservation of both local feasibility and the full no-shortcut invariant. Common local parity may be odd.
delete_earliest_pair has the source's exact leaf and degree hypotheses and identifies the
removed arcs. removeRootCopy and removeCopy prove stronger deletion variants that retain
isolated supported nodes as appropriate. reroot_earliest retains every unselected outgoing
child and proves the changed topological order, moving the selected variable before all others.
valid_flip_of_pairedCopies proves a stronger form of Corollary 36 by induction on constraint
copies: every copy has precisely two incident arcs, at least one incoming. The path-to-Walk
bridges are in DAGPaths. Nothing excludes revisits of an original constraint at different times.
flip_walk_of_no_prefix_extension is Lemma 43 with actual Walk.take/snoc hypotheses.
Its proof is an alternative to the paper's temporary earlier timestamp: direct exchange gives
external_pair, which is iterated over all variable-ended prefixes. Thus no assumption that a
smaller natural timestamp exists is needed, including when a current timestamp is zero.
The local surgery arguments in fact hold for arbitrary occurrence-indexed CSP lists; an
EdgeInstance identifies this positional extension with the source's no-repeat edge model.
No surgery conclusion, path validity, comparison labeling, forest construction or solver is
included among the six invariant assumptions. Algorithm 1 and its Lemma 34 are separate work.
Main results #
IsFDAG.delete_earliest_pair: Lemma 35, including exact removal of the two displayed arcs.IsFDAG.reroot_earliest: Lemma 37, retaining other children.IsFDAG.valid_flip_of_pairedCopies: the graph form of Corollary 36.IsFDAG.flip_walk_of_no_prefix_extension: Lemma 43 on actual positional walks.
Cancelling pairs are symmetric, including equal occurrences.
Two pair moves sharing their middle occurrence cancel that occurrence.
Feasibility of a two-port move is exactly local feasibility at its positional constraint.
The substantive property-(5) transfer in KKR Lemmas 35 and 37. The two forbidden old-incoming cross-pairs force the four-coordinate move.
The substantive no-shortcut transfer in KKR Lemmas 35 and 37. Exchange toward the feasible base would produce one of three forbidden pairs.
Different timestamps cannot reuse an original incidence.
Opposite orientations cannot reuse an original incidence.
Local feasibility at a later copy survives the earliest two-port move. All original-constraint revisits are retained; the four-coordinate exchange handles them.
The no-shortcut prohibition between later copies survives the earliest two-port move.
A different copy is strictly later than a minimum copy: timestamps are globally unique.
Delete the old root arc and reverse one selected child arc, retaining all other children.
Instances For
Delete a variable root and a constraint copy, retaining all other supported nodes.
Instances For
Earliest-copy deletion preserves the full f-DAG invariant after its two-port move. This stronger form deletes every incident arc at the selected root and copy; the degree hypotheses in Lemma 35 identify these with precisely its two displayed arcs.
Lemma 35, KKR v6, printed pp. 16–17: flip u C v, remove u,C^s and exactly
the two displayed arcs. Both local feasibility and no shortcuts are proved by even exchange.
Lemma 37, KKR v6, printed pp. 18–19: an earliest copy with a single incoming root arc can be rerooted at any outgoing child. Other outgoing children are retained.
Delete a constraint copy, retaining its variable endpoints as isolated nodes if necessary.
Instances For
The earliest-copy exchange argument also applies to two incoming ports. This covers the terminal meeting copy in Corollary 36(1).
Each supported constraint copy has precisely two incident arcs, at least one incoming. This purely graph-theoretic condition includes directed paths and two paths meeting at a copy. It places no restriction on revisits of an original constraint at different timestamps.
Instances For
Removing one copy preserves the two-arc condition at every remaining copy.
Flip every used original incidence of a DAG, independently of isolated node support.
Instances For
Removing a two-arc constraint copy factors the full DAG flip into its first pair move and the remaining incidence flip. Original incidences are not counted twice.
Corollary 36 in a stronger graph form: if every copy has two incident arcs with at least one incoming, flipping the entire f-DAG is valid. Directed variable-to-variable paths and two otherwise-disjoint directed paths meeting at a constraint copy are special cases. The induction removes copies, and therefore permits repeated original constraints.
A feasible external step preserves the same DAG when its first port cannot exchange with any used port. This is the direct local-exchange argument for Lemma 43: unlike the source's proof, it needs no new minimum timestamp, and therefore also handles existing timestamp zero.
Lemma 43, KKR v6, printed p. 20, with explicit occurrence-level avoidance and
Walk.take/Walk.snoc extension conditions. Every used DAG arc is tested regardless of
orientation. Direct four-coordinate exchange replaces the source proof's temporary earlier
copy, so timestamp zero needs neither a nonexistent smaller natural nor a reindexing premise.