Documentation

LeanPool.BrillNoetherGraphs.Utilities.Pseudocore.PseudocoreMarkerWedge

Wedge packages extracted from pseudocore loop markers #

A compatible split-loop marker is more than a local two-cycle: after an arbitrary positive subdivision of the split core it canonically exhibits the whole graph as a vertex wedge of a genus-one rigid factor and its complement. This file packages that length-uniform statement in the orientation used by the genus-five loop-aware normal-form interface: the complementary graph is the left (base) factor and the marker cycle is the right factor.

source
noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.data {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (_hCore : spec.core = split.splitCore) :
CoreVertexCut.Data spec.core

The marker-cut data, transported across a displayed equality of cores.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.data_eq_cut {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) :
    (data split spec marker hCore).glue = (PseudocoreMarkerCut.cut split marker).glue ∧ (data split spec marker hCore).left = (PseudocoreMarkerCut.cut split marker).left
    source
    theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.data_valid {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
    (data split spec marker hCore).Valid
    source
    theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.data_leftRigidConditions {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (hConnected : split.splitCore.Connected) :
    (data split spec marker hCore).LeftRigidConditions
    source
    noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.cut {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
    OneVertexCut spec.graph

    A marker package uses the complementary induced graph as base and the canonical marker cycle as rigid factor.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.base {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
      CFGraph

      The base graph remaining on the right side of the cut after separating the selected loop marker.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.factor {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
        CFGraph

        The left factor isolated by the selected loop-marker cut.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.attachment {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
          (base split spec marker hCore hCompatible).V

          The glue vertex in the base graph where the separated marker factor is attached.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.root {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
            (factor split spec marker hCore hCompatible).V

            The corresponding root vertex in the separated marker factor.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.wedgeIso {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
              CFGraphIso (vertexWedge (base split spec marker hCore hCompatible) (factor split spec marker hCore hCompatible) (attachment split spec marker hCore hCompatible) (root split spec marker hCore hCompatible)) spec.graph

              The wedge isomorphism in base-first orientation.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.factor_rigid {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (hConnected : split.splitCore.Connected) :
                PointedGenusOneRigid (factor split spec marker hCore hCompatible) (root split spec marker hCore hCompatible)
                source
                theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.base_connected {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (hConnected : split.splitCore.Connected) :
                graphConnected (base split spec marker hCore hCompatible)
                source
                theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.base_genus {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) :
                (base split spec marker hCore hCompatible).genus = spec.graph.genus - 1
                source
                noncomputable def Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.wedgeEquiv {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) {G : CFGraph} (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (presentation : LaplacianEquiv G spec.graph) :
                LaplacianEquiv G (vertexWedge (base split spec marker hCore hCompatible) (factor split spec marker hCore hCompatible) (attachment split spec marker hCore hCompatible) (root split spec marker hCore hCompatible))

                Compose a presentation of G by the split subdivision with the base-first marker wedge isomorphism.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.wedgeEquiv_apply_base {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) {G : CFGraph} (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (presentation : LaplacianEquiv G spec.graph) (z : G.V) (hz : presentation.toEquiv z ∈ (cut split spec marker hCore hCompatible).right) :
                  (wedgeEquiv split spec marker hCore hCompatible presentation).toEquiv z = Sum.inl ⟨presentation.toEquiv z, hz⟩

                  A target vertex on the complementary side is transported to the base summand of the base-first wedge.

                  source
                  theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.wedgeEquiv_apply_factor {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) {G : CFGraph} (marker : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (presentation : LaplacianEquiv G spec.graph) (z : G.V) (hz : presentation.toEquiv z ∈ (cut split spec marker hCore hCompatible).left) :
                  (wedgeEquiv split spec marker hCore hCompatible presentation).toEquiv z = wedgeRightVertex (base split spec marker hCore hCompatible) (factor split spec marker hCore hCompatible) (attachment split spec marker hCore hCompatible) (root split spec marker hCore hCompatible) ⟨presentation.toEquiv z, hz⟩

                  A target vertex on the marker side is transported to the corresponding vertex of the rigid factor in the base-first wedge.

                  source
                  theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.cut_left_subset_right_of_ne {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (first second : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (hNe : second ≠ first) :
                  (cut split spec second hCore hCompatible).left ⊆ (cut split spec first hCore hCompatible).right

                  The second of two distinct marker cuts restricts to the complementary factor of the first, uniformly in all positive subdivision lengths.

                  source
                  theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.restricted_second_factor_rigid {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (first second : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (hConnected : split.splitCore.Connected) (hNe : second ≠ first) :
                  have hSubset := ⋯; have restricted := (cut split spec first hCore hCompatible).restrictRight (cut split spec second hCore hCompatible) hSubset; PointedGenusOneRigid restricted.leftGraph restricted.leftGlue

                  After restricting a second distinct marker cut through the first, its left factor is still the same pointed rigid genus-one cycle.

                  source
                  theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.restricted_base_connected {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (first second : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (hConnected : split.splitCore.Connected) (hNe : second ≠ first) :
                  have hSubset := ⋯; have restricted := (cut split spec first hCore hCompatible).restrictRight (cut split spec second hCore hCompatible) hSubset; graphConnected restricted.rightGraph

                  The residual base after two distinct marker cuts is connected.

                  source
                  theorem Utilities.Certificate.PseudocoreMarkerWedge.MarkerPackage.restricted_base_genus_three {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (first second : Fin core.loopCount) (hCore : spec.core = split.splitCore) (hCompatible : PseudocoreSplitGlue.Compatible split) (hConnected : split.splitCore.Connected) (hNe : second ≠ first) (hGenus : spec.graph.genus = 5) :
                  have hSubset := ⋯; have restricted := (cut split spec first hCore hCompatible).restrictRight (cut split spec second hCore hCompatible) hSubset; restricted.rightGraph.genus = 3

                  In a genus-five presentation, removing two distinct marker cycles leaves a genus-three residual base.