Multi-break firing scripts on the closed length orthant

This is the closed-face counterpart of the concrete part of MultiBreakScript.lean. A row leaf first evaluates its named break positions, then supplies the resulting concrete lists here. A zero-length slot has no steps; BreakData.balance consequently forces its endpoint potential to agree.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.effective_of_cases {n p : ℕ} (d : DegSpec n p) {D : CFDiv d.graph} (hcore : ∀ (c : d.Class), 0 ≤ D (Sum.inl c)) (hint : ∀ (edge : Fin p) (offset : Fin (d.length edge - 1)), 0 ≤ D (d.interiorVertex edge offset)) : effective D

Effectivity on a contracted subdivision reduces to its quotient-core and interior summands. This is the closed-face counterpart of the positive multi-break helper, and is the assembly point a row leaf uses after W4/W5.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.reaches_of_script {n p : ℕ} (d : DegSpec n p) (D : CFDiv d.graph) (script : firingScript d.graph) (q : d.graph.V) (hEffective : effective (D + (prin d.graph) script)) (hChip : 1 ≤ (D + (prin d.graph) script) q) : StrongSeparator.Reaches d.graph D q

An effective representative carrying a chip at a target vertex witnesses reachability there. It works verbatim on closed faces, including when core vertices have merged.

def Utilities.Certificate.DegenerateSpec.DegSpec.breakValue {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (breaks : Fin p → List (ℕ × ℤ)) : Fin p → ℕ → ℤ

Path values of a closed-face multi-break script.

Equations

• d.breakValue potential breaks edge k = potential (d.core.tail edge) + ∑ j ∈ Finset.range k, Utilities.Certificate.SubdivisionGraph.Spec.breakSlope (breaks edge) j

def Utilities.Certificate.DegenerateSpec.DegSpec.breakScript {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (breaks : Fin p → List (ℕ × ℤ)) : firingScript d.graph

The concrete multi-break firing script on a contracted subdivision.

Equations

• d.breakScript potential breaks = d.slotValueScript potential (d.breakValue potential breaks)

structure Utilities.Certificate.DegenerateSpec.DegSpec.BreakData {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (breaks : Fin p → List (ℕ × ℤ)) : Prop

Closing condition for a multi-break script, including zero slots.

• balance (edge : Fin p) : potential (d.core.head edge) = potential (d.core.tail edge) + ∑ j ∈ Finset.range (d.length edge), SubdivisionGraph.Spec.breakSlope (breaks edge) j

@[simp]

theorem Utilities.Certificate.DegenerateSpec.DegSpec.breakValue_zero {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {breaks : Fin p → List (ℕ × ℤ)} (edge : Fin p) : d.breakValue potential breaks edge 0 = potential (d.core.tail edge)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.slotValueCompatible_breakValue {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {breaks : Fin p → List (ℕ × ℤ)} (hInv : d.RepInvariant potential) (hData : d.BreakData potential breaks) : d.SlotValueCompatible potential (d.breakValue potential breaks)

theorem Utilities.Certificate.DegenerateSpec.DegSpec.isStepSlope_breakScript {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {breaks : Fin p → List (ℕ × ℤ)} (hInv : d.RepInvariant potential) (hData : d.BreakData potential breaks) : d.IsStepSlope (d.breakScript potential breaks) fun (edge : Fin p) (k : ℕ) => SubdivisionGraph.Spec.breakSlope (breaks edge) k

The unit-step slopes are the decoded break slopes. Vanishing slots impose no condition because their step type is empty.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_breakScript_coreVertex {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {breaks : Fin p → List (ℕ × ℤ)} (hInv : d.RepInvariant potential) (hData : d.BreakData potential breaks) (vertex : Fin n) : (prin d.graph) (d.breakScript potential breaks) (d.coreVertex vertex) = ∑ edge : Fin p, ((if d.rep (d.core.tail edge) = d.rep vertex then SubdivisionGraph.Spec.breakSlope (breaks edge) 0 else 0) + if d.rep (d.core.head edge) = d.rep vertex then -SubdivisionGraph.Spec.breakSlope (breaks edge) (d.length edge - 1) else 0)

At a contracted core class, the Laplacian is the endpoint sum over every original slot, including vanishing slots (which cancel in the generic formula).

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_breakScript_interiorVertex {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {breaks : Fin p → List (ℕ × ℤ)} (hInv : d.RepInvariant potential) (hData : d.BreakData potential breaks) (edge : Fin p) (offset : Fin (d.length edge - 1)) : (prin d.graph) (d.breakScript potential breaks) (d.interiorVertex edge offset) = SubdivisionGraph.Spec.breakSlope (breaks edge) (↑offset + 1) - SubdivisionGraph.Spec.breakSlope (breaks edge) ↑offset

At a surviving interior vertex, the Laplacian is the jump of the break slope.

theorem Utilities.Certificate.DegenerateSpec.DegSpec.prin_breakScript_interiorVertex_eq_zero {n p : ℕ} {d : DegSpec n p} {potential : Fin n → ℤ} {breaks : Fin p → List (ℕ × ℤ)} (hInv : d.RepInvariant potential) (hData : d.BreakData potential breaks) (edge : Fin p) (offset : Fin (d.length edge - 1)) (hNoBreak : ∀ entry ∈ breaks edge, entry.1 ≠ ↑offset + 1) : (prin d.graph) (d.breakScript potential breaks) (d.interiorVertex edge offset) = 0

The principal divisor vanishes away from named break positions.