The single-pair gluing infrastructure

The infrastructure of the single-pair gluing analysis: the extended-state evaluation (extendPair_left, extendPair_right, extendPair_surviving), the glueAttach correspondence, the through-flag membership characterization, and the through-factor arithmetic (oddPartnerSign_sq, oddPartnerSign_cast_sq).

Why every cut in the development is ordered: the naive transposed-factor weighting is order-sensitive — the W-side through-product of a closed-off edge reads throughStateFactor (st (min i j)) (st (max i j)), so for i < j the ε pairs with its transpose and the odd block sums to −2ℓ (as required by the circle prefactor (k − 2ℓ)), while for j < i it pairs with itself and sums to +2ℓ; gluing a strand's two ends with i = 1, j = 0 gives k + 2ℓ instead of k − 2ℓ. All cuts in the development are therefore ordered.

Evaluation of the extended state

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

The extended state's value at the first glued label.

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

At the second glued label.

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

And at a surviving label, where it is the state extended.

The ledger sums

theorem RS.oddPartnerSign_sq (ℓ : ℕ) (c : Fin (2 * ℓ)) : ↑(oddPartnerSign ℓ c) * ↑(oddPartnerSign ℓ c) = 1

The square of the odd partner sign is one.

theorem RS.oddPartnerSign_cast_sq (ℓ : ℕ) (c : Fin (2 * ℓ)) : ↑(oddPartnerSign ℓ c) * ↑(oddPartnerSign ℓ c) = 1

The square of the odd partner sign is one, read through the integer cast.

The closed-case correspondence engine

theorem RS.EdgeSubset.mem_throughFlags_iff {β : Type} {V : Fragment β} {F : EdgeSubset V} {f : V.Flag} : f ∈ F.throughFlags ↔ f ∈ F.flags ∧ (∃ (i : β), V.attach f = Sum.inr i) ∧ ∃ (j : β), V.attach (V.pairing f) = Sum.inr j

Unfolded membership in the through-flags (stated generically to avoid reducibility friction at glued fragments).

List and membership helpers

theorem RS.EdgeSubset.perm_attachWith {γ : Type u_1} {p : γ → Prop} {l₁ l₂ : List γ} : l₁.Perm l₂ → ∀ (H₁ : ∀ x ∈ l₁, p x) (H₂ : ∀ x ∈ l₂, p x), (l₁.attachWith p H₁).Perm (l₂.attachWith p H₂)

attachWith respects permutations.

theorem RS.EdgeSubset.multiset_map_eq_of_bij {γ : Type u_1} {δ : Type u_2} {X : Type u_3} (s : Finset γ) (t : Finset δ) (e : δ → γ) (hinj : Function.Injective e) (hmem : ∀ (y : δ), y ∈ t ↔ e y ∈ s) (hsurj : ∀ x ∈ s, ∃ (y : δ), e y = x) (g : γ → X) (g' : δ → X) (hg : ∀ y ∈ t, g (e y) = g' y) : Multiset.map g s.val = Multiset.map g' t.val

Finset-supported multisets map equally along a bijection of their supports (stated without decidability data so that it applies by unification against glued-fragment goals).

The in-flag lists across the closed glue

theorem RS.EdgeSubset.relInFlagsAt_perm_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) (v : W.Vertex) : ({ flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.relInFlagsAt (unglueOrientationClosed hclosed b s' hc' hc κ' o') v).Perm (List.map Subtype.val ({ flags := s', pairing_mem := hc' }.relInFlagsAt o' v))

The lifted in-flag list is a permutation of the projected glued in-flag list.

theorem RS.EdgeSubset.mem_map_relInFlagsAt_internal {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) {v : W.Vertex} (f : W.Flag) : f ∈ List.map Subtype.val ({ flags := s', pairing_mem := hc' }.relInFlagsAt o' v) → f ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.internalFlags

Members of the projected glued in-flag list are internal in the lift.

Pointwise core data agreement

The list conversions

The vertex data transports

theorem RS.EdgeSubset.evenColoursAt_transport_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) {k : ℕ} (ψW : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.EvenColouring k) (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) (hψ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∉ Fragment.liftSubsetClosed s' b) (h2 : g ∉ s'), ↑ψW ⟨↑g, h1⟩ = ↑ψ' ⟨g, h2⟩) (v : W.Vertex) : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.evenColoursAt ψW v = { flags := s', pairing_mem := hc' }.evenColoursAt ψ' v

The even colour multiset agrees across the closed glue.

theorem RS.EdgeSubset.coreOddSignAt_transport_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) {ℓ : ℕ} (φW : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.CoreOddColouring ℓ) (φ' : { flags := s', pairing_mem := hc' }.CoreOddColouring ℓ) (hφ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.coreFlags) (h2 : g ∈ { flags := s', pairing_mem := hc' }.coreFlags), ↑φW ⟨↑g, h1⟩ = ↑φ' ⟨g, h2⟩) (v : W.Vertex) : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.coreOddSignAt (unglueOrientationClosed hclosed b s' hc' hc κ' o') φW v = { flags := s', pairing_mem := hc' }.coreOddSignAt o' φ' v

The core odd sign at a vertex agrees across the closed glue.

theorem RS.EdgeSubset.evalOdd_coreOddListAt_transport_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (φW : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.CoreOddColouring ℓ) (φ' : { flags := s', pairing_mem := hc' }.CoreOddColouring ℓ) (hφ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.coreFlags) (h2 : g ∈ { flags := s', pairing_mem := hc' }.coreFlags), ↑φW ⟨↑g, h1⟩ = ↑φ' ⟨g, h2⟩) (μ : Multiset (Fin k)) (v : W.Vertex) : h.evalOdd μ ({ flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.coreOddListAt (unglueOrientationClosed hclosed b s' hc' hc κ' o') φW v) = h.evalOdd μ ({ flags := s', pairing_mem := hc' }.coreOddListAt o' φ' v)

The evaluated core odd list at a vertex agrees across the closed glue.

Boundary-match transports

theorem RS.EdgeSubset.vertexFactor_transport_closed {α : Type} {W : Fragment α} {i j : α} (hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j) (s' : Finset (W.SurvivingFlag i j)) (b : Bool) (hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s') (hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b) (κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem) (o' : κ'.Orientation) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (ψW : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.EvenColouring k) (ψ' : { flags := s', pairing_mem := hc' }.EvenColouring k) (hψ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∉ Fragment.liftSubsetClosed s' b) (h2 : g ∉ s'), ↑ψW ⟨↑g, h1⟩ = ↑ψ' ⟨g, h2⟩) (φW : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.CoreOddColouring ℓ) (φ' : { flags := s', pairing_mem := hc' }.CoreOddColouring ℓ) (hφ : ∀ (g : W.SurvivingFlag i j) (h1 : ↑g ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.coreFlags) (h2 : g ∈ { flags := s', pairing_mem := hc' }.coreFlags), ↑φW ⟨↑g, h1⟩ = ↑φ' ⟨g, h2⟩) (v : W.Vertex) : ↑({ flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.coreOddSignAt (unglueOrientationClosed hclosed b s' hc' hc κ' o') φW v) * h.evalOdd ({ flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.evenColoursAt ψW v) ({ flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.coreOddListAt (unglueOrientationClosed hclosed b s' hc' hc κ' o') φW v) = ↑({ flags := s', pairing_mem := hc' }.coreOddSignAt o' φ' v) * h.evalOdd ({ flags := s', pairing_mem := hc' }.evenColoursAt ψ' v) ({ flags := s', pairing_mem := hc' }.coreOddListAt o' φ' v)

The vertex factor transport across the closed glue.