The closure of two fragments, read on the base

The connection pairing evaluates the mixed partition function at pairClose F G, which is the interface glue of the two fragments' disjoint union, relabelled to the empty label type. Composing the closed identification with the colouring recursion writes that value as the base's summands, summed over its subsets and over the interface colours.

@[reducible]

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

The lexicographic order on the interface's label type.

Equations

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

@[reducible]

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

The same order one stage up.

Equations

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

@[reducible]

def RS.EdgeSubset.assemblySurvOrder (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.assemblyTopOrder : LinearOrder (Fin 0 ⊕ Fin 0)

The order the composition's own label type carries.

Equations

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

@[reducible, inline]

noncomputable abbrev RS.EdgeSubset.closeBase {t : ℕ} (F G : Fragment (Fin t)) : Fragment (Fin (0 + t) ⊕ Fin (t + 0))

The two fragments, moved onto the interface's label type.

Equations

• RS.EdgeSubset.closeBase F G = (F.relabel (finCongr ⋯)).disjUnion (G.relabel (finCongr ⋯))

theorem RS.EdgeSubset.pairClose_eq {t : ℕ} (F G : Fragment (Fin t)) : pairClose F G = (glueInterface 0 t 0 (closeBase F G)).relabel finSumFinEquiv

The closure is the interface glue, relabelled.

theorem RS.EdgeSubset.mixedPartition_pairClose {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)) : mixedPartition h (pairClose F G) = throughMixedPartitionC h (glueInterface 0 t 0 (closeBase F G)) emptyState

The closure's value is the interface glue's constrained value.

The tensor side, split over subsets

The closing display of RS21's Theorem 6 sums the identity (13) over the Eulerian subsets of the two fragments. Splitting the fragment tensors into their per-subset terms and exchanging the four sums puts the pairing in that form.

noncomputable def RS.EdgeSubset.tensorTermAt {α : Type} [LinearOrder α] [Fintype α] (V : Fragment α) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (s : Finset V.Flag) (x : GenBoundaryState k ℓ α) : ℂ

A fragment tensor's term at one subset.

Equations

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

theorem RS.EdgeSubset.tensorSum_eq_sum {α : Type} [LinearOrder α] [Fintype α] (V : Fragment α) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (x : GenBoundaryState k ℓ α) : tensorSum V h x = ∑ s : Finset V.Flag, tensorTermAt V h s x

The fragment tensor is the sum of its terms.

theorem RS.EdgeSubset.tensorTermAt_pos {α : Type} [LinearOrder α] [Fintype α] (V : Fragment α) {k ℓ : ℕ} (h : MixedFunctional k ℓ) {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) (x : GenBoundaryState k ℓ α) : tensorTermAt V h s x = { flags := s, pairing_mem := hc }.tFull h (Classical.choice hne).fst (↑(Classical.choice hne).snd) x

A tensor term at a good subset is the normalised tensor.

theorem RS.EdgeSubset.exists_sum_sum_superForm_tensorTermAt {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)) {s₁ : Finset F.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian) (hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData) {s₂ : Finset G.Flag} (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian) (hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData) (_hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂) (hb : ∀ (i : Fin t), F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags) : ∃ (o₁' : (Classical.choice hn₁).fst.Orientation) (o₂' : (Classical.choice hn₂).fst.Orientation) (M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ })) (M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ })), (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ↑(M₁.edge a) = { flags := s₁, pairing_mem := hc₁ }.chordInv (Classical.choice hn₁).fst ↑a) ∧ (∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }), ↑(M₂.edge b) = { flags := s₂, pairing_mem := hc₂ }.chordInv (Classical.choice hn₂).fst ↑b) ∧ (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), M₂.tail (({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) = !M₁.tail a) ∧ (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } ↑a → M₁.tail a = (cutMatching { flags := s₁, pairing_mem := hc₁ } (Classical.choice hn₁).fst o₁').tail a) ∧ (∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }), ¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } ↑b → M₂.tail b = (cutMatching { flags := s₂, pairing_mem := hc₂ } (Classical.choice hn₂).fst o₂').tail b) ∧ (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } ↑a → ¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } ↑(({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) → (cutMatching { flags := s₂, pairing_mem := hc₂ } (Classical.choice hn₂).fst o₂').tail (({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) = !(cutMatching { flags := s₁, pairing_mem := hc₁ } (Classical.choice hn₁).fst o₁').tail a) ∧ ∑ x : GenBoundaryState k ℓ (Fin t), ∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = ↑↑((DirMatching.stdMatching ⋯).sgnRel M₁) * (-1) ^ (Classical.choice hn₁).fst.openCircuitCount * (↑↑((DirMatching.stdMatching ⋯).sgnRel M₂) * (-1) ^ (Classical.choice hn₂).fst.openCircuitCount) * ∑ st : GenBoundaryState k ℓ (Fin t), { flags := s₁, pairing_mem := hc₁ }.pairAgreeValue { flags := s₂, pairing_mem := hc₂ } h o₁' o₂' st

The pair term when the two subsets use the same labels. This is RS21's (13), read on the two fragment tensors' per-subset terms: the pairing is the two circuit-and-matching signs times the colouring sum of the two subsets' agreement.

The diagonal state on the two sides

The interface colours enter the base as one state on the disjoint union. Restricting it to either summand and pulling back along that fragment's relabel gives the colours themselves, which is the form relabel_edgeSum and edgeSum_disjUnion consume.

theorem RS.EdgeSubset.diagOf_inl_relabel {k ℓ : ℕ} (t : ℕ) (x : GenBoundaryState k ℓ (Fin t)) : (fun (a : Fin t) => diagOf t x (Sum.inl ((finCongr ⋯) a))) = x

The diagonal state, restricted to the left fragment.

theorem RS.EdgeSubset.diagOf_inr_relabel {k ℓ : ℕ} (t : ℕ) (x : GenBoundaryState k ℓ (Fin t)) : (fun (b : Fin t) => diagOf t x (Sum.inr ((finCongr ⋯) b))) = x

The diagonal state, restricted to the right fragment.

The base's colouring sum, split into the two fragments'

The base is the two fragments' disjoint union, so its colouring sum factors; each factor then comes down to its own fragment along that fragment's relabel.

theorem RS.EdgeSubset.edgeSum_closeBase {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)) (B : EdgeSubset (closeBase F G)) (st : GenBoundaryState k ℓ (Fin (0 + t) ⊕ Fin (t + 0))) (hbnd : genBoundarySubsetMatches (closeBase F G) B.flags st) (hbnd₁ : genBoundarySubsetMatches (F.relabel (finCongr ⋯)) (leftSub B).flags fun (a : Fin (0 + t)) => st (Sum.inl a)) (hbnd₂ : genBoundarySubsetMatches (G.relabel (finCongr ⋯)) (rightSub B).flags fun (b : Fin (t + 0)) => st (Sum.inr b)) {κ₁ : (leftSub B).RelTransitionSystem} {κ₂ : (rightSub B).RelTransitionSystem} (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) : B.edgeSum h st hbnd (prodOrient o₁ o₂) = (leftSub B).edgeSum h (fun (a : Fin (0 + t)) => st (Sum.inl a)) hbnd₁ o₁ * (rightSub B).edgeSum h (fun (b : Fin (t + 0)) => st (Sum.inr b)) hbnd₂ o₂

The base's colouring sum factors.

theorem RS.EdgeSubset.edgeSum_relabelDown {k ℓ : ℕ} (h : MixedFunctional k ℓ) {t n : ℕ} (F : Fragment (Fin t)) (he : t = n) (A : EdgeSubset (F.relabel (finCongr he))) (st : GenBoundaryState k ℓ (Fin n)) (st' : GenBoundaryState k ℓ (Fin t)) (hst : (fun (a : Fin t) => st ((finCongr he) a)) = st') (hbnd : genBoundarySubsetMatches (F.relabel (finCongr he)) A.flags st) (hbnd' : genBoundarySubsetMatches F (relabelDown (finCongr he) A).flags st') {κ : (relabelDown (finCongr he) A).RelTransitionSystem} (o : κ.Orientation) : A.edgeSum h st hbnd (relabelOrientUp (finCongr he) (relabelDown (finCongr he) A) o) = (relabelDown (finCongr he) A).edgeSum h st' hbnd' o

A half's colouring sum comes down to its own fragment.

theorem RS.EdgeSubset.edgeSum_closeBase_eq_pairAgreeValue {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)) (x : GenBoundaryState k ℓ (Fin t)) (B : EdgeSubset (closeBase F G)) (hbnd : genBoundarySubsetMatches (closeBase F G) B.flags (diagOf t x)) (hbnd₁ : genBoundarySubsetMatches F (leftSub B).flags x) (hbnd₂ : genBoundarySubsetMatches G (rightSub B).flags x) {κ₁ : (relabelDown (finCongr ⋯) (leftSub B)).RelTransitionSystem} {κ₂ : (relabelDown (finCongr ⋯) (rightSub B)).RelTransitionSystem} (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) : B.edgeSum h (diagOf t x) hbnd (prodOrient (relabelOrientUp (finCongr ⋯) (relabelDown (finCongr ⋯) (leftSub B)) o₁) (relabelOrientUp (finCongr ⋯) (relabelDown (finCongr ⋯) (rightSub B)) o₂)) = (relabelDown (finCongr ⋯) (leftSub B)).pairAgreeValue (relabelDown (finCongr ⋯) (rightSub B)) h o₁ o₂ x

The base's colouring sum is the pair's agreement value. This is the composition's side of RS21's (13): the base subset's colouring sum at a diagonal state is exactly the object the pairing identity produces.

Transports of a subset along a relabel

The colouring recursion and the ledger recursion carry their subsets along equalities of fragments taken at different points: one before the stage's relabel, one after. The two agree.

theorem RS.EdgeSubset.flagsOfEq_relabel {L L' : Type} {V₁ V₂ : Fragment L} (hV : V₁ = V₂) (e : L ≃ L') (t : Finset V₁.Flag) : flagsOfEq (V₁.relabel e) (V₂.relabel e) ⋯ t = flagsOfEq V₁ V₂ hV t

A transport commutes with a relabel.

theorem RS.EdgeSubset.stageDataOfEq_sub_flags {m : ℕ} {V₁ V₂ : Fragment (Fin (0 + m) ⊕ Fin (m + 0))} (hV : V₁ = V₂) (Dm : StageData m V₁) : (stageDataOfEq hV Dm).sub.flags = flagsOfEq V₁ V₂ hV Dm.sub.flags

The transported stage data's subset.

theorem RS.EdgeSubset.stepData_sub_flags_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : (stepData n V D).sub.flags = flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) D.sub.flags)

The ledger's step drops the subset, at a closing cut.

theorem RS.EdgeSubset.stepData_sub_flags_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : (stepData n V D).sub.flags = flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) D.sub.flags)

The ledger's step drops the subset, at an open cut.

theorem RS.EdgeSubset.carried_eq_glueCount (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (D : StageData n V) : carried n V D.sub.flags = glueCount n V D

The colouring side's carried count is the ledger's. Both count the closing cuts whose own edge the subset carries.

theorem RS.EdgeSubset.imageOf_eq_glueData_sub (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (D : StageData n V) : imageOf n V D.sub.flags = (glueData n V D).sub.flags

The colouring side's image subset is the ledger's. Both are the iterated drop of the base subset.

The base's subsets, split into the two fragments'

A subset of a disjoint union is a pair of subsets, so the sum over the base's subsets is the double sum the tensor side carries.

noncomputable def RS.EdgeSubset.partsEquiv {α β : Type} (W₁ : Fragment α) (W₂ : Fragment β) : Finset (W₁.disjUnion W₂).Flag ≃ Finset W₁.Flag × Finset W₂.Flag

A subset of a disjoint union is a pair of subsets.

Equations

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

theorem RS.EdgeSubset.sum_subsets_disjUnion {α β : Type} {W₁ : Fragment α} {W₂ : Fragment β} {M : Type} [AddCommMonoid M] (f : Finset (W₁.disjUnion W₂).Flag → M) : ∑ s : Finset (W₁.disjUnion W₂).Flag, f s = ∑ s₁ : Finset W₁.Flag, ∑ s₂ : Finset W₂.Flag, f (joinParts s₁ s₂)

The sum over the base's subsets is the double sum.

@[reducible, inline]

noncomputable abbrev RS.EdgeSubset.closeJoin {t : ℕ} {F G : Fragment (Fin t)} (s₁ : Finset F.Flag) (s₂ : Finset G.Flag) : Finset (closeBase F G).Flag

The base subset a pair of subsets makes.

Equations

• RS.EdgeSubset.closeJoin s₁ s₂ = RS.joinParts s₁ s₂

theorem RS.EdgeSubset.swapPaired_joinParts (t : ℕ) (F G : Fragment (Fin t)) (s₁ : Finset F.Flag) (s₂ : Finset G.Flag) (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂) : { flags := closeJoin s₁ s₂, pairing_mem := hc }.SwapPaired (interfaceSwap (stepIdent t))

The base subset is interface-paired exactly when the two fragments' subsets use the same labels. This is (14)'s hypothesis, read on the pair.

theorem RS.EdgeSubset.closeJoin_pairing_mem {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (f : (closeBase F G).Flag) : f ∈ closeJoin s₁ s₂ → (closeBase F G).pairing f ∈ closeJoin s₁ s₂

The base subset a pair makes is closed under the pairing.

theorem RS.EdgeSubset.leftSub_closeJoin {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, (F.relabel (finCongr ⋯)).pairing f ∈ s₁) : leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc } = { flags := s₁, pairing_mem := hc₁ }

The base subset's left half is the first subset.

theorem RS.EdgeSubset.rightSub_closeJoin {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, (G.relabel (finCongr ⋯)).pairing f ∈ s₂) : rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc } = { flags := s₂, pairing_mem := hc₂ }

The base subset's right half is the second subset.

The matchings under a relabel

RS21's (13) produces its matchings on the fragments' own subsets; (14) asks for them on the halves of the base subset, which live one relabel away. The used labels correspond (usedLabRelabelEquiv) and the chord matching shifts with them (cutMatching_relabelUp_edge); what is left is the sign.

theorem RS.EdgeSubset.sgnRel_stdMatching_map {α β : Type} [LinearOrder α] [Fintype α] [LinearOrder β] [Fintype β] (e : α ≃o β) {m : ℕ} (h : Fintype.card α = 2 * m) (h' : Fintype.card β = 2 * m) (M : DirMatching α) : (DirMatching.stdMatching h').sgnRel (DirMatching.map e.toEquiv M) = (DirMatching.stdMatching h).sgnRel M

A matching's sign survives a transport. The two fragments' matchings may therefore be read on the base subset's halves, where (14) wants them.

theorem RS.EdgeSubset.interfaceSideDisjEquiv_val {γ δ : Type} {W₁ : Fragment γ} {W₂ : Fragment δ} (F : EdgeSubset (W₁.disjUnion W₂)) (e : γ ≃ δ) (hp : F.InterfacePaired e) (a : UsedLab (leftSub F)) : ↑((F.interfaceSideDisjEquiv e hp) a) = e ↑a

The interface identification acts by the interface map. It is therefore the same identification exists_eulerianPosition uses, read on the two halves.

The pair's transition data, read on the base

(14) asks for the two systems on the halves of the base subset. The fragments' own systems get there by the relabel and the half identification, and neither move changes the open circuit count.

noncomputable def RS.EdgeSubset.pairRelLeft {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc₁ : ∀ f ∈ s₁, (F.relabel (finCongr ⋯)).pairing f ∈ s₁) (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem) : (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc }).RelTransitionSystem

The first fragment's system, read on the base subset's left half.

Equations

• RS.EdgeSubset.pairRelLeft hc₁ hc κ₁ = RS.EdgeSubset.relOfEq ⋯ κ₁

noncomputable def RS.EdgeSubset.pairRelRight {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc₂ : ∀ f ∈ s₂, (G.relabel (finCongr ⋯)).pairing f ∈ s₂) (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem) : (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc }).RelTransitionSystem

The second fragment's system, read on the base subset's right half.

Equations

• RS.EdgeSubset.pairRelRight hc₂ hc κ₂ = RS.EdgeSubset.relOfEq ⋯ κ₂

theorem RS.EdgeSubset.openCircuitCount_pairRelLeft {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc₁ : ∀ f ∈ s₁, (F.relabel (finCongr ⋯)).pairing f ∈ s₁) (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem) : (pairRelLeft hc₁ hc κ₁).openCircuitCount = κ₁.openCircuitCount

Reading the first system on the half leaves its circuit count alone.

theorem RS.EdgeSubset.openCircuitCount_pairRelRight {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc₂ : ∀ f ∈ s₂, (G.relabel (finCongr ⋯)).pairing f ∈ s₂) (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem) : (pairRelRight hc₂ hc κ₂).openCircuitCount = κ₂.openCircuitCount

Reading the second system on the half leaves its circuit count alone.

theorem RS.EdgeSubset.edge_eq_cutMatching {α : Type} [LinearOrder α] {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (M : DirMatching (UsedLab F)) (hM : ∀ (a : UsedLab F), ↑(M.edge a) = F.chordInv κ ↑a) : M.edge = (cutMatching F κ o).edge

A matching with the chord pairings is the chord matching, on pairings. RS21's (13) records its matchings pointwise; (14) wants them as an equality of pairing maps.

def RS.EdgeSubset.usedLabOrderIsoOfEq {α : Type} [LinearOrder α] {W : Fragment α} {F₁ F₂ : EdgeSubset W} (h : F₁ = F₂) : UsedLab F₁ ≃o UsedLab F₂

The used labels are untouched by an equality of subsets, as an order isomorphism — the form the sign transport wants.

Equations

• RS.EdgeSubset.usedLabOrderIsoOfEq h = h ▸ OrderIso.refl (RS.UsedLab F₁)

noncomputable def RS.EdgeSubset.usedLabRelabelOrderIso {α β : Type} [LinearOrder α] [LinearOrder β] {W : Fragment α} (e : α ≃o β) (F : EdgeSubset W) : UsedLab (relabelUp e.toEquiv F) ≃o UsedLab F

The used labels shift through a relabel, as an order isomorphism.

Equations

• RS.EdgeSubset.usedLabRelabelOrderIso e F = { toEquiv := RS.usedLabRelabelEquiv e F, map_rel_iff' := ⋯ }

def RS.EdgeSubset.leftIso (t : ℕ) : Fin t ≃o Fin (0 + t)

The left relabel, as an order isomorphism.

Equations

• RS.EdgeSubset.leftIso t = Fin.castOrderIso ⋯

def RS.EdgeSubset.rightIso (t : ℕ) : Fin t ≃o Fin (t + 0)

The right relabel, as an order isomorphism.

Equations

• RS.EdgeSubset.rightIso t = Fin.castOrderIso ⋯

noncomputable def RS.EdgeSubset.usedLabLeftCloseJoin {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) : UsedLab (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc }) ≃o UsedLab { flags := s₁, pairing_mem := hc₁ }

The base subset's left half has the first subset's used labels.

Equations

• RS.EdgeSubset.usedLabLeftCloseJoin hc hc₁ = (RS.EdgeSubset.usedLabOrderIsoOfEq ⋯).trans (RS.EdgeSubset.usedLabRelabelOrderIso (RS.EdgeSubset.leftIso t) { flags := s₁, pairing_mem := hc₁ })

noncomputable def RS.EdgeSubset.usedLabRightCloseJoin {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) : UsedLab (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc }) ≃o UsedLab { flags := s₂, pairing_mem := hc₂ }

The base subset's right half has the second subset's used labels.

Equations

• RS.EdgeSubset.usedLabRightCloseJoin hc hc₂ = (RS.EdgeSubset.usedLabOrderIsoOfEq ⋯).trans (RS.EdgeSubset.usedLabRelabelOrderIso (RS.EdgeSubset.rightIso t) { flags := s₂, pairing_mem := hc₂ })

theorem RS.EdgeSubset.card_usedLab_leftSub_closeJoin {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) : Fintype.card (UsedLab (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc })) = Fintype.card (UsedLab { flags := s₁, pairing_mem := hc₁ })

The base subset's left half has as many used labels as the first subset.

theorem RS.EdgeSubset.card_usedLab_rightSub_closeJoin {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) : Fintype.card (UsedLab (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc })) = Fintype.card (UsedLab { flags := s₂, pairing_mem := hc₂ })

The base subset's right half has as many used labels as the second subset.

theorem RS.EdgeSubset.chordInv_pairRelLeft {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem) (a : Fin (0 + t)) : (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc }).chordInv (pairRelLeft hc₁ hc (relabelTransUp (leftIso t).toEquiv { flags := s₁, pairing_mem := hc₁ } κ₁)) a = (leftIso t) ({ flags := s₁, pairing_mem := hc₁ }.chordInv κ₁ ((leftIso t).symm a))

The chord involution on the base subset's left half is the first subset's, shifted by the relabel.

theorem RS.EdgeSubset.chordInv_pairRelRight {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem) (b : Fin (t + 0)) : (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc }).chordInv (pairRelRight hc₂ hc (relabelTransUp (rightIso t).toEquiv { flags := s₂, pairing_mem := hc₂ } κ₂)) b = (rightIso t) ({ flags := s₂, pairing_mem := hc₂ }.chordInv κ₂ ((rightIso t).symm b))

The chord involution on the base subset's right half is the second subset's, shifted by the relabel.

theorem RS.EdgeSubset.usedLabOrderIsoOfEq_val {α : Type} [LinearOrder α] {W : Fragment α} {F₁ F₂ : EdgeSubset W} (h : F₁ = F₂) (x : UsedLab F₁) : ↑((usedLabOrderIsoOfEq h) x) = ↑x

The subset-equality transport keeps the label.

theorem RS.EdgeSubset.usedLabLeftCloseJoin_val {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (a : UsedLab (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc })) : ↑((usedLabLeftCloseJoin hc hc₁) a) = (leftIso t).symm ↑a

The left transport acts by the relabel on labels.

theorem RS.EdgeSubset.usedLabRightCloseJoin_val {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (b : UsedLab (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc })) : ↑((usedLabRightCloseJoin hc hc₂) b) = (rightIso t).symm ↑b

The right transport acts by the relabel on labels.

theorem RS.EdgeSubset.usedLabLeftCloseJoin_symm_val {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (x : UsedLab { flags := s₁, pairing_mem := hc₁ }) : ↑((usedLabLeftCloseJoin hc hc₁).symm x) = (leftIso t) ↑x

The left transport's inverse acts by the relabel.

theorem RS.EdgeSubset.usedLabRightCloseJoin_symm_val {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (x : UsedLab { flags := s₂, pairing_mem := hc₂ }) : ↑((usedLabRightCloseJoin hc hc₂).symm x) = (rightIso t) ↑x

The right transport's inverse acts by the relabel.

theorem RS.EdgeSubset.edge_val_map_left {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem) (M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ })) (hM₁ : ∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ↑(M₁.edge a) = { flags := s₁, pairing_mem := hc₁ }.chordInv κ₁ ↑a) (a : UsedLab (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc })) : ↑((DirMatching.map (usedLabLeftCloseJoin hc hc₁).symm.toEquiv M₁).edge a) = (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc }).chordInv (pairRelLeft hc₁ hc (relabelTransUp (leftIso t).toEquiv { flags := s₁, pairing_mem := hc₁ } κ₁)) ↑a

The transported matching keeps the chord record, on the base subset's left half.

theorem RS.EdgeSubset.edge_val_map_right {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem) (M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ })) (hM₂ : ∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }), ↑(M₂.edge b) = { flags := s₂, pairing_mem := hc₂ }.chordInv κ₂ ↑b) (b : UsedLab (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc })) : ↑((DirMatching.map (usedLabRightCloseJoin hc hc₂).symm.toEquiv M₂).edge b) = (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc }).chordInv (pairRelRight hc₂ hc (relabelTransUp (rightIso t).toEquiv { flags := s₂, pairing_mem := hc₂ } κ₂)) ↑b

The transported matching keeps the chord record, on the base subset's right half.

theorem RS.EdgeSubset.usedLabRight_interfaceSideDisj {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (hp : { flags := closeJoin s₁ s₂, pairing_mem := hc }.InterfacePaired (stepIdentOrderIso t).toEquiv) (hb : ∀ (i : Fin t), F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags) (a : UsedLab (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc })) : (usedLabRightCloseJoin hc hc₂) (({ flags := closeJoin s₁ s₂, pairing_mem := hc }.interfaceSideDisjOrderIso (stepIdentOrderIso t) hp) a) = ({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) ((usedLabLeftCloseJoin hc hc₁) a)

The two interface identifications agree. (14) states its alternation against the base subset's halves, (13) against the two fragments' own subsets; the transports carry one to the other.

The stage data a pair of subsets makes

Everything (14) reads off the composition is a function of this one object: the base subset, its interface pairing, and the two systems carried over from the fragments.

noncomputable def RS.EdgeSubset.pairStage {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂) (κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem) (κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem) : StageData t (closeBase F G)

The stage data a pair of subsets makes.

Equations

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

theorem RS.EdgeSubset.sign_composition_pair {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂) (hb : ∀ (i : Fin t), F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags) (κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem) (o₁ : κ₁.Orientation) (κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem) (o₂ : κ₂.Orientation) (M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ })) (M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ })) {m : ℕ} (hcard₁ : Fintype.card (UsedLab { flags := s₁, pairing_mem := hc₁ }) = 2 * m) (hcard₂ : Fintype.card (UsedLab { flags := s₂, pairing_mem := hc₂ }) = 2 * m) (hM₁ : ∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ↑(M₁.edge a) = { flags := s₁, pairing_mem := hc₁ }.chordInv κ₁ ↑a) (hM₂ : ∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }), ↑(M₂.edge b) = { flags := s₂, pairing_mem := hc₂ }.chordInv κ₂ ↑b) (halt : ∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), M₂.tail (({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) = !M₁.tail a) : ↑↑((DirMatching.stdMatching hcard₁).sgnRel M₁) * (-1) ^ κ₁.openCircuitCount * (↑↑((DirMatching.stdMatching hcard₂).sgnRel M₂) * (-1) ^ κ₂.openCircuitCount) = (-1) ^ ((glueData t (closeBase F G) (pairStage hc₁ hc₂ hused κ₁ κ₂)).rel.openCircuitCount + glueCount t (closeBase F G) (pairStage hc₁ hc₂ hused κ₁ κ₂))

RS21's (14), read on a pair of subsets. The two fragments' circuit-and-matching signs multiply to the composition's own sign, with one extra factor for each closing cut the subsets carry.

theorem RS.EdgeSubset.exists_pairTerm_eq_glued_sign {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)) {s₁ : Finset F.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian) (hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData) {s₂ : Finset G.Flag} (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian) (hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData) (hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂) (hb : ∀ (i : Fin t), F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags) : ∃ (o₁' : (Classical.choice hn₁).fst.Orientation) (o₂' : (Classical.choice hn₂).fst.Orientation) (M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ })) (M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ })), (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ↑(M₁.edge a) = { flags := s₁, pairing_mem := hc₁ }.chordInv (Classical.choice hn₁).fst ↑a) ∧ (∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }), ↑(M₂.edge b) = { flags := s₂, pairing_mem := hc₂ }.chordInv (Classical.choice hn₂).fst ↑b) ∧ (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), M₂.tail (({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) = !M₁.tail a) ∧ (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } ↑a → M₁.tail a = (cutMatching { flags := s₁, pairing_mem := hc₁ } (Classical.choice hn₁).fst o₁').tail a) ∧ (∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }), ¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } ↑b → M₂.tail b = (cutMatching { flags := s₂, pairing_mem := hc₂ } (Classical.choice hn₂).fst o₂').tail b) ∧ (∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }), ¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } ↑a → ¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } ↑(({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) → (cutMatching { flags := s₂, pairing_mem := hc₂ } (Classical.choice hn₂).fst o₂').tail (({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) = !(cutMatching { flags := s₁, pairing_mem := hc₁ } (Classical.choice hn₁).fst o₁').tail a) ∧ ∑ x : GenBoundaryState k ℓ (Fin t), ∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = (-1) ^ ((glueData t (closeBase F G) (pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst)).rel.openCircuitCount + glueCount t (closeBase F G) (pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst)) * ∑ st : GenBoundaryState k ℓ (Fin t), { flags := s₁, pairing_mem := hc₁ }.pairAgreeValue { flags := s₂, pairing_mem := hc₂ } h o₁' o₂' st

The pair term, with its constant named. RS21's (13) read against (14): the pairing of the two fragments' terms at a pair of subsets is the composition's own circuit sign, one factor for each cut the pair closes, times the colouring sum of their agreement.

theorem RS.EdgeSubset.circles_closeBase {t : ℕ} (F G : Fragment (Fin t)) : (closeBase F G).circles = F.circles + G.circles

The base's free circles are the two fragments'.

Restricting the composition's data to the two fragments

The base's own transition data restrict to its two halves and descend to the fragments; these are the data RS21's (13) is applied at, so that the orientations on the two sides are the composition's own.

noncomputable def RS.EdgeSubset.pairRelLeftDown {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) (κ : { flags := closeJoin s₁ s₂, pairing_mem := hc }.RelTransitionSystem) : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem

The base's system, restricted to the first fragment.

Equations

• RS.EdgeSubset.pairRelLeftDown hc hc₁ κ = RS.relabelTransDown (RS.EdgeSubset.leftIso t).toEquiv { flags := s₁, pairing_mem := hc₁ } (RS.EdgeSubset.relOfEq ⋯ (RS.leftRel κ))

noncomputable def RS.EdgeSubset.pairRelRightDown {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} {s₂ : Finset G.Flag} (hc : ∀ f ∈ closeJoin s₁ s₂, (closeBase F G).pairing f ∈ closeJoin s₁ s₂) (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (κ : { flags := closeJoin s₁ s₂, pairing_mem := hc }.RelTransitionSystem) : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem

The base's system, restricted to the second fragment.

Equations

• RS.EdgeSubset.pairRelRightDown hc hc₂ κ = RS.relabelTransDown (RS.EdgeSubset.rightIso t).toEquiv { flags := s₂, pairing_mem := hc₂ } (RS.EdgeSubset.relOfEq ⋯ (RS.rightRel κ))

noncomputable def RS.EdgeSubset.orientReplace {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) (g : W.Flag → Bool) : κ.Orientation

Replacing an orientation off the internal flags. The two laws bind only internal flags, so the directions elsewhere may be given by any function at all.

Equations

• RS.EdgeSubset.orientReplace o g = { isOut := fun (f : W.Flag) => if f ∈ F.internalFlags then o.isOut f else g f, match_flip := ⋯, pairing_flip := ⋯ }

theorem RS.EdgeSubset.isOut_orientReplace_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) (g : W.Flag → Bool) {f : W.Flag} (hf : f ∈ F.internalFlags) : (orientReplace o g).isOut f = o.isOut f

At an internal flag the replacement keeps the direction.

theorem RS.EdgeSubset.isOut_orientReplace_of_not_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} (o : κ.Orientation) (g : W.Flag → Bool) {f : W.Flag} (hf : f ∉ F.internalFlags) : (orientReplace o g).isOut f = g f

Off the internal flags the replacement is the given function.

The colouring sum sees only the internal directions

RS21's colouring sum is built from the in-flag list at each vertex, and a flag is on that list only if it is attached to the vertex — that is, only if it is internal. So the sum does not see how an orientation directs a labelled end, and in particular is unchanged by the port flips (13) performs.

theorem RS.EdgeSubset.relInFlagsAt_congr_internal {α : Type} {W : Fragment α} (F : EdgeSubset W) {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) (v : W.Vertex) : F.relInFlagsAt o v = F.relInFlagsAt o' v

The in-flag list sees only the internal directions.

theorem RS.EdgeSubset.coreOddSignAt_congr_internal {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) (φ : F.CoreOddColouring ℓ) (v : W.Vertex) : F.coreOddSignAt o φ v = F.coreOddSignAt o' φ v

The odd sign at a vertex sees only the internal directions.

theorem RS.EdgeSubset.coreOddListAt_congr_internal {α : Type} {W : Fragment α} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) (φ : F.CoreOddColouring ℓ) (v : W.Vertex) : F.coreOddListAt o φ v = F.coreOddListAt o' φ v

The odd list at a vertex sees only the internal directions.

theorem RS.EdgeSubset.edgeSum_congr_orient {α : Type} {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o o' : κ.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) : F.edgeSum h st hbnd o = F.edgeSum h st hbnd o'

RS21's colouring sum sees only the internal directions. It is therefore unchanged by a port flip.

theorem RS.EdgeSubset.edgeSum_orientReplace {α : Type} {W : Fragment α} (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.RelTransitionSystem} (o : κ.Orientation) (g : W.Flag → Bool) : F.edgeSum h st hbnd (orientReplace o g) = F.edgeSum h st hbnd o

Replacing off the internal flags costs the colouring sum nothing.

The composition's value at any canonical family

The composition's constrained value does not depend on which canonical data compute it, so the colouring recursion may be run from whichever family is convenient — in particular from one built out of the two fragments' own data.

theorem RS.EdgeSubset.throughMixedPartitionC_eq_edgeTermAt_canon {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) (𝒟 : DataFamily V) (hcanon : ∀ (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), PathCanonical (𝒟 s hc hE hne).snd) : throughMixedPartitionC h V st = (↑k - 2 * ↑ℓ) ^ V.circles * ∑ s : Finset V.Flag, circuitWeight 𝒟 s * edgeTermAt h 𝒟 st s 0

The composition's constrained value at an arbitrary canonical family.

theorem RS.EdgeSubset.pathCanonical_isEmpty {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} (F : EdgeSubset V) {κ : F.RelTransitionSystem} (o : κ.Orientation) : PathCanonical o

At the composition every orientation is path-canonical. So any family of transition data there is a canonical one.

theorem RS.EdgeSubset.throughMixedPartitionC_eq_edgeTermAt_any {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) (𝒟 : DataFamily V) : throughMixedPartitionC h V st = (↑k - 2 * ↑ℓ) ^ V.circles * ∑ s : Finset V.Flag, circuitWeight 𝒟 s * edgeTermAt h 𝒟 st s 0

The composition's constrained value at an arbitrary family. No canonicality hypothesis is needed: at an empty label type there are no chords to order.

The alternation, in chain-direction form

(13) reports its alternation on the chord matchings' tails; the glue reads it on the chain directions. At a chain label the two are the same thing, negated.

theorem RS.EdgeSubset.cutMatching_tail_of_not_through {α : Type} [LinearOrder α] {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (o : κ.Orientation) (i : UsedLab F) (hnt : ¬IsThroughLabel F ↑i) : (cutMatching F κ o).tail i = !chainDir o (W.boundaryFlag ↑i)

The chord matching's tail at a chain label is that label's chain direction, reversed.

Lifting a data family across an open cut

The downward direction is unglueDataOpen; this is its upward counterpart. Where the family's own orientation directs the two rewired ends oppositely — which is what RS21's step 1 arranges — the glue applies; elsewhere the value is junk the identity never reads.

noncomputable def RS.EdgeSubset.glueDataOpen {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟 : DataFamily V) : DataFamily (V.gluePairOpen i j hij hopen)

The upward glue of a data family, at an open cut.

Equations

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

noncomputable def RS.EdgeSubset.glueDataClosed {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (b : Bool) (𝒟 : DataFamily V) : DataFamily (V.gluePairClosed i j hclosed)

The upward glue of a data family, at a closing cut. A closing cut rewires no directions, so no compatibility is needed; what it does need is the lift's bit, since a glued subset has two lifts and they are different subsets of the base.

Equations

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

noncomputable def RS.EdgeSubset.relabelDataUp {α' β' : Type} [LinearOrder α'] [LinearOrder β'] (e : α' ≃o β') {W' : Fragment α'} (𝒟 : DataFamily W') : DataFamily (W'.relabel e.toEquiv)

A data family under a relabel, upward. The counterpart of relabelDataDown.

Equations

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

noncomputable def RS.EdgeSubset.stepDataUp (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (b : Bool) (𝒟 : DataFamily V) : DataFamily (stepFragment n V)

One stage of the upward lift. The mirror of stepDataDown: dispatch on whether the stage's cut closes, glue the family across it, and relabel up.

Equations

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

noncomputable def RS.EdgeSubset.liftData (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : (Fin n → Bool) → DataFamily V → DataFamily (glueInterface 0 n 0 V)

The upward lift over the whole interface. The mirror of pushData, carrying one bit for each stage — the lift the closing cuts leave undetermined.

Equations

• RS.EdgeSubset.liftData 0 x_4 x_5 𝒟 = RS.EdgeSubset.relabelDataUp RS.EdgeSubset.baseIso 𝒟
• RS.EdgeSubset.liftData n.succ V bits 𝒟 = RS.EdgeSubset.liftData n (RS.EdgeSubset.stepFragment n V) (fun (a : Fin n) => bits a.castSucc) (RS.EdgeSubset.stepDataUp n V (bits (Fin.last n)) 𝒟)

The colouring sum under a matching-equal system

The single-cut round trips rebuild the system rather than storing it, so they hold only up to MatchEq. The colouring sum reads the system only through the partner of an internal flag, so it does not tell the difference.

theorem RS.EdgeSubset.coreOddSignFn_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hm : κ.MatchEq κ') {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) : F.coreOddSignFn κ φ f = F.coreOddSignFn κ' φ f

The odd sign function sees only the internal partners.

theorem RS.EdgeSubset.coreOddPairFn_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hm : κ.MatchEq κ') {ℓ : ℕ} (φ : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) : F.coreOddPairFn κ φ f = F.coreOddPairFn κ' φ f

The odd pair function sees only the internal partners.

theorem RS.EdgeSubset.relInFlagsAt_congr_isOut_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (o : κ.Orientation) (o' : κ'.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) (v : W.Vertex) : F.relInFlagsAt o v = F.relInFlagsAt o' v

The in-flag list sees only the internal directions, across two systems: it is cut out by the directions at the flags attached to the vertex, and those are internal.

theorem RS.EdgeSubset.coreOddSignAt_matchEq_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hm : κ.MatchEq κ') {ℓ : ℕ} (o : κ.Orientation) (o' : κ'.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) (φ : F.CoreOddColouring ℓ) (v : W.Vertex) : F.coreOddSignAt o φ v = F.coreOddSignAt o' φ v

The odd sign at a vertex, under a matching-equal system, from the internal directions alone.

theorem RS.EdgeSubset.coreOddListAt_matchEq_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hm : κ.MatchEq κ') {ℓ : ℕ} (o : κ.Orientation) (o' : κ'.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) (φ : F.CoreOddColouring ℓ) (v : W.Vertex) : F.coreOddListAt o φ v = F.coreOddListAt o' φ v

The odd list at a vertex, under a matching-equal system, from the internal directions alone.

theorem RS.EdgeSubset.edgeSum_matchEq_internal {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (hm : κ.MatchEq κ') {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (o : κ.Orientation) (o' : κ'.Orientation) (hio : ∀ f ∈ F.internalFlags, o.isOut f = o'.isOut f) : F.edgeSum h st hbnd o = F.edgeSum h st hbnd o'

RS21's colouring sum under a matching-equal system, from the internal directions alone. The sum reads the directions only at the flags attached to a vertex, so two orientations that agree there compute it alike.

The summand under a change of family

Two families whose data at a subset are matching-equal at the same directions give that subset the same summand. This is the form in which the round trip is read.

theorem RS.EdgeSubset.match_relOfEq {L : Type} {V : Fragment L} {F₁ F₂ : EdgeSubset V} (hF : F₁ = F₂) (κ : F₁.RelTransitionSystem) (f : V.Flag) : (relOfEq hF κ).match_ f = κ.match_ f

A transported system has the same partner map.

theorem RS.EdgeSubset.isOut_orientOfEq {L : Type} {V : Fragment L} {F₁ F₂ : EdgeSubset V} (hF : F₁ = F₂) {κ : F₁.RelTransitionSystem} (o : κ.Orientation) (f : V.Flag) : (orientOfEq hF o).isOut f = o.isOut f

A transported orientation has the same directions.

theorem RS.EdgeSubset.glueDataOpen_pos {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟 : DataFamily V) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hEL : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hopen t) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag j)) = !(𝒟 (Fragment.liftSubsetOpen hopen t) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag i))) : (glueDataOpen hij hopen 𝒟 t hct hEt hnet).fst = RelTransitionSystem.glueOpen hij hopen t hct hcL (𝒟 (Fragment.liftSubsetOpen hopen t) hcL hEL hneL).fst

The open glue's value where it applies. Stated with the lifted subset's own proofs, so that the call site may supply them rather than reconstruct the definition's.

theorem RS.EdgeSubset.isOut_glueDataClosed_pos {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (b : Bool) (𝒟 : DataFamily V) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t b, V.pairing f ∈ Fragment.liftSubsetClosed t b) (hEL : { flags := Fragment.liftSubsetClosed t b, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetClosed t b, pairing_mem := hcL }.CanonData) (f' : V.SurvivingFlag i j) : (glueDataClosed hclosed b 𝒟 t hct hEt hnet).snd.isOut f' = (𝒟 (Fragment.liftSubsetClosed t b) hcL hEL hneL).snd.isOut ↑f'

The closing glue's directions. A closing cut rewires nothing, so the glued orientation reads a surviving flag exactly as the family at the lift does.

theorem RS.EdgeSubset.isOut_glueDataOpen_pos {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟 : DataFamily V) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hEL : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hopen t) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag j)) = !(𝒟 (Fragment.liftSubsetOpen hopen t) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag i))) (f' : V.SurvivingFlag i j) : (glueDataOpen hij hopen 𝒟 t hct hEt hnet).snd.isOut f' = (𝒟 (Fragment.liftSubsetOpen hopen t) hcL hEL hneL).snd.isOut ↑f'

The open glue's directions where it applies.

theorem RS.EdgeSubset.match_dataFamily_congr {L : Type} [LinearOrder L] {V : Fragment L} (𝒟 : DataFamily V) {s₁ s₂ : Finset V.Flag} (hs : s₁ = s₂) (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.pairing f ∈ s₂) (hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian) (hne₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData) (f : V.Flag) : (𝒟 s₁ hc₁ hE₁ hne₁).fst.match_ f = (𝒟 s₂ hc₂ hE₂ hne₂).fst.match_ f

A family at equal subsets has the same partner map. The two values have different types, so the equality is read on the partner map rather than on the data.

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

A family at equal subsets has the same directions.

theorem RS.EdgeSubset.match_unglue_glueDataOpen {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟 : 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) (hdc : ∀ f ∈ V.dropSubset i j s, (V.gluePairOpen i j hij hopen).pairing f ∈ V.dropSubset i j s) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen (V.dropSubset i j s), V.pairing f ∈ Fragment.liftSubsetOpen hopen (V.dropSubset i j s)) (hEL : { flags := Fragment.liftSubsetOpen hopen (V.dropSubset i j s), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hopen (V.dropSubset i j s), pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hopen (V.dropSubset i j s)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag j)) = !(𝒟 (Fragment.liftSubsetOpen hopen (V.dropSubset i j s)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag i))) : (unglueDataOpen hij hopen (glueDataOpen hij hopen 𝒟) s hc hE hne).fst.MatchEq (𝒟 s hc hE hne).fst

The single-cut round trip, at an open cut. Lifting a family across the cut and pushing it back returns the system up to MatchEq — the glue rebuilds it rather than storing it.

theorem RS.EdgeSubset.isOut_unglue_glueDataOpen {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟 : 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) (hdc : ∀ f ∈ V.dropSubset i j s, (V.gluePairOpen i j hij hopen).pairing f ∈ V.dropSubset i j s) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen (V.dropSubset i j s), V.pairing f ∈ Fragment.liftSubsetOpen hopen (V.dropSubset i j s)) (hEL : { flags := Fragment.liftSubsetOpen hopen (V.dropSubset i j s), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetOpen hopen (V.dropSubset i j s), pairing_mem := hcL }.CanonData) (hag : (𝒟 (Fragment.liftSubsetOpen hopen (V.dropSubset i j s)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag j)) = !(𝒟 (Fragment.liftSubsetOpen hopen (V.dropSubset i j s)) hcL hEL hneL).snd.isOut (V.pairing (V.boundaryFlag i))) (f : V.Flag) (h1 : f ≠ V.boundaryFlag i) (h2 : f ≠ V.boundaryFlag j) : (unglueDataOpen hij hopen (glueDataOpen hij hopen 𝒟) s hc hE hne).snd.isOut f = (𝒟 s hc hE hne).snd.isOut f

The single-cut round trip on directions, at an open cut. At a surviving flag the round trip returns the direction on the nose.

theorem RS.EdgeSubset.match_unglue_glueDataClosed {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (𝒟 : 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) (hcL : ∀ f ∈ Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s)), V.pairing f ∈ Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s))) (hEL : { flags := Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s)), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s)), pairing_mem := hcL }.CanonData) : (unglueDataClosed hij hclosed (glueDataClosed hclosed (decide (V.boundaryFlag i ∈ s)) 𝒟) s hc hE hne).fst.MatchEq (𝒟 s hc hE hne).fst

The single-cut round trip, at a closing cut. With the bit the subset itself determines, lifting and pushing back returns the system up to MatchEq.

theorem RS.EdgeSubset.isOut_unglue_glueDataClosed {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (𝒟 : 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) (hcL : ∀ f ∈ Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s)), V.pairing f ∈ Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s))) (hEL : { flags := Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s)), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetClosed (V.dropSubset i j s) (decide (V.boundaryFlag i ∈ s)), pairing_mem := hcL }.CanonData) (f : V.Flag) (h1 : f ≠ V.boundaryFlag i) (h2 : f ≠ V.boundaryFlag j) : (unglueDataClosed hij hclosed (glueDataClosed hclosed (decide (V.boundaryFlag i ∈ s)) 𝒟) s hc hE hne).snd.isOut f = (𝒟 s hc hE hne).snd.isOut f

The single-cut round trip on directions, at a closing cut.

theorem RS.EdgeSubset.relabelData_roundTrip {α' β' : Type} [LinearOrder α'] [LinearOrder β'] (e : α' ≃o β') {W' : Fragment α'} (𝒟 : DataFamily W') : relabelDataDown e (relabelDataUp e 𝒟) = 𝒟

The relabel round trip is the identity on families.

theorem RS.EdgeSubset.dataOfEq_roundTrip {L : Type} [LinearOrder L] {V₁ V₂ : Fragment L} (h : V₁ = V₂) (𝒟 : DataFamily V₁) : dataOfEq h (dataOfEq ⋯ 𝒟) = 𝒟

The transport round trip is the identity on families.