A closed-orthant row proof implies every contraction of its row

the corresponding closed-row proof module moves a (domain closed) row proof down to the same core's open-orthant obligation, by observing that a strictly positive length vector has empty vanishing set. This file makes the other, larger move: the closed orthant of a core C also contains, as a face, the whole closed orthant of every equal-genus contraction C / F.

Concretely, let F be a slot set of C which is a forest and whose contraction leaves no loop, and let C' be the contracted core. Send a length vector ℓ' of C' to the length vector of C that is ℓ' on the surviving slots and 0 on F. Its vanishing set is exactly F, so a closed row proof of C applies there, and Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.laplacianEquiv identifies the resulting degenerate graph with the honest subdivision of C'.

So one closed-orthant row proof discharges the open-orthant obligation of its core and of every core below it in the contraction order.

What the data has to supply, and why orientation is a real constraint

DegenerateSpec.Contraction matches slots with their orientation: it asks for vtx (C'.tail e') = rep (C.tail (slot e')), not for the unordered pair. Slot reversal is deliberately not part of that structure — it is supplied separately by SubdivisionGraph.Spec.Relabeling. ContractionData below inherits that restriction, so it witnesses only orientation-exact contractions. A contraction that needs a slot flipped has to be composed with a Relabeling; that composition is not built here.

Where this does not reach

Contracting a slot of a split loop (a bivalent marker w carrying two parallel slots to its base v) is never admissible: contracting one of the pair identifies v with w, so the other becomes a loop and IsLoopy holds; contracting both is not a forest. The number of split loops is therefore constant along every face reachable this way, and a loop-carrying row is never a face of a loopless one. See the corresponding closed-row proof module.

theorem Utilities.Certificate.ClosedContraction.core_ext {m q : ℕ} {a b : ExplicitPotential.Core m q} (ht : a.tail = b.tail) (hh : a.head = b.head) : a = b

A core is its two endpoint maps. Used by the RowNNNFromRowMMM files to check, rather than assume, that the core they write out by hand is the one the catalog names.

structure Utilities.Certificate.ClosedContraction.ContractionData {n p n' p' : ℕ} (core : ExplicitPotential.Core n p) (core' : ExplicitPotential.Core n' p') : Type

Data exhibiting core' as the contraction of core along the slot set F, orientation included. Every field is decidable on concrete cores, so an instance is built by decide.

• F : Finset (Fin p)

  The contracted slot set.

• vtx : Fin n' → Fin n

  Which vertex of core represents each vertex of core'.

• slot : Fin p' → Fin p

  Which slot of core each slot of core' is.

• isForest : ContractionForestCensusGeneral.IsForest core self.F

  Contracting F preserves the genus.

• notLoopy : ¬ContractionForestCensusGeneral.IsLoopy core self.F

  Contracting F leaves no loop.

• slot_inj : Function.Injective self.slot
• slot_notMem (e' : Fin p') : self.slot e' ∉ self.F
• slot_surj (e : Fin p) : e ∉ self.F → ∃ (e' : Fin p'), self.slot e' = e
• vtx_inj : Function.Injective self.vtx
• vtx_rep (v' : Fin n') : ContractionForestCensusGeneral.compFold core self.F (self.vtx v') = self.vtx v'
• vtx_surj (v : Fin n) : ∃ (v' : Fin n'), self.vtx v' = ContractionForestCensusGeneral.compFold core self.F v
• tail_eq (e' : Fin p') : self.vtx (core'.tail e') = ContractionForestCensusGeneral.compFold core self.F (core.tail (self.slot e'))
• head_eq (e' : Fin p') : self.vtx (core'.head e') = ContractionForestCensusGeneral.compFold core self.F (core.head (self.slot e'))

def Utilities.Certificate.ClosedContraction.ContractionData.lift {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') (e : Fin p) : ℕ

The length vector of core which is s.length on the surviving slots and 0 on F.

Equations

• c.lift s e = ∑ e' : Fin p', if c.slot e' = e then s.length e' else 0

theorem Utilities.Certificate.ClosedContraction.ContractionData.lift_slot {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') (e' : Fin p') : c.lift s (c.slot e') = s.length e'

theorem Utilities.Certificate.ClosedContraction.ContractionData.lift_of_mem {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') {e : Fin p} (he : e ∈ c.F) : c.lift s e = 0

theorem Utilities.Certificate.ClosedContraction.ContractionData.zeroSet_lift {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') : ClosedFaceCensus.zeroSet (c.lift s) = c.F

theorem Utilities.Certificate.ClosedContraction.ContractionData.isForest_lift {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') : ContractionForestCensusGeneral.IsForest core (ClosedFaceCensus.zeroSet (c.lift s))

theorem Utilities.Certificate.ClosedContraction.ContractionData.notLoopy_lift {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') : ¬ContractionForestCensusGeneral.IsLoopy core (ClosedFaceCensus.zeroSet (c.lift s))

theorem Utilities.Certificate.ClosedContraction.ContractionData.rep_censusSpec {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') (hn : 0 < n) : (ClosedFaceCensus.censusSpec core hn (c.lift s) ⋯ ⋯).rep = ContractionForestCensusGeneral.compFold core c.F

def Utilities.Certificate.ClosedContraction.ContractionData.contraction {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') (hn : 0 < n) (hcore : s.core = core') : (ClosedFaceCensus.censusSpec core hn (c.lift s) ⋯ ⋯).Contraction s

The face {ℓ = 0 on F} of the closed orthant of core, matched with the honest subdivision of the contracted core core'.

Equations

• c.contraction s hn hcore = { vtx := c.vtx, vtx_rep := ⋯, vtx_inj := ⋯, vtx_surj := ⋯, slot := c.slot, slot_inj := ⋯, slot_surj := ⋯, length_eq := ⋯, tail_eq := ⋯, head_eq := ⋯ }

theorem Utilities.Certificate.ClosedContraction.bnExists_spec_of_closed_contraction {n p n' p' : ℕ} (core : ExplicitPotential.Core n p) (hn : 0 < n) (degree : ℤ) (hclosed : ∀ (ℓ : Fin p → ℕ) (hForest : ContractionForestCensusGeneral.IsForest core (ClosedFaceCensus.zeroSet ℓ)) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy core (ClosedFaceCensus.zeroSet ℓ)), BNExists (ClosedFaceCensus.censusSpec core hn ℓ hForest hNotLoopy).graph 1 degree) {core' : ExplicitPotential.Core n' p'} (c : ContractionData core core') (s : SubdivisionGraph.Spec n' p') (hcore : s.core = core') : BNExists s.graph 1 degree

The contraction bridge. A closed-orthant row proof for core discharges the open-orthant row obligation of every orientation-exact equal-genus contraction core' of core.