Graph properties of compatible pseudocore subdivisions

The lightweight PseudocoreSplitGlue.Compatible predicate omits displayed core connectedness on purpose. Together with validity of the underlying pseudocore, however, it determines all graph-theoretic properties needed by the low-genus normalizers: connectedness, genus, and leaflessness of every positive subdivision.

theorem Utilities.Certificate.PseudocoreSubdivisionProperties.slotValence_baseVertex {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (hCompatible : PseudocoreSplitGlue.Compatible split) (vertex : Fin n) : PseudocorePresentation.slotValence split.splitCore (core.baseVertex vertex) = core.valence vertex

Original base vertices retain their loop-aware pseudocore valence after semantic loops are displayed as two-edge marker cycles.

theorem Utilities.Certificate.PseudocoreSubdivisionProperties.slotValence_markerVertex {n : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (hCompatible : PseudocoreSplitGlue.Compatible split) (marker : Fin core.loopCount) : PseudocorePresentation.slotValence split.splitCore (core.markerVertex marker) = 2

Every displayed semantic-loop marker has the two incident slot ends of its marker cycle.

theorem Utilities.Certificate.PseudocoreSubdivisionProperties.two_le_slotValence {n g : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (hValid : core.ValidAt g) (hCompatible : PseudocoreSplitGlue.Compatible split) (vertex : Fin (n + core.loopCount)) : 2 ≤ PseudocorePresentation.slotValence split.splitCore vertex

Every displayed core vertex has valence at least two; base vertices in fact have valence at least three and marker vertices exactly two.

theorem Utilities.Certificate.PseudocoreSubdivisionProperties.graphConnected {n g : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (hValid : core.ValidAt g) (hCompatible : PseudocoreSplitGlue.Compatible split) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (hCore : spec.core = split.splitCore) : _root_.graphConnected spec.graph

Every positive subdivision of a valid compatible pseudocore split is connected.

theorem Utilities.Certificate.PseudocoreSubdivisionProperties.genus_eq {n g : ℕ} {core : GenusFourPseudocore.Pseudocore n} (hValid : core.ValidAt g) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) : spec.graph.genus = ↑g

Every positive subdivision has the genus certified by the underlying pseudocore.

theorem Utilities.Certificate.PseudocoreSubdivisionProperties.leafless {n g : ℕ} {core : GenusFourPseudocore.Pseudocore n} (split : core.SplitMetadata) (hValid : core.ValidAt g) (hCompatible : PseudocoreSplitGlue.Compatible split) (spec : SubdivisionGraph.Spec (n + core.loopCount) core.splitEdgeCount) (hCore : spec.core = split.splitCore) (vertex : spec.graph.V) : vertexDegree spec.graph vertex ≠ 1

Every positive subdivision of a stable compatible pseudocore split is leafless. Interior subdivision vertices have degree two; displayed core vertices have degree at least two by two_le_slotValence.