Signed window profiles on subdivision slots

Many compact Dhar calculations are specified by assigning an integral value to each core vertex and, on every oriented subdivision slot, allowing one interval of constant integral slope. Outside that interval the script is constant. Endpoint compatibility is the only gluing condition.

This file turns that description into an actual firing script and computes its principal divisor solely from the signed window endpoints. The slope is allowed to be any integer; the -1, 0, and 1 profiles used in genus four are special cases.

One numerical window

def Utilities.Certificate.WindowProfile.windowValue (start stop : ℕ) (slope : ℤ) (i : ℕ) : ℤ

Value gained by offset i across a signed window [start, stop]. The value is zero before start, changes with constant slope inside the window, and is constant after stop.

Equations

• Utilities.Certificate.WindowProfile.windowValue start stop slope i = if i ≤ start then 0 else if i ≤ stop then slope * ↑(i - start) else slope * ↑(stop - start)

def Utilities.Certificate.WindowProfile.windowSlope (start stop : ℕ) (slope : ℤ) (i : ℕ) : ℤ

Slope across the unit step beginning at offset i.

Equations

• Utilities.Certificate.WindowProfile.windowSlope start stop slope i = if start ≤ i ∧ i < stop then slope else 0

@[simp]

theorem Utilities.Certificate.WindowProfile.windowValue_zero (start stop : ℕ) (slope : ℤ) : windowValue start stop slope 0 = 0

theorem Utilities.Certificate.WindowProfile.windowValue_of_stop_le {start stop i : ℕ} {slope : ℤ} (hStop : stop ≤ i) (hOrder : start ≤ stop) : windowValue start stop slope i = slope * ↑(stop - start)

theorem Utilities.Certificate.WindowProfile.windowValue_succ_sub_windowValue {start stop i : ℕ} {slope : ℤ} (hOrder : start ≤ stop) : windowValue start stop slope (i + 1) - windowValue start stop slope i = windowSlope start stop slope i

Consecutive window values have the advertised slope.

theorem Utilities.Certificate.WindowProfile.windowSlope_divergence {length start stop j : ℕ} {slope : ℤ} (hOrder : start ≤ stop) (hStop : stop ≤ length) (hj : j ≤ length) : ((if j < length then windowSlope start stop slope j else 0) - if 0 < j then windowSlope start stop slope (j - 1) else 0) = (if j = start then slope else 0) - if j = stop then slope else 0

The divergence of a window slope is concentrated at its two endpoints. Coincident endpoints cancel automatically.

Compatible profiles and their firing scripts

structure Utilities.Certificate.WindowProfile.Data {n p : ℕ} (spec : SubdivisionGraph.Spec n p) : Type

One signed slope window on every slot, together with compatible values at the core vertices. A zero slope or a degenerate window represents a constant slot.

• coreValue : Fin n → ℤ

  The integer potential value at each core vertex of the window profile.

• start : Fin p → ℕ

  The initial path coordinate of the constant-slope window on each slot.

• stop : Fin p → ℕ

  The final path coordinate of each window, between its start and the slot length.

• slope : Fin p → ℤ

  The integer slope inside each slot's window, compatible with the difference of the endpoint potentials.

• start_le_stop (edge : Fin p) : self.start edge ≤ self.stop edge
• stop_le_length (edge : Fin p) : self.stop edge ≤ spec.length edge
• endpoint_compatible (edge : Fin p) : self.coreValue (spec.core.head edge) = self.coreValue (spec.core.tail edge) + self.slope edge * ↑(self.stop edge - self.start edge)

def Utilities.Certificate.WindowProfile.Data.pathValue {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (offset : ℕ) : ℤ

Numerical value of the profile along one oriented slot.

Equations

• data.pathValue edge offset = data.coreValue (spec.core.tail edge) + Utilities.Certificate.WindowProfile.windowValue (data.start edge) (data.stop edge) (data.slope edge) offset

def Utilities.Certificate.WindowProfile.Data.script {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) : firingScript spec.graph

Extend a compatible profile over every subdivision vertex.

Equations

• data.script (Sum.inl vertex) = data.coreValue vertex
• data.script (Sum.inr interior) = data.pathValue interior.fst (↑interior.snd + 1)

@[simp]

theorem Utilities.Certificate.WindowProfile.Data.script_core {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (vertex : Fin n) : data.script (spec.coreVertex vertex) = data.coreValue vertex

@[simp]

theorem Utilities.Certificate.WindowProfile.Data.script_interior {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (offset : Fin (spec.length edge - 1)) : data.script (spec.interiorVertex edge offset) = data.pathValue edge (↑offset + 1)

theorem Utilities.Certificate.WindowProfile.Data.pathValue_zero {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) : data.pathValue edge 0 = data.coreValue (spec.core.tail edge)

theorem Utilities.Certificate.WindowProfile.Data.pathValue_length {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) : data.pathValue edge (spec.length edge) = data.coreValue (spec.core.head edge)

theorem Utilities.Certificate.WindowProfile.Data.script_pathVertex {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (position : spec.PathPosition edge) : data.script (spec.pathVertex edge position) = data.pathValue edge ↑position

The profile script agrees with its numerical path value at every named position, including both core endpoints.

theorem Utilities.Certificate.WindowProfile.Data.script_stepLeft {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (offset : Fin (spec.length edge)) : data.script (spec.stepLeft edge offset) = data.pathValue edge ↑offset

theorem Utilities.Certificate.WindowProfile.Data.script_stepRight {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (offset : Fin (spec.length edge)) : data.script (spec.stepRight edge offset) = data.pathValue edge (↑offset + 1)

theorem Utilities.Certificate.WindowProfile.Data.script_stepDifference {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (offset : Fin (spec.length edge)) : data.script (spec.stepRight edge offset) - data.script (spec.stepLeft edge offset) = windowSlope (data.start edge) (data.stop edge) (data.slope edge) ↑offset

Every emitted unit step has the profile's advertised slope.

Exact principal divisor

def Utilities.Certificate.WindowProfile.Data.startPosition {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) : spec.PathPosition edge

The initial endpoint of a slot's signed slope window.

Equations

• data.startPosition edge = ⟨data.start edge, ⋯⟩

def Utilities.Certificate.WindowProfile.Data.stopPosition {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) : spec.PathPosition edge

The terminal endpoint of a slot's signed slope window.

Equations

• data.stopPosition edge = ⟨data.stop edge, ⋯⟩

@[simp]

theorem Utilities.Certificate.WindowProfile.Data.startPosition_val {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) : ↑(data.startPosition edge) = data.start edge

@[simp]

theorem Utilities.Certificate.WindowProfile.Data.stopPosition_val {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) : ↑(data.stopPosition edge) = data.stop edge

def Utilities.Certificate.WindowProfile.Data.edgeDivergence {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (vertex : spec.Vertex) : ℤ

Contribution of one oriented subdivision slot to a principal-divisor coefficient, expressed only in terms of the slot's signed step slopes.

Equations

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

theorem Utilities.Certificate.WindowProfile.Data.prin_script_eq_sum_edgeDivergence {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (vertex : spec.Vertex) : (prin spec.graph) data.script vertex = ∑ edge : Fin p, data.edgeDivergence edge vertex

The global principal divisor is the sum of the independent divergences of the signed slope windows on its subdivision slots.

theorem Utilities.Certificate.WindowProfile.Data.edgeDivergence_pathVertex {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (probe : spec.PathPosition edge) : data.edgeDivergence edge (spec.pathVertex edge probe) = (if ↑probe = data.start edge then data.slope edge else 0) - if ↑probe = data.stop edge then data.slope edge else 0

At a named position of one slot, its edge divergence is the numerical divergence of the two adjacent window slopes.

theorem Utilities.Certificate.WindowProfile.Data.edgeDivergence_eq_endpointDivisor {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) (edge : Fin p) (vertex : spec.Vertex) : data.edgeDivergence edge vertex = (data.slope edge • (oneChip (spec.pathVertex edge (data.startPosition edge)) - oneChip (spec.pathVertex edge (data.stopPosition edge)))) vertex

One slot contributes exactly a positive chip at the start of its signed window and a negative chip at the stop, both weighted by its integral slope. The statement also covers degenerate and zero-slope windows.

theorem Utilities.Certificate.WindowProfile.Data.prin_script_eq_endpointDivisors {n p : ℕ} {spec : SubdivisionGraph.Spec n p} (data : Data spec) : (prin spec.graph) data.script = ∑ edge : Fin p, data.slope edge • (oneChip (spec.pathVertex edge (data.startPosition edge)) - oneChip (spec.pathVertex edge (data.stopPosition edge)))

Exact signed-endpoint formula for the principal divisor of a compatible window profile. This is the compact replay theorem: a checker only needs to validate the profile bounds and endpoint compatibility, not a full potential at every subdivision vertex.