The two-path separated move

A repair square is non-localized when its two re-paired edges lie on genuinely distinct boundary chains. This file establishes the chain geometry of such a square and the count invariance it gives:

• EdgeSubset.not_periodic_of_onBoundaryChain — flags on a boundary chain are not periodic;
• EdgeSubset.onBoundaryChain_disjoint — genuinely distinct boundary chains share no flag (chain rigidity);
• EdgeSubset.square_hit — a chain carrying one matched edge of the square crosses it exactly once, by a pairing argument;
• EdgeSubset.openCircuitCount_repair_of_not_localized — count invariance: a non-localized square leaves the open circuit count unchanged, the repaired components being still boundary chains, so periodicFlags and the periodic walk permutation are untouched.

The transform factor the move contributes to the summand is pinned in TransposeLedger.lean, on top of this count invariance.

Chain membership excludes periodicity

theorem RS.EdgeSubset.not_periodic_of_onBoundaryChain {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β f : W.Flag} (hβ : β ∈ F.boundaryFlags) (h : OnBoundaryChain κ β f) : ¬κ.PeriodicFlag f

A flag on a boundary chain is not periodic.

Distinct chains share no flag

theorem RS.EdgeSubset.onBoundaryChain_disjoint {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β β' f : W.Flag} (hβ : β ∈ F.boundaryFlags) (hβ' : β' ∈ F.boundaryFlags) (hne : β' ≠ β) (hne' : β' ≠ κ.pathMatch β hβ) (h : OnBoundaryChain κ β f) (h' : OnBoundaryChain κ β' f) : False

Chain disjointness: two genuinely distinct boundary chains (the second end not among the first chain's two ends) share no flag, on either side of an edge.

The square hit on a chain

theorem RS.EdgeSubset.square_hit {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {X Y β : W.Flag} (hβ : β ∈ F.boundaryFlags) (hXi : X ∈ F.internalFlags) (hXY : κ.match_ X = Y) {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) (hon : OnBoundaryChain κ β X) : ∃ s < k, W.pairing (iterWalk κ β s) = X ∧ iterWalk κ β (s + 1) = Y ∨ W.pairing (iterWalk κ β s) = Y ∧ iterWalk κ β (s + 1) = X

A chain carrying one matched edge X ↔ Y of the square meets it as a pairing argument: at some step s < k the argument is X or Y, and the next walk flag is the other.

Repaired chains through the square

theorem RS.EdgeSubset.onBoundaryChain_repair_of_hit {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) {β : W.Flag} (hβ : β ∈ F.boundaryFlags) {k s : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hs : s < k) (havoid : ∀ j < s, W.pairing (iterWalk κ β j) ≠ a ∧ W.pairing (iterWalk κ β j) ≠ b ∧ W.pairing (iterWalk κ β j) ≠ c ∧ W.pairing (iterWalk κ β j) ≠ d) : OnBoundaryChain (κ.repair a b c d v hsq) β (W.pairing (iterWalk κ β s))

The repaired chain from β reaches the first square argument: if the arguments before step s avoid the square, the argument at step s lies on the repaired chain of β.

theorem RS.EdgeSubset.not_periodic_repair_of_tail {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) {β : W.Flag} {k s : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) (hs : s < k) (hav : ∀ (j : ℕ), s < j → j < k → W.pairing (iterWalk κ β j) ≠ a ∧ W.pairing (iterWalk κ β j) ≠ b ∧ W.pairing (iterWalk κ β j) ≠ c ∧ W.pairing (iterWalk κ β j) ≠ d) : ¬(κ.repair a b c d v hsq).PeriodicFlag (iterWalk κ β (s + 1))

The walk-side square flag on a chain is not periodic in the repaired system: the repaired walk from it follows the old chain tail to the boundary.

theorem RS.EdgeSubset.chain_side_not_periodic_repair {α : 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₂) : ¬(κ.repair a b c d v hsq).PeriodicFlag X ∧ ¬(κ.repair a b c d v hsq).PeriodicFlag Y

One chain side of a two-chain square: its two square flags are non-periodic in the repaired system. Stated for a matched pair X ↔ Y on the chain of β, with the other two square flags on the genuinely distinct chain of βo; hperm identifies the four square flags with {X, Y, Z₁, Z₂}.

theorem RS.EdgeSubset.periodicFlag_repair_iff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (hna : ¬κ.PeriodicFlag a) (hnb : ¬κ.PeriodicFlag b) (hnc : ¬κ.PeriodicFlag c) (hnd : ¬κ.PeriodicFlag d) (hna' : ¬(κ.repair a b c d v hsq).PeriodicFlag a) (hnb' : ¬(κ.repair a b c d v hsq).PeriodicFlag b) (hnc' : ¬(κ.repair a b c d v hsq).PeriodicFlag c) (hnd' : ¬(κ.repair a b c d v hsq).PeriodicFlag d) (f : W.Flag) : (κ.repair a b c d v hsq).PeriodicFlag f ↔ κ.PeriodicFlag f

Periodicity transfer across a repair whose four flags are non-periodic on both sides.

theorem RS.EdgeSubset.openCircuitCount_repair_of_not_localized {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (hnl : ¬SquareLocalized κ a b c d) : (κ.repair a b c d v hsq).openCircuitCount = κ.openCircuitCount

Count invariance for two-chain squares: a non-localized square leaves the open circuit count unchanged — both repaired components are still boundary-terminated chains, so the periodic flags and the periodic walk permutation are untouched.