The closed identification at an arbitrary empty label type

The composition of two fragments is built at the label type Fin 0 ⊕ Fin 0 and then relabelled to Fin 0. The Definition 5 value lives at the latter, the colouring recursion at the former, so the two have to be matched across the relabel.

Both sides are the same sum of RS21 summands. At an empty label type the chord sign is one and the label chords are empty, so any two canonical data give the same summand; and the summand itself is carried across a relabel by relabel_throughSummand. Together these identify the relabelled fragment's Definition 5 value with the constrained value downstairs, with no independence input.

theorem RS.EdgeSubset.throughSummand_canon_indep {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (F : EdgeSubset V) (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) (hbnd : genBoundarySubsetMatches V F.flags st) (d₁ d₂ : F.CanonData) : F.throughSummand h st hbnd (↑d₁.snd) d₁.fst.openCircuitCount = F.throughSummand h st hbnd (↑d₂.snd) d₂.fst.openCircuitCount

At an empty label type the summand does not depend on the canonical data. The chord sign is one and the label chords are empty, so Proposition 3 equates the two signed values.

theorem RS.EdgeSubset.attach_inl_isEmpty {L : Type} [IsEmpty L] {V : Fragment L} (F : EdgeSubset V) (f : V.Flag) : f ∈ F.flags → ∃ (v : V.Vertex), V.attach f = Sum.inl v

Every flag of a subset at an empty label type is internally attached.

theorem RS.EdgeSubset.mixedValue_relabelUp_closed {L : Type} [LinearOrder L] {V : Fragment L} (e : L ≃o Fin 0) (F : EdgeSubset V) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) (hbnd : genBoundarySubsetMatches V F.flags st) (hE : F.Eulerian) (d : F.CanonData) : (relabelUp e.toEquiv F).mixedValue h = F.throughSummand h st hbnd (↑d.snd) d.fst.openCircuitCount

The relabelled fragment's Definition 5 value is the summand downstairs. Both are RS21's s_h(G,H) for the same subset.

theorem RS.EdgeSubset.genBoundarySubsetMatches_isEmpty {L : Type} [IsEmpty L] {V : Fragment L} {k ℓ : ℕ} (s : Finset V.Flag) (st : GenBoundaryState k ℓ L) : genBoundarySubsetMatches V s st

At an empty label type every subset matches every state.

def RS.EdgeSubset.emptyOrderIso {L : Type} [LinearOrder L] [IsEmpty L] (ee : L ≃ Fin 0) : L ≃o Fin 0

At an empty label type every bijection to Fin 0 is monotone.

Equations

• RS.EdgeSubset.emptyOrderIso ee = { toEquiv := ee, map_rel_iff' := ⋯ }

theorem RS.EdgeSubset.mixedPartition_relabel_orderIso {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} (e : L ≃o Fin 0) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) : mixedPartition h (V.relabel e.toEquiv) = throughMixedPartitionC h V st

The relabelled fragment's Definition 5 partition value is the constrained value downstairs, at a monotone relabel.

theorem RS.EdgeSubset.mixedPartition_relabel_closed {L : Type} [LinearOrder L] [IsEmpty L] {V : Fragment L} (ee : L ≃ Fin 0) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) : mixedPartition h (V.relabel ee) = throughMixedPartitionC h V st

The relabelled fragment's Definition 5 partition value is the constrained value downstairs. Monotonicity is automatic: there is nothing to compare.

theorem RS.EdgeSubset.mixedPartition_relabel_closed_of_eq {L : Type} [LinearOrder L] [IsEmpty L] (V₀ : Fragment L) (ee : L ≃ Fin 0) {V' : ClosedFragment} (hV : V' = V₀.relabel ee) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) : mixedPartition h V' = throughMixedPartitionC h V₀ st

The same identification, for a fragment presented as a relabel. Naming the relabelled fragment keeps the elaborator from having to solve for it under the relabel.