Dispatching one exact closed face to its contracted core

ClosedContraction lifts a positive target subdivision into a face of a larger closed row. This module records the converse use of the same data: if the zero set of an already-given closed length vector is exactly the forest stored in ContractionData, its degenerate subdivision is equivalent to a positive subdivision of the displayed target core.

def Utilities.Certificate.ClosedFaceDispatch.ContractionData.targetSpec {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ClosedContraction.ContractionData core core') (hn' : 0 < n') (length : Fin p → ℕ) (hZero : ClosedFaceCensus.zeroSet length = c.F) : SubdivisionGraph.Spec n' p'

The honest positive target subdivision obtained by retaining the slots named by an exact contraction face.

Equations

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

theorem Utilities.Certificate.ClosedFaceDispatch.ContractionData.lift_targetSpec {n p n' p' : ℕ} {core : ExplicitPotential.Core n p} {core' : ExplicitPotential.Core n' p'} (c : ClosedContraction.ContractionData core core') (hn' : 0 < n') (length : Fin p → ℕ) (hZero : ClosedFaceCensus.zeroSet length = c.F) : c.lift (targetSpec c hn' length hZero) = length

Lifting the descended target subdivision recovers the original exact-face length vector, slot by slot.

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

An exact forest face is equivalent to the positive subdivision of its ContractionData target. This is the small reusable dispatcher behind human-readable finite face ledgers.

theorem Utilities.Certificate.ClosedFaceDispatch.bnExists_spec_of_reoriented_core {n' p' : ℕ} {core' : ExplicitPotential.Core n' p'} (rev : Fin p' → Bool) (degree : ℤ) (hTarget : ∀ (t : SubdivisionGraph.Spec n' p'), t.core = core' → BNExists t.graph 1 degree) (s : SubdivisionGraph.Spec n' p') (hCore : s.core = ReorientContraction.Core.reorient core' rev) : BNExists s.graph 1 degree

A positive-subdivision theorem for a core also applies when some target slots are presented backwards.