Equal-genus contractions of an arbitrary n-vertex, p-slot core

Certificate/ContractionForestCensus.lean builds the union-find census machinery (compFold, compFold_iff, IsForest, IsLoopy) for the one fixed shape ExplicitPotential.Core 8 12, the shape of every genus-five AR row core. This file lifts the same machinery, verbatim in argument, to an arbitrary ExplicitPotential.Core n p, so that a row of any shape — not just the two eight-vertex, twelve-slot rows 11/15 — can use the census, and so that Certificate/DegenerateSpecCensus.lean can turn a forest into the DegSpec face datum (rep, rep_idem, rep_zero, rep_loopless, forest) generically.

Nothing in ContractionForestCensus.lean is modified; that file, and Generated/GenusFiveARRow1115ContractionCensus.lean, keep working untouched. §4 below checks — cheaply, by rfl — that specializing this file's definitions at n = 8, p = 12 recovers the fixed-shape file's definitions exactly, so row 11/15's already-landed 2656/2686-target census is literally an instance of this one, not a parallel development.

Two additions beyond a straight generalization

The fixed-shape file stops at compFold/IsForest/IsLoopy: enough to classify contraction targets, but not enough to emit a DegSpec face datum. Two more facts are needed for that (DegenerateSpecCensus.lean consumes both):

• compFold is idempotent (compFold_idem): the union-find fold, folded again through itself, is a no-op. This is what makes compFold core F usable as DegSpec.rep directly — DegSpec.rep_idem is exactly this fact. Proved by induction on the edge list, carrying idempotence of the accumulator as the loop invariant (unionStep_idem); no decide, no per-shape work.
• A contracted edge really does identify its endpoints (compFold_tail_eq_head_of_mem) and compFold reaches every vertex from itself along F (reachIn_self_compFold): together with compFold_iff, the second is what lets DegenerateSpecCensus.lean produce the ZeroReach witness the interpolated layer needs, straight from the spanning-forest structure that already defines rep — no separate search.

Direct adjacency along an explicit list of edge slots

def Utilities.Certificate.ContractionForestCensusGeneral.AdjInList {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) (u v : Fin n) : Prop

u and v are joined by one edge slot drawn from the list l (in either reading direction).

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.AdjInList core l u v = ∃ e ∈ l, core.tail e = u ∧ core.head e = v ∨ core.head e = u ∧ core.tail e = v

@[instance_reducible]

instance Utilities.Certificate.ContractionForestCensusGeneral.decidableAdjInList {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) (u v : Fin n) : Decidable (AdjInList core l u v)

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.decidableAdjInList core l u v = id inferInstance

theorem Utilities.Certificate.ContractionForestCensusGeneral.AdjInList.symm {n p : ℕ} (core : ExplicitPotential.Core n p) {l : List (Fin p)} {u v : Fin n} (h : AdjInList core l u v) : AdjInList core l v u

theorem Utilities.Certificate.ContractionForestCensusGeneral.adjInList_symmetric {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) ⦃u v : Fin n⦄ : AdjInList core l u v → AdjInList core l v u

theorem Utilities.Certificate.ContractionForestCensusGeneral.adjInList_snoc {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) (e : Fin p) (x y : Fin n) : AdjInList core (l ++ [e]) x y ↔ AdjInList core l x y ∨ x = core.tail e ∧ y = core.head e ∨ x = core.head e ∧ y = core.tail e

One new edge appended at the end joins the list's adjacency relation with one literal pair.

def Utilities.Certificate.ContractionForestCensusGeneral.ReachInList {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) : Fin n → Fin n → Prop

The reachability relation generated by a list of edge slots: the reflexive-transitive closure of direct adjacency. Symmetric because AdjInList already is.

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.ReachInList core l = Relation.ReflTransGen (Utilities.Certificate.ContractionForestCensusGeneral.AdjInList core l)

theorem Utilities.Certificate.ContractionForestCensusGeneral.reachInList_symmetric {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) ⦃u v : Fin n⦄ : ReachInList core l u v → ReachInList core l v u

theorem Utilities.Certificate.ContractionForestCensusGeneral.reachInList_equivalence {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) : Equivalence (ReachInList core l)

Merging one related pair into an equivalence relation

def Utilities.Certificate.ContractionForestCensusGeneral.mergePair {n : ℕ} (R : Fin n → Fin n → Prop) (u v x y : Fin n) : Prop

R extended by declaring u and v related (and closing under the equivalence-relation axioms already available from R).

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.mergePair R u v x y = (R x y ∨ R x u ∧ R y v ∨ R x v ∧ R y u)

theorem Utilities.Certificate.ContractionForestCensusGeneral.mergePair_equivalence {n : ℕ} {R : Fin n → Fin n → Prop} (hR : Equivalence R) (u v : Fin n) : Equivalence (mergePair R u v)

Reflexive-transitive closure of a one-pair extension

theorem Utilities.Certificate.ContractionForestCensusGeneral.reachInList_snoc {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) (e : Fin p) (x y : Fin n) : ReachInList core (l ++ [e]) x y ↔ mergePair (ReachInList core l) (core.tail e) (core.head e) x y

unionStep matches mergePair exactly

def Utilities.Certificate.ContractionForestCensusGeneral.unionStep {n : ℕ} (rep : Fin n → Fin n) (u v : Fin n) : Fin n → Fin n

Merge the rep-class of u into the rep-class of v. See ContractionForestCensus.unionStep's docstring for the sharing discipline this let-binding shape enforces.

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.unionStep rep u v = fun (x : Fin n) => if rep x = rep u then rep v else rep x

theorem Utilities.Certificate.ContractionForestCensusGeneral.unionStep_iff {n : ℕ} {rep : Fin n → Fin n} {R : Fin n → Fin n → Prop} (hIff : ∀ (a b : Fin n), rep a = rep b ↔ R a b) (hR : Equivalence R) (u v x y : Fin n) : unionStep rep u v x = unionStep rep u v y ↔ mergePair R u v x y

theorem Utilities.Certificate.ContractionForestCensusGeneral.unionStep_idem {n : ℕ} {rep : Fin n → Fin n} (hidem : ∀ (x : Fin n), rep (rep x) = rep x) (u v x : Fin n) : unionStep rep u v (unionStep rep u v x) = unionStep rep u v x

New. unionStep preserves idempotence of the accumulator: if rep is already a retraction onto its own fixed points, so is unionStep rep u v. This is the loop invariant foldRep_idem inducts on.

theorem Utilities.Certificate.ContractionForestCensusGeneral.card_image_le_card_image_unionStep_succ {n : ℕ} (rep : Fin n → Fin n) (u v : Fin n) : (Finset.image rep Finset.univ).card ≤ (Finset.image (unionStep rep u v) Finset.univ).card + 1

New. One unionStep merges at most two classes, so it destroys at most one element of the image: image rep ⊆ insert (rep u) (image (unionStep …)), because the only vertices whose value changes are those already sent to rep u. This is the inductive heart of the graphic-matroid rank inequality card_le_card_image_compFold_add_card.

Folding over a list of edges: union-find, and its correctness

def Utilities.Certificate.ContractionForestCensusGeneral.foldRep {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) : Fin n → Fin n

Union-find over a list of edge slots, applied in order.

Equations

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

theorem Utilities.Certificate.ContractionForestCensusGeneral.foldRep_nil {n p : ℕ} (core : ExplicitPotential.Core n p) : foldRep core [] = id

theorem Utilities.Certificate.ContractionForestCensusGeneral.foldRep_snoc {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) (e : Fin p) : foldRep core (l ++ [e]) = unionStep (foldRep core l) (core.tail e) (core.head e)

theorem Utilities.Certificate.ContractionForestCensusGeneral.foldRep_iff {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) (x y : Fin n) : foldRep core l x = foldRep core l y ↔ ReachInList core l x y

Union-find correctness. foldRep-equality exactly characterizes reachability via the processed edge list.

theorem Utilities.Certificate.ContractionForestCensusGeneral.foldRep_idem {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) (x : Fin n) : foldRep core l (foldRep core l x) = foldRep core l x

New. The union-find fold is idempotent: refolding through itself is a no-op. Proved by induction on the edge list, carrying unionStep_idem as the loop invariant — no decide, and independent of n/p. This is exactly DegSpec.rep_idem once compFold is used as rep.

theorem Utilities.Certificate.ContractionForestCensusGeneral.card_le_card_image_foldRep_add_length {n p : ℕ} (core : ExplicitPotential.Core n p) (l : List (Fin p)) : n ≤ (Finset.image (foldRep core l) Finset.univ).card + l.length

New. The graphic-matroid rank inequality, at list level: folding k edges can cut the number of vertex classes by at most k. Induction on the edge list, with card_image_le_card_image_unionStep_succ as the step.

The census-facing interface: a specific contracted edge set F

def Utilities.Certificate.ContractionForestCensusGeneral.edgeList {p : ℕ} (F : Finset (Fin p)) : List (Fin p)

The edge slots of the core belonging to a finite set F, listed in the fixed canonical order 0, 1, …, p - 1.

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.edgeList F = List.filter (fun (e : Fin p) => decide (e ∈ F)) (List.finRange p)

theorem Utilities.Certificate.ContractionForestCensusGeneral.mem_edgeList {p : ℕ} (F : Finset (Fin p)) (e : Fin p) : e ∈ edgeList F ↔ e ∈ F

theorem Utilities.Certificate.ContractionForestCensusGeneral.length_edgeList {p : ℕ} (F : Finset (Fin p)) : (edgeList F).length = F.card

New. edgeList lists each slot of F exactly once, so its length is F.card. This is what converts the list-level rank inequality into the Finset-level one.

def Utilities.Certificate.ContractionForestCensusGeneral.compFold {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : Fin n → Fin n

The vertex partition induced by contracting the edge set F: each vertex's canonical representative under the union-find fold.

Equations

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

@[simp]

theorem Utilities.Certificate.ContractionForestCensusGeneral.compFold_empty {n p : ℕ} (core : ExplicitPotential.Core n p) : compFold core ∅ = id

def Utilities.Certificate.ContractionForestCensusGeneral.ReachIn {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : Fin n → Fin n → Prop

The reachability relation actually induced by contracting F.

Equations

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

theorem Utilities.Certificate.ContractionForestCensusGeneral.reachIn_equivalence {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : Equivalence (ReachIn core F)

theorem Utilities.Certificate.ContractionForestCensusGeneral.compFold_iff {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) (x y : Fin n) : compFold core F x = compFold core F y ↔ ReachIn core F x y

The main correctness theorem. compFold-equality exactly characterizes vertex reachability through the contracted edge set F.

@[instance_reducible]

instance Utilities.Certificate.ContractionForestCensusGeneral.decidableReachIn {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : DecidableRel (ReachIn core F)

Equations

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

theorem Utilities.Certificate.ContractionForestCensusGeneral.compFold_idem {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) (x : Fin n) : compFold core F (compFold core F x) = compFold core F x

New. compFold is idempotent: refolding a class through compFold again does nothing. This is exactly DegSpec.rep_idem.

theorem Utilities.Certificate.ContractionForestCensusGeneral.compFold_tail_eq_head_of_mem {n p : ℕ} (core : ExplicitPotential.Core n p) {F : Finset (Fin p)} {e : Fin p} (he : e ∈ F) : compFold core F (core.tail e) = compFold core F (core.head e)

New. A contracted edge's two endpoints land in the same class: this is exactly DegSpec.rep_zero for e ∈ F.

theorem Utilities.Certificate.ContractionForestCensusGeneral.reachIn_self_compFold {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) (v : Fin n) : ReachIn core F v (compFold core F v)

New. Every vertex reaches its own compFold representative through F — trivial from idempotence, but this is precisely the fact DegenerateSpecCensus.lean transports into a ZeroReach witness.

Genus preservation: the graphic-matroid rank equation

def Utilities.Certificate.ContractionForestCensusGeneral.IsForest {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : Prop

F is a forest of the core: contracting it is an equal-genus topological contraction.

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.IsForest core F = (F.card = n - (Finset.image (Utilities.Certificate.ContractionForestCensusGeneral.compFold core F) Finset.univ).card)

@[instance_reducible]

instance Utilities.Certificate.ContractionForestCensusGeneral.decidableIsForest {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : Decidable (IsForest core F)

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.decidableIsForest core F = id inferInstance

theorem Utilities.Certificate.ContractionForestCensusGeneral.card_image_compFold_le {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : (Finset.image (compFold core F) Finset.univ).card ≤ n

The image of compFold core F has at most n elements — trivial, but what forest_image_add_card_eq needs to turn the truncated-subtraction IsForest equation into the additive DegSpec.forest equation.

theorem Utilities.Certificate.ContractionForestCensusGeneral.card_le_card_image_compFold_add_card {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : n ≤ (Finset.image (compFold core F) Finset.univ).card + F.card

New. The graphic-matroid rank inequality. Contracting F cuts the number of vertex classes by at most F.card, for every slot set F — each contracted slot merges at most two classes. IsForest core F is precisely the equality case (see forest_image_add_card_eq), so this is the inequality whose saturation "contracting F preserves the genus" means.

Consequence used by the split-loop analysis: a slot set carrying a cycle cannot be a forest, because deleting a redundant slot from it leaves the partition — hence the image cardinality — unchanged while dropping F.card by one, which would violate this bound.

theorem Utilities.Certificate.ContractionForestCensusGeneral.card_image_le_of_rep_iff {m : ℕ} {r₁ r₂ : Fin m → Fin m} (h₁ : ∀ (x : Fin m), r₁ (r₁ x) = r₁ x) (hiff : ∀ (x y : Fin m), r₁ x = r₁ y ↔ r₂ x = r₂ y) : (Finset.image r₁ Finset.univ).card ≤ (Finset.image r₂ Finset.univ).card

New. Two idempotent representative maps with the same fibres have images of the same size; only the ≤ direction is stated, since the converse is the same lemma with the arguments swapped. The injection is r₂ itself: idempotence of r₁ makes r₂ (r₁ x) = r₂ x, so r₂ separates distinct r₁-classes. Used to compare compFold core F with compFold core F' when F and F' induce the same reachability relation.

theorem Utilities.Certificate.ContractionForestCensusGeneral.forest_image_add_card_eq {n p : ℕ} (core : ExplicitPotential.Core n p) {F : Finset (Fin p)} (hForest : IsForest core F) : (Finset.image (compFold core F) Finset.univ).card + F.card = n

New. IsForest, stated additively: exactly the DegSpec.forest field, once rep := compFold core F and F is the zero-length slot set.

theorem Utilities.Certificate.ContractionForestCensusGeneral.forest_card_lt {n p : ℕ} (core : ExplicitPotential.Core n p) {F : Finset (Fin p)} (hn : 0 < n) (h : IsForest core F) : F.card ≤ n - 1

Every forest of an n-vertex graph has at most n - 1 edges: the vertex-partition image is nonempty (given n > 0), so n - image.card ≤ n - 1.

def Utilities.Certificate.ContractionForestCensusGeneral.IsLoopy {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : Prop

F leaves a semantic loop: some uncontracted edge slot has both endpoints identified by the contraction. Exactly the negation of core_loopless/rep_loopless for the contraction target.

Equations

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

@[instance_reducible]

instance Utilities.Certificate.ContractionForestCensusGeneral.decidableIsLoopy {n p : ℕ} (core : ExplicitPotential.Core n p) (F : Finset (Fin p)) : Decidable (IsLoopy core F)

Equations

• Utilities.Certificate.ContractionForestCensusGeneral.decidableIsLoopy core F = id inferInstance

theorem Utilities.Certificate.ContractionForestCensusGeneral.rep_loopless_of_not_isLoopy {n p : ℕ} (core : ExplicitPotential.Core n p) {F : Finset (Fin p)} (hNotLoopy : ¬IsLoopy core F) (e : Fin p) : e ∉ F → compFold core F (core.tail e) ≠ compFold core F (core.head e)

New. The rep_loopless reading of ¬ IsLoopy, stated pointwise: a surviving slot (e ∉ F) is not a loop after contracting F.