The pair datum at one pair of subsets #
RS21's (13) and (14) at a single pair of subsets of two composable fragments: the tail function the pair's chords induce on the interface labels, how it behaves at a through edge, at a cut and at a pinned end, and the edge term the pair contributes.
ConverseFamily.lean chooses one such datum at every subset of the
composition's base and sums the results; ConverseTrip.lean carries
the choice up and down the interface.
@[reducible]
The lexicographic order on the interface's label type.
Equations
- RS.EdgeSubset.pairBaseOrder n = RS.sumLexLinearOrder (Fin (0 + n)) (Fin (n + 0))
Instances For
@[reducible]
The same order one stage up.
Equations
- RS.EdgeSubset.pairOrderSucc n = RS.sumLexLinearOrder (Fin (0 + n + 1)) (Fin (n + 1 + 0))
Instances For
@[reducible]
The order a stage's surviving labels carry.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible]
The order the composition's own label type carries.
Equations
Instances For
Every interface has a cut colouring: a two-colouring of its flags alternating along every edge and across every interface pair. Each stage extends the next one's colouring. At an open cut the cut's two flags take the opposite colour to their partners, which survive the glue, and the top cut's own condition is then the stage's alternation along the edge the glue creates. At a closing cut both flags leave with the glue, so their colours are free, and the one constraint the edge and the pair jointly impose is met by opposing them.
noncomputable def
RS.EdgeSubset.pairTailFun
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
:
The directions the two matchings prescribe. At a used label's boundary flag the matching's tail; elsewhere the given colouring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
RS.EdgeSubset.pairTailFun_of_not_used
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(f : (closeBase F G).Flag)
(h :
¬∃ (m : Fin t),
f = (closeBase F G).boundaryFlag (intL t m) ∧ F.boundaryFlag m ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
(h' :
¬∃ (m : Fin t),
f = (closeBase F G).boundaryFlag (intR t m) ∧ G.boundaryFlag m ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
:
At a flag that is no used label's, the prescribed direction is the colouring's.
theorem
RS.EdgeSubset.pairTailFun_intL
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(m : Fin t)
(hm : F.boundaryFlag m ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
:
At a used left label the prescribed direction is the left matching's tail.
theorem
RS.EdgeSubset.pairTailFun_intR
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(m : Fin t)
(hm : G.boundaryFlag m ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
:
At a used right label the prescribed direction is the right matching's tail.
theorem
RS.EdgeSubset.boundaryFlag_chordInv_of_through
{α : Type}
{W : Fragment α}
(F : EdgeSubset W)
(κ : F.RelTransitionSystem)
{i : α}
(h : W.boundaryFlag i ∈ F.boundaryFlags)
(hthr : IsThroughLabel F i)
:
At a through label the chord is the edge. The chain from a through label's flag is the single edge, so the chord partner's flag is the pairing partner.
theorem
RS.EdgeSubset.pairTailFun_flip_through_left
{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₂)
{κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem}
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hM₁ :
∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }),
↑(M₁.edge a) = { flags := s₁, pairing_mem := hc₁ }.chordInv κ₁ ↑a)
(m : Fin t)
(hm : F.boundaryFlag m ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
(hthr : IsThroughLabel { flags := s₁, pairing_mem := hc₁ } m)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).pairing ((closeBase F G).boundaryFlag (intL t m))) = !pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intL t m))
The prescribed directions flip along a through edge on the left. The chord is the edge, and a matching's two ends are oppositely directed.
theorem
RS.EdgeSubset.pairTailFun_flip_through_right
{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₂)
{κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem}
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hM₂ :
∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }),
↑(M₂.edge b) = { flags := s₂, pairing_mem := hc₂ }.chordInv κ₂ ↑b)
(m : Fin t)
(hm : G.boundaryFlag m ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(hthr : IsThroughLabel { flags := s₂, pairing_mem := hc₂ } m)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).pairing ((closeBase F G).boundaryFlag (intR t m))) = !pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intR t m))
The prescribed directions flip along a through edge on the right.
theorem
RS.EdgeSubset.pairTailFun_cut
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hb :
∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(halt :
∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }),
M₂.tail (({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) = !M₁.tail a)
(m : Fin t)
(hm : F.boundaryFlag m ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intR t m)) = !pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intL t m))
The prescribed directions alternate across a used cut. This is RS21's Eulerian position, read at the interface pair: the two matchings' tails are opposite at every used label.
theorem
RS.EdgeSubset.flip_pinned_left
{t : ℕ}
{F G : Fragment (Fin t)}
{B : EdgeSubset (closeBase F G)}
{κ : B.RelTransitionSystem}
(O : κ.Orientation)
(g : (closeBase F G).Flag → Bool)
{A₁ : EdgeSubset F}
{κ₁ : A₁.RelTransitionSystem}
(o₁ : κ₁.Orientation)
(hL : ∀ (x : F.Flag), O.isOut (Sum.inl x) = o₁.isOut x)
(m : Fin t)
(hint : cutFlagL F G m ∈ B.internalFlags)
(hg : g ((closeBase F G).boundaryFlag (intL t m)) = !chainDir o₁ (F.boundaryFlag m))
:
(orientReplace O g).isOut (cutFlagL F G m) = !(orientReplace O g).isOut ((closeBase F G).boundaryFlag (intL t m))
The flip at a pinned left label. When the label's partner is internal its direction is the orientation's own, so the boundary flag's prescribed direction has only to be the chain direction's opposite — which is what the matching's tail is.
theorem
RS.EdgeSubset.flip_pinned_right
{t : ℕ}
{F G : Fragment (Fin t)}
{B : EdgeSubset (closeBase F G)}
{κ : B.RelTransitionSystem}
(O : κ.Orientation)
(g : (closeBase F G).Flag → Bool)
{A₂ : EdgeSubset G}
{κ₂ : A₂.RelTransitionSystem}
(o₂ : κ₂.Orientation)
(hR : ∀ (y : G.Flag), O.isOut (Sum.inr y) = o₂.isOut y)
(m : Fin t)
(hint : cutFlagR F G m ∈ B.internalFlags)
(hg : g ((closeBase F G).boundaryFlag (intR t m)) = !chainDir o₂ (G.boundaryFlag m))
:
(orientReplace O g).isOut (cutFlagR F G m) = !(orientReplace O g).isOut ((closeBase F G).boundaryFlag (intR t m))
The flip at a pinned right label.
theorem
RS.EdgeSubset.pairTailFun_pinned_left
{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₂)
{κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem}
(o₁ : κ₁.Orientation)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hag₁ :
∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }),
¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } ↑a →
M₁.tail a = (cutMatching { flags := s₁, pairing_mem := hc₁ } κ₁ o₁).tail a)
(m : Fin t)
(hm : F.boundaryFlag m ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
(hnt : ¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } m)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intL t m)) = !chainDir o₁ (F.boundaryFlag m)
At a pinned left label the tail is the chain direction's opposite.
theorem
RS.EdgeSubset.pairTailFun_pinned_right
{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₂)
{κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem}
(o₂ : κ₂.Orientation)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hag₂ :
∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }),
¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } ↑b →
M₂.tail b = (cutMatching { flags := s₂, pairing_mem := hc₂ } κ₂ o₂).tail b)
(m : Fin t)
(hm : G.boundaryFlag m ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(hnt : ¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } m)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intR t m)) = !chainDir o₂ (G.boundaryFlag m)
At a pinned right label the tail is the chain direction's opposite.
theorem
RS.EdgeSubset.not_used_of_pairing
{α : Type}
{W : Fragment α}
{s : Finset W.Flag}
(hc : ∀ f ∈ s, W.pairing f ∈ s)
{a b : α}
(h : W.pairing (W.boundaryFlag a) = W.boundaryFlag b)
(hu : W.boundaryFlag a ∉ { flags := s, pairing_mem := hc }.boundaryFlags)
:
W.boundaryFlag b ∉ { flags := s, pairing_mem := hc }.boundaryFlags
An unused label's partner label is unused. The subset is closed under the pairing, so a used partner would drag the label in with it.
theorem
RS.EdgeSubset.pairTailFun_flip_unused_left
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hcol : ∀ (f : (closeBase F G).Flag), c ((closeBase F G).pairing f) = !c f)
(m : Fin t)
(hu : F.boundaryFlag m ∉ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).pairing ((closeBase F G).boundaryFlag (intL t m))) = !pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intL t m))
The prescribed directions flip at an unused left label. Both ends fall to the colouring, which alternates along every edge.
theorem
RS.EdgeSubset.pairTailFun_flip_unused_right
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hcol : ∀ (f : (closeBase F G).Flag), c ((closeBase F G).pairing f) = !c f)
(m : Fin t)
(hu : G.boundaryFlag m ∉ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).pairing ((closeBase F G).boundaryFlag (intR t m))) = !pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intR t m))
The prescribed directions flip at an unused right label.
theorem
RS.EdgeSubset.pairTailFun_cut_unused
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hcut : ∀ (m : Fin t), c ((closeBase F G).boundaryFlag (intR t m)) = !c ((closeBase F G).boundaryFlag (intL t m)))
(m : Fin t)
(hu₁ : F.boundaryFlag m ∉ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
(hu₂ : G.boundaryFlag m ∉ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
:
pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intR t m)) = !pairTailFun hc₁ hc₂ M₁ M₂ c ((closeBase F G).boundaryFlag (intL t m))
The prescribed directions alternate across an unused cut.
theorem
RS.EdgeSubset.pairing_not_internal_of_not_mem
{α : Type}
{W : Fragment α}
(B : EdgeSubset W)
{f : W.Flag}
(hf : f ∉ B.flags)
:
W.pairing f ∉ B.internalFlags
An absent flag's partner is not internal.
theorem
RS.EdgeSubset.inl_boundaryFlag_not_mem_closeJoin
{t : ℕ}
{F G : Fragment (Fin t)}
{s₁ : Finset F.Flag}
(hc₁ : ∀ f ∈ s₁, F.pairing f ∈ s₁)
(s₂ : Finset G.Flag)
(m : Fin t)
(hu : F.boundaryFlag m ∉ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags)
:
(closeBase F G).boundaryFlag (intL t m) ∉ closeJoin s₁ s₂
An unused left label's flag is absent from the joined subset.
theorem
RS.EdgeSubset.inr_boundaryFlag_not_mem_closeJoin
{t : ℕ}
{F G : Fragment (Fin t)}
(s₁ : Finset F.Flag)
{s₂ : Finset G.Flag}
(hc₂ : ∀ f ∈ s₂, G.pairing f ∈ s₂)
(m : Fin t)
(hu : G.boundaryFlag m ∉ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
:
(closeBase F G).boundaryFlag (intR t m) ∉ closeJoin s₁ s₂
An unused right label's flag is absent from the joined subset.
theorem
RS.EdgeSubset.orientReplace_pairTailFun_flip
{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₂)
{κ₁ : { flags := s₁, pairing_mem := hc₁ }.RelTransitionSystem}
(o₁ : κ₁.Orientation)
{κ₂ : { flags := s₂, pairing_mem := hc₂ }.RelTransitionSystem}
(o₂ : κ₂.Orientation)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hcol : ∀ (f : (closeBase F G).Flag), c ((closeBase F G).pairing f) = !c f)
(hM₁ :
∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }),
↑(M₁.edge a) = { flags := s₁, pairing_mem := hc₁ }.chordInv κ₁ ↑a)
(hM₂ :
∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }),
↑(M₂.edge b) = { flags := s₂, pairing_mem := hc₂ }.chordInv κ₂ ↑b)
(hag₁ :
∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }),
¬IsThroughLabel { flags := s₁, pairing_mem := hc₁ } ↑a →
M₁.tail a = (cutMatching { flags := s₁, pairing_mem := hc₁ } κ₁ o₁).tail a)
(hag₂ :
∀ (b : UsedLab { flags := s₂, pairing_mem := hc₂ }),
¬IsThroughLabel { flags := s₂, pairing_mem := hc₂ } ↑b →
M₂.tail b = (cutMatching { flags := s₂, pairing_mem := hc₂ } κ₂ o₂).tail b)
{κ : { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.RelTransitionSystem}
(O : κ.Orientation)
(hL : ∀ (x : F.Flag), O.isOut (Sum.inl x) = o₁.isOut x)
(hR : ∀ (y : G.Flag), O.isOut (Sum.inr y) = o₂.isOut y)
(ℓ : Fin (0 + t) ⊕ Fin (t + 0))
:
(orientReplace O (pairTailFun hc₁ hc₂ M₁ M₂ c)).isOut ((closeBase F G).pairing ((closeBase F G).boundaryFlag ℓ)) = !(orientReplace O (pairTailFun hc₁ hc₂ M₁ M₂ c)).isOut ((closeBase F G).boundaryFlag ℓ)
The pair's prescribed orientation flips along every interface
edge. Six cases: at a used label the matchings supply the
direction — the chord's two ends by tail_flip, the pinned end by
the tail's agreement with the chain — and at an unused label the cut
colouring does.
theorem
RS.EdgeSubset.orientReplace_pairTailFun_cut
{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₂)
(M₁ : DirMatching (UsedLab { flags := s₁, pairing_mem := hc₁ }))
(M₂ : DirMatching (UsedLab { flags := s₂, pairing_mem := hc₂ }))
(c : (closeBase F G).Flag → Bool)
(hcut : ∀ (m : Fin t), c ((closeBase F G).boundaryFlag (intR t m)) = !c ((closeBase F G).boundaryFlag (intL t m)))
(hb :
∀ (i : Fin t),
F.boundaryFlag i ∈ { flags := s₁, pairing_mem := hc₁ }.boundaryFlags ↔ G.boundaryFlag i ∈ { flags := s₂, pairing_mem := hc₂ }.boundaryFlags)
(halt :
∀ (a : UsedLab { flags := s₁, pairing_mem := hc₁ }),
M₂.tail (({ flags := s₁, pairing_mem := hc₁ }.usedLabInterfaceEquiv { flags := s₂, pairing_mem := hc₂ } hb) a) = !M₁.tail a)
{κ : { flags := closeJoin s₁ s₂, pairing_mem := ⋯ }.RelTransitionSystem}
(O : κ.Orientation)
(m : Fin t)
:
(orientReplace O (pairTailFun hc₁ hc₂ M₁ M₂ c)).isOut ((closeBase F G).boundaryFlag (intR t m)) = !(orientReplace O (pairTailFun hc₁ hc₂ M₁ M₂ c)).isOut ((closeBase F G).boundaryFlag (intL t m))
The pair's prescribed orientation alternates across every interface pair. At a used label this is the Eulerian position of the two matchings; at an unused one, the cut colouring.
theorem
RS.EdgeSubset.cutBalanced_top_liftSubsetOpen
{t : ℕ}
{V : Fragment (Fin (0 + t) ⊕ Fin (t + 0))}
{i j : Fin (0 + t) ⊕ Fin (t + 0)}
(hij : i ≠ j)
(hop : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(s' : Finset (V.SurvivingFlag i j))
(hcs : ∀ f ∈ s', Fragment.rewire hop f ∈ s')
:
V.boundaryFlag i ∈ Fragment.liftSubsetOpen hop s' ↔ V.boundaryFlag j ∈ Fragment.liftSubsetOpen hop s'
The lift is balanced at the top cut. The glue joins the two cut flags' partners into one edge, so a pairing-closed stage subset takes them together — and the lift then takes both cut flags or neither.
theorem
RS.EdgeSubset.mem_stage_boundaryFlag_iff
(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.SurvivingFlag (cutL n) (cutR n)))
(bl : Fin (0 + n) ⊕ Fin (n + 0))
:
(stepFragment n V).boundaryFlag bl ∈ flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ s' ↔ V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl) ∈ Fragment.liftSubsetOpen hop s'
A stage boundary flag is in the transported subset exactly when the base's is in the lift.
theorem
RS.EdgeSubset.cutBalanced_liftSubsetOpen
(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.SurvivingFlag (cutL n) (cutR n)))
(hcs : ∀ f ∈ s', Fragment.rewire hop f ∈ s')
(hbal :
CutBalanced (stepFragment n V)
(flagsOfEq (V.gluePairOpen (cutL n) (cutR n) ⋯ hop) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ s'))
:
CutBalanced V (Fragment.liftSubsetOpen hop s')
The lift of a balanced stage subset is balanced. The top cut is balanced by the glue's own edge, and each lower pair is the stage's own.
theorem
RS.EdgeSubset.mem_stage_boundaryFlag_iff_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.SurvivingFlag (cutL n) (cutR n)))
(b : Bool)
(bl : Fin (0 + n) ⊕ Fin (n + 0))
:
(stepFragment n V).boundaryFlag bl ∈ flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ s' ↔ V.boundaryFlag ↑((interfaceStepEquiv 0 n 0).symm bl) ∈ Fragment.liftSubsetClosed s' b
A stage boundary flag is in the stage's subset exactly when the base's is in the lift, at a closing cut.
theorem
RS.EdgeSubset.cutBalanced_liftSubsetClosed
(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.SurvivingFlag (cutL n) (cutR n)))
(b : Bool)
(hbal :
CutBalanced (stepFragment n V)
(flagsOfEq (V.gluePairClosed (cutL n) (cutR n) hcl) (V.gluePair (cutL n) (cutR n) ⋯) ⋯ s'))
:
CutBalanced V (Fragment.liftSubsetClosed s' b)
The lift of a balanced stage subset is balanced, at a closing cut: the cut's own pair is in or out together, by the bit.
theorem
RS.EdgeSubset.cutBalanced_stepData
(n : ℕ)
(V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)))
(hop : V.pairing (V.boundaryFlag (cutL n)) ≠ V.boundaryFlag (cutR n))
(D : StageData (n + 1) V)
(hbal : CutBalanced V D.sub.flags)
:
CutBalanced (stepFragment n V) (stepData n V D).sub.flags
The ledger's step keeps the balance.
theorem
RS.EdgeSubset.cutBalanced_stepData_closed
(n : ℕ)
(V : Fragment (Fin (0 + (n + 1)) ⊕ Fin (n + 1 + 0)))
(hcl : V.pairing (V.boundaryFlag (cutL n)) = V.boundaryFlag (cutR n))
(D : StageData (n + 1) V)
(hbal : CutBalanced V D.sub.flags)
:
CutBalanced (stepFragment n V) (stepData n V D).sub.flags
The ledger's step keeps the balance, at a closing cut.
noncomputable def
RS.EdgeSubset.edgeTermOf
{α : Type}
{V : Fragment α}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
{s : Finset V.Flag}
{hc : ∀ f ∈ s, V.pairing f ∈ s}
(d : (κ : { flags := s, pairing_mem := hc }.RelTransitionSystem) × κ.Orientation)
(st : GenBoundaryState k ℓ α)
(C : ℕ)
:
The summand a single datum computes. The total form of the colouring sum: zero where the subset does not carry the state.
Equations
- RS.EdgeSubset.edgeTermOf h d st C = if hbnd : RS.genBoundarySubsetMatches V s st then (-1) ^ C * { flags := s, pairing_mem := hc }.edgeSum h st hbnd d.snd else 0
Instances For
theorem
RS.EdgeSubset.edgeTermAt_eq_edgeTermOf
{α : Type}
[LinearOrder α]
{V : Fragment α}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily V)
(st : GenBoundaryState k ℓ α)
{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)
(C : ℕ)
:
The family's summand is its datum's.
theorem
RS.EdgeSubset.edgeTermOf_ofEq
{α : Type}
{V : Fragment α}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
{s s' : Finset V.Flag}
{hc : ∀ f ∈ s, V.pairing f ∈ s}
{hc' : ∀ f ∈ s', V.pairing f ∈ s'}
(hu : { flags := s, pairing_mem := hc } = { flags := s', pairing_mem := hc' })
(d : (κ : { flags := s, pairing_mem := hc }.RelTransitionSystem) × κ.Orientation)
(st : GenBoundaryState k ℓ α)
(C : ℕ)
:
The datum's summand transports along an equality of subsets.
theorem
RS.EdgeSubset.matches_closeJoin_iff
{k ℓ t : ℕ}
{F G : Fragment (Fin t)}
(s₁ : Finset F.Flag)
(s₂ : Finset G.Flag)
(x : GenBoundaryState k ℓ (Fin t))
:
genBoundarySubsetMatches (closeBase F G) (closeJoin s₁ s₂) (diagOf t x) ↔ genBoundarySubsetMatches F s₁ x ∧ genBoundarySubsetMatches G s₂ x
The join carries a diagonal state exactly when its halves carry the state.