Canonical integer interpolation on the CLOSED length orthant

This is the DegSpec counterpart of the interpolated layer of Certificate/SubdivisionGraph.lean (coreRise, pathValue, interpolatedScript) together with the two exact Laplacian formulas that Certificate/ExplicitPotentialRankOne.lean derives from it (prin_interpolatedScript_core_eq_endpointSum, prin_interpolatedScript_interior_eq_stepDifference).

Nothing in SubdivisionGraph.Spec is touched; these are separate statements about DegSpec.graph.

The one genuinely new hypothesis: RepInvariant

DegSpec.interpolatedScript has to be a function on the contracted vertex set, whose core summand is DegSpec.Class, not Fin n. Its value at the class of v can only be potential v if potential is constant on classes. That is RepInvariant, and it is genuinely an extra input:

• on the interior it is free (repInvariant_of_pos, since rep = id there);
• along a single collapsed slot it is free for a certificate potential, by ValidClosed's shared lowerForm/upperForm rows (ExplicitPotential.CertificateData.potential_eq_of_segment_eval_zero);
• on a whole class it is exactly the statement that rep merges only vertices joined by chains of collapsed slots. The forest field does not imply this (see the caveat in the design note), so it is supplied, and repInvariant_evaluatedPotential_of_zeroReach in Certificate/DegenerateRankOne.lean discharges it from such a chain.

Note that coreRise below is defined without rep, exactly as on a Spec. That is deliberate: it keeps coreRise (evaluatedPotential …) = riseValue definitionally, so the certificate's endpoint bounds apply verbatim. Under RepInvariant the two readings agree anyway (coreRise_eq_zero_of_length_zero).

Potentials constant on the contracted classes

def Utilities.Certificate.DegenerateSpec.DegSpec.RepInvariant {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) : Prop

A core potential that is constant on every contracted class.

Equations

• d.RepInvariant potential = ∀ (v : Fin n), potential (d.rep v) = potential v

theorem Utilities.Certificate.DegenerateSpec.DegSpec.repInvariant_of_pos {n p : ℕ} (d : DegSpec n p) (hpos : ∀ (e : Fin p), 0 < d.length e) (potential : Fin n → ℤ) : d.RepInvariant potential

On the interior of the orthant rep is the identity, so every potential is rep-invariant: the hypothesis costs nothing where the strictly positive layer already applies.

Rise, path value, interpolated script

def Utilities.Certificate.DegenerateSpec.DegSpec.coreRise {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (e : Fin p) : ℤ

Rise of a core potential along an oriented edge slot. Verbatim the Spec definition; no rep appears.

Equations

• d.coreRise potential e = potential (d.core.head e) - potential (d.core.tail e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.coreRise_eq_zero_of_length_zero {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) {e : Fin p} (hzero : d.length e = 0) : d.coreRise potential e = 0

A collapsed slot has zero rise, for any rep-invariant potential. This is what makes the arithmetic interpolator well behaved at length = 0, where SubdivisionArithmetic.potential_zero is unavailable.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.arith_potential_zero_rise (L i : ℕ) (hi : i ≤ L) : SubdivisionArithmetic.potential L 0 i = 0

The interpolator of a zero rise is identically zero up to the slot length. Needed at length = 0, where potential_zero and potential_length both require positivity.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.arith_potential_first {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (e : Fin p) : SubdivisionArithmetic.potential (d.length e) (d.coreRise potential e) 0 = 0

Normalization at the tail endpoint, valid on the closed orthant.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.arith_potential_last {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (e : Fin p) : SubdivisionArithmetic.potential (d.length e) (d.coreRise potential e) (d.length e) = d.coreRise potential e

Realization of the rise at the head endpoint, valid on the closed orthant.

def Utilities.Certificate.DegenerateSpec.DegSpec.pathValue {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (e : Fin p) (k : ℕ) : ℤ

Value at a numerical path offset, normalized by the tail potential.

Equations

• d.pathValue potential e k = potential (d.core.tail e) + Utilities.Certificate.SubdivisionArithmetic.potential (d.length e) (d.coreRise potential e) k

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

Extend a rep-invariant core potential over every surviving slot by the canonical convex interpolation. Collapsed slots contribute nothing: they carry no interior vertex and their two endpoints are already one class.

Equations

• d.interpolatedScript potential = d.slotValueScript potential (d.pathValue potential)

@[simp]

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

@[simp]

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

theorem Utilities.Certificate.DegenerateSpec.DegSpec.slotValueCompatible_pathValue {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) : d.SlotValueCompatible potential (d.pathValue potential)

The interpolated path values are compatible with the core potential at both endpoints of every slot, collapsed ones included.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.interpolatedScript_stepLeft {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (e : Fin p) (o : Fin (d.length e)) : d.interpolatedScript potential (d.stepLeft e o) = d.pathValue potential e ↑o

theorem Utilities.Certificate.DegenerateSpec.DegSpec.interpolatedScript_stepRight {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (e : Fin p) (o : Fin (d.length e)) : d.interpolatedScript potential (d.stepRight e o) = d.pathValue potential e (↑o + 1)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.isStepSlope_interpolatedScript {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) : d.IsStepSlope (d.interpolatedScript potential) fun (e : Fin p) (k : ℕ) => SubdivisionArithmetic.step (d.length e) (d.coreRise potential e) k

The script difference across a unit edge is the arithmetic interpolator's step slope.

The two exact Laplacian formulas

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_interpolatedScript_coreVertex_eq_endpointSum {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (r : Fin n) : (prin d.graph) (d.interpolatedScript potential) (d.coreVertex r) = ∑ e : Fin p, ((if d.rep (d.core.tail e) = d.rep r then SubdivisionArithmetic.step (d.length e) (d.coreRise potential e) 0 else 0) + if d.rep (d.core.head e) = d.rep r then -SubdivisionArithmetic.step (d.length e) (d.coreRise potential e) (d.length e - 1) else 0)

Core-class formula. At a contracted class only the first and last unit steps of the incident slots contribute, and the sum runs over every slot of the uncontracted core — collapsed ones cancel by zero_slot_cancels.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_interpolatedScript_coreVertex_eq_classSum {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (r : Fin n) : (prin d.graph) (d.interpolatedScript potential) (d.coreVertex r) = ∑ v : Fin n with d.rep v = d.rep r, ∑ e : Fin p, ((if d.core.tail e = v then SubdivisionArithmetic.step (d.length e) (d.coreRise potential e) 0 else 0) + if d.core.head e = v then -SubdivisionArithmetic.step (d.length e) (d.coreRise potential e) (d.length e - 1) else 0)

The reuse mechanism, for the interpolated layer. The Laplacian at a contracted class is the sum, over the members of that class, of the strictly positive per-core-vertex endpoint formula.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_interpolatedScript_interiorVertex_eq_stepDifference {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (e : Fin p) (o : Fin (d.length e - 1)) : (prin d.graph) (d.interpolatedScript potential) (d.interiorVertex e o) = SubdivisionArithmetic.step (d.length e) (d.coreRise potential e) (↑o + 1) - SubdivisionArithmetic.step (d.length e) (d.coreRise potential e) ↑o

Interior formula. Unchanged in shape: an interior vertex exists only on a slot of length at least two.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_interpolatedScript_interiorVertex_nonneg {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} (hInv : d.RepInvariant potential) (e : Fin p) (o : Fin (d.length e - 1)) : 0 ≤ (prin d.graph) (d.interpolatedScript potential) (d.interiorVertex e o)

Convexity of the interpolator: the interior Laplacian coefficient is non-negative.

Path positions from numerical offsets

SubdivisionGraph.Spec.pathPosition lives in Certificate/MovingPosition.lean; this is its DegSpec counterpart, needed by the affine position decoder. The consumer-facing difference is the trichotomy: pathVertex_zero, pathVertex_length and pathVertex_interior are three separate cases, and at a collapsed slot the first two coincide.

def Utilities.Certificate.DegenerateSpec.DegSpec.pathPosition {n p : ℕ} (d : DegSpec n p) (e : Fin p) (offset : ℕ) (hOffset : offset ≤ d.length e) : d.PathPosition e

The path position at a numerical offset known not to pass the head.

Equations

• d.pathPosition e offset hOffset = ⟨offset, ⋯⟩

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathPosition_val {n p : ℕ} (d : DegSpec n p) (e : Fin p) (offset : ℕ) (hOffset : offset ≤ d.length e) : ↑(d.pathPosition e offset hOffset) = offset

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_pathPosition_zero {n p : ℕ} (d : DegSpec n p) (e : Fin p) (hOffset : 0 ≤ d.length e) : d.pathVertex e (d.pathPosition e 0 hOffset) = d.coreVertex (d.core.tail e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_pathPosition_length {n p : ℕ} (d : DegSpec n p) (e : Fin p) (hOffset : d.length e ≤ d.length e) : d.pathVertex e (d.pathPosition e (d.length e) hOffset) = d.coreVertex (d.core.head e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_pathPosition_interior {n p : ℕ} (d : DegSpec n p) (e : Fin p) (offset : ℕ) (hOffset : offset ≤ d.length e) (hZero : offset ≠ 0) (hLast : offset ≠ d.length e) : d.pathVertex e (d.pathPosition e offset hOffset) = d.interiorVertex e ⟨offset - 1, ⋯⟩

theorem Utilities.Certificate.DegenerateSpec.DegSpec.pathVertex_pathPosition_trichotomy {n p : ℕ} (d : DegSpec n p) (e : Fin p) (offset : ℕ) (hOffset : offset ≤ d.length e) : d.pathVertex e (d.pathPosition e offset hOffset) = d.coreVertex (d.core.tail e) ∨ d.pathVertex e (d.pathPosition e offset hOffset) = d.coreVertex (d.core.head e) ∨ ∃ (o : Fin (d.length e - 1)), d.pathVertex e (d.pathPosition e offset hOffset) = d.interiorVertex e o

The trichotomy, in one statement. On the closed orthant a numerical path offset lands on the tail class, the head class, or an interior vertex — the positive-world two-case split (offset = 0 versus offset > 0 ⟹ interior) has no case for offset = length.