The lift's round trip, and the identity at no cuts

The second half of the converse assembly: a stage of the lift followed by a stage of the push, the congruences that let that iterate over the interface, and the identity when the interface is empty.

@[reducible]

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

The lexicographic order on the interface's label type.

Equations

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

@[reducible]

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

The same order one stage up.

Equations

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

@[reducible]

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

The order the composition's own label type carries.

Equations

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

The stage round trip

The relabel and the transport cancel outright at the level of families, so a stage of the lift followed by a stage of the push is the single-cut round trip and nothing more.

theorem RS.EdgeSubset.stepData_roundTrip_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) : stepDataDown n V (stepDataUp n V b 𝒟) = unglueDataOpen ⋯ hop (glueDataOpen ⋯ hop 𝒟)

A stage of the lift, pushed back — at an open cut.

theorem RS.EdgeSubset.stepData_roundTrip_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) : stepDataDown n V (stepDataUp n V b 𝒟) = unglueDataClosed ⋯ hcl (glueDataClosed hcl b 𝒟)

A stage of the lift, pushed back — at a closing cut.

Ungluing sees the system only through its partners

So a stage of the push is insensitive to replacing the family it consumes by a matching-equal one — which is what the round trip delivers.

theorem RS.EdgeSubset.match_unglueOpen_matchEq {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (s' : Finset (V.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (V.gluePairOpen i j hij hopen).pairing f ∈ s') (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen s', V.pairing f ∈ Fragment.liftSubsetOpen hopen s') {κ₁ κ₂ : { flags := s', pairing_mem := hc' }.RelTransitionSystem} (hm : κ₁.MatchEq κ₂) {f : V.Flag} (hf : f ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hcL }.internalFlags) : (RelTransitionSystem.unglueOpen hij hopen s' hc' hcL κ₁).match_ f = (RelTransitionSystem.unglueOpen hij hopen s' hc' hcL κ₂).match_ f

Ungluing respects matching equality, at an open cut.

theorem RS.EdgeSubset.match_unglueClosed_matchEq {α : Type} [LinearOrder α] {V : Fragment α} {i j : α} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (b : Bool) (s' : Finset (V.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (V.gluePairClosed i j hclosed).pairing f ∈ s') (hcL : ∀ f ∈ Fragment.liftSubsetClosed s' b, V.pairing f ∈ Fragment.liftSubsetClosed s' b) {κ₁ κ₂ : { flags := s', pairing_mem := hc' }.RelTransitionSystem} (hm : κ₁.MatchEq κ₂) {f : V.Flag} (hf : f ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hcL }.internalFlags) : (RelTransitionSystem.unglueClosed hclosed b s' hc' hcL κ₁).match_ f = (RelTransitionSystem.unglueClosed hclosed b s' hc' hcL κ₂).match_ f

Ungluing respects matching equality, at a closing cut.

theorem RS.EdgeSubset.match_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), (𝒟₁ (V.dropSubset i j s) hct hEt hnet).fst.MatchEq (𝒟₂ (V.dropSubset i j s) hct hEt hnet).fst) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : (unglueDataOpen hij hopen 𝒟₁ s hc hE hne).fst.MatchEq (unglueDataOpen hij hopen 𝒟₂ s hc hE hne).fst

One subset is enough, at an open cut: the ungluing at s reads the family only at s's own drop.

theorem RS.EdgeSubset.match_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), (𝒟₁ (flagsOfEq V₁ V₂ h s) hc' hE' hne').fst.MatchEq (𝒟₂ (flagsOfEq V₁ V₂ h s) hc' hE' hne').fst) (hc : ∀ f ∈ s, V₁.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : (dataOfEq h 𝒟₁ s hc hE hne).fst.MatchEq (dataOfEq h 𝒟₂ s hc hE hne).fst

One subset is enough, under a transport.

theorem RS.EdgeSubset.match_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), (𝒟₁ s hc' hE' hne').fst.MatchEq (𝒟₂ s hc' hE' hne').fst) (hc : ∀ f ∈ s, W'.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : (relabelDataDown e 𝒟₁ s hc hE hne).fst.MatchEq (relabelDataDown e 𝒟₂ s hc hE hne).fst

One subset is enough, under a relabel.

theorem RS.EdgeSubset.match_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), (𝒟₁ t hct hEt hnet).fst.MatchEq (𝒟₂ t hct hEt hnet).fst) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : (stepDataDown n V 𝒟₁ s hc hE hne).fst.MatchEq (stepDataDown n V 𝒟₂ s hc hE hne).fst

One subset is enough, for a whole stage of the push at an open cut: the stage reads the family only at the stage subset the drop makes.

theorem RS.EdgeSubset.match_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), (𝒟₁ (V.dropSubset i j s) hct hEt hnet).fst.MatchEq (𝒟₂ (V.dropSubset i j s) hct hEt hnet).fst) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : (unglueDataClosed hij hclosed 𝒟₁ s hc hE hne).fst.MatchEq (unglueDataClosed hij hclosed 𝒟₂ s hc hE hne).fst

One subset is enough, at a closing cut: the push reads the glued family only at the subset the drop makes.

theorem RS.EdgeSubset.match_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), (𝒟₁ t hct hEt hnet).fst.MatchEq (𝒟₂ t hct hEt hnet).fst) (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) : (stepDataDown n V 𝒟₁ s hc hE hne).fst.MatchEq (stepDataDown n V 𝒟₂ s hc hE hne).fst

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

theorem RS.EdgeSubset.match_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) : (pushData 0 V (liftData 0 V bits 𝒟) s hc hE hne).fst.MatchEq (𝒟 s hc hE hne).fst

The interface round trip, at no cuts. The lift and the push are inverse outright.

theorem RS.EdgeSubset.match_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), (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).fst.MatchEq (stepDataUp n V (bits (Fin.last n)) 𝒟 t hct hEt hnet).fst) (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)))) : (pushData (n + 1) V (liftData (n + 1) V bits 𝒟) s hc hE hne).fst.MatchEq (𝒟 s hc hE hne).fst

The interface round trip, one stage on — at an open cut, reading the family at the one stage subset the drop makes.

theorem RS.EdgeSubset.match_pushData_liftData_succ_closed_at (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : 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) (hbit : bits (Fin.last n) = decide (V.boundaryFlag (cutL n) ∈ s)) (hIH : ∀ (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), (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).fst.MatchEq (stepDataUp n V (bits (Fin.last n)) 𝒟 t hct hEt hnet).fst) (hcL : ∀ f ∈ Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s)), V.pairing f ∈ Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s))) (hEL : { flags := Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s)), pairing_mem := hcL }.Eulerian) (hneL : Nonempty { flags := Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s)), pairing_mem := hcL }.CanonData) : (pushData (n + 1) V (liftData (n + 1) V bits 𝒟) s hc hE hne).fst.MatchEq (𝒟 s hc hE hne).fst

The interface round trip, one stage on, at a closing cut, at one subset. The stage reads the family only at the subset the drop makes, and the stage's bit is the one the subset itself determines.

The summand factorizes over a disjoint union of closed

fragments

At empty label types the chord sign is one and every orientation is path-canonical, so the pinned disjoint-union factorization reads directly on the summand.

theorem RS.EdgeSubset.relabelDown_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₁) : relabelDown (finCongr ⋯) (leftSub { flags := closeJoin s₁ s₂, pairing_mem := hc }) = { flags := s₁, pairing_mem := hc₁ }

The base subset's left half, brought down to the first fragment, is the first subset. This is the form edgeSum_closeBase_eq_pairAgreeValue reads its data at.

theorem RS.EdgeSubset.relabelDown_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₂) : relabelDown (finCongr ⋯) (rightSub { flags := closeJoin s₁ s₂, pairing_mem := hc }) = { flags := s₂, pairing_mem := hc₂ }

The base subset's right half, brought down to the second fragment, is the second subset.

theorem RS.EdgeSubset.pairAgreeValue_congr_subset {t : ℕ} {W₁ W₂ : Fragment (Fin t)} {F₁ F₁' : EdgeSubset W₁} (h₁ : F₁ = F₁') {F₂ F₂' : EdgeSubset W₂} (h₂ : F₂ = F₂') {k ℓ : ℕ} (h : MixedFunctional k ℓ) {κ₁ : F₁.RelTransitionSystem} (o₁ : κ₁.Orientation) {κ₂ : F₂.RelTransitionSystem} (o₂ : κ₂.Orientation) (st : GenBoundaryState k ℓ (Fin t)) : F₁.pairAgreeValue F₂ h o₁ o₂ st = F₁'.pairAgreeValue F₂' h (orientOfEq h₁ o₁) (orientOfEq h₂ o₂) st

The agreement value transports along equalities of the two subsets. This is what lets (13)'s orientations, which live on the fragments' own subsets, be read on the base subset's halves.

theorem RS.EdgeSubset.pairAgreeValue_eq_edgeSum_closeJoin {k ℓ : ℕ} (h : MixedFunctional k ℓ) (t : ℕ) (F G : Fragment (Fin t)) {s₁ : Finset F.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) {s₂ : Finset G.Flag} (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) {κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem} (o₁ : κ₁.Orientation) {κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem} (o₂ : κ₂.Orientation) (x : GenBoundaryState k ℓ (Fin t)) (hbnd : genBoundarySubsetMatches (closeBase F G) (closeJoin s₁ s₂) (diagOf t x)) (hbnd₁ : genBoundarySubsetMatches F (leftSub { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }).flags x) (hbnd₂ : genBoundarySubsetMatches G (rightSub { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }).flags x) : { flags := s₁, pairing_mem := hc₁ }.pairAgreeValue { flags := s₂, pairing_mem := hc₂ } h o₁ o₂ x = { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.edgeSum h (diagOf t x) hbnd (prodOrient (relabelOrientUp (finCongr ⋯) (relabelDown (finCongr ⋯) (leftSub { flags := closeJoin s₁ s₂, pairing_mem := ⋯ })) (orientOfEq ⋯ o₁)) (relabelOrientUp (finCongr ⋯) (relabelDown (finCongr ⋯) (rightSub { flags := closeJoin s₁ s₂, pairing_mem := ⋯ })) (orientOfEq ⋯ o₂)))

The pair's agreement value is the base subset's colouring sum. RS21's (13) produces its orientations on the fragments' own subsets; this reads the resulting agreement value on the base.

theorem RS.EdgeSubset.ne_boundaryFlag_of_mem_internalFlags {L : Type} {V : Fragment L} (F : EdgeSubset V) {f : V.Flag} (hf : f ∈ F.internalFlags) (a : L) : f ≠ V.boundaryFlag a

An internal flag is not a boundary flag: it is attached to a vertex.

theorem RS.EdgeSubset.edgeTermAt_eq_signed_edgeSum_internal {k ℓ : ℕ} {L : Type} [LinearOrder L] {V : Fragment L} (h : MixedFunctional k ℓ) (𝒟 : DataFamily V) (st : GenBoundaryState k ℓ L) {s : Finset V.Flag} (hc : ∀ f ∈ s, V.pairing f ∈ s) (hbnd : genBoundarySubsetMatches V s st) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) (C : ℕ) {κ : { flags := s, pairing_mem := hc }.RelTransitionSystem} (O : κ.Orientation) (hm : (𝒟 s hc hE hne).fst.MatchEq κ) (hio : ∀ f ∈ { flags := s, pairing_mem := hc }.internalFlags, (𝒟 s hc hE hne).snd.isOut f = O.isOut f) : edgeTermAt h 𝒟 st s C = (-1) ^ C * { flags := s, pairing_mem := hc }.edgeSum h st hbnd O

A subset's term is its colouring sum at any data of the same shape, needing the directions only where the sum reads them.

theorem RS.EdgeSubset.pairing_boundaryFlag_intL {t : ℕ} (F G : Fragment (Fin t)) (m : Fin t) : (closeBase F G).pairing ((closeBase F G).boundaryFlag (intL t m)) = Sum.inl ((F.relabel (finCongr ⋯)).pairing ((F.relabel (finCongr ⋯)).boundaryFlag (Fin.cast ⋯ m)))

The left interface partner, read on the disjoint union.

theorem RS.EdgeSubset.pairing_boundaryFlag_intR {t : ℕ} (F G : Fragment (Fin t)) (m : Fin t) : (closeBase F G).pairing ((closeBase F G).boundaryFlag (intR t m)) = Sum.inr ((G.relabel (finCongr ⋯)).pairing ((G.relabel (finCongr ⋯)).boundaryFlag (Fin.cast ⋯ m)))

The right interface partner, read on the disjoint union.

@[reducible, inline]

noncomputable abbrev RS.EdgeSubset.cutFlagL {t : ℕ} (F G : Fragment (Fin t)) (m : Fin t) : (closeBase F G).Flag

The flag the left half of the m-th cut points at.

Equations

• RS.EdgeSubset.cutFlagL F G m = (RS.EdgeSubset.closeBase F G).pairing ((RS.EdgeSubset.closeBase F G).boundaryFlag (RS.EdgeSubset.intL t m))

@[reducible, inline]

noncomputable abbrev RS.EdgeSubset.cutFlagR {t : ℕ} (F G : Fragment (Fin t)) (m : Fin t) : (closeBase F G).Flag

The flag the right half of the m-th cut points at.

Equations

• RS.EdgeSubset.cutFlagR F G m = (RS.EdgeSubset.closeBase F G).pairing ((RS.EdgeSubset.closeBase F G).boundaryFlag (RS.EdgeSubset.intR t m))

theorem RS.EdgeSubset.internal_cutFlagL {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) {s₂ : Finset G.Flag} (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (m : Fin t) (hm : F.boundaryFlag m ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags) (hnt : ¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } m) : cutFlagL F G m ∈ { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.internalFlags

A used, non-through left label has an internal cut flag.

theorem RS.EdgeSubset.internal_cutFlagR {t : ℕ} {F G : Fragment (Fin t)} {s₁ : Finset F.Flag} (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁) {s₂ : Finset G.Flag} (hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂) (m : Fin t) (hm : G.boundaryFlag m ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags) (hnt : ¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } m) : cutFlagR F G m ∈ { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.internalFlags

A used, non-through right label has an internal cut flag.

The composition's weighted term is family-free

At an empty label type the circuit weight times the summand does not depend on which data compute it. This is what makes the composition's side of the identity independent of the family, one subset at a time.

theorem RS.EdgeSubset.circuitWeight_mul_edgeTermAt_indep {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) (u : Finset V.Flag) (C : ℕ) (𝒟 𝒟' : DataFamily V) : circuitWeight 𝒟 u * edgeTermAt h 𝒟 st u C = circuitWeight 𝒟' u * edgeTermAt h 𝒟' st u C

The weighted summand at the composition is family-free.