The multi-break interpolated script

AffinePositionMultiBreak names a passive multi-break slope script by a list of affine-positioned breaks and computes its Laplacian exactly: the endpoint sum at a core vertex, the jump of the break list at an interior vertex, and in particular the vanishing of that jump away from every named break. What it does not yet supply is the value at a named break, or the small amount of vertex-by-vertex bookkeeping (effective, Reaches) that every concrete instance of it would otherwise have to restate. Both are entirely row-independent, so both are proved here once, directly on top of AffinePositionMultiBreak (component 1).

• Sorted break lists. SegmentReflection.value/slope hard-code a three-piece step function (down, flat, up), and GenusFourCore100.rampSlope/capSlope hard-code two- and three-piece step functions via min/max. The multi-break format of component 1 allows an arbitrary number of pieces, named by an arbitrary (unsorted) list; BreakSorted isolates the case that every script actually produces — start positions strictly increasing along the list — and breakSlope_eq_of_breakSorted gives, once, for any number of pieces, the same kind of closed form those files hard-code by hand: the value of a sorted break list at one of its own start positions is exactly that entry's slope. The supporting lemma breakSlope_append_cons_eq is more general still: it needs no global sortedness, only that nothing after the chosen entry in list order also starts at or before the query point.

• March data. AffinePosition.SlopeScript.MarchData bundles the closing balance condition of AffinePosition.SlopeScript.Balanced with sortedness on every slot — the affine-positioned analogue of GenusFourCore100.RampData, generalized from one window per slot to an arbitrary sorted sequence of them. sortedBreaks_of_coordinate_lt gives a convenient sufficient condition for sortedness (breaks listed in increasing coordinate order by script index), and prin_firingScript_atBreak computes the Laplacian of a march at one of its own named breaks in closed form, generalizing GenusFourCore100.rampSlope_diff/capSlope_diff to an arbitrary sorted sequence of breaks.

• Effectiveness and reachability bookkeeping. effective_of_cases and reaches_of_script, restated verbatim in every direct genus-four row (GenusFourCore100.lean etc.) for its own fixed n, p, are proved once here for an arbitrary SubdivisionGraph.Spec n p, so no row needs to restate them again.

Nothing here is row specific, and nothing here is decidable-by-decide: the only Boolean checks anywhere in the stack are the fail-closed bound checks already introduced by AffinePosition.

Generic effectiveness and reachability bookkeeping

theorem Utilities.Certificate.SubdivisionGraph.Spec.effective_of_cases {n p : ℕ} (spec : Spec n p) {D : CFDiv spec.graph} (hcore : ∀ (u : Fin n), 0 ≤ D (spec.coreVertex u)) (hint : ∀ (edge : Fin p) (offset : Fin (spec.length edge - 1)), 0 ≤ D (spec.interiorVertex edge offset)) : effective D

Effectivity is checked vertex by vertex: core vertices and interior vertices separately. Row-independent generalization of the effective_of_cases helper otherwise restated for each direct genus-four row (e.g. GenusFourCore100.effective_of_cases).

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

An explicit firing script realizing an effective representative with a chip at q proves that D reaches q. Row-independent generalization of the reaches_of_script helper otherwise restated for each direct genus-four row (e.g. GenusFourCore100.reaches_of_script).

Sorted break lists

Pure list combinatorics on List (ℕ × ℤ): none of it mentions a SubdivisionGraph.Spec, but it is housed in the same namespace as breakSlope/breakSlopeFrom (AffinePositionMultiBreak.lean) for discoverability.

def Utilities.Certificate.SubdivisionGraph.Spec.BreakSorted (breaks : List (ℕ × ℤ)) : Prop

A break list is sorted when its start positions strictly increase along the list, in list order. Every break list actually produced by a script whose entries are supplied in increasing-coordinate order has this shape (AffinePosition.SlopeScript.sortedBreaks_of_coordinate_lt).

Equations

• Utilities.Certificate.SubdivisionGraph.Spec.BreakSorted breaks = List.Pairwise (fun (a b : ℕ × ℤ) => a.1 < b.1) breaks

@[simp]

theorem Utilities.Certificate.SubdivisionGraph.Spec.breakSorted_nil : BreakSorted []

theorem Utilities.Certificate.SubdivisionGraph.Spec.breakSlopeFrom_eq_initial_of_forall_lt (breaks : List (ℕ × ℤ)) (k : ℕ) (hAfter : ∀ entry ∈ breaks, k < entry.1) (initial : ℤ) : breakSlopeFrom initial breaks k = initial

The scan never fires, and the initial value survives, once every remaining entry starts strictly after the query point.

theorem Utilities.Certificate.SubdivisionGraph.Spec.breakSlope_eq_zero_of_forall_lt (breaks : List (ℕ × ℤ)) (k : ℕ) (hAfter : ∀ entry ∈ breaks, k < entry.1) : breakSlope breaks k = 0

A break list evaluates to 0 strictly before its first entry: the k below every start behaves as if the list were empty.

theorem Utilities.Certificate.SubdivisionGraph.Spec.breakSlopeFrom_append (initial : ℤ) (pre rest : List (ℕ × ℤ)) (k : ℕ) : breakSlopeFrom initial (pre ++ rest) k = breakSlopeFrom (breakSlopeFrom initial pre k) rest k

The scan distributes over list append: it can be run on the first part and resumed on the rest with the resulting value as the new initial value.

theorem Utilities.Certificate.SubdivisionGraph.Spec.breakSlope_append_cons_eq (pre : List (ℕ × ℤ)) (entry : ℕ × ℤ) (post : List (ℕ × ℤ)) (k : ℕ) (hEntry : entry.1 ≤ k) (hPost : ∀ e ∈ post, k < e.1) : breakSlope (pre ++ entry :: post) k = entry.2

The value of the scan at a chosen entry's own start position: whatever precedes the entry is irrelevant (the entry itself applies once reached, since entry.1 ≤ k for k = entry.1), and nothing after it in the list can override it once everything after it starts strictly later than k. This is the closed form SegmentReflection.value/GenusFourCore100.rampSlope/ capSlope hard-code for two or three pieces, given here once for any number of pieces and needing no global sortedness hypothesis.

theorem Utilities.Certificate.SubdivisionGraph.Spec.breakSlope_eq_of_breakSorted_le {breaks : List (ℕ × ℤ)} (hSorted : BreakSorted breaks) {entry : ℕ × ℤ} (hMem : entry ∈ breaks) {k : ℕ} (hLe : entry.1 ≤ k) (hNoOther : ∀ other ∈ breaks, entry.1 < other.1 → k < other.1) : breakSlope breaks k = entry.2

The value of a sorted break list at any point k at or after a member entry, as long as no other member of the list starts strictly between entry and k, is exactly entry's slope: sortedness places every other member either at or before entry (irrelevant, entry overrides it) or strictly after k (irrelevant, it is never reached). This is the general "current regime" reading of a sorted break list; evaluating it at k = entry.1 recovers breakSlope_eq_of_breakSorted below.

theorem Utilities.Certificate.SubdivisionGraph.Spec.breakSlope_eq_of_breakSorted {breaks : List (ℕ × ℤ)} (hSorted : BreakSorted breaks) {entry : ℕ × ℤ} (hMem : entry ∈ breaks) : breakSlope breaks entry.1 = entry.2

The value of a sorted break list at one of its own start positions is exactly that entry's slope. Special case of breakSlope_eq_of_breakSorted_le at k = entry.1.

Affine-positioned marches

theorem MarkedGraphs.Certificate.AffinePosition.SlopeScript.mem_breaks_of_edge_eq {m n p b : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : SlopeScript m p b) (point : Fin m → ℤ) (edge : Fin p) (index : Fin b) (hEdge : (script.entry index).position.edge = edge) : (Code.coordinate certificate (script.entry index).position point, (script.entry index).slope) ∈ breaks certificate script point edge

If a script entry names edge, its decoded (coordinate, slope) pair is a member of the decoded break list for edge. Converse of exists_of_mem_breaks.

def MarkedGraphs.Certificate.AffinePosition.SlopeScript.SortedBreaks {m n p b : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : SlopeScript m p b) (point : Fin m → ℤ) : Prop

Every slot's decoded break list is sorted.

Equations

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

theorem MarkedGraphs.Certificate.AffinePosition.SlopeScript.sortedBreaks_of_coordinate_lt {m n p b : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : SlopeScript m p b) (point : Fin m → ℤ) (hOrder : ∀ (edge : Fin p) (i j : Fin b), i < j → (script.entry i).position.edge = edge → (script.entry j).position.edge = edge → Code.coordinate certificate (script.entry i).position point < Code.coordinate certificate (script.entry j).position point) : SortedBreaks certificate script point

Sufficient condition for SortedBreaks: on every slot, breaks named by an earlier script index have a strictly smaller decoded coordinate than breaks named by a later one. This is the condition a script author actually establishes (breaks are written down in the order the chip should pass through them), and it is enough to make every slot's decoded break list sorted, without ever materializing that list.

structure MarkedGraphs.Certificate.AffinePosition.SlopeScript.MarchData {m n p b : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : SlopeScript m p b) (potential : Fin n → ℤ) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) : Prop

Consistency data for a multi-break script that marches through its breaks in coordinate order on every slot: the closing balance condition of Balanced, together with sortedness of every slot's decoded break list. The affine-positioned analogue of GenusFourCore100.RampData, generalized from one window per slot to an arbitrary sorted sequence of them.

• balanced : Balanced certificate script potential point core_nonempty hValid hCone
• sorted : SortedBreaks certificate script point

theorem MarkedGraphs.Certificate.AffinePosition.SlopeScript.prin_firingScript_atBreak {m n p b : ℕ} (certificate : Utilities.Certificate.ExplicitPotential.CertificateData m n p) (script : SlopeScript m p b) (potential : Fin n → ℤ) (point : Fin m → ℤ) (core_nonempty : 0 < n) {degree : ℤ} (hValid : certificate.Valid degree) (hCone : Utilities.Certificate.ExplicitPotential.FormsHold certificate.cone point) (hMarch : MarchData certificate script potential point core_nonempty hValid hCone) (edge : Fin p) (offset : Fin ((certificate.subdivisionSpec point core_nonempty hValid hCone).length edge - 1)) (index : Fin b) (hEdge : (script.entry index).position.edge = edge) (hCoordinate : Code.coordinate certificate (script.entry index).position point = ↑offset + 1) : (prin (certificate.subdivisionSpec point core_nonempty hValid hCone).graph) (firingScript certificate script potential point core_nonempty hValid hCone) ((certificate.subdivisionSpec point core_nonempty hValid hCone).interiorVertex edge offset) = (script.entry index).slope - Utilities.Certificate.SubdivisionGraph.Spec.breakSlope (breaks certificate script point edge) ↑offset

The Laplacian of a march at one of its own named breaks: the entry's slope minus the running value just before it. Generalizes GenusFourCore100.rampSlope_diff/capSlope_diff to an arbitrary sorted sequence of affine-positioned breaks.