The interface round trip

At an open cut the lift is a left inverse of the drop, and the family pushed back down is the family itself. Iterating over the interface gives the composition's sum in terms of the base's own subsets.

@[reducible]

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

The lexicographic order on the interface's label type.

Equations

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

@[reducible]

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

The same order one stage up.

Equations

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

@[reducible]

def RS.EdgeSubset.tripSurvOrder (n : ℕ) : LinearOrder (Fragment.SurvivingLabel (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))

The order a stage's surviving labels carry.

Equations

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

@[reducible]

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

The order the composition's own label type carries.

Equations

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

An open cut loses nothing

At an open cut the lift is a left inverse of the drop, so the drop is injective on subsets closed under the pairing. This is why a fibre is a singleton when no cut on the way to it closes.

theorem RS.EdgeSubset.dropSubset_rewire_closed_of_matches {k ℓ : ℕ} (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) (x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ)) (hm : genBoundarySubsetMatches V s (diagOf (n + 1) x)) (f : V.SurvivingFlag (cutL n) (cutR n)) : f ∈ V.dropSubset (cutL n) (cutR n) s → (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ V.dropSubset (cutL n) (cutR n) s

A closed subset matching a diagonal state has a rewire-closed drop. So the terms the identity reads are the reached ones, and off them everything vanishes.

theorem RS.EdgeSubset.dropSubset_matches_of_matches {k ℓ : ℕ} (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) (x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ)) (hm : genBoundarySubsetMatches V s (diagOf (n + 1) x)) : genBoundarySubsetMatches (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.dropSubset (cutL n) (cutR n) s) (stageState n (diagOf n fun (a : Fin n) => x a.castSucc))

The drop matches the stage's diagonal state. So the boundary constraint descends the interface along with the subset.

theorem RS.EdgeSubset.genBoundarySubsetMatches_flagsOfEq {k ℓ : ℕ} {L : Type} {V₁ V₂ : Fragment L} (hV : V₁ = V₂) (s : Finset V₁.Flag) (st : GenBoundaryState k ℓ L) (h : genBoundarySubsetMatches V₁ s st) : genBoundarySubsetMatches V₂ (flagsOfEq V₁ V₂ hV s) st

The boundary constraint transports along an equality of fragments.

theorem RS.EdgeSubset.stage_matches_of_matches {k ℓ : ℕ} (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) (x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ)) (hm : genBoundarySubsetMatches V s (diagOf (n + 1) x)) : genBoundarySubsetMatches (stepFragment n V) (flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s)) (diagOf n fun (a : Fin n) => x a.castSucc)

The stage subset matches the stage's diagonal state. This is dropSubset_matches_of_matches read at the stage fragment, across the relabel that renumbers the surviving labels.

theorem RS.EdgeSubset.isOut_unglueDataOpen_congr_at {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟₁ 𝒟₂ : DataFamily (V.gluePairOpen i j hij hopen)) {s : Finset V.Flag} (hm : ∀ (hct : ∀ f ∈ V.dropSubset i j s, (V.gluePairOpen i j hij hopen).pairing f ∈ V.dropSubset i j s) (hEt : { flags := V.dropSubset i j s, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := V.dropSubset i j s, pairing_mem := hct }.CanonData) (g : V.SurvivingFlag i j), (∀ (ℓ : Fragment.SurvivingLabel α i j), g ≠ (V.gluePairOpen i j hij hopen).boundaryFlag ℓ) → (𝒟₁ (V.dropSubset i j s) hct hEt hnet).snd.isOut g = (𝒟₂ (V.dropSubset i j s) hct hEt hnet).snd.isOut g) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (f : V.Flag) (hfb : ∀ (a : α), f ≠ V.boundaryFlag a) : (unglueDataOpen hij hopen 𝒟₁ s hc hE hne).snd.isOut f = (unglueDataOpen hij hopen 𝒟₂ s hc hE hne).snd.isOut f

One subset is enough for the directions, at an open cut.

theorem RS.EdgeSubset.isOut_unglueDataClosed_congr_at {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (𝒟₁ 𝒟₂ : DataFamily (V.gluePairClosed i j hclosed)) {s : Finset V.Flag} (hm : ∀ (hct : ∀ f ∈ V.dropSubset i j s, (V.gluePairClosed i j hclosed).pairing f ∈ V.dropSubset i j s) (hEt : { flags := V.dropSubset i j s, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := V.dropSubset i j s, pairing_mem := hct }.CanonData) (g : V.SurvivingFlag i j), (∀ (ℓ : Fragment.SurvivingLabel α i j), g ≠ (V.gluePairClosed i j hclosed).boundaryFlag ℓ) → (𝒟₁ (V.dropSubset i j s) hct hEt hnet).snd.isOut g = (𝒟₂ (V.dropSubset i j s) hct hEt hnet).snd.isOut g) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (f : V.Flag) (hfb : ∀ (a : α), f ≠ V.boundaryFlag a) : (unglueDataClosed hij hclosed 𝒟₁ s hc hE hne).snd.isOut f = (unglueDataClosed hij hclosed 𝒟₂ s hc hE hne).snd.isOut f

One subset is enough for the directions, at a closing cut.

theorem RS.EdgeSubset.isOut_dataOfEq_congr_at {L : Type} [LinearOrder L] {V₁ V₂ : Fragment L} (h : V₁ = V₂) (𝒟₁ 𝒟₂ : DataFamily V₂) (s : Finset V₁.Flag) (hm : ∀ (hc' : ∀ f ∈ flagsOfEq V₁ V₂ h s, V₂.pairing f ∈ flagsOfEq V₁ V₂ h s) (hE' : { flags := flagsOfEq V₁ V₂ h s, pairing_mem := hc' }.Eulerian) (hne' : Nonempty { flags := flagsOfEq V₁ V₂ h s, pairing_mem := hc' }.CanonData) (g : V₂.Flag), (∀ (ℓ : L), g ≠ V₂.boundaryFlag ℓ) → (𝒟₁ (flagsOfEq V₁ V₂ h s) hc' hE' hne').snd.isOut g = (𝒟₂ (flagsOfEq V₁ V₂ h s) hc' hE' hne').snd.isOut g) (hc : ∀ f ∈ s, V₁.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (f : V₁.Flag) (hfb : ∀ (ℓ : L), f ≠ V₁.boundaryFlag ℓ) : (dataOfEq h 𝒟₁ s hc hE hne).snd.isOut f = (dataOfEq h 𝒟₂ s hc hE hne).snd.isOut f

One subset is enough for the directions, under a transport.

theorem RS.EdgeSubset.isOut_relabelDataDown_congr_at {α' β' : Type} [LinearOrder α'] [LinearOrder β'] (e : α' ≃o β') {W' : Fragment α'} (𝒟₁ 𝒟₂ : DataFamily (W'.relabel e.toEquiv)) (s : Finset W'.Flag) (hm : ∀ (hc' : ∀ f ∈ s, (W'.relabel e.toEquiv).pairing f ∈ s) (hE' : { flags := s, pairing_mem := hc' }.Eulerian) (hne' : Nonempty { flags := s, pairing_mem := hc' }.CanonData) (g : W'.Flag), (∀ (b : β'), g ≠ (W'.relabel e.toEquiv).boundaryFlag b) → (𝒟₁ s hc' hE' hne').snd.isOut g = (𝒟₂ s hc' hE' hne').snd.isOut g) (hc : ∀ f ∈ s, W'.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (f : W'.Flag) (hfb : ∀ (a : α'), f ≠ W'.boundaryFlag a) : (relabelDataDown e 𝒟₁ s hc hE hne).snd.isOut f = (relabelDataDown e 𝒟₂ s hc hE hne).snd.isOut f

One subset is enough for the directions, under a relabel.

theorem RS.EdgeSubset.isOut_stepDataDown_congr_at_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (𝒟₁ 𝒟₂ : DataFamily (stepFragment n V)) {s : Finset V.Flag} (hm : ∀ (t : Finset (stepFragment n V).Flag), t = flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s) → ∀ (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (g : (stepFragment n V).Flag), (∀ (b : Fin (0 + n) ⊕ Fin (n + 0)), g ≠ (stepFragment n V).boundaryFlag b) → (𝒟₁ t hct hEt hnet).snd.isOut g = (𝒟₂ t hct hEt hnet).snd.isOut g) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (f : V.Flag) (hfb : ∀ (a : Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)), f ≠ V.boundaryFlag a) : (stepDataDown n V 𝒟₁ s hc hE hne).snd.isOut f = (stepDataDown n V 𝒟₂ s hc hE hne).snd.isOut f

One subset is enough for the directions, for a whole stage of the push at an open cut.

theorem RS.EdgeSubset.isOut_stepDataDown_congr_at_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (𝒟₁ 𝒟₂ : DataFamily (stepFragment n V)) {s : Finset V.Flag} (hm : ∀ (t : Finset (stepFragment n V).Flag), t = flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s) → ∀ (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (g : (stepFragment n V).Flag), (∀ (b : Fin (0 + n) ⊕ Fin (n + 0)), g ≠ (stepFragment n V).boundaryFlag b) → (𝒟₁ t hct hEt hnet).snd.isOut g = (𝒟₂ t hct hEt hnet).snd.isOut g) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (f : V.Flag) (hfb : ∀ (a : Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)), f ≠ V.boundaryFlag a) : (stepDataDown n V 𝒟₁ s hc hE hne).snd.isOut f = (stepDataDown n V 𝒟₂ s hc hE hne).snd.isOut f

One subset is enough for the directions, for a whole stage of the push at a closing cut.

theorem RS.EdgeSubset.isOut_pushData_liftData_zero (V : Fragment (Fin (0 + 0) ⊕ Fin (0 + 0))) (bits : Fin 0 → Bool) (𝒟 : 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) (f : V.Flag) : (pushData 0 V (liftData 0 V bits 𝒟) s hc hE hne).snd.isOut f = (𝒟 s hc hE hne).snd.isOut f

The interface round trip on directions, at no cuts.

theorem RS.EdgeSubset.isOut_pushData_liftData_succ_open_at (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (bits : Fin (n + 1) → Bool) (𝒟 : 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) (hIH : ∀ (t : Finset (stepFragment n V).Flag), t = flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s) → ∀ (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (g : (stepFragment n V).Flag), (∀ (b : Fin (0 + n) ⊕ Fin (n + 0)), g ≠ (stepFragment n V).boundaryFlag b) → (pushData n (stepFragment n V) (liftData n (stepFragment n V) (fun (a : Fin n) => bits a.castSucc) (stepDataUp n V (bits (Fin.last n)) 𝒟)) t hct hEt hnet).snd.isOut g = (stepDataUp n V (bits (Fin.last n)) 𝒟 t hct hEt hnet).snd.isOut g) (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) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hop (V.dropSubset (cutL n) (cutR n) s), V.pairing f ∈ Fragment.liftSubsetOpen hop (V.dropSubset (cutL n) (cutR n) s)) (hEL : { flags := Fragment.liftSubsetOpen hop (V.dropSubset (cutL n) (cutR n) s), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hop (V.dropSubset (cutL n) (cutR n) s), pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hop (V.dropSubset (cutL n) (cutR n) s)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutR n))) = !(𝒟 (Fragment.liftSubsetOpen hop (V.dropSubset (cutL n) (cutR n) s)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutL n)))) (f : V.Flag) (hfb : ∀ (a : Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)), f ≠ V.boundaryFlag a) : (pushData (n + 1) V (liftData (n + 1) V bits 𝒟) s hc hE hne).snd.isOut f = (𝒟 s hc hE hne).snd.isOut f

The interface round trip on directions, one stage on — at an open cut. Away from the cut's own two flags the directions come back on the nose.

theorem RS.EdgeSubset.glueOpen_matchEq {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s') {κ₁ κ₂ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem} (hm : κ₁.MatchEq κ₂) : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ₁).MatchEq (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ₂)

The upward glue respects matching equality. At an internal flag the glued system's partner is the base system's, so two systems that agree there glue to systems that agree.

theorem RS.EdgeSubset.glueClosed_matchEq {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (b : Bool) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) {κ₁ κ₂ : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem} (hm : κ₁.MatchEq κ₂) : (RelTransitionSystem.glueClosed hclosed b s' hc' hc κ₁).MatchEq (RelTransitionSystem.glueClosed hclosed b s' hc' hc κ₂)

The closing glue respects matching equality. It keeps every internal flag's partner, so two systems that agree there glue to systems that agree.

theorem RS.EdgeSubset.relabelTransUp_matchEq {α' β' : Type} (ee : α' ≃ β') {W' : Fragment α'} (F : EdgeSubset W') {κ₁ κ₂ : F.RelTransitionSystem} (hm : κ₁.MatchEq κ₂) : (relabelTransUp ee F κ₁).MatchEq (relabelTransUp ee F κ₂)

The upward relabel respects matching equality. It keeps the partner map and only renames the labels.

theorem RS.EdgeSubset.match_glueDataOpen_stepDataOpen (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (𝒟 : DataFamily V) (D : StageData (n + 1) V) (hcompat : ∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData), (𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel) (hag : ∀ (hcL : ∀ f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D), V.pairing f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D)) (hEL : { flags := Fragment.liftSubsetOpen hop (stepFlags n V D), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hop (stepFlags n V D), pairing_mem := hcL }.CanonData), (𝒟 (Fragment.liftSubsetOpen hop (stepFlags n V D)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutR n))) = !(𝒟 (Fragment.liftSubsetOpen hop (stepFlags n V D)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutL n)))) (hct : ∀ f ∈ stepFlags n V D, (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ stepFlags n V D) (hEt : { flags := stepFlags n V D, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := stepFlags n V D, pairing_mem := hct }.CanonData) : (glueDataOpen ⋯ hop 𝒟 (stepFlags n V D) hct hEt hnet).fst.MatchEq (RelTransitionSystem.glueOpen ⋯ hop (stepFlags n V D) hct ⋯ (relOfEq ⋯ D.rel))

The family's upward glue is the ledger's, at an open cut: a family whose data at the stage's subset match the stage's system glues to a system matching the ledger's glue.

theorem RS.EdgeSubset.flagsOfEq_symm {L : Type} {V₁ V₂ : Fragment L} (h : V₁ = V₂) (t : Finset V₁.Flag) : flagsOfEq V₂ V₁ ⋯ (flagsOfEq V₁ V₂ h t) = t

The transport of a subset, undone.

theorem RS.EdgeSubset.relabelDataUp_dataOfEq {L L' : Type} [LinearOrder L] [LinearOrder L'] (e : L ≃o L') {W₁ W₂ : Fragment L} (hW : W₁ = W₂) (𝒳 : DataFamily W₂) : relabelDataUp e (dataOfEq hW 𝒳) = dataOfEq ⋯ (relabelDataUp e 𝒳)

The upward relabel and a transport commute.

theorem RS.EdgeSubset.match_dataOfEq_stageDataOfEq {m : ℕ} {V₁ V₂ : Fragment (Fin (0 + m) ⊕ Fin (m + 0))} (hV : V₁ = V₂) (Dm : StageData m V₁) (𝒴 : DataFamily V₁) (hm : ∀ (hc : ∀ f ∈ Dm.sub.flags, V₁.pairing f ∈ Dm.sub.flags) (hE : { flags := Dm.sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := Dm.sub.flags, pairing_mem := hc }.CanonData), (𝒴 Dm.sub.flags hc hE hne).fst.MatchEq Dm.rel) (hc : ∀ f ∈ (stageDataOfEq hV Dm).sub.flags, V₂.pairing f ∈ (stageDataOfEq hV Dm).sub.flags) (hE : { flags := (stageDataOfEq hV Dm).sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := (stageDataOfEq hV Dm).sub.flags, pairing_mem := hc }.CanonData) : (dataOfEq ⋯ 𝒴 (stageDataOfEq hV Dm).sub.flags hc hE hne).fst.MatchEq (stageDataOfEq hV Dm).rel

Both sides transported alike. A family that matches a stage datum still matches it after both are carried along an equality of fragments.

theorem RS.EdgeSubset.match_relabelDataUp_stepDataOpen (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (𝒟 : DataFamily V) (D : StageData (n + 1) V) (hcompat : ∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData), (𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel) (hag : ∀ (hcL : ∀ f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D), V.pairing f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D)) (hEL : { flags := Fragment.liftSubsetOpen hop (stepFlags n V D), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hop (stepFlags n V D), pairing_mem := hcL }.CanonData), (𝒟 (Fragment.liftSubsetOpen hop (stepFlags n V D)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutR n))) = !(𝒟 (Fragment.liftSubsetOpen hop (stepFlags n V D)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutL n)))) (hc : ∀ f ∈ (stepDataOpen n V D hop).sub.flags, ((V.gluePairOpen (cutL n) (cutR n) ⋯ hop).relabel (interfaceStepEquiv 0 n 0)).pairing f ∈ (stepDataOpen n V D hop).sub.flags) (hE : { flags := (stepDataOpen n V D hop).sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := (stepDataOpen n V D hop).sub.flags, pairing_mem := hc }.CanonData) : (relabelDataUp (stepIso n) (glueDataOpen ⋯ hop 𝒟) (stepDataOpen n V D hop).sub.flags hc hE hne).fst.MatchEq (stepDataOpen n V D hop).rel

The lifted family matches the ledger's step, before the transport that the dispatch on the cut demands.

theorem RS.EdgeSubset.match_stepDataUp_stepData_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (b : Bool) (𝒟 : DataFamily V) (D : StageData (n + 1) V) (hcompat : ∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData), (𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel) (hag : ∀ (hcL : ∀ f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D), V.pairing f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D)) (hEL : { flags := Fragment.liftSubsetOpen hop (stepFlags n V D), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hop (stepFlags n V D), pairing_mem := hcL }.CanonData), (𝒟 (Fragment.liftSubsetOpen hop (stepFlags n V D)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutR n))) = !(𝒟 (Fragment.liftSubsetOpen hop (stepFlags n V D)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutL n)))) (hct : ∀ f ∈ (stepData n V D).sub.flags, (stepFragment n V).pairing f ∈ (stepData n V D).sub.flags) (hEt : { flags := (stepData n V D).sub.flags, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := (stepData n V D).sub.flags, pairing_mem := hct }.CanonData) : (stepDataUp n V b 𝒟 (stepData n V D).sub.flags hct hEt hnet).fst.MatchEq (stepData n V D).rel

One stage of the lift matches one stage of the ledger. At an open cut the family's glue and the ledger's step are the same system up to its partner map, transports and relabel included.

theorem RS.EdgeSubset.match_glueDataClosed_stepDataClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (𝒟 : DataFamily V) (D : StageData (n + 1) V) (hcompat : ∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData), (𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel) (hct : ∀ f ∈ stepFlags n V D, (V.gluePairClosed (cutL n) (cutR n) hcl).pairing f ∈ stepFlags n V D) (hEt : { flags := stepFlags n V D, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := stepFlags n V D, pairing_mem := hct }.CanonData) : (glueDataClosed hcl (stepBit n V D) 𝒟 (stepFlags n V D) hct hEt hnet).fst.MatchEq (RelTransitionSystem.glueClosed hcl (stepBit n V D) (stepFlags n V D) hct ⋯ (relOfEq ⋯ D.rel))

The family's upward glue is the ledger's, at a closing cut. The ledger's own bit is the one the subset determines, and with it the glue reads the family at exactly the ledger's subset.

theorem RS.EdgeSubset.match_relabelDataUp_stepDataClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (𝒟 : DataFamily V) (D : StageData (n + 1) V) (hcompat : ∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData), (𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel) (hc : ∀ f ∈ (stepDataClosed n V D hcl).sub.flags, ((V.gluePairClosed (cutL n) (cutR n) hcl).relabel (interfaceStepEquiv 0 n 0)).pairing f ∈ (stepDataClosed n V D hcl).sub.flags) (hE : { flags := (stepDataClosed n V D hcl).sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := (stepDataClosed n V D hcl).sub.flags, pairing_mem := hc }.CanonData) : (relabelDataUp (stepIso n) (glueDataClosed hcl (stepBit n V D) 𝒟) (stepDataClosed n V D hcl).sub.flags hc hE hne).fst.MatchEq (stepDataClosed n V D hcl).rel

The lifted family matches the ledger's step, at a closing cut, before the transport the dispatch demands.

theorem RS.EdgeSubset.match_stepDataUp_stepData_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (𝒟 : DataFamily V) (D : StageData (n + 1) V) (hcompat : ∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData), (𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel) (hct : ∀ f ∈ (stepData n V D).sub.flags, (stepFragment n V).pairing f ∈ (stepData n V D).sub.flags) (hEt : { flags := (stepData n V D).sub.flags, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := (stepData n V D).sub.flags, pairing_mem := hct }.CanonData) : (stepDataUp n V (stepBit n V D) 𝒟 (stepData n V D).sub.flags hct hEt hnet).fst.MatchEq (stepData n V D).rel

One stage of the lift matches one stage of the ledger, at a closing cut: with the subset's own bit the family's glue and the ledger's step are the same system up to its partner map.

theorem RS.EdgeSubset.flagOfEq_symm {L : Type} {V₁ V₂ : Fragment L} (h : V₁ = V₂) (f : V₁.Flag) : flagOfEq ⋯ (flagOfEq h f) = f

The transport of a flag, undone.

theorem RS.EdgeSubset.flagOfEq_pairing {L : Type} {V₁ V₂ : Fragment L} (h : V₁ = V₂) (f : V₁.Flag) : flagOfEq h (V₁.pairing f) = V₂.pairing (flagOfEq h f)

The transport commutes with the pairing.

theorem RS.EdgeSubset.isOut_dataOfEq_apply {L : Type} [LinearOrder L] {V₁ V₂ : Fragment L} (h : 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₂ h s, V₂.pairing f ∈ flagsOfEq V₁ V₂ h s) (hE' : { flags := flagsOfEq V₁ V₂ h s, pairing_mem := hc' }.Eulerian) (hne' : Nonempty { flags := flagsOfEq V₁ V₂ h s, pairing_mem := hc' }.CanonData) (f : V₁.Flag) : (dataOfEq h 𝒟 s hc hE hne).snd.isOut f = (𝒟 (flagsOfEq V₁ V₂ h s) hc' hE' hne').snd.isOut (flagOfEq h f)

A transported family's directions, evaluated.

theorem RS.EdgeSubset.isOut_stepDataUp_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (b : Bool) (𝒟 : DataFamily V) (u : Finset (V.SurvivingFlag (cutL n) (cutR n))) (t : Finset (stepFragment n V).Flag) (ht : t = flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ u) (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hop u, V.pairing f ∈ Fragment.liftSubsetOpen hop u) (hEL : { flags := Fragment.liftSubsetOpen hop u, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hop u, pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutR n))) = !(𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutL n)))) (f' : V.SurvivingFlag (cutL n) (cutR n)) (g : (stepFragment n V).Flag) (hg : g = flagOfEq ⋯ f') : (stepDataUp n V b 𝒟 t hct hEt hnet).snd.isOut g = (𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut ↑f'

A stage of the lift keeps the base's directions. At a surviving flag the glued family reads the direction the base family gave it, so the alignment at deeper cuts is the base's own.

theorem RS.EdgeSubset.isOut_stepDataUp_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (b : Bool) (𝒟 : DataFamily V) (u : Finset (V.SurvivingFlag (cutL n) (cutR n))) (t : Finset (stepFragment n V).Flag) (ht : t = flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ u) (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetClosed u b, V.pairing f ∈ Fragment.liftSubsetClosed u b) (hEL : { flags := Fragment.liftSubsetClosed u b, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetClosed u b, pairing_mem := hcL }.CanonData) (f' : V.SurvivingFlag (cutL n) (cutR n)) (g : (stepFragment n V).Flag) (hg : g = flagOfEq ⋯ f') : (stepDataUp n V b 𝒟 t hct hEt hnet).snd.isOut g = (𝒟 (Fragment.liftSubsetClosed u b) hcL hEL hneL).snd.isOut ↑f'

The stage's directions at a closing cut are the base family's, read at the lift with the stage's bit. Nothing is rewired, so no alternation is asked for.

theorem RS.EdgeSubset.boundaryFlag_stepFragment_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (bl : Fin (0 + n) ⊕ Fin (n + 0)) : (stepFragment n V).boundaryFlag bl = flagOfEq ⋯ ((V.gluePairOpen (cutL n) (cutR n) ⋯ hop).boundaryFlag ((interfaceStepEquiv 0 n 0).symm bl))

The stage's boundary flag is the base's, carried across the transport the dispatch on the cut demands.

theorem RS.EdgeSubset.isOut_rewire_eq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (hflip : ∀ (ℓ : α), o.isOut (W.pairing (W.boundaryFlag ℓ)) = !o.isOut (W.boundaryFlag ℓ)) (halign : o.isOut (W.pairing (W.boundaryFlag j)) = !o.isOut (W.pairing (W.boundaryFlag i))) (ℓ : α) (h1 : W.boundaryFlag ℓ ≠ W.boundaryFlag i) (h2 : W.boundaryFlag ℓ ≠ W.boundaryFlag j) : o.isOut ↑(Fragment.rewire hopen ⟨W.boundaryFlag ℓ, ⋯⟩) = o.isOut (W.pairing (W.boundaryFlag ℓ))

The glue does not move the chain directions. With the pairing flipping at every boundary flag and the cut's own two ends oppositely directed, the rewired partner of a surviving label carries the direction the base's partner carried: crossing the cut costs two flips, and two flips are none.

theorem RS.EdgeSubset.pairing_boundaryFlag_stepFragment (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (bl : Fin (0 + n) ⊕ Fin (n + 0)) : (stepFragment n V).pairing ((stepFragment n V).boundaryFlag bl) = flagOfEq ⋯ (Fragment.rewire hop ⟨V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl), ⋯⟩)

The stage's boundary partner is the rewired one. The glue sends a surviving boundary flag to its rewired partner, which is the base's partner except across the cut's own edge.

theorem RS.EdgeSubset.chainDir_stepDataUp_eq (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (b : Bool) (𝒟 : DataFamily V) (u : Finset (V.SurvivingFlag (cutL n) (cutR n))) (t : Finset (stepFragment n V).Flag) (ht : t = flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ u) (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hop u, V.pairing f ∈ Fragment.liftSubsetOpen hop u) (hEL : { flags := Fragment.liftSubsetOpen hop u, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hop u, pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutR n))) = !(𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutL n)))) (hflip : ∀ (ℓ : Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)), (𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag ℓ)) = !(𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.boundaryFlag ℓ)) (bl : Fin (0 + n) ⊕ Fin (n + 0)) : (stepDataUp n V b 𝒟 t hct hEt hnet).snd.isOut ((stepFragment n V).pairing ((stepFragment n V).boundaryFlag bl)) = (𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl)))

A stage of the lift keeps the base's chain directions. The stage's boundary partner is the rewired one, the glue does not move the directions, and the lifted family reads the base's own — so the alternation the next cut needs is the base's at the same label.

theorem RS.EdgeSubset.interfaceStepEquiv_symm_intL (n : ℕ) (m : Fin n) : ↑((interfaceStepEquiv 0 n 0).symm (intL n m)) = intL (n + 1) m.castSucc

The stage's m-th left label is the base's.

theorem RS.EdgeSubset.interfaceStepEquiv_symm_intR (n : ℕ) (m : Fin n) : ↑((interfaceStepEquiv 0 n 0).symm (intR n m)) = intR (n + 1) m.castSucc

The stage's m-th right label is the base's.

theorem RS.EdgeSubset.isOut_stepDataUp_boundaryFlag (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (b : Bool) (𝒟 : DataFamily V) (u : Finset (V.SurvivingFlag (cutL n) (cutR n))) (t : Finset (stepFragment n V).Flag) (ht : t = flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ u) (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hop u, V.pairing f ∈ Fragment.liftSubsetOpen hop u) (hEL : { flags := Fragment.liftSubsetOpen hop u, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hop u, pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutR n))) = !(𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag (cutL n)))) (bl : Fin (0 + n) ⊕ Fin (n + 0)) : (stepDataUp n V b 𝒟 t hct hEt hnet).snd.isOut ((stepFragment n V).boundaryFlag bl) = (𝒟 (Fragment.liftSubsetOpen hop u) hcL hEL hneL).snd.isOut (V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl))

A stage of the lift keeps the base's boundary directions.

theorem RS.EdgeSubset.isOut_cut_iff_boundary {n : ℕ} {V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))} {B : EdgeSubset V} {κ : B.RelTransitionSystem} (o : κ.Orientation) (hflip : ∀ (ℓ : Fin (0 + n) ⊕ Fin (n + 0)), o.isOut (V.pairing (V.boundaryFlag ℓ)) = !o.isOut (V.boundaryFlag ℓ)) (m : Fin n) : o.isOut (V.pairing (V.boundaryFlag (intR n m))) = !o.isOut (V.pairing (V.boundaryFlag (intL n m))) ↔ o.isOut (V.boundaryFlag (intR n m)) = !o.isOut (V.boundaryFlag (intL n m))

The cut alternation, read at the cut's own flags. Once the pairing flips at every boundary flag, the two ends of a cut are oppositely directed exactly when the cut's two boundary flags are — one flip on each side.

def RS.EdgeSubset.CutBalanced {n : ℕ} (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (u : Finset V.Flag) : Prop

A subset is cut-balanced when it uses the two labels of each interface pair together.

Equations

• RS.EdgeSubset.CutBalanced V u = ∀ (m : Fin n), V.boundaryFlag (RS.EdgeSubset.intL n m) ∈ u ↔ V.boundaryFlag (RS.EdgeSubset.intR n m) ∈ u

theorem RS.EdgeSubset.cutBalanced_of_matches_diag {k ℓ n : ℕ} {V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))} {u : Finset V.Flag} (x : Fin n → Fin k ⊕ Fin (2 * ℓ)) (hbnd : genBoundarySubsetMatches V u (diagOf n x)) : CutBalanced V u

A subset matching a diagonal state is cut-balanced. The diagonal gives a pair's two labels the same colour, so the subset uses both or neither.

def RS.EdgeSubset.BaseDirections {n : ℕ} (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (𝒟 : DataFamily V) : Prop

The base's directions, as the lift consumes them. The pairing flips at every boundary flag, and the two ends of every interface pair are oppositely directed.

Equations

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

theorem RS.EdgeSubset.exists_edge_colouring {α : Type} (V : Fragment α) : ∃ (c : V.Flag → Bool), ∀ (f : V.Flag), c (V.pairing f) = !c f

Every fragment's edges can be two-coloured. The pairing is a fixed-point-free involution, so comparing a flag's index with its partner's orients every edge.

The stage at a closing cut

A closing cut rewires nothing: its two flags bound one edge, which the glue turns into a free circle, and every other flag keeps the partner it had. So a flag survives the cut exactly when its partner does, and the stage's pairing is the base's.

theorem RS.EdgeSubset.pairing_ne_cutL_of_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (f : V.Flag) (h2 : f ≠ V.boundaryFlag (cutR n)) : V.pairing f ≠ V.boundaryFlag (cutL n)

A survivor's partner survives, at the cut's left flag. The two cut flags are each other's partners, so nothing else can pair to either.

theorem RS.EdgeSubset.pairing_ne_cutR_of_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) : V.pairing f ≠ V.boundaryFlag (cutR n)

A survivor's partner survives, at the cut's right flag.

noncomputable def RS.EdgeSubset.stageFlagClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) : (V.gluePair (cutL n) (cutR n) ⋯).Flag

A surviving flag, read at the stage fragment, at a closing cut.

Equations

• RS.EdgeSubset.stageFlagClosed n V hcl f h1 h2 = RS.EdgeSubset.flagOfEq ⋯ ⟨f, ⋯⟩

theorem RS.EdgeSubset.pairing_stageFlagClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) (k1 : V.pairing f ≠ V.boundaryFlag (cutL n)) (k2 : V.pairing f ≠ V.boundaryFlag (cutR n)) : (stepFragment n V).pairing (stageFlagClosed n V hcl f h1 h2) = stageFlagClosed n V hcl (V.pairing f) k1 k2

At a closing cut the stage's partner is the base's.

theorem RS.EdgeSubset.boundaryFlag_stepFragment_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (bl : Fin (0 + n) ⊕ Fin (n + 0)) : (stepFragment n V).boundaryFlag bl = flagOfEq ⋯ ((V.gluePairClosed (cutL n) (cutR n) hcl).boundaryFlag ((interfaceStepEquiv 0 n 0).symm bl))

The stage's boundary flag is the base's, at a closing cut.

theorem RS.EdgeSubset.stageFlagClosed_boundaryFlag (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (bl : Fin (0 + n) ⊕ Fin (n + 0)) (h1 : V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl) ≠ V.boundaryFlag (cutL n)) (h2 : V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl) ≠ V.boundaryFlag (cutR n)) : stageFlagClosed n V hcl (V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl)) h1 h2 = (stepFragment n V).boundaryFlag bl

A surviving boundary flag is the stage's own, at a closing cut.

noncomputable def RS.EdgeSubset.stageFlag (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) : (V.gluePair (cutL n) (cutR n) ⋯).Flag

A surviving flag, read at the stage fragment.

Equations

• RS.EdgeSubset.stageFlag n V hop f h1 h2 = RS.EdgeSubset.flagOfEq ⋯ ⟨f, ⋯⟩

theorem RS.EdgeSubset.pairing_stageFlag (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) : (stepFragment n V).pairing (stageFlag n V hop f h1 h2) = flagOfEq ⋯ (Fragment.rewire hop ⟨f, ⋯⟩)

The stage's partner of a surviving flag is its rewired one.

theorem RS.EdgeSubset.pairing_stageFlag_of_ne (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) (k1 : V.pairing f ≠ V.boundaryFlag (cutL n)) (k2 : V.pairing f ≠ V.boundaryFlag (cutR n)) : (stepFragment n V).pairing (stageFlag n V hop f h1 h2) = stageFlag n V hop (V.pairing f) k1 k2

Away from the cut, the stage's partner is the base's.

theorem RS.EdgeSubset.pairing_stageFlag_cutR (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (k1 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutL n)) (k2 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutR n)) (h1 : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutL n)) (h2 : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : (stepFragment n V).pairing (stageFlag n V hop (V.pairing (V.boundaryFlag (cutR n))) k1 k2) = stageFlag n V hop (V.pairing (V.boundaryFlag (cutL n))) h1 h2

At the cut's right edge the stage's partner is the far end of the left edge.

theorem RS.EdgeSubset.stageFlag_boundaryFlag (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (bl : Fin (0 + n) ⊕ Fin (n + 0)) (h1 : V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl) ≠ V.boundaryFlag (cutL n)) (h2 : V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl) ≠ V.boundaryFlag (cutR n)) : stageFlag n V hop (V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl)) h1 h2 = (stepFragment n V).boundaryFlag bl

The stage's boundary flag is the base's, read as a stage flag.

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

A lower interface pair's left label is not the top cut's.

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

A lower interface pair's right label is not the top cut's.

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

A left label is never a right one.

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

A right label is never a left one.

noncomputable def RS.EdgeSubset.cutExtend (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hL1 : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutL n)) (hR1 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutL n)) (hR2 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) : V.Flag → Bool

Extending a colouring across a cut. The two cut flags take the opposite colour to their partners, which survive the glue.

Equations

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

theorem RS.EdgeSubset.cutExtend_of_ne (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hL1 : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutL n)) (hR1 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutL n)) (hR2 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) : cutExtend n V hop hL1 hR1 hR2 c' f = c' (stageFlag n V hop f h1 h2)

Away from the cut the extension is the stage's colouring.

theorem RS.EdgeSubset.cutExtend_cutL (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hL1 : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutL n)) (hR1 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutL n)) (hR2 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) : cutExtend n V hop hL1 hR1 hR2 c' (V.boundaryFlag (cutL n)) = !c' (stageFlag n V hop (V.pairing (V.boundaryFlag (cutL n))) hL1 hop)

At the cut's left flag the extension is the opposite of its partner's colour.

theorem RS.EdgeSubset.cutExtend_cutR (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (hL1 : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutL n)) (hR1 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutL n)) (hR2 : V.pairing (V.boundaryFlag (cutR n)) ≠ V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) : cutExtend n V hop hL1 hR1 hR2 c' (V.boundaryFlag (cutR n)) = !c' (stageFlag n V hop (V.pairing (V.boundaryFlag (cutR n))) hR1 hR2)

At the cut's right flag the extension is the opposite of its partner's colour.

theorem RS.EdgeSubset.stageFlagClosed_congr (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) {f g : V.Flag} (hfg : f = g) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) (k1 : g ≠ V.boundaryFlag (cutL n)) (k2 : g ≠ V.boundaryFlag (cutR n)) : stageFlagClosed n V hcl f h1 h2 = stageFlagClosed n V hcl g k1 k2

Stage flags at equal base flags agree.

noncomputable def RS.EdgeSubset.cutExtendClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) : V.Flag → Bool

Extending a colouring across a closing cut. The cut's two flags are each other's partners, and the glue takes both away, so their colours are free: give the left one true and the right one false and both the edge and the interface pair alternate at once.

Equations

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

theorem RS.EdgeSubset.cutExtendClosed_of_ne (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) (f : V.Flag) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) : cutExtendClosed n V hcl c' f = c' (stageFlagClosed n V hcl f h1 h2)

Away from the cut the extension is the stage's colouring.

theorem RS.EdgeSubset.cutExtendClosed_cutL (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) : cutExtendClosed n V hcl c' (V.boundaryFlag (cutL n)) = true

At the cut's left flag the extension is true.

theorem RS.EdgeSubset.cutExtendClosed_cutR (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (c' : (stepFragment n V).Flag → Bool) : cutExtendClosed n V hcl c' (V.boundaryFlag (cutR n)) = false

At the cut's right flag the extension is false.

theorem RS.EdgeSubset.stageFlag_congr (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) {f g : V.Flag} (hfg : f = g) (h1 : f ≠ V.boundaryFlag (cutL n)) (h2 : f ≠ V.boundaryFlag (cutR n)) (k1 : g ≠ V.boundaryFlag (cutL n)) (k2 : g ≠ V.boundaryFlag (cutR n)) : stageFlag n V hop f h1 h2 = stageFlag n V hop g k1 k2

The stage flag does not depend on which proof of survival it is given.

theorem RS.EdgeSubset.isOut_stepDataUp_boundaryFlag_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (b : Bool) (𝒟 : DataFamily V) (u : Finset (V.SurvivingFlag (cutL n) (cutR n))) (t : Finset (stepFragment n V).Flag) (ht : t = flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ u) (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetClosed u b, V.pairing f ∈ Fragment.liftSubsetClosed u b) (hEL : { flags := Fragment.liftSubsetClosed u b, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetClosed u b, pairing_mem := hcL }.CanonData) (bl : Fin (0 + n) ⊕ Fin (n + 0)) : (stepDataUp n V b 𝒟 t hct hEt hnet).snd.isOut ((stepFragment n V).boundaryFlag bl) = (𝒟 (Fragment.liftSubsetClosed u b) hcL hEL hneL).snd.isOut (V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl))

The stage's boundary direction at a closing cut is the base family's at the same label.

theorem RS.EdgeSubset.chainDir_stepDataUp_eq_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (b : Bool) (𝒟 : DataFamily V) (u : Finset (V.SurvivingFlag (cutL n) (cutR n))) (t : Finset (stepFragment n V).Flag) (ht : t = flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ u) (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetClosed u b, V.pairing f ∈ Fragment.liftSubsetClosed u b) (hEL : { flags := Fragment.liftSubsetClosed u b, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetClosed u b, pairing_mem := hcL }.CanonData) (bl : Fin (0 + n) ⊕ Fin (n + 0)) : (stepDataUp n V b 𝒟 t hct hEt hnet).snd.isOut ((stepFragment n V).pairing ((stepFragment n V).boundaryFlag bl)) = (𝒟 (Fragment.liftSubsetClosed u b) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl)))

The stage's boundary partner's direction at a closing cut is the base family's at the partner of the same label. Nothing is rewired, so no alternation is asked for.