The glue ledger at a cut the subset misses #
RS21's bookkeeping (14) compares the circuit count of the composed graph with the two fragments' counts and the number of components of the union of their matchings. In the flag model the composition is built one interface pair at a time, and each step moves those quantities together: the circuit count and the number of components of the union.
GlueChord carries that ledger across a glue whose edge the subset
uses. This file carries it across the glues the subset misses —
where the interface edge is not in the subset, and where a closed cut
is left out of it. There nothing moves at all: the used labels are
the same on both sides, the chord matching is unchanged, and so is
the circuit count.
The ledger reads only the matching #
Both quantities the ledger tracks — the circuit count and the chord matching's pairing — are read off the transition system's matching alone, so two systems that match alike carry the same ledger. That is what lets the ledger be stated in whichever direction a glue happens to construct its system.
theorem
RS.EdgeSubset.chordInv_congr_matchEq
{α : Type}
{W : Fragment α}
{F : EdgeSubset W}
{κ₁ κ₂ : F.RelTransitionSystem}
(h : κ₁.MatchEq κ₂)
(a : α)
:
The chord matching reads only the matching.
theorem
RS.EdgeSubset.cutMatching_congr_matchEq
{α : Type}
{W : Fragment α}
{F : EdgeSubset W}
[LinearOrder α]
{κ₁ κ₂ : F.RelTransitionSystem}
(h : κ₁.MatchEq κ₂)
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
:
The cut matching's pairing reads only the matching.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_congr_matchEq
{α : Type}
{W : Fragment α}
{F : EdgeSubset W}
[LinearOrder α]
[Fintype α]
{κ₁ κ₂ : F.RelTransitionSystem}
(h : κ₁.MatchEq κ₂)
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
(N : DirMatching { a : α // W.boundaryFlag a ∈ F.boundaryFlags })
:
κ₂.openCircuitCount + (cutMatching F κ₂ o₂).unionCount N = κ₁.openCircuitCount + (cutMatching F κ₁ o₁).unionCount N
The ledger reads only the matching.
An open glue whose edge the subset misses #
theorem
RS.EdgeSubset.boundaryFlagI_not_mem_of_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s')
(hni : Fragment.partnerSurvI hopen ∉ s')
:
W.boundaryFlag i ∉ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags
Neither glued label is used when the interface edge is out of the subset.
theorem
RS.EdgeSubset.boundaryFlagJ_not_mem_of_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s')
(hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s')
(hni : Fragment.partnerSurvI hopen ∉ s')
:
W.boundaryFlag j ∉ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags
At a cut the subset misses, the second glued flag is not a boundary flag of the lift.
theorem
RS.EdgeSubset.chordInv_glueOpen_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s')
(hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s')
(hni : Fragment.partnerSurvI hopen ∉ s')
(κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem)
(l : Fragment.SurvivingLabel α i j)
(hlg : (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags)
:
↑({ flags := s', pairing_mem := hc' }.chordInv (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) l) = { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.chordInv κ ↑l
The chord matching is unchanged across a glue whose edge the subset misses: no chain reaches the cut, so no chain is rerouted.
noncomputable def
RS.EdgeSubset.usedLabelGlueMissEquiv
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s')
(hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s')
(hni : Fragment.partnerSurvI hopen ∉ s')
:
{ l : Fragment.SurvivingLabel α i j // (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags } ≃ { a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags }
The used labels are the same across a glue whose edge the subset misses.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
RS.EdgeSubset.cutMatching_glueOpen_miss_edge
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s')
(hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s')
(hni : Fragment.partnerSurvI hopen ∉ s')
[LinearOrder α]
(κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).Orientation)
:
(DirMatching.map (usedLabelGlueMissEquiv hij hopen s' hc' hc hni)
(cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) o')).edge = (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).edge
The glued cut matching's pairing is the lifted one's across a glue whose edge the subset misses.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_glueOpen_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s')
(hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s')
(hni : Fragment.partnerSurvI hopen ∉ s')
[LinearOrder α]
[Fintype α]
(κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).Orientation)
{N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags }}
{Ng :
DirMatching
{ l : Fragment.SurvivingLabel α i j // (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }}
(hNg : (DirMatching.map (usedLabelGlueMissEquiv hij hopen s' hc' hc hni) Ng).edge = N.edge)
:
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).openCircuitCount + (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) o').unionCount
Ng = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).unionCount N
A glue whose edge the subset misses moves nothing. The circuit count and the number of components of the union are both unchanged.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_stage_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hopen : W.pairing (W.boundaryFlag i) ≠ W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairOpen i j hij hopen).pairing f ∈ s')
(hc : ∀ f ∈ Fragment.liftSubsetOpen hopen s', W.pairing f ∈ Fragment.liftSubsetOpen hopen s')
(hni : Fragment.partnerSurvI hopen ∉ s')
[LinearOrder α]
[Fintype α]
{γ : Type}
[LinearOrder γ]
[Fintype γ]
(E : Fragment.SurvivingLabel α i j ≃o γ)
(κ : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ).Orientation)
{N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags }}
{Ng :
DirMatching
{ l : Fragment.SurvivingLabel α i j // (W.gluePairOpen i j hij hopen).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }}
(hNg : (DirMatching.map (usedLabelGlueMissEquiv hij hopen s' hc' hc hni) Ng).edge = N.edge)
{Mr Nr :
DirMatching
{ b : γ // ((W.gluePairOpen i j hij hopen).relabel E.toEquiv).boundaryFlag b ∈ (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }).boundaryFlags }}
(heM :
(DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Mr).edge = (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueOpen hij hopen s' hc' hc κ) o').edge)
(heN : (DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge = Ng.edge)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).openCircuitCount + Mr.unionCount Nr = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).unionCount N
One stage of the interface recursion at an open cut the subset misses.
A closed glue whose edge the subset leaves out #
At a closed cut the subset has a free choice: the closed-off edge is
in it or not. When it is not, the two glued labels are unused, the
chord matching simply transports, and the circuit count is
unchanged — so nothing moves here either. (When it is, one component
disappears; that is GlueChord's closed ledger.)
theorem
RS.EdgeSubset.boundaryFlagI_not_mem_of_closed_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(s' : Finset (W.SurvivingFlag i j))
(hcF : ∀ f ∈ Fragment.liftSubsetClosed s' false, W.pairing f ∈ Fragment.liftSubsetClosed s' false)
:
W.boundaryFlag i ∉ { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.boundaryFlags
Neither glued label is used when the closed-off edge is left out of the subset.
theorem
RS.EdgeSubset.boundaryFlagJ_not_mem_of_closed_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(s' : Finset (W.SurvivingFlag i j))
(hcF : ∀ f ∈ Fragment.liftSubsetClosed s' false, W.pairing f ∈ Fragment.liftSubsetClosed s' false)
:
W.boundaryFlag j ∉ { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.boundaryFlags
The same at a closed cut the subset misses.
noncomputable def
RS.EdgeSubset.usedLabelGlueClosedMissEquiv
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hcF : ∀ f ∈ Fragment.liftSubsetClosed s' false, W.pairing f ∈ Fragment.liftSubsetClosed s' false)
:
{ l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags } ≃ { a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.boundaryFlags }
The used labels are the same across a closed glue whose edge the subset leaves out.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
RS.EdgeSubset.cutMatching_glueClosedMiss_edge
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hcF : ∀ f ∈ Fragment.liftSubsetClosed s' false, W.pairing f ∈ Fragment.liftSubsetClosed s' false)
[LinearOrder α]
(κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem)
(o' : κ'.Orientation)
(o : (RelTransitionSystem.unglueClosed hclosed false s' hc' hcF κ').Orientation)
:
(DirMatching.map (usedLabelGlueClosedMissEquiv hij hclosed s' hc' hcF)
(cutMatching { flags := s', pairing_mem := hc' } κ' o')).edge = (cutMatching { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }
(RelTransitionSystem.unglueClosed hclosed false s' hc' hcF κ') o).edge
The glued cut matching's pairing is the lifted one's across a closed glue whose edge the subset leaves out.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_glueClosed_miss
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hcF : ∀ f ∈ Fragment.liftSubsetClosed s' false, W.pairing f ∈ Fragment.liftSubsetClosed s' false)
[LinearOrder α]
[Fintype α]
(κ' : { flags := s', pairing_mem := hc' }.RelTransitionSystem)
(o' : κ'.Orientation)
(o : (RelTransitionSystem.unglueClosed hclosed false s' hc' hcF κ').Orientation)
{N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.boundaryFlags }}
{Ng :
DirMatching
{ l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }}
(hNg : (DirMatching.map (usedLabelGlueClosedMissEquiv hij hclosed s' hc' hcF) Ng).edge = N.edge)
:
κ'.openCircuitCount + (cutMatching { flags := s', pairing_mem := hc' } κ' o').unionCount Ng = (RelTransitionSystem.unglueClosed hclosed false s' hc' hcF κ').openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }
(RelTransitionSystem.unglueClosed hclosed false s' hc' hcF κ') o).unionCount
N
A closed glue whose edge the subset leaves out moves nothing. The circuit count and the number of components of the union are both unchanged.
The closed glue, in the direction the recursion runs #
The interface recursion is given the fragment before the glue and
builds the one after it, so it wants its transition system built the
same way round. RelTransitionSystem.glueClosed does that, and the
ledger transports to it because the round trip leaves the matching
alone.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_unglue_glueClosed
{α : Type}
{W : Fragment α}
{i j : α}
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(b : Bool)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hc : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b)
[LinearOrder α]
[Fintype α]
(κ : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.RelTransitionSystem)
(o : κ.Orientation)
(o₀ :
(RelTransitionSystem.unglueClosed hclosed b s' hc' hc
(RelTransitionSystem.glueClosed hclosed b s' hc' hc κ)).Orientation)
(N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.boundaryFlags })
:
(RelTransitionSystem.unglueClosed hclosed b s' hc' hc
(RelTransitionSystem.glueClosed hclosed b s' hc' hc κ)).openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }
(RelTransitionSystem.unglueClosed hclosed b s' hc' hc (RelTransitionSystem.glueClosed hclosed b s' hc' hc κ))
o₀).unionCount
N = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc } κ o).unionCount N
The ledger transports to the forward glue. Ungluing the forward glue returns a system matching like the original, so the two carry the same ledger.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_glueClosed_forward
{α : Type}
{W : Fragment α}
{i j : α}
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hcT : ∀ f ∈ Fragment.liftSubsetClosed s' true, W.pairing f ∈ Fragment.liftSubsetClosed s' true)
[LinearOrder α]
[Fintype α]
(κ : { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ).Orientation)
(o₀ :
(RelTransitionSystem.unglueClosed hclosed true s' hc' hcT
(RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ)).Orientation)
(hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags)
(hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags)
{N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags }}
(hNij : N.edge ⟨i, hbi⟩ = ⟨j, hbj⟩)
{Ng :
DirMatching
{ l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }}
(hNg : (DirMatching.map (usedLabelGlueClosedEquiv hclosed s' hc' hcT hbi hbj) Ng).edge = (N.restrict hNij).edge)
:
(RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ).openCircuitCount + (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ)
o').unionCount
Ng + 1 = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT } κ o).unionCount N
A closed glue whose edge the subset carries drops one component, stated at the forward glue.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_stage_closed_forward
{α : Type}
{W : Fragment α}
{i j : α}
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hcT : ∀ f ∈ Fragment.liftSubsetClosed s' true, W.pairing f ∈ Fragment.liftSubsetClosed s' true)
[LinearOrder α]
[Fintype α]
{γ : Type}
[LinearOrder γ]
[Fintype γ]
(E : Fragment.SurvivingLabel α i j ≃o γ)
(κ : { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ).Orientation)
(o₀ :
(RelTransitionSystem.unglueClosed hclosed true s' hc' hcT
(RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ)).Orientation)
(hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags)
(hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags)
{N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }.boundaryFlags }}
(hNij : N.edge ⟨i, hbi⟩ = ⟨j, hbj⟩)
{Ng :
DirMatching
{ l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }}
(hNg : (DirMatching.map (usedLabelGlueClosedEquiv hclosed s' hc' hcT hbi hbj) Ng).edge = (N.restrict hNij).edge)
{Mr Nr :
DirMatching
{ b : γ // ((W.gluePairClosed i j hclosed).relabel E.toEquiv).boundaryFlag b ∈ (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }).boundaryFlags }}
(heM :
(DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Mr).edge = (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ)
o').edge)
(heN : (DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge = Ng.edge)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ)).openCircuitCount + Mr.unionCount Nr + 1 = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT } κ o).unionCount N
One stage of the interface recursion at a closed cut the subset carries, stated at the forward glue.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_glueClosed_miss_forward
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hcF : ∀ f ∈ Fragment.liftSubsetClosed s' false, W.pairing f ∈ Fragment.liftSubsetClosed s' false)
[LinearOrder α]
[Fintype α]
(κ : { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ).Orientation)
(o₀ :
(RelTransitionSystem.unglueClosed hclosed false s' hc' hcF
(RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ)).Orientation)
{N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.boundaryFlags }}
{Ng :
DirMatching
{ l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }}
(hNg : (DirMatching.map (usedLabelGlueClosedMissEquiv hij hclosed s' hc' hcF) Ng).edge = N.edge)
:
(RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ).openCircuitCount + (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ)
o').unionCount
Ng = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF } κ o).unionCount N
A closed glue whose edge the subset leaves out moves nothing, stated at the forward glue.
theorem
RS.EdgeSubset.openCircuitCount_add_unionCount_stage_closed_miss_forward
{α : Type}
{W : Fragment α}
{i j : α}
(hij : i ≠ j)
(hclosed : W.pairing (W.boundaryFlag i) = W.boundaryFlag j)
(s' : Finset (W.SurvivingFlag i j))
(hc' : ∀ f ∈ s', (W.gluePairClosed i j hclosed).pairing f ∈ s')
(hcF : ∀ f ∈ Fragment.liftSubsetClosed s' false, W.pairing f ∈ Fragment.liftSubsetClosed s' false)
[LinearOrder α]
[Fintype α]
{γ : Type}
[LinearOrder γ]
[Fintype γ]
(E : Fragment.SurvivingLabel α i j ≃o γ)
(κ : { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ).Orientation)
(o₀ :
(RelTransitionSystem.unglueClosed hclosed false s' hc' hcF
(RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ)).Orientation)
{N :
DirMatching
{ a : α // W.boundaryFlag a ∈ { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }.boundaryFlags }}
{Ng :
DirMatching
{ l : Fragment.SurvivingLabel α i j // (W.gluePairClosed i j hclosed).boundaryFlag l ∈ { flags := s', pairing_mem := hc' }.boundaryFlags }}
(hNg : (DirMatching.map (usedLabelGlueClosedMissEquiv hij hclosed s' hc' hcF) Ng).edge = N.edge)
{Mr Nr :
DirMatching
{ b : γ // ((W.gluePairClosed i j hclosed).relabel E.toEquiv).boundaryFlag b ∈ (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }).boundaryFlags }}
(heM :
(DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Mr).edge = (cutMatching { flags := s', pairing_mem := hc' } (RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ)
o').edge)
(heN : (DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge = Ng.edge)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ)).openCircuitCount + Mr.unionCount Nr = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF } κ o).unionCount N
One stage of the interface recursion at a closed cut the subset leaves out, stated at the forward glue.