Integer interpolation along a subdivided edge

This file isolates the arithmetic needed to turn integral endpoint potentials into a convex integral potential on a path. It deliberately contains no graph construction.

For a positive length L and an integral rise T, write

T = q * L + r, with 0 <= r < L.

The potential below has slope q for the first L - r unit steps and slope q + 1 for the final r steps. Thus it has endpoint values 0 and T, and its slopes are nondecreasing. The sign convention is chosen for the future chip-firing application: at an interior path vertex, prin will be the next slope minus the previous slope.

def Utilities.Certificate.SubdivisionArithmetic.quotient (L : ℕ) (T : ℤ) : ℤ

The lower of the two slopes used to realize rise T over length L.

Equations

• Utilities.Certificate.SubdivisionArithmetic.quotient L T = T / ↑L

def Utilities.Certificate.SubdivisionArithmetic.remainder (L : ℕ) (T : ℤ) : ℤ

The number of final steps on which the slope is quotient L T + 1.

Equations

• Utilities.Certificate.SubdivisionArithmetic.remainder L T = T % ↑L

def Utilities.Certificate.SubdivisionArithmetic.bend (L : ℕ) (T : ℤ) : ℤ

The integral offset at which the slope changes from q to q + 1.

Equations

• Utilities.Certificate.SubdivisionArithmetic.bend L T = ↑L - Utilities.Certificate.SubdivisionArithmetic.remainder L T

def Utilities.Certificate.SubdivisionArithmetic.potential (L : ℕ) (T : ℤ) (i : ℕ) : ℤ

The two-slope potential at integral offset i from the tail endpoint.

Equations

• Utilities.Certificate.SubdivisionArithmetic.potential L T i = Utilities.Certificate.SubdivisionArithmetic.quotient L T * ↑i + max 0 (↑i - Utilities.Certificate.SubdivisionArithmetic.bend L T)

def Utilities.Certificate.SubdivisionArithmetic.step (L : ℕ) (T : ℤ) (i : ℕ) : ℤ

The slope on the unit step from offset i to offset i + 1.

Equations

• Utilities.Certificate.SubdivisionArithmetic.step L T i = Utilities.Certificate.SubdivisionArithmetic.potential L T (i + 1) - Utilities.Certificate.SubdivisionArithmetic.potential L T i

theorem Utilities.Certificate.SubdivisionArithmetic.sum_steps (L : ℕ) (T : ℤ) : ∑ i ∈ Finset.range L, step L T i = potential L T L - potential L T 0

The canonical unit slopes telescope to the difference of the endpoint values. Unlike potential_length, this identity is also meaningful at length zero.

theorem Utilities.Certificate.SubdivisionArithmetic.remainder_nonneg {L : ℕ} (T : ℤ) (hL : 0 < L) : 0 ≤ remainder L T

theorem Utilities.Certificate.SubdivisionArithmetic.remainder_lt {L : ℕ} (T : ℤ) (hL : 0 < L) : remainder L T < ↑L

theorem Utilities.Certificate.SubdivisionArithmetic.bend_pos {L : ℕ} (T : ℤ) (hL : 0 < L) : 0 < bend L T

theorem Utilities.Certificate.SubdivisionArithmetic.bend_le_length {L : ℕ} (T : ℤ) (hL : 0 < L) : bend L T ≤ ↑L

@[simp]

theorem Utilities.Certificate.SubdivisionArithmetic.potential_zero {L : ℕ} (T : ℤ) (hL : 0 < L) : potential L T 0 = 0

The potential is normalized to zero at the tail endpoint.

@[simp]

theorem Utilities.Certificate.SubdivisionArithmetic.potential_length {L : ℕ} (T : ℤ) (hL : 0 < L) : potential L T L = T

The potential realizes the prescribed rise at the head endpoint.

theorem Utilities.Certificate.SubdivisionArithmetic.sum_steps_eq_rise {L : ℕ} (T : ℤ) (hL : 0 < L) : ∑ i ∈ Finset.range L, step L T i = T

On a nonempty block, the canonical unit slopes realize its declared rise. This is the telescoping fact used when concatenating piecewise blocks.

theorem Utilities.Certificate.SubdivisionArithmetic.step_eq_quotient_of_succ_le_bend {L i : ℕ} {T : ℤ} (hi : ↑(i + 1) ≤ bend L T) : step L T i = quotient L T

Before the bend, the unit-step slope is exactly the quotient q.

theorem Utilities.Certificate.SubdivisionArithmetic.step_eq_quotient_add_one_of_bend_le {L i : ℕ} {T : ℤ} (hi : bend L T ≤ ↑i) : step L T i = quotient L T + 1

At and after the bend, the unit-step slope is q + 1.

theorem Utilities.Certificate.SubdivisionArithmetic.step_eq_quotient_or_add_one (L i : ℕ) (T : ℤ) : step L T i = quotient L T ∨ step L T i = quotient L T + 1

Every unit-step slope is one of the two consecutive integers q, q+1.

theorem Utilities.Certificate.SubdivisionArithmetic.step_mono {L i j : ℕ} {T : ℤ} (hij : i ≤ j) : step L T i ≤ step L T j

The two-slope sequence is nondecreasing.

theorem Utilities.Certificate.SubdivisionArithmetic.lower_le_step_of_mul_le {L i : ℕ} (rise lo : ℤ) (hL : 0 < L) (hLower : lo * ↑L ≤ rise) : lo ≤ step L rise i

A canonical unit slope is at least any declared lower endpoint bound whose total rise is feasible. This is the W2 arithmetic bridge used when a piecewise block contributes the outgoing slope at a merged boundary.

theorem Utilities.Certificate.SubdivisionArithmetic.step_le_upper_of_le_mul {L i : ℕ} (rise hi : ℤ) (hL : 0 < L) (hiStep : i < L) (hUpper : rise ≤ hi * ↑L) : step L rise i ≤ hi

A canonical unit slope is at most any declared upper endpoint bound whose total rise is feasible. The strict case uses the quotient bound; at equality the Euclidean remainder vanishes, so every genuine unit step is the quotient itself.

theorem Utilities.Certificate.SubdivisionArithmetic.secondDifference_nonneg (L i : ℕ) (T : ℤ) : 0 ≤ potential L T i - 2 * potential L T (i + 1) + potential L T (i + 2)

Convexity in the form needed at an interior path vertex: the next slope minus the previous slope is nonnegative. Offset i + 1 is interior whenever i + 1 < L; the inequality itself holds without that extra restriction.

theorem Utilities.Certificate.SubdivisionArithmetic.interiorSecondDifference_nonneg {L i : ℕ} (T : ℤ) (hi : 0 < i) : 0 ≤ potential L T (i - 1) - 2 * potential L T i + potential L T (i + 1)

Centered form of secondDifference_nonneg, ready to identify with prin at a positive interior offset.

theorem Utilities.Certificate.SubdivisionArithmetic.firstStep_eq_quotient {L : ℕ} (T : ℤ) (hL : 0 < L) : step L T 0 = quotient L T

The first slope is the Euclidean quotient.

theorem Utilities.Certificate.SubdivisionArithmetic.lastStep_eq_ite {L : ℕ} (T : ℤ) (hL : 0 < L) : step L T (L - 1) = if remainder L T = 0 then quotient L T else quotient L T + 1

The final slope is q when the rise is divisible by the length and q + 1 otherwise.

theorem Utilities.Certificate.SubdivisionArithmetic.lastStep_eq_neg_ediv_neg {L : ℕ} (T : ℤ) (hL : 0 < L) : step L T (L - 1) = -(-T / ↑L)

Equivalently, the final slope is the ceiling of T / L, expressed using integer Euclidean division and no rational arithmetic.

theorem Utilities.Certificate.SubdivisionArithmetic.endpointSlopeBounds {L : ℕ} (T alpha beta : ℤ) (hL : 0 < L) (hlower : alpha * ↑L ≤ T) (hupper : T ≤ -beta * ↑L) : alpha ≤ step L T 0 ∧ beta ≤ -step L T (L - 1)

Lower bounds on the two outgoing endpoint slopes follow from the homogeneous rise bounds used by local subdivision certificates.

Closed arithmetic regressions

theorem Utilities.Certificate.SubdivisionArithmetic.negativeNondivisible_steps : step 3 (-1) 0 = -1 ∧ step 3 (-1) 1 = 0 ∧ step 3 (-1) 2 = 0

A negative, nondivisible rise uses the floor quotient first and the next integer on the remaining steps.

theorem Utilities.Certificate.SubdivisionArithmetic.negativeDivisible_steps : step 3 (-6) 0 = -2 ∧ step 3 (-6) 1 = -2 ∧ step 3 (-6) 2 = -2

A negative rise divisible by the path length has constant slope.

theorem Utilities.Certificate.SubdivisionArithmetic.lengthOne_step (T : ℤ) : step 1 T 0 = T

On a path of length one, the unique step realizes every integral rise.

theorem Utilities.Certificate.SubdivisionArithmetic.step_zero_of_lt {L i : ℕ} (hi : i < L) : step L 0 i = 0

A path with equal endpoint potentials has zero slope on each of its actual unit steps.

A truncated negative ramp

The loop lemma needs the potential of rise -k along a path of length L, where 0 < k ≤ L. It falls with slope -1 for exactly k steps and is constant afterwards. Thus it places one unit of Laplacian at distance k from the zero endpoint (unless that point is the far endpoint).

theorem Utilities.Certificate.SubdivisionArithmetic.quotient_neg_eq_neg_one {L k : ℕ} (hk : 0 < k) (hkL : k ≤ L) : quotient L (-↑k) = -1

Euclidean division of -k by a positive L, for 0 < k ≤ L.

theorem Utilities.Certificate.SubdivisionArithmetic.remainder_neg_eq_sub {L k : ℕ} (hk : 0 < k) (hkL : k ≤ L) : remainder L (-↑k) = ↑L - ↑k

The complementary remainder in the same negative division.

theorem Utilities.Certificate.SubdivisionArithmetic.bend_neg_eq {L k : ℕ} (hk : 0 < k) (hkL : k ≤ L) : bend L (-↑k) = ↑k

The unique bend of the truncated negative ramp is at offset k.

theorem Utilities.Certificate.SubdivisionArithmetic.step_neg_eq_ite {L k i : ℕ} (hk : 0 < k) (hkL : k ≤ L) : step L (-↑k) i = if i < k then -1 else 0

The truncated negative ramp has slope -1 before k and zero from k onwards.