The pair family and the base sum #
A choice of pair datum (ConversePair.lean) at every subset of the
composition's base: the family pairFamily, its behaviour under
the interface glue, and the sum of the composition's own terms over
the base. The sum is read with the bits each subset itself
determines, and base_sum_eq_superForm_pairing_bitsOf writes it as
the super form pairing of the two fragments' tensors — the tensor
side of the Gram identity.
@[reducible]
The lexicographic order on the interface's label type.
Equations
- RS.EdgeSubset.famBaseOrder n = RS.sumLexLinearOrder (Fin (0 + n)) (Fin (n + 0))
Instances For
@[reducible]
The same order one stage up.
Equations
- RS.EdgeSubset.famOrderSucc n = RS.sumLexLinearOrder (Fin (0 + n + 1)) (Fin (n + 1 + 0))
Instances For
@[reducible]
The order a stage's surviving labels carry.
Equations
Instances For
@[reducible]
The order the composition's own label type carries.
Equations
Instances For
theorem
RS.EdgeSubset.exists_pairDatum_total
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
(hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian)
(hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian)
(hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData)
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂)
(hb :
∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
:
∃ (κ : { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.RelTransitionSystem) (O : κ.Orientation),
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = (-1) ^ (glueData t (closeBase F G)
(pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst)).rel.openCircuitCount * ∑ x : GenBoundaryState k ℓ (Fin t),
edgeTermOf h ⟨κ, O⟩ (diagOf t x)
(glueCount t (closeBase F G)
(pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst)) ∧ (∀ (ℓ' : Fin (0 + t) ⊕ Fin (t + 0)),
O.isOut ((closeBase F G).pairing ((closeBase F G).boundaryFlag ℓ')) = !O.isOut ((closeBase F G).boundaryFlag ℓ')) ∧ (∀ (m : Fin t),
O.isOut ((closeBase F G).boundaryFlag (intR t m)) = !O.isOut ((closeBase F G).boundaryFlag (intL t m))) ∧ κ.MatchEq (pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst).rel
The pair datum, against the total summand. RS21's (13) and (14) in the form the composition's sum needs: no state-matching hypothesis, the mismatched states contributing nothing on both sides.
theorem
RS.EdgeSubset.exists_pairDatum_ofEq
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
(hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian)
(hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian)
(hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData)
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂)
(hb :
∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(u : Finset (closeBase F G).Flag)
(hc : ∀ f ∈ u, (closeBase F G).pairing f ∈ u)
(hu : { flags := u, pairing_mem := hc } = { flags := closeJoin s₁ s₂, pairing_mem := ⋯ })
:
∃ (κ : { flags := u, pairing_mem := hc }.RelTransitionSystem) (O : κ.Orientation),
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = (-1) ^ (glueData t (closeBase F G)
(pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst)).rel.openCircuitCount * ∑ x : GenBoundaryState k ℓ (Fin t),
edgeTermOf h ⟨κ, O⟩ (diagOf t x)
(glueCount t (closeBase F G)
(pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst)) ∧ (∀ (ℓ' : Fin (0 + t) ⊕ Fin (t + 0)),
O.isOut ((closeBase F G).pairing ((closeBase F G).boundaryFlag ℓ')) = !O.isOut ((closeBase F G).boundaryFlag ℓ')) ∧ (∀ (m : Fin t),
O.isOut ((closeBase F G).boundaryFlag (intR t m)) = !O.isOut ((closeBase F G).boundaryFlag (intL t m))) ∧ κ.MatchEq (relOfEq ⋯ (pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst).rel)
The pair datum, read at an equal subset. Everything the datum says transports along an equality of subsets.
theorem
RS.EdgeSubset.cutBalanced_closeJoin
{t : ℕ}
{F G : Fragment (Fin t)}
{s₁ : Finset F.Flag}
{s₂ : Finset G.Flag}
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂)
:
CutBalanced (closeBase F G) (closeJoin s₁ s₂)
Matching used labels make the join balanced.
theorem
RS.EdgeSubset.exists_pairDatum_sigma_full
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(u : Finset (closeBase F G).Flag)
(hc : ∀ f ∈ u, (closeBase F G).pairing f ∈ u)
(hE : { flags := u, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := u, pairing_mem := hc }.CanonData)
:
∃ (d : (κ : { flags := u, pairing_mem := hc }.RelTransitionSystem) × κ.Orientation),
(CutBalanced (closeBase F G) u →
(∀ (ℓ' : Fin (0 + t) ⊕ Fin (t + 0)),
d.snd.isOut ((closeBase F G).pairing ((closeBase F G).boundaryFlag ℓ')) = !d.snd.isOut ((closeBase F G).boundaryFlag ℓ')) ∧ ∀ (m : Fin t),
d.snd.isOut ((closeBase F G).boundaryFlag (intR t m)) = !d.snd.isOut ((closeBase F G).boundaryFlag (intL t m))) ∧ ∀ (s₁ : Finset F.Flag) (hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁),
{ flags := s₁, pairing_mem := hc₁ }.Eulerian →
∀ (hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData) (s₂ : Finset G.Flag)
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂),
{ flags := s₂, pairing_mem := hc₂ }.Eulerian →
∀ (hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData)
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂),
(∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags) →
∀ (hu : { flags := u, pairing_mem := hc } = { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }),
d.fst.MatchEq
(relOfEq ⋯ (pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst).rel) ∧ ∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t),
superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = (-1) ^ (glueData t (closeBase F G)
(pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst
(Classical.choice hn₂).fst)).rel.openCircuitCount * ∑ x : GenBoundaryState k ℓ (Fin t),
edgeTermOf h d (diagOf t x)
(glueCount t (closeBase F G)
(pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst))
A datum at every subset, carrying both the directions and, at a join of compatible halves, RS21's value.
noncomputable def
RS.EdgeSubset.pairFamily
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
:
DataFamily (closeBase F G)
The pair family. At every balanced subset of the base it carries the directions the lift asks for.
Equations
- RS.EdgeSubset.pairFamily h t F G u hc hE hne = Classical.choose ⋯
Instances For
theorem
RS.EdgeSubset.baseDirections_pairFamily
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
:
BaseDirections (closeBase F G) (pairFamily h t F G)
The pair family has the base's directions.
theorem
RS.EdgeSubset.pairFamily_matchEq
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(u : Finset (closeBase F G).Flag)
(hc : ∀ f ∈ u, (closeBase F G).pairing f ∈ u)
(hE : { flags := u, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := u, pairing_mem := hc }.CanonData)
(s₁ : Finset F.Flag)
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
(hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian)
(hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData)
(s₂ : Finset G.Flag)
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian)
(hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData)
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂)
(hb :
∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(hu : { flags := u, pairing_mem := hc } = { flags := closeJoin s₁ s₂, pairing_mem := ⋯ })
:
(pairFamily h t F G u hc hE hne).fst.MatchEq
(relOfEq ⋯ (pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst).rel)
The pair family's system is the pair stage's. The two agree on the partner map, which is what the circuit count sees.
theorem
RS.EdgeSubset.pairFamily_value
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(u : Finset (closeBase F G).Flag)
(hc : ∀ f ∈ u, (closeBase F G).pairing f ∈ u)
(hE : { flags := u, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := u, pairing_mem := hc }.CanonData)
(s₁ : Finset F.Flag)
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
(hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian)
(hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData)
(s₂ : Finset G.Flag)
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian)
(hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData)
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂)
(hb :
∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(hu : { flags := u, pairing_mem := hc } = { flags := closeJoin s₁ s₂, pairing_mem := ⋯ })
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = (-1) ^ (glueData t (closeBase F G)
(pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst)).rel.openCircuitCount * ∑ x : GenBoundaryState k ℓ (Fin t),
edgeTermOf h (pairFamily h t F G u hc hE hne) (diagOf t x)
(glueCount t (closeBase F G) (pairStage hc₁ hc₂ hused (Classical.choice hn₁).fst (Classical.choice hn₂).fst))
The pair family computes RS21's pair term. At a join of compatible halves, the family's own datum is the one (13) and (14) speak of.
theorem
RS.EdgeSubset.baseDirections_stepDataUp
(n : ℕ)
(V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)))
(hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n))
(b : Bool)
(𝒟 : DataFamily V)
(hbd : BaseDirections V 𝒟)
:
BaseDirections (stepFragment n V) (stepDataUp n V b 𝒟)
The base's directions survive a stage of the lift. Both halves of the invariant come back at the stage: the glue neither moves a direction nor breaks a flip.
theorem
RS.EdgeSubset.baseDirections_stepDataUp_closed
(n : ℕ)
(V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)))
(hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n))
(b : Bool)
(𝒟 : DataFamily V)
(hbd : BaseDirections V 𝒟)
:
BaseDirections (stepFragment n V) (stepDataUp n V b 𝒟)
The base's directions survive a closing glue. A closing cut rewires nothing, so the stage's family reads its boundary flags and their partners exactly as the base family reads the lift's — and the lift of a balanced subset is balanced.
def
RS.EdgeSubset.Aligned
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
:
(Fin n → Bool) → DataFamily V → Prop
The family alternates at every cut of the interface. RS21's step 1, as a condition on the family the lift consumes: at every stage the data give the cut's two flags opposite directions, which is what an open cut needs to glue its two arcs into one.
Equations
- One or more equations did not get rendered due to their size.
- RS.EdgeSubset.Aligned 0 x_4 x_5 x_6 = True
Instances For
noncomputable def
RS.EdgeSubset.bitsOf
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(_s : Finset V.Flag)
:
The bits a subset determines. At each stage the bit records whether the subset carries the cut's own edge; the deeper stages read the dropped subset.
Equations
- RS.EdgeSubset.bitsOf 0 x_3 x_4 = fun (i : Fin 0) => i.elim0
- RS.EdgeSubset.bitsOf n.succ V s = Fin.snoc (RS.EdgeSubset.bitsOf n (RS.EdgeSubset.stepFragment n V) (RS.EdgeSubset.stageSubset n V s)) (decide (V.boundaryFlag (RS.EdgeSubset.cutL n) ∈ s))
Instances For
theorem
RS.EdgeSubset.cutBalanced_stageSubset
(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)
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(hbal : CutBalanced V s)
:
CutBalanced (stepFragment n V) (stageSubset n V s)
A balanced subset's drop is balanced.
theorem
RS.EdgeSubset.stageSubset_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)
:
stageSubset n V s = flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯
(V.dropSubset (cutL n) (cutR n) s)
The stage subset, at a closing cut.
theorem
RS.EdgeSubset.stageSubset_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)
:
stageSubset n V s = flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯
(V.dropSubset (cutL n) (cutR n) s)
The stage subset, at an open cut.
theorem
RS.EdgeSubset.aligned_of_baseDirections
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(bits : Fin n → Bool)
(𝒟 : DataFamily V)
:
BaseDirections V 𝒟 → Aligned n V bits 𝒟
The base's directions give the alignment at every stage. With no closing cut, a family whose directions flip at the boundary flags and alternate at every interface pair is aligned all the way down the interface.
theorem
RS.EdgeSubset.dropSubset_matches_of_matches_closed
{k ℓ : ℕ}
(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)
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ))
(hm : genBoundarySubsetMatches V s (diagOf (n + 1) x))
:
genBoundarySubsetMatches (V.gluePairClosed (cutL n) (cutR n) hcl) (V.dropSubset (cutL n) (cutR n) s)
(stageState n (diagOf n fun (a : Fin n) => x a.castSucc))
The drop carries the stage's state, at a closing cut.
theorem
RS.EdgeSubset.stage_matches_of_matches_closed
{k ℓ : ℕ}
(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)
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(x : Fin (n + 1) → Fin k ⊕ Fin (2 * ℓ))
(hm : genBoundarySubsetMatches V s (diagOf (n + 1) x))
:
genBoundarySubsetMatches (stepFragment n V)
(flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯
(V.dropSubset (cutL n) (cutR n) s))
(diagOf n fun (a : Fin n) => x a.castSucc)
The stage carries the stage's state, at a closing cut.
theorem
RS.EdgeSubset.match_pushData_liftData_bitsOf
{k ℓ : ℕ}
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(x : Fin n → Fin k ⊕ Fin (2 * ℓ))
(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)
:
The interface round trip at one subset, with the subset's own bits. A closing cut's lift needs a bit, and the bit the subset itself determines is the one that returns it; the open cuts need the alignment, as before.
theorem
RS.EdgeSubset.isOut_pushData_liftData_succ_closed_at
(n : ℕ)
(V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)))
(hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n))
(bits : Fin (n + 1) → Bool)
(𝒟 : 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)
(hbit : bits (Fin.last n) = decide (V.boundaryFlag (cutL n) ∈ s))
(hIH :
∀ (t : Finset (stepFragment n V).Flag),
t = flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯
(V.dropSubset (cutL n) (cutR n) s) →
∀ (hct : ∀ f ∈ t, (stepFragment n V).pairing f ∈ t) (hEt : { flags := t, pairing_mem := hct }.Eulerian)
(hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData) (g : (stepFragment n V).Flag),
(∀ (b : Fin (0 + n) ⊕ Fin (n + 0)), g ≠ (stepFragment n V).boundaryFlag b) →
(pushData n (stepFragment n V)
(liftData n (stepFragment n V) (fun (a : Fin n) => bits a.castSucc)
(stepDataUp n V (bits (Fin.last n)) 𝒟))
t hct hEt hnet).snd.isOut
g = (stepDataUp n V (bits (Fin.last n)) 𝒟 t hct hEt hnet).snd.isOut g)
(hcL :
∀ f ∈ Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s)),
V.pairing f ∈ Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s)))
(hEL :
{ flags := Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s)),
pairing_mem := hcL }.Eulerian)
(hneL :
Nonempty
{ flags := Fragment.liftSubsetClosed (V.dropSubset (cutL n) (cutR n) s) (decide (V.boundaryFlag (cutL n) ∈ s)),
pairing_mem := hcL }.CanonData)
(f : V.Flag)
(hfb : ∀ (a : Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)), f ≠ V.boundaryFlag a)
:
The round trip on directions, one stage on, at a closing cut, at one subset.
theorem
RS.EdgeSubset.isOut_pushData_liftData_bitsOf
{k ℓ : ℕ}
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(x : Fin n → Fin k ⊕ Fin (2 * ℓ))
(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)
:
The round trip on directions at one subset, with the subset's own bits.
theorem
RS.EdgeSubset.cutBalanced_stageSubset_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)
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(hbal : CutBalanced V s)
:
CutBalanced (stepFragment n V) (stageSubset n V s)
A balanced subset's drop is balanced, at a closing cut.
theorem
RS.EdgeSubset.edgeTermAt_pushData_colourSum
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒢 : DataFamily (glueInterface 0 n 0 V))
(s : Finset V.Flag)
:
(∀ f ∈ s, V.pairing f ∈ s) →
CutBalanced V s →
∀ (C : ℕ),
∑ x : Fin n → Fin k ⊕ Fin (2 * ℓ), edgeTermAt h (pushData n V 𝒢) (diagOf n x) s (C + carried n V s) = cutFactor k ℓ n V s * edgeTermAt h 𝒢 emptyState (imageOf n V s) C
A base subset's whole colour sum is the composition's own term. Summed over the interface colourings, a guarded balanced subset's summand is the composition's term at the subset's image, times the free circles the subset's own closing cuts contribute. Nothing is asked of the family: the identification is stage by stage, an open cut summing its colour away and a closing one splitting into the free circle's two sectors.
def
RS.EdgeSubset.BaseSumBitsOf
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(C : ℕ)
:
The base sum with the subset's own bits — the statement the closing cut needs. The composition's own sum is family-free, so the left side may be read at any fixed bits; the right side reads each base subset with the bits that subset itself determines, which is what the round trip asks for.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
RS.EdgeSubset.summandSum_bits_indep
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(s : Finset V.Flag)
(C : ℕ)
(bits bits' : Fin n → Bool)
:
∑ x : Fin n → Fin k ⊕ Fin (2 * ℓ),
circuitWeight (liftData n V bits 𝒟) (imageOf n V s) * edgeTermAt h (pushData n V (liftData n V bits 𝒟)) (diagOf n x) s (C + carried n V s) = ∑ x : Fin n → Fin k ⊕ Fin (2 * ℓ),
circuitWeight (liftData n V bits' 𝒟) (imageOf n V s) * edgeTermAt h (pushData n V (liftData n V bits' 𝒟)) (diagOf n x) s (C + carried n V s)
THE SUMMAND DOES NOT READ THE LIFT'S BITS. Summed over the interface colourings, a base subset's weighted summand is the free circles its own closing cuts contribute, times the composition's own weighted term at its image — and that product is family-free at the closed top. So which lift computed it makes no difference.
theorem
RS.EdgeSubset.baseSumBitsOf_all
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(C : ℕ)
:
BaseSumBitsOf h n V 𝒟 C
THE BASE SUM, WITH EACH SUBSET'S OWN BITS. The composition's own total is the sum over the base's subsets of the summand each subset's own bits compute — because the summand does not read the bits at all.
theorem
RS.EdgeSubset.edgeTermAt_pushData_liftData_bitsOf
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(x : Fin n → Fin k ⊕ Fin (2 * ℓ))
{s : Finset V.Flag}
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(hbnd : genBoundarySubsetMatches V s (diagOf n x))
(hE : { flags := s, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := s, pairing_mem := hc }.CanonData)
(hal : Aligned n V (bitsOf n V s) 𝒟)
(C : ℕ)
:
edgeTermAt h (pushData n V (liftData n V (bitsOf n V s) 𝒟)) (diagOf n x) s C = edgeTermAt h 𝒟 (diagOf n x) s C
The pushed lift computes the family's own term, with the subset's own bits — at a closing cut as much as an open one.
theorem
RS.EdgeSubset.edgeTermAt_pushData_liftData_all_bitsOf
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(hal : ∀ (s : Finset V.Flag), Aligned n V (bitsOf n V s) 𝒟)
(x : Fin n → Fin k ⊕ Fin (2 * ℓ))
(s : Finset V.Flag)
(C : ℕ)
:
edgeTermAt h (pushData n V (liftData n V (bitsOf n V s) 𝒟)) (diagOf n x) s C = edgeTermAt h 𝒟 (diagOf n x) s C
The pushed lift computes the family's own term, at every subset, with the subset's own bits. Off the matching subsets both terms vanish, and elsewhere the round trip at the subset's own bits returns the family — at a closing cut as much as an open one.
theorem
RS.EdgeSubset.match_liftData_glueData_bitsOf
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(D : StageData n V)
:
Aligned n V (bitsOf n V D.sub.flags) 𝒟 →
(∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData),
(𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel) →
CutBalanced V D.sub.flags →
∀ (hc : ∀ f ∈ (glueData n V D).sub.flags, (glueInterface 0 n 0 V).pairing f ∈ (glueData n V D).sub.flags)
(hE : { flags := (glueData n V D).sub.flags, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := (glueData n V D).sub.flags, pairing_mem := hc }.CanonData),
(liftData n V (bitsOf n V D.sub.flags) 𝒟 (glueData n V D).sub.flags hc hE hne).fst.MatchEq (glueData n V D).rel
The lift is the ledger, at every interface. Read with the bits the ledger's own subset determines, the lifted family's system at the glued subset is the ledger's glued system, up to its partner map — at a closing cut as much as an open one, because the bit the subset determines is the bit the ledger's step uses.
theorem
RS.EdgeSubset.circuitWeight_liftData_imageOf_bitsOf
(n : ℕ)
(V : Fragment (Fin (0 + n) ⊕ Fin (n + 0)))
(𝒟 : DataFamily V)
(D : StageData n V)
(hal : Aligned n V (bitsOf n V D.sub.flags) 𝒟)
(hcompat :
∀ (hc : ∀ f ∈ D.sub.flags, V.pairing f ∈ D.sub.flags) (hE : { flags := D.sub.flags, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := D.sub.flags, pairing_mem := hc }.CanonData), (𝒟 D.sub.flags hc hE hne).fst.MatchEq D.rel)
(hbal : CutBalanced V D.sub.flags)
(hE : { flags := (glueData n V D).sub.flags, pairing_mem := ⋯ }.Eulerian)
(hne : Nonempty { flags := (glueData n V D).sub.flags, pairing_mem := ⋯ }.CanonData)
:
The composition's weight is the ledger's sign, at every interface. Read with the bits the ledger's own subset determines, the weight the composition's sum carries at the image of a base subset is exactly the circuit sign the ledger records for it.
theorem
RS.EdgeSubset.tensorTermAt_eq_zero_of_not_matches
{α : Type}
[LinearOrder α]
[Fintype α]
(V : Fragment α)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(s : Finset V.Flag)
(x : GenBoundaryState k ℓ α)
(hx : ¬genBoundarySubsetMatches V s x)
:
A term of the fragment tensor needs its own labels.
theorem
RS.EdgeSubset.tensorTermAt_eq_zero_of_not_closed
{α : Type}
[LinearOrder α]
[Fintype α]
(V : Fragment α)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(s : Finset V.Flag)
(x : GenBoundaryState k ℓ α)
(hc : ¬∀ f ∈ s, V.pairing f ∈ s)
:
An unclosed subset carries no tensor term.
theorem
RS.EdgeSubset.tensorTermAt_eq_zero_of_not_eulerian
{α : Type}
[LinearOrder α]
[Fintype α]
(V : Fragment α)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
{s : Finset V.Flag}
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(x : GenBoundaryState k ℓ α)
(hE : ¬{ flags := s, pairing_mem := hc }.Eulerian)
:
A non-Eulerian subset carries no tensor term.
theorem
RS.EdgeSubset.tensorTermAt_eq_zero_of_not_canon
{α : Type}
[LinearOrder α]
[Fintype α]
(V : Fragment α)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
{s : Finset V.Flag}
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(hE : { flags := s, pairing_mem := hc }.Eulerian)
(x : GenBoundaryState k ℓ α)
(hne : ¬Nonempty { flags := s, pairing_mem := hc }.CanonData)
:
A subset with no canonical data carries no tensor term.
theorem
RS.EdgeSubset.pairTerm_eq_zero_of_used_ne
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(s₁ : Finset F.Flag)
(s₂ : Finset G.Flag)
(i : Fin t)
(h₁ : F.boundaryFlag i ∈ s₁)
(h₂ : G.boundaryFlag i ∉ s₂)
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = 0
Tensors of subsets using different labels are orthogonal.
theorem
RS.EdgeSubset.eulerian_closeJoin
{t : ℕ}
{F G : Fragment (Fin t)}
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian)
(hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian)
:
The join is Eulerian when its halves are.
theorem
RS.EdgeSubset.canonData_closeJoin
{t : ℕ}
{F G : Fragment (Fin t)}
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂)
(hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData)
(hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData)
:
The join carries canonical data when its halves do.
theorem
RS.EdgeSubset.not_eulerian_closeJoin
{t : ℕ}
{F G : Fragment (Fin t)}
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hbad : ¬({ flags := s₁, pairing_mem := hc₁ }.Eulerian ∧ { flags := s₂, pairing_mem := hc₂ }.Eulerian))
:
A non-Eulerian half leaves the join non-Eulerian.
theorem
RS.EdgeSubset.base_term_eq_zero_of_not_matches
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(bits : Fin t → Bool)
(s : Finset (closeBase F G).Flag)
(C : ℕ)
(hbad : ∀ (x : GenBoundaryState k ℓ (Fin t)), ¬genBoundarySubsetMatches (closeBase F G) s (diagOf t x))
:
∑ x : GenBoundaryState k ℓ (Fin t),
circuitWeight (liftData t (closeBase F G) bits (pairFamily h t F G)) (imageOf t (closeBase F G) s) * edgeTermAt h (pairFamily h t F G) (diagOf t x) s C = 0
The base's summand vanishes off a matching subset.
theorem
RS.EdgeSubset.not_matches_of_used_ne
{k ℓ t : ℕ}
{F G : Fragment (Fin t)}
{s₁ : Finset F.Flag}
{s₂ : Finset G.Flag}
(i : Fin t)
(hne : ¬(F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂))
(x : GenBoundaryState k ℓ (Fin t))
:
¬genBoundarySubsetMatches (closeBase F G) (closeJoin s₁ s₂) (diagOf t x)
A mismatched join carries no diagonal state.
theorem
RS.EdgeSubset.pairTerm_eq_zero_of_not_closed_left
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(s₁ : Finset F.Flag)
(s₂ : Finset G.Flag)
(hc₁ : ¬∀ f ∈ s₁, F.pairing f ∈ s₁)
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = 0
A tensor term needs a closed subset.
theorem
RS.EdgeSubset.pairTerm_eq_zero_of_not_closed_right
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(s₁ : Finset F.Flag)
(s₂ : Finset G.Flag)
(hc₂ : ¬∀ f ∈ s₂, G.pairing f ∈ s₂)
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = 0
A tensor term needs a closed subset, on the right.
theorem
RS.EdgeSubset.pairTerm_eq_zero_of_not_eulerian
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hbad : ¬({ flags := s₁, pairing_mem := hc₁ }.Eulerian ∧ { flags := s₂, pairing_mem := hc₂ }.Eulerian))
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = 0
A tensor term needs an Eulerian subset.
theorem
RS.EdgeSubset.pairTerm_eq_zero_of_not_canon
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian)
(hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian)
(hbad :
¬(Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData ∧ Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData))
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = 0
A tensor term needs canonical data.
theorem
RS.EdgeSubset.base_term_eq_zero_of_not_guarded
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(bits : Fin t → Bool)
(s : Finset (closeBase F G).Flag)
(C : ℕ)
(hbad :
¬∃ (hc : ∀ f ∈ s, (closeBase F G).pairing f ∈ s),
{ flags := s, pairing_mem := hc }.Eulerian ∧ Nonempty { flags := s, pairing_mem := hc }.CanonData)
:
∑ x : GenBoundaryState k ℓ (Fin t),
circuitWeight (liftData t (closeBase F G) bits (pairFamily h t F G)) (imageOf t (closeBase F G) s) * edgeTermAt h (pairFamily h t F G) (diagOf t x) s C = 0
The base's summand vanishes at an unguarded subset.
theorem
RS.EdgeSubset.sum_pairs_regroup
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
:
∑ s₁ : Finset F.Flag,
∑ s₂ : Finset G.Flag,
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = ∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t),
(superForm t x y * ∑ s₁ : Finset F.Flag, tensorTermAt F h s₁ x) * ∑ s₂ : Finset G.Flag, tensorTermAt G h s₂ y
The pair sums regroup. Summing the pair terms over all subsets of the two fragments is the superform pairing of the two fragments' vectors.
theorem
RS.EdgeSubset.base_term_eq_pairTerm_bitsOf
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
(hE₁ : { flags := s₁, pairing_mem := hc₁ }.Eulerian)
(hn₁ : Nonempty { flags := s₁, pairing_mem := hc₁ }.CanonData)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(hE₂ : { flags := s₂, pairing_mem := hc₂ }.Eulerian)
(hn₂ : Nonempty { flags := s₂, pairing_mem := hc₂ }.CanonData)
(hused : ∀ (i : Fin t), F.boundaryFlag i ∈ s₁ ↔ G.boundaryFlag i ∈ s₂)
(hb :
∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(hEJ : { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.Eulerian)
(hneJ : Nonempty { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.CanonData)
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = ∑ x : GenBoundaryState k ℓ (Fin t),
circuitWeight (liftData t (closeBase F G) (bitsOf t (closeBase F G) (closeJoin s₁ s₂)) (pairFamily h t F G))
(imageOf t (closeBase F G) (closeJoin s₁ s₂)) * edgeTermAt h (pairFamily h t F G) (diagOf t x) (closeJoin s₁ s₂) (carried t (closeBase F G) (closeJoin s₁ s₂))
At a good pair of subsets the composition's own term is the pair's term: RS21's (13) and (14) at one subset of the base.
theorem
RS.EdgeSubset.base_term_eq_pairTerm_all_bitsOf
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
(s₁ : Finset F.Flag)
(s₂ : Finset G.Flag)
:
∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t), superForm t x y * tensorTermAt F h s₁ x * tensorTermAt G h s₂ y = ∑ x : GenBoundaryState k ℓ (Fin t),
circuitWeight (liftData t (closeBase F G) (bitsOf t (closeBase F G) (closeJoin s₁ s₂)) (pairFamily h t F G))
(imageOf t (closeBase F G) (closeJoin s₁ s₂)) * edgeTermAt h (pairFamily h t F G) (diagOf t x) (closeJoin s₁ s₂) (carried t (closeBase F G) (closeJoin s₁ s₂))
Summed over all boundary states, the form-weighted product of the two fragments' terms is the composition's base sum — the identity the converse runs on.
theorem
RS.EdgeSubset.base_sum_eq_superForm_pairing_bitsOf
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(t : ℕ)
(F G : Fragment (Fin t))
:
∑ s : Finset (closeBase F G).Flag,
∑ x : GenBoundaryState k ℓ (Fin t),
circuitWeight (liftData t (closeBase F G) (bitsOf t (closeBase F G) s) (pairFamily h t F G))
(imageOf t (closeBase F G) s) * edgeTermAt h (pairFamily h t F G) (diagOf t x) s (carried t (closeBase F G) s) = ∑ x : GenBoundaryState k ℓ (Fin t),
∑ y : GenBoundaryState k ℓ (Fin t),
(superForm t x y * ∑ s₁ : Finset F.Flag, tensorTermAt F h s₁ x) * ∑ s₂ : Finset G.Flag, tensorTermAt G h s₂ y
The composition's base sum is the superform pairing, at every interface. Summing each base subset's term — read with the bits that subset itself determines — over all subsets gives RS21's pairing of the two fragments' tensors.