Short first returns in executable boundary restrictions

These equations inspect the literal list-funded scan used by restrictPrefix. Its first retained successor is read after one, two or three steps. The raw table may be malformed elsewhere; the stated length and retained-index hypotheses are sufficient for these local equations.

theorem Cslib.Complexity.CSP.OrderedBoundary.getD_restrictPrefix_one (c : Graph.RotationCertificate) (darts i : ℕ) (hi : i < darts) (hc : 0 < c.successor.length) (hs : c.successor.getD i 0 < darts) : (restrictPrefix darts c).successor.getD i 0 = c.successor.getD i 0

A retained immediate successor is the first return, provided the table funds one step.

theorem Cslib.Complexity.CSP.OrderedBoundary.restrictPrefix_eq_self (c : Graph.RotationCertificate) (h : ∀ i < c.successor.length, c.successor.getD i 0 < c.successor.length) : restrictPrefix c.successor.length c = c

Restriction to the full table is literal identity when every successor stays within its length. This includes the empty table, without inventing a positive scan clock.

theorem Cslib.Complexity.CSP.OrderedBoundary.getD_restrictPrefix_two (c : Graph.RotationCertificate) (darts i : ℕ) (hi : i < darts) (hc : 2 ≤ c.successor.length) (hs : darts ≤ c.successor.getD i 0) (ht : c.successor.getD (c.successor.getD i 0) 0 < darts) : (restrictPrefix darts c).successor.getD i 0 = c.successor.getD (c.successor.getD i 0) 0

If the first successor is deleted and the second retained, two list-funded steps find the second successor exactly. No search clock depends on the numerical table entries.

theorem Cslib.Complexity.CSP.OrderedBoundary.getD_restrictPrefix_three (c : Graph.RotationCertificate) (darts i : ℕ) (hi : i < darts) (hc : 3 ≤ c.successor.length) (hs : darts ≤ c.successor.getD i 0) (ht : darts ≤ c.successor.getD (c.successor.getD i 0) 0) (hu : c.successor.getD (c.successor.getD (c.successor.getD i 0) 0) 0 < darts) : (restrictPrefix darts c).successor.getD i 0 = c.successor.getD (c.successor.getD (c.successor.getD i 0) 0) 0

If exactly the first two successors are deleted, three list-funded steps find the third successor. In particular the clock is not funded by the deleted numerical indices.

theorem Cslib.Complexity.CSP.OrderedBoundary.restrictPrefix_restrictPrefix_of_short_returns (c : Graph.RotationCertificate) (m n : ℕ) (hmn : m ≤ n) (hc : 2 ≤ c.successor.length) (hshort : ∀ i < m, c.successor.getD i 0 < m ∨ c.successor.getD (c.successor.getD i 0) 0 < m) : restrictPrefix m (restrictPrefix n c) = restrictPrefix m c

An intermediate restriction does not change first returns that reach the smaller prefix in at most two steps. Both scans use their literal list-funded clocks; the raw table may be malformed away from the stated prefix. This applies to distinct boundary markers.