The paired assembly: PairedLedgerUnsigned

The final assembly of Proposition 3's paired step. Along any π-returning repair block, the canonical route accumulates a state relabel and a sign; this file pins both.

The state: the accumulated relabel set is the status difference statusDiff of the endpoint systems — per step the relabel pairs are exactly the labels whose high-status changed (antiLow_labels_eq_statusChange for separated steps, nonsep_labels_eq_statusChange for non-separated ones), and the status difference telescopes (statusDiff_trans) to ∅ at the π-returning endpoint (statusDiff_of_samePairing).

The sign: the accumulated sign is carried as (−1)^tp · flipSignProd g T — one −1 per two-path step, and the port-sign product of the full flip list T at the evolving colours. At the endpoint the flip list has all label counts even (its parity fold is the empty status difference), so flipSignProd_of_even evaluates the product to (−1)^{T.length}; the per-step parity identity tp_k + |T_k| ≡ Δcc_k (mod 2) — the four-label parity lemmas fed by the exact per-step flip counts — telescopes the exponent against the chord-crossing counts, which return with the pairing. Hence the total sign is +1.

Main results: chainStatusLedger (the enriched chain induction), stepStatusLedger (the per-step composed ledger), pairedLedgerUnsigned, and pairedLedger.

Flip-sign list algebra

theorem RS.flipSignProd_mul_self {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (L : List (α × α)) : flipSignProd f L * flipSignProd f L = 1

The flip-sign product is involutive: each factor is ±1.

noncomputable def RS.flipColoursFold {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (L : List (α × α)) : α → Fin (2 * ℓ)

The accumulated colour relabel of a flip sequence.

Equations

• RS.flipColoursFold f L = List.foldl RS.flipColours f L

theorem RS.flipColoursFold_nil {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) : flipColoursFold f [] = f

The empty flip sequence leaves the colours alone.

theorem RS.flipColoursFold_cons {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (p : α × α) (L : List (α × α)) : flipColoursFold f (p :: L) = flipColoursFold (flipColours f p) L

One more flip moves its two labels' colours, then continues.

theorem RS.flipSignProd_append {α : Type} {ℓ : ℕ} (f : α → Fin (2 * ℓ)) (L₁ L₂ : List (α × α)) : flipSignProd f (L₁ ++ L₂) = flipSignProd f L₁ * flipSignProd (flipColoursFold f L₁) L₂

The flip-sign product splits along an append, the second block evaluated at the accumulated colours of the first.

theorem RS.pairFold_eq_oddCountLabels {α : Type} {L : List (α × α)} (hd : ∀ p ∈ L, p.1 ≠ p.2) : pairFold L = oddCountLabels L

For pairs with distinct components the symmetric-difference fold is the odd-count set.

theorem RS.flipColoursFold_apply {α : Type} {ℓ : ℕ} {L : List (α × α)} (hd : ∀ p ∈ L, p.1 ≠ p.2) (f : α → Fin (2 * ℓ)) (i : α) : flipColoursFold f L i = if i ∈ oddCountLabels L then oddPartner ℓ (f i) else f i

The accumulated colour relabel is the odd-partner relabel at the odd-count labels.

Indicator and crossing-symmetry helpers

Status-difference membership and transport

theorem RS.EdgeSubset.repartner_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {ε : W.Flag} (hε : ε ∈ F.boundaryFlags) (hch : κ'.pathMatch ε hε ≠ κ.pathMatch ε hε) : W.pairing ε ∈ F.internalFlags

A re-partnered end participates: if the path match of a boundary flag differs between two systems, its entry edge is internal — a boundary-paired end has the same (pairing-determined) path match in every system.

Colour functions matching a state

The signed full re-canonicalization

theorem RS.EdgeSubset.exists_recanonicalize_signed {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) (g : α → Fin (2 * ℓ)) (hg : ∀ (i : α) (c : Fin (2 * ℓ)), st i = Sum.inr c → g i = c) : ∃ (o₁ : κ.Orientation) (L : List (α × α)), PathCanonical o₁ ∧ L.length = (antiLowSet o).card ∧ List.Pairwise PairDisjoint L ∧ (∀ p ∈ L, AntiLowPair o p) ∧ ∀ (n : ℕ), F.throughSummand hM st hbnd o n = ↑(flipSignProd g L) * F.throughSummand hM (stateOddFlipSet st (pairFold L)) ⋯ o₁ n

Sign-explicit full re-canonicalization: as exists_recanonicalize_sets, but with the accumulated sign pinned as the flip-sign product flipSignProd g L of the flip list at any colour function g matching the state.

The anchored transported frame: per-end evaluation

The per-step composed status ledger

theorem RS.EdgeSubset.stepStatusLedger {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ₁ κ₂ : F.RelTransitionSystem} (hstep : IsRepairStep κ₁ κ₂) {o₁ : κ₁.Orientation} (hc₁ : PathCanonical o₁) (g : α → Fin (2 * ℓ)) (hg : ∀ (i : α) (c : Fin (2 * ℓ)), st i = Sum.inr c → g i = c) : ∃ (o₂ : κ₂.Orientation) (T : List (α × α)) (tp : ℕ), PathCanonical o₂ ∧ (∀ p ∈ T, p.1 ≠ p.2) ∧ pairFold T = statusDiff κ₁ κ₂ ∧ (tp + T.length + chordCrossingCount κ₁ + chordCrossingCount κ₂) % 2 = 0 ∧ F.throughSummand hM (stateOddFlipSet st (pairFold T)) ⋯ o₂ κ₂.openCircuitCount = ↑((-1) ^ tp * flipSignProd g T) * F.throughSummand hM st hbnd o₁ κ₁.openCircuitCount

The per-step composed ledger: across one repair step from a canonical frame, the state relabel is stateOddFlipSet at the fold of an explicit flip list T with pairFold T = statusDiff κ₁ κ₂, the sign is (−1)^tp · flipSignProd g T at any colour function g matching the state, and the flip count satisfies the crossing parity tp + |T| ≡ cc κ₁ + cc κ₂ (mod 2).

theorem RS.EdgeSubset.chainStatusLedger {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {n : ℕ} (chain : Fin (n + 1) → F.RelTransitionSystem) (hstep : ∀ (r : Fin n), IsRepairStep (chain r.castSucc) (chain r.succ)) {o₀ : (chain 0).Orientation} (hc₀ : PathCanonical o₀) (g : α → Fin (2 * ℓ)) (hg : ∀ (i : α) (c : Fin (2 * ℓ)), st i = Sum.inr c → g i = c) (r : Fin (n + 1)) : ∃ (oᵣ : (chain r).Orientation) (T : List (α × α)) (tp : ℕ), PathCanonical oᵣ ∧ (∀ p ∈ T, p.1 ≠ p.2) ∧ pairFold T = statusDiff (chain 0) (chain r) ∧ (tp + T.length + chordCrossingCount (chain 0) + chordCrossingCount (chain r)) % 2 = 0 ∧ F.throughSummand hM (stateOddFlipSet st (pairFold T)) ⋯ oᵣ (chain r).openCircuitCount = ↑((-1) ^ tp * flipSignProd g T) * F.throughSummand hM st hbnd o₀ (chain 0).openCircuitCount

The chain status ledger: fold the per-step ledger along a repair chain — the relabel set is the status difference of the endpoint stages, the sign is the explicit (−1)^tp · flipSignProd g T, and the flip count carries the crossing parity telescope.

The paired assembly

theorem RS.pairedLedgerUnsigned : PairedLedgerUnsigned

The paired step, unsigned form: across any π-returning repair block, a canonical frame carries to a canonical frame with the same summand at the same state — the accumulated relabel is the (empty) status difference of the endpoints, and the accumulated sign telescopes to +1 through the crossing-parity ledger.

theorem RS.pairedLedger : EdgeSubset.PairedLedger

The paired step: the last input of Proposition 3's per-π well-definedness — across any π-returning repair block the pathSign-weighted canonical summand is preserved.