Boundary states over general label types

A boundary state gives one colour per boundary label: even when the boundary edge is outside the Eulerian subset, odd when it participates. The labels are an arbitrary type, because the single-pair gluing decomposition works label-locally and its states are indexed by the surviving labels of a gluePair rather than by an initial segment of ℕ.

def RS.GenBoundaryState (k ℓ : ℕ) (α : Type) : Type

A boundary state over an arbitrary label type: one colour per label, even (Sum.inl) when the boundary edge is outside the Eulerian subset and odd (Sum.inr) when it participates.

Equations

• RS.GenBoundaryState k ℓ α = (α → Fin k ⊕ Fin (2 * ℓ))

@[instance_reducible]

instance RS.instFintypeGenBoundaryStateOfDecidableEq {k ℓ : ℕ} {α : Type} [Fintype α] [DecidableEq α] : Fintype (GenBoundaryState k ℓ α)

Boundary states over a finite label type are finite in number.

Equations

• RS.instFintypeGenBoundaryStateOfDecidableEq = { elems := RS.instFintypeGenBoundaryStateOfDecidableEq._aux_1, complete := ⋯ }

@[instance_reducible]

noncomputable instance RS.instDecidableEqGenBoundaryState {k ℓ : ℕ} {α : Type} : DecidableEq (GenBoundaryState k ℓ α)

And can be compared, classically.

Equations

• RS.instDecidableEqGenBoundaryState = Classical.decEq (RS.GenBoundaryState k ℓ α)

theorem RS.card_genBoundaryState (k ℓ : ℕ) (α : Type) [Fintype α] [DecidableEq α] : Fintype.card (GenBoundaryState k ℓ α) = (k + 2 * ℓ) ^ Fintype.card α

There are (k + 2ℓ) colours per label, so that many states to the number of labels.

def RS.genBoundarySubsetMatches {k ℓ : ℕ} {α : Type} (W : Fragment α) (s : Finset W.Flag) (st : GenBoundaryState k ℓ α) : Prop

The boundary-membership constraint over a general label type.

Equations

• RS.genBoundarySubsetMatches W s st = ∀ (i : α), W.boundaryFlag i ∈ s ↔ ∃ (c : Fin (2 * ℓ)), st i = Sum.inr c

theorem RS.genBoundaryFlag_not_mem_of_even {k ℓ : ℕ} {α : Type} {W : Fragment α} {s : Finset W.Flag} {st : GenBoundaryState k ℓ α} (hbnd : genBoundarySubsetMatches W s st) (i : α) (c : Fin k) (hst : st i = Sum.inl c) : W.boundaryFlag i ∉ s

An even-coloured label's boundary flag is outside matching subsets.

def RS.genEvenBoundaryMatch {k ℓ : ℕ} {α : Type} {W : Fragment α} (F : EdgeSubset W) (st : GenBoundaryState k ℓ α) (hbnd : genBoundarySubsetMatches W F.flags st) (ψ : F.EvenColouring k) : Prop

The even-colouring boundary constraint over a general label type.

Equations

• RS.genEvenBoundaryMatch F st hbnd ψ = ∀ (i : α) (c : Fin k) (hst : st i = Sum.inl c), ↑ψ ⟨W.boundaryFlag i, ⋯⟩ = c