RS21's summand, at a prescribed circuit count #
edgeSum is RS21's colouring sum; s_h(F,H,ω,κ) is that sum with
the circuit sign in front. The composition carries its own count
from stage to stage — an open glue may or may not close a circuit,
and settling that is the ledger's business, not the colouring's — so
the summand is named here with the count as a parameter, extended by
zero off the good subsets, exactly as termAt is.
theorem
RS.EdgeSubset.edgeSum_relOfEq
{L : Type}
{V : Fragment L}
{F F' : EdgeSubset V}
(hF : F = F')
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(st : GenBoundaryState k ℓ L)
(hbnd : genBoundarySubsetMatches V F.flags st)
(hbnd' : genBoundarySubsetMatches V F'.flags st)
{κ : F.RelTransitionSystem}
(o : κ.Orientation)
:
Transporting the colouring sum along an equality of subsets.
noncomputable def
RS.EdgeSubset.edgeTermAt
{L : Type}
[LinearOrder L]
{V : Fragment L}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily V)
(st : GenBoundaryState k ℓ L)
(s : Finset V.Flag)
(C : ℕ)
:
RS21's summand at a prescribed circuit count.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
RS.EdgeSubset.edgeTermAt_eq_zero_of_not_closed
{L : Type}
[LinearOrder L]
{V : Fragment L}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily V)
(st : GenBoundaryState k ℓ L)
{s : Finset V.Flag}
(hc : ¬∀ f ∈ s, V.pairing f ∈ s)
(C : ℕ)
:
The summand vanishes off edge-closed flag sets.
theorem
RS.EdgeSubset.edgeTermAt_eq_zero_of_not_matches
{L : Type}
[LinearOrder L]
{V : Fragment L}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily V)
(st : GenBoundaryState k ℓ L)
{s : Finset V.Flag}
(hbnd : ¬genBoundarySubsetMatches V s st)
(C : ℕ)
:
And off subsets that do not match the boundary state.
theorem
RS.EdgeSubset.edgeTermAt_eq_zero_of_not_eulerian
{L : Type}
[LinearOrder L]
{V : Fragment L}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily V)
(st : GenBoundaryState k ℓ L)
{s : Finset V.Flag}
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(hE : ¬{ flags := s, pairing_mem := hc }.Eulerian)
(C : ℕ)
:
And off non-Eulerian subsets.
theorem
RS.EdgeSubset.edgeTermAt_eq_zero_of_not_canon
{L : Type}
[LinearOrder L]
{V : Fragment L}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily V)
(st : GenBoundaryState k ℓ L)
{s : Finset V.Flag}
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(hne : ¬Nonempty { flags := s, pairing_mem := hc }.CanonData)
(C : ℕ)
:
And off subsets carrying no canonical datum — so the sum runs over the good subsets only.
theorem
RS.EdgeSubset.edgeTermAt_pos
{L : Type}
[LinearOrder L]
{V : Fragment L}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily V)
(st : GenBoundaryState k ℓ L)
{s : Finset V.Flag}
(hc : ∀ f ∈ s, V.pairing f ∈ s)
(hbnd : genBoundarySubsetMatches V s st)
(hE : { flags := s, pairing_mem := hc }.Eulerian)
(hne : Nonempty { flags := s, pairing_mem := hc }.CanonData)
(C : ℕ)
:
The summand at a good subset.
One open cut #
The boundary state's colour at the cut is even exactly when the subset misses it, so the sum over that colour runs over one block and is the glued fragment's summand.
theorem
RS.EdgeSubset.not_matches_liftOpen_odd_of_miss
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hni : Fragment.partnerSurvI hopen ∉ t)
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(d : Fin (2 * ℓ))
(c' : Fin k ⊕ Fin (2 * ℓ))
:
¬genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t) (GenBoundaryState.extendPair i j st' (Sum.inr d) c')
A missed cut admits no odd colour at the interface.
theorem
RS.EdgeSubset.not_matches_liftOpen_even_of_hit
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hpi : Fragment.partnerSurvI hopen ∈ t)
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(a : Fin k)
(c' : Fin k ⊕ Fin (2 * ℓ))
:
¬genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t) (GenBoundaryState.extendPair i j st' (Sum.inl a) c')
A carried cut admits no even colour at the interface.
theorem
RS.EdgeSubset.matches_liftOpen_of_miss
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t)
(hni : Fragment.partnerSurvI hopen ∉ t)
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairOpen i j hij hopen) t st')
(hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t)
(a : Fin k)
:
genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t)
(GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a))
On a missed cut the even extensions all match.
theorem
RS.EdgeSubset.matches_liftOpen_of_hit
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t)
(hpi : Fragment.partnerSurvI hopen ∈ t)
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairOpen i j hij hopen) t st')
(d : Fin (2 * ℓ))
:
genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t)
(GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d))
On a carried cut the odd extensions all match.
theorem
RS.EdgeSubset.edgeTermAt_liftOpen
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairOpen i j hij hopen))
(hcL : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t)
(st : GenBoundaryState k ℓ L)
(hbnd : genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t) st)
(hE : { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.Eulerian)
(hne : Nonempty { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.CanonData)
(hEt : { flags := t, pairing_mem := hct }.Eulerian)
(hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData)
(C : ℕ)
:
edgeTermAt h (unglueDataOpen hij hopen 𝒟') st (Fragment.liftSubsetOpen hopen t) C = (-1) ^ C * { flags := Fragment.liftSubsetOpen hopen t, pairing_mem := hcL }.edgeSum h st hbnd
(unglueOrientationOpen hij hopen t hct hcL (𝒟' t hct hEt hnet).fst (𝒟' t hct hEt hnet).snd)
The base's summand at an open lift is the glued fragment's data, unglued.
theorem
RS.EdgeSubset.edgeTermAt_openCut
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairOpen i j hij hopen).pairing f ∈ t)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairOpen i j hij hopen))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairOpen i j hij hopen) t st')
(hEt : { flags := t, pairing_mem := hct }.Eulerian)
(hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData)
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataOpen hij hopen 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetOpen hopen t) C = edgeTermAt h 𝒟' st' t C
One open cut, on RS21's summands. The interface colour is even exactly when the subset misses the cut, so the sum over it is the glued fragment's summand.
One open cut, with nothing assumed of the subset #
The iteration sums over every subset of the glued fragment, so the cut's identity is needed with no hypothesis on it. Off the good subsets both sides vanish — and where the glue's closure fails, what kills the lift is the interface state's own diagonality: the lift would hold one glued flag and not the other, and so want the state odd at one label and even at the other.
theorem
RS.EdgeSubset.rewire_closed_of_liftOpen_closed
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(c : Fin k ⊕ Fin (2 * ℓ))
(hcl : ∀ f ∈ Fragment.liftSubsetOpen hopen t, V.pairing f ∈ Fragment.liftSubsetOpen hopen t)
(hm : genBoundarySubsetMatches V (Fragment.liftSubsetOpen hopen t) (GenBoundaryState.extendPair i j st' c c))
(f : V.SurvivingFlag i j)
:
f ∈ t → (V.gluePairOpen i j hij hopen).pairing f ∈ t
A diagonal state forces the glue's closure.
theorem
RS.EdgeSubset.edgeTermAt_openCut_all
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hopen : V.pairing (V.boundaryFlag i) ≠ V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairOpen i j hij hopen))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataOpen hij hopen 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetOpen hopen t) C = edgeTermAt h 𝒟' st' t C
One open cut, with nothing assumed of the subset.
One closing cut #
Gluing an edge with both ends labelled leaves a free circle. On the
base the edge is a trail from one label to the other and carries no
circuit; in the composition it is a circuit, and the ledger records
that as the extra count the carried branch is taken at. The two
branches then weigh k and −2ℓ, which is the circle's own value.
theorem
RS.EdgeSubset.not_matches_liftClosed_odd_false
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(d : Fin (2 * ℓ))
(c' : Fin k ⊕ Fin (2 * ℓ))
:
¬genBoundarySubsetMatches V (Fragment.liftSubsetClosed t false) (GenBoundaryState.extendPair i j st' (Sum.inr d) c')
The empty branch admits no odd colour at the cut.
theorem
RS.EdgeSubset.not_matches_liftClosed_even_true
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(a : Fin k)
(c' : Fin k ⊕ Fin (2 * ℓ))
:
¬genBoundarySubsetMatches V (Fragment.liftSubsetClosed t true) (GenBoundaryState.extendPair i j st' (Sum.inl a) c')
The carried branch admits no even colour at the cut.
theorem
RS.EdgeSubset.matches_liftClosed_false
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st')
(a : Fin k)
:
genBoundarySubsetMatches V (Fragment.liftSubsetClosed t false)
(GenBoundaryState.extendPair i j st' (Sum.inl a) (Sum.inl a))
On the empty branch the even extensions all match.
theorem
RS.EdgeSubset.matches_liftClosed_true
{L : Type}
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st')
(d : Fin (2 * ℓ))
:
genBoundarySubsetMatches V (Fragment.liftSubsetClosed t true)
(GenBoundaryState.extendPair i j st' (Sum.inr d) (Sum.inr d))
On the carried branch the odd extensions all match.
theorem
RS.EdgeSubset.edgeTermAt_liftClosed
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairClosed i j hclosed))
(b : Bool)
(hcL : ∀ f ∈ Fragment.liftSubsetClosed t b, V.pairing f ∈ Fragment.liftSubsetClosed t b)
(st : GenBoundaryState k ℓ L)
(hbnd : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t b) st)
(hE : { flags := Fragment.liftSubsetClosed t b, pairing_mem := hcL }.Eulerian)
(hne : Nonempty { flags := Fragment.liftSubsetClosed t b, pairing_mem := hcL }.CanonData)
(hEt : { flags := t, pairing_mem := hct }.Eulerian)
(hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData)
(C : ℕ)
:
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') st (Fragment.liftSubsetClosed t b) C = (-1) ^ C * { flags := Fragment.liftSubsetClosed t b, pairing_mem := hcL }.edgeSum h st hbnd
(unglueOrientationClosed hclosed b t hct hcL (𝒟' t hct hEt hnet).fst (𝒟' t hct hEt hnet).snd)
The base's summand at a closed lift is the glued fragment's data, unglued.
theorem
RS.EdgeSubset.edgeTermAt_closedCut_false_row
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairClosed i j hclosed))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st')
(hEt : { flags := t, pairing_mem := hct }.Eulerian)
(hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData)
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t false) C = ↑k * edgeTermAt h 𝒟' st' t C
The empty branch of a closing cut weighs k. Only the even
colours reach it — the odd ones would ask for the cut's own edge —
and each of them gives the glued term back.
theorem
RS.EdgeSubset.edgeTermAt_closedCut_true_row
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairClosed i j hclosed))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st')
(hEt : { flags := t, pairing_mem := hct }.Eulerian)
(hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData)
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t true) (C + 1) = -↑(2 * ℓ) * edgeTermAt h 𝒟' st' t C
The carried branch of a closing cut weighs −2ℓ. Only the
odd colours reach it, and each of them gives the glued term back with
the sign the extra carried cut supplies.
theorem
RS.EdgeSubset.edgeTermAt_closedCut
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(hct : ∀ f ∈ t, (V.gluePairClosed i j hclosed).pairing f ∈ t)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairClosed i j hclosed))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(hbnd' : genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st')
(hEt : { flags := t, pairing_mem := hct }.Eulerian)
(hnet : Nonempty { flags := t, pairing_mem := hct }.CanonData)
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t false) C + ∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t true) (C + 1) = (↑k - 2 * ↑ℓ) * edgeTermAt h 𝒟' st' t C
One closing cut, on RS21's summands. The two branches of the
closed edge weigh k and −2ℓ, the free circle's own value.
One closing cut, with nothing assumed of the subset #
theorem
RS.EdgeSubset.genBoundarySubsetMatches_glued_of_liftClosed
{L : Type}
{V : Fragment L}
{i j : L}
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(b : Bool)
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(c c' : Fin k ⊕ Fin (2 * ℓ))
(hm : genBoundarySubsetMatches V (Fragment.liftSubsetClosed t b) (GenBoundaryState.extendPair i j st' c c'))
:
genBoundarySubsetMatches (V.gluePairClosed i j hclosed) t st'
The glued boundary constraint from the lift's.
theorem
RS.EdgeSubset.glued_closed_of_liftClosed_closed
{L : Type}
{V : Fragment L}
{i j : L}
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
(b : Bool)
(hcl : ∀ f ∈ Fragment.liftSubsetClosed t b, V.pairing f ∈ Fragment.liftSubsetClosed t b)
(f : V.SurvivingFlag i j)
:
f ∈ t → (V.gluePairClosed i j hclosed).pairing f ∈ t
A closed lift's closure is the glue's.
theorem
RS.EdgeSubset.edgeTermAt_closedCut_all
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairClosed i j hclosed))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t false) C + ∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t true) (C + 1) = (↑k - 2 * ↑ℓ) * edgeTermAt h 𝒟' st' t C
One closing cut, with nothing assumed of the subset.
theorem
RS.EdgeSubset.edgeTermAt_closedCut_false_row_all
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairClosed i j hclosed))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t false) C = ↑k * edgeTermAt h 𝒟' st' t C
The empty branch of a closing cut weighs k, with nothing
assumed of the subset.
theorem
RS.EdgeSubset.edgeTermAt_closedCut_true_row_all
{L : Type}
[LinearOrder L]
{V : Fragment L}
{i j : L}
(hij : i ≠ j)
(hclosed : V.pairing (V.boundaryFlag i) = V.boundaryFlag j)
(t : Finset (V.SurvivingFlag i j))
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟' : DataFamily (V.gluePairClosed i j hclosed))
(st' : GenBoundaryState k ℓ (Fragment.SurvivingLabel L i j))
(C : ℕ)
:
∑ c : Fin k ⊕ Fin (2 * ℓ),
edgeTermAt h (unglueDataClosed hij hclosed 𝒟') (GenBoundaryState.extendPair i j st' c c)
(Fragment.liftSubsetClosed t true) (C + 1) = -↑(2 * ℓ) * edgeTermAt h 𝒟' st' t C
The carried branch of a closing cut weighs −2ℓ, with
nothing assumed of the subset.
RS21's sum over a disjoint union #
The two halves of a composition colour their own edges, and a through-edge of the union is a through-edge of one of them, so the agreement splits with the sum.
theorem
RS.EdgeSubset.usedColour_inl
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
{k ℓ : ℕ}
(st : GenBoundaryState k ℓ (α ⊕ β))
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₁ : genBoundarySubsetMatches W₁ (leftSub F).flags fun (a : α) => st (Sum.inl a))
{g : W₁.Flag}
(hbD : Sum.inl g ∈ F.boundaryFlags)
(hb : g ∈ (leftSub F).boundaryFlags)
:
The named colour of a left flag is the left half's.
theorem
RS.EdgeSubset.usedColour_inr
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
{k ℓ : ℕ}
(st : GenBoundaryState k ℓ (α ⊕ β))
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₂ : genBoundarySubsetMatches W₂ (rightSub F).flags fun (b : β) => st (Sum.inr b))
{g : W₂.Flag}
(hbD : Sum.inr g ∈ F.boundaryFlags)
(hb : g ∈ (rightSub F).boundaryFlags)
:
The named colour of a right flag is the right half's.
theorem
RS.EdgeSubset.throughAgree_left
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
{k ℓ : ℕ}
(st : GenBoundaryState k ℓ (α ⊕ β))
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₁ : genBoundarySubsetMatches W₁ (leftSub F).flags fun (a : α) => st (Sum.inl a))
(hag : F.ThroughAgree st hbnd)
:
(leftSub F).ThroughAgree (fun (a : α) => st (Sum.inl a)) hbnd₁
Agreement restricts to the left half.
theorem
RS.EdgeSubset.throughAgree_right
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
{k ℓ : ℕ}
(st : GenBoundaryState k ℓ (α ⊕ β))
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₂ : genBoundarySubsetMatches W₂ (rightSub F).flags fun (b : β) => st (Sum.inr b))
(hag : F.ThroughAgree st hbnd)
:
(rightSub F).ThroughAgree (fun (b : β) => st (Sum.inr b)) hbnd₂
Agreement restricts to the right half.
theorem
RS.EdgeSubset.throughAgree_of_parts
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
{k ℓ : ℕ}
(st : GenBoundaryState k ℓ (α ⊕ β))
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₁ : genBoundarySubsetMatches W₁ (leftSub F).flags fun (a : α) => st (Sum.inl a))
(hbnd₂ : genBoundarySubsetMatches W₂ (rightSub F).flags fun (b : β) => st (Sum.inr b))
(hag₁ : (leftSub F).ThroughAgree (fun (a : α) => st (Sum.inl a)) hbnd₁)
(hag₂ : (rightSub F).ThroughAgree (fun (b : β) => st (Sum.inr b)) hbnd₂)
:
F.ThroughAgree st hbnd
Agreement on both halves is agreement.
theorem
RS.EdgeSubset.edgeSum_disjUnion
{α β : Type}
{W₁ : Fragment α}
{W₂ : Fragment β}
(F : EdgeSubset (W₁.disjUnion W₂))
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(st : GenBoundaryState k ℓ (α ⊕ β))
(hbnd : genBoundarySubsetMatches (W₁.disjUnion W₂) F.flags st)
(hbnd₁ : genBoundarySubsetMatches W₁ (leftSub F).flags fun (a : α) => st (Sum.inl a))
(hbnd₂ : genBoundarySubsetMatches W₂ (rightSub F).flags fun (b : β) => st (Sum.inr b))
{κ₁ : (leftSub F).RelTransitionSystem}
{κ₂ : (rightSub F).RelTransitionSystem}
(o₁ : κ₁.Orientation)
(o₂ : κ₂.Orientation)
:
RS21's colouring sum splits over a disjoint union.
RS21's sum under a relabel #
The composition's stages relabel the surviving interface, and the colouring sum does not see the labels beyond the boundary match.
theorem
RS.EdgeSubset.relabel_edgeOddBoundaryMatch_iff
{α β : Type}
{W : Fragment α}
(ee : α ≃ β)
(F : EdgeSubset W)
{k ℓ : ℕ}
(st : GenBoundaryState k ℓ β)
(φ : (relabelUp ee F).EdgeOddColouring ℓ)
:
The odd boundary constraint reindexes through the relabel.
def
RS.EdgeSubset.edgeOddRelabelEquiv
{α β : Type}
{W : Fragment α}
(ee : α ≃ β)
(F : EdgeSubset W)
(ℓ : ℕ)
:
The odd colourings are the same on both sides of a relabel: the flags and the pairing are untouched.
Equations
- RS.EdgeSubset.edgeOddRelabelEquiv ee F ℓ = Equiv.refl ((RS.EdgeSubset.relabelUp ee F).EdgeOddColouring ℓ)
Instances For
theorem
RS.EdgeSubset.core_relabel_eq
{α β : Type}
{W : Fragment α}
(ee : α ≃ β)
(F : EdgeSubset W)
{ℓ : ℕ}
(φ : (relabelUp ee F).EdgeOddColouring ℓ)
:
The core of a relabelled colouring is the relabelled core.
theorem
RS.EdgeSubset.relabel_edgeSum
{α β : Type}
{W : Fragment α}
(ee : α ≃ β)
(F : EdgeSubset W)
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(st : GenBoundaryState k ℓ β)
(hbnd : genBoundarySubsetMatches (W.relabel ee) (relabelUp ee F).flags st)
(hbnd' : genBoundarySubsetMatches W F.flags fun (a : α) => st (ee a))
{κ : F.RelTransitionSystem}
(o : κ.Orientation)
:
(relabelUp ee F).edgeSum h st hbnd (relabelOrientUp ee F o) = F.edgeSum h (fun (a : α) => st (ee a)) hbnd' o
RS21's colouring sum is untouched by a relabel.
noncomputable def
RS.EdgeSubset.relabelDataDown
{α' β' : Type}
[LinearOrder α']
[LinearOrder β']
(e : α' ≃o β')
{W' : Fragment α'}
(𝒟 : DataFamily (W'.relabel e.toEquiv))
:
DataFamily W'
The data family pulled back along a relabel.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
RS.EdgeSubset.edgeTermAt_relabel
{α' β' : Type}
[LinearOrder α']
[LinearOrder β']
(e : α' ≃o β')
{W' : Fragment α'}
{k ℓ : ℕ}
(h : MixedFunctional k ℓ)
(𝒟 : DataFamily (W'.relabel e.toEquiv))
(st : GenBoundaryState k ℓ β')
(s : Finset W'.Flag)
(C : ℕ)
:
RS21's summand is untouched by a relabel.