The frame across a separated two-path step

The separated transport keeps isOut verbatim, so the chain direction observable is preserved pointwise; canonicality after the step is therefore measured by the new chords' low ends against the old directions — pure label combinatorics. The new pairing's rigidity forces the re-paired ends to carry opposite directions, a constraint on the old frame derived from the new system.

theorem RS.EdgeSubset.chainDir_transportRepair {α : 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) (hflip : o.isOut c = !o.isOut a) (δ : W.Flag) : chainDir (RelTransitionSystem.Orientation.transportRepair hsq o hflip) δ = chainDir o δ

The separated transport preserves the chain direction at every flag.

theorem RS.EdgeSubset.swap_dirs_opposite {α : 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) (hflip : o.isOut c = !o.isOut a) {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (hcross : (κ.repair a b c d v hsq).pathMatch e₁ he₁ = e₂) (hint : W.pairing e₁ ∈ F.internalFlags) : chainDir o e₂ = !chainDir o e₁

The re-paired ends carry opposite directions: the new chord's rigidity, read back through the preserved directions, is a constraint on the old frame.

theorem RS.EdgeSubset.mem_antiLowSet_transport {α : Type} [LinearOrder α] {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) (hflip : o.isOut c = !o.isOut a) {x : W.Flag} : x ∈ antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq o hflip) ↔ ∃ (hx : x ∈ F.boundaryFlags), W.pairing x ∈ F.internalFlags ∧ F.boundaryLabel hx < F.boundaryLabel ⋯ ∧ chainDir o x = true

Membership in the transported frame's anti-canonical set: directions are the old ones, labels are the new chords'.

theorem RS.EdgeSubset.mem_antiLowSet_transport_untouched {α : Type} [LinearOrder α] {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) (hflip : o.isOut c = !o.isOut a) {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags) (hout : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) {x : W.Flag} (hx1 : x ≠ e₁) (hx2 : x ≠ e₂) (hx3 : x ≠ κ.pathMatch e₁ he₁) (hx4 : x ≠ κ.pathMatch e₂ he₂) : x ∈ antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq o hflip) ↔ x ∈ antiLowSet o

Untouched chains keep their anti-canonicality across the transported step: off the four re-paired ends both the label comparison and the direction are unchanged.

theorem RS.EdgeSubset.chainDir_true_iff_high {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} (hc : PathCanonical o) {x : W.Flag} (hx : x ∈ F.boundaryFlags) (hint : W.pairing x ∈ F.internalFlags) : chainDir o x = true ↔ F.boundaryLabel ⋯ < F.boundaryLabel hx

The canonical direction formula: on a participating chain a canonical frame points true exactly at the high-labelled end.

theorem RS.EdgeSubset.mem_antiLowSet_transport_of_canonical {α : Type} [LinearOrder α] {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} (hflip : o.isOut c = !o.isOut a) (hc : PathCanonical o) {x y : W.Flag} (hx : x ∈ F.boundaryFlags) (hy : y ∈ F.boundaryFlags) (hint : W.pairing x ∈ F.internalFlags) (hnew : (κ.repair a b c d v hsq).pathMatch x hx = y) : x ∈ antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq o hflip) ↔ F.boundaryLabel hx < F.boundaryLabel hy ∧ F.boundaryLabel ⋯ < F.boundaryLabel hx

The four-end evaluation: from a canonical frame, an end of a re-paired chord is anti-canonical after the transported step exactly when it is low in its new chord but was high in its old one. (Instantiate at the four swap ends with the new partners from pathMatch_repair_swap.)

theorem RS.EdgeSubset.antiLowSet_transport_subset {α : Type} [LinearOrder α] {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} (hflip : o.isOut c = !o.isOut a) (hc : PathCanonical o) {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags) (hout : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) : antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq o hflip) ⊆ {e₁, e₂, κ.pathMatch e₁ he₁, κ.pathMatch e₂ he₂}

The transported anti-canonical set lives on the four re-paired ends: from a canonical source frame, every other chain stays canonical.

noncomputable def RS.EdgeSubset.newLow {α : Type} [LinearOrder α] {W : Fragment α} (F : EdgeSubset W) {e₁ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (e₂ : W.Flag) (he₂ : e₂ ∈ F.boundaryFlags) : W.Flag

The low end of the (e₁, e₂) chord, as a flag.

Equations

• F.newLow he₁ e₂ he₂ = if F.boundaryLabel he₁ < F.boundaryLabel he₂ then e₁ else e₂

theorem RS.EdgeSubset.antiLowSet_transport_eq {α : Type} [LinearOrder α] {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} (hflip : o.isOut c = !o.isOut a) (hc : PathCanonical o) {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags) (hne : e₁ ≠ e₂) (hPne : κ.pathMatch e₁ he₁ ≠ e₂) (hcross : (κ.repair a b c d v hsq).pathMatch e₁ he₁ = e₂) (hfar : (κ.repair a b c d v hsq).pathMatch (κ.pathMatch e₁ he₁) ⋯ = κ.pathMatch e₂ he₂) (hout : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) (hint₁ : W.pairing e₁ ∈ F.internalFlags) (hint₂ : W.pairing e₂ ∈ F.internalFlags) (hintP₁ : W.pairing (κ.pathMatch e₁ he₁) ∈ F.internalFlags) (hintP₂ : W.pairing (κ.pathMatch e₂ he₂) ∈ F.internalFlags) : antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq o hflip) = (if if F.boundaryLabel he₁ < F.boundaryLabel he₂ then F.boundaryLabel ⋯ < F.boundaryLabel he₁ else F.boundaryLabel ⋯ < F.boundaryLabel he₂ then {F.newLow he₁ e₂ he₂} else ∅) ∪ if if F.boundaryLabel ⋯ < F.boundaryLabel ⋯ then F.boundaryLabel he₁ < F.boundaryLabel ⋯ else F.boundaryLabel he₂ < F.boundaryLabel ⋯ then {F.newLow ⋯ (κ.pathMatch e₂ he₂) ⋯} else ∅

The transported anti set, exactly: the two new chords' low ends, each present exactly when it was high in its old chord.

theorem RS.EdgeSubset.antiLowSet_transport_card {α : Type} [LinearOrder α] {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} (hflip : o.isOut c = !o.isOut a) (hc : PathCanonical o) {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags) (hne : e₁ ≠ e₂) (hPne : κ.pathMatch e₁ he₁ ≠ e₂) (hcross : (κ.repair a b c d v hsq).pathMatch e₁ he₁ = e₂) (hfar : (κ.repair a b c d v hsq).pathMatch (κ.pathMatch e₁ he₁) ⋯ = κ.pathMatch e₂ he₂) (hout : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) (hint₁ : W.pairing e₁ ∈ F.internalFlags) (hint₂ : W.pairing e₂ ∈ F.internalFlags) (hintP₁ : W.pairing (κ.pathMatch e₁ he₁) ∈ F.internalFlags) (hintP₂ : W.pairing (κ.pathMatch e₂ he₂) ∈ F.internalFlags) : (antiLowSet (RelTransitionSystem.Orientation.transportRepair hsq o hflip)).card = (if if F.boundaryLabel he₁ < F.boundaryLabel he₂ then F.boundaryLabel ⋯ < F.boundaryLabel he₁ else F.boundaryLabel ⋯ < F.boundaryLabel he₂ then 1 else 0) + if if F.boundaryLabel ⋯ < F.boundaryLabel ⋯ then F.boundaryLabel he₁ < F.boundaryLabel ⋯ else F.boundaryLabel he₂ < F.boundaryLabel ⋯ then 1 else 0

The flip count of a separated canonical step: the four-label indicator sum — the exact left side of the parity identity.

theorem RS.EdgeSubset.matchEq_canonical_transfer {α : 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} (hc : PathCanonical o) : ∃ (o' : κ₂.Orientation), PathCanonical o' ∧ F.throughSummand hM st hbnd o' κ₂.openCircuitCount = F.throughSummand hM st hbnd o κ₁.openCircuitCount

Canonicality and the summand cross a MatchEq unchanged (the unsigned endpoint transfer).

def RS.PairedLedgerUnsigned : Prop

The paired step without the chord signs: within a block the pairing returns, so the two path signs agree and cancel.

Equations

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

theorem RS.EdgeSubset.pairedLedger_iff_unsigned : PairedLedger ↔ PairedLedgerUnsigned

The signed and unsigned paired steps coincide.