The non-separated repair move: the flipped-segment ledger

The non-separated case of the per-move path ledger: a repair square whose two re-paired edges are traversed coherently (o.isOut c = o.isOut a). The repaired walk reverses the segment between the two match-pairs, and the transported orientation must flip isOut exactly on the reversed segment.

Main results

• EdgeSubset.RepairSegment — the abstract reversal-segment package: a pairing-closed set of internal flags containing b and c, avoiding a and d, and closed under the matching except at the two cut points b, c.
• EdgeSubset.RelTransitionSystem.Orientation.segFlip — the flipped-segment orientation of the repaired system (valid exactly because the flip meets the non-separated condition at the cuts).
• EdgeSubset.throughSummand_segFlip — the flipped-segment ledger: the constrained summand over the repaired system with the flipped-segment orientation equals the old summand at every fixed circuit exponent (total +1: the vertex transposition's −1 cancels against the cut-block ∂-sign, and the reversed segment telescopes to ∏_{f ∈ S} sign(φ f) = 1).
• EdgeSubset.WalkReach / EdgeSubset.exists_repairSegment — the same-component configuration (the walk from c reaches a) and the construction of the reversal segment from it; covers both the same-circuit and the same-path (chain) reversal sub-cases.
• EdgeSubset.squareLocalized_of_walkReach — a same-component square is localized, so the path sign is untouched (committed pathMatch_repair_of_localized).
• EdgeSubset.RepairSquare.swap and repair_swap_matchEq — the square with the roles of the two re-paired edges exchanged produces the same repaired system.

The two counting inputs

The ledger needs the circuit-count parity of the move, which is a separate, orbit-counting question. It is named here and proved in the parity files:

• NonSeparatedSegmentParity — a same-component square preserves the circuit-count parity (the segment reversal maps the two traversal orbits of the affected component to two orbits, Δ = 0);
• NonSeparatedMergeParity — a square whose c-edge lies on a circuit not carrying a flips the count parity (the splice merges the circuit into a's component, Δ = −1).

The abstract reversal-segment package

structure RS.EdgeSubset.RepairSegment {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (a b c d : W.Flag) (S : Finset W.Flag) : Prop

The reversal-segment data for a repair square: a pairing-closed set of internal flags containing the two cut flags b, c, avoiding a, d, and closed under the matching away from the cuts. The repaired matching sends the cuts outside (b ↦ d, c ↦ a), so the set is exactly the flag support of the walk segment the repair reverses.

• hbS : b ∈ S
• hcS : c ∈ S
• haS : a ∉ S
• hdS : d ∉ S
• int_of_mem (f : W.Flag) : f ∈ S → f ∈ F.internalFlags
• pairing_mem (f : W.Flag) : f ∈ S → W.pairing f ∈ S
• match_mem (f : W.Flag) : f ∈ S → f ≠ b → f ≠ c → κ.match_ f ∈ S

theorem RS.EdgeSubset.RepairSegment.pairing_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {S : Finset W.Flag} (h : RepairSegment κ a b c d S) {f : W.Flag} (hf : f ∉ S) : W.pairing f ∉ S

The complement is closed under the pairing.

theorem RS.EdgeSubset.RepairSegment.match_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} {S : Finset W.Flag} (h : RepairSegment κ a b c d S) (hsq : RepairSquare κ a b c d v) {f : W.Flag} (hf : f ∈ F.internalFlags) (hfS : f ∉ S) (h1 : f ≠ a) (h4 : f ≠ d) : κ.match_ f ∉ S

The complement is closed under the matching away from a, d.

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

Boundary flags are never on the segment.

The flipped-segment orientation of the repaired system

noncomputable def RS.EdgeSubset.RelTransitionSystem.Orientation.segFlip {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} {S : Finset W.Flag} (hsq : RepairSquare κ a b c d v) (o : κ.Orientation) (hsame : o.isOut c = o.isOut a) (hseg : RepairSegment κ a b c d S) : (κ.repair a b c d v hsq).Orientation

The flipped-segment orientation: flip isOut exactly on the reversal segment. The result is an orientation of the repaired system: at the cuts the new matches a ↔ c, b ↔ d flip orientation exactly because the move is non-separated (isOut c = isOut a).

Equations

• RS.EdgeSubset.RelTransitionSystem.Orientation.segFlip hsq o hsame hseg = { isOut := fun (f : W.Flag) => if f ∈ S then !o.isOut f else o.isOut f, match_flip := ⋯, pairing_flip := ⋯ }

theorem RS.EdgeSubset.segFlip_isOut_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} {S : Finset W.Flag} (hsq : RepairSquare κ a b c d v) (o : κ.Orientation) (hsame : o.isOut c = o.isOut a) (hseg : RepairSegment κ a b c d S) {f : W.Flag} (hf : f ∉ S) : (RelTransitionSystem.Orientation.segFlip hsq o hsame hseg).isOut f = o.isOut f

Off the segment it is unchanged.

The ∂-flip of the colouring on the segment

noncomputable def RS.EdgeSubset.segFlipColouring {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} (hSpair : ∀ f ∈ S, W.pairing f ∈ S) {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) : F.CoreOddColouring ℓ

The ∂-flip of a core odd colouring on the segment edges.

Equations

• RS.EdgeSubset.segFlipColouring hSpair φ = ⟨fun (g : ↥F.coreFlags) => if ↑g ∈ S then RS.oddPartner ℓ (↑φ g) else ↑φ g, ⋯⟩

theorem RS.EdgeSubset.segFlipColouring_val {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} (hSpair : ∀ f ∈ S, W.pairing f ∈ S) {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (g : ↥F.coreFlags) : ↑(segFlipColouring hSpair φ) g = if ↑g ∈ S then oddPartner ℓ (↑φ g) else ↑φ g

The segment-flipped colouring, unfolded.

theorem RS.EdgeSubset.segFlipColouring_involutive {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} (hSpair : ∀ f ∈ S, W.pairing f ∈ S) {ℓ : ℕ} : Function.Involutive (segFlipColouring hSpair)

It is an involution, so it is a bijection of the colouring sum.

theorem RS.EdgeSubset.coreOddBoundaryMatch_segFlipColouring {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} {k ℓ : ℕ} (st : GenBoundaryState k ℓ α) (hSpair : ∀ f ∈ S, W.pairing f ∈ S) (hSb : ∀ (i : α), W.boundaryFlag i ∉ S) (φ : F.CoreOddColouring ℓ) : F.coreOddBoundaryMatch st (segFlipColouring hSpair φ) ↔ F.coreOddBoundaryMatch st φ

The ∂-flip preserves the odd boundary constraint when the segment carries no boundary flags.

The flipped-segment ledger

The pairing sign as a total function

Vertex-local in-sets

noncomputable def RS.EdgeSubset.keepS {α : Type} {W : Fragment α} {F : EdgeSubset W} (S : Finset W.Flag) {κ₀ : F.RelTransitionSystem} (o₀ : κ₀.Orientation) (vv : W.Vertex) : Finset W.Flag

The in-flags at a vertex whose colours the flip on S leaves alone.

Equations

• RS.EdgeSubset.keepS S o₀ vv = {g ∈ RS.relInSetAt o₀ vv | g ∉ S}

noncomputable def RS.EdgeSubset.flipS {α : Type} {W : Fragment α} {F : EdgeSubset W} (S : Finset W.Flag) {κ₀ : F.RelTransitionSystem} (o₀ : κ₀.Orientation) (vv : W.Vertex) : Finset W.Flag

The in-flags at a vertex whose colours the flip on S reverses.

Equations

• RS.EdgeSubset.flipS S o₀ vv = {g ∈ RS.relInSetAt o₀ vv | g ∈ S}

theorem RS.EdgeSubset.mem_keepS {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} {κ₀ : F.RelTransitionSystem} {o₀ : κ₀.Orientation} {vv : W.Vertex} {g : W.Flag} : g ∈ keepS S o₀ vv ↔ g ∈ relInSetAt o₀ vv ∧ g ∉ S

Membership in the kept part of a vertex's in-set.

theorem RS.EdgeSubset.mem_flipS {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} {κ₀ : F.RelTransitionSystem} {o₀ : κ₀.Orientation} {vv : W.Vertex} {g : W.Flag} : g ∈ flipS S o₀ vv ↔ g ∈ relInSetAt o₀ vv ∧ g ∈ S

Membership in the flipped part of a vertex's in-set.

theorem RS.EdgeSubset.relInSetAt_val_split {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} {κ₀ : F.RelTransitionSystem} (o₀ : κ₀.Orientation) (vv : W.Vertex) : (relInSetAt o₀ vv).val = (keepS S o₀ vv).val + (flipS S o₀ vv).val

The flip on S splits a vertex's in-set into the kept and the flipped part.

theorem RS.EdgeSubset.prod_relInSetAt_split {α : Type} {W : Fragment α} {F : EdgeSubset W} {S : Finset W.Flag} {M : Type u_1} [CommMonoid M] {κ₀ : F.RelTransitionSystem} (o₀ : κ₀.Orientation) (vv : W.Vertex) (f : W.Flag → M) : ∏ g ∈ relInSetAt o₀ vv, f g = (∏ g ∈ flipS S o₀ vv, f g) * ∏ g ∈ keepS S o₀ vv, f g

A product over a vertex's in-set splits along that partition.

The pair blocks

The parametric vertex data of the move

theorem RS.EdgeSubset.throughSummand_segFlip {α : Type} {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} {S : Finset W.Flag} [LinearOrder α] (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (hsq : RepairSquare κ a b c d v) (o : κ.Orientation) (hsame : o.isOut c = o.isOut a) (hseg : RepairSegment κ a b c d S) (n : ℕ) : F.throughSummand hM st hbnd (RelTransitionSystem.Orientation.segFlip hsq o hsame hseg) n = F.throughSummand hM st hbnd o n

The flipped-segment ledger: the constrained summand of the repaired system over the flipped-segment orientation and equals the old summand at every fixed circuit exponent.

The same-component configuration and its segment

def RS.EdgeSubset.WalkReach {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (c a : W.Flag) : Prop

The walk from c reaches a with internal pairings: the same-component configuration of the non-separated move (both the same-circuit and the same-chain reversal sub-cases).

Equations

• RS.EdgeSubset.WalkReach κ c a = ∃ (m : ℕ), 1 ≤ m ∧ (∀ j < m, W.pairing (RS.EdgeSubset.iterWalk κ c j) ∈ F.internalFlags) ∧ RS.EdgeSubset.iterWalk κ c m = a

theorem RS.EdgeSubset.iterWalk_int_of_cont {α : 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) (j : ℕ) : j ≤ m → iterWalk κ f j ∈ F.internalFlags

Iterates along an internally-continuing walk are internal.

theorem RS.EdgeSubset.isOut_iterWalk_of_cont {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {f : W.Flag} (hf : f ∈ F.internalFlags) {m : ℕ} (hcont : ∀ j < m, W.pairing (iterWalk κ f j) ∈ F.internalFlags) (j : ℕ) : j ≤ m → o.isOut (iterWalk κ f j) = o.isOut f

The orientation is constant along the walk positions of an internally-continuing walk.

theorem RS.EdgeSubset.exists_repairSegment {α : 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 : κ.Orientation) (hsame : o.isOut c = o.isOut a) (hreach : WalkReach κ c a) : ∃ (S : Finset W.Flag), RepairSegment κ a b c d S

The reversal segment of a same-component non-separated square: the flags of the walk from c up to (excluding) a, on both sides of each visited edge.

Localization of the same-component square

theorem RS.EdgeSubset.onBoundaryChain_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β f : W.Flag} (h : OnBoundaryChain κ β f) : OnBoundaryChain κ β (W.pairing f)

The chain membership is closed under the pairing.

theorem RS.EdgeSubset.onBoundaryChain_iterWalk {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β f : W.Flag} (hβ : β ∈ F.boundaryFlags) (h : OnBoundaryChain κ β f) {m : ℕ} (hcont : ∀ j < m, W.pairing (iterWalk κ f j) ∈ F.internalFlags) (j : ℕ) : j ≤ m → OnBoundaryChain κ β (iterWalk κ f j)

The chain membership is closed along internally-continuing walks.

theorem RS.EdgeSubset.squareLocalized_of_walkReach {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (hreach : WalkReach κ c a) : SquareLocalized κ a b c d

A same-component square is localized: c's component either is a circuit carrying all four flags, or is the chain of a boundary flag carrying them.

theorem RS.EdgeSubset.walkReach_of_orbitFlag {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a c : W.Flag} {o : κ.Orientation} (hpc : κ.PeriodicFlag c) (hsame : o.isOut c = o.isOut a) (hac : a ≠ c) (horb : OrbitFlag κ c a) : WalkReach κ c a

On a component with an orientation, membership of a on c's periodic orbit forces the forward reach under the non-separated condition: the pairing-side (reverse) membership contradicts the orientation.

theorem RS.EdgeSubset.periodicFlag_of_orbitFlag {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {c f : W.Flag} (hpc : κ.PeriodicFlag c) (horb : OrbitFlag κ c f) : κ.PeriodicFlag f

Orbit membership on a periodic component is periodic.

The swapped square

theorem RS.EdgeSubset.RepairSquare.swap {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : RepairSquare κ c d a b v

The square with the two re-paired edges exchanged.

theorem RS.EdgeSubset.repair_swap_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : (κ.repair c d a b v ⋯).MatchEq (κ.repair a b c d v h)

The swapped square repairs to the same system.

The inputs and the dispatch

def RS.NonSeparatedSegmentParity : Prop

Input (segment count parity): a same-component square preserves the circuit-count parity — the segment reversal maps the two traversal orbits of the affected component onto two orbits of the same sizes (Δ = 0 on circuits; chains carry no periodic flags). Proved in OrbitParities.lean.

Equations

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

def RS.NonSeparatedMergeParity : Prop

Input (merge count parity): a square whose c-edge lies on a circuit not carrying a flips the count parity — the splice merges the circuit into a's component (Δ = −1). Proved in OrbitParities.lean.

Equations

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