Core vertex cuts on the CLOSED length orthant #
Certificate/CoreVertexCutGenusFour.lean proves
bnExists_one_three_of_genusFourRankOneCheck against a
SubdivisionGraph.Spec, hence only at strictly positive lengths. The
contraction bridge (the corresponding closed-row proof module,
the corresponding closed-row proof module) consumes the closed-orthant shape
∀ ℓ, IsForest … → ¬ IsLoopy … → BNExists (censusSpec … ℓ …).graph 1 3.
This module supplies the closed statement for the vertex-cut route.
Why this port is possible where the mixed-cover port is not #
Certificate/ClosedRowInterface.lean records that the generated mixed-cover
corpus cannot move onto the closed layer: each of its pieces outputs a
SubdivisionGraph.Spec, whose length_pos is a structural field, so a
piece cannot even be constructed at a face. The vertex-cut certificate is a
different object: CoreVertexCut.Data core is proof-free data on the core
(glue : Fin n, left : Finset (Fin n)), with no length information at all,
and Valid is a statement about core slots only. There is no field to
construct at a face, so no structural obstruction.
What is genuinely length-dependent is the arithmetic:
CoreVertexCutGenus.leftGraph_genus uses spec.length_pos to turn
length e - 1 + 1 back into length e. At a face a vanishing left slot
loses an edge and merges two left vertices, so the factor genus is preserved
— but only because the vanishing set is a forest. That is the mathematical
content of this file, and it is a theorem, not an assumption.
The route: contract, do not re-derive #
We do not re-port the 437 lines of CoreVertexCut.lean to DegSpec
vertex types. Certificate/DegenerateSeparator.lean already builds
DegSpec.contractedSpec, a genuinely positive SubdivisionGraph.Spec on the
contracted core, together with DegSpec.canonicalContraction, whose
laplacianEquiv identifies its graph with d.graph. So it suffices to push
the finite core data CoreVertexCut.Data d.core forward to
CoreVertexCut.Data d.contractedCore and check that Valid, the factor
genera and the two-regularity conditions survive. Everything below is finite
combinatorics on cores; no subdivision vertex type is ever touched.
The one hypothesis a bare DegSpec does not supply #
DegSpec.rep is only required to identify the endpoints of vanishing slots
(rep_zero); nothing forces its classes to be generated by them. Without
that, a rep could merge a left class into a right class across no edge at
all, and no cut could survive. DegSpec.RepIsContraction below is exactly
the missing direction, and it is free for every object a row actually uses:
censusSpec's rep is compFold, for which compFold_iff is precisely this
statement.
Looplessness #
Two different looplessness facts are in play and both are discharged, not assumed away:
- the contracted core is loopless — supplied by
DegSpec.rep_loopless, which oncensusSpeccomes from the census hypothesis¬ IsLoopy. This is theRESULTS.md§9 hazard: core vertices are not rank-determining on a loop-carrying core. It enters here throughcontractedSpec.core_loopless. - the uncontracted core is loopless — needed to know that no core slot lies
in both sides at once (
leftSlots_disjoint_rightSlots). ADegSpecdoes not imply it (a vanishing slot could be a loop), so it is carried as an explicit hypothesishLoopless, exactly asSubdivisionGraph.Speccarries it as the fieldcore_loopless; on a concrete row core it isby decide.
zeroSlotSet, forest', RepIsContraction and rep_eq_of_reachIn moved
down to Utilities/Subdivision/DegenerateRepRigidity.lean on 2026-08-25, where
the forest-face rigidity statements need them.
Generic reachability monotonicity #
This extends the census namespace, which lives in the public Utilities
library, so the block is opened absolutely rather than relative to the private
MarkedGraphs.Certificate namespace below.
The cut, transported to a face #
Vanishing slots lying wholly in the named side.
Equations
Instances For
Vanishing slots lying wholly in the complementary side.
Equations
Instances For
The vertex identification produced by the vanishing slots of the named side alone.
Equations
Instances For
The vertex identification produced by the vanishing slots of the complementary side alone.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Confinement of reachability to one side #
A left-vanishing-slot walk out of the named side stays in it.
A right-vanishing-slot walk out of the complementary side stays in it.
The confinement lemma. A vanishing-slot walk starting inside the
named side either never leaves it, or has already reached the articulation
inside it. This is the whole reason a cut survives contraction: the only way
out of a side is through glue.
The complementary confinement lemma.
Side-local representatives #
Side stability: a class off the articulation lies wholly on one side #
Side stability. If a class does not contain the articulation, its members all lie on the same side of the cut. This is the fact that makes the push-forward of a cut along a contraction well defined.
Fibre equality. On the named side the global classes and the side-local classes agree: a walk between two left vertices can be rerouted through left slots only.
The rank inequality on each side #
The two sides exhaust, and the inequalities are tight #
The face-restricted forest count on the named side. This is the
identity that replaces spec.length_pos in the genus calculation: a vanishing
left slot removes exactly one left vertex class.
The push-forward of the cut to the contracted core #
The uncontracted core vertex naming a contracted class.
Equations
Instances For
The uncontracted slot naming a surviving slot.
Equations
Instances For
The push-forward cut. A contracted class is on the named side exactly when it contains a named-side vertex. Off the articulation class that is unambiguous, by side stability.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership of a class in the named side, read on the uncontracted core.
Validity of the push-forward #
The two counts #
A surviving slot is wholly on the named side after contraction exactly
when it already was before. The forward direction is where
DegSpec.rep_loopless — hence the census hypothesis ¬ IsLoopy — is used.
The surviving named slots, read on the uncontracted core, are exactly the named slots that do not vanish.
Genus is preserved #
The named factor genus is preserved at every forest face. This is the
theorem that replaces SubdivisionGraph.Spec.length_pos in
CoreVertexCutGenus.leftGraph_genus: a vanishing left slot removes one left
slot and one left vertex class, so the difference is unchanged.
The complementary factor genus is preserved too — by genus additivity on both cores, so no second counting argument is needed.
Two-regularity, the rigidity half of the (3,1) branch #
GenusFourRankOneAlternatives conjoins RightTwoRegular with
rightGenus = 1 for a reason: PointedGenusOneRigid is what the (3,1) wedge
theorem consumes, and genus one alone does not supply it. So the push-forward
has to carry two-regularity, not just the genus.
The count is: a contracted class k of the complementary side has retained
degree 2 · #(k ∩ right) - 2 · #(vanishing right slots inside k), because each
collapsed slot destroys exactly two incidences. That is 2 exactly when the
class carries one fewer collapsed slot than vertices — the per-class form of
card_right_eq, which the global identity forces once each class satisfies the
matroid inequality separately.
The members of one contracted class on the complementary side.
Equations
- Utilities.Certificate.DegenerateCoreVertexCut.rightFibre d cut k = {v ∈ cut.right | d.rep v = k}
Instances For
The vanishing complementary slots inside one contracted class.
Equations
- Utilities.Certificate.DegenerateCoreVertexCut.rightFibreSlots d cut k = {e ∈ Utilities.Certificate.DegenerateCoreVertexCut.rightZero d cut | d.rep (d.core.tail e) = k}
Instances For
The members of one contracted class on the named side.
Equations
- Utilities.Certificate.DegenerateCoreVertexCut.leftFibre d cut k = {v ∈ cut.left | d.rep v = k}
Instances For
The vanishing named slots inside one contracted class.
Equations
- Utilities.Certificate.DegenerateCoreVertexCut.leftFibreSlots d cut k = {e ∈ Utilities.Certificate.DegenerateCoreVertexCut.leftZero d cut | d.rep (d.core.tail e) = k}
Instances For
The contracted class is constant along a vanishing-slot walk.
A vanishing-slot walk between two vertices of one contracted class uses only slots of that class, so the walk survives restriction to the fibre.
The left twin of reachIn_rightFibreSlots_of_reachIn.
Fibre bookkeeping #
Both endpoints of a vanishing complementary slot of class k lie in the
fibre of k: the slot lies wholly on the complementary side, and vanishing
makes its two endpoints share a class.
A walk through the slots of one class cannot start outside that class.
The whole fibre is one class of its own slot set. This is what
reachIn_rightFibreSlots_of_reachIn buys: the walk joining two members of a
class can be rerouted through the slots of that class alone.
The per-class matroid inequality. The whole fibre collapses to a
single class of its own slot set, which off the fibre is the identity, so the
graphic-matroid rank bound applied to rightFibreSlots k alone reads
#(rightFibre k) ≤ #(rightFibreSlots k) + 1.
Per-class tightness on the complementary side. Each class satisfies
the matroid inequality card_rightFibre_le separately; the fibres partition
cut.right and the fibre slot sets partition rightZero, so summing those
inequalities over the classes reproduces the already-proved global identity
card_right_eq. A sum of ≤s that meets its bound is termwise tight.
Per-class tightness on the named side; the mirror of
card_rightFibre_eq.
Regrouping incidences by contracted class #
Generic incidence regrouping. For a slot set S all of whose slots
have both endpoints in a vertex set V, the incidences of the surviving
slots of S at one contracted class k are the incidences of all of S at
the members of that class, less the two incidences that each vanishing slot of
the class contributes to it.
The complementary-side instance of sum_incidence_class.
The named-side instance of sum_incidence_class.
The complementary side of the push-forward, read on the core #
A contracted class on the complementary side of the push-forward is the class of an uncontracted complementary vertex.
The mirror of contractedCut_leftSlot_iff, obtained from it by the
side dichotomy on both cores.
The contracted incident degree, transported back to the uncontracted core: it counts the surviving complementary slots incident to the class.
Two-regularity of the complementary side survives contraction.
For a class k' of right', the sum defining rightIncidentDegree'
transports back along slotOf/classVal to the surviving complementary slots
incident to the class, and regrouping by the fibre gives
rightIncidentDegree' k'
= ∑_{v ∈ rightFibre k} rightIncidentDegree v − 2 · #(rightFibreSlots k)
= 2 · #(rightFibre k) − 2 · #(rightFibreSlots k) [by `hReg`]
= 2 [by `card_rightFibre_eq`].
Two-regularity of the named side survives contraction. The mirror of
contractedCut_rightTwoRegular.
The closed-orthant conclusion #
The closed-orthant genus-four vertex-cut theorem.
Same hypotheses as CoreVertexCut.Data.bnExists_one_three_of_genusFourRankOneConditions
— a valid cut on a connected core with admissible factor genera — but the
conclusion holds on the whole closed length orthant: at every face where the
vanishing set is a forest whose contraction leaves no loop, not only at
strictly positive lengths.
The (2,2) branch, with no two-regularity obligation. Stated
separately rather than as a corollary of the theorem above, because the
three-way rcases in contractedCut_alternatives puts all three branches in
the proof term, so while the two-regularity transfer was still deferred a
(2,2) row routed through the general theorem inherited the (3,1) branch's
sorry. Both routes are now sorry-free; this one is kept because it is
also the cheaper proof term.
Checker-facing form: the same finite genusFourRankOneCheck that the
open-orthant corpus already runs, now concluding on the closed orthant.