Documentation

CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Differences

Edge differences and parity on actual face orbits #

Spins are functions on the original natural-number vertex names; edge differences retain listed edge positions. Face parity sums over darts, so an edge traversed twice cancels, while a singleton loop face counts its edge once. No bound on vertex names is used.

The permutation telescoping proof is an original reconstruction of the difference operation in [DK15], Section 3, printed pp. 439–440. The numerical genus predicate is distinct from geometric realization and from native compilation.

Main definitions #

source
def Cslib.Complexity.Graph.edgeGradient (G : Graph) (spin : ℕ → Bool) :
Fin G.edges.length → Bool

Boolean spin difference at each listed edge occurrence, including loops and parallels.

Instances For
    source
    theorem Cslib.Complexity.Graph.edgeGradient_dart (G : Graph) (spin : ℕ → Bool) (d : G.Dart) :
    G.edgeGradient spin d.1 = (spin d.vertex ^^ spin d.reverse.vertex)

    Reading a difference from either dart gives the same endpoint exclusive or.

    source
    theorem Cslib.Complexity.Graph.edgeGradient_not (G : Graph) (spin : ℕ → Bool) :
    (G.edgeGradient fun (v : ℕ) => !spin v) = G.edgeGradient spin

    Complementing all vertex spins leaves every edge difference unchanged.

    source
    noncomputable def Cslib.Complexity.Graph.RotationSystem.faceParity {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) (f : r.Face) :
    Bool

    Parity of the edge labels on all darts of one actual face. The two ends of an edge are separate summands, so repeated edge traversals have their proper multiplicity.

    Instances For
      source
      def Cslib.Complexity.Graph.RotationSystem.FaceEven {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) :
      Prop

      Every actual face orbit has even Boolean edge parity, including singleton orbits.

      Instances For
        source
        theorem Cslib.Complexity.Graph.RotationSystem.faceParity_mk {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) (d : G.Dart) :
        r.faceParity x ⟦d⟧ = parityOn {e : G.Dart | r.faceNext.SameCycle d e} fun (e : G.Dart) => x e.1

        Reading face parity from a dart uses exactly its permutation orbit.

        source
        theorem Cslib.Complexity.Graph.RotationSystem.faceEven_iff_dart {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) :
        r.FaceEven x ↔ ∀ (d : G.Dart), r.faceParity x ⟦d⟧ = false

        Quantifying over dart representatives covers every actual face, including fixed points.

        source
        theorem Cslib.Complexity.Graph.RotationSystem.faceParity_eq_sum_faceId {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) (d : G.Dart) :
        r.faceParity x ⟦d⟧ = ∑ e : G.Dart, if r.faceId e = r.faceId d then x e.1 else 0

        Canonical face IDs compute parity on the same actual orbit, with dart multiplicity.

        source
        theorem Cslib.Complexity.Graph.RotationSystem.faceParity_add {G : Graph} (r : G.RotationSystem) (x y : Fin G.edges.length → Bool) (f : r.Face) :
        r.faceParity (x + y) f = (r.faceParity x f ^^ r.faceParity y f)

        Face parity is additive in edge labels.

        source
        theorem Cslib.Complexity.Graph.RotationSystem.faceEven_edgeGradient {G : Graph} (r : G.RotationSystem) (spin : ℕ → Bool) :
        r.FaceEven (G.edgeGradient spin)

        Edge gradients telescope around any face, with no endpoint declaration or genus hypothesis.

        source
        theorem Cslib.Complexity.Graph.RotationSystem.FaceEven.add {G : Graph} (r : G.RotationSystem) {x y : Fin G.edges.length → Bool} (hx : r.FaceEven x) (hy : r.FaceEven y) :
        r.FaceEven (x + y)

        Face-even assignments are closed under exclusive-or addition.