The path ledger for the repair move

The corrected per-move target for Proposition 3: the path-sign-weighted constrained summand pathSign κ * throughSummand … o κ.openCircuitCount under one elementary repair move. The RepairInvariance ledger handles the summand factor; this file supplies the pathSign factor and the case analysis that controls it.

Main results

• third_chord_reparity — the third-chord parity lemma (chord combinatorics, self-contained): re-pairing four fixed points of a linear order into chords in any two ways changes the number of crossings with any third chord by an even amount.
• chain_meet — chain rigidity: two boundary-terminated chains sharing a walk flag have the same starting boundary flag (walks are forward- and backward-deterministic).
• pathMatch_repair_of_avoid — a chain whose pairing arguments avoid the four flags of the square walks identically in the repaired system.
• periodicFlag_pairing / periodicFlag_match — the periodic flags are closed under the edge pairing and the matching.
• pathMatch_repair_of_periodic — case 1: a square on periodic (circuit) components leaves every path matching unchanged.
• pathMatch_repair_of_chainLocal — cases 2–3: a square whose four flags are each periodic or on the chain of one boundary flag β leaves every path matching unchanged — untouched chains avoid the square by rigidity, and the two ends of β's chain must re-pair with each other because pathMatch remains a fixed-point-free involution (pathMatch_ne_self).
• pathSign_congr / pathSign_matchEq — the crossing sign only depends on the path matching, so it is unchanged in cases 1–3 and invariant under MatchEq.
• RelTransitionSystem.Orientation.flipOrbit and throughSummand_flipOrbit — reversing one whole circuit, and the summand's invariance under doing so.
• SeparatedCountParity and NonSeparatedStep — the two per-case hypotheses the move analysis is stated over, discharged in SeparatedParity.lean and NonSeparatedStep.lean respectively.

(i) Chord combinatorics: the third-chord parity lemma

def RS.ChordPairCross {γ : Type u_1} [LinearOrder γ] (x y u w : γ) : Prop

Two chords of a linear order, each recorded low-to-high, interleave (in either relative position).

Equations

• RS.ChordPairCross x y u w = (x < u ∧ u < y ∧ y < w ∨ u < x ∧ x < w ∧ w < y)

def RS.InsideChord {γ : Type u_1} [LinearOrder γ] (x y p : γ) : Prop

A point lies strictly inside a chord.

Equations

• RS.InsideChord x y p = (x < p ∧ p < y)

theorem RS.chordPairCross_iff_xor {γ : Type u_1} [LinearOrder γ] {x y u w : γ} (huw : u < w) (hux : u ≠ x) (hwy : w ≠ y) : ChordPairCross x y u w ↔ Xor (InsideChord x y u) (InsideChord x y w)

Crossing a chord is interleaving: exactly one endpoint inside.

theorem RS.chordPairCross_parity {γ : Type u_1} [LinearOrder γ] {x y u w : γ} (huw : u < w) (hux : u ≠ x) (hwy : w ≠ y) : (if ChordPairCross x y u w then 1 else 0) % 2 = ((if InsideChord x y u then 1 else 0) + if InsideChord x y w then 1 else 0) % 2

The crossing indicator of one chord has the parity of the number of its endpoints inside the third chord.

theorem RS.third_chord_reparity {γ : Type u_1} [LinearOrder γ] {x y u₁ w₁ u₂ w₂ p₁ q₁ p₂ q₂ : γ} (h₁ : u₁ < w₁) (h₂ : u₂ < w₂) (h₁' : p₁ < q₁) (h₂' : p₂ < q₂) (hmul : {u₁, w₁, u₂, w₂} = {p₁, q₁, p₂, q₂}) (hne : ∀ p ∈ {u₁, w₁, u₂, w₂}, p ≠ x ∧ p ≠ y) : ((if ChordPairCross x y u₁ w₁ then 1 else 0) + if ChordPairCross x y u₂ w₂ then 1 else 0) % 2 = ((if ChordPairCross x y p₁ q₁ then 1 else 0) + if ChordPairCross x y p₂ q₂ then 1 else 0) % 2

The third-chord parity lemma: re-pairing the same four points of a linear order into two chords in any two ways (the same multiset of endpoints, each chord recorded low-to-high, no endpoint shared with the third chord) preserves the parity of the number of crossings with the third chord.

(ii) Walk rigidity

theorem RS.EdgeSubset.chain_exit_unique {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} {k k' : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) (hcont' : ∀ j < k', W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm' : W.pairing (iterWalk κ β k') ∈ F.boundaryFlags) : k = k'

The exit step of a boundary-terminated chain is unique.

theorem RS.EdgeSubset.chain_meet {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β β' : W.Flag} (hβ : β ∈ F.boundaryFlags) (hβ' : β' ∈ F.boundaryFlags) {k k' : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hcont' : ∀ j < k', W.pairing (iterWalk κ β' j) ∈ F.internalFlags) (t s : ℕ) : t ≤ k' → s ≤ k → iterWalk κ β' t = iterWalk κ β s → β' = β ∧ t = s

Chain rigidity: the walk is forward- and backward-deterministic, so two boundary-terminated chains sharing a walk flag start at the same boundary flag, at the same step.

Walk transfer under square avoidance

theorem RS.EdgeSubset.repair_iterWalk_of_avoid {α : 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 : ℕ} (havoid : ∀ t < k, W.pairing (iterWalk κ δ t) ≠ a ∧ W.pairing (iterWalk κ δ t) ≠ b ∧ W.pairing (iterWalk κ δ t) ≠ c ∧ W.pairing (iterWalk κ δ t) ≠ d) (t : ℕ) : t ≤ k → iterWalk (κ.repair a b c d v hsq) δ t = iterWalk κ δ t

A walk whose pairing arguments avoid the four flags of the square is untouched by the repair.

theorem RS.EdgeSubset.pathMatch_repair_of_avoid {α : 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 : ℕ} (hk : k ≤ F.flags.card) (hcont : ∀ j < k, W.pairing (iterWalk κ δ j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ δ k) ∈ F.boundaryFlags) (havoid : ∀ t < k, W.pairing (iterWalk κ δ t) ≠ a ∧ W.pairing (iterWalk κ δ t) ≠ b ∧ W.pairing (iterWalk κ δ t) ≠ c ∧ W.pairing (iterWalk κ δ t) ≠ d) : (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ

The path matching is untouched at a boundary flag whose chain avoids the square.

Closure of the periodic flags

theorem RS.EdgeSubset.periodicFlag_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {f : W.Flag} (hf : κ.PeriodicFlag f) : κ.PeriodicFlag (W.pairing f)

The edge pairing of a periodic flag is periodic (the reversed traversal of its circuit).

theorem RS.EdgeSubset.periodicFlag_match {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {f : W.Flag} (hf : κ.PeriodicFlag f) : κ.PeriodicFlag (κ.match_ f)

The matching image of a periodic flag is periodic.

theorem RS.EdgeSubset.chain_arg_ne_of_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {δ f : W.Flag} (hδ : δ ∈ F.boundaryFlags) {kδ : ℕ} (hcontδ : ∀ j < kδ, W.pairing (iterWalk κ δ j) ∈ F.internalFlags) (htermδ : W.pairing (iterWalk κ δ kδ) ∈ F.boundaryFlags) (hper : κ.PeriodicFlag f) {s : ℕ} (hs : s < kδ) : W.pairing (iterWalk κ δ s) ≠ f

No boundary chain hits a periodic flag in its pairing-argument position: chains are non-periodic.

Avoidance of a foreign chain

theorem RS.EdgeSubset.chain_arg_ne_of_onChain {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β δ f : W.Flag} (hβ : β ∈ F.boundaryFlags) (hδ : δ ∈ F.boundaryFlags) {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ β j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ β k) ∈ F.boundaryFlags) {kδ : ℕ} (hcontδ : ∀ j < kδ, W.pairing (iterWalk κ δ j) ∈ F.internalFlags) (hδβ : δ ≠ β) (hδγ : δ ≠ W.pairing (iterWalk κ β k)) {t : ℕ} (ht : t ≤ k) (hf : f = iterWalk κ β t ∨ f = W.pairing (iterWalk κ β t)) {s : ℕ} (hs : s < kδ) : W.pairing (iterWalk κ δ s) ≠ f

A chain distinct from β and from β's far end never hits a flag of β's chain in its pairing-argument position.

Membership on a boundary chain

def RS.EdgeSubset.OnBoundaryChain {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (β f : W.Flag) : Prop

Membership on the boundary chain of β: the flag appears on the walk from β (on either side of an edge) before the chain exits.

Equations

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

theorem RS.EdgeSubset.onBoundaryChain_match {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β f : W.Flag} (hβ : β ∈ F.boundaryFlags) (hf : f ∈ F.internalFlags) (h : OnBoundaryChain κ β f) : OnBoundaryChain κ β (κ.match_ f)

The chain membership is closed under the matching (on internal flags).

Case 1: squares on circuits

theorem RS.EdgeSubset.pathMatch_repair_of_periodic {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (hpa : κ.PeriodicFlag a) (hpc : κ.PeriodicFlag c) (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags) : (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ

Case 1: a square on periodic (circuit) components leaves every path matching unchanged.

Cases 2–3: squares localized to one chain

theorem RS.EdgeSubset.pathMatch_repair_of_chainLocal {α : 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) (hloc : ∀ (f : W.Flag), f = a ∨ f = b ∨ f = c ∨ f = d → κ.PeriodicFlag f ∨ OnBoundaryChain κ β f) (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags) : (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ

Cases 2–3: a square whose four flags are each periodic or on the chain of one boundary flag β leaves every path matching unchanged. Untouched chains avoid the square by rigidity (chain_meet); the two ends of β's chain must then re-pair with each other, because the repaired path matching is a fixed-point-free involution and every other boundary end is already taken.

The localized case predicate

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

The square is localized (cases 1–3 of the path ledger): the two re-paired edges lie on periodic components, or each of the four flags is periodic or on the chain of a single boundary flag. The complement is the genuine two-path case (case 4).

Equations

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

theorem RS.EdgeSubset.pathMatch_repair_of_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) (hloc : SquareLocalized κ a b c d) (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags) : (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ

(ii) pathMatch invariance in cases 1–3: a localized square leaves every path matching unchanged.

The crossing sign under pathMatch-preserving moves

theorem RS.EdgeSubset.chordCross_congr {α : Type} {W : Fragment α} [LinearOrder α] {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hpm : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), κ'.pathMatch δ hδ = κ.pathMatch δ hδ) (b b' : ↥F.boundaryFlags) : ChordCross κ' b b' ↔ ChordCross κ b b'

The chord-interleaving relation only depends on the path matching.

theorem RS.EdgeSubset.chordCrossingCount_congr {α : Type} {W : Fragment α} [LinearOrder α] {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hpm : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), κ'.pathMatch δ hδ = κ.pathMatch δ hδ) : chordCrossingCount κ' = chordCrossingCount κ

The chord-crossing count only depends on the path matching.

theorem RS.EdgeSubset.pathSign_congr {α : Type} {W : Fragment α} [LinearOrder α] {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hpm : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), κ'.pathMatch δ hδ = κ.pathMatch δ hδ) : pathSign κ' = pathSign κ

The path sign only depends on the path matching.

The MatchEq layer for the path sign

theorem RS.EdgeSubset.pathMatch_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) {δ : W.Flag} (hδ : δ ∈ F.boundaryFlags) : κ₂.pathMatch δ hδ = κ₁.pathMatch δ hδ

Matching-equal systems have equal path matchings.

theorem RS.EdgeSubset.chordCrossingCount_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) : chordCrossingCount κ₂ = chordCrossingCount κ₁

Matching-equal systems have equal chord-crossing counts.

theorem RS.EdgeSubset.pathSign_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} [LinearOrder α] {κ₁ κ₂ : F.RelTransitionSystem} (heq : κ₁.MatchEq κ₂) : pathSign κ₂ = pathSign κ₁

Matching-equal systems have equal path signs.

Classification: periodic, one chain, or two chains

theorem RS.EdgeSubset.periodic_or_onBoundaryChain {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f : W.Flag} (hf : f ∈ F.internalFlags) : κ.PeriodicFlag f ∨ ∃ β ∈ F.boundaryFlags, OnBoundaryChain κ β f

Every internal flag is periodic or lies on the chain of some boundary flag.

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

Chain membership from the far end of a chain is chain membership from the near end.

theorem RS.EdgeSubset.twoChains_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) : ∃ (β₁ : W.Flag) (β₂ : W.Flag) (hβ₁ : β₁ ∈ F.boundaryFlags) (_ : β₂ ∈ F.boundaryFlags), OnBoundaryChain κ β₁ a ∧ OnBoundaryChain κ β₂ c ∧ β₂ ≠ β₁ ∧ β₂ ≠ κ.pathMatch β₁ hβ₁

The two-path classification: a non-localized square has its two re-paired edges on two genuinely distinct boundary chains.

Circuit flips: orbit-supported orientation gauges

def RS.EdgeSubset.OrbitFlag {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (g f : W.Flag) : Prop

The flags of the walk orbit through g, on both sides of each visited edge.

Equations

• RS.EdgeSubset.OrbitFlag κ g f = ∃ (m : ℕ), f = RS.EdgeSubset.iterWalk κ g m ∨ f = W.pairing (RS.EdgeSubset.iterWalk κ g m)

theorem RS.EdgeSubset.orbitFlag_self {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (g : W.Flag) : OrbitFlag κ g g

A flag lies on its own orbit.

theorem RS.EdgeSubset.orbitFlag_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {g f : W.Flag} (hf : OrbitFlag κ g f) : OrbitFlag κ g (W.pairing f)

Orbits are closed under the edge pairing.

theorem RS.EdgeSubset.orbitFlag_of_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {g f : W.Flag} (h : OrbitFlag κ g (W.pairing f)) : OrbitFlag κ g f

And under it backwards.

theorem RS.EdgeSubset.orbitFlag_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {g f : W.Flag} (hg : κ.PeriodicFlag g) (hf : OrbitFlag κ g f) : f ∈ F.internalFlags

Every flag on a periodic flag's orbit is internal: a closed circuit never reaches the boundary.

theorem RS.EdgeSubset.orbitFlag_pairing_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {g f : W.Flag} (hg : κ.PeriodicFlag g) (hf : OrbitFlag κ g f) : W.pairing f ∈ F.internalFlags

So is each such flag's edge partner.

theorem RS.EdgeSubset.orbitFlag_match {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {g f : W.Flag} (hg : κ.PeriodicFlag g) (hf : OrbitFlag κ g f) : OrbitFlag κ g (κ.match_ f)

A periodic orbit is closed under the matching.

theorem RS.EdgeSubset.orbitFlag_of_match {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {g f : W.Flag} (hg : κ.PeriodicFlag g) (hf : f ∈ F.internalFlags) (h : OrbitFlag κ g (κ.match_ f)) : OrbitFlag κ g f

And under it backwards.

noncomputable def RS.EdgeSubset.RelTransitionSystem.Orientation.flipOrbit {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {g : W.Flag} (hg : κ.PeriodicFlag g) : κ.Orientation

Flip an orientation on the walk orbit of a periodic flag: a circuit-supported orientation gauge.

Equations

• o.flipOrbit hg = { isOut := fun (f : W.Flag) => if RS.EdgeSubset.OrbitFlag κ g f then !o.isOut f else o.isOut f, match_flip := ⋯, pairing_flip := ⋯ }

theorem RS.EdgeSubset.flipOrbit_isOut_of_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {g : W.Flag} (hg : κ.PeriodicFlag g) {f : W.Flag} (hf : OrbitFlag κ g f) : (o.flipOrbit hg).isOut f = !o.isOut f

Flipping an orbit reverses the orientation on it.

theorem RS.EdgeSubset.flipOrbit_isOut_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {g : W.Flag} (hg : κ.PeriodicFlag g) {f : W.Flag} (hf : ¬OrbitFlag κ g f) : (o.flipOrbit hg).isOut f = o.isOut f

And leaves it alone elsewhere.

theorem RS.EdgeSubset.throughSummand_flipOrbit {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} [LinearOrder α] {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) {g : W.Flag} (hg : κ.PeriodicFlag g) (c : ℕ) : F.throughSummand hM st hbnd (o.flipOrbit hg) c = F.throughSummand hM st hbnd o c

An orbit flip is a circuit-supported gauge, so the constrained summand is invariant under it: the difference is supported on closed circuits.

The per-move interface and its inputs

def RS.SeparatedCountParity : Prop

The count-parity hypothesis (cases 1–3): a separated square on a localized configuration flips the circuit-count parity (the splice merges two circuits, Δ = −1, or splits one component, Δ = +1). Discharged in SeparatedParity.lean.

Equations

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

def RS.NonSeparatedStep : Prop

The flipped-segment hypothesis (non-separated moves): a non-separated square (isOut c = isOut a) admits an orientation on the repaired system realizing the same pathSign-weighted summand. The structure: the repaired walk reverses a segment (Δ = 0), the transported orientation flips on the reversed segment, and the vertex transposition (−1) cancels against the segment-reversal telescope (+1 total). Discharged in NonSeparatedStep.lean.

Equations

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