Laplacians of subdivision scripts described by their unit-step slopes

ExplicitPotentialRankOne computes prin for the interpolated script, whose value along a slot is forced to be affine. Several all-length constructions need potentials that bend inside a slot, so this file records the same two formulas for an arbitrary firing script, keyed only on its unit-step differences.

A script is described here by a slope datum slope : Fin p → ℕ → ℤ together with the hypothesis that the script rises by slope edge k across the k-th unit step of slot edge. Then

• at a core vertex the Laplacian is the sum, over all slots, of the outgoing slope at each incident endpoint; and
• at an interior vertex it is the difference of the two adjacent slopes.

Both statements are exact, and neither refers to the values of the script.

def Utilities.Certificate.SubdivisionGraph.Spec.IsStepSlope {n p : ℕ} (spec : Spec n p) (script : firingScript spec.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.

Equations

• spec.IsStepSlope script slope = ∀ (edge : Fin p) (offset : Fin (spec.length edge)), script (spec.stepRight edge offset) - script (spec.stepLeft edge offset) = slope edge ↑offset

theorem Utilities.Certificate.SubdivisionGraph.Spec.sum_over_first_step {n p : ℕ} (spec : Spec n p) (edge : Fin p) (value : Fin (spec.length edge) → ℤ) : (∑ offset : Fin (spec.length edge), if ↑offset = 0 then value offset else 0) = value ⟨0, ⋯⟩

theorem Utilities.Certificate.SubdivisionGraph.Spec.sum_over_last_step {n p : ℕ} (spec : Spec n p) (edge : Fin p) (value : Fin (spec.length edge) → ℤ) : (∑ offset : Fin (spec.length edge), if ↑offset + 1 = spec.length edge then value offset else 0) = value ⟨spec.length edge - 1, ⋯⟩

theorem Utilities.Certificate.SubdivisionGraph.Spec.prin_eq_sum_slopes {n p : ℕ} (spec : Spec n p) {script : firingScript spec.graph} {slope : Fin p → ℕ → ℤ} (hslope : spec.IsStepSlope script slope) (vertex : spec.Vertex) : (prin spec.graph) script vertex = ∑ step : spec.Step, ((if spec.stepLeft step.fst step.snd = vertex then slope step.fst ↑step.snd else 0) + if spec.stepRight step.fst step.snd = vertex then -slope step.fst ↑step.snd else 0)

The Laplacian of any script, written entirely in terms of its unit-step slopes.

theorem Utilities.Certificate.SubdivisionGraph.Spec.prin_coreVertex_eq_endpointSum {n p : ℕ} (spec : Spec n p) {script : firingScript spec.graph} {slope : Fin p → ℕ → ℤ} (hslope : spec.IsStepSlope script slope) (vertex : Fin n) : (prin spec.graph) script (spec.coreVertex vertex) = ∑ edge : Fin p, ((if spec.core.tail edge = vertex then slope edge 0 else 0) + if spec.core.head edge = vertex then -slope edge (spec.length edge - 1) else 0)

At a core vertex, the Laplacian is the sum over all slots of the outgoing slope at each incident endpoint.

theorem Utilities.Certificate.SubdivisionGraph.Spec.prin_interiorVertex_eq_slopeDifference {n p : ℕ} (spec : Spec n p) {script : firingScript spec.graph} {slope : Fin p → ℕ → ℤ} (hslope : spec.IsStepSlope script slope) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : (prin spec.graph) script (spec.interiorVertex edge offset) = slope edge (↑offset + 1) - slope edge ↑offset

At an interior vertex, the Laplacian is the difference of the two adjacent slopes.

Scripts assembled from per-slot path values

def Utilities.Certificate.SubdivisionGraph.Spec.slotValueScript {n p : ℕ} (spec : Spec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) : firingScript spec.graph

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

Equations

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

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.slotValueScript_core {n p : ℕ} (spec : Spec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) (vertex : Fin n) : spec.slotValueScript potential value (spec.coreVertex vertex) = potential vertex

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.slotValueScript_interior {n p : ℕ} (spec : Spec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : spec.slotValueScript potential value (spec.interiorVertex edge offset) = value edge (↑offset + 1)

structure Utilities.Certificate.SubdivisionGraph.Spec.SlotValueCompatible {n p : ℕ} (spec : Spec n p) (potential : Fin n → ℤ) (value : Fin p → ℕ → ℤ) : Prop

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

• tail (edge : Fin p) : value edge 0 = potential (spec.core.tail edge)
• head (edge : Fin p) : value edge (spec.length edge) = potential (spec.core.head edge)

theorem Utilities.Certificate.SubdivisionGraph.Spec.slotValueScript_stepLeft {n p : ℕ} (spec : Spec n p) {potential : Fin n → ℤ} {value : Fin p → ℕ → ℤ} (hCompat : spec.SlotValueCompatible potential value) (edge : Fin p) (offset : Fin (spec.length edge)) : spec.slotValueScript potential value (spec.stepLeft edge offset) = value edge ↑offset

theorem Utilities.Certificate.SubdivisionGraph.Spec.slotValueScript_stepRight {n p : ℕ} (spec : Spec n p) {potential : Fin n → ℤ} {value : Fin p → ℕ → ℤ} (hCompat : spec.SlotValueCompatible potential value) (edge : Fin p) (offset : Fin (spec.length edge)) : spec.slotValueScript potential value (spec.stepRight edge offset) = value edge (↑offset + 1)

theorem Utilities.Certificate.SubdivisionGraph.Spec.isStepSlope_slotValueScript {n p : ℕ} (spec : Spec n p) {potential : Fin n → ℤ} {value : Fin p → ℕ → ℤ} (hCompat : spec.SlotValueCompatible potential value) : spec.IsStepSlope (spec.slotValueScript potential value) fun (edge : Fin p) (k : ℕ) => value edge (k + 1) - value edge k

The unit-step slopes of a compatible slot-value script are the forward differences of its path values.