Iterating the glue

RS21's ∗ glues every interface pair at once; glueInterface glues them one at a time, top pair first, relabelling the survivors at each stage. This file carries RS21's summand along that iteration: the per-cut identities of EdgeTerm are the step, and the transports below are the bookkeeping the staging needs — the relabel at each stage and at the base, and the dispatch on whether the stage's cut closes.

The base of the iteration

At an empty interface the composition still relabels, between two label types that are both empty.

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

The order isomorphism the base stage relabels along.

Equations

• RS.EdgeSubset.baseIso = { toEquiv := (finCongr RS.EdgeSubset.baseIso._proof_2).sumCongr (finCongr RS.EdgeSubset.baseIso._proof_2), map_rel_iff' := @RS.EdgeSubset.baseIso._proof_4 }

Transporting a family along an equality of fragments

The stage's glue dispatches on whether the cut closes, and each branch is built over its own fragment; the finished family is carried back across that identification.

noncomputable def RS.EdgeSubset.flagsOfEq {β : Type} (V₁ V₂ : Fragment β) (hV : V₁ = V₂) (s : Finset V₁.Flag) : Finset V₂.Flag

Transport a set of flags along an equality of fragments.

Equations

• RS.EdgeSubset.flagsOfEq V₁ V₂ hV s = hV ▸ s

noncomputable def RS.EdgeSubset.dataOfEq {β : Type} [LinearOrder β] {V₁ V₂ : Fragment β} (hV : V₁ = V₂) (𝒟 : DataFamily V₂) : DataFamily V₁

Transport a data family along an equality of fragments.

Equations

• RS.EdgeSubset.dataOfEq hV 𝒟 = Eq.ndrec (motive := fun {V₂ : RS.Fragment β} => RS.EdgeSubset.DataFamily V₂ → RS.EdgeSubset.DataFamily V₁) (fun (𝒟 : RS.EdgeSubset.DataFamily V₁) => 𝒟) hV 𝒟

theorem RS.EdgeSubset.edgeTermAt_dataOfEq {β : Type} [LinearOrder β] {V₁ V₂ : Fragment β} (hV : V₁ = V₂) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (𝒟 : DataFamily V₂) (st : GenBoundaryState k ℓ β) (s : Finset V₁.Flag) (C : ℕ) : edgeTermAt h (dataOfEq hV 𝒟) st s C = edgeTermAt h 𝒟 st (flagsOfEq V₁ V₂ hV s) C

The summand reads the transported family on the transported subset.

One stage of the iteration

The stage glues the top interface pair and relabels the survivors. Its data family therefore comes back in two moves: pull along the relabel, then unglue.

@[reducible]

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

The lexicographic order on the stage's label type.

Equations

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

@[reducible]

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

The same order one stage up.

Equations

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

@[reducible]

def RS.EdgeSubset.recSurvOrder (n : ℕ) : LinearOrder (Fragment.SurvivingLabel (Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))

The order the surviving labels of a stage carry.

Equations

• RS.EdgeSubset.recSurvOrder n = RS.sumLexSubtypeLinearOrder (Fin (0 + n + 1)) (Fin (n + 1 + 0)) fun (x : Fin (0 + n + 1) ⊕ Fin (n + 1 + 0)) => x ≠ RS.EdgeSubset.cutL n ∧ x ≠ RS.EdgeSubset.cutR n

noncomputable def RS.EdgeSubset.stepDataGlued (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟 : DataFamily (stepFragment n V)) : DataFamily (V.gluePair (cutL n) (cutR n) ⋯)

The stage's family, pulled back along the relabel.

Equations

• RS.EdgeSubset.stepDataGlued n V 𝒟 = RS.EdgeSubset.relabelDataDown (RS.EdgeSubset.stepIso n) 𝒟

theorem RS.EdgeSubset.gluePair_eq_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) : V.gluePairClosed (cutL n) (cutR n) hcl = V.gluePair (cutL n) (cutR n) ⋯

The stage's glue, at a closing cut.

theorem RS.EdgeSubset.gluePair_eq_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) : V.gluePairOpen (cutL n) (cutR n) ⋯ hop = V.gluePair (cutL n) (cutR n) ⋯

The stage's glue, at an open cut.

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

One stage of the composition, on the data. The family is chosen at the composition and pushed back: along the relabel, then across the glue.

Equations

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

noncomputable def RS.EdgeSubset.stageState (n : ℕ) {k ℓ : ℕ} (stβ : GenBoundaryState k ℓ (Fin (0 + n) ⊕ Fin (n + 0))) : GenBoundaryState k ℓ (Fragment.SurvivingLabel (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)) (cutL n) (cutR n))

The stage's state, read back through the relabel.

Equations

• RS.EdgeSubset.stageState n stβ a = stβ ((RS.EdgeSubset.stepIso n) a)

theorem RS.EdgeSubset.edgeTermAt_stepOpen_all (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (𝒟 : DataFamily (stepFragment n V)) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) (stβ : GenBoundaryState k ℓ (Fin (0 + n) ⊕ Fin (n + 0))) (C : ℕ) : ∑ c : Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (stepDataDown n V 𝒟) (GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n stβ) c c) (Fragment.liftSubsetOpen hop t) C = edgeTermAt h 𝒟 stβ (flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t) C

One open stage, with nothing assumed of the subset.

theorem RS.EdgeSubset.edgeTermAt_stepClosed_false_all (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (𝒟 : DataFamily (stepFragment n V)) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) (stβ : GenBoundaryState k ℓ (Fin (0 + n) ⊕ Fin (n + 0))) (C : ℕ) : ∑ c : Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (stepDataDown n V 𝒟) (GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n stβ) c c) (Fragment.liftSubsetClosed t false) C = ↑k * edgeTermAt h 𝒟 stβ (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t) C

The empty branch of a closing stage weighs k, with nothing assumed of the subset.

theorem RS.EdgeSubset.edgeTermAt_stepClosed_true_all (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (𝒟 : DataFamily (stepFragment n V)) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) (stβ : GenBoundaryState k ℓ (Fin (0 + n) ⊕ Fin (n + 0))) (C : ℕ) : ∑ c : Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (stepDataDown n V 𝒟) (GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n stβ) c c) (Fragment.liftSubsetClosed t true) (C + 1) = -↑(2 * ℓ) * edgeTermAt h 𝒟 stβ (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t) C

The carried branch of a closing stage weighs −2ℓ, with nothing assumed of the subset.

theorem RS.EdgeSubset.edgeTermAt_stepClosed_all (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (𝒟 : DataFamily (stepFragment n V)) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) (stβ : GenBoundaryState k ℓ (Fin (0 + n) ⊕ Fin (n + 0))) (C : ℕ) : ∑ c : Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (stepDataDown n V 𝒟) (GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n stβ) c c) (Fragment.liftSubsetClosed t false) C + ∑ c : Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (stepDataDown n V 𝒟) (GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n stβ) c c) (Fragment.liftSubsetClosed t true) (C + 1) = (↑k - 2 * ↑ℓ) * edgeTermAt h 𝒟 stβ (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t) C

One closing stage, with nothing assumed of the subset.

The iteration

The family is chosen at the composition and pushed back stage by stage; the count the base is read at rises by one at each closing cut whose edge the subset carries, which is the ledger's glueCount.

@[reducible]

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

The lexicographic order on the stage's label type.

Equations

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

@[reducible]

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

The same order one stage up.

Equations

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

@[reducible]

def RS.EdgeSubset.closureOrder : LinearOrder (Fin 0 ⊕ Fin 0)

The order the composition's own (empty) label type carries.

Equations

• RS.EdgeSubset.closureOrder = RS.sumLexLinearOrder (Fin 0) (Fin 0)

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

The family, pushed back to the base. A choice at the composition determines one at every stage, by ungluing.

Equations

• RS.EdgeSubset.pushData 0 x_3 𝒟 = RS.EdgeSubset.relabelDataDown RS.EdgeSubset.baseIso 𝒟
• RS.EdgeSubset.pushData n.succ V 𝒟 = RS.EdgeSubset.stepDataDown n V (RS.EdgeSubset.pushData n (RS.EdgeSubset.stepFragment n V) 𝒟)

noncomputable def RS.EdgeSubset.carried (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : Finset V.Flag → ℕ

The closing cuts a subset carries. This is the ledger's glueCount, read on the colouring side: the count the base's summand is taken at rises by one at each of them.

Equations

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

noncomputable def RS.EdgeSubset.diagOf {k ℓ : ℕ} (n : ℕ) (x : Fin n → Fin k ⊕ Fin (2 * ℓ)) : GenBoundaryState k ℓ (Fin (0 + n) ⊕ Fin (n + 0))

The diagonal interface state: both ends of a cut carry the colour the composition gives it.

Equations

• RS.EdgeSubset.diagOf n x = Sum.elim (fun (a : Fin (0 + n)) => x (Fin.cast ⋯ a)) fun (b : Fin (n + 0)) => x (Fin.cast ⋯ b)

theorem RS.EdgeSubset.diagOf_succ {k ℓ : ℕ} (n : ℕ) (x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ)) : diagOf (n + 1) x = GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n (diagOf n fun (a : Fin n) => x a.castSucc)) (x (Fin.last n)) (x (Fin.last n))

The diagonal state, one stage down. Its top colour is the stage's cut colour, and the rest is the next stage's diagonal state.

theorem RS.EdgeSubset.carried_liftOpen (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) : carried (n + 1) V (Fragment.liftSubsetOpen hop t) = carried n (stepFragment n V) (flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t)

The carried count at an open stage is the next stage's.

theorem RS.EdgeSubset.carried_liftClosed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) (b : Bool) : carried (n + 1) V (Fragment.liftSubsetClosed t b) = (if b = true then 1 else 0) + carried n (stepFragment n V) (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t)

The carried count at a closing stage rises by one exactly when the subset carries the closed edge.

noncomputable def RS.EdgeSubset.emptyState {k ℓ : ℕ} : GenBoundaryState k ℓ (Fin 0 ⊕ Fin 0)

The composition's own state: its label type is empty.

Equations

• RS.EdgeSubset.emptyState a = isEmptyElim a

def RS.EdgeSubset.snocEquiv (n : ℕ) (α : Type) : (Fin n → α) × α ≃ (Fin (n + 1) → α)

The interface colours, split off the last cut.

Equations

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

theorem RS.EdgeSubset.sum_snoc {n : ℕ} {α : Type} [Fintype α] (F : (Fin (n + 1) → α) → ℂ) : ∑ x : Fin (n + 1) → α, F x = ∑ y : Fin n → α, ∑ c : α, F (Fin.snoc y c)

The interface colour sum, one cut at a time.

noncomputable def RS.EdgeSubset.imageOf (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : Finset V.Flag → Finset (glueInterface 0 n 0 V).Flag

The composition's subset a stage's subset maps to.

Equations

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

theorem RS.EdgeSubset.imageOf_succ_open (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (s : Finset V.Flag) : imageOf (n + 1) V s = imageOf n (stepFragment n V) (flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s))

The image, one stage down, at an open cut.

theorem RS.EdgeSubset.imageOf_succ_closed (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (s : Finset V.Flag) : imageOf (n + 1) V s = imageOf n (stepFragment n V) (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s))

The image, one stage down, at a closing cut.

theorem RS.EdgeSubset.sum_flagsOfEq {β : Type} {V₁ V₂ : Fragment β} (hV : V₁ = V₂) (F : Finset V₂.Flag → ℂ) : ∑ s : Finset V₂.Flag, F s = ∑ s : Finset V₁.Flag, F (flagsOfEq V₁ V₂ hV s)

Sums over the flags of identified fragments agree.

theorem RS.EdgeSubset.stageSum_snoc {k ℓ : ℕ} (h : MixedFunctional k ℓ) (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟 : DataFamily (stepFragment n V)) (C : ℕ) (W : Finset V.Flag → ℂ) : ∑ s : Finset V.Flag, ∑ x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ), W s * edgeTermAt h (stepDataDown n V 𝒟) (diagOf (n + 1) x) s (C + carried (n + 1) V s) = ∑ y : Fin n → Fin k ⊕ Fin (2 * ℓ), ∑ s : Finset V.Flag, ∑ c : Fin k ⊕ Fin (2 * ℓ), W s * edgeTermAt h (stepDataDown n V 𝒟) (GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n (diagOf n y)) c c) s (C + carried (n + 1) V s)

The stage's sum, with the interface colour split off.

noncomputable def RS.EdgeSubset.cutFactor (k ℓ n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) : Finset V.Flag → ℂ

The free circles a subset's own cuts contribute. At an open cut, nothing; at a closing cut, k if the subset leaves the cut's edge out and −2ℓ if it carries it — the free circle's two sectors, read one subset at a time.

Equations

• One or more equations did not get rendered due to their size.
• RS.EdgeSubset.cutFactor k ℓ 0 x_3 x_4 = 1

theorem RS.EdgeSubset.cutFactor_liftOpen (k ℓ n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) : cutFactor k ℓ (n + 1) V (Fragment.liftSubsetOpen hop t) = cutFactor k ℓ n (stepFragment n V) (flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t)

The factor at an open cut is the next stage's.

theorem RS.EdgeSubset.cutFactor_liftClosed (k ℓ n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (t : Finset (V.SurvivingFlag (cutL n) (cutR n))) (b : Bool) : cutFactor k ℓ (n + 1) V (Fragment.liftSubsetClosed t b) = (if b = true then -↑(2 * ℓ) else ↑k) * cutFactor k ℓ n (stepFragment n V) (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ t)

The factor at a closing cut: k on the empty branch and −2ℓ on the carried one.

theorem RS.EdgeSubset.sum_colours_snoc {k ℓ : ℕ} (h : MixedFunctional k ℓ) (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟 : DataFamily (stepFragment n V)) (s : Finset V.Flag) (C : ℕ) : ∑ x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (stepDataDown n V 𝒟) (diagOf (n + 1) x) s C = ∑ y : Fin n → Fin k ⊕ Fin (2 * ℓ), ∑ c : Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (stepDataDown n V 𝒟) (GenBoundaryState.extendPair (cutL n) (cutR n) (stageState n (diagOf n y)) c c) s C

A subset's colour sum, one cut at a time.

theorem RS.EdgeSubset.stageSum_open {k ℓ : ℕ} (h : MixedFunctional k ℓ) (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟 : DataFamily (stepFragment n V)) (hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n)) (C : ℕ) (w : Finset (stepFragment n V).Flag → ℂ) : ∑ s : Finset V.Flag, ∑ x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ), w (flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s)) * edgeTermAt h (stepDataDown n V 𝒟) (diagOf (n + 1) x) s (C + carried (n + 1) V s) = ∑ t : Finset (stepFragment n V).Flag, ∑ y : Fin n → Fin k ⊕ Fin (2 * ℓ), w t * edgeTermAt h 𝒟 (diagOf n y) t (C + carried n (stepFragment n V) t)

An open stage, summed against a weight on the composition's subsets.

theorem RS.EdgeSubset.stageSum_closed {k ℓ : ℕ} (h : MixedFunctional k ℓ) (n : ℕ) (V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0))) (𝒟 : DataFamily (stepFragment n V)) (hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n)) (C : ℕ) (w : Finset (stepFragment n V).Flag → ℂ) : ∑ s : Finset V.Flag, ∑ x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ), w (flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ (V.dropSubset (cutL n) (cutR n) s)) * edgeTermAt h (stepDataDown n V 𝒟) (diagOf (n + 1) x) s (C + carried (n + 1) V s) = (↑k - 2 * ↑ℓ) * ∑ t : Finset (stepFragment n V).Flag, ∑ y : Fin n → Fin k ⊕ Fin (2 * ℓ), w t * edgeTermAt h 𝒟 (diagOf n y) t (C + carried n (stepFragment n V) t)

A closing stage, summed against a weight on the composition's subsets.

theorem RS.EdgeSubset.edgeTermAt_glueInterface {k ℓ : ℕ} (h : MixedFunctional k ℓ) (n : ℕ) (V : Fragment (Fin (0 + n) ⊕ Fin (n + 0))) (𝒟 : DataFamily (glueInterface 0 n 0 V)) (C : ℕ) (w : Finset (glueInterface 0 n 0 V).Flag → ℂ) : (↑k - 2 * ↑ℓ) ^ closedCuts n V * ∑ s' : Finset (glueInterface 0 n 0 V).Flag, w s' * edgeTermAt h 𝒟 emptyState s' C = ∑ s : Finset V.Flag, ∑ x : Fin n → Fin k ⊕ Fin (2 * ℓ), w (imageOf n V s) * edgeTermAt h (pushData n V 𝒟) (diagOf n x) s (C + carried n V s)

The composition's summand, stage by stage. RS21's ∗ glues the whole interface at once; iterating the per-cut identity carries the composition's summand back to the two fragments, with the free circles' k − 2ℓ in front and the ledger's count on the base's side. The weight rides along on the composition's own subsets.