Contracting the interface

RS21's (13) contracts the two fragments' tensors with the super form one leg at a time, and the closing display of Theorem 6's proof sums the result over the Eulerian subsets. In the flag model the composition glues one interface pair at a time, and each glue is exactly such a contraction: the glued fragment's summand is the base's summed over the two glued labels' colours against the cut's own kernel.

This file names the data that contraction carries — the fragment, the subset and the state at each stage — and the accumulated weight. The per-cut kernels are the ones the dispatches deliver: the super form at a closed cut, and at an open one the configuration's own kernel, which is the same form read in the basis the tensor twists into.

@[reducible]

def RS.EdgeSubset.contractOrder (n : ℕ) : LinearOrder (Fin (0 + n) ⊕ Fin (n + 0))

The lexicographic order on the recursion's label type.

Equations

• RS.EdgeSubset.contractOrder n = RS.sumLexLinearOrder (Fin (0 + n)) (Fin (n + 0))

@[reducible]

def RS.EdgeSubset.contractOrderSucc (n : ℕ) : LinearOrder (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0))

The same order one stage up.

Equations

• RS.EdgeSubset.contractOrderSucc n = RS.sumLexLinearOrder (Fin (0 + n + 1)) (Fin (n + 1 + 0))

The stage's fragment and state

noncomputable def RS.EdgeSubset.stepFragment (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) : Fragment (Fin (0 + n) ⊕ Fin (n + 0))

The fragment one stage down: glue the top interface pair, then relabel.

Equations

• RS.EdgeSubset.stepFragment n V = (V.gluePair (RS.EdgeSubset.cutL n) (RS.EdgeSubset.cutR n) ⋯).relabel (RS.interfaceStepEquiv 0 n 0)

The data a subset carries, and its summand

RS21 chooses an Eulerian orientation and a compatible local pairing for each Eulerian subset; the flag model's counterpart is a transition system with an orientation. A family of those — one per good subset — is what the interface recursion pushes forward, and the summand it names is RS21's s_h, with no chord sign in it.

def RS.EdgeSubset.DataFamily {L : Type} [LinearOrder L] (V : Fragment L) : Type

A choice of transition system and orientation at every good subset.

Equations

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

The data pushed back across one glue

The dispatch reads the base's summand at the unglued data, and an orientation only ever ungloues — building one across a glue is step 1 again. So the choice is made at the glued fragment and pushed back, which is the direction this construction runs.

noncomputable def RS.EdgeSubset.unglueDataOpen {L : Type} [LinearOrder L] {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟' : DataFamily (V.gluePairOpen i j hij hopen)) : DataFamily V

The glued fragment's data, read on the base. At a subset whose drop is closed under the rewire the base's data are the unglue of the glued fragment's; elsewhere any choice serves, the summand vanishing there.

Equations

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

theorem RS.EdgeSubset.unglueDataOpen_apply {L : Type} [LinearOrder L] {V : Fragment L} {i j : L} (hij : i ≠ j) (hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j) (𝒟' : DataFamily (V.gluePairOpen i j hij hopen)) (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) (t : Finset (V.SurvivingFlag i j)) (hdrop : V.dropSubset i j s = t) (hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t) (hF : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL } = { flags := s, pairing_mem := hc }) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) : unglueDataOpen hij hopen 𝒟' s hc hE hne = ⟨relOfEq hF (RelTransitionSystem.unglueOpen hij hopen t hct hcL (𝒟' t hct hEt hnet).fst), orientOfEq hF (unglueOrientationOpen hij hopen t hct hcL (𝒟' t hct hEt hnet).fst (𝒟' t hct hEt hnet).snd)⟩

The unglued data at an open cut, evaluated. As in the closed case the drop is abstracted, so that the dependent proofs the definition carries can be substituted rather than rewritten.

theorem RS.EdgeSubset.eulerian_liftClosed_iff' {L : Type} {V : Fragment L} {i j : L} (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (b : Bool) (s' : Finset (V.SurvivingFlag i j)) (hc' : ∀ f ∈ s', (V.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, V.pairing f ∈ Fragment.liftSubsetClosed s' b) : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.Eulerian ↔ { flags := s', pairing_mem := hc' }.Eulerian

A closed glue does not change any vertex's degree, so the lift is Eulerian exactly when the glued subset is.

noncomputable def RS.EdgeSubset.unglueDataClosed {L : Type} [LinearOrder L] {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (𝒟' : DataFamily (V.gluePairClosed i j hclosed)) : DataFamily V

The glued fragment's data at a closed cut, read on the base. Here no agreement is needed: a closed subset's drop is always closed under the glued pairing, the two cut flags being partners.

Equations

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

theorem RS.EdgeSubset.unglueDataClosed_apply {L : Type} [LinearOrder L] {V : Fragment L} {i j : L} (hij : i ≠ j) (hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j) (𝒟' : DataFamily (V.gluePairClosed i j hclosed)) (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) (t : Finset (V.SurvivingFlag i j)) (b : Bool) (hdrop : V.dropSubset i j s = t) (hb : decide (V.boundaryFlag i ∈ s) = b) (hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t) (hcL : ∀ f ∈ Fragment.liftSubsetClosed t b, V.pairing f ∈ Fragment.liftSubsetClosed t b) (hF : { flags := Fragment.liftSubsetClosed t b, pairing_mem := hcL } = { flags := s, pairing_mem := hc }) (hEt : { flags := t, pairing_mem := hct }.Eulerian) (hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) : unglueDataClosed hij hclosed 𝒟' s hc hE hne = ⟨relOfEq hF (RelTransitionSystem.unglueClosed hclosed b t hct hcL (𝒟' t hct hEt hnet).fst), orientOfEq hF (unglueOrientationClosed hclosed b t hct hcL (𝒟' t hct hEt hnet).fst (𝒟' t hct hEt hnet).snd)⟩

The unglued data, evaluated. The drop and the bit are abstracted so that the dependent proofs the definition carries can be substituted rather than rewritten: rewriting them in place is not type correct, every one of them mentioning the drop.