Finite block-end decoding

The rich RPF leaf records a finite (weakly ordered) list of block endpoints. This file supplies the one semantic operation the interpolation layer needs: for every surviving unit step, choose the first endpoint strictly to its right. Repeated endpoints are intentional -- they represent zero-length blocks -- and are skipped by the selector.

The small FiniteBlockEnds interface keeps list bookkeeping out of the closed-face soundness proof. The lowerer/checker bridge proves its three displayed facts from a concrete RPF block list.

structure MarkedGraphs.Certificate.FiniteBlockEnds (L : ℕ) : Type

A finite, weakly ordered endpoint list ending at L.

cover is deliberately bounded by ends.length: although endAt has the convenient default L out of bounds, no phantom block may be selected.

• ends : List ℕ

  The nonempty, weakly ordered list of block endpoints ending at L, covering every unit step below L.

• nonempty : 0 < self.ends.length
• last : self.ends.getD (self.ends.length - 1) L = L
• ordered (i : ℕ) : self.ends.getD i L ≤ self.ends.getD (i + 1) L
• cover (k : ℕ) : k < L → ∃ i < self.ends.length, k < self.ends.getD i L

def MarkedGraphs.Certificate.FiniteBlockEnds.ofOrderedLast {L : ℕ} (ends : List ℕ) (hNonempty : 0 < ends.length) (hLast : ends.getD (ends.length - 1) L = L) (hOrdered : ∀ (i : ℕ), ends.getD i L ≤ ends.getD (i + 1) L) : FiniteBlockEnds L

A nonempty weakly ordered list whose final endpoint is L automatically covers every unit step below L: the final block is always a possible owner. This is the form produced directly by the W1 checks of a rich row leaf.

Equations

• MarkedGraphs.Certificate.FiniteBlockEnds.ofOrderedLast ends hNonempty hLast hOrdered = { ends := ends, nonempty := hNonempty, last := hLast, ordered := hOrdered, cover := ⋯ }

def MarkedGraphs.Certificate.FiniteBlockEnds.endAt {L : ℕ} (b : FiniteBlockEnds L) (i : ℕ) : ℕ

The endpoint at a block index, defaulting to the total length.

Equations

• b.endAt i = b.ends.getD i L

def MarkedGraphs.Certificate.FiniteBlockEnds.startAt {L : ℕ} (b : FiniteBlockEnds L) (i : ℕ) : ℕ

The left endpoint of a block.

Equations

• b.startAt i = if i = 0 then 0 else b.endAt (i - 1)

def MarkedGraphs.Certificate.FiniteBlockEnds.blockAt {L : ℕ} (b : FiniteBlockEnds L) (k : ℕ) : ℕ

The first (finite) block ending strictly after k; its arbitrary value outside [0,L) is never used by the interpolation interface.

Equations

• b.blockAt k = if hk : k < L then Nat.find ⋯ else 0

@[simp]

theorem MarkedGraphs.Certificate.FiniteBlockEnds.endAt_def {L : ℕ} (b : FiniteBlockEnds L) (i : ℕ) : b.endAt i = b.ends.getD i L

theorem MarkedGraphs.Certificate.FiniteBlockEnds.endAt_mono {L : ℕ} (b : FiniteBlockEnds L) {i j : ℕ} (hij : i ≤ j) : b.endAt i ≤ b.endAt j

theorem MarkedGraphs.Certificate.FiniteBlockEnds.endAt_le_length {L : ℕ} (b : FiniteBlockEnds L) (i : ℕ) (hi : i < b.ends.length) : b.endAt i ≤ L

Every actual listed endpoint lies at or before the total path length.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.lt_of_endAt_eq_zero_of_endAt_pos {L : ℕ} (b : FiniteBlockEnds L) {i s : ℕ} (hZero : b.endAt i = 0) (hPos : 0 < b.endAt s) : i < s

If the endpoint of block s is strictly beyond the tail, every endpoint at the tail occurs strictly before s. This remains valid when earlier blocks have length zero and hence have repeated endpoints.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.lt_of_endAt_lt_length_of_endAt_eq_length {L : ℕ} (b : FiniteBlockEnds L) {i s : ℕ} (hLength : b.endAt i = L) (hLt : b.endAt s < L) : s < i

Dually, if the endpoint of block s is strictly before the head, every endpoint at the total length occurs strictly after s. Repeated endpoints at the head are therefore an allowed suffix, never an interior run.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.blockAt_spec {L : ℕ} (b : FiniteBlockEnds L) (k : ℕ) (hk : k < L) : k < b.endAt (b.blockAt k)

theorem MarkedGraphs.Certificate.FiniteBlockEnds.blockAt_lt_length {L : ℕ} (b : FiniteBlockEnds L) (k : ℕ) (hk : k < L) : b.blockAt k < b.ends.length

theorem MarkedGraphs.Certificate.FiniteBlockEnds.lt_blockAt_of_endAt_le {L : ℕ} (b : FiniteBlockEnds L) (k i : ℕ) (hk : k < L) (hEnd : b.endAt i ≤ k) : i < b.blockAt k

Once the endpoint of a block lies at or before a surviving step, the first-endpoint selector must have moved strictly past that block. This is the basic boundary fact used to turn a selector change into a run of coincident finite endpoints.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.endAt_le_of_lt_blockAt {L : ℕ} (b : FiniteBlockEnds L) (k i : ℕ) (hk : k < L) (hIndex : i < b.blockAt k) : b.endAt i ≤ k

Conversely, every block strictly before the selected one has already ended. Together with lt_blockAt_of_endAt_le, this characterizes the selector by the endpoint inequalities, including repeated (zero-length) endpoints.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.endAt_eq_succ_of_selector_lt {L : ℕ} (b : FiniteBlockEnds L) (k i j t : ℕ) (hk : k + 1 < L) (hi : i = b.blockAt k) (hj : j = b.blockAt (k + 1)) (hChange : i < j) (hRun : i ≤ t) (ht : t < j) : b.endAt t = k + 1

When the selector changes between adjacent surviving steps, every listed endpoint from the old selected block through the block immediately before the new selection is exactly their common boundary. This is the finite ``collapsed run'' decoded by W4.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.blockAt_mono {L : ℕ} (b : FiniteBlockEnds L) {k l : ℕ} (hk : k < L) (hl : l < L) (hkl : k ≤ l) : b.blockAt k ≤ b.blockAt l

The first-endpoint selector is monotone along a slot. Thus two adjacent surviving steps either belong to the same canonical interpolator or form the forward collapsed-boundary situation handled by W4.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.covers {L : ℕ} (b : FiniteBlockEnds L) (k : ℕ) (hk : k < L) : b.startAt (b.blockAt k) ≤ k ∧ k < b.endAt (b.blockAt k)

The selected block contains the step.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.ownsInterval {L : ℕ} (b : FiniteBlockEnds L) (block k : ℕ) (hStart : b.startAt block ≤ k) (hEnd : k < b.endAt block) : b.blockAt k = block

Any nonempty block interval has a unique owner: the first endpoint to its right is exactly that block. This is the PiecewiseData.ownsInterval law.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.sum_range_eq_sum_blocks {L : ℕ} (b : FiniteBlockEnds L) (f : ℕ → ℤ) : ∑ k ∈ Finset.range L, f k = ∑ i ∈ Finset.range b.ends.length, ∑ j ∈ Finset.range (b.endAt i - b.startAt i), f (b.startAt i + j)

The nonempty block intervals partition the surviving unit steps. This is stated for integer-valued functions because it is used to concatenate the canonical interpolation slopes.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.sum_selected_steps_eq_sum_rises {L : ℕ} (b : FiniteBlockEnds L) (rises : ℕ → ℤ) : ∑ k ∈ Finset.range L, Utilities.Certificate.SubdivisionArithmetic.step (b.endAt (b.blockAt k) - b.startAt (b.blockAt k)) (rises (b.blockAt k)) (k - b.startAt (b.blockAt k)) = ∑ i ∈ Finset.range b.ends.length, if b.startAt i < b.endAt i then rises i else 0

Concatenating the canonical interpolation on the selected blocks realizes the sum of the rises of exactly the nonempty blocks. Repeated endpoints represent zero-length blocks and therefore contribute zero independently of their (irrelevant) stored rise.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.sum_rises_eq_sum_nonempty {L : ℕ} (b : FiniteBlockEnds L) (rises : ℕ → ℤ) (hEmpty : ∀ (i : ℕ), b.endAt i ≤ b.startAt i → rises i = 0) : ∑ i ∈ Finset.range b.ends.length, rises i = ∑ i ∈ Finset.range b.ends.length, if b.startAt i < b.endAt i then rises i else 0

W2 makes the rise of an empty block zero. Under exactly that condition, the nonempty-block sum used by canonical interpolation is the full declared rise sum.

theorem MarkedGraphs.Certificate.FiniteBlockEnds.sum_selected_steps_eq_total_rises {L : ℕ} (b : FiniteBlockEnds L) (rises : ℕ → ℤ) (hEmpty : ∀ (i : ℕ), b.endAt i ≤ b.startAt i → rises i = 0) : ∑ k ∈ Finset.range L, Utilities.Certificate.SubdivisionArithmetic.step (b.endAt (b.blockAt k) - b.startAt (b.blockAt k)) (rises (b.blockAt k)) (k - b.startAt (b.blockAt k)) = ∑ i ∈ Finset.range b.ends.length, rises i

The canonical selected slopes realize every declared rise once W2 has discharged the zero-length blocks.

def Utilities.Certificate.DegenerateSpec.DegSpec.decodePiecewiseData {n p : ℕ} (d : DegSpec n p) (potential : Fin n → ℤ) (blocks : (e : Fin p) → MarkedGraphs.Certificate.FiniteBlockEnds (d.length e)) (rises : Fin p → ℕ → ℤ) (balance : ∀ (e : Fin p), potential (d.core.head e) = potential (d.core.tail e) + ∑ k ∈ Finset.range (d.length e), blockSlope (fun (e : Fin p) (k : ℕ) => (blocks e).blockAt k) (fun (e : Fin p) (k : ℕ) => (blocks e).endAt k) rises e k) : d.PiecewiseData potential

Decode one finite endpoint list per slot into the selector portion of a PiecewiseData. Endpoint rises and the endpoint balance are supplied by the rich leaf separately.

Equations

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