Subdivision specifications on the CLOSED length orthant

SubdivisionGraph.Spec carries length_pos : ∀ edge, 0 < length edge, so a certificate written against it is valid only on the interior of the length orthant. Every equal-genus contraction of the core therefore has to be treated as a separate certificate target. This module introduces the degenerate variant, whose lengths may vanish, so that a contraction target is a face of a cone a certificate already covers rather than a new case.

The one thing that is not just "drop the field"

Dropping length_pos from Spec and keeping Spec.graph verbatim gives the wrong graph. A slot of length 0 emits no unit steps and no interior vertices, so Spec.graph would delete it and leave its two endpoints as distinct vertices. Metric degeneration contracts: a segment of length zero identifies its endpoints. Deletion drops the genus by one per deleted slot; contraction preserves it. A degenerate spec must therefore carry the vertex identification explicitly, as an idempotent representative map rep.

Why no vertex weights are needed

Write z for the number of zero slots. The graph below has ∑ length edges and #(image rep) + ∑ (length - 1) vertices, so

genus = #positiveSlots - #(image rep) + 1 .

Genus equals the core's p - n + 1 exactly when #(image rep) + z = n, which is the field forest below. For the canonical representative map generated by the zero slots, this is precisely the graphic-matroid statement that the zero set is a forest. For an arbitrary bare DegSpec, however, the cardinality equation alone does not prevent an unrelated extra identification from balancing a redundant zero edge. Consumer interfaces that mean an honest contraction must therefore require exact generation by the zero slots or use a canonical union-find representative. Genus preservation itself still follows from the displayed cardinality equation, so no vertex weight is needed.

What is not defined here

No rank, no winnable, no Riemann--Roch on a degenerate object. A DegSpec has a graph : CFGraph and nothing else; all semantics remain on CFGraph. The two bridges are

• Contraction, the face-equals-contraction-target correspondence: a DegSpec whose zero set is a forest is LaplacianEquiv to the strictly positive Spec on the contracted core; and
• toSpec, the translation lemma: at a strictly positive length vector a DegSpec is an ordinary Spec, with rep = id.

structure Utilities.Certificate.DegenerateSpec.DegSpec (n p : ℕ) : Type

Subdivision data on the closed length orthant.

length may vanish. rep names the vertex identification produced by collapsing the zero slots; forest is the genus-preserving cardinality condition. Honest closed-face authoring interfaces use the canonical union-find representative rather than treating an arbitrary rep as a contraction.

• core : ExplicitPotential.Core n p

  The ordered core whose slots are subdivided when positive and contracted when their lengths vanish.

• length : Fin p → ℕ

  The natural-number length of each slot; zero denotes contraction of its endpoints.

• core_nonempty : 0 < n
• rep : Fin n → Fin n

  Canonical representative of a core vertex after collapsing zero slots.

• rep_idem (v : Fin n) : self.rep (self.rep v) = self.rep v
• rep_zero (e : Fin p) : self.length e = 0 → self.rep (self.core.tail e) = self.rep (self.core.head e)

  A vanishing slot identifies its two endpoints: this is contraction, not deletion.

• rep_loopless (e : Fin p) : 0 < self.length e → self.rep (self.core.tail e) ≠ self.rep (self.core.head e)

  A surviving slot is not a loop after the contraction.

• forest : (Finset.image self.rep Finset.univ).card + {e : Fin p | self.length e = 0}.card = n

  The Euler-characteristic equation for genus preservation. When rep is the canonical quotient generated by the zero slots, this is exactly the assertion that those slots form a forest; see genus_graph.

The vertex and step types

@[reducible, inline]

abbrev Utilities.Certificate.DegenerateSpec.DegSpec.Class {n p : ℕ} (d : DegSpec n p) : Type

Surviving core vertices: the rep-fixed points, i.e. one per class.

Equations

• d.Class = { v : Fin n // d.rep v = v }

@[reducible, inline]

abbrev Utilities.Certificate.DegenerateSpec.DegSpec.Interior {n p : ℕ} (d : DegSpec n p) : Type

Interior vertices of the surviving slots. A slot of length 0 or 1 contributes none, because Fin (0 - 1) = Fin (1 - 1) = Fin 0.

Equations

• d.Interior = ((e : Fin p) × Fin (d.length e - 1))

@[reducible, inline]

abbrev Utilities.Certificate.DegenerateSpec.DegSpec.Vertex {n p : ℕ} (d : DegSpec n p) : Type

Vertices of the closed subdivision: representative core classes together with interior vertices of surviving slots.

Equations

• d.Vertex = (d.Class ⊕ d.Interior)

@[reducible, inline]

abbrev Utilities.Certificate.DegenerateSpec.DegSpec.Step {n p : ℕ} (d : DegSpec n p) : Type

A unit step exists only on a slot of positive length.

Equations

• d.Step = ((e : Fin p) × Fin (d.length e))

def Utilities.Certificate.DegenerateSpec.DegSpec.coreVertex {n p : ℕ} (d : DegSpec n p) (v : Fin n) : d.Vertex

The class of a core vertex, as a vertex of the degenerate subdivision.

Equations

• d.coreVertex v = Sum.inl ⟨d.rep v, ⋯⟩

def Utilities.Certificate.DegenerateSpec.DegSpec.interiorVertex {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e - 1)) : d.Vertex

The interior vertex at zero-based offset o on a slot, corresponding to path position o + 1.

Equations

• d.interiorVertex e o = Sum.inr ⟨e, o⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.coreVertex_eq_iff {n p : ℕ} (d : DegSpec n p) (u v : Fin n) : d.coreVertex u = d.coreVertex v ↔ d.rep u = d.rep v

def Utilities.Certificate.DegenerateSpec.DegSpec.stepLeft {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e)) : d.Vertex

The left vertex of a unit step, using the tail core class at the initial step.

Equations

• d.stepLeft e o = if hzero : ↑o = 0 then d.coreVertex (d.core.tail e) else d.interiorVertex e ⟨↑o - 1, ⋯⟩

def Utilities.Certificate.DegenerateSpec.DegSpec.stepRight {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e)) : d.Vertex

The right vertex of a unit step, using the head core class at the final step.

Equations

• d.stepRight e o = if hlast : ↑o + 1 = d.length e then d.coreVertex (d.core.head e) else d.interiorVertex e ⟨↑o, ⋯⟩

def Utilities.Certificate.DegenerateSpec.DegSpec.unitEdge {n p : ℕ} (d : DegSpec n p) (s : d.Step) : d.Vertex × d.Vertex

The ordered endpoint pair of a unit-step occurrence in the degenerate subdivision.

Equations

• d.unitEdge s = (d.stepLeft s.fst s.snd, d.stepRight s.fst s.snd)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.stepLeft_ne_stepRight {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e)) : d.stepLeft e o ≠ d.stepRight e o

@[reducible, inline]

abbrev Utilities.Certificate.DegenerateSpec.DegSpec.graph {n p : ℕ} (d : DegSpec n p) : CFGraph

The degenerate subdivision graph. Zero slots emit nothing; their endpoints have already been identified by rep.

Equations

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

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.graph_edges {n p : ℕ} (d : DegSpec n p) : d.graph.edges = Multiset.map d.unitEdge Finset.univ.val

Path positions

The chip-position trichotomy. On a Spec a certificate may get away with a two-case split (offset = 0 versus offset > 0, the latter always interior) whenever the offset is strictly below the slot length — a bound that usually comes from length_pos. On the closed orthant the third case, offset = length, is reachable and must be present.

@[reducible, inline]

abbrev Utilities.Certificate.DegenerateSpec.DegSpec.PathPosition {n p : ℕ} (d : DegSpec n p) (e : Fin p) : Type

All integer positions along a slot, including both endpoint positions even when the length is zero.

Equations

• d.PathPosition e = Fin (d.length e + 1)

def Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex {n p : ℕ} (d : DegSpec n p) (e : Fin p) (k : d.PathPosition e) : d.Vertex

Decode a slot position as its tail, interior, or head vertex; a zero-length slot has a single contracted endpoint.

Equations

• d.pathVertex e k = if hzero : ↑k = 0 then d.coreVertex (d.core.tail e) else if hlast : ↑k = d.length e then d.coreVertex (d.core.head e) else d.interiorVertex e ⟨↑k - 1, ⋯⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_zero {n p : ℕ} (d : DegSpec n p) (e : Fin p) : d.pathVertex e ⟨0, ⋯⟩ = d.coreVertex (d.core.tail e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_length {n p : ℕ} (d : DegSpec n p) (e : Fin p) : d.pathVertex e ⟨d.length e, ⋯⟩ = d.coreVertex (d.core.head e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_interior {n p : ℕ} (d : DegSpec n p) (e : Fin p) (k : d.PathPosition e) (h0 : ↑k ≠ 0) (hL : ↑k ≠ d.length e) : d.pathVertex e k = d.interiorVertex e ⟨↑k - 1, ⋯⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_eq_of_val_eq {n p : ℕ} (d : DegSpec n p) (e : Fin p) {j k : d.PathPosition e} (h : ↑j = ↑k) : d.pathVertex e j = d.pathVertex e k

def Utilities.Certificate.DegenerateSpec.DegSpec.clampPos {n p : ℕ} (d : DegSpec n p) (e : Fin p) (k : ℕ) : d.PathPosition e

A path position clamped into range. On a slot the certificate actually uses this is the identity; it exists so that a generic statement can name a position on every slot without carrying a bound for the slots it ignores.

Equations

• d.clampPos e k = ⟨min k (d.length e), ⋯⟩

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.clampPos_val_of_le {n p : ℕ} (d : DegSpec n p) {e : Fin p} {k : ℕ} (hk : k ≤ d.length e) : ↑(d.clampPos e k) = k

def Utilities.Certificate.DegenerateSpec.DegSpec.pathAt {n p : ℕ} (d : DegSpec n p) (e : Fin p) (k : ℕ) : d.Vertex

The path vertex at a clamped position, total in the natural number k.

This is the form a row proof should use throughout. pathVertex is indexed by Fin (length e + 1), so naming a position costs a bound proof at every occurrence; on the closed orthant those bounds are exactly the ones that stop being free. pathAt carries none: positions beyond the end of the slot are clamped to the head, which is where a chip pushed off the end belongs.

It lives here rather than beside its first consumer because the two consumers sit on independent branches of the tower: ramp scripts read chips off it, and Certificate/ScaleQReduced.lean walks along it.

Equations

• d.pathAt e k = d.pathVertex e (d.clampPos e k)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathAt_congr {n p : ℕ} (d : DegSpec n p) (e : Fin p) {j k : ℕ} (h : min j (d.length e) = min k (d.length e)) : d.pathAt e j = d.pathAt e k

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathAt_of_eq {n p : ℕ} (d : DegSpec n p) (e : Fin p) {j k : ℕ} (h : j = k) : d.pathAt e j = d.pathAt e k

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathAt_zero {n p : ℕ} (d : DegSpec n p) (e : Fin p) : d.pathAt e 0 = d.coreVertex (d.core.tail e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathAt_length {n p : ℕ} (d : DegSpec n p) {e : Fin p} {k : ℕ} (hk : d.length e ≤ k) : d.pathAt e k = d.coreVertex (d.core.head e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathAt_interior {n p : ℕ} (d : DegSpec n p) {e : Fin p} {k : ℕ} (h0 : k ≠ 0) (hk : k < d.length e) : d.pathAt e k = d.interiorVertex e ⟨k - 1, ⋯⟩

Genus: the whole point of the forest field

theorem Utilities.Certificate.DegenerateSpec.DegSpec.image_rep_eq_filter {n p : ℕ} (d : DegSpec n p) : Finset.image d.rep Finset.univ = {v : Fin n | d.rep v = v}

The rep-fixed points are exactly the image of rep.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.card_class {n p : ℕ} (d : DegSpec n p) : Fintype.card d.Class = (Finset.image d.rep Finset.univ).card

theorem Utilities.Certificate.DegenerateSpec.DegSpec.card_edges {n p : ℕ} (d : DegSpec n p) : d.graph.edges.card = ∑ e : Fin p, d.length e

theorem Utilities.Certificate.DegenerateSpec.DegSpec.card_vertices {n p : ℕ} (d : DegSpec n p) : Fintype.card d.graph.V = (Finset.image d.rep Finset.univ).card + ∑ e : Fin p, (d.length e - 1)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.sum_length_eq {n p : ℕ} (d : DegSpec n p) : ∑ e : Fin p, d.length e = ∑ e : Fin p, (d.length e - 1) + {e : Fin p | 0 < d.length e}.card

Splitting the edge count into interior vertices plus one per surviving slot.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.card_pos_add_card_zero {n p : ℕ} (d : DegSpec n p) : {e : Fin p | 0 < d.length e}.card + {e : Fin p | d.length e = 0}.card = p

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.genus_graph {n p : ℕ} (d : DegSpec n p) : d.graph.genus = ↑p - ↑n + 1

Genus is preserved on every forest face. No vertex weight appears: the forest field is exactly what makes the two z's cancel.

Multiplicities

theorem Utilities.Certificate.DegenerateSpec.DegSpec.num_edges_eq_card_filter_steps {n p : ℕ} (d : DegSpec n p) (x y : d.Vertex) : numEdges d.graph x y = {s : d.Step | d.unitEdge s = (x, y) ∨ d.unitEdge s = (y, x)}.card

Fibre regrouping

The transferable half of a symbolic certificate. Every quantity a SlopeScript-style certificate computes at a core vertex is an endpoint-indicator sum over slots. On the contracted core such a sum is the sum, over the members of one collapsed class, of the uncontracted sums — so a row's per-core-vertex lemmas are reusable at every face by addition instead of being reproved per face.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.sum_tail_class {n p : ℕ} (d : DegSpec n p) (r : Fin n) (F : Fin p → ℤ) : (∑ e : Fin p, if d.rep (d.core.tail e) = r then F e else 0) = ∑ v : Fin n with d.rep v = r, ∑ e : Fin p, if d.core.tail e = v then F e else 0

theorem Utilities.Certificate.DegenerateSpec.DegSpec.sum_head_class {n p : ℕ} (d : DegSpec n p) (r : Fin n) (G : Fin p → ℤ) : (∑ e : Fin p, if d.rep (d.core.head e) = r then G e else 0) = ∑ v : Fin n with d.rep v = r, ∑ e : Fin p, if d.core.head e = v then G e else 0

theorem Utilities.Certificate.DegenerateSpec.DegSpec.zero_slot_cancels {n p : ℕ} (d : DegSpec n p) (r : Fin n) (F G : Fin p → ℤ) (e : Fin p) (hzero : d.length e = 0) (hFG : F e = G e) : ((if d.rep (d.core.tail e) = r then F e else 0) + if d.rep (d.core.head e) = r then -G e else 0) = 0

A vanishing slot contributes nothing to a contracted endpoint sum, because its two endpoints lie in the same class and its two endpoint contributions are equal and opposite. This is why a certificate's per-slot data may be summed over all slots of the uncontracted core, zero ones included.

The face-equals-contraction-target correspondence

structure Utilities.Certificate.DegenerateSpec.DegSpec.Contraction {n p n' p' : ℕ} (d : DegSpec n p) (target : SubdivisionGraph.Spec n' p') : Type

Matching data identifying a DegSpec with the strictly positive Spec on its contracted core. All four maps are pure index bookkeeping; no lengths change. Slot reorientation is deliberately not included: it is already supplied by SubdivisionGraph.Spec.Relabeling, which composes with the LaplacianEquiv produced here.

• vtx : Fin n' → Fin n

  Which uncontracted core vertex represents each target vertex.

• vtx_rep (v' : Fin n') : d.rep (self.vtx v') = self.vtx v'
• vtx_inj : Function.Injective self.vtx
• vtx_surj (v : Fin n) : ∃ (v' : Fin n'), self.vtx v' = d.rep v
• slot : Fin p' → Fin p

  Which uncontracted slot each target slot is.

• slot_inj : Function.Injective self.slot
• slot_surj (e : Fin p) : 0 < d.length e → ∃ (e' : Fin p'), self.slot e' = e
• length_eq (e' : Fin p') : target.length e' = d.length (self.slot e')
• tail_eq (e' : Fin p') : self.vtx (target.core.tail e') = d.rep (d.core.tail (self.slot e'))
• head_eq (e' : Fin p') : self.vtx (target.core.head e') = d.rep (d.core.head (self.slot e'))

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.slot_pos {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) (e' : Fin p') : 0 < d.length (c.slot e')

def Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.classMap {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : Fin n' → d.Class

Core-vertex half of the vertex bijection.

Equations

• c.classMap v' = ⟨c.vtx v', ⋯⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.classMap_bijective {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : Function.Bijective c.classMap

def Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.interiorMap {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : (e' : Fin p') × Fin (target.length e' - 1) → d.Interior

Interior half of the vertex bijection.

Equations

• c.interiorMap s = ⟨c.slot s.fst, ⟨↑s.snd, ⋯⟩⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.interiorMap_bijective {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : Function.Bijective c.interiorMap

def Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.stepMap {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : target.Step → d.Step

Unit-step bijection.

Equations

• c.stepMap s = ⟨c.slot s.fst, ⟨↑s.snd, ⋯⟩⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.stepMap_bijective {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : Function.Bijective c.stepMap

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.vertexEquiv {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : target.Vertex ≃ d.Vertex

Vertex bijection of the correspondence.

Equations

• c.vertexEquiv = (Equiv.ofBijective c.classMap ⋯).sumCongr (Equiv.ofBijective c.interiorMap ⋯)

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.stepEquiv {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : target.Step ≃ d.Step

The bijection from unit steps in the positive contracted presentation to surviving unit steps in the closed presentation, preserving offsets.

Equations

• c.stepEquiv = Equiv.ofBijective c.stepMap ⋯

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.vertexEquiv_coreVertex {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) (v' : Fin n') : c.vertexEquiv (target.coreVertex v') = d.coreVertex (c.vtx v')

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.vertexEquiv_interiorVertex {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) (e' : Fin p') (o : Fin (target.length e' - 1)) : c.vertexEquiv (target.interiorVertex e' o) = d.interiorVertex (c.slot e') ⟨↑o, ⋯⟩

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.stepEquiv_apply {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) (e' : Fin p') (o : Fin (target.length e')) : c.stepEquiv ⟨e', o⟩ = ⟨c.slot e', ⟨↑o, ⋯⟩⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.unitEdge_stepEquiv {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) (s : target.Step) : d.unitEdge (c.stepEquiv s) = (c.vertexEquiv (target.unitEdge s).1, c.vertexEquiv (target.unitEdge s).2)

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.laplacianEquiv {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : LaplacianEquiv target.graph d.graph

The correspondence. A face of the closed orthant whose zero set is a forest carries the same Laplacian as the strictly positive subdivision of the contracted core.

Equations

• c.laplacianEquiv = { toEquiv := c.vertexEquiv, num_edges_eq := ⋯ }

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.Contraction.graphIso {n p n' p' : ℕ} {d : DegSpec n p} {target : SubdivisionGraph.Spec n' p'} (c : d.Contraction target) : CFGraphIso target.graph d.graph

The graph isomorphism from the positive contracted-core subdivision to the closed-face graph, preserving edge multiplicities.

Equations

• c.graphIso = { vertexEquiv := c.vertexEquiv, map_num_edges := ⋯ }

The translation lemma: strictly positive lengths

theorem Utilities.Certificate.DegenerateSpec.DegSpec.rep_eq_self_of_pos {n p : ℕ} (d : DegSpec n p) (hpos : ∀ (e : Fin p), 0 < d.length e) (v : Fin n) : d.rep v = v

At a strictly positive length vector the forest field forces rep to be the identity: there are no zero slots, so rep has n values, hence is surjective, hence bijective, hence — being idempotent — the identity.

def Utilities.Certificate.DegenerateSpec.DegSpec.toSpec {n p : ℕ} (d : DegSpec n p) (hpos : ∀ (e : Fin p), 0 < d.length e) : SubdivisionGraph.Spec n p

A degenerate spec with strictly positive lengths is an ordinary subdivision spec on the same core and lengths.

Equations

• d.toSpec hpos = { core := d.core, length := d.length, core_nonempty := ⋯, core_loopless := ⋯, length_pos := hpos }

def Utilities.Certificate.DegenerateSpec.DegSpec.toSpecContraction {n p : ℕ} (d : DegSpec n p) (hpos : ∀ (e : Fin p), 0 < d.length e) : d.Contraction (d.toSpec hpos)

The identity matching, exhibiting a strictly positive DegSpec as its own Spec.

Equations

• d.toSpecContraction hpos = { vtx := id, vtx_rep := ⋯, vtx_inj := ⋯, vtx_surj := ⋯, slot := id, slot_inj := ⋯, slot_surj := ⋯, length_eq := ⋯, tail_eq := ⋯, head_eq := ⋯ }

noncomputable def Utilities.Certificate.DegenerateSpec.DegSpec.laplacianEquivToSpec {n p : ℕ} (d : DegSpec n p) (hpos : ∀ (e : Fin p), 0 < d.length e) : LaplacianEquiv (d.toSpec hpos).graph d.graph

Translation lemma. Whatever a certificate proves about the degenerate graph at a strictly positive length vector, it proves about the genuine SubdivisionGraph.Spec subdivision there.

Equations

• d.laplacianEquivToSpec hpos = (d.toSpecContraction hpos).laplacianEquiv

theorem Utilities.Certificate.DegenerateSpec.DegSpec.bnExists_toSpec_iff {n p : ℕ} (d : DegSpec n p) (hpos : ∀ (e : Fin p), 0 < d.length e) (r deg : ℤ) : BNExists (d.toSpec hpos).graph r deg ↔ BNExists d.graph r deg

Core-supported divisors on a face

def Utilities.Certificate.DegenerateSpec.DegSpec.coreClassDivisor {n p : ℕ} (d : DegSpec n p) (weight : Fin n → ℤ) : CFDiv d.graph

Push arbitrary core weights to contracted core classes. A class carries the sum of its members' weights and subdivision-interior vertices carry zero.

Equations

• d.coreClassDivisor weight (Sum.inl c) = ∑ v : Fin n with d.rep v = ↑c, weight v
• d.coreClassDivisor weight (Sum.inr _interior) = 0

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.coreClassDivisor_coreVertex {n p : ℕ} (d : DegSpec n p) (weight : Fin n → ℤ) (r : Fin n) : d.coreClassDivisor weight (d.coreVertex r) = ∑ v : Fin n with d.rep v = d.rep r, weight v

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.coreClassDivisor_interiorVertex {n p : ℕ} (d : DegSpec n p) (weight : Fin n → ℤ) (e : Fin p) (o : Fin (d.length e - 1)) : d.coreClassDivisor weight (d.interiorVertex e o) = 0

theorem Utilities.Certificate.DegenerateSpec.DegSpec.coreClassDivisor_effective {n p : ℕ} (d : DegSpec n p) (weight : Fin n → ℤ) (hWeight : ∀ (v : Fin n), 0 ≤ weight v) : effective (d.coreClassDivisor weight)

Nonnegative source weights remain effective after classes are merged.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.one_le_classSum_of_chip {n p : ℕ} (d : DegSpec n p) (weight : Fin n → ℤ) (hWeight : ∀ (v : Fin n), 0 ≤ weight v) {c : Fin n} (hChip : 1 ≤ weight c) : 1 ≤ ∑ v : Fin n with d.rep v = d.rep c, weight v

A chip survives contraction. If the weights are nonnegative and c carries one, then the sum over c's contracted class is at least one: the other members of the class can only add.

This is the one fact every guarding row needs about its own chip vertices, and it was written out by hand — the same Finset.single_le_sum argument — in each of them. It is stated at the class sum rather than at coreClassDivisor because a row whose divisor carries interior chips as well (GenusFiveRow05, GenusFiveRow08, GenusFiveRow10) reduces to a class sum of a combined weight, not to a bare coreClassDivisor.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.one_le_coreClassDivisor_of_chip {n p : ℕ} (d : DegSpec n p) (weight : Fin n → ℤ) (hWeight : ∀ (v : Fin n), 0 ≤ weight v) {c : Fin n} (hChip : 1 ≤ weight c) : 1 ≤ d.coreClassDivisor weight (d.coreVertex c)

The coreClassDivisor reading of one_le_classSum_of_chip. This is the form Guarding.GuardingSet.one_le_divisor_of_chip is a corollary of.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.deg_coreClassDivisor {n p : ℕ} (d : DegSpec n p) (weight : Fin n → ℤ) : CFDiv.degree (d.coreClassDivisor weight) = ∑ v : Fin n, weight v

Contracting core classes preserves the total core weight.