The DegSpec face datum, emitted by the contraction census

Certificate/DegenerateSeparator.lean and Certificate/DegenerateRankOne.lean take rep, rep_idem, rep_zero, rep_loopless, forest — and, for the interpolated layer, a ZeroReach witness — as inputs that a row supplies by hand (see Certificate/Examples/GenusFourCore100Face.lean's faceRep, proved by five separate decides). This file makes them outputs of the generalized contraction census (Certificate/ContractionForestCensusGeneral.lean): name the set of slots that vanish at a point, check once that it is a forest with no semantic loop, and every one of those five obligations — the four DegSpec fields plus the ZeroReach witness the interpolated layer needs — falls out.

The bridge, in one picture

A Certificate m n p fixes a core and a point point : Fin m → ℤ fixes a length vector certificate.segmentNat point : Fin p → ℕ. Write zeroSlots certificate point for the Finset (Fin p) of vanishing slots. Then:

• censusRep := ContractionForestCensusGeneral.compFold certificate.core (zeroSlots certificate point) is a legal DegSpec.rep;
• censusRep_idem is compFold_idem, generically, no decide;
• censusRep_zero is compFold_tail_eq_head_of_mem, applied to slots in zeroSlots, which are exactly the ones membership needs;
• censusRep_loopless is rep_loopless_of_not_isLoopy, given the one census fact ¬ IsLoopy certificate.core (zeroSlots certificate point);
• censusRep_forest is forest_image_add_card_eq, given the one census fact IsForest certificate.core (zeroSlots certificate point); and
• censusRep_zeroReach upgrades reachIn_self_compFold — the same spanning-forest fact rep is built from — into the ZeroReach witness bnExists_..._of_zeroReach asks for, by matching AdjInList along zeroSlots with ZeroLink pointwise (adjInList_edgeList_zeroSlots_iff_zeroLink).

So the only two facts a row ever supplies are IsForest and ¬ IsLoopy of the concrete Finset zeroSlots certificate point — both decidable, both already what a census enumerates. bnExists_on_degenerate_subdivision_of_validClosed_of_forestCensus below is the resulting one-call wrapper, shaped to exactly match ExplicitPotential.CertificateData.bnExists_on_degenerate_subdivision_of_validClosed_of_zeroReach's conclusion.

The vanishing-slot set at a point

def Utilities.Certificate.ExplicitPotential.CertificateData.zeroSlots {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) : Finset (Fin p)

The slots that vanish at point: exactly the Finset a contraction census classifies.

Equations

• certificate.zeroSlots point = {edge : Fin p | certificate.segmentNat point edge = 0}

@[simp]

theorem Utilities.Certificate.ExplicitPotential.CertificateData.mem_zeroSlots {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (edge : Fin p) : edge ∈ certificate.zeroSlots point ↔ certificate.segmentNat point edge = 0

theorem Utilities.Certificate.ExplicitPotential.CertificateData.not_mem_zeroSlots_of_pos {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) {edge : Fin p} (hpos : 0 < certificate.segmentNat point edge) : edge ∉ certificate.zeroSlots point

The face datum, produced from the census's two facts

def Utilities.Certificate.ExplicitPotential.CertificateData.censusRep {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) : Fin n → Fin n

The census-produced rep. No row ever writes this by hand: it is the union-find component map of the vanishing-slot set.

Equations

• certificate.censusRep point = Utilities.Certificate.ContractionForestCensusGeneral.compFold certificate.core (certificate.zeroSlots point)

theorem Utilities.Certificate.ExplicitPotential.CertificateData.censusRep_idem {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (v : Fin n) : certificate.censusRep point (certificate.censusRep point v) = certificate.censusRep point v

theorem Utilities.Certificate.ExplicitPotential.CertificateData.censusRep_zero {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (edge : Fin p) : certificate.segmentNat point edge = 0 → certificate.censusRep point (certificate.core.tail edge) = certificate.censusRep point (certificate.core.head edge)

theorem Utilities.Certificate.ExplicitPotential.CertificateData.censusRep_loopless {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy certificate.core (certificate.zeroSlots point)) (edge : Fin p) : 0 < certificate.segmentNat point edge → certificate.censusRep point (certificate.core.tail edge) ≠ certificate.censusRep point (certificate.core.head edge)

theorem Utilities.Certificate.ExplicitPotential.CertificateData.censusRep_forest {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (hForest : ContractionForestCensusGeneral.IsForest certificate.core (certificate.zeroSlots point)) : (Finset.image (certificate.censusRep point) Finset.univ).card + {edge : Fin p | certificate.segmentNat point edge = 0}.card = n

The ZeroReach witness, from the same spanning-forest structure

theorem Utilities.Certificate.ExplicitPotential.CertificateData.adjInList_edgeList_zeroSlots_iff_zeroLink {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (u v : Fin n) : ContractionForestCensusGeneral.AdjInList certificate.core (ContractionForestCensusGeneral.edgeList (certificate.zeroSlots point)) u v ↔ certificate.ZeroLink point u v

Direct adjacency along zeroSlots is exactly ZeroLink, pointwise: both say "some vanishing slot joins u and v, in either reading direction".

theorem Utilities.Certificate.ExplicitPotential.CertificateData.reachIn_zeroSlots_iff_zeroReach {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (u v : Fin n) : ContractionForestCensusGeneral.ReachIn certificate.core (certificate.zeroSlots point) u v ↔ certificate.ZeroReach point u v

Reachability along zeroSlots is exactly ZeroReach: the reflexive-transitive closures of the two pointwise-equal relations above agree, by Relation.ReflTransGen.mono in both directions.

theorem Utilities.Certificate.ExplicitPotential.CertificateData.censusRep_zeroReach {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (v : Fin n) : certificate.ZeroReach point v (certificate.censusRep point v)

The ZeroReach witness the interpolated layer needs, emitted by the census. Every vertex reaches its own censusRep image along a chain of vanishing slots — the same spanning-forest fact censusRep is defined from, via reachIn_self_compFold, read through reachIn_zeroSlots_iff_zeroReach. No separate search: it falls out of rep's own construction.

The one-call wrapper, shaped to bnExists_..._of_zeroReach exactly

theorem Utilities.Certificate.ExplicitPotential.CertificateData.bnExists_on_degenerate_subdivision_of_validClosed_of_forestCensus {m n p : ℕ} (certificate : CertificateData m n p) (point : Fin m → ℤ) (core_nonempty : 0 < n) (degree : ℤ) (hValid : certificate.ValidClosed degree) (hCone : FormsHold certificate.cone point) (hForest : ContractionForestCensusGeneral.IsForest certificate.core (certificate.zeroSlots point)) (hNotLoopy : ¬ContractionForestCensusGeneral.IsLoopy certificate.core (certificate.zeroSlots point)) (hCoreConnected : certificate.core.Connected) : BNExists (certificate.degenerateSpec point core_nonempty (certificate.censusRep point) ⋯ ⋯ ⋯ ⋯).graph 1 degree

The acceptance-test wrapper. Everything bnExists_on_degenerate_subdivision_of_validClosed_of_zeroReach needs beyond ValidClosed/FormsHold/core connectivity is produced from a single decidable pair of census facts about zeroSlots certificate point: that it is a forest (IsForest) and carries no semantic loop (¬ IsLoopy). No rep, no ZeroReach witness, and no forest cardinality proof is ever written by a row again.