Closed-face vertex-cut adapter for row certificates

The generic degenerate vertex-cut theorem is stated for an arbitrary DegSpec whose representative map is known to encode contraction by its zero slots. Canonical closed faces use compFold, so that extra hypothesis is automatic. This small adapter presents the result in the exact form consumed by the deep-embedded closed-row checker.

theorem Utilities.Subdivision.ClosedRowProof.repIsContraction_censusSpec {n p : ℕ} (core : Certificate.ExplicitPotential.Core n p) (hn : 0 < n) (length : Fin p → ℕ) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (Certificate.ClosedFaceCensus.zeroSet length)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (Certificate.ClosedFaceCensus.zeroSet length)) : (Certificate.ClosedFaceCensus.censusSpec core hn length hForest hNotLoopy).RepIsContraction

A canonical census face identifies exactly the vertices joined by its zero-length slots.

theorem Utilities.Subdivision.ClosedRowProof.bnExists_censusSpec_of_genusFourRankOneCheck {n p : ℕ} (core : Certificate.ExplicitPotential.Core n p) (hn : 0 < n) (cut : Certificate.CoreVertexCut.Data core) (tree : MarkedGraphs.Certificate.SpanningTreeConnectivity.CertificateData core) (hLoopless : ∀ (e : Fin p), core.tail e ≠ core.head e) (hCheck : cut.genusFourRankOneCheck tree = true) (length : Fin p → ℕ) (hForest : Certificate.ContractionForestCensusGeneral.IsForest core (Certificate.ClosedFaceCensus.zeroSet length)) (hNotLoopy : ¬Certificate.ContractionForestCensusGeneral.IsLoopy core (Certificate.ClosedFaceCensus.zeroSet length)) : BNExists (Certificate.ClosedFaceCensus.censusSpec core hn length hForest hNotLoopy).graph 1 3

A checked genus-four core cut supplies a degree-three pencil on every genus-preserving canonical closed face.