Contraction up to slot reversal

RowProof.ClosedContraction derives a contracted row's open-orthant obligation from a closed-orthant proof of the core it contracts from. Its ContractionData matches slots with orientation: tail_eq and head_eq demand that the contracted slot's tail is the tail, not the head.

That is the binding constraint in practice. Of the 94 non-trivalent genus-four rows, only 27 admit an orientation-exact contraction from a proved trivalent row; rows 010, 011, 031, 035 and 070 all sit under the proved row 099 yet need slots flipped. Reversing a slot does not change the subdivided graph at all — the path is the same, walked the other way — so this is pure bookkeeping, and this file removes it.

The route is the one Certificate/SubdivisionIso.lean already supports: reorient the target spec, contract there, and transport back along the identity relabeling whose reversed field records the flips.

def Utilities.Certificate.ReorientContraction.Core.reorient {n p : ℕ} (core : ExplicitPotential.Core n p) (rev : Fin p → Bool) : ExplicitPotential.Core n p

Reverse a chosen set of slots of a core.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Utilities.Certificate.ReorientContraction.Core.reorient_tail {n p : ℕ} (core : ExplicitPotential.Core n p) (rev : Fin p → Bool) (e : Fin p) : (reorient core rev).tail e = if rev e = true then core.head e else core.tail e

@[simp]

theorem Utilities.Certificate.ReorientContraction.Core.reorient_head {n p : ℕ} (core : ExplicitPotential.Core n p) (rev : Fin p → Bool) (e : Fin p) : (reorient core rev).head e = if rev e = true then core.tail e else core.head e

theorem Utilities.Certificate.ReorientContraction.Core.reorient_loopless {n p : ℕ} {core : ExplicitPotential.Core n p} {rev : Fin p → Bool} (h : ∀ (e : Fin p), core.tail e ≠ core.head e) (e : Fin p) : (reorient core rev).tail e ≠ (reorient core rev).head e

Reversing slots preserves looplessness.

def Utilities.Certificate.ReorientContraction.reorientSpec {n p : ℕ} (s : SubdivisionGraph.Spec n p) (rev : Fin p → Bool) : SubdivisionGraph.Spec n p

The same subdivision, with a chosen set of slots read backwards.

Equations

• One or more equations did not get rendered due to their size.

def Utilities.Certificate.ReorientContraction.reorientRelabeling {n p : ℕ} (s : SubdivisionGraph.Spec n p) (rev : Fin p → Bool) : s.Relabeling (reorientSpec s rev)

Reorientation is an identity relabeling: same vertices, same slots, same lengths, with reversed recording which slots were flipped.

Equations

• One or more equations did not get rendered due to their size.

theorem Utilities.Certificate.ReorientContraction.bnExists_spec_of_closed_contraction_reorient {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'} (rev : Fin p' → Bool) (c : ClosedContraction.ContractionData core (Core.reorient core' rev)) (s : SubdivisionGraph.Spec n' p') (hcore : s.core = core') : BNExists s.graph 1 degree

Contraction up to slot reversal.

A closed-orthant row proof for core yields the open-orthant obligation for any core' that contracts from it after reorienting some slots of core'. This is what takes the census reduction from the 27 orientation-exact rows to all 94.