Compositional width bounds for binary routines -- definitions

SpaceBoundByWidthAt separates exact all-prefix resource accounting from the final asymptotic argument. Its certificates compose along pure value effects, while BinaryForSpaceEnvelope bounds an input-dependent loop by one envelope covering every reachable comparison, body invocation, and successor.

def Complexity.BinaryRoutine.SpaceBoundInLogAt {n : ℕ} (routine : BinaryRoutine n) (initialSpace : ℕ → ℕ) (values : ℕ → BinaryValues n) : Prop

A routine's advertised all-prefix space bound is logarithmic along one input-indexed initial-space and pure-value trajectory.

Equations

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

def Complexity.BinaryRoutine.SpaceBoundByWidthAt {n : ℕ} (routine : BinaryRoutine n) (initialSpace : ℕ → ℕ) (values : ℕ → BinaryValues n) (width : ℕ → ℕ) : Prop

A routine's advertised all-prefix space is bounded by one fixed multiple of the binary width of an input-indexed value, in addition to the incoming space budget. This pointwise certificate composes before any asymptotic reasoning is required.

Equations

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

def Complexity.BinaryRoutine.SeqListSpaceBoundByWidthAt {n : ℕ} : List (BinaryRoutine n) → (ℕ → ℕ) → (ℕ → BinaryValues n) → (ℕ → ℕ) → Prop

Pointwise width certificates for a list of routines, following the exact pure effect after every prefix.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.BinaryRoutine.SeqListSpaceBoundByWidthAt [] x✝² x✝¹ x✝ = True

structure Complexity.BinaryRoutine.BinaryForSpaceEnvelope {n : ℕ} (body : BinaryRoutine n) (counterIdx limitIdx : Fin n) (initialSpace : ℕ) (initial : BinaryValues n) (bound : ℕ) : Prop

A single pointwise upper bound for every component of one binary count-up loop's advertised auxiliary-space budget.

• compareSpace : initialSpace + TM.binaryForCompareTime (initial limitIdx) ≤ bound

  The full-width counter/limit comparison fits in the envelope.

• initialSpace_le : initialSpace ≤ bound

  The zero-iteration base case fits in the envelope.

• bodySpace (count : ℕ) : count < binaryForCount counterIdx limitIdx initial → body.spaceBound initialSpace (body.binaryForValues counterIdx initial count) ≤ bound

  Every reachable body invocation fits in the envelope.

• successorSpace (count : ℕ) : count < binaryForCount counterIdx limitIdx initial → let current := body.binaryForValues counterIdx initial count; initialSpace + TM.binarySuccTime (current counterIdx) ≤ bound

  Every reachable controller successor fits in the envelope.

def Complexity.BinaryRoutine.binaryForClampedValues {n : ℕ} (body : BinaryRoutine n) (counterIdx limitIdx : Fin n) (values : ℕ → BinaryValues n) (code : ℕ) : BinaryValues n

A single input-indexed trajectory containing every reachable body-entry state of a binary loop. Pairing the input index with an arbitrary iteration index lets one SpaceBoundByWidthAt certificate expose a constant uniform in both parameters. Out-of-range iterations are clamped to the last valid index; the zero-iteration case is harmless because no body state is then queried.

Equations

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