Path matching on boundary flags

For a boundary-relative transition system κ : RelTransitionSystem F, the alternating paths traced by traceChain pair the boundary flags of the edge subset. This file constructs the path matching as a proven involution on boundary flags.

Main results

• RelTransitionSystem.pathMatch — sends each boundary flag to the boundary flag at the other end of its alternating chain.
• pathMatch_mem — the result is a boundary flag.
• pathMatch_invol — pathMatch is an involution.

Proof architecture

Chain termination uses a pigeonhole/backward-injectivity argument on the pairings visited at each step. The involution is proved via an identity on the reverse iterate sequence: iterWalk κ b' j = σ(iterWalk κ b (k - j)) (where b' is the chain result and σ is the edge pairing), established by induction on j using match_invol.

Flag classification helpers

traceChain rewriting lemmas

theorem RS.EdgeSubset.traceChain_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (n : ℕ) (f : W.Flag) (h : W.pairing f ∈ F.internalFlags) : traceChain κ (n + 1) f = traceChain κ n (κ.match_ (W.pairing f))

One step of the chain when the flag's edge partner is internal: match and recurse on one less fuel.

theorem RS.EdgeSubset.traceChain_boundary {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (n : ℕ) (f : W.Flag) (h : W.pairing f ∈ F.boundaryFlags) : traceChain κ (n + 1) f = some (W.pairing f)

The chain stops at the first boundary partner and returns it.

theorem RS.EdgeSubset.traceChain_neither {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (n : ℕ) (f : W.Flag) (hb : W.pairing f ∉ F.boundaryFlags) (hi : W.pairing f ∉ F.internalFlags) : traceChain κ (n + 1) f = none

The chain fails on a partner outside the subset.

Fuel monotonicity

theorem RS.EdgeSubset.traceChain_fuel_mono {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f g : W.Flag} {n m : ℕ} (hnm : n ≤ m) (h : traceChain κ n f = some g) : traceChain κ m f = some g

Extra fuel does not change a successful result.

Result is boundary

theorem RS.EdgeSubset.traceChain_result_boundary {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {f g : W.Flag} {n : ℕ} (h : traceChain κ n f = some g) : g ∈ F.boundaryFlags

A chain that succeeds ends at a boundary flag.

Iterated walk

noncomputable def RS.EdgeSubset.iterWalk {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) : ℕ → W.Flag

The fuel-free chain step iterated: cross the edge, then match. This is traceChain's recursion without the termination test, so the two can be compared step by step.

Equations

• RS.EdgeSubset.iterWalk κ f 0 = f
• RS.EdgeSubset.iterWalk κ f n.succ = κ.match_ (W.pairing (RS.EdgeSubset.iterWalk κ f n))

@[simp]

theorem RS.EdgeSubset.iterWalk_zero {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) : iterWalk κ f 0 = f

No steps leave the flag where it is.

theorem RS.EdgeSubset.iterWalk_succ {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (n : ℕ) : iterWalk κ f (n + 1) = κ.match_ (W.pairing (iterWalk κ f n))

One more step: cross the edge from the current flag, then match.

theorem RS.EdgeSubset.iterWalk_add {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (a b : ℕ) : iterWalk κ f (a + b) = iterWalk κ (iterWalk κ f a) b

Splitting an iterated walk.

theorem RS.EdgeSubset.iterWalk_shift {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (k : ℕ) : iterWalk κ (κ.match_ (W.pairing f)) k = iterWalk κ f (k + 1)

Starting one step along is the same as taking one more step.

theorem RS.EdgeSubset.iterWalk_mem_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (k : ℕ) {j : ℕ} (hj : 1 ≤ j) (hjk : j ≤ k) (hcont : ∀ i < k, W.pairing (iterWalk κ b i) ∈ F.internalFlags) : iterWalk κ b j ∈ F.internalFlags

While the chain continues, every flag it reaches after the first step is internal.

match_ injectivity on internal flags

theorem RS.EdgeSubset.RelTransitionSystem.match_injOn {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {x y : W.Flag} (hx : x ∈ F.internalFlags) (hy : y ∈ F.internalFlags) (h : κ.match_ x = κ.match_ y) : x = y

The matching is injective on internal flags, being an involution there.

Chain unfolding

theorem RS.EdgeSubset.traceChain_unfold {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (f : W.Flag) (k m : ℕ) (hcont : ∀ j < k, W.pairing (iterWalk κ f j) ∈ F.internalFlags) : traceChain κ (k + m + 1) f = traceChain κ (m + 1) (iterWalk κ f k)

Splitting the fuel: k steps of a continuing chain can be run first, leaving the rest of the chain from the flag reached.

Backward injectivity

theorem RS.EdgeSubset.iterWalk_no_repeat {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) (k : ℕ) (hcont : ∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) (i d : ℕ) (hd : 1 ≤ d) (hidk : i + d ≤ k) (heq : iterWalk κ b i = iterWalk κ b (i + d)) : False

A continuing chain never revisits a flag. A repeat would force the matching to send two distinct internal flags to the same place, or the chain to re-enter its own boundary start.

theorem RS.EdgeSubset.pairing_iterWalk_injective {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) (k : ℕ) (hcont : ∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) {i j : ℕ} (hi : i < k) (hj : j < k) (heq : W.pairing (iterWalk κ b i) = W.pairing (iterWalk κ b j)) : i = j

The edge partners visited by a continuing chain are pairwise distinct — the pigeonhole input for termination.

Chain termination with data

theorem RS.EdgeSubset.chain_terminates_with_data {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) : ∃ k ≤ F.flags.card, (∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) ∧ W.pairing (iterWalk κ b k) ∈ F.boundaryFlags

The chain terminates, within F.flags.card steps, at a boundary partner: the visited partners are distinct and there are only that many flags.

traceChain terminates

theorem RS.EdgeSubset.traceChain_terminates {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) : ∃ (g : W.Flag), traceChain κ (F.flags.card + 1) b = some g

With F.flags.card + 1 fuel every chain from a boundary flag succeeds.

pathMatch definition

noncomputable def RS.EdgeSubset.RelTransitionSystem.pathMatch {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (b : W.Flag) (hb : b ∈ F.boundaryFlags) : W.Flag

The path matching: the boundary flag at the other end of a boundary flag's alternating chain.

Equations

• κ.pathMatch b hb = (RS.EdgeSubset.traceChain κ (F.flags.card + 1) b).get ⋯

theorem RS.EdgeSubset.RelTransitionSystem.pathMatch_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b g : W.Flag} (hb : b ∈ F.boundaryFlags) (h : traceChain κ (F.flags.card + 1) b = some g) : κ.pathMatch b hb = g

Reading pathMatch off any successful trace at the standard fuel.

theorem RS.EdgeSubset.RelTransitionSystem.pathMatch_mem {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) : κ.pathMatch b hb ∈ F.boundaryFlags

The path matching lands in the boundary flags.

Forward/reverse chain helpers

theorem RS.EdgeSubset.traceChain_forward {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (b : W.Flag) {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ b k) ∈ F.boundaryFlags) : traceChain κ (k + 1) b = some (W.pairing (iterWalk κ b k))

A chain that continues for k steps and then meets a boundary partner traces to that partner.

theorem RS.EdgeSubset.iterWalk_reverse {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) (j : ℕ) (hjk : j ≤ k) : iterWalk κ (W.pairing (iterWalk κ b k)) j = W.pairing (iterWalk κ b (k - j))

The reverse-iterate identity: walking back from the chain's far end retraces the forward walk under the edge pairing. This is what makes the path matching an involution.

theorem RS.EdgeSubset.reverse_chain_continues {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (_hb : b ∈ F.boundaryFlags) {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) (j : ℕ) (hjk : j < k) : W.pairing (iterWalk κ (W.pairing (iterWalk κ b k)) j) ∈ F.internalFlags

The reversed chain continues wherever the forward one did.

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

The reversed chain arrives back at the original start.

Involution

theorem RS.EdgeSubset.traceChain_reverse {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) {k : ℕ} (hcont : ∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) (hterm : W.pairing (iterWalk κ b k) ∈ F.boundaryFlags) : traceChain κ (k + 1) (W.pairing (iterWalk κ b k)) = some b

The trace from the far end returns the original boundary flag.

theorem RS.EdgeSubset.RelTransitionSystem.pathMatch_invol {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) : κ.pathMatch (κ.pathMatch b hb) ⋯ = b

The path matching is an involution: it pairs the boundary flags of the subset.

Self-matching analysis

theorem RS.EdgeSubset.RelTransitionSystem.pathMatch_eq_pairing {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) (hp : W.pairing b ∈ F.boundaryFlags) : κ.pathMatch b hb = W.pairing b

A boundary flag whose edge partner is also boundary is matched to that partner: the chain has no internal steps.

Interaction lemmas

theorem RS.EdgeSubset.pathMatch_chain_length {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) {b : W.Flag} (hb : b ∈ F.boundaryFlags) : ∃ k ≤ F.flags.card, (∀ j < k, W.pairing (iterWalk κ b j) ∈ F.internalFlags) ∧ κ.pathMatch b hb = W.pairing (iterWalk κ b k)

The path matching, together with the length of the chain that produced it and the continuation data along the way — the form downstream chain arguments consume.