Maximum closure and clamping of firing scripts

Winning scripts for a fixed divisor are closed under pointwise maximum. Consequently an effective divisor stays effective after truncating a winning script from below. A script winning for an effective divisor with one chip demanded at q can also be made nonnegative and zero at q.

These statements require neither connectedness nor a choice of vertex type. They use only the basic chip-firing API. The general truncation statement also appears in Utilities.Gonality.LegalFiring; here it is a short consequence of maximum closure, without importing the gonality development.

theorem Utilities.prin_le_of_script_le_of_eq {G : CFGraph} {σ τ : firingScript G} (hle : ∀ (w : G.V), σ w ≤ τ w) {v : G.V} (heq : σ v = τ v) : (prin G) σ v ≤ (prin G) τ v

Raising a script away from a vertex, while fixing its value at that vertex, can only increase the principal divisor there.

theorem Utilities.effective_add_prin_max {G : CFGraph} {D : CFDiv G} {σ τ : firingScript G} (hσ : effective (D + (prin G) σ)) (hτ : effective (D + (prin G) τ)) : effective (D + (prin G) fun (v : G.V) => max (σ v) (τ v))

The pointwise maximum of two winning scripts wins for the same divisor. The starting divisor itself need not be effective.

def Utilities.clampScript {G : CFGraph} (σ : firingScript G) (c : ℤ) : firingScript G

Subtract a constant from a script and replace negative values by zero.

Equations

• Utilities.clampScript σ c v = max (σ v - c) 0

@[simp]

theorem Utilities.clampScript_apply {G : CFGraph} (σ : firingScript G) (c : ℤ) (v : G.V) : clampScript σ c v = max (σ v - c) 0

theorem Utilities.clampScript_nonneg {G : CFGraph} (σ : firingScript G) (c : ℤ) (v : G.V) : 0 ≤ clampScript σ c v

theorem Utilities.clampScript_eq_zero_of_le {G : CFGraph} (σ : firingScript G) {c : ℤ} {v : G.V} (h : σ v ≤ c) : clampScript σ c v = 0

theorem Utilities.clampScript_eq_sub_of_le {G : CFGraph} (σ : firingScript G) {c : ℤ} {v : G.V} (h : c ≤ σ v) : clampScript σ c v = σ v - c

theorem Utilities.clampScript_at_base {G : CFGraph} (σ : firingScript G) (q : G.V) : clampScript σ (σ q) q = 0

theorem Utilities.effective_add_prin_clamp {G : CFGraph} {D : CFDiv G} {σ : firingScript G} (hD : effective D) (hσ : effective (D + (prin G) σ)) (c : ℤ) : effective (D + (prin G) (clampScript σ c))

Truncating a winning script preserves effectivity of an effective starting divisor. No nonnegativity assumption on the script or cutoff is needed. This does not retain an extra demanded chip.

theorem Utilities.clampScript_eq_zero_of_eq_zero {G : CFGraph} (σ : firingScript G) {q : G.V} (hq : σ q = 0) {c : ℤ} (hc : 0 ≤ c) : clampScript σ c q = 0

At a pole where the script vanishes, a nonnegative cutoff keeps it zero.

theorem Utilities.effective_add_prin_clamp_at {G : CFGraph} {D : CFDiv G} {σ : firingScript G} (q : G.V) (hD : qEffective q D) (hσ : effective (D + (prin G) σ)) : effective (D + (prin G) (clampScript σ (σ q)))

If a divisor is effective away from q, normalize a winning script at q and clamp it at zero without losing effectivity, including at q.

theorem Utilities.effective_sub_one_chip_add_prin_clamp_at {G : CFGraph} {D : CFDiv G} {σ : firingScript G} (q : G.V) (hD : effective D) (hσ : effective (D - oneChip q + (prin G) σ)) : effective (D - oneChip q + (prin G) (clampScript σ (σ q)))

A winning script for an effective divisor with one chip demanded at q can be normalized and clamped at q.

theorem Utilities.exists_nonneg_firing_script_of_winnable {G : CFGraph} {D : CFDiv G} (q : G.V) (hD : qEffective q D) (hwin : winnable G D) : ∃ (σ : firingScript G), σ q = 0 ∧ (∀ (v : G.V), 0 ≤ σ v) ∧ effective (D + (prin G) σ)

Winnability for a divisor effective away from q has a nonnegative script witness vanishing at q.

theorem Utilities.exists_nonneg_firing_script_sub_one_chip {G : CFGraph} {D : CFDiv G} (q : G.V) (hD : effective D) (hwin : winnable G (D - oneChip q)) : ∃ (σ : firingScript G), σ q = 0 ∧ (∀ (v : G.V), 0 ≤ σ v) ∧ effective (D - oneChip q + (prin G) σ)

Reachability of q from an effective divisor has a nonnegative winning script that vanishes at the demanded vertex.

Degree bounds on the slopes of a winning firing script

On every edge, a script taking an effective divisor to an effective divisor changes height by at most its degree. To see this, clamp the script at the lower endpoint. The resulting effective divisor has the same degree, while its coefficient at that endpoint bounds the contribution of the chosen edge.

The same bound holds when the script first has to pay an effective demand. No connectedness hypothesis is needed.

theorem Utilities.script_sub_le_deg_of_effective_add_prin {G : CFGraph} {D : CFDiv G} {f : firingScript G} (hD : effective D) (hWin : effective (D + (prin G) f)) {u v : G.V} (hEdge : 0 < numEdges G u v) : f u - f v ≤ CFDiv.degree D

A winning script for an effective divisor changes height along any edge by at most the degree of that divisor. This is the one-sided form.

theorem Utilities.abs_script_sub_le_deg_of_effective_add_prin {G : CFGraph} {D : CFDiv G} {f : firingScript G} (hD : effective D) (hWin : effective (D + (prin G) f)) {u v : G.V} (hEdge : 0 < numEdges G u v) : |f u - f v| ≤ CFDiv.degree D

The absolute edge slope of a winning script is bounded by the degree of the effective starting divisor.

theorem Utilities.abs_script_sub_le_deg_of_le {G : CFGraph} {D R : CFDiv G} {f : firingScript G} (hD : effective D) (hRD : ∀ (w : G.V), R w ≤ D w) (hWin : effective (R + (prin G) f)) {u v : G.V} (hEdge : 0 < numEdges G u v) : |f u - f v| ≤ CFDiv.degree D

An effective pointwise majorant gives the same edge-slope bound for a script winning from a possibly signed starting divisor.

theorem Utilities.abs_script_sub_le_deg_of_effective_sub_add_prin {G : CFGraph} {D E : CFDiv G} {f : firingScript G} (hD : effective D) (hE : effective E) (hWin : effective (D - E + (prin G) f)) {u v : G.V} (hEdge : 0 < numEdges G u v) : |f u - f v| ≤ CFDiv.degree D

Subtracting an effective demand before applying the script does not increase the degree bound on any edge slope.