Rigidity of the representative map on a forest face

A DegSpec carries its vertex identification as a chosen function rep : Fin n → Fin n, not as a partition, and its forest field is a cardinality equation rather than the assertion that the vanishing slots generate rep. Two consequences, both recorded in Utilities/Subdivision/DegenerateSpec.lean's own header and in the corresponding closed-row proof module §4:

• a DegSpec on a non-forest vanishing set may merge blocks that no metric degeneration merges — the cardinality equation lets an unrelated extra identification balance a redundant zero slot; and
• even on a forest face, rep may pick different representatives of the right classes than the union-find map compFold does, so DegSpec.ext' (which compares rep as a function) cannot identify the two.

This file removes both obstacles for the forest case.

What is proved

rep_eq_of_compFold_eq — rep always coarsens the census partition; this is just rep_zero propagated along a ReachIn chain, and needs no hypothesis.

compFold_eq_of_rep_eq — the sharpening. On a forest face the coarsening is an equality. forest gives |image rep| + |zeroSlots| = n and IsForest gives |image compFold| + |zeroSlots| = n, so a coarsening between partitions of equal class count is the identity. Together: rep_iff_compFold.

repEquiv — representative independence. Two closed faces on the same core and lengths that induce the same partition have LaplacianEquiv graphs, matching core vertex for core vertex (repEquiv_coreVertex). No new combinatorics: d₁ is exhibited as a Contraction onto d₂'s canonical positive quotient d₂.contractedSpec, and the equivalence is that datum composed with d₂.canonicalContraction.

censusFace / censusFaceEquiv — the payoff. Every forest face of a closed orthant is LaplacianEquiv, mark for mark, to the face a census-facing producer speaks about (rep := compFold of the vanishing slots — literally the corresponding closed-row proof module's rep). Note that censusFace needs no ¬ IsLoopy hypothesis: its rep_loopless field is inherited from d's through rep_eq_of_compFold_eq.

What is not proved here

Nothing about non-forest faces. On those rep genuinely is not determined by the length vector, and the enumeration in the accompanying analysis measures how many such faces a genus-five legged row has.

The class of a core vertex on the canonical positive quotient

These two live here rather than beside their first consumer because they are pure DegSpec bookkeeping and both the legged reduction and the rigidity statement below need them.

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.contractedClass {n p : ℕ} (d : DegSpec n p) (v : Fin n) : Fin d.classCard

The class of a core vertex, as a core vertex index of the canonical contracted core. This is the mark-carrying half of the legged reduction: a pinned mark on a closed face is again a pinned core mark on the canonical positive quotient.

Equations

• d.contractedClass v = d.classIndex ⟨d.rep v, ⋯⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.canonicalContraction_coreVertex_contractedClass {n p : ℕ} (d : DegSpec n p) (v : Fin n) : d.canonicalContraction.laplacianEquiv.toEquiv (d.contractedSpec.coreVertex (d.contractedClass v)) = d.coreVertex v

The canonical Laplacian equivalence carries the contracted class of a core vertex back to that core vertex's class on the closed face.

Representative independence

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.contractionOfRepIff {n p : ℕ} (d₁ d₂ : DegSpec n p) (hcore : d₁.core = d₂.core) (hlength : d₁.length = d₂.length) (hiff : ∀ (u v : Fin n), d₁.rep u = d₁.rep v ↔ d₂.rep u = d₂.rep v) : d₁.Contraction d₂.contractedSpec

Two closed faces on the same core and lengths that induce the same vertex partition: d₁ is a Contraction onto d₂'s canonical positive quotient.

Every field is index bookkeeping through d₂.classIndex/d₂.slotIndex; the only mathematical input is hiff, used three times to move a d₂.rep inside a d₁.rep.

Equations

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

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.repEquiv {n p : ℕ} (d₁ d₂ : DegSpec n p) (hcore : d₁.core = d₂.core) (hlength : d₁.length = d₂.length) (hiff : ∀ (u v : Fin n), d₁.rep u = d₁.rep v ↔ d₂.rep u = d₂.rep v) : LaplacianEquiv d₁.graph d₂.graph

Representative independence. Two closed faces on the same core and lengths with the same vertex partition carry the same Laplacian.

Equations

• d₁.repEquiv d₂ hcore hlength hiff = (d₁.contractionOfRepIff d₂ hcore hlength hiff).laplacianEquiv.symm.trans d₂.canonicalContraction.laplacianEquiv

theorem Utilities.Certificate.DegenerateSpec.DegSpec.repEquiv_coreVertex {n p : ℕ} (d₁ d₂ : DegSpec n p) (hcore : d₁.core = d₂.core) (hlength : d₁.length = d₂.length) (hiff : ∀ (u v : Fin n), d₁.rep u = d₁.rep v ↔ d₂.rep u = d₂.rep v) (v : Fin n) : (d₁.repEquiv d₂ hcore hlength hiff).toEquiv (d₁.coreVertex v) = d₂.coreVertex v

The equivalence matches core vertex for core vertex — so a pinned mark survives the change of representatives.

The vanishing-slot set and the census partition

def Utilities.Certificate.DegenerateSpec.DegSpec.zeroSlotSet {n p : ℕ} (d : DegSpec n p) : Finset (Fin p)

The vanishing slots of a degenerate spec. Syntactically the Finset appearing in the forest field.

Equations

• d.zeroSlotSet = {e : Fin p | d.length e = 0}

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.mem_zeroSlotSet {n p : ℕ} (d : DegSpec n p) (e : Fin p) : e ∈ d.zeroSlotSet ↔ d.length e = 0

theorem Utilities.Certificate.DegenerateSpec.DegSpec.forest' {n p : ℕ} (d : DegSpec n p) : (Finset.image d.rep Finset.univ).card + d.zeroSlotSet.card = n

def Utilities.Certificate.DegenerateSpec.DegSpec.RepIsContraction {n p : ℕ} (d : DegSpec n p) : Prop

The classes of rep are generated by the vanishing slots. rep_zero is the easy direction; this is the converse, which a bare DegSpec does not carry. It holds by definition for every rep built as a compFold.

Equations

• d.RepIsContraction = ∀ (u v : Fin n), d.rep u = d.rep v → Utilities.Certificate.ContractionForestCensusGeneral.ReachIn d.core d.zeroSlotSet u v

theorem Utilities.Certificate.DegenerateSpec.DegSpec.rep_eq_of_reachIn {n p : ℕ} (d : DegSpec n p) {x y : Fin n} (h : ContractionForestCensusGeneral.ReachIn d.core d.zeroSlotSet x y) : d.rep x = d.rep y

rep is constant along vanishing-slot reachability: the direction every DegSpec has, packaged for ReflTransGen.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.rep_eq_of_compFold_eq {n p : ℕ} (d : DegSpec n p) {u v : Fin n} (h : ContractionForestCensusGeneral.compFold d.core d.zeroSlotSet u = ContractionForestCensusGeneral.compFold d.core d.zeroSlotSet v) : d.rep u = d.rep v

rep coarsens the census partition. No hypothesis: this is rep_zero propagated along a reachability chain through the vanishing slots.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.isForest_of_repIsContraction {n p : ℕ} (d : DegSpec n p) (h : d.RepIsContraction) : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet

An honest face has a forest vanishing set. If rep's classes really are generated by the vanishing slots — which is what every metric degeneration gives, and what RepIsContraction names — then the two partitions coincide, so their class counts agree, and the forest cardinality field upgrades to IsForest.

Contrapositively: the faces the forest field admits but no degeneration produces are exactly the non-forest ones. That is the precise content of the corresponding closed-row proof module §4's counterexample.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.not_isLoopy_zeroSlotSet {n p : ℕ} (d : DegSpec n p) : ¬ContractionForestCensusGeneral.IsLoopy d.core d.zeroSlotSet

A closed face is never loopy. rep_loopless plus the coarsening of rep_eq_of_compFold_eq rules out a semantic loop on the census partition, with no hypothesis at all — so the second census check a row-proof leaf asks for is free once one has a DegSpec in hand.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.compFold_eq_of_rep_eq {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) {u v : Fin n} (h : d.rep u = d.rep v) : ContractionForestCensusGeneral.compFold d.core d.zeroSlotSet u = ContractionForestCensusGeneral.compFold d.core d.zeroSlotSet v

The sharpening. On a forest face the coarsening of rep_eq_of_compFold_eq is an equality: rep and compFold induce the same partition.

Both partitions have n - |zeroSlots| classes — one by the forest field, the other by IsForest — and a coarsening between partitions of equal class count is the identity.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.rep_iff_compFold {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) (u v : Fin n) : d.rep u = d.rep v ↔ ContractionForestCensusGeneral.compFold d.core d.zeroSlotSet u = ContractionForestCensusGeneral.compFold d.core d.zeroSlotSet v

The sharpening, as the partition identity.

The census face

def Utilities.Certificate.DegenerateSpec.DegSpec.censusFace {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) : DegSpec n p

The census face of a forest face: the same core and the same lengths, with rep replaced by the union-find component map of the vanishing slots — that is, by exactly the rep a census-facing producer builds (the corresponding closed-row proof module).

No ¬ IsLoopy hypothesis is needed: rep_loopless is inherited from d through rep_eq_of_compFold_eq.

Equations

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

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.censusFace_core {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) : (d.censusFace hForest).core = d.core

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.censusFace_length {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) : (d.censusFace hForest).length = d.length

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.censusFace_rep {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) : (d.censusFace hForest).rep = ContractionForestCensusGeneral.compFold d.core d.zeroSlotSet

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.censusFaceEquiv {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) : LaplacianEquiv d.graph (d.censusFace hForest).graph

The payoff. Every forest face is LaplacianEquiv to its census face.

Equations

• d.censusFaceEquiv hForest = d.repEquiv (d.censusFace hForest) ⋯ ⋯ ⋯

theorem Utilities.Certificate.DegenerateSpec.DegSpec.censusFaceEquiv_coreVertex {n p : ℕ} (d : DegSpec n p) (hForest : ContractionForestCensusGeneral.IsForest d.core d.zeroSlotSet) (v : Fin n) : (d.censusFaceEquiv hForest).toEquiv (d.coreVertex v) = (d.censusFace hForest).coreVertex v

…matching core vertex for core vertex, so a pinned mark survives.