Documentation

LeanPool.RegtsSevenster.RS.Novel.Skein.ClosedAgreement

Closed-fragment agreement: throughMixedPartitionAt = mixedPartition #

For a closed fragment (Fragment (Fin 0)), every quantifier ∀ i : Fin 0, ... is vacuously true. This makes the through-edge corrections trivial — there are no boundary flags, so throughFlags = ∅, coreFlags = flags, throughProduct = 1, and the boundary-match conditions all hold vacuously. The corrected constrained partition value therefore equals the unconstrained Definition 5 value.

This is the base case of the converse's factorization induction.

Vacuous boundary conditions on closed fragments #

source
theorem RS.EdgeSubset.allInternal_of_closed {W : ClosedFragment} (F : EdgeSubset W) :
F.allInternal

On a closed fragment, no flag is boundary-attached.

source
theorem RS.EdgeSubset.coreFlags_eq_flags {W : ClosedFragment} (F : EdgeSubset W) :
F.coreFlags = F.flags

On a closed fragment, the core flags equal the full flags.

source
theorem RS.EdgeSubset.throughProduct_one {W : ClosedFragment} [LinearOrder (Fin 0)] (F : EdgeSubset W) {k ℓ : ℕ} (st : GenBoundaryState k ℓ (Fin 0)) :
F.throughProduct st = 1

On a closed fragment, the through product is 1: each through-flag's factor is 1 because W.attach f always lands in Sum.inl.

source
theorem RS.genEvenBoundaryMatch_closed {W : ClosedFragment} (F : EdgeSubset W) {k ℓ : ℕ} (st : GenBoundaryState k ℓ (Fin 0)) (hbnd : genBoundarySubsetMatches W F.flags st) (ψ : F.EvenColouring k) :
genEvenBoundaryMatch F st hbnd ψ

On a closed fragment, every even colouring satisfies the even boundary match.

source
theorem RS.EdgeSubset.coreOddBoundaryMatch_closed {W : ClosedFragment} (F : EdgeSubset W) {k ℓ : ℕ} (st : GenBoundaryState k ℓ (Fin 0)) (φ : F.CoreOddColouring ℓ) :
F.coreOddBoundaryMatch st φ

On a closed fragment, every core odd colouring satisfies the core odd boundary match.

The colouring equivalence #

source
noncomputable def RS.EdgeSubset.coreOddEquiv {W : ClosedFragment} (F : EdgeSubset W) (ℓ : ℕ) :
F.CoreOddColouring ℓ ≃ F.OddColouring ℓ

On a closed fragment, the core odd colouring type is equivalent to the full odd colouring type, via coreFlags = flags.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    Vertex-local data agreement #

    source
    theorem RS.EdgeSubset.coreOddPairFn_eq {W : ClosedFragment} (F : EdgeSubset W) {ℓ : ℕ} (κ : F.TransitionSystem) (φ_core : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) :
    F.coreOddPairFn κ.toRelTransitionSystem φ_core f = F.oddPairFn κ ((F.coreOddEquiv ℓ) φ_core) ⟨↑f, ⋯⟩

    On a closed fragment, coreOddPairFn at φ_core agrees with oddPairFn at coreOddEquiv φ_core.

    source
    theorem RS.EdgeSubset.coreOddSignFn_eq {W : ClosedFragment} (F : EdgeSubset W) {ℓ : ℕ} (κ : F.TransitionSystem) (φ_core : F.CoreOddColouring ℓ) (f : ↥F.internalFlags) :
    F.coreOddSignFn κ.toRelTransitionSystem φ_core f = F.oddSignFn κ ((F.coreOddEquiv ℓ) φ_core) ⟨↑f, ⋯⟩

    On a closed fragment, coreOddSignFn at φ_core agrees with oddSignFn at coreOddEquiv φ_core.

    source
    theorem RS.EdgeSubset.coreOddListAt_eq {W : ClosedFragment} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ_core : F.CoreOddColouring ℓ) (v : W.Vertex) :
    F.coreOddListAt o.toRel φ_core v = F.oddListAt o ((F.coreOddEquiv ℓ) φ_core) v

    On a closed fragment, coreOddListAt at φ_core agrees with oddListAt at coreOddEquiv φ_core.

    source
    theorem RS.EdgeSubset.coreOddSignAt_eq {W : ClosedFragment} (F : EdgeSubset W) {ℓ : ℕ} {κ : F.TransitionSystem} (o : κ.Orientation) (φ_core : F.CoreOddColouring ℓ) (v : W.Vertex) :
    F.coreOddSignAt o.toRel φ_core v = F.oddSignAt o ((F.coreOddEquiv ℓ) φ_core) v

    On a closed fragment, coreOddSignAt at φ_core agrees with oddSignAt at coreOddEquiv φ_core.

    Circuit count agreement #

    source
    theorem RS.EdgeSubset.openCircuitCount_eq_circuitCount {W : ClosedFragment} (F : EdgeSubset W) (κ : F.TransitionSystem) :
    κ.toRelTransitionSystem.openCircuitCount = κ.circuitCount

    On a closed fragment, the open circuit count of the relative transition system equals the standard circuit count.

    The per-subset summand agreement #

    source
    theorem RS.EdgeSubset.throughSummand_eq_mixedSummand {W : ClosedFragment} [LinearOrder (Fin 0)] (F : EdgeSubset W) {k ℓ : ℕ} (h : MixedFunctional k ℓ) (st : GenBoundaryState k ℓ (Fin 0)) (hbnd : genBoundarySubsetMatches W F.flags st) {κ : F.TransitionSystem} (o : κ.Orientation) :
    F.throughSummand h st hbnd o.toRel κ.toRelTransitionSystem.openCircuitCount = F.mixedSummand h o

    On a closed fragment, the through summand at an Eulerian subset equals the standard mixed summand.