The pairing-preserving step ledger

Discharges the single-repair disjunct of MatchPreservingLedger: every pairing-preserving repair step (MatchPreservingStep) carries a path-canonical orientation to a path-canonical orientation on the repaired side with the same pathSign-weighted canonical summand.

Main results

• EdgeSubset.squareLocalized_of_pathMatch_eq — two-path exclusion: a repair square that preserves every path matching is localized. A non-localized square has its two re-paired edges on genuinely distinct boundary chains (twoChains_of_not_localized); after the repair, the a-flag and the c-flag land on the repaired chains of the two old chains' ends (hit_membership, from the unique square crossing of each chain), and a, c are matched by the repaired system, so the two repaired chains share a flag — contradicting chain disjointness when the pairing is preserved.
• EdgeSubset.walkReach_or_walkReach_of_chain — on one boundary chain, two coherently oriented internal flags see one another along the walk (orientation rigidity kills the mixed walk-side / pairing-side cases; positions order the same-side cases).
• Canonicality transfer: EdgeSubset.pathCanonical_of_entry_eq plus the per-case entry computations — transportRepair keeps isOut verbatim; flipOrbit is supported on a periodic orbit and entry flags are non-periodic (entry_not_periodic); the reversal segment of segFlip is pairing-closed and internal, so it carries no entry flag (entry_notMem_repairSegment).
• EdgeSubset.stepLedger_single — the single-step ledger: the MatchPreservingStep disjunct of the per-move interface, fully discharged from the parity theorems (separatedCountParity, nonSeparatedSegmentParity, nonSeparatedMergeParity).
• EdgeSubset.PairedLedger — the named input: the PairedStep disjunct (two consecutive repairs with net pairing preservation); a theorem downstream (pairedLedger, PairedAssembly.lean).
• EdgeSubset.matchPreservingLedger_of — the dispatch: MatchPreservingLedger from PairedLedger and the single-step theorem.

Why a pair is one move

PairedLedger carries the content. Each half of a PairedStep may be a two-path repair that changes the boundary pairing, where the per-repair vertex ledger negates the summand and re-pairs the boundary colour blocks; across the pair the values net-agree via a re-pairing (colour-swap) identity for the vertex functional on the re-routed strand. TwoPathStep supplies the count invariance the halves need (openCircuitCount_repair_of_not_localized). A single two-path repair does not carry the ledger on its own, which is why a pair is treated as one composite move.

Entry flags: non-periodicity and segment avoidance

theorem RS.EdgeSubset.entry_not_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {i : α} (hb : W.boundaryFlag i ∈ F.boundaryFlags) (hint : W.pairing (W.boundaryFlag i) ∈ F.internalFlags) : ¬κ.PeriodicFlag (W.pairing (W.boundaryFlag i))

The entry edge of a participating boundary flag is not periodic: it is the step-0 pairing argument of a boundary-terminated chain.

theorem RS.EdgeSubset.entry_notMem_repairSegment {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {S : Finset W.Flag} (hseg : RepairSegment κ a b c d S) (i : α) : W.pairing (W.boundaryFlag i) ∉ S

A reversal segment carries no entry flag: the segment is pairing-closed and internal, while the pairing of an entry flag is a boundary flag.

theorem RS.EdgeSubset.pathCanonical_of_entry_eq {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {o : κ.Orientation} {o' : κ'.Orientation} (hpm : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), κ'.pathMatch δ hδ = κ.pathMatch δ hδ) (hentry : ∀ (i : α), W.boundaryFlag i ∈ F.boundaryFlags → W.pairing (W.boundaryFlag i) ∈ F.internalFlags → o'.isOut (W.pairing (W.boundaryFlag i)) = o.isOut (W.pairing (W.boundaryFlag i))) (hc : PathCanonical o) : PathCanonical o'

Canonicality transfer: an orientation of a system with the same path matching, agreeing with a path-canonical orientation on every entry flag, is path-canonical.

Two-path exclusion

theorem RS.EdgeSubset.onBoundaryChain_of_exit {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {f : W.Flag} (hf : f ∈ F.internalFlags) {m : ℕ} (hcont : ∀ j < m, W.pairing (iterWalk κ f j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ f m) ∈ F.boundaryFlags) : OnBoundaryChain κ (W.pairing (iterWalk κ f m)) f

Chain membership from the exit end of a terminating forward walk.

theorem RS.EdgeSubset.hit_membership {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) {β βo X Y Z₁ Z₂ : W.Flag} (hβ : β ∈ F.boundaryFlags) (hβo : βo ∈ F.boundaryFlags) (hne1 : β ≠ βo) (hne2 : β ≠ κ.pathMatch βo hβo) (hXi : X ∈ F.internalFlags) (hXY : κ.match_ X = Y) (honX : OnBoundaryChain κ β X) (honZ₁ : OnBoundaryChain κ βo Z₁) (honZ₂ : OnBoundaryChain κ βo Z₂) (hperm : ∀ (g : W.Flag), g = a ∨ g = b ∨ g = c ∨ g = d ↔ g = X ∨ g = Y ∨ g = Z₁ ∨ g = Z₂) : OnBoundaryChain (κ.repair a b c d v hsq) β X ∨ OnBoundaryChain (κ.repair a b c d v hsq) (κ.pathMatch β hβ) X

The hit membership: on a two-chain square, the X-flag of the matched pair carried by β's chain lies, after the repair, on the repaired chain of β or of β's far end.

theorem RS.EdgeSubset.squareLocalized_of_pathMatch_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (hpres : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) : SquareLocalized κ a b c d

Two-path exclusion: a repair square that preserves every path matching is localized. On a non-localized square the repaired a-flag and its repaired match c land on the repaired chains of two genuinely distinct pairs of ends, which share no flag.

Same-chain reach for coherent orientations

theorem RS.EdgeSubset.walkReach_or_walkReach_of_chain {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β f g : W.Flag} (hβ : β ∈ F.boundaryFlags) (o : κ.Orientation) (hsame : o.isOut f = o.isOut g) (hfg : f ≠ g) (hf : f ∈ F.internalFlags) (hg : g ∈ F.internalFlags) (honf : OnBoundaryChain κ β f) (hong : OnBoundaryChain κ β g) : WalkReach κ f g ∨ WalkReach κ g f

Same-chain reach: two distinct coherently oriented internal flags on one boundary chain see one another along the walk. Orientation rigidity (walk-side flags carry the negated seed, pairing-side flags the seed) excludes the mixed cases; on a common side the walk runs from the earlier to the later position.

The single-step ledger

theorem RS.EdgeSubset.stepLedger_single {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (κ₁ κ₂ : F.RelTransitionSystem) (hstep : MatchPreservingStep κ₁ κ₂) (o₁ : κ₁.Orientation) (hc₁ : PathCanonical o₁) : ∃ (o₂ : κ₂.Orientation), PathCanonical o₂ ∧ pathSign κ₂ * F.throughSummand hM st hbnd o₂ κ₂.openCircuitCount = pathSign κ₁ * F.throughSummand hM st hbnd o₁ κ₁.openCircuitCount

The single-step ledger (the MatchPreservingStep disjunct of MatchPreservingLedger, fully discharged): a pairing-preserving repair step carries a path-canonical orientation to a path-canonical orientation with the same pathSign-weighted canonical summand. The square is localized by the two-path exclusion; the separated case transports the orientation verbatim, the non-separated case dispatches into the segment-reversal, swapped-segment, orbit-flip, and swapped-orbit-flip ledgers, whose count parities are separatedCountParity, nonSeparatedSegmentParity, and nonSeparatedMergeParity; in every case the produced orientation agrees with the input on all entry flags, so canonicality transfers.

The paired step and the dispatch

def RS.EdgeSubset.PairedLedger : Prop

The paired two-path move (a theorem downstream, pairedLedger): a PairedStep — two consecutive repairs κ₁ → κmid → κ₂ whose net effect preserves the boundary pairing — carries a path-canonical orientation to a path-canonical orientation with the same pathSign-weighted canonical summand.

The pair is the unit, not the half. In the double-crossing configuration each half is a two-path repair that changes the pairing, so stepLedger_single does not apply to it: the per-half vertex ledger negates the summand while re-pairing the boundary colour blocks across the two chains. Across the pair the second repair undoes the re-routing of the first, the composite walk change is supported on the two crossing squares, and the two vertex negations cancel against the net chord-parity change. Proved in PairedAssembly.lean.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.EdgeSubset.matchPreservingLedger_of (HPaired : PairedLedger) : MatchPreservingLedger

The per-move ledger from the paired step: the MatchPreservingStep disjunct is discharged by stepLedger_single; the PairedStep disjunct is the named input.