Transport across a through-edge cut

A cut whose edge is a through-edge of the fragment -- both its flags on the boundary -- carries no vertex data, so the colour and vertex factors transport across the glue unchanged. The two transports here are what the colouring recursion needs at such a cut.

The shared participating context

The even-colouring layer (participating, any configuration)

theorem RS.EdgeSubset.multiset_map_eq_of_bijT {γ : Type u_1} {δ : Type u_2} {X : Type u_3} (s : Finset γ) (t : Finset δ) (e : δ → γ) (hinj : Function.Injective e) (hmem : ∀ (y : δ), y ∈ t ↔ e y ∈ s) (hsurj : ∀ x ∈ s, ∃ (y : δ), e y = x) (g : γ → X) (g' : δ → X) (hg : ∀ y ∈ t, g (e y) = g' y) : Multiset.map g s.val = Multiset.map g' t.val

Finset-supported multisets map equally along a bijection of their supports.

theorem RS.EdgeSubset.evenColoursAt_transport_T {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s') {k : ℕ} (ψW : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.EvenColouring k) (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) (hψ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∉ Fragment.liftSubsetOpen hopen s') (h2 : g ∉ s'), ↑ψW ⟨↑g, h1⟩ = ↑ψ' ⟨g, h2⟩) (v : W.Vertex) : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.evenColoursAt ψW v = { flags := s', pairing_mem := hc' }.evenColoursAt ψ' v

The even colour multiset agrees (participating case).

theorem RS.EdgeSubset.vertexFactor_transport_T {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s') (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (ψW : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.EvenColouring k) (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) (hψ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∉ Fragment.liftSubsetOpen hopen s') (h2 : g ∉ s'), ↑ψW ⟨↑g, h1⟩ = ↑ψ' ⟨g, h2⟩) (φW : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.CoreOddColouring ℓ) (φ' : { flags := s', pairing_mem := hc' }.CoreOddColouring ℓ) (hφ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.coreFlags) (h2 : g ∈ { flags := s', pairing_mem := hc' }.coreFlags), ↑φW ⟨↑g, h1⟩ = ↑φ' ⟨g, h2⟩) (v : W.Vertex) : ↑({ flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.coreOddSignAt (unglueOrientationOpen hij hopen s' hc' hc κ' o') φW v) * h.evalOdd ({ flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.evenColoursAt ψW v) ({ flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.coreOddListAt (unglueOrientationOpen hij hopen s' hc' hc κ' o') φW v) = ↑({ flags := s', pairing_mem := hc' }.coreOddSignAt o' φ' v) * h.evalOdd ({ flags := s', pairing_mem := hc' }.evenColoursAt ψ' v) ({ flags := s', pairing_mem := hc' }.coreOddListAt o' φ' v)

The vertex factor transport (participating case).