The interface alternates

RS21's step 1 puts the two fragments' arc directions in Eulerian position: at every used interface label one side's arc comes in and the other's goes out. For data the composition itself provides that is automatic — the glued chain passes through the interface, so the glued orientation makes one end incoming and the other outgoing, and ungluing keeps both values.

The statement below is that fact at one cut: where both entry edges are internal — that is, where the label is a chain label on both sides — the unglued orientation's chain directions at the two glued labels are opposite.

theorem RS.EdgeSubset.gluePairOpen_partnerSurvI {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) : (V.gluePairOpen i j hij hopen).pairing (Fragment.partnerSurvI hopen) = Fragment.partnerSurvJ hopen

The glued fragment pairs the two glued flags' partners.

theorem RS.EdgeSubset.chainDir_unglueOpen_alternates {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) (hI : ↑(Fragment.partnerSurvI hopen) ∈ { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.internalFlags) (hJ : ↑(Fragment.partnerSurvJ hopen) ∈ { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.internalFlags) : chainDir (unglueOrientationOpen hij hopen t hct hcL κ' o') (V.boundaryFlag j) = !chainDir (unglueOrientationOpen hij hopen t hct hcL κ' o') (V.boundaryFlag i)

The interface alternates. At a label whose entry edges are internal on both sides, the unglued orientation's chain directions are opposite.

theorem RS.EdgeSubset.internal_ne_boundaryFlag {L : Type} {V : Fragment L} {i j : L} (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) {f : V.Flag} {b : L} (hint : f ∈ { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.internalFlags) : f ≠ V.boundaryFlag b

An internal flag is not a glued boundary flag.

theorem RS.EdgeSubset.chainDir_unglueOpen_surviving {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) (b : Fragment.SurvivingLabel L i j) (hint : V.pairing (V.boundaryFlag ↑b) ∈ { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.internalFlags) : chainDir (unglueOrientationOpen hij hopen t hct hcL κ' o') (V.boundaryFlag ↑b) = chainDir o' ((V.gluePairOpen i j hij hopen).boundaryFlag b)

The chain direction survives the glue. At a surviving label whose entry edge is internal, the unglued orientation reads what the glued one does.

theorem RS.EdgeSubset.chainDir_alternates_unglueOpen {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) (bl br : Fragment.SurvivingLabel L i j) (hIl : V.pairing (V.boundaryFlag ↑bl) ∈ { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.internalFlags) (hIr : V.pairing (V.boundaryFlag ↑br) ∈ { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.internalFlags) (halt : chainDir o' ((V.gluePairOpen i j hij hopen).boundaryFlag br) = !chainDir o' ((V.gluePairOpen i j hij hopen).boundaryFlag bl)) : chainDir (unglueOrientationOpen hij hopen t hct hcL κ' o') (V.boundaryFlag ↑br) = !chainDir (unglueOrientationOpen hij hopen t hct hcL κ' o') (V.boundaryFlag ↑bl)

The alternation passes down an open glue. At a pair of surviving labels whose entry edges are internal, the base inherits the glued fragment's alternation.

Across a through-edge into the cut

Where the entry edge at a surviving label is the cut's own flag — that is, where the label is joined to the cut by a single edge — the glue absorbs that edge and the label's new entry edge is the other side's. The chain direction there is therefore the base's at the other glued label, and this is what carries the interface's alternation along a chain of through-edges.

The closing cut

A closing cut takes its own edge away and touches nothing else: no surviving label's entry edge is one of its flags, and every direction reads through unchanged.

theorem RS.EdgeSubset.chainDir_unglueClosed_surviving {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (b : Bool) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t b, V.pairing f ∈ Fragment.liftSubsetClosed t b) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) (bl : Fragment.SurvivingLabel L i j) : chainDir (unglueOrientationClosed hclosed b t hct hcL κ' o') (V.boundaryFlag ↑bl) = chainDir o' ((V.gluePairClosed i j hclosed).boundaryFlag bl)

The chain direction survives a closing glue.

theorem RS.EdgeSubset.chainDir_alternates_unglueClosed {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (b : Bool) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t b, V.pairing f ∈ Fragment.liftSubsetClosed t b) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) (bl br : Fragment.SurvivingLabel L i j) (halt : chainDir o' ((V.gluePairClosed i j hclosed).boundaryFlag br) = !chainDir o' ((V.gluePairClosed i j hclosed).boundaryFlag bl)) : chainDir (unglueOrientationClosed hclosed b t hct hcL κ' o') (V.boundaryFlag ↑br) = !chainDir (unglueOrientationClosed hclosed b t hct hcL κ' o') (V.boundaryFlag ↑bl)

The alternation passes down a closing glue.

Reading the direction through the transports

The stage's data reaches the base through a relabel and, at the gluePair dispatch, an equality of fragments. Neither touches the orientation's values, so neither touches the chain direction.

theorem RS.EdgeSubset.chainDir_orientOfEq {L : Type} {V : Fragment L} {F F' : EdgeSubset V} (hF : F = F') {κ : F.RelTransitionSystem} (o : κ.Orientation) (f : V.Flag) : chainDir (orientOfEq hF o) f = chainDir o f

Transporting a subset does not move a direction.

noncomputable def RS.EdgeSubset.flagOfEq {L : Type} {V₁ V₂ : Fragment L} (hV : V₁ = V₂) (f : V₁.Flag) : V₂.Flag

Transport a flag along an equality of fragments.

Equations

• RS.EdgeSubset.flagOfEq hV f = hV ▸ f

theorem RS.EdgeSubset.chainDir_dataOfEq {L : Type} [LinearOrder L] {V₁ V₂ : Fragment L} (hV : V₁ = V₂) (𝒟 : DataFamily V₂) (s : Finset V₁.Flag) (hc : ∀ f ∈ s, V₁.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (hc' : ∀ f ∈ flagsOfEq V₁ V₂ hV s, V₂.pairing f ∈ flagsOfEq V₁ V₂ hV s) (hE' : { flags := flagsOfEq V₁ V₂ hV s, pairing_mem := hc' }.Eulerian) (hne' : Nonempty { flags := flagsOfEq V₁ V₂ hV s, pairing_mem := hc' }.CanonData) (f : V₁.Flag) : chainDir (dataOfEq hV 𝒟 s hc hE hne).snd f = chainDir (𝒟 (flagsOfEq V₁ V₂ hV s) hc' hE' hne').snd (flagOfEq hV f)

The direction reads through a transport of the family along an equality of fragments.

theorem RS.EdgeSubset.chainDir_relabelDataDown {L : Type} [LinearOrder L] {V : Fragment L} {β : Type} [LinearOrder β] (e : L ≃o β) (𝒟 : DataFamily (V.relabel e.toEquiv)) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (hc' : ∀ f ∈ s, (V.relabel e.toEquiv).pairing f ∈ s) (hE' : { flags := s, pairing_mem := hc' }.Eulerian) (hne' : Nonempty { flags := s, pairing_mem := hc' }.CanonData) (f : V.Flag) : chainDir (relabelDataDown e 𝒟 s hc hE hne).snd f = chainDir (𝒟 s hc' hE' hne').snd f

The direction reads through a transport of the family along a relabel.

The interface pairs of a stage

The composition glues the pair (inl a, inr a) at each a. Naming those labels lets the alternation be stated for a whole stage, and the two lemmas below are the identifications the iteration needs: the top pair is the stage's own cut, and a lower pair survives it unchanged.

def RS.EdgeSubset.intL (n : ℕ) (a : Fin n) : Fin (0 + n) ⊕ Fin (n + 0)

The left label of the a-th interface pair.

Equations

• RS.EdgeSubset.intL n a = Sum.inl (Fin.cast ⋯ a)

def RS.EdgeSubset.intR (n : ℕ) (a : Fin n) : Fin (0 + n) ⊕ Fin (n + 0)

The right label of the a-th interface pair.

Equations

• RS.EdgeSubset.intR n a = Sum.inr (Fin.cast ⋯ a)

theorem RS.EdgeSubset.intL_last (n : ℕ) : intL (n + 1) (Fin.last n) = cutL n

The top pair is the stage's own cut.

theorem RS.EdgeSubset.intR_last (n : ℕ) : intR (n + 1) (Fin.last n) = cutR n

The top pair is the stage's own cut.

theorem RS.EdgeSubset.intL_castSucc_ne (n : ℕ) (b : Fin n) : intL (n + 1) b.castSucc ≠ cutL n ∧ intL (n + 1) b.castSucc ≠ cutR n

A lower pair survives the stage's cut.

theorem RS.EdgeSubset.intR_castSucc_ne (n : ℕ) (b : Fin n) : intR (n + 1) b.castSucc ≠ cutL n ∧ intR (n + 1) b.castSucc ≠ cutR n

A lower pair survives the stage's cut.

theorem RS.EdgeSubset.interfaceStepEquiv_intL (n : ℕ) (b : Fin n) : (interfaceStepEquiv 0 n 0) ⟨intL (n + 1) b.castSucc, ⋯⟩ = intL n b

The step reads a lower left label as the next stage's.

theorem RS.EdgeSubset.interfaceStepEquiv_intR (n : ℕ) (b : Fin n) : (interfaceStepEquiv 0 n 0) ⟨intR (n + 1) b.castSucc, ⋯⟩ = intR n b

The step reads a lower right label as the next stage's.

The subsets the composition reaches

The glue's own subsets are the base's whose drop is closed under the rewire at every stage. Off those the base's summand vanishes on a diagonal state (rewire_closed_of_liftOpen_closed), so the alternation is only ever wanted on them.

@[reducible]

def RS.EdgeSubset.reachOrder (n : ℕ) : LinearOrder (Fin (0 + n) ⊕ Fin (n + 0))

The lexicographic order on the stage's label type.

Equations

• RS.EdgeSubset.reachOrder n = RS.sumLexLinearOrder (Fin (0 + n)) (Fin (n + 0))

@[reducible]

def RS.EdgeSubset.reachOrderTop : LinearOrder (Fin 0 ⊕ Fin 0)

The order the composition's own (empty) label type carries.

Equations

• RS.EdgeSubset.reachOrderTop = RS.sumLexLinearOrder (Fin 0) (Fin 0)

@[reducible]

def RS.EdgeSubset.reachOrderSucc (n : ℕ) : LinearOrder (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0))

The same order one stage up.

Equations

• RS.EdgeSubset.reachOrderSucc n = RS.sumLexLinearOrder (Fin (0 + n + 1)) (Fin (n + 1 + 0))

def RS.EdgeSubset.Reachable (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : Finset V.Flag → Prop

The subsets the composition reaches.

Equations

• One or more equations did not get rendered due to their size.
• RS.EdgeSubset.Reachable 0 x_3 x_4 = True

theorem RS.EdgeSubset.reachable_succ_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (s : Finset V.Flag) (hr : Reachable (n + 1) V s) : (∀ f ∈ V.dropSubset (cutL n) (cutR n) s, (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ V.dropSubset (cutL n) (cutR n) s) ∧ Reachable n (stepFragment n V) (flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s))

The reach, one stage down, at an open cut.

theorem RS.EdgeSubset.reachable_succ_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (s : Finset V.Flag) (hr : Reachable (n + 1) V s) : Reachable n (stepFragment n V) (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s))

The reach, one stage down, at a closing cut.

theorem RS.EdgeSubset.chainDir_stepDataDown_top (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟step : DataFamily (stepFragment n V)) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hdc : ∀ f ∈ V.dropSubset (cutL n) (cutR n) s, (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ V.dropSubset (cutL n) (cutR n) s) (hIl : V.pairing (V.boundaryFlag (cutL n)) ∈ { flags := s, pairing_mem := hc }.internalFlags) (hIr : V.pairing (V.boundaryFlag (cutR n)) ∈ { flags := s, pairing_mem := hc }.internalFlags) : chainDir (stepDataDown n V 𝒟step s hc hE hne).snd (V.boundaryFlag (cutR n)) = !chainDir (stepDataDown n V 𝒟step s hc hE hne).snd (V.boundaryFlag (cutL n))

The stage's own cut alternates. For a reached subset the pushed-back data is the glued fragment's, unglued, and there the two glued labels' directions are opposite.

theorem RS.EdgeSubset.chainDir_stepDataDown_lower_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟step : DataFamily (stepFragment n V)) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hdc : ∀ f ∈ V.dropSubset (cutL n) (cutR n) s, (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ V.dropSubset (cutL n) (cutR n) s) (bl br : Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)) (hIl : V.pairing (V.boundaryFlag ↑bl) ∈ { flags := s, pairing_mem := hc }.internalFlags) (hIr : V.pairing (V.boundaryFlag ↑br) ∈ { flags := s, pairing_mem := hc }.internalFlags) (hEt : { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := hdc }.Eulerian) (hnet : Nonempty { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := hdc }.CanonData) (halt : chainDir (dataOfEq ⋯ (stepDataGlued n V 𝒟step) (V.dropSubset (cutL n) (cutR n) s) hdc hEt hnet).snd ((V.gluePairOpen (cutL n) (cutR n) ⋯ hop).boundaryFlag br) = !chainDir (dataOfEq ⋯ (stepDataGlued n V 𝒟step) (V.dropSubset (cutL n) (cutR n) s) hdc hEt hnet).snd ((V.gluePairOpen (cutL n) (cutR n) ⋯ hop).boundaryFlag bl)) : chainDir (stepDataDown n V 𝒟step s hc hE hne).snd (V.boundaryFlag ↑br) = !chainDir (stepDataDown n V 𝒟step s hc hE hne).snd (V.boundaryFlag ↑bl)

A lower pair's alternation passes down an open stage.

theorem RS.EdgeSubset.chainDir_stepDataDown_lower_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟step : DataFamily (stepFragment n V)) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (bl br : Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)) (hEt : { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := ⋯ }.Eulerian) (hnet : Nonempty { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := ⋯ }.CanonData) (halt : chainDir (dataOfEq ⋯ (stepDataGlued n V 𝒟step) (V.dropSubset (cutL n) (cutR n) s) ⋯ hEt hnet).snd ((V.gluePairClosed (cutL n) (cutR n) hcl).boundaryFlag br) = !chainDir (dataOfEq ⋯ (stepDataGlued n V 𝒟step) (V.dropSubset (cutL n) (cutR n) s) ⋯ hEt hnet).snd ((V.gluePairClosed (cutL n) (cutR n) hcl).boundaryFlag bl)) : chainDir (stepDataDown n V 𝒟step s hc hE hne).snd (V.boundaryFlag ↑br) = !chainDir (stepDataDown n V 𝒟step s hc hE hne).snd (V.boundaryFlag ↑bl)

A pair's alternation passes down a closing stage.

theorem RS.EdgeSubset.boundaryFlag_not_internal {L' : Type} {W : Fragment L'} (F : EdgeSubset W) (b : L') : W.boundaryFlag b ∉ F.internalFlags

A boundary flag is never internal.

theorem RS.EdgeSubset.flagOfEq_boundaryFlag {L' : Type} {V₁ V₂ : Fragment L'} (hV : V₁ = V₂) (b : L') : flagOfEq hV (V₁.boundaryFlag b) = V₂.boundaryFlag b

Transporting a boundary flag along an equality of fragments.

theorem RS.EdgeSubset.flagsOfEq_pairing_mem {L : Type} {V₁ V₂ : Fragment L} (hV : V₁ = V₂) (t : Finset V₁.Flag) (h : ∀ f ∈ t, V₁.pairing f ∈ t) (f : V₂.Flag) : f ∈ flagsOfEq V₁ V₂ hV t → V₂.pairing f ∈ flagsOfEq V₁ V₂ hV t

Closure transports along an equality of fragments.

theorem RS.EdgeSubset.flagsOfEq_eulerian {L : Type} {V₁ V₂ : Fragment L} (hV : V₁ = V₂) (t : Finset V₁.Flag) (h : ∀ f ∈ t, V₁.pairing f ∈ t) (hEt : { flags := t, pairing_mem := h }.Eulerian) : { flags := flagsOfEq V₁ V₂ hV t, pairing_mem := ⋯ }.Eulerian

Being Eulerian transports along an equality of fragments.

theorem RS.EdgeSubset.flagsOfEq_canon {L : Type} [LinearOrder L] {V₁ V₂ : Fragment L} (hV : V₁ = V₂) (t : Finset V₁.Flag) (h : ∀ f ∈ t, V₁.pairing f ∈ t) (hnet : Nonempty { flags := t, pairing_mem := h }.CanonData) : Nonempty { flags := flagsOfEq V₁ V₂ hV t, pairing_mem := ⋯ }.CanonData

Canonical data transport along an equality of fragments.

theorem RS.EdgeSubset.stepFragment_boundaryFlag (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (b : Fin (0 + n) ⊕ Fin (n + 0)) : (stepFragment n V).boundaryFlag b = (V.gluePair (cutL n) (cutR n) ⋯).boundaryFlag ((interfaceStepEquiv 0 n 0).symm b)

The stage's boundary flag, read on the glued fragment.

theorem RS.EdgeSubset.eulerian_drop_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hdc : ∀ f ∈ V.dropSubset (cutL n) (cutR n) s, (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ V.dropSubset (cutL n) (cutR n) s) : { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := hdc }.Eulerian

The dropped subset is Eulerian at an open stage.

theorem RS.EdgeSubset.canon_drop_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hdc : ∀ f ∈ V.dropSubset (cutL n) (cutR n) s, (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ V.dropSubset (cutL n) (cutR n) s) : Nonempty { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := hdc }.CanonData

The dropped subset carries canonical data at an open stage.

theorem RS.EdgeSubset.eulerian_drop_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := ⋯ }.Eulerian

The dropped subset is Eulerian at a closing stage.

theorem RS.EdgeSubset.canon_drop_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : Nonempty { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := ⋯ }.CanonData

The dropped subset carries canonical data at a closing stage.

theorem RS.EdgeSubset.stage_pairing_mem (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {Vg : Fragment (Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))} (hV : Vg = V.gluePair (cutL n) (cutR n) ⋯) (t : Finset Vg.Flag) (hct : ∀ f ∈ t, Vg.pairing f ∈ t) (f : (V.gluePair (cutL n) (cutR n) ⋯).Flag) : f ∈ flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t → (stepFragment n V).pairing f ∈ flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t

The stage's subset, from the glued fragment's.

theorem RS.EdgeSubset.chainDir_stepDataGlued (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟step : DataFamily (stepFragment n V)) {Vg : Fragment (Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))} (hV : Vg = V.gluePair (cutL n) (cutR n) ⋯) (t : Finset Vg.Flag) (hct : ∀ f ∈ t, Vg.pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hES : { flags := flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t, pairing_mem := ⋯ }.Eulerian) (hneS : Nonempty { flags := flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t, pairing_mem := ⋯ }.CanonData) (bl : Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)) : chainDir (dataOfEq hV (stepDataGlued n V 𝒟step) t hct hEt hnet).snd (Vg.boundaryFlag bl) = chainDir (𝒟step (flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t) ⋯ hES hneS).snd ((stepFragment n V).boundaryFlag ((interfaceStepEquiv 0 n 0) bl))

The stage's data, read on the glued fragment. The dispatch's identification and the stage's relabel both leave the direction alone, so a direction at the glued fragment is the stage's at the relabelled label.

theorem RS.EdgeSubset.internal_stage_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (bl : Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)) (hI : V.pairing (V.boundaryFlag ↑bl) ∈ { flags := s, pairing_mem := hc }.internalFlags) : (V.gluePairClosed (cutL n) (cutR n) hcl).pairing ((V.gluePairClosed (cutL n) (cutR n) hcl).boundaryFlag bl) ∈ { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := ⋯ }.internalFlags

Internality passes from the base to the stage, at a closing cut.

theorem RS.EdgeSubset.internal_stage_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hdc : ∀ f ∈ V.dropSubset (cutL n) (cutR n) s, (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ V.dropSubset (cutL n) (cutR n) s) (bl : Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)) (hI : V.pairing (V.boundaryFlag ↑bl) ∈ { flags := s, pairing_mem := hc }.internalFlags) : (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing ((V.gluePairOpen (cutL n) (cutR n) ⋯ hop).boundaryFlag bl) ∈ { flags := V.dropSubset (cutL n) (cutR n) s, pairing_mem := hdc }.internalFlags

Internality passes from the base to the stage, at an open cut.

theorem RS.EdgeSubset.stage_eulerian (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {Vg : Fragment (Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))} (hV : Vg = V.gluePair (cutL n) (cutR n) ⋯) (t : Finset Vg.Flag) (hct : ∀ f ∈ t, Vg.pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) : { flags := flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t, pairing_mem := ⋯ }.Eulerian

Being Eulerian passes to the stage.

theorem RS.EdgeSubset.stage_canon (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {Vg : Fragment (Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))} (hV : Vg = V.gluePair (cutL n) (cutR n) ⋯) (t : Finset Vg.Flag) (hct : ∀ f ∈ t, Vg.pairing f ∈ t) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) : Nonempty { flags := flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t, pairing_mem := ⋯ }.CanonData

Canonical data passes to the stage.

theorem RS.EdgeSubset.stage_internal (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {Vg : Fragment (Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))} (hV : Vg = V.gluePair (cutL n) (cutR n) ⋯) (t : Finset Vg.Flag) (hct : ∀ f ∈ t, Vg.pairing f ∈ t) (bl : Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)) (hf : Vg.pairing (Vg.boundaryFlag bl) ∈ { flags := t, pairing_mem := hct }.internalFlags) : (stepFragment n V).pairing ((stepFragment n V).boundaryFlag ((interfaceStepEquiv 0 n 0) bl)) ∈ { flags := flagsOfEq Vg (V.gluePair (cutL n) (cutR n) ⋯) hV t, pairing_mem := ⋯ }.internalFlags

Internality passes to the stage.

theorem RS.EdgeSubset.chainDir_pushData_alternates (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (𝒟 : DataFamily (glueInterface 0 n 0 V)) (s : Finset V.Flag) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (_hr : Reachable n V s) (a : Fin n) : V.pairing (V.boundaryFlag (intL n a)) ∈ { flags := s, pairing_mem := hc }.internalFlags → V.pairing (V.boundaryFlag (intR n a)) ∈ { flags := s, pairing_mem := hc }.internalFlags → chainDir (pushData n V 𝒟 s hc hE hne).snd (V.boundaryFlag (intR n a)) = !chainDir (pushData n V 𝒟 s hc hE hne).snd (V.boundaryFlag (intL n a))

The interface alternates. At a reached subset, the data the composition pushes back to the base gives opposite directions at the two ends of every interface pair whose partners are both internal.

This is RS21's step 1: the composition's Eulerian orientation, read on the base, enters at one end of each glued pair and leaves at the other.