Subset sums split across a single cut

A weight that vanishes off the pairing-closed subsets sums the same over all subsets of W as over the lifts of the subsets of the glued fragment. At a closed cut the lifts are indexed by a Bool — whether the cut edge is taken — and at an open cut there is one lift per glued subset.

This is the reindexing half of a one-cut descent: it says that summing over W's subsets is summing over the glued fragment's subsets and the cut's own data, with nothing left over. Both halves are the round trips of GlueSubsetBij: dropSubset recovers the glued subset, liftSubsetClosed/liftSubsetOpen recover the original, and a pairing-closed subset is always a lift.

The cut's two ends

theorem RS.Fragment.extendPair_left {k ℓ : ℕ} {α : Type} (i j : α) (st : GenBoundaryState k ℓ (SurvivingLabel α i j)) (c c' : Fin k ⊕ Fin (2 * ℓ)) : GenBoundaryState.extendPair i j st c c' i = c

The extension takes the prescribed value at the first cut label.

theorem RS.Fragment.extendPair_right {k ℓ : ℕ} {α : Type} {i j : α} (hij : i ≠ j) (st : GenBoundaryState k ℓ (SurvivingLabel α i j)) (c c' : Fin k ⊕ Fin (2 * ℓ)) : GenBoundaryState.extendPair i j st c c' j = c'

And at the second, when the two are distinct.

theorem RS.Fragment.extendPair_surviving {k ℓ : ℕ} {α : Type} (i j : α) (st : GenBoundaryState k ℓ (SurvivingLabel α i j)) (c c' : Fin k ⊕ Fin (2 * ℓ)) (x : SurvivingLabel α i j) : GenBoundaryState.extendPair i j st c c' ↑x = st x

And the restriction elsewhere.

The closed cut

theorem RS.Fragment.liftSubsetClosed_injective {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) : Function.Injective fun (p : Finset (W.SurvivingFlag i j) × Bool) => liftSubsetClosed p.1 p.2

At a closed cut the two lifts of distinct glued subsets are distinct, and a lift determines which of the two it is.

theorem RS.Fragment.sum_split_closed {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (X : Finset W.Flag → ℂ) (hz : ∀ (sb : Finset W.Flag), (¬∀ f ∈ sb, W.pairing f ∈ sb) → X sb = 0) : ∑ sb : Finset W.Flag, X sb = ∑ s' : Finset (W.SurvivingFlag i j), ∑ b : Bool, X (liftSubsetClosed s' b)

The subset sum splits at a closed cut. A weight vanishing off the pairing-closed subsets sums over all subsets of W exactly as it sums over the glued subsets and the two lifts.

The open cut

theorem RS.Fragment.liftSubsetOpen_injective {α : Type} {W : Fragment α} {i j : α} (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) : Function.Injective fun (s' : Finset (W.SurvivingFlag i j)) => liftSubsetOpen hopen s'

At an open cut distinct glued subsets have distinct lifts.

theorem RS.Fragment.sum_split_open {α : Type} {W : Fragment α} {i j : α} (hij : i ≠ j) (hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j) (X : Finset W.Flag → ℂ) (hz : ∀ (sb : Finset W.Flag), (¬∀ f ∈ sb, W.pairing f ∈ sb) → X sb = 0) : ∑ sb : Finset W.Flag, X sb = ∑ s' : Finset (W.SurvivingFlag i j), X (liftSubsetOpen hopen s')

The subset sum splits at an open cut.