The data the interface recursion carries

RS21 composes two fragments in one step; the flag model glues the interface one pair at a time, so the ledger (14) is proved by a recursion over glueInterface. What the recursion carries is a subset of the current fragment, a transition system on it, and the record that the subset uses the two halves of every remaining interface pair together — the condition that makes the interface matching exist and that a glue preserves.

This file names that data and the step that advances it.

@[reducible]

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

The lexicographic order on the recursion's label type, as the ambient instance. It has to outrank the sum's own ≤, which otherwise wins on a sum type and does not agree with it.

Equations

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

@[reducible]

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

The same order one stage up, where the index shape differs.

Equations

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

@[reducible, inline]

abbrev RS.EdgeSubset.cutL (n : ℕ) : Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)

The left label of the pair the recursion glues at size n+1.

Equations

• RS.EdgeSubset.cutL n = Sum.inl ⟨0 + n, ⋯⟩

@[reducible, inline]

abbrev RS.EdgeSubset.cutR (n : ℕ) : Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)

The right label of the pair the recursion glues at size n+1.

Equations

• RS.EdgeSubset.cutR n = Sum.inr ⟨n, ⋯⟩

theorem RS.EdgeSubset.cutL_ne_cutR (n : ℕ) : cutL n ≠ cutR n

The two labels of the pair being glued are distinct.

@[reducible]

noncomputable def RS.EdgeSubset.stepIso (n : ℕ) : Fragment.SurvivingLabel (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n) ≃o Fin (0 + n) ⊕ Fin (n + 0)

The relabel the recursion performs after a glue. The order has to be pinned: on a sum type the ambient ≤ is the sum's own, which is not the lexicographic one the interface uses.

Equations

• RS.EdgeSubset.stepIso n = RS.interfaceStepOrderIso 0 n 0

noncomputable def RS.EdgeSubset.stepSwap (n : ℕ) : Fragment.SurvivingLabel (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n) → Fragment.SurvivingLabel (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)

The swap on the labels surviving the glue: the next stage's swap, read back through the relabel.

Equations

• RS.EdgeSubset.stepSwap n x = (RS.interfaceStepEquiv 0 n 0).symm (RS.EdgeSubset.interfaceSwap (RS.EdgeSubset.stepIdent n) ((RS.interfaceStepEquiv 0 n 0) x))

theorem RS.EdgeSubset.stepSwap_val (n : ℕ) (x : Fragment.SurvivingLabel (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n)) : ↑(stepSwap n x) = interfaceSwap (stepIdent (n + 1)) ↑x

The surviving-label swap agrees with the current stage's interface swap on underlying labels.

theorem RS.EdgeSubset.interfaceSwap_cutL (n : ℕ) : interfaceSwap (stepIdent (n + 1)) (cutL n) = cutR n

The interface swap exchanges the pair the recursion glues.

structure RS.EdgeSubset.StageData (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : Type

The data one stage of the recursion carries.

• sub : EdgeSubset V

  The subset of the current fragment.

• paired : self.sub.SwapPaired (interfaceSwap (stepIdent n))

  It uses the two halves of every remaining interface pair together.

• rel : self.sub.RelTransitionSystem

  A transition system on it.

One step

Gluing the top interface pair takes the subset to its drop, the system to its glue, and the pairing record along with them; the relabel that follows carries all three. The subset's own pairing record is what makes the step total: it is exactly the condition under which the drop is closed under the glued pairing.

The two branches are built over the fragment each glue actually produces, and the dispatch Fragment.gluePair performs is undone once, on the finished data.

noncomputable def RS.EdgeSubset.stepFlags (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) : Finset (V.SurvivingFlag (cutL n) (cutR n))

The flags the glue passes down: the subset's, less the two glued ones.

Equations

• RS.EdgeSubset.stepFlags n V D = V.dropSubset (RS.EdgeSubset.cutL n) (RS.EdgeSubset.cutR n) D.sub.flags

noncomputable def RS.EdgeSubset.stepBit (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) : Bool

Whether the subset carries the closed cut's own edge.

Equations

• RS.EdgeSubset.stepBit n V D = decide (V.boundaryFlag (RS.EdgeSubset.cutL n) ∈ D.sub.flags)

noncomputable def RS.EdgeSubset.stageDataOfEq {m : ℕ} {V₁ V₂ : Fragment (Fin (0 + m) ⊕ Fin (m + 0))} (h : V₁ = V₂) (Dm : StageData m V₁) : StageData m V₂

Transport the stage data along an equality of fragments.

Equations

• RS.EdgeSubset.stageDataOfEq h Dm = h ▸ Dm

theorem RS.EdgeSubset.stepFlags_closed_pairing_mem (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (f : V.SurvivingFlag (cutL n) (cutR n)) : f ∈ stepFlags n V D → (V.gluePairClosed (cutL n) (cutR n) hcl).pairing f ∈ stepFlags n V D

On a closed cut the passed-down flags are edge-closed in the glued fragment.

theorem RS.EdgeSubset.liftSubsetClosed_stepFlags (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : Fragment.liftSubsetClosed (stepFlags n V D) (stepBit n V D) = D.sub.flags

Lifting the passed-down flags back through a closed glue recovers the subset's flags.

theorem RS.EdgeSubset.liftSubsetClosed_stepFlags_pairing_mem (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (f : V.Flag) : f ∈ Fragment.liftSubsetClosed (stepFlags n V D) (stepBit n V D) → V.pairing f ∈ Fragment.liftSubsetClosed (stepFlags n V D) (stepBit n V D)

The lifted flags are edge-closed in the unglued fragment.

theorem RS.EdgeSubset.sub_eq_liftSubsetClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : D.sub = { flags := Fragment.liftSubsetClosed (stepFlags n V D) (stepBit n V D), pairing_mem := ⋯ }

The stage's subset is the lift of what the closed glue passes down: nothing is lost across the step.

@[reducible]

noncomputable def RS.EdgeSubset.stepSubClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : EdgeSubset (V.gluePairClosed (cutL n) (cutR n) hcl)

The glued subset at a closed cut.

Equations

• RS.EdgeSubset.stepSubClosed n V D hcl = { flags := RS.EdgeSubset.stepFlags n V D, pairing_mem := ⋯ }

noncomputable def RS.EdgeSubset.stepDataClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : StageData n ((V.gluePairClosed (cutL n) (cutR n) hcl).relabel (interfaceStepEquiv 0 n 0))

One step at a closed cut.

Equations

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

theorem RS.EdgeSubset.agreeingSubset_sub (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) : AgreeingSubset (cutL n) (cutR n) D.sub.flags

The stage's subset uses the two halves of the glued pair together — the record the recursion carries.

theorem RS.EdgeSubset.stepFlags_open_pairing_mem (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (f : V.SurvivingFlag (cutL n) (cutR n)) : f ∈ stepFlags n V D → (V.gluePairOpen (cutL n) (cutR n) ⋯ hop).pairing f ∈ stepFlags n V D

On an open cut the passed-down flags are edge-closed in the glued fragment.

theorem RS.EdgeSubset.liftSubsetOpen_stepFlags (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : Fragment.liftSubsetOpen hop (stepFlags n V D) = D.sub.flags

Lifting the passed-down flags back through an open glue recovers the subset's flags.

theorem RS.EdgeSubset.liftSubsetOpen_stepFlags_pairing_mem (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (f : V.Flag) : f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D) → V.pairing f ∈ Fragment.liftSubsetOpen hop (stepFlags n V D)

The lifted flags are edge-closed in the unglued fragment.

theorem RS.EdgeSubset.sub_eq_liftSubsetOpen (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : D.sub = { flags := Fragment.liftSubsetOpen hop (stepFlags n V D), pairing_mem := ⋯ }

The open-cut analogue: the stage's subset is the lift.

@[reducible]

noncomputable def RS.EdgeSubset.stepSubOpen (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : EdgeSubset (V.gluePairOpen (cutL n) (cutR n) ⋯ hop)

The glued subset at an open cut.

Equations

• RS.EdgeSubset.stepSubOpen n V D hop = { flags := RS.EdgeSubset.stepFlags n V D, pairing_mem := ⋯ }

noncomputable def RS.EdgeSubset.stepDataOpen (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : StageData n ((V.gluePairOpen (cutL n) (cutR n) ⋯ hop).relabel (interfaceStepEquiv 0 n 0))

One step at an open cut.

Equations

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

noncomputable def RS.EdgeSubset.stepData (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) : StageData n ((V.gluePair (cutL n) (cutR n) ⋯).relabel (interfaceStepEquiv 0 n 0))

One step of the recursion: glue the top interface pair and relabel.

Equations

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

The recursion

Iterating the step over the whole interface carries the data to the composed fragment, and the accumulator records the cuts at which a component of the union disappears: the closed ones whose edge the subset carries.

noncomputable def RS.EdgeSubset.endEquiv : Fin (0 + 0) ⊕ Fin (0 + 0) ≃ Fin 0 ⊕ Fin 0

The relabel that closes the recursion at the empty interface.

Equations

• RS.EdgeSubset.endEquiv = (finCongr RS.EdgeSubset.endEquiv._proof_2).sumCongr (finCongr RS.EdgeSubset.endEquiv._proof_2)

noncomputable def RS.EdgeSubset.glueData (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : StageData n V → StageData 0 (glueInterface 0 n 0 V)

The data carried to the composed fragment.

Equations

• RS.EdgeSubset.glueData 0 x_3 D = { sub := RS.EdgeSubset.relabelUp RS.EdgeSubset.endEquiv D.sub, paired := ⋯, rel := RS.relabelTransUp RS.EdgeSubset.endEquiv D.sub D.rel }
• RS.EdgeSubset.glueData n.succ V D = RS.EdgeSubset.glueData n ((V.gluePair (Sum.inl ⟨0 + n, ⋯⟩) (Sum.inr ⟨n, ⋯⟩) ⋯).relabel (RS.interfaceStepEquiv 0 n 0)) (RS.EdgeSubset.stepData n V D)

noncomputable def RS.EdgeSubset.glueCount (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : StageData n V → ℕ

The cuts at which a component disappears: the closed ones whose edge the subset carries.

Equations

• One or more equations did not get rendered due to their size.
• RS.EdgeSubset.glueCount 0 x_3 D = 0

The ledger the recursion transports

RS21's (14) compares the composed system's circuit count with the two fragments' counts and the number of components of the union. In the recursion that quantity is read at every stage, of the current fragment's own system and the interface matching still to be glued.

noncomputable def RS.EdgeSubset.ledgerOf {n : ℕ} {V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))} (F : EdgeSubset V) (hp : F.SwapPaired (interfaceSwap (stepIdent n))) (κ : F.RelTransitionSystem) : ℕ

The ledger at one stage: the circuit count plus the number of components of the union with the interface matching.

Equations

• F.ledgerOf hp κ = κ.openCircuitCount + (RS.cutMatching F κ (RS.relBuildOrientation κ)).unionCount (F.interfaceCut (RS.EdgeSubset.stepIdent n) ⋯)

noncomputable def RS.EdgeSubset.stageLedger (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (D : StageData n V) : ℕ

The ledger of a stage's data.

Equations

• RS.EdgeSubset.stageLedger n V D = D.sub.ledgerOf ⋯ D.rel

theorem RS.EdgeSubset.ledgerOf_congr {n : ℕ} {V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))} {F F' : EdgeSubset V} (hF : F = F') (hp : F.SwapPaired (interfaceSwap (stepIdent n))) (hp' : F'.SwapPaired (interfaceSwap (stepIdent n))) (κ : F.RelTransitionSystem) : F'.ledgerOf hp' (relOfEq hF κ) = F.ledgerOf hp κ

The ledger does not see which of two equal subsets it is stated at.

theorem RS.EdgeSubset.stageLedger_stageDataOfEq {m : ℕ} {V₁ V₂ : Fragment (Fin (0 + m) ⊕ Fin (m + 0))} (h : V₁ = V₂) (D : StageData m V₁) : stageLedger m V₂ (stageDataOfEq h D) = stageLedger m V₁ D

Transporting the stage data along an equality of fragments does not change its ledger.

theorem RS.EdgeSubset.stepData_eq_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : stepData n V D = stageDataOfEq ⋯ (stepDataClosed n V D hcl)

On a closed cut the step is the closed branch, transported.

theorem RS.EdgeSubset.stepData_eq_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : stepData n V D = stageDataOfEq ⋯ (stepDataOpen n V D hop)

On an open cut the step is the open branch, transported.

One stage of the ledger

Each branch of the step is discharged by the stage theorem for its kind of cut, at the interface matching and any orientation — the ledger reads neither the orientation nor which proof of the pairing record is supplied.

theorem RS.EdgeSubset.stageLedger_stepDataClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : (stageLedger n ((V.gluePairClosed (cutL n) (cutR n) hcl).relabel (interfaceStepEquiv 0 n 0)) (stepDataClosed n V D hcl) + if stepBit n V D = true then 1 else 0) = stageLedger (n + 1) V D

The closed-cut step of the ledger: gluing a closed pair the subset carries closes one more circuit, so the ledger drops by the step bit.

theorem RS.EdgeSubset.stageLedger_stepDataOpen (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (D : StageData (n + 1) V) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : stageLedger n ((V.gluePairOpen (cutL n) (cutR n) ⋯ hop).relabel (interfaceStepEquiv 0 n 0)) (stepDataOpen n V D hop) = stageLedger (n + 1) V D

The open-cut step of the ledger: gluing an open pair closes nothing, so the ledger is unchanged.

RS21's (14)

The ledger is transported by the whole recursion: the composed system's circuit count, plus one for each closed cut whose edge the subset carries, is the starting system's circuit count plus the number of components of the union with the interface matching.

instance RS.EdgeSubset.stageEmpty : IsEmpty (Fin (0 + 0) ⊕ Fin (0 + 0))

At stage zero there are no labels left: the recursion's base.

theorem RS.EdgeSubset.ledgerOf_isEmpty {V : Fragment (Fin (0 + 0) ⊕ Fin (0 + 0))} (F : EdgeSubset V) (hp : F.SwapPaired (interfaceSwap (stepIdent 0))) (κ : F.RelTransitionSystem) : F.ledgerOf hp κ = κ.openCircuitCount

At the empty interface the ledger is the circuit count: there are no used labels, hence no components to count.

theorem RS.EdgeSubset.ledger_glueData (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (D : StageData n V) : stageLedger 0 (glueInterface 0 n 0 V) (glueData n V D) + glueCount n V D = stageLedger n V D

RS21's (14), transported by the recursion.

theorem RS.EdgeSubset.openCircuitCount_glueData (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (D : StageData n V) : (glueData n V D).rel.openCircuitCount + glueCount n V D = stageLedger n V D

RS21's (14). The composed system's circuit count, plus one for each closed cut whose edge the subset carries, is the starting system's circuit count plus the number of components of its union with the interface matching.

The circles the composition creates

A closed cut turns its edge into a free circle, and the partition function weights each by k - 2ℓ. RS21's graph model has no room for a vertex-free circle, so this is bookkeeping the flag model has to carry on its own; it depends only on the fragment, not on the subset.

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

The cuts the composition closes.

Equations

• One or more equations did not get rendered due to their size.
• RS.EdgeSubset.closedCuts 0 x_2 = 0

theorem RS.EdgeSubset.circles_glueInterface (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : (glueInterface 0 n 0 V).circles = V.circles + closedCuts n V

The composition's free circles.

The ledger at the start of the recursion

The recursion starts at the disjoint union of the two fragments, and there the ledger splits into RS21's own terms: the two circuit counts and the number of components of the union of the two chord matchings, read on one copy of the label set.

theorem RS.EdgeSubset.stageLedger_disjUnion (n : ℕ) {W₁ : Fragment (Fin (0 + n))} {W₂ : Fragment (Fin (n + 0))} (F : EdgeSubset (W₁.disjUnion W₂)) (hp : F.SwapPaired (interfaceSwap (stepIdent n))) (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) : stageLedger n (W₁.disjUnion W₂) { sub := F, paired := hp, rel := prodRel κ₁ κ₂ } = κ₁.openCircuitCount + κ₂.openCircuitCount + (cutMatching (leftSub F) κ₁ o₁).unionCount (DirMatching.map (F.interfaceSideDisjEquiv (stepIdent n) ⋯).symm (cutMatching (rightSub F) κ₂ o₂))

The ledger at a disjoint union.

def RS.EdgeSubset.stepIdentOrderIso (n : ℕ) : Fin (0 + n) ≃o Fin (n + 0)

The interface identification at size n, as an order isomorphism.

Equations

• RS.EdgeSubset.stepIdentOrderIso n = Fin.castOrderIso ⋯

theorem RS.EdgeSubset.sign_composition (n : ℕ) {W₁ : Fragment (Fin (0 + n))} {W₂ : Fragment (Fin (n + 0))} (F : EdgeSubset (W₁.disjUnion W₂)) (hp : F.SwapPaired (interfaceSwap (stepIdent n))) (κ₁ : (leftSub F).RelTransitionSystem) (κ₂ : (rightSub F).RelTransitionSystem) (o₁ : κ₁.Orientation) (o₂ : κ₂.Orientation) (M₁ : DirMatching (UsedLab (leftSub F))) (M₂ : DirMatching (UsedLab (rightSub F))) {m : ℕ} (hc₁ : Fintype.card (UsedLab (leftSub F)) = 2 * m) (hc₂ : Fintype.card (UsedLab (rightSub F)) = 2 * m) (hM₁ : M₁.edge = (cutMatching (leftSub F) κ₁ o₁).edge) (hM₂ : M₂.edge = (cutMatching (rightSub F) κ₂ o₂).edge) (halt : ∀ (a : UsedLab (leftSub F)), M₂.tail ((F.interfaceSideDisjOrderIso (stepIdentOrderIso n) ⋯) a) = !M₁.tail a) : ↑↑((DirMatching.stdMatching hc₁).sgnRel M₁) * (-1) ^ κ₁.openCircuitCount * (↑↑((DirMatching.stdMatching hc₂).sgnRel M₂) * (-1) ^ κ₂.openCircuitCount) = (-1) ^ ((glueData n (W₁.disjUnion W₂) { sub := F, paired := hp, rel := prodRel κ₁ κ₂ }).rel.openCircuitCount + glueCount n (W₁.disjUnion W₂) { sub := F, paired := hp, rel := prodRel κ₁ κ₂ })

RS21's (14), as the sign identity it is used as. The two fragments' matching signs and circuit signs multiply to the composed system's circuit sign, together with the sign of the cuts at which a component disappears.