The canonical frame: chain directions and re-canonicalization

Vocabulary for the final PairedLedger induction. Every participating boundary chain of a relative transition system carries a direction observable — the orientation value at its entry edge (chainDir). Path-canonicality is exactly the vanishing of chainDir at every low-labelled chain end (pathCanonical_iff_chainDir), and chainDir is constant along a chain (chainDir_eq), so an arbitrary orientation differs from the canonical frame exactly on the chains its low ends point out of (antiLowSet, pathCanonical_iff_antiLowSet_empty). Flipping one offending chain (exists_chainRecanonicalize) toggles the two end directions, preserves every other chain, and transforms the constrained summand by the two end-colour signs at a ∂-relabelled state; iterating over the anti-canonical chains re-canonicalizes any orientation (exists_recanonicalize).

The chain-direction observable

def RS.EdgeSubset.chainDir {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) (β : W.Flag) : Bool

The chain direction of an orientation at a boundary flag: the orientation value at the flag's entry edge (the internal partner of the boundary flag). false means the entry edge is incoming — the chain leaves this end.

Equations

• RS.EdgeSubset.chainDir o β = o.isOut (W.pairing β)

theorem RS.EdgeSubset.chainDir_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) (β : W.Flag) : chainDir o β = o.isOut (W.pairing β)

A chain's direction is the orientation at its entry edge.

theorem RS.EdgeSubset.pathMatch_pairing_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) (hint : W.pairing β ∈ F.internalFlags) : W.pairing (κ.pathMatch β hβ) ∈ F.internalFlags

The entry edge of the far chain end is internal whenever the near one is: the chain has at least one step, and its last walk flag is internal.

theorem RS.EdgeSubset.chainDir_pathMatch {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {β : W.Flag} (hβ : β ∈ F.boundaryFlags) (hint : W.pairing β ∈ F.internalFlags) : chainDir o (κ.pathMatch β hβ) = !chainDir o β

Chain-direction rigidity: the chain is coherently directed, so the two ends' entry flags carry opposite orientation values — for any orientation of the system.

Canonicality via the chain direction

theorem RS.EdgeSubset.pathCanonical_iff_chainDir {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) : PathCanonical o ↔ ∀ (β : W.Flag) (hβ : β ∈ F.boundaryFlags), W.pairing β ∈ F.internalFlags → F.boundaryLabel hβ < F.boundaryLabel ⋯ → chainDir o β = false

Path-canonicality is a chain-direction condition: an orientation is path-canonical iff its chain direction vanishes at every participating boundary flag that is the low-labelled end of its chord.

Chain directions under the ported chain flip

theorem RS.EdgeSubset.chainDir_portFlip_of_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {γ : W.Flag} (hγ : W.pairing γ ∈ S) : chainDir (o.portFlip h) γ = !chainDir o γ

Flipping a ported set toggles the chain direction at ends whose entry edge lies in the set.

theorem RS.EdgeSubset.chainDir_portFlip_of_notMem {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {γ : W.Flag} (hγ : W.pairing γ ∉ S) : chainDir (o.portFlip h) γ = chainDir o γ

Flipping a ported set preserves the chain direction at ends whose entry edge avoids the set.

theorem RS.EdgeSubset.exists_chainFlipSet {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) (hint : W.pairing β ∈ F.internalFlags) : ∃ (S : Finset W.Flag), PortedFlipSet κ S (W.pairing β) (W.pairing (κ.pathMatch β hβ)) (F.boundaryLabel hβ) (F.boundaryLabel ⋯) ∧ W.pairing (κ.pathMatch β hβ) ∈ S ∧ ∀ γ ∈ F.boundaryFlags, γ ≠ β → γ ≠ κ.pathMatch β hβ → W.pairing γ ∉ S

The chain flip set of a participating boundary flag: the boundary chain of β realizes a ported flip set whose ports are the entry edges of β and of its path match, labelled by the two chain ends, and whose flip set avoids the entry edge of every other boundary flag.

The re-canonicalization ledger, one chain

theorem RS.EdgeSubset.signPairSq (ℓ : ℕ) (c₁ c₂ : Fin (2 * ℓ)) : ↑(oddPartnerSign ℓ c₁ * oddPartnerSign ℓ c₂) * ↑(oddPartnerSign ℓ c₁ * oddPartnerSign ℓ c₂) = 1

The two-sign cast squares to one.

theorem RS.EdgeSubset.throughSummand_portFlip_inv {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {S : Finset W.Flag} {p₁ p₂ : W.Flag} {i₁ i₂ : α} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) (h : PortedFlipSet κ S p₁ p₂ i₁ i₂) {c₁ c₂ : Fin (2 * ℓ)} (hc₁ : st i₁ = Sum.inr c₁) (hc₂ : st i₂ = Sum.inr c₂) (n : ℕ) : F.throughSummand hM st hbnd o n = ↑(oddPartnerSign ℓ c₁ * oddPartnerSign ℓ c₂) * F.throughSummand hM (stateOddFlip st i₁ i₂) ⋯ (o.portFlip h) n

The inverted chain-flip ledger: the summand of the original orientation equals the two chain-end colour signs times the summand of the flipped orientation at the ∂-relabelled state — the direction useful for re-canonicalization, obtained from throughSummand_portFlip by involution of the relabel and the sign.

theorem RS.EdgeSubset.exists_chainRecanonicalize {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) {β : W.Flag} (hβ : β ∈ F.boundaryFlags) (hint : W.pairing β ∈ F.internalFlags) {c₁ c₂ : Fin (2 * ℓ)} (hc₁ : st (F.boundaryLabel hβ) = Sum.inr c₁) (hc₂ : st (F.boundaryLabel ⋯) = Sum.inr c₂) : ∃ (o₁ : κ.Orientation), chainDir o₁ β = !chainDir o β ∧ chainDir o₁ (κ.pathMatch β hβ) = !chainDir o (κ.pathMatch β hβ) ∧ (∀ γ ∈ F.boundaryFlags, γ ≠ β → γ ≠ κ.pathMatch β hβ → chainDir o₁ γ = chainDir o γ) ∧ ∀ (n : ℕ), F.throughSummand hM st hbnd o n = ↑(oddPartnerSign ℓ c₁ * oddPartnerSign ℓ c₂) * F.throughSummand hM (stateOddFlip st (F.boundaryLabel hβ) (F.boundaryLabel ⋯)) ⋯ o₁ n

One-chain re-canonicalization: for any orientation and any participating boundary flag β with internal entry partner, there is an orientation of the same system that toggles the chain direction at β and its path match, preserves the chain direction of every other boundary flag, and satisfies the inverted value ledger with the chain's two boundary labels explicit.

The anti-canonical chain set and full re-canonicalization

noncomputable def RS.EdgeSubset.antiLowSet {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) : Finset W.Flag

The set of low chain ends whose chain is directed against the canonical frame: participating boundary flags that are the low-labelled end of their chord and whose entry edge is outgoing. Each anti-canonical chain contributes exactly one element — its low end.

Equations

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

theorem RS.EdgeSubset.mem_antiLowSet {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o : κ.Orientation} {β : W.Flag} : β ∈ antiLowSet o ↔ ∃ (hβ : β ∈ F.boundaryFlags), W.pairing β ∈ F.internalFlags ∧ F.boundaryLabel hβ < F.boundaryLabel ⋯ ∧ chainDir o β = true

Membership in the anti-canonical set: the low end of a chain that runs the wrong way — exactly the chains re-canonicalization flips.

theorem RS.EdgeSubset.pathCanonical_iff_antiLowSet_empty {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) : PathCanonical o ↔ antiLowSet o = ∅

An orientation is path-canonical exactly when its anti-canonical low-end set is empty.

theorem RS.EdgeSubset.low_ne_pathMatch_of_low {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {β γ : W.Flag} (hβ : β ∈ F.boundaryFlags) (hγ : γ ∈ F.boundaryFlags) (hlowβ : F.boundaryLabel hβ < F.boundaryLabel ⋯) (hlowγ : F.boundaryLabel hγ < F.boundaryLabel ⋯) : γ ≠ κ.pathMatch β hβ

A low chain end is never the path match of a low chain end: the path match of a low end is the high end of the same chord.

theorem RS.EdgeSubset.antiLowSet_flip {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o₁ : κ.Orientation} {β : W.Flag} (hβ : β ∈ F.boundaryFlags) (hβmem : β ∈ antiLowSet o) (hd₁ : chainDir o₁ β = !chainDir o β) (hpres : ∀ γ ∈ F.boundaryFlags, γ ≠ β → γ ≠ κ.pathMatch β hβ → chainDir o₁ γ = chainDir o γ) : antiLowSet o₁ = (antiLowSet o).erase β

The flip step shrinks the anti-canonical set by exactly its chain: an orientation that toggles the chain direction at an anti-canonical low end β (and possibly at β's path match) and preserves every other chain direction has anti-canonical set antiLowSet o minus β.

theorem RS.EdgeSubset.exists_recanonicalize {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {k ℓ : ℕ} (hM : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) : ∃ (o₁ : κ.Orientation) (s : ℂ) (st₁ : GenBoundaryState k ℓ α) (hbnd₁ : genBoundarySubsetMatches W F.flags st₁), PathCanonical o₁ ∧ s * s = 1 ∧ ∀ (n : ℕ), F.throughSummand hM st hbnd o n = s * F.throughSummand hM st₁ hbnd₁ o₁ n

Full re-canonicalization: any orientation of a relative transition system is connected to a path-canonical orientation of the same system by a value ledger — the summand at the original data equals a sign (a product of chain-end colour sign pairs, hence squaring to 1) times the summand of the canonical orientation at an iterated ∂-relabel of the state. Induction on the number of anti-canonical chains, flipping one chain per step via exists_chainRecanonicalize.