Canonical closed-face subdivision data

This is the row-independent adapter from a nonnegative slot-length vector and its forest census to a DegSpec. The representative map is the canonical union-find map generated by the zero slots.

def Utilities.Certificate.ClosedFaceCensus.zeroSet {p : ℕ} (length : Fin p → ℕ) : Finset (Fin p)

The vanishing slots of a nonnegative length assignment.

Equations

• Utilities.Certificate.ClosedFaceCensus.zeroSet length = {edge : Fin p | length edge = 0}

@[simp]

theorem Utilities.Certificate.ClosedFaceCensus.mem_zeroSet {p : ℕ} (length : Fin p → ℕ) (edge : Fin p) : edge ∈ zeroSet length ↔ length edge = 0

def Utilities.Certificate.ClosedFaceCensus.censusSpec {n p : ℕ} (core : ExplicitPotential.Core n p) (hn : 0 < n) (length : Fin p → ℕ) (hForest : ContractionForestCensusGeneral.IsForest core (zeroSet length)) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy core (zeroSet length)) : DegenerateSpec.DegSpec n p

The canonical degenerate subdivision attached to a forest face.

Equations

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

theorem Utilities.Certificate.ClosedFaceCensus.degSpec_ext {n p : ℕ} {d d' : DegenerateSpec.DegSpec n p} (hCore : d.core = d'.core) (hLength : d.length = d'.length) (hRep : d.rep = d'.rep) : d = d'

Extensionality for degenerate specifications; all other fields are proofs.