Firing scripts with a marked point inside each slot

DegSpec.interpolatedScript puts one canonical ramp on each slot, so its interior Laplacian is nonnegative everywhere and a chip strictly inside a slot is never used. Atanasov--Ranganathan's sixth and seventh genus-five families place chips exactly there, and no core-supported degree-four divisor covers either row, so those rows need a script whose slot value may bend downward at one marked offset.

This file is that script. A slot e carries a mark mark e -- the offset of its chip -- and a mark value markValue e, the script's value there; the slot value is the canonical ramp from the tail class up to the mark, followed by the canonical ramp from the mark down to the head class. Taking mark e = 0 and markValue e = potential (rep (tail e)) recovers interpolatedScript on that slot, so a row may mark only the slots it needs.

The two Laplacian formulas come from DegenerateSlopeScript unchanged: they are stated for an arbitrary slot-value function. What this file adds is

• splitValueCompatible, so the value really assembles into a script;
• isStepSlope_splitScript, naming the slope as SubdivisionArithmetic.splitStep;
• prin_splitScript_interiorVertex_nonneg_of_ne, the interior residual away from the mark; and
• prin_splitScript_interiorVertex_ge_neg_one, the residual at the mark, which is where the chip is spent.

The arithmetic lives in SplitRampArithmetic.lean.

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

The rise of the ramp from the tail class up to the mark.

Equations

• d.markRiseIn potential markValue e = markValue e - potential (d.rep (d.core.tail e))

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

The rise of the ramp from the mark down to the head class.

Equations

• d.markRiseOut potential markValue e = potential (d.rep (d.core.head e)) - markValue e

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

Admissibility of the marks: each sits inside its slot, and a mark at an end of its slot carries that end's value.

Equations

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

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

The slot value: two canonical ramps meeting at the mark.

Equations

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

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

The firing script assembled from the marked slot values.

Equations

• d.splitScript potential mark markValue = d.slotValueScript potential (d.splitValue potential mark markValue)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.splitValueCompatible {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {mark : Fin p → ℕ} {markValue : Fin p → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) : d.SlotValueCompatible potential (d.splitValue potential mark markValue)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.isStepSlope_splitScript {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {mark : Fin p → ℕ} {markValue : Fin p → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) : d.IsStepSlope (d.splitScript potential mark markValue) fun (e : Fin p) (k : ℕ) => SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) k

The slope of the marked script is the split ramp's slope.

The core-class formula

prin_coreVertex_eq_endpointSum applies verbatim; the two endpoint slopes are identified with the surviving half's own endpoint slopes by SubdivisionArithmetic.splitStep_first and splitStep_last.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_splitScript_coreVertex_eq_endpointSum {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {mark : Fin p → ℕ} {markValue : Fin p → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) (r : Fin n) : (prin d.graph) (d.splitScript potential mark markValue) (d.coreVertex r) = ∑ e : Fin p, ((if d.rep (d.core.tail e) = d.rep r then SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) 0 else 0) + if d.rep (d.core.head e) = d.rep r then -SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) (d.length e - 1) else 0)

The interior formula

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_splitScript_interiorVertex_eq_slopeDifference {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {mark : Fin p → ℕ} {markValue : Fin p → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) (e : Fin p) (o : Fin (d.length e - 1)) : (prin d.graph) (d.splitScript potential mark markValue) (d.interiorVertex e o) = SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) (↑o + 1) - SubdivisionArithmetic.splitStep (d.length e) (mark e) (d.markRiseIn potential markValue e) (d.markRiseOut potential markValue e) ↑o

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_splitScript_interiorVertex_nonneg_of_ne {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {mark : Fin p → ℕ} {markValue : Fin p → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) (e : Fin p) (o : Fin (d.length e - 1)) (hne : ↑o + 1 ≠ mark e) : 0 ≤ (prin d.graph) (d.splitScript potential mark markValue) (d.interiorVertex e o)

Away from the mark the marked script is still convex, so its interior residual is nonnegative exactly as for interpolatedScript.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_splitScript_interiorVertex_ge_neg_one {n p : ℕ} (d : DegSpec n p) {potential : Fin n → ℤ} {mark : Fin p → ℕ} {markValue : Fin p → ℤ} (hMarks : d.MarksAdmissible potential mark markValue) (e : Fin p) (o : Fin (d.length e - 1)) (hmark : ↑o + 1 = mark e) (hlt : mark e < d.length e) (hIn : d.markRiseIn potential markValue e ≤ ↑(mark e)) (hOut : -↑(d.length e - mark e) ≤ d.markRiseOut potential markValue e) (hflat : d.markRiseIn potential markValue e = 0 ∨ d.markRiseOut potential markValue e = 0) : -1 ≤ (prin d.graph) (d.splitScript potential mark markValue) (d.interiorVertex e o)

At the mark. The residual drops by at most one, so a divisor carrying one chip at the marked vertex stays effective there. The two rise bounds and the flatness disjunction are what a configuration supplies.