Two canonical ramps meeting at an interior chip

SubdivisionArithmetic.potential realizes a rise over a slot by the convex two-slope interpolation, whose unit slopes are nondecreasing. That convexity is exactly what makes DegSpec.interpolatedScript's interior Laplacian nonnegative -- and exactly what makes a single ramp useless for a divisor whose chip sits inside a slot: a convex script never draws on that chip, so the row would have to succeed with the remaining core-supported chips alone.

Atanasov--Ranganathan's sixth and seventh genus-five families (rows 05 and 08 of the atlas) are of that kind: no core-supported degree-four divisor covers either row, and the figures place two of the four chips at interior points whose offset is a length.

This file supplies the replacement slot value. splitPotential L t first second is the canonical ramp of rise first over the first t unit steps, followed by the canonical ramp of rise second over the remaining L - t. It is convex on each side of t, and it may be concave exactly at t, where the divisor's chip pays for the deficit. splitStep_kink_ge_neg_one bounds that deficit by one chip, under a hypothesis every intended configuration has anyway: neither ramp is steeper than one unit per step, and one of the two is flat -- the chip is placed exactly where a flat stretch meets a full ramp.

Everything here is arithmetic on ℕ and ℤ. The layer that turns it into a firing script is generic already -- DegSpec.slotValueScript, DegSpec.SlotValueCompatible and DegSpec.IsStepSlope in Utilities/Subdivision/DegenerateSlopeScript.lean are stated for an arbitrary slot-value function, interpolatedScript being merely the instance whose value is one ramp.

structure Utilities.Certificate.SubdivisionArithmetic.SplitRamp (L t : ℕ) (first second : ℤ) : Prop

Admissibility of a split point. The two degeneracy clauses say that a ramp of length zero carries no rise; they hold in every intended use, where the split point is the position of a chip and a collapsed half means that chip has reached the core vertex at that end.

• le : t ≤ L
• first_zero : t = 0 → first = 0
• second_zero : t = L → second = 0

def Utilities.Certificate.SubdivisionArithmetic.splitPotential (L t : ℕ) (first second : ℤ) (i : ℕ) : ℤ

The value at offset i of the ramp of rise first over [0, t] followed by the ramp of rise second over [t, L].

Equations

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

def Utilities.Certificate.SubdivisionArithmetic.splitStep (L t : ℕ) (first second : ℤ) (i : ℕ) : ℤ

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

Equations

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

@[simp]

theorem Utilities.Certificate.SubdivisionArithmetic.potential_zero_zero_zero : potential 0 0 0 = 0

The two regimes

theorem Utilities.Certificate.SubdivisionArithmetic.splitPotential_of_lt {L t i : ℕ} {first second : ℤ} (h : i < t) : splitPotential L t first second i = potential t first i

theorem Utilities.Certificate.SubdivisionArithmetic.splitPotential_of_le {L t i : ℕ} {first second : ℤ} (h : t ≤ i) : splitPotential L t first second i = first + potential (L - t) second (i - t)

theorem Utilities.Certificate.SubdivisionArithmetic.potential_second_zero {L t : ℕ} {first second : ℤ} (h : SplitRamp L t first second) : potential (L - t) second 0 = 0

The second ramp starts at zero: either it has positive length, or the split point is the head and its rise vanishes.

Endpoint values

theorem Utilities.Certificate.SubdivisionArithmetic.splitPotential_zero {L t : ℕ} {first second : ℤ} (h : SplitRamp L t first second) : splitPotential L t first second 0 = 0

theorem Utilities.Certificate.SubdivisionArithmetic.splitPotential_length {L t : ℕ} {first second : ℤ} (h : SplitRamp L t first second) : splitPotential L t first second L = first + second

The two slope regimes

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_right {L t i : ℕ} {first second : ℤ} (hi : t ≤ i) : splitStep L t first second i = step (L - t) second (i - t)

At and above the split point the slope is the second ramp's, shifted.

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_left_of_lt {L t i : ℕ} {first second : ℤ} (h : i + 1 < t) : splitStep L t first second i = step t first i

Strictly below the split point the slope is the first ramp's.

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_left_of_succ_eq {L t i : ℕ} {first second : ℤ} (h : SplitRamp L t first second) (hi : i + 1 = t) : splitStep L t first second i = step t first i

The step ending at the split point is the first ramp's last step: the value at the split point is first, by potential_length.

@[simp]

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_mark_zero (L : ℕ) (first second : ℤ) (k : ℕ) : splitStep L 0 first second k = step L second k

An unmarked slot -- split point at the tail -- is the ordinary canonical ramp. This is what lets a row mark only the slots that carry an interior chip and keep the single-ramp ledger everywhere else.

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_left {L t i : ℕ} {first second : ℤ} (h : SplitRamp L t first second) (hi : i + 1 ≤ t) : splitStep L t first second i = step t first i

Below the split point the slope is the first ramp's.

The endpoint slopes are the surviving half's own endpoint slopes

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_first {L t : ℕ} {first second : ℤ} (h : SplitRamp L t first second) : splitStep L t first second 0 = if 0 < t then step t first 0 else step L second 0

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_last {L t : ℕ} {first second : ℤ} (h : SplitRamp L t first second) (hL : 0 < L) : splitStep L t first second (L - 1) = if t < L then step (L - t) second (L - 1 - t) else step L first (L - 1)

Convexity away from the split point, and the kink at it

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_mono_left {L t i j : ℕ} {first second : ℤ} (h : SplitRamp L t first second) (hij : i ≤ j) (hj : j + 1 ≤ t) : splitStep L t first second i ≤ splitStep L t first second j

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_mono_right {L t i j : ℕ} {first second : ℤ} (hij : i ≤ j) (hi : t ≤ i) : splitStep L t first second i ≤ splitStep L t first second j

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_kink_ge_neg_one {L t : ℕ} {first second : ℤ} (h : SplitRamp L t first second) (ht : 0 < t) (htL : t < L) (hfirstLe : first ≤ ↑t) (hsecond : -↑(L - t) ≤ second) (hflat : first = 0 ∨ second = 0) : -1 ≤ splitStep L t first second t - splitStep L t first second (t - 1)

The kink. Across the split point the slope can drop, but by at most one, provided neither half is steeper than one unit per step and one of the two is flat. A divisor with one chip at the split point therefore stays effective.

theorem Utilities.Certificate.SubdivisionArithmetic.splitStep_diff_nonneg_of_ne {L t i : ℕ} {first second : ℤ} (h : SplitRamp L t first second) (hk : 0 < i) (hne : i ≠ t) : 0 ≤ splitStep L t first second i - splitStep L t first second (i - 1)

Convexity at every interior offset other than the split point. This is what the DegSpec interior Laplacian consumes; at the split point itself the residual is paid for by the chip, via splitStep_kink_ge_neg_one.