The colouring correspondence at one cut

RS21 glues two open ends by removing the two labelled vertices and joining the two edges into one, so a colouring of the glued graph is a colouring of the two halves that agrees at the join — and the colour at the join is exactly the interface state's colour there. Summing the halves' colouring sums over that colour is therefore the glued graph's own colouring sum.

This file proves that, one cut at a time, for RS21's colouring sum edgeSum. The two ends of the cut are either both outside the subset, when the join carries an even colour, or both inside it, when it carries an odd one; the sum over the state's colour at the cut runs over the corresponding block.

The cut the subset misses

Neither glued flag is in the subset, so the join carries an even colour and the subset's own flags are the glued fragment's, unchanged.

theorem RS.EdgeSubset.boundaryFlagI_notMem_lift_of_miss {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hni : Fragment.partnerSurvI hopen ∉ t) : V.boundaryFlag i ∉ Fragment.liftSubsetOpen hopen t

The i-flag is out of the lift.

theorem RS.EdgeSubset.boundaryFlagJ_notMem_lift_of_miss {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hni : Fragment.partnerSurvI hopen ∉ t) : V.boundaryFlag j ∉ Fragment.liftSubsetOpen hopen t

The j-flag is out of the lift.

theorem RS.EdgeSubset.surviving_of_mem_lift_of_miss {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hni : Fragment.partnerSurvI hopen ∉ t) {f : V.Flag} (hf : f ∈ Fragment.liftSubsetOpen hopen t) : f ≠ V.boundaryFlag i ∧ f ≠ V.boundaryFlag j

A flag of the lift survives the glue.

noncomputable def RS.EdgeSubset.survOfLift {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hni : Fragment.partnerSurvI hopen ∉ t) {f : V.Flag} (hf : f ∈ Fragment.liftSubsetOpen hopen t) : V.SurvivingFlag i j

A flag of the lift, as a flag of the glued fragment.

Equations

• RS.EdgeSubset.survOfLift hij hopen t hct hni hf = ⟨f, ⋯⟩

theorem RS.EdgeSubset.survOfLift_mem {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hni : Fragment.partnerSurvI hopen ∉ t) {f : V.Flag} (hf : f ∈ Fragment.liftSubsetOpen hopen t) : survOfLift hij hopen t hct hni hf ∈ t

A flag of the lift, read as a glued flag, lies in the glued subset.

theorem RS.EdgeSubset.mem_lift_of_mem {L : Type} {V : Fragment L} {i j : L} (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) {g : V.SurvivingFlag i j} (hg : g ∈ t) : ↑g ∈ Fragment.liftSubsetOpen hopen t

Conversely a glued subset flag's underlying flag lies in the lift.

noncomputable def RS.EdgeSubset.oddColourEquivMiss {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hni : Fragment.partnerSurvI hopen ∉ t) (ℓ : ℕ) : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EdgeOddColouring ℓ ≃ { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ

Odd colourings agree across a missed cut. The cut's own edge is outside the subset, so the two sides colour the same edges.

Equations

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

theorem RS.EdgeSubset.edgeOddBoundaryMatch_miss {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hni : Fragment.partnerSurvI hopen ∉ t) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (a : Fin k) (φ : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EdgeOddColouring ℓ) : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) φ ↔ { flags := t, pairing_mem := hct }.edgeOddBoundaryMatch st' ((oddColourEquivMiss hij hopen t hct hcL hni ℓ) φ)

The odd boundary constraint matches across a missed cut.

theorem RS.EdgeSubset.sum_odd_miss {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hni : Fragment.partnerSurvI hopen ∉ t) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (a : Fin k) (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) : (∑ φ : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EdgeOddColouring ℓ, if { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) φ then ∏ v : V.Vertex, ↑({ flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.coreOddSignAt (unglueOrientationOpen hij hopen t hct hcL κ' o') φ.core v) * h.evalOdd ({ flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.evenColoursAt (evenPushOpen hij hopen t hct hcL hni ψ') v) ({ flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.coreOddListAt (unglueOrientationOpen hij hopen t hct hcL κ' o') φ.core v) else 0) = ∑ φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ, if { flags := t, pairing_mem := hct }.edgeOddBoundaryMatch st' φ' then ∏ v : V.Vertex, ↑({ flags := t, pairing_mem := hct }.coreOddSignAt o' φ'.core v) * h.evalOdd ({ flags := t, pairing_mem := hct }.evenColoursAt ψ' v) ({ flags := t, pairing_mem := hct }.coreOddListAt o' φ'.core v) else 0

The odd colouring sum transports across a missed cut.

theorem RS.EdgeSubset.edgeSum_openCut_miss {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hni : Fragment.partnerSurvI hopen ∉ t) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) [LinearOrder L] {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (hbnd' : genBoundarySubsetMatches (V.gluePairOpen i j hij hopen) t st') (hbndW : ∀ (a : Fin k), genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t) (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a))) : ∑ a : Fin k, { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeSum h (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) ⋯ (unglueOrientationOpen hij hopen t hct hcL κ' o') = { flags := t, pairing_mem := hct }.edgeSum h st' hbnd' o'

One missed cut, on RS21's colouring sums. The join carries an even colour, and that colour is the glued colouring's own at the far end of the cut — so the sum over it has a single term.

The cut the subset carries

Both glued flags are in the subset, so the join carries an odd colour; the even colourings are the same on both sides and the sum over the join's colour is absorbed by the odd ones.

theorem RS.EdgeSubset.boundaryFlagI_mem_lift_of_hit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hpi : Fragment.partnerSurvI hopen ∈ t) : V.boundaryFlag i ∈ Fragment.liftSubsetOpen hopen t

The i-flag is in the lift.

theorem RS.EdgeSubset.partnerSurvJ_mem_of_hit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) : Fragment.partnerSurvJ hopen ∈ t

The far end of the j-edge is in the subset too.

theorem RS.EdgeSubset.boundaryFlagJ_mem_lift_of_hit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) : V.boundaryFlag j ∈ Fragment.liftSubsetOpen hopen t

The j-flag is in the lift.

theorem RS.EdgeSubset.surviving_of_notMem_lift_of_hit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {f : V.Flag} (hf : f ∉ Fragment.liftSubsetOpen hopen t) : f ≠ V.boundaryFlag i ∧ f ≠ V.boundaryFlag j

A flag outside the lift survives the glue.

noncomputable def RS.EdgeSubset.survOfNotLift {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {f : V.Flag} (hf : f ∉ Fragment.liftSubsetOpen hopen t) : V.SurvivingFlag i j

A flag outside the lift, as a flag of the glued fragment.

Equations

• RS.EdgeSubset.survOfNotLift hij hopen t hct hpi hf = ⟨f, ⋯⟩

theorem RS.EdgeSubset.survOfNotLift_notMem {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {f : V.Flag} (hf : f ∉ Fragment.liftSubsetOpen hopen t) : survOfNotLift hij hopen t hct hpi hf ∉ t

A flag outside the lift, read as a glued flag, lies outside the glued subset.

theorem RS.EdgeSubset.notMem_lift_of_notMem {L : Type} {V : Fragment L} {i j : L} (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) {g : V.SurvivingFlag i j} (hg : g ∉ t) : ↑g ∉ Fragment.liftSubsetOpen hopen t

Conversely a flag outside the glued subset has its underlying flag outside the lift.

theorem RS.EdgeSubset.pairing_val_hit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {g : V.SurvivingFlag i j} (hg : g ∉ t) : ↑((V.gluePairOpen i j hij hopen).pairing g) = V.pairing ↑g

Away from the interface the glued pairing is the base's.

noncomputable def RS.EdgeSubset.evenColourEquivHit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) (k : ℕ) : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EvenColouring k ≃ { flags := t, pairing_mem := hct }.EvenColouring k

Even colourings agree across a carried cut. The cut's own edge is in the subset, so the two sides colour the same complement.

Equations

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

theorem RS.EdgeSubset.glued_odd_merged {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {ℓ : ℕ} (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) : ↑φ' ⟨Fragment.partnerSurvJ hopen, ⋯⟩ = ↑φ' ⟨Fragment.partnerSurvI hopen, hpi⟩

The glued colouring is constant across the join.

noncomputable def RS.EdgeSubset.oddPushHitFun {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {ℓ : ℕ} (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (f : ↥(Fragment.liftSubsetOpen hopen t)) : Fin (2 * ℓ)

The pushed colouring's value at a flag of the lift.

Equations

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

theorem RS.EdgeSubset.oddPushHitFun_at_i {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {ℓ : ℕ} (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (hP : V.boundaryFlag i ∈ Fragment.liftSubsetOpen hopen t) : oddPushHitFun hij hopen t hct hpi φ' ⟨V.boundaryFlag i, hP⟩ = ↑φ' ⟨Fragment.partnerSurvI hopen, hpi⟩

At the first glued boundary flag the pushed colouring takes the join's colour.

theorem RS.EdgeSubset.oddPushHitFun_at_j {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {ℓ : ℕ} (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (hP : V.boundaryFlag j ∈ Fragment.liftSubsetOpen hopen t) : oddPushHitFun hij hopen t hct hpi φ' ⟨V.boundaryFlag j, hP⟩ = ↑φ' ⟨Fragment.partnerSurvI hopen, hpi⟩

At the second it takes the same colour: the two ends of the join are one edge after gluing.

theorem RS.EdgeSubset.oddPushHitFun_agrees {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hpi : Fragment.partnerSurvI hopen ∈ t) {ℓ : ℕ} (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (g : V.SurvivingFlag i j) (h1 : ↑g ∈ Fragment.liftSubsetOpen hopen t) (h2 : g ∈ t) : oddPushHitFun hij hopen t hct hpi φ' ⟨↑g, h1⟩ = ↑φ' ⟨g, h2⟩

Away from the two glued flags the pushed colouring is the colouring it was pushed from.

noncomputable def RS.EdgeSubset.oddPushHit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) {ℓ : ℕ} (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EdgeOddColouring ℓ

Push a glued odd colouring up to the lift, colouring the two glued flags with the join's own colour.

Equations

• RS.EdgeSubset.oddPushHit hij hopen t hct hcL hpi φ' = ⟨RS.EdgeSubset.oddPushHitFun hij hopen t hct hpi φ', ⋯⟩

theorem RS.EdgeSubset.edgeOddBoundaryMatch_hit_iff {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) (oddPushHit hij hopen t hct hcL hpi φ') ↔ ↑φ' ⟨Fragment.partnerSurvI hopen, hpi⟩ = d ∧ { flags := t, pairing_mem := hct }.edgeOddBoundaryMatch st' φ'

The odd boundary constraint across a carried cut. It pins the join's colour to the state's, and is the glued constraint otherwise.

theorem RS.EdgeSubset.oddPushHit_injective {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) {ℓ : ℕ} : Function.Injective (oddPushHit hij hopen t hct hcL hpi)

The push is injective.

theorem RS.EdgeSubset.oddPushHit_covers {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (φW : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EdgeOddColouring ℓ) (hmatch : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) φW) : ∃ (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ), oddPushHit hij hopen t hct hcL hpi φ' = φW

Every colouring meeting the join's constraint is a push.

theorem RS.EdgeSubset.genEvenBoundaryMatch_hit_iff {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (hbndW : genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t) (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d))) (hbnd' : genBoundarySubsetMatches (V.gluePairOpen i j hij hopen) t st') (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) : genEvenBoundaryMatch { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL } (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) hbndW ((evenColourEquivHit hij hopen t hct hcL hpi k).symm ψ') ↔ genEvenBoundaryMatch { flags := t, pairing_mem := hct } st' hbnd' ψ'

The even boundary constraint across a carried cut.

theorem RS.EdgeSubset.sum_odd_hit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (G : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EdgeOddColouring ℓ → ℂ) : (∑ φW : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.EdgeOddColouring ℓ, if { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) φW then G φW else 0) = ∑ φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ, if { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) (oddPushHit hij hopen t hct hcL hpi φ') then G (oddPushHit hij hopen t hct hcL hpi φ') else 0

The odd colouring sum is a sum over the glued colourings.

theorem RS.EdgeSubset.edgeSum_openCut_hit {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hpi : Fragment.partnerSurvI hopen ∈ t) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (hbnd' : genBoundarySubsetMatches (V.gluePairOpen i j hij hopen) t st') (hbndW : ∀ (d : Fin (2 * ℓ)), genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t) (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d))) : ∑ d : Fin (2 * ℓ), { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeSum h (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) ⋯ (unglueOrientationOpen hij hopen t hct hcL κ' o') = { flags := t, pairing_mem := hct }.edgeSum h st' hbnd' o'

One carried cut, on RS21's colouring sums. The join carries an odd colour, and that colour is the glued colouring's own there — so again the sum over it has a single term.

The cut that closes

Gluing an edge whose two ends are both labelled removes it and leaves a free circle. RS21 records this explicitly; the colourings see it as two blocks — the edge outside the subset, carrying an even colour, and inside it, carrying an odd one — each of which is the glued fragment's colouring sum over again.

theorem RS.EdgeSubset.boundaryFlagI_notMem_liftClosed_false {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) : V.boundaryFlag i ∉ Fragment.liftSubsetClosed t false

The i-flag is out of the empty lift.

theorem RS.EdgeSubset.boundaryFlagJ_notMem_liftClosed_false {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) : V.boundaryFlag j ∉ Fragment.liftSubsetClosed t false

The j-flag is out of the empty lift.

theorem RS.EdgeSubset.surviving_of_mem_liftClosed_false {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) {f : V.Flag} (hf : f ∈ Fragment.liftSubsetClosed t false) : f ≠ V.boundaryFlag i ∧ f ≠ V.boundaryFlag j

A flag of the empty lift survives the glue.

noncomputable def RS.EdgeSubset.survOfLiftClosedFalse {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) {f : V.Flag} (hf : f ∈ Fragment.liftSubsetClosed t false) : V.SurvivingFlag i j

A flag of the empty lift, as a flag of the glued fragment.

Equations

• RS.EdgeSubset.survOfLiftClosedFalse hij t hf = ⟨f, ⋯⟩

theorem RS.EdgeSubset.mem_liftClosed_false_of_mem {L : Type} {V : Fragment L} {i j : L} (t : Finset (V.SurvivingFlag i j)) {g : V.SurvivingFlag i j} (hg : g ∈ t) : ↑g ∈ Fragment.liftSubsetClosed t false

A glued subset flag's underlying flag lies in the untaken closed lift.

theorem RS.EdgeSubset.survOfLiftClosedFalse_mem {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) {f : V.Flag} (hf : f ∈ Fragment.liftSubsetClosed t false) : survOfLiftClosedFalse hij t hf ∈ t

A flag of the untaken closed lift lies in the glued subset.

noncomputable def RS.EdgeSubset.oddColourEquivClosedFalse {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) (ℓ : ℕ) : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.EdgeOddColouring ℓ ≃ { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ

Odd colourings agree across a closing cut the subset misses.

Equations

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

theorem RS.EdgeSubset.edgeOddBoundaryMatch_closedFalse {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (a : Fin k) (φ : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.EdgeOddColouring ℓ) : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) φ ↔ { flags := t, pairing_mem := hct }.edgeOddBoundaryMatch st' ((oddColourEquivClosedFalse hij hclosed t hct hcL ℓ) φ)

The odd boundary constraint matches across a closing cut the subset misses.

noncomputable def RS.EdgeSubset.evenPushClosedFalseFun {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {k : ℕ} (a : Fin k) (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) (f : { g : V.Flag // g ∉ Fragment.liftSubsetClosed t false }) : Fin k

The pushed even colouring's value at a flag outside the lift.

Equations

• RS.EdgeSubset.evenPushClosedFalseFun hclosed t hct a ψ' f = if hfi : ↑f = V.boundaryFlag i then a else if hfj : ↑f = V.boundaryFlag j then a else ↑ψ' ⟨⟨↑f, ⋯⟩, ⋯⟩

theorem RS.EdgeSubset.evenPushClosedFalseFun_at_i {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {k : ℕ} (a : Fin k) (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) (hP : V.boundaryFlag i ∉ Fragment.liftSubsetClosed t false) : evenPushClosedFalseFun hclosed t hct a ψ' ⟨V.boundaryFlag i, hP⟩ = a

At the first glued boundary flag the pushed even colouring takes the summation colour.

theorem RS.EdgeSubset.evenPushClosedFalseFun_at_j {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {k : ℕ} (a : Fin k) (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) (hP : V.boundaryFlag j ∉ Fragment.liftSubsetClosed t false) : evenPushClosedFalseFun hclosed t hct a ψ' ⟨V.boundaryFlag j, hP⟩ = a

At the second it takes the same colour.

theorem RS.EdgeSubset.evenPushClosedFalseFun_agrees {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {k : ℕ} (a : Fin k) (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) (g : V.SurvivingFlag i j) (h1 : ↑g ∉ Fragment.liftSubsetClosed t false) (h2 : g ∉ t) : evenPushClosedFalseFun hclosed t hct a ψ' ⟨↑g, h1⟩ = ↑ψ' ⟨g, h2⟩

Away from the two glued flags the pushed even colouring is unchanged.

noncomputable def RS.EdgeSubset.evenPushClosedFalse {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) {k : ℕ} (a : Fin k) (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.EvenColouring k

Push a glued even colouring up to the lift, colouring the closed edge with the join's colour.

Equations

• RS.EdgeSubset.evenPushClosedFalse hij hclosed t hct hcL a ψ' = ⟨RS.EdgeSubset.evenPushClosedFalseFun hclosed t hct a ψ', ⋯⟩

theorem RS.EdgeSubset.evenPushClosedFalse_injective {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) {k : ℕ} (a : Fin k) : Function.Injective (evenPushClosedFalse hij hclosed t hct hcL a)

The push is injective.

theorem RS.EdgeSubset.genEvenBoundaryMatch_closedFalse_iff {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (a : Fin k) (hbndW : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t false) (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a))) (hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st') (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) : genEvenBoundaryMatch { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL } (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) hbndW (evenPushClosedFalse hij hclosed t hct hcL a ψ') ↔ genEvenBoundaryMatch { flags := t, pairing_mem := hct } st' hbnd' ψ'

The even boundary constraint across a closing cut the subset misses.

theorem RS.EdgeSubset.evenPushClosedFalse_covers {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (a : Fin k) (hbndW : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t false) (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a))) (ψW : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.EvenColouring k) (hmatch : genEvenBoundaryMatch { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL } (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) hbndW ψW) : ∃ (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k), evenPushClosedFalse hij hclosed t hct hcL a ψ' = ψW

Every colouring meeting the join's constraint is a push.

theorem RS.EdgeSubset.sum_even_closed_false {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (a : Fin k) (hbndW : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t false) (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a))) (G : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.EvenColouring k → ℂ) : (∑ ψW : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.EvenColouring k, if genEvenBoundaryMatch { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL } (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) hbndW ψW then G ψW else 0) = ∑ ψ' : { flags := t, pairing_mem := hct }.EvenColouring k, if genEvenBoundaryMatch { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL } (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) hbndW (evenPushClosedFalse hij hclosed t hct hcL a ψ') then G (evenPushClosedFalse hij hclosed t hct hcL a ψ') else 0

The even colouring sum is a sum over the glued colourings.

theorem RS.EdgeSubset.edgeSum_closedCut_false {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t false, V.pairing f ∈ Fragment.liftSubsetClosed t false) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (a : Fin k) (hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st') (hbndW : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t false) (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a))) : { flags := Fragment.liftSubsetClosed t false, pairing_mem := hcL }.edgeSum h (GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a)) hbndW (unglueOrientationClosed hclosed false t hct hcL κ' o') = { flags := t, pairing_mem := hct }.edgeSum h st' hbnd' o'

A closing cut the subset misses, on RS21's colouring sums. The closed edge carries the join's even colour and nothing else changes, so each of the k colours reproduces the glued sum.

theorem RS.EdgeSubset.boundaryFlagI_mem_liftClosed_true {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) : V.boundaryFlag i ∈ Fragment.liftSubsetClosed t true

The i-flag is in the carried lift.

theorem RS.EdgeSubset.boundaryFlagJ_mem_liftClosed_true {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) : V.boundaryFlag j ∈ Fragment.liftSubsetClosed t true

The j-flag is in the carried lift.

theorem RS.EdgeSubset.surviving_of_notMem_liftClosed_true {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) {f : V.Flag} (hf : f ∉ Fragment.liftSubsetClosed t true) : f ≠ V.boundaryFlag i ∧ f ≠ V.boundaryFlag j

A flag outside the carried lift survives the glue.

noncomputable def RS.EdgeSubset.survOfNotLiftClosedTrue {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) {f : V.Flag} (hf : f ∉ Fragment.liftSubsetClosed t true) : V.SurvivingFlag i j

A flag outside the carried lift, as a glued flag.

Equations

• RS.EdgeSubset.survOfNotLiftClosedTrue hij t hf = ⟨f, ⋯⟩

theorem RS.EdgeSubset.survOfNotLiftClosedTrue_notMem {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (t : Finset (V.SurvivingFlag i j)) {f : V.Flag} (hf : f ∉ Fragment.liftSubsetClosed t true) : survOfNotLiftClosedTrue hij t hf ∉ t

A flag outside the taken closed lift lies outside the glued subset.

theorem RS.EdgeSubset.mem_liftClosed_true_of_mem {L : Type} {V : Fragment L} {i j : L} (t : Finset (V.SurvivingFlag i j)) {g : V.SurvivingFlag i j} (hg : g ∈ t) : ↑g ∈ Fragment.liftSubsetClosed t true

A glued subset flag's underlying flag lies in the taken closed lift.

theorem RS.EdgeSubset.notMem_liftClosed_true_of_notMem {L : Type} {V : Fragment L} {i j : L} (t : Finset (V.SurvivingFlag i j)) {g : V.SurvivingFlag i j} (hg : g ∉ t) : ↑g ∉ Fragment.liftSubsetClosed t true

And a flag outside the glued subset lies outside it.

noncomputable def RS.EdgeSubset.evenColourEquivClosedTrue {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) (k : ℕ) : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.EvenColouring k ≃ { flags := t, pairing_mem := hct }.EvenColouring k

Even colourings agree across a closing cut the subset carries.

Equations

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

theorem RS.EdgeSubset.genEvenBoundaryMatch_closedTrue_iff {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (hbndW : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t true) (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d))) (hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st') (ψ' : { flags := t, pairing_mem := hct }.EvenColouring k) : genEvenBoundaryMatch { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT } (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) hbndW ((evenColourEquivClosedTrue hij hclosed t hct hcT k).symm ψ') ↔ genEvenBoundaryMatch { flags := t, pairing_mem := hct } st' hbnd' ψ'

The even boundary constraint across a closing cut the subset carries.

noncomputable def RS.EdgeSubset.oddPushClosedTrueFun {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {ℓ : ℕ} (d : Fin (2 * ℓ)) (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (f : ↥(Fragment.liftSubsetClosed t true)) : Fin (2 * ℓ)

The pushed odd colouring's value at a flag of the carried lift.

Equations

• RS.EdgeSubset.oddPushClosedTrueFun hclosed t hct d φ' f = if hfi : ↑f = V.boundaryFlag i then d else if hfj : ↑f = V.boundaryFlag j then d else ↑φ' ⟨⟨↑f, ⋯⟩, ⋯⟩

theorem RS.EdgeSubset.oddPushClosedTrueFun_at_i {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {ℓ : ℕ} (d : Fin (2 * ℓ)) (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (hP : V.boundaryFlag i ∈ Fragment.liftSubsetClosed t true) : oddPushClosedTrueFun hclosed t hct d φ' ⟨V.boundaryFlag i, hP⟩ = d

At the first glued boundary flag the pushed odd colouring takes the circle's colour.

theorem RS.EdgeSubset.oddPushClosedTrueFun_at_j {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {ℓ : ℕ} (d : Fin (2 * ℓ)) (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (hP : V.boundaryFlag j ∈ Fragment.liftSubsetClosed t true) : oddPushClosedTrueFun hclosed t hct d φ' ⟨V.boundaryFlag j, hP⟩ = d

At the second it takes the same colour.

theorem RS.EdgeSubset.oddPushClosedTrueFun_agrees {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) {ℓ : ℕ} (d : Fin (2 * ℓ)) (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) (g : V.SurvivingFlag i j) (h1 : ↑g ∈ Fragment.liftSubsetClosed t true) (h2 : g ∈ t) : oddPushClosedTrueFun hclosed t hct d φ' ⟨↑g, h1⟩ = ↑φ' ⟨g, h2⟩

Away from the two glued flags the pushed odd colouring is unchanged.

noncomputable def RS.EdgeSubset.oddPushClosedTrue {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) {ℓ : ℕ} (d : Fin (2 * ℓ)) (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.EdgeOddColouring ℓ

Push a glued odd colouring up to the carried lift, colouring the closed edge with the join's colour.

Equations

• RS.EdgeSubset.oddPushClosedTrue hij hclosed t hct hcT d φ' = ⟨RS.EdgeSubset.oddPushClosedTrueFun hclosed t hct d φ', ⋯⟩

theorem RS.EdgeSubset.oddPushClosedTrue_injective {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) {ℓ : ℕ} (d : Fin (2 * ℓ)) : Function.Injective (oddPushClosedTrue hij hclosed t hct hcT d)

The push is injective.

theorem RS.EdgeSubset.edgeOddBoundaryMatch_closedTrue_iff {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ) : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) (oddPushClosedTrue hij hclosed t hct hcT d φ') ↔ { flags := t, pairing_mem := hct }.edgeOddBoundaryMatch st' φ'

The odd boundary constraint across a closing cut the subset carries.

theorem RS.EdgeSubset.oddPushClosedTrue_covers {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (φW : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.EdgeOddColouring ℓ) (hmatch : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) φW) : ∃ (φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ), oddPushClosedTrue hij hclosed t hct hcT d φ' = φW

Every colouring meeting the join's constraint is a push.

theorem RS.EdgeSubset.sum_odd_closed_true {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) {k ℓ : ℕ} (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (G : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.EdgeOddColouring ℓ → ℂ) : (∑ φW : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.EdgeOddColouring ℓ, if { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) φW then G φW else 0) = ∑ φ' : { flags := t, pairing_mem := hct }.EdgeOddColouring ℓ, if { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.edgeOddBoundaryMatch (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) (oddPushClosedTrue hij hclosed t hct hcT d φ') then G (oddPushClosedTrue hij hclosed t hct hcT d φ') else 0

The odd colouring sum is a sum over the glued colourings.

theorem RS.EdgeSubset.edgeSum_closedCut_true {L : Type} {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (t : Finset (V.SurvivingFlag i j)) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcT : ∀ f ∈ Fragment.liftSubsetClosed t true, V.pairing f ∈ Fragment.liftSubsetClosed t true) (κ' : { flags := t, pairing_mem := hct }.RelTransitionSystem) (o' : κ'.Orientation) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j)) (d : Fin (2 * ℓ)) (hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st') (hbndW : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t true) (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d))) : { flags := Fragment.liftSubsetClosed t true, pairing_mem := hcT }.edgeSum h (GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d)) hbndW (unglueOrientationClosed hclosed true t hct hcT κ' o') = { flags := t, pairing_mem := hct }.edgeSum h st' hbnd' o'

A closing cut the subset carries, on RS21's colouring sums. The closed edge carries the join's odd colour and nothing else changes, so each of the 2ℓ colours reproduces the glued sum.