One stage of the interface recursion, with the matchings supplied #
The per-glue ledgers ask for two matchings and a handful of equations between their pairings. In the recursion both matchings pair by an involution of the labels — the chord matching by the subset's chords, the interface matching by the swap — and the equations are then automatic. This file states each stage with the interface matching given that way, so that a stage consumes only the involution and the one equation saying the glued labels are partners.
theorem
RS.EdgeSubset.ledgerStage_open
{α : 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')
[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)
(o'' :
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).Orientation)
(hpi : Fragment.partnerSurvI hopen ∈ s')
(hbi : W.boundaryFlag i ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags)
(hbj : W.boundaryFlag j ∈ { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.boundaryFlags)
(ι : α → α)
(hcut : ι i = j)
{N : DirMatching (UsedLab { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc })}
(hN : ∀ (x : UsedLab { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }), ↑(N.edge x) = ι ↑x)
{Nr : DirMatching (UsedLab (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }))}
(hNr :
∀ (z : UsedLab { flags := s', pairing_mem := hc' }),
↑↑((DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge z) = ι ↑↑z)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).openCircuitCount + (cutMatching (relabelUp E.toEquiv { flags := s', pairing_mem := hc' })
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ))
o'').unionCount
Nr = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).unionCount N
One stage at an open cut the subset uses. The circuit count and the number of components of the union move together.
theorem
RS.EdgeSubset.ledgerStage_open_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')
[LinearOrder α]
[Fintype α]
{γ : Type}
[LinearOrder γ]
[Fintype γ]
(hni : Fragment.partnerSurvI hopen ∉ s')
(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)
(o'' :
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).Orientation)
(ι : α → α)
{N : DirMatching (UsedLab { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc })}
(hN : ∀ (x : UsedLab { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }), ↑(N.edge x) = ι ↑x)
{Nr : DirMatching (UsedLab (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }))}
(hNr :
∀ (z : UsedLab { flags := s', pairing_mem := hc' }),
↑↑((DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge z) = ι ↑↑z)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).openCircuitCount + (cutMatching (relabelUp E.toEquiv { flags := s', pairing_mem := hc' })
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ))
o'').unionCount
Nr = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).unionCount N
One stage at an open cut the subset misses. Nothing moves: the two glued labels are unused, so the chord matching and the interface matching both simply transport.
theorem
RS.EdgeSubset.ledgerStage_closed
{α : 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)
(o'' :
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(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)
(ι : α → α)
(hcut : ι i = j)
{N : DirMatching (UsedLab { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT })}
(hN : ∀ (x : UsedLab { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT }), ↑(N.edge x) = ι ↑x)
{Nr : DirMatching (UsedLab (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }))}
(hNr :
∀ (z : UsedLab { flags := s', pairing_mem := hc' }),
↑↑((DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge z) = ι ↑↑z)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ)).openCircuitCount + (cutMatching (relabelUp E.toEquiv { flags := s', pairing_mem := hc' })
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed true s' hc' hcT κ))
o'').unionCount
Nr + 1 = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' true, pairing_mem := hcT } κ o).unionCount N
One stage at a closed cut the subset carries. One component of the union disappears, into the free circle the glue creates.
theorem
RS.EdgeSubset.ledgerStage_closed_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 α]
{γ : 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)
(o'' :
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ)).Orientation)
(ι : α → α)
{N : DirMatching (UsedLab { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF })}
(hN : ∀ (x : UsedLab { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF }), ↑(N.edge x) = ι ↑x)
{Nr : DirMatching (UsedLab (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }))}
(hNr :
∀ (z : UsedLab { flags := s', pairing_mem := hc' }),
↑↑((DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge z) = ι ↑↑z)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ)).openCircuitCount + (cutMatching (relabelUp E.toEquiv { flags := s', pairing_mem := hc' })
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed false s' hc' hcF κ))
o'').unionCount
Nr = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' false, pairing_mem := hcF } κ o).unionCount N
One stage at a closed cut the subset leaves out. Nothing moves; the free circle the glue creates carries no chord.
The two cut kinds, each in one statement #
Whether the subset uses a cut is decided by the data, not by the caller, so each kind of cut is better stated once: an open cut moves nothing either way, and a closed one drops a component exactly when the subset carries its edge.
theorem
RS.EdgeSubset.ledgerStage_open_any
{α : 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')
[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)
(o'' :
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).Orientation)
(ι : α → α)
(hcut : ι i = j)
{N : DirMatching (UsedLab { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc })}
(hN : ∀ (x : UsedLab { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }), ↑(N.edge x) = ι ↑x)
{Nr : DirMatching (UsedLab (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }))}
(hNr :
∀ (z : UsedLab { flags := s', pairing_mem := hc' }),
↑↑((DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge z) = ι ↑↑z)
:
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ)).openCircuitCount + (cutMatching (relabelUp E.toEquiv { flags := s', pairing_mem := hc' })
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueOpen hij hopen s' hc' hc κ))
o'').unionCount
Nr = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc } κ o).unionCount N
One stage at an open cut. Nothing moves, whether or not the subset uses the cut.
theorem
RS.EdgeSubset.ledgerStage_closed_bit
{α : Type}
{W : Fragment α}
{i j : α}
(hij : 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')
(hcb : ∀ f ∈ Fragment.liftSubsetClosed s' b, W.pairing f ∈ Fragment.liftSubsetClosed s' b)
[LinearOrder α]
[Fintype α]
{γ : Type}
[LinearOrder γ]
[Fintype γ]
(E : Fragment.SurvivingLabel α i j ≃o γ)
(κ : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hcb }.RelTransitionSystem)
(o : κ.Orientation)
(o' : (RelTransitionSystem.glueClosed hclosed b s' hc' hcb κ).Orientation)
(o₀ :
(RelTransitionSystem.unglueClosed hclosed b s' hc' hcb
(RelTransitionSystem.glueClosed hclosed b s' hc' hcb κ)).Orientation)
(o'' :
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed b s' hc' hcb κ)).Orientation)
(ι : α → α)
(hcut : ι i = j)
{N : DirMatching (UsedLab { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hcb })}
(hN : ∀ (x : UsedLab { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hcb }), ↑(N.edge x) = ι ↑x)
{Nr : DirMatching (UsedLab (relabelUp E.toEquiv { flags := s', pairing_mem := hc' }))}
(hNr :
∀ (z : UsedLab { flags := s', pairing_mem := hc' }),
↑↑((DirMatching.map (usedLabRelabelEquiv E { flags := s', pairing_mem := hc' }) Nr).edge z) = ι ↑↑z)
:
((relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed b s' hc' hcb κ)).openCircuitCount + (cutMatching (relabelUp E.toEquiv { flags := s', pairing_mem := hc' })
(relabelTransUp E.toEquiv { flags := s', pairing_mem := hc' }
(RelTransitionSystem.glueClosed hclosed b s' hc' hcb κ))
o'').unionCount
Nr + if b = true then 1 else 0) = κ.openCircuitCount + (cutMatching { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hcb } κ o).unionCount N
One stage at a closed cut. A component of the union disappears exactly when the subset carries the cut's own edge.
Pairing across a glue #
Both glues read a surviving label as a label, so the pairing record transports as soon as the glued swap does — one equation between label maps, with the subset's own data nowhere in it.
theorem
RS.EdgeSubset.swapPaired_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)
(ι : α → α)
(ιg : Fragment.SurvivingLabel α i j → Fragment.SurvivingLabel α i j)
(hcomp : ∀ (x : Fragment.SurvivingLabel α i j), ↑(ιg x) = ι ↑x)
(hp : { flags := Fragment.liftSubsetClosed s' b, pairing_mem := hc }.SwapPaired ι)
:
{ flags := s', pairing_mem := hc' }.SwapPaired ιg
Pairing across a closed glue.
theorem
RS.EdgeSubset.swapPaired_glueOpen
{α : 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')
(ι : α → α)
(ιg : Fragment.SurvivingLabel α i j → Fragment.SurvivingLabel α i j)
(hcomp : ∀ (x : Fragment.SurvivingLabel α i j), ↑(ιg x) = ι ↑x)
(hp : { flags := Fragment.liftSubsetOpen hopen s', pairing_mem := hc }.SwapPaired ι)
:
{ flags := s', pairing_mem := hc' }.SwapPaired ιg
Pairing across an open glue.