Marker-loop cuts of compatible pseudocore splits

Each marker introduced by loop splitting is joined only to its designated base vertex, by two parallel slot occurrences. The two vertices therefore form a canonical genus-one side of a core vertex cut.

def Utilities.Certificate.PseudocoreMarkerCut.nonloopValence {n : ℕ} (core : GenusFourPseudocore.Pseudocore n) (vertex : Fin n) : ℕ

Nonloop incidence degree at a pseudocore vertex.

Equations

• Utilities.Certificate.PseudocoreMarkerCut.nonloopValence core vertex = ∑ neighbor : Fin n, core.multiplicity vertex neighbor

theorem Utilities.Certificate.PseudocoreMarkerCut.splitCore_incidenceDegree_baseVertex {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (vertex : Fin n) (hCompatible : PseudocoreSplitGlue.Compatible split) : split.splitCore.incidenceDegree (core.baseVertex vertex) = core.valence vertex

The incidence degree of an original vertex in a compatible loopless split core is its loop-aware pseudocore valence.

theorem Utilities.Certificate.PseudocoreMarkerCut.loops_markerBase_pos {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) : 0 < core.loops (split.markerBase marker)

A displayed marker certifies a positive semantic-loop multiplicity at its base vertex.

theorem Utilities.Certificate.PseudocoreMarkerCut.loops_markerBase_eq_one_of_loopCount_eq_one {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) (hLoopCount : core.loopCount = 1) : core.loops (split.markerBase marker) = 1

If the pseudocore has only one semantic loop in total, every displayed marker is based at a vertex carrying exactly that one loop.

theorem Utilities.Certificate.PseudocoreMarkerCut.nonloopValence_markerBase_pos_of_loopCount_eq_one {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) {g : ℕ} (marker : Fin core.loopCount) (hValid : core.ValidAt g) (hCompatible : PseudocoreSplitGlue.Compatible split) (hLoopCount : core.loopCount = 1) : 0 < nonloopValence core (split.markerBase marker)

Stability forces the base of a unique semantic loop to have at least one nonloop exit.

theorem Utilities.Certificate.PseudocoreMarkerCut.nonloopValence_markerBase_eq_one_or_ge_two {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) {g : ℕ} (marker : Fin core.loopCount) (hValid : core.ValidAt g) (hCompatible : PseudocoreSplitGlue.Compatible split) (hLoopCount : core.loopCount = 1) : nonloopValence core (split.markerBase marker) = 1 ∨ 2 ≤ nonloopValence core (split.markerBase marker)

The exact single-loop structural dichotomy: its base has one nonloop incidence (the separating-bridge case), or at least two (the wedge case).

def Utilities.Certificate.PseudocoreMarkerCut.cut {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) : CoreVertexCut.Data split.splitCore

The canonical two-vertex cut side for one split-loop marker.

Equations

• Utilities.Certificate.PseudocoreMarkerCut.cut split marker = { glue := core.baseVertex (split.markerBase marker), left := {core.baseVertex (split.markerBase marker), core.markerVertex marker} }

theorem Utilities.Certificate.PseudocoreMarkerCut.baseVertex_ne_markerVertex_any {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (base : Fin n) (marker : Fin core.loopCount) : core.baseVertex base ≠ core.markerVertex marker

Base and marker vertices lie in the two disjoint summands of the split core's vertex type.

theorem Utilities.Certificate.PseudocoreMarkerCut.baseVertex_injective {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} : Function.Injective core.baseVertex

theorem Utilities.Certificate.PseudocoreMarkerCut.markerVertex_injective {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} : Function.Injective core.markerVertex

theorem Utilities.Certificate.PseudocoreMarkerCut.baseVertex_ne_markerVertex {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) : core.baseVertex (split.markerBase marker) ≠ core.markerVertex marker

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_left_card {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) : (cut split marker).left.card = 2

theorem Utilities.Certificate.PseudocoreMarkerCut.marker_pairMultiplicity {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) : split.splitCore.pairMultiplicity (core.baseVertex (split.markerBase marker)) (core.markerVertex marker) = 2

theorem Utilities.Certificate.PseudocoreMarkerCut.leftSlots_eq_markerPair {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) : (cut split marker).leftSlots = {edge : Fin core.splitEdgeCount | split.splitCore.tail edge = core.baseVertex (split.markerBase marker) ∧ split.splitCore.head edge = core.markerVertex marker ∨ split.splitCore.tail edge = core.markerVertex marker ∧ split.splitCore.head edge = core.baseVertex (split.markerBase marker)}

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_leftSlotCount {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) : (cut split marker).leftSlotCount = 2

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_leftGenus {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) : (cut split marker).leftGenus = 1

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_leftTwoRegular {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) : (cut split marker).LeftTwoRegular

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_valid {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) : (cut split marker).Valid

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_leftRigidConditions {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) (hConnected : split.splitCore.Connected) : (cut split marker).LeftRigidConditions

The marker side is a rigid genus-one left factor whenever the split core is connected.

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_leftRigidConditions_of_presentation {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (marker : Fin core.loopCount) (hCompatible : PseudocoreSplitGlue.Compatible split) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (hCore : spec.core = split.splitCore) (hConnected : graphConnected spec.graph) : (cut split marker).LeftRigidConditions

A connected subdivision presentation supplies the split-core connectedness needed by the canonical marker rigidity theorem. This is the form produced directly by pseudocorePresentation_genusFive.

theorem Utilities.Certificate.PseudocoreMarkerCut.cut_left_subset_right_of_ne {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (first second : Fin core.loopCount) (hNe : second ≠ first) : (cut split second).left ⊆ (cut split first).right

Distinct loop-marker sides are nested in the expected way: after cutting off one marker cycle, the entire two-vertex side of any other marker remains in the complementary factor. The two marker cycles may share their base vertex; that common vertex is precisely the first cut's glue.