The composition's own sum #

At the composition there are no labels left: the through-edge product is one and the agreement is vacuous, so the flag model's summand is RS21's colouring sum times the circuit sign. This file names that sign as a weight on the composition's subsets and reads the constrained partition value as the weighted sum the iteration carries.

source

noncomputable def RS.EdgeSubset.circuitWeight {L : Type} [LinearOrder L] {V : Fragment L} (𝒟 : DataFamily V) (s : Finset V.Flag) :

ℂ

The circuit sign of a subset, off the family.

Equations

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

Instances For

source

theorem RS.EdgeSubset.circuitWeight_pos {L : Type} [LinearOrder L] {V : Fragment L} (𝒟 : DataFamily V) {s : Finset V.Flag} (hc : ∀ f ∈ s, V.pairing f ∈ s) (hE : { flags := s, pairing_mem := hc }.Eulerian) (hne : Nonempty { flags := s, pairing_mem := hc }.CanonData) :

circuitWeight 𝒟 s = (-1) ^ (𝒟 s hc hE hne).fst.openCircuitCount

At a good subset the circuit weight is the sign of the datum's own circuit count.

source

theorem RS.EdgeSubset.throughAgree_isEmpty {L : Type} {V : Fragment L} [IsEmpty L] {k ℓ : ℕ} (F : EdgeSubset V) (st : GenBoundaryState k ℓ L) (hbnd : genBoundarySubsetMatches V F.flags st) :

F.ThroughAgree st hbnd

At the composition the agreement is vacuous: there are no labelled ends.

source

theorem RS.EdgeSubset.throughSummand_eq_edgeSum {L : Type} [LinearOrder L] {V : Fragment L} [IsEmpty L] {k ℓ : ℕ} (F : EdgeSubset V) (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ L) (hbnd : genBoundarySubsetMatches V F.flags st) {κ : F.RelTransitionSystem} (o : κ.Orientation) (C : ℕ) :

F.throughSummand h st hbnd o C = (-1) ^ C * F.edgeSum h st hbnd o

At the composition the summand is the colouring sum, signed.

The composition's value, read on the base #

Putting the composition's own sum together with the iteration: the constrained value of a composition is the base's summands, summed over its subsets and over the interface colours, with the two fragments' own free circles in front. The composition's extra circles — one for each closing cut — are exactly the iteration's factor.

source

@[reducible]

def RS.EdgeSubset.baseOrder (n : ℕ) :

LinearOrder (Fin (0 + n) ⊕ Fin (n + 0))

The lexicographic order on the interface's label type.

Equations