Pairing-preserving connectivity

The pairing-resolved value is well-defined once systems inducing the same boundary pairing are connected by pairing-preserving repair steps. This file fixes the step relation and the connectivity statement, proves that localized repairs qualify, and derives the same-pairing invariance of the signed summand from connectivity and the per-step ledger.

def RS.EdgeSubset.SamePairing {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ κ' : F.RelTransitionSystem) : Prop

Two systems induce the same boundary pairing.

Equations

• RS.EdgeSubset.SamePairing κ κ' = ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), κ.pathMatch δ hδ = κ'.pathMatch δ hδ

theorem RS.EdgeSubset.SamePairing.refl {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : SamePairing κ κ

Inducing the same boundary pairing is reflexive.

theorem RS.EdgeSubset.SamePairing.symm {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (h : SamePairing κ κ') : SamePairing κ' κ

It is symmetric.

theorem RS.EdgeSubset.SamePairing.trans {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ κ₃ : F.RelTransitionSystem} (h : SamePairing κ₁ κ₂) (h' : SamePairing κ₂ κ₃) : SamePairing κ₁ κ₃

And transitive — an equivalence on transition systems.

def RS.EdgeSubset.MatchPreservingStep {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ₁ κ₂ : F.RelTransitionSystem) : Prop

A repair step that preserves the boundary pairing.

Equations

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

theorem RS.EdgeSubset.samePairing_of_step {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (h : MatchPreservingStep κ₁ κ₂) : SamePairing κ₁ κ₂

A pairing-preserving step indeed preserves the pairing.

def RS.EdgeSubset.PairedStep {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ₁ κ₂ : F.RelTransitionSystem) : Prop

A composite move: a repair block whose net effect preserves the boundary pairing (individual repairs may cross two chains and change it; the double-crossing example shows single-step connectivity fails, and non-adjacent restorations force general blocks rather than pairs).

Equations

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

def RS.EdgeSubset.MatchPreservingMove {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ₁ κ₂ : F.RelTransitionSystem) : Prop

A pairing-preserving move: a single preserved step or a π-restoring pair.

Equations

• RS.EdgeSubset.MatchPreservingMove κ₁ κ₂ = (RS.EdgeSubset.MatchPreservingStep κ₁ κ₂ ∨ RS.EdgeSubset.PairedStep κ₁ κ₂)

def RS.EdgeSubset.PairingConnectivity : Prop

The connectivity statement (the keystone, move form): systems with the same boundary pairing are connected by pairing-preserving moves, up to match-equality at the endpoints. (Single steps do not suffice: the double-crossing configuration disconnects the fibre.)

Equations

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

theorem RS.EdgeSubset.pairingConnectivity : PairingConnectivity

Connectivity is a theorem in the block form: any repair chain between same-pairing systems is a single pairing-preserving move, so the general connectivity of TransitionMove suffices.

def RS.EdgeSubset.MatchPreservingLedger : Prop

The per-step ledger interface: every pairing-preserving step preserves the signed canonical summand (dischargeable from the localized/non-separated ledgers plus the orbit parities; two-path moves change the pairing and are excluded by the step relation).

Equations

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

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

The MatchEq layer for the signed canonical summand.

theorem RS.EdgeSubset.chain_carry {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (HLedger : MatchPreservingLedger) {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o : κ.Orientation) (hc : PathCanonical o) {n : ℕ} (chain : Fin (n + 1) → F.RelTransitionSystem) (h0 : (chain 0).MatchEq κ) (hstep : ∀ (r : Fin n), MatchPreservingMove (chain r.castSucc) (chain r.succ)) (r : Fin (n + 1)) : ∃ (oᵣ : (chain r).Orientation), PathCanonical oᵣ ∧ pathSign (chain r) * F.throughSummand hM st hbnd oᵣ (chain r).openCircuitCount = pathSign κ * F.throughSummand hM st hbnd o κ.openCircuitCount

The forward-carried chain induction: along a chain of pairing-preserving steps, a canonical orientation and the signed value propagate from the base.

theorem RS.EdgeSubset.endpoint_transfer {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ₁ κ' : F.RelTransitionSystem} (hlast : κ₁.MatchEq κ') (olast : κ₁.Orientation) (hclast : PathCanonical olast) : ∃ (oκ' : κ'.Orientation), PathCanonical oκ' ∧ pathSign κ' * F.throughSummand hM st hbnd oκ' κ'.openCircuitCount = pathSign κ₁ * F.throughSummand hM st hbnd olast κ₁.openCircuitCount

The endpoint transfer: a canonical orientation and the signed value cross a MatchEq to the target system.

theorem RS.EdgeSubset.samePairing_invariance_of {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (HConn : PairingConnectivity) (HLedger : MatchPreservingLedger) {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (κ κ' : F.RelTransitionSystem) (hsp : SamePairing κ κ') (o : κ.Orientation) (hc : PathCanonical o) (o' : κ'.Orientation) (hc' : PathCanonical o') : pathSign κ * F.throughSummand hM st hbnd o κ.openCircuitCount = pathSign κ' * F.throughSummand hM st hbnd o' κ'.openCircuitCount

Same-pairing invariance from connectivity and the step ledger: with these two inputs the signed canonical summand depends only on the boundary pairing — the well-definedness of the pairing-resolved value.