Firing scripts, potentials and the Laplacian on the closed length orthant

This is the DegSpec counterpart of Certificate/SubdivisionGraph.lean's prin_eq_sum_steps and of Certificate/SlopeScript.lean. Nothing in SubdivisionGraph.Spec or SlopeScript is touched; these are separate statements about DegSpec.graph, so the strictly positive path keeps working verbatim while the closed-orthant path is proved out beside it.

The one statement that makes the whole design pay

prin_coreVertex_eq_endpointSum below is word for word the Spec statement with rep applied to the two endpoints:

prin d.graph script (d.coreVertex r) =
  ∑ e : Fin p, ((if d.rep (d.core.tail e) = d.rep r then slope e 0 else 0) +
                (if d.rep (d.core.head e) = d.rep r then
                   -slope e (d.length e - 1) else 0))

In particular the sum still runs over every slot of the uncontracted core, vanishing slots included. That is not an accident and it is not free: a vanishing slot emits no unit steps, so it contributes nothing to the left-hand side, and it contributes nothing to the right-hand side either because its two endpoints lie in one rep-class (rep_zero) and its two endpoint terms are slope e 0 and -slope e (d.length e - 1) = -slope e 0. That is exactly DegSpec.zero_slot_cancels.

Consequently prin_coreVertex_eq_classSum says the Laplacian at a contracted class is the sum over the class members of the uncontracted per-vertex formula. A row's per-core-vertex value lemmas are therefore reusable at every face by addition, rather than being reproved once per face. That is the whole economic argument for the closed-orthant layer, and it is a theorem here.

Which unit steps meet a given vertex

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

The step immediately before the interior vertex with coordinate j.

Equations

• d.previousStep e o = ⟨↑o, ⋯⟩

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

The step immediately after the interior vertex with coordinate j.

Equations

• d.nextStep e o = ⟨↑o + 1, ⋯⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.stepLeft_eq_coreVertex_iff {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e)) (v : Fin n) : d.stepLeft e o = d.coreVertex v ↔ ↑o = 0 ∧ d.rep (d.core.tail e) = d.rep v

theorem Utilities.Certificate.DegenerateSpec.DegSpec.stepRight_eq_coreVertex_iff {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e)) (v : Fin n) : d.stepRight e o = d.coreVertex v ↔ ↑o + 1 = d.length e ∧ d.rep (d.core.head e) = d.rep v

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.stepRight_previousStep {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e - 1)) : d.stepRight e (d.previousStep e o) = d.interiorVertex e o

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.stepLeft_nextStep {n p : ℕ} (d : DegSpec n p) (e : Fin p) (o : Fin (d.length e - 1)) : d.stepLeft e (d.nextStep e o) = d.interiorVertex e o

theorem Utilities.Certificate.DegenerateSpec.DegSpec.stepRight_eq_interiorVertex_iff {n p : ℕ} (d : DegSpec n p) (s : d.Step) (e : Fin p) (o : Fin (d.length e - 1)) : d.stepRight s.fst s.snd = d.interiorVertex e o ↔ s = ⟨e, d.previousStep e o⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.stepLeft_eq_interiorVertex_iff {n p : ℕ} (d : DegSpec n p) (s : d.Step) (e : Fin p) (o : Fin (d.length e - 1)) : d.stepLeft s.fst s.snd = d.interiorVertex e o ↔ s = ⟨e, d.nextStep e o⟩

The Laplacian as a sum over unit steps

theorem Utilities.Certificate.DegenerateSpec.DegSpec.num_edges_eq_sum_steps {n p : ℕ} (d : DegSpec n p) (x y : d.Vertex) : numEdges d.graph x y = ∑ s : d.Step, if d.unitEdge s = (x, y) ∨ d.unitEdge s = (y, x) then 1 else 0

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_eq_sum_steps {n p : ℕ} (d : DegSpec n p) (script : firingScript d.graph) (v : d.Vertex) : (prin d.graph) script v = ∑ s : d.Step, ((if d.stepLeft s.fst s.snd = v then script (d.stepRight s.fst s.snd) - script v else 0) + if d.stepRight s.fst s.snd = v then script (d.stepLeft s.fst s.snd) - script v else 0)

Slope data

def Utilities.Certificate.DegenerateSpec.DegSpec.IsStepSlope {n p : ℕ} (d : DegSpec n p) (script : firingScript d.graph) (slope : Fin p → ℕ → ℤ) : Prop

A slope datum for a firing script: the script rises by slope edge k across the k-th unit step of slot edge. Vanishing slots impose no condition, since they carry no unit step.

Equations

• d.IsStepSlope script slope = ∀ (e : Fin p) (o : Fin (d.length e)), script (d.stepRight e o) - script (d.stepLeft e o) = slope e ↑o

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_eq_sum_slopes {n p : ℕ} (d : DegSpec n p) {script : firingScript d.graph} {slope : Fin p → ℕ → ℤ} (hslope : d.IsStepSlope script slope) (v : d.Vertex) : (prin d.graph) script v = ∑ s : d.Step, ((if d.stepLeft s.fst s.snd = v then slope s.fst ↑s.snd else 0) + if d.stepRight s.fst s.snd = v then -slope s.fst ↑s.snd else 0)

Endpoint sums, including the vanishing slots

theorem Utilities.Certificate.DegenerateSpec.DegSpec.sum_over_first_step {n p : ℕ} (d : DegSpec n p) {e : Fin p} (hpos : 0 < d.length e) (value : Fin (d.length e) → ℤ) : (∑ o : Fin (d.length e), if ↑o = 0 then value o else 0) = value ⟨0, hpos⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.sum_over_last_step {n p : ℕ} (d : DegSpec n p) {e : Fin p} (hpos : 0 < d.length e) (value : Fin (d.length e) → ℤ) : (∑ o : Fin (d.length e), if ↑o + 1 = d.length e then value o else 0) = value ⟨d.length e - 1, ⋯⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_coreVertex_eq_endpointSum {n p : ℕ} (d : DegSpec n p) {script : firingScript d.graph} {slope : Fin p → ℕ → ℤ} (hslope : d.IsStepSlope script slope) (r : Fin n) : (prin d.graph) script (d.coreVertex r) = ∑ e : Fin p, ((if d.rep (d.core.tail e) = d.rep r then slope e 0 else 0) + if d.rep (d.core.head e) = d.rep r then -slope e (d.length e - 1) else 0)

The load-bearing formula. At a contracted core class the Laplacian is the endpoint sum over all slots of the uncontracted core. Vanishing slots appear in the sum and contribute zero, by zero_slot_cancels.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_interiorVertex_eq_slopeDifference {n p : ℕ} (d : DegSpec n p) {script : firingScript d.graph} {slope : Fin p → ℕ → ℤ} (hslope : d.IsStepSlope script slope) (e : Fin p) (o : Fin (d.length e - 1)) : (prin d.graph) script (d.interiorVertex e o) = slope e (↑o + 1) - slope e ↑o

At an interior vertex the Laplacian is the difference of the two adjacent slopes. Unchanged in form from the strictly positive case: an interior vertex only ever exists on a slot of length at least two.

The fibre form: a row's per-core-vertex lemmas, reused by addition

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_coreVertex_eq_classSum {n p : ℕ} (d : DegSpec n p) {script : firingScript d.graph} {slope : Fin p → ℕ → ℤ} (hslope : d.IsStepSlope script slope) (r : Fin n) : (prin d.graph) script (d.coreVertex r) = ∑ v : Fin n with d.rep v = d.rep r, ∑ e : Fin p, ((if d.core.tail e = v then slope e 0 else 0) + if d.core.head e = v then -slope e (d.length e - 1) else 0)

Additivity across a face. The Laplacian at a contracted class is the sum, over the members of that class, of the uncontracted per-core-vertex endpoint formula — the same expression SlopeScript's prin_coreVertex_eq_endpointSum produces on a strictly positive Spec.

This is what makes a retrofit additive rather than per-face: a row proves its value lemmas once, at each of the n core vertices, and every face reads them off by summing over classes.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.sum_nonneg_of_members {n p : ℕ} (d : DegSpec n p) {F : Fin n → ℤ} (r : Fin n) (h : ∀ (v : Fin n), 0 ≤ F v) : 0 ≤ ∑ v : Fin n with d.rep v = d.rep r, F v

Effectivity transfers across a face for free: a class value is a sum of member values.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.le_sum_of_member {n p : ℕ} (d : DegSpec n p) {F : Fin n → ℤ} (r u : Fin n) (hu : d.rep u = d.rep r) (h : ∀ (v : Fin n), 0 ≤ F v) : F u ≤ ∑ v : Fin n with d.rep v = d.rep r, F v

Reachability transfers across a face for free: a class value dominates any one member's value once every member is non-negative.

Scripts assembled from per-slot path values

def Utilities.Certificate.DegenerateSpec.DegSpec.slotValueScript {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) : firingScript d.graph

The script whose value at path position k of slot edge is value edge k, and potential (rep v) at the class of the core vertex v.

Equations

• d.slotValueScript potential value (Sum.inl c) = potential ↑c
• d.slotValueScript potential value (Sum.inr interior) = value interior.fst (↑interior.snd + 1)

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.slotValueScript_core {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) (v : Fin n) : d.slotValueScript potential value (d.coreVertex v) = potential (d.rep v)

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.slotValueScript_interior {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) (e : Fin p) (o : Fin (d.length e - 1)) : d.slotValueScript potential value (d.interiorVertex e o) = value e (↑o + 1)

structure Utilities.Certificate.DegenerateSpec.DegSpec.SlotValueCompatible {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) : Prop

Compatibility of the per-slot values with the core potential.

On a vanishing slot the two conditions collide at index 0 and force potential (rep (tail e)) = potential (rep (head e)) — which rep_zero already grants. So a compatible slot-value script is automatically a well-defined function on the contracted graph, with no extra field.

• tail (e : Fin p) : value e 0 = potential (d.rep (d.core.tail e))
• head (e : Fin p) : value e (d.length e) = potential (d.rep (d.core.head e))

theorem Utilities.Certificate.DegenerateSpec.DegSpec.slotValueScript_stepLeft {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {value : Fin p → ℕ → ℤ} (hCompat : d.SlotValueCompatible potential value) (e : Fin p) (o : Fin (d.length e)) : d.slotValueScript potential value (d.stepLeft e o) = value e ↑o

theorem Utilities.Certificate.DegenerateSpec.DegSpec.slotValueScript_stepRight {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {value : Fin p → ℕ → ℤ} (hCompat : d.SlotValueCompatible potential value) (e : Fin p) (o : Fin (d.length e)) : d.slotValueScript potential value (d.stepRight e o) = value e (↑o + 1)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.isStepSlope_slotValueScript {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {value : Fin p → ℕ → ℤ} (hCompat : d.SlotValueCompatible potential value) : d.IsStepSlope (d.slotValueScript potential value) fun (e : Fin p) (k : ℕ) => value e (k + 1) - value e k

Agreement with the strictly positive layer

At a strictly positive length vector rep is the identity, so every statement above is the corresponding SlopeScript statement transported along laplacianEquivToSpec. Nothing in SlopeScript is restated or weakened.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.isStepSlope_congr {n p : ℕ} (d : DegSpec n p) {script : firingScript d.graph} {slope slope' : Fin p → ℕ → ℤ} (h : ∀ (e : Fin p), ∀ k < d.length e, slope e k = slope' e k) (hslope : d.IsStepSlope script slope) : d.IsStepSlope script slope'

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

On the interior the class sum degenerates to a single term, so prin_coreVertex_eq_classSum reduces literally to the Spec formula.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_coreVertex_eq_endpointSum_of_pos {n p : ℕ} (d : DegSpec n p) {script : firingScript d.graph} {slope : Fin p → ℕ → ℤ} (hslope : d.IsStepSlope script slope) (hpos : ∀ (e : Fin p), 0 < d.length e) (r : Fin n) : (prin d.graph) script (d.coreVertex r) = ∑ e : Fin p, ((if d.core.tail e = r then slope e 0 else 0) + if d.core.head e = r then -slope e (d.length e - 1) else 0)

Consistency with the strictly positive layer: on the interior the class sum collapses to a single term and the formula is literally SubdivisionGraph.Spec.prin_coreVertex_eq_endpointSum.