Ramp firing scripts on positive subdivisions

A ramp is constant, then affine with slope -1, 0, or 1 on a bounded window of each edge slot, then constant again. This is the generic positive- length infrastructure behind the readable genus-four pencil proofs.

theorem Utilities.Certificate.SubdivisionRamp.divisor_ext {n p : ℕ} {spec : SubdivisionGraph.Spec n p} {D E : CFDiv spec.graph} (hcore : ∀ (v : Fin n), D (spec.coreVertex v) = E (spec.coreVertex v)) (hint : ∀ (edge : Fin p) (offset : Fin (spec.length edge - 1)), D (spec.interiorVertex edge offset) = E (spec.interiorVertex edge offset)) : D = E

Two divisors on a subdivision agree when they agree on core and interior vertices separately.

theorem Utilities.Certificate.SubdivisionRamp.pathVertex_interior {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (edge : Fin p) (k : ℕ) (hk0 : 0 < k) (hk : k < spec.length edge) : spec.pathVertex edge ⟨k, ⋯⟩ = spec.interiorVertex edge ⟨k - 1, ⋯⟩

A strictly interior path position is its corresponding interior vertex.

theorem Utilities.Certificate.SubdivisionRamp.interiorVertex_eq_iff {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (e e' : Fin p) (off : Fin (spec.length e - 1)) (off' : Fin (spec.length e' - 1)) : spec.interiorVertex e off = spec.interiorVertex e' off' ↔ e = e' ∧ ↑off = ↑off'

Distinct interior vertices are distinguished by slot and offset.

theorem Utilities.Certificate.SubdivisionRamp.coreVertex_ne_interiorVertex {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (v : Fin n) (e : Fin p) (off : Fin (spec.length e - 1)) : spec.coreVertex v ≠ spec.interiorVertex e off

A core vertex cannot be an interior vertex.

def Utilities.Certificate.SubdivisionRamp.rampValue {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (pot : Fin n → ℤ) (sgn : Fin p → ℤ) (lo : Fin p → ℕ) (t : ℕ) : Fin p → ℕ → ℤ

Path values of a ramp script.

Equations

• Utilities.Certificate.SubdivisionRamp.rampValue spec pot sgn lo t edge k = pot (spec.core.tail edge) + sgn edge * ↑(min (k - lo edge) t)

def Utilities.Certificate.SubdivisionRamp.rampScript {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (pot : Fin n → ℤ) (sgn : Fin p → ℤ) (lo : Fin p → ℕ) (t : ℕ) : firingScript spec.graph

The ramp firing script.

Equations

• Utilities.Certificate.SubdivisionRamp.rampScript spec pot sgn lo t = spec.slotValueScript pot (Utilities.Certificate.SubdivisionRamp.rampValue spec pot sgn lo t)

def Utilities.Certificate.SubdivisionRamp.rampSlope {p : ℕ} (sgn : Fin p → ℤ) (lo : Fin p → ℕ) (t : ℕ) : Fin p → ℕ → ℤ

Unit-step slopes of a ramp script.

Equations

• Utilities.Certificate.SubdivisionRamp.rampSlope sgn lo t edge k = if lo edge ≤ k ∧ k < lo edge + t then sgn edge else 0

structure Utilities.Certificate.SubdivisionRamp.RampData {n p : ℕ} (spec : SubdivisionGraph.Spec n p) (pot : Fin n → ℤ) (sgn : Fin p → ℤ) (lo : Fin p → ℕ) (t : ℕ) : Prop

Consistency of ramp data with the endpoint potentials and edge lengths.

• potential (edge : Fin p) : pot (spec.core.head edge) = pot (spec.core.tail edge) + sgn edge * ↑t
• window (edge : Fin p) : lo edge + t ≤ spec.length edge ∨ sgn edge = 0

theorem Utilities.Certificate.SubdivisionRamp.rampCompatible {n p : ℕ} {spec : SubdivisionGraph.Spec n p} {pot : Fin n → ℤ} {sgn : Fin p → ℤ} {lo : Fin p → ℕ} {t : ℕ} (h : RampData spec pot sgn lo t) : spec.SlotValueCompatible pot (rampValue spec pot sgn lo t)

theorem Utilities.Certificate.SubdivisionRamp.isStepSlope_ramp {n p : ℕ} {spec : SubdivisionGraph.Spec n p} {pot : Fin n → ℤ} {sgn : Fin p → ℤ} {lo : Fin p → ℕ} {t : ℕ} (h : RampData spec pot sgn lo t) : spec.IsStepSlope (rampScript spec pot sgn lo t) (rampSlope sgn lo t)

theorem Utilities.Certificate.SubdivisionRamp.prin_ramp_coreVertex {n p : ℕ} {spec : SubdivisionGraph.Spec n p} {pot : Fin n → ℤ} {sgn : Fin p → ℤ} {lo : Fin p → ℕ} {t : ℕ} (h : RampData spec pot sgn lo t) (v : Fin n) : (prin spec.graph) (rampScript spec pot sgn lo t) (spec.coreVertex v) = ∑ edge : Fin p, ((if spec.core.tail edge = v then rampSlope sgn lo t edge 0 else 0) + if spec.core.head edge = v then -rampSlope sgn lo t edge (spec.length edge - 1) else 0)

theorem Utilities.Certificate.SubdivisionRamp.prin_ramp_interiorVertex {n p : ℕ} {spec : SubdivisionGraph.Spec n p} {pot : Fin n → ℤ} {sgn : Fin p → ℤ} {lo : Fin p → ℕ} {t : ℕ} (h : RampData spec pot sgn lo t) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : (prin spec.graph) (rampScript spec pot sgn lo t) (spec.interiorVertex edge offset) = rampSlope sgn lo t edge (↑offset + 1) - rampSlope sgn lo t edge ↑offset

theorem Utilities.Certificate.SubdivisionRamp.rampSlope_zero {p : ℕ} (sgn : Fin p → ℤ) (lo : Fin p → ℕ) (t : ℕ) (edge : Fin p) : rampSlope sgn lo t edge 0 = if lo edge = 0 ∧ 0 < t then sgn edge else 0

theorem Utilities.Certificate.SubdivisionRamp.rampSlope_last {n p : ℕ} {spec : SubdivisionGraph.Spec n p} {pot : Fin n → ℤ} {sgn : Fin p → ℤ} {lo : Fin p → ℕ} {t : ℕ} (h : RampData spec pot sgn lo t) (edge : Fin p) : rampSlope sgn lo t edge (spec.length edge - 1) = if lo edge + t = spec.length edge ∧ 0 < t then sgn edge else 0

theorem Utilities.Certificate.SubdivisionRamp.rampSlope_zero_t {p : ℕ} (sgn : Fin p → ℤ) (lo : Fin p → ℕ) (edge : Fin p) (k : ℕ) : rampSlope sgn lo 0 edge k = 0

theorem Utilities.Certificate.SubdivisionRamp.rampSlope_diff {p : ℕ} (sgn : Fin p → ℤ) (lo : Fin p → ℕ) (t : ℕ) (edge : Fin p) (k : ℕ) (hk : 0 < k) : rampSlope sgn lo t edge k - rampSlope sgn lo t edge (k - 1) = (if k = lo edge ∧ 0 < t then sgn edge else 0) - if k = lo edge + t ∧ 0 < t then sgn edge else 0

Divergence of a ramp along one slot.