Substituting width and depth bounds in Savitch's stack invariant

length_encState_le_of_bounds separates the stack accounting from the application-specific choice of vertex width. When depth and width are each bounded by a multiple of a common scale, the actual encoded state has a quadratic bound in that scale. The invariant still has to hold for the concrete state; a linear-space transition alone supplies no such guarantee.

theorem Cslib.Reachability.Savitch.length_encState_le_of_bounds {w d L D W : ℕ} {s : State} (h : Invariant w d s) (hd : d ≤ D * L) (hw : w ≤ W * L) (hL : 1 ≤ L) : (encState s).length ≤ 24 * (D + 1) * (D + W + 1) * L ^ 2

Depth times frame size gives a quadratic state bound when both are linear in L.