Chain agreement of path-canonical orientations

Two path-canonical orientations of the same boundary-relative transition system agree on every non-periodic internal flag: a non-periodic flag lies on the boundary-to-boundary chain of a unique pair of boundary ends, the low-labelled end's entry value is pinned to incoming by canonicality, and orientation values propagate rigidly along a chain (match_flip and pairing_flip alternate), so the whole chain's values are determined by the pinned seed.

Main results

• pathCanonical_agree_nonperiodic — path-canonical orientations agree off the periodic flags.
• pathCanonical_diff_pairing_closed — hence their difference set is pairing-closed on internal flags (disagreement forces periodicity, and periodic flags have internal pairings).
• throughSummand_pathCanonical — hence the constrained summand does not depend on the choice of path-canonical orientation, discharging the hchain hypothesis of throughSummand_canonical_unique.

Proof route

1. traceChain_some_exit converts a terminating chain into walk data: an exit step count with internal pairings before it.
2. isOut_iterWalk_eq_not_seed / isOut_pairing_iterWalk_eq_seed propagate any orientation's value along a chain: every match-side flag carries the negated seed value, every pairing-side flag the seed value, where the seed is the value at the entry edge.
3. pathCanonical_agree_on_chain compares the two chain ends by label; canonicality pins the seed at the low end, and the reverse walk identities transport the pinned value to the given flag.
4. pathCanonical_agree_nonperiodic places an arbitrary non-periodic internal flag on the chain of the boundary end its forward walk reaches, as a pairing-side flag of the reverse chain.

1. From terminating chains to walk exit data

theorem RS.EdgeSubset.traceChain_some_exit {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (fuel : ℕ) (f b : W.Flag) : traceChain κ fuel f = some b → ∃ (k : ℕ), (∀ j < k, W.pairing (iterWalk κ f j) ∈ F.internalFlags) ∧ W.pairing (iterWalk κ f k) = b ∧ b ∈ F.boundaryFlags

A terminating chain yields walk data: an exit step k whose earlier pairings are all internal and whose pairing at k is the boundary result.

2. Rigid propagation of orientation values along a chain

theorem RS.EdgeSubset.isOut_iterWalk_eq_not_seed {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {b : W.Flag} {k : ℕ} (hcont : ∀ t < k, W.pairing (iterWalk κ b t) ∈ F.internalFlags) (j : ℕ) : 1 ≤ j → j ≤ k → o.isOut (iterWalk κ b j) = !o.isOut (W.pairing b)

Match-side propagation: along a walk with internal pairings up to step k, every visited flag (step 1 ≤ j ≤ k) carries the negated seed value, for any orientation.

theorem RS.EdgeSubset.isOut_pairing_iterWalk_eq_seed {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {b : W.Flag} {k : ℕ} (hcont : ∀ t < k, W.pairing (iterWalk κ b t) ∈ F.internalFlags) (j : ℕ) : j < k → o.isOut (W.pairing (iterWalk κ b j)) = o.isOut (W.pairing b)

Pairing-side propagation: along a walk with internal pairings up to step k, every intermediate pairing (step j < k) carries the seed value, for any orientation.

3. Chain agreement from the low-end seed

theorem RS.EdgeSubset.pathCanonical_agree_on_chain {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (hc : PathCanonical o) (hc' : PathCanonical o') {b : W.Flag} (hb : b ∈ F.boundaryFlags) {k : ℕ} (hcont : ∀ t < k, W.pairing (iterWalk κ b t) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ b k) ∈ F.boundaryFlags) (hkle : k ≤ F.flags.card) {m : ℕ} (hm : m < k) : o.isOut (W.pairing (iterWalk κ b m)) = o'.isOut (W.pairing (iterWalk κ b m))

Agreement on a chain: two path-canonical orientations agree on every pairing-side flag of a boundary-terminated chain — whichever end has the lower label, canonicality pins its entry value to incoming for both orientations, and rigid propagation transports the pinned seed to the given flag.

Agreement off the periodic flags

theorem RS.EdgeSubset.pathCanonical_agree_nonperiodic {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (hc : PathCanonical o) (hc' : PathCanonical o') (f : W.Flag) : f ∈ F.internalFlags → ¬κ.PeriodicFlag f → o.isOut f = o'.isOut f

Chain agreement of path-canonical orientations: two path-canonical orientations of one relative transition system agree on every non-periodic internal flag.

5. Corollaries

theorem RS.EdgeSubset.pathCanonical_diff_pairing_closed {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (hc : PathCanonical o) (hc' : PathCanonical o') (f : W.Flag) : f ∈ F.internalFlags → o.isOut f ≠ o'.isOut f → W.pairing f ∈ F.internalFlags

Pairing-closure of the difference set: where two path-canonical orientations disagree, the flag is periodic, so its pairing is internal — exactly the hchain hypothesis of throughSummand_canonical_unique.

theorem RS.EdgeSubset.throughSummand_pathCanonical {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} {o o' : κ.Orientation} (hc : PathCanonical o) (hc' : PathCanonical o') (c : ℕ) : F.throughSummand h st hbnd o c = F.throughSummand h st hbnd o' c

Well-definedness of the canonical summand: the constrained summand agrees across all path-canonical orientations of one relative transition system, unconditionally.