WP-A: the pseudocore presentation theorem #
This module builds, for an arbitrary connected leafless graph, a subdivision
presentation over a small core: one in which every core vertex either has
core valence at least three, or is a bivalent marker whose two slots run to a
common neighbour. That shape is exactly the loopless split of a loop-aware
pseudocore, which is what Certificate/PseudocoreSplitGlue.lean consumes.
The construction is genus-generic. Its engine is a single merge step at the level of subdivision specifications:
mergeSpec— given a specification with a core vertex carrying exactly two slot ends whose far endpoints are distinct, produce a specification with one fewer core vertex and one fewer slot, presenting the same graph;exists_reduced— iterate the merge step until no core vertex is mergeable.
Both are proved by exhibiting the larger specification as a
SubdivisionGraph.Spec.Relabeling of the canonical one-slot split
(OneEdgeSplitRefinement.splitSpec) of the smaller one, so no new
vertex/unit-step bijection has to be built by hand: the split's own
canonicalSplitLaplacianEquiv supplies it.
A total left inverse of Fin.castSucc, defaulting to 0.
Equations
Instances For
Slot ends at a core vertex #
The set of slot ends at a core vertex. (edge, true) is the head end of
edge and (edge, false) its tail end.
Equations
Instances For
Core valence: the number of slot ends at a core vertex.
Equations
- Utilities.Certificate.PseudocorePresentation.slotValence core vertex = (Utilities.Certificate.PseudocorePresentation.slotEnds core vertex).card
Instances For
The merge step #
Witness that a core vertex carries exactly two slot ends, lying on two distinct slots whose far endpoints differ. Such a vertex is a genuine subdivision point and can be suppressed.
- vertex : Fin n
The degree-two core vertex to suppress by merging its two incident slots.
The first incident slot end at the suppressed vertex, including its orientation flag.
The second incident slot end; its slot differs from the first and together they exhaust the incident ends.
Instances For
Suppressing a bivalent core vertex preserves the subdivided graph. The smaller specification is obtained by concatenating the two slots at the vertex; the equality of graphs is read off from the canonical one-slot split of the smaller specification.
Iterating the merge step #
A core is reduced when no vertex of it can be suppressed.
Equations
Instances For
Every subdivision specification presents its graph over a reduced core.
Valence of a core vertex inside the subdivided graph #
Handshake at the core: every slot has two ends.
Slots incident to a vertex, counted without their orientation.
Reading off the shape of a reduced core #
In a reduced loopless core, a vertex with exactly two slot ends carries them on two distinct slots running to one common neighbour.
Core connectedness from graph connectedness #
The side of a vertex cut of the core that a subdivision vertex lies on: core vertices by themselves, interior vertices by the tail of their slot.
Equations
Instances For
Cut connectedness of the subdivided graph implies cut connectedness of the
core. This is the converse of graph_connected_of_coreConnected.
Unordered multiplicities of a core #
Total unordered multiplicity at a vertex is its slot valence.
The shape of a reduced core #
A core presented as the loopless split of a loop-aware pseudocore: every vertex is either stable, or a marker carrying exactly two slots to a single stable partner.
The Boolean designation of loop markers, distinguishing them from stable base vertices.
The stable base partner of each marker, joined to it by exactly two edge occurrences and its only neighbor.
Instances For
Building the marked shape of a reduced core #
In a reduced core, a vertex with exactly two slot ends has all of its slots running to one common neighbour.
Two adjacent bivalent vertices would exhaust the graph, which has genus one.
Shape of a reduced presentation. Every vertex of a reduced core is either stable or a bivalent marker attached to a single stable base.
The genus-four specialization of exists_markedShapeAt.
Encoding a marked shape as a pseudocore with split metadata #
The pseudocore encoding. A marked-shape presentation of a connected
genus-g graph is the loopless split of a valid pseudocore on at most
2 * (g - 1) vertices.
The genus-four specialization of
pseudocorePresentation_of_markedShapeAt.
Every connected leafless graph of genus at least two is
Laplacian-equivalent to a positive subdivision of the loopless split of a
valid pseudocore on at most 2(g-1) base vertices.
Every connected leafless genus-five graph is Laplacian-equivalent to a positive subdivision of the loopless split of a valid genus-five pseudocore on at most eight vertices.