The closed and open masters

The per-subset ledgers and the open-cut engine, assembled into the master splitting identities.

The open engine: non-participating correspondences

theorem RS.EdgeSubset.hnj_of {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') : Fragment.partnerSurvJ hopen ∉ s'

The far end of the j-edge is also absent.

theorem RS.EdgeSubset.eulerian_lift_open_iff {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s') : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.Eulerian ↔ { flags := s', pairing_mem := hc' }.Eulerian

Eulerian transport across the open lift.

theorem RS.EdgeSubset.genBoundarySubsetMatches_glued_of_liftOpen {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) {k ℓ : ℕ} (st : GenBoundaryState k ℓ (Fragment.SurvivingLabel α i j)) (c c' : Fin k ⊕ Fin (2 * ℓ)) (hbndW : genBoundarySubsetMatches W (Fragment.liftSubsetOpen hopen s') (GenBoundaryState.extendPair i j st c c')) : genBoundarySubsetMatches (W.gluePairOpen i j hij hopen) s' st

The glued boundary-state constraint follows from the lifted one (open case).

Through product (open, non-participating)

In-flag lists (open)

theorem RS.EdgeSubset.relInFlagsAt_perm_open {α : 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) (v : W.Vertex) : ({ flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.relInFlagsAt (unglueOrientationOpen hij hopen s' hc' hc κ' o') v).Perm (List.map Subtype.val ({ flags := s', pairing_mem := hc' }.relInFlagsAt o' v))

The lifted in-flag list is a permutation of the projected glued in-flag list (open case).

theorem RS.EdgeSubset.mem_map_relInFlagsAt_internal_open {α : 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) {v : W.Vertex} (f : W.Flag) : f ∈ List.map Subtype.val ({ flags := s', pairing_mem := hc' }.relInFlagsAt o' v) → f ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.internalFlags

Members of the projected glued in-flag list are internal in the open lift.

Pointwise core data agreement (open)

List conversions (open)

Vertex data transports (open)

theorem RS.EdgeSubset.coreOddSignAt_transport_open {α : 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) {ℓ : ℕ} (φ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 = { flags := s', pairing_mem := hc' }.coreOddSignAt o' φ' v

The core odd sign at a vertex agrees (open).

theorem RS.EdgeSubset.evalOdd_coreOddListAt_transport_open {α : 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 }.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⟩) (μ : Multiset (Fin k)) (v : W.Vertex) : h.evalOdd μ ({ flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.coreOddListAt (unglueOrientationOpen hij hopen s' hc' hc κ' o') φW v) = h.evalOdd μ ({ flags := s', pairing_mem := hc' }.coreOddListAt o' φ' v)

The evaluated core odd list at a vertex agrees (open).

The even colouring correspondence (open)

noncomputable def RS.EdgeSubset.evenPushOpen {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k : ℕ} (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.EvenColouring k

Push a glued even colouring to the open lift: the two glued half-edges inherit the merged edge's colour.

Equations

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

theorem RS.EdgeSubset.evenPushOpen_agrees {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k : ℕ} (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) (g : W.SurvivingFlag i j) (h1 : ↑g ∉ Fragment.liftSubsetOpen hopen s') (h2 : g ∉ s') : ↑(evenPushOpen hij hopen s' hc' hc hni ψ') ⟨↑g, h1⟩ = ↑ψ' ⟨g, h2⟩

Pointwise agreement of the open even push at subset-avoiding surviving flags.

theorem RS.EdgeSubset.evenPushOpen_at_i {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k : ℕ} (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) (hP : W.boundaryFlag i ∉ Fragment.liftSubsetOpen hopen s') : ↑(evenPushOpen hij hopen s' hc' hc hni ψ') ⟨W.boundaryFlag i, hP⟩ = ↑ψ' ⟨Fragment.partnerSurvI hopen, hni⟩

The open even push at the two glued boundary flags.

theorem RS.EdgeSubset.evenPushOpen_at_j {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k : ℕ} (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) (hP : W.boundaryFlag j ∉ Fragment.liftSubsetOpen hopen s') : ↑(evenPushOpen hij hopen s' hc' hc hni ψ') ⟨W.boundaryFlag j, hP⟩ = ↑ψ' ⟨Fragment.partnerSurvJ hopen, ⋯⟩

The pushed even colouring at the second glued boundary flag.

theorem RS.EdgeSubset.evenPushOpen_injective {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k : ℕ} : Function.Injective (evenPushOpen hij hopen s' hc' hc hni)

The open even push is injective.

theorem RS.EdgeSubset.glued_even_merged {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k : ℕ} (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) : ↑ψ' ⟨Fragment.partnerSurvJ hopen, ⋯⟩ = ↑ψ' ⟨Fragment.partnerSurvI hopen, hni⟩

The glued constancy across the merged edge.

The even boundary match across the open glue

theorem RS.EdgeSubset.genEvenBoundaryMatch_open_iff {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') [LinearOrder α] {k ℓ : ℕ} (st : GenBoundaryState k ℓ (Fragment.SurvivingLabel α i j)) (a₀ : Fin k) (hbndW : genBoundarySubsetMatches W (Fragment.liftSubsetOpen hopen s') (GenBoundaryState.extendPair i j st (Sum.inl a₀) (Sum.inl a₀))) (hbnd' : genBoundarySubsetMatches (W.gluePairOpen i j hij hopen) s' st) (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) : genEvenBoundaryMatch { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } (GenBoundaryState.extendPair i j st (Sum.inl a₀) (Sum.inl a₀)) hbndW (evenPushOpen hij hopen s' hc' hc hni ψ') ↔ ↑ψ' ⟨Fragment.partnerSurvI hopen, hni⟩ = a₀ ∧ genEvenBoundaryMatch { flags := s', pairing_mem := hc' } st hbnd' ψ'

Even boundary matching transfers across an open cut: matching the extended state upstairs is matching the state downstairs.

theorem RS.EdgeSubset.evenPushOpen_covers {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k ℓ : ℕ} (st : GenBoundaryState k ℓ (Fragment.SurvivingLabel α i j)) (a₀ : Fin k) (hbndW : genBoundarySubsetMatches W (Fragment.liftSubsetOpen hopen s') (GenBoundaryState.extendPair i j st (Sum.inl a₀) (Sum.inl a₀))) (ψW : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.EvenColouring k) (hmatch : genEvenBoundaryMatch { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } (GenBoundaryState.extendPair i j st (Sum.inl a₀) (Sum.inl a₀)) hbndW ψW) : ∃ (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k), evenPushOpen hij hopen s' hc' hc hni ψ' = ψW

Every colouring satisfying the diagonal lifted match lies in the image of the open push.

theorem RS.EdgeSubset.sum_even_open {α : 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') (hni : Fragment.partnerSurvI hopen ∉ s') {k ℓ : ℕ} (st : GenBoundaryState k ℓ (Fragment.SurvivingLabel α i j)) (a₀ : Fin k) (hbndW : genBoundarySubsetMatches W (Fragment.liftSubsetOpen hopen s') (GenBoundaryState.extendPair i j st (Sum.inl a₀) (Sum.inl a₀))) (G : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.EvenColouring k → ℂ) : (∑ ψW : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.EvenColouring k, if genEvenBoundaryMatch { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } (GenBoundaryState.extendPair i j st (Sum.inl a₀) (Sum.inl a₀)) hbndW ψW then G ψW else 0) = ∑ ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k, if genEvenBoundaryMatch { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } (GenBoundaryState.extendPair i j st (Sum.inl a₀) (Sum.inl a₀)) hbndW (evenPushOpen hij hopen s' hc' hc hni ψ') then G (evenPushOpen hij hopen s' hc' hc hni ψ') else 0

The constrained lifted even sum reindexes along the open push.

The open per-subset master