Canonical piecewise interpolation on closed subdivision faces

A PiecewiseData describes a path potential by its successive block ends and the total rise of each block. The slope inside a block is not supplied by a certificate: it is the canonical integer interpolation slope for that block's length and rise. Thus the only interior coefficients which a leaf needs to check separately are the block boundaries.

The data deliberately uses a selector rather than a list traversal. A lowerer can decode its finite block list into blockAt; covers is the small, arithmetic statement that the selected block contains every surviving unit step. This formulation is also meaningful on a closed face: a zero-length slot has no selected step, and balance then forces its two endpoint values to coincide.

def Utilities.Certificate.DegenerateSpec.DegSpec.blockStart {p : ℕ} (blockEnd : Fin p → ℕ → ℕ) (e : Fin p) (block : ℕ) : ℕ

The left endpoint of a block. Block zero starts at the tail; every later block starts where its predecessor ended.

Equations

• Utilities.Certificate.DegenerateSpec.DegSpec.blockStart blockEnd e block = if block = 0 then 0 else blockEnd e (block - 1)

def Utilities.Certificate.DegenerateSpec.DegSpec.blockSlope {p : ℕ} (blockAt blockEnd : Fin p → ℕ → ℕ) (blockRise : Fin p → ℕ → ℤ) (e : Fin p) (k : ℕ) : ℤ

The canonical slope at a unit step, selected from its containing block.

Equations

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

structure Utilities.Certificate.DegenerateSpec.DegSpec.PiecewiseData {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) : Type

Block-end/rise data for a canonically interpolated piecewise script.

blockEnd e j is the right endpoint of block j; the preceding endpoint is blockStart e j. blockAt selects the block containing a surviving step. The latter is intentionally a semantic finite-data interface: list indexing, ordering, and affine endpoint decoding belong in the lowering layer, while the proof below only needs the displayed containment inequalities.

• blockAt : Fin p → ℕ → ℕ

  The selected block for a slot and unit-step index; the containment laws constrain every surviving step.

• blockEnd : Fin p → ℕ → ℕ

  The right endpoint position of each block on each slot.

• blockRise : Fin p → ℕ → ℤ

  The prescribed total integer rise of each block, used to determine its canonical interpolation slopes.

• covers (e : Fin p) (k : ℕ) : k < d.length e → blockStart self.blockEnd e (self.blockAt e k) ≤ k ∧ k < self.blockEnd e (self.blockAt e k)
• ownsInterval (e : Fin p) (block k : ℕ) : blockStart self.blockEnd e block ≤ k → k < self.blockEnd e block → self.blockAt e k = block
• balance (e : Fin p) : potential (d.core.head e) = potential (d.core.tail e) + ∑ k ∈ Finset.range (d.length e), blockSlope self.blockAt self.blockEnd self.blockRise e k

theorem Utilities.Certificate.DegenerateSpec.DegSpec.blockSlope_eq_of_mem {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (edge : Fin p) (block k : ℕ) (hStart : blockStart data.blockEnd edge block ≤ k) (hEnd : k < data.blockEnd edge block) : blockSlope data.blockAt data.blockEnd data.blockRise edge k = SubdivisionArithmetic.step (data.blockEnd edge block - blockStart data.blockEnd edge block) (data.blockRise edge block) (k - blockStart data.blockEnd edge block)

Inside a declared block, the selected slope is exactly that block's canonical interpolation slope. This is the direct W2-facing reading of a block endpoint/rise pair.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.lower_le_blockSlope_of_mul_le {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (edge : Fin p) (k : ℕ) (lo : ℤ) (hk : k < d.length edge) (hLower : lo * ↑(data.blockEnd edge (data.blockAt edge k) - blockStart data.blockEnd edge (data.blockAt edge k)) ≤ data.blockRise edge (data.blockAt edge k)) : lo ≤ blockSlope data.blockAt data.blockEnd data.blockRise edge k

W2 bounds on the total rise of the selected nonempty block bound every canonical unit slope of its integer interpolation. This is the precise bridge used by a rich leaf's W4 boundary residual: it does not assume that the endpoint list has no repeated entries.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.blockSlope_le_upper_of_le_mul {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (edge : Fin p) (k : ℕ) (hi : ℤ) (hk : k < d.length edge) (hUpper : data.blockRise edge (data.blockAt edge k) ≤ hi * ↑(data.blockEnd edge (data.blockAt edge k) - blockStart data.blockEnd edge (data.blockAt edge k))) : blockSlope data.blockAt data.blockEnd data.blockRise edge k ≤ hi

The upper-half of the selected canonical slope bound.

def Utilities.Certificate.DegenerateSpec.DegSpec.piecewiseValue {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} (data : d.PiecewiseData potential) : Fin p → ℕ → ℤ

The path values obtained by accumulating the canonical selected slopes.

Equations

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

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

The resulting firing script on the contracted subdivision.

Equations

• Utilities.Certificate.DegenerateSpec.DegSpec.piecewiseScript data = d.slotValueScript potential (Utilities.Certificate.DegenerateSpec.DegSpec.piecewiseValue data)

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.piecewiseValue_zero {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (e : Fin p) : piecewiseValue data e 0 = potential (d.core.tail e)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.slotValueCompatible_piecewiseValue {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (hInv : d.RepInvariant potential) : d.SlotValueCompatible potential (piecewiseValue data)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.isStepSlope_piecewiseScript {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (hInv : d.RepInvariant potential) : d.IsStepSlope (piecewiseScript data) fun (e : Fin p) (k : ℕ) => blockSlope data.blockAt data.blockEnd data.blockRise e k

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_piecewiseScript_coreVertex {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (hInv : d.RepInvariant potential) (vertex : Fin n) : (prin d.graph) (piecewiseScript data) (d.coreVertex vertex) = ∑ edge : Fin p, ((if d.rep (d.core.tail edge) = d.rep vertex then blockSlope data.blockAt data.blockEnd data.blockRise edge 0 else 0) + if d.rep (d.core.head edge) = d.rep vertex then -blockSlope data.blockAt data.blockEnd data.blockRise edge (d.length edge - 1) else 0)

Exact endpoint formula at a contracted core class. In particular this retains all collapsed slots; their two displayed endpoint terms cancel.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_piecewiseScript_coreVertex_eq_classSum {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (hInv : d.RepInvariant potential) (vertex : Fin n) : (prin d.graph) (piecewiseScript data) (d.coreVertex vertex) = ∑ v : Fin n with d.rep v = d.rep vertex, ∑ edge : Fin p, ((if d.core.tail edge = v then blockSlope data.blockAt data.blockEnd data.blockRise edge 0 else 0) + if d.core.head edge = v then -blockSlope data.blockAt data.blockEnd data.blockRise edge (d.length edge - 1) else 0)

The quotient-core version of the endpoint formula. It expands a contracted class into its original core vertices, which is the form needed to combine W5's per-anchor residuals with chips that have slid onto a face.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_piecewiseScript_interiorVertex {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (hInv : d.RepInvariant potential) (edge : Fin p) (offset : Fin (d.length edge - 1)) : (prin d.graph) (piecewiseScript data) (d.interiorVertex edge offset) = blockSlope data.blockAt data.blockEnd data.blockRise edge (↑offset + 1) - blockSlope data.blockAt data.blockEnd data.blockRise edge ↑offset

Exact interior formula: the coefficient is the jump of the two selected canonical block slopes.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_piecewiseScript_interiorVertex_nonneg_of_sameBlock {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {data : d.PiecewiseData potential} (hInv : d.RepInvariant potential) (edge : Fin p) (offset : Fin (d.length edge - 1)) (hSame : data.blockAt edge (↑offset + 1) = data.blockAt edge ↑offset) : 0 ≤ (prin d.graph) (piecewiseScript data) (d.interiorVertex edge offset)

Away from a block boundary the two adjacent unit steps are selected from the same canonical interpolator, hence the interior coefficient is non-negative. W4 need only check the omitted boundary case.