Compositional width bounds for binary routines

This module exposes pointwise width certificates for routine leaves, sequential composition, fixed repetition, branches, and binary loops. Loop certificates collapse the recursive maximum in binaryForSpace to four local obligations, so the number of iterations does not appear additively in the resulting auxiliary-space bound. A final polynomial width bound converts the composed certificate to logarithmic space.

theorem Complexity.BinaryRoutine.values_update_le {n : ℕ} {values : BinaryValues n} {width value : ℕ} (index : Fin n) (hvalues : ∀ (current : Fin n), values current ≤ width) (hvalue : value ≤ width) (current : Fin n) : Function.update values index value current ≤ width

Updating one binary register preserves a common pointwise upper bound when both the old vector and the replacement value satisfy that bound.

theorem Complexity.BinaryRoutine.SpaceBoundInLogAt.of_le {n : ℕ} {routine : BinaryRoutine n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {bound : ℕ → ℕ} (hle : ∀ (inputLength : ℕ), routine.spaceBound (initialSpace inputLength) (values inputLength) ≤ bound inputLength) (hbound : BigO bound fun (inputLength : ℕ) => Nat.log 2 inputLength) : routine.SpaceBoundInLogAt initialSpace values

A pointwise logarithmic envelope proves logarithmic routine space along a fixed input-indexed trajectory.

theorem Complexity.BinaryRoutine.SpaceBoundInLogAt.restrict {n : ℕ} {routine : BinaryRoutine n} {requires : BinaryValues n → Prop} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} (hspace : routine.SpaceBoundInLogAt initialSpace values) : (routine.restrict requires).SpaceBoundInLogAt initialSpace values

Strengthening a precondition preserves an asymptotic space certificate.

theorem Complexity.BinaryRoutine.SpaceBoundInLogAt.seq {n : ℕ} {first second : BinaryRoutine n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} (hfirst : first.SpaceBoundInLogAt initialSpace values) (hsecond : second.SpaceBoundInLogAt initialSpace fun (inputLength : ℕ) => first.effect (values inputLength)) : (first.seq second).SpaceBoundInLogAt initialSpace values

Sequential phases preserve logarithmic space when the second certificate is stated along the first phase's exact pure effect.

theorem Complexity.BinaryRoutine.SpaceBoundInLogAt.branchZero {n : ℕ} {onZero onPositive : BinaryRoutine n} (idx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} (hzero : onZero.SpaceBoundInLogAt initialSpace values) (hpositive : onPositive.SpaceBoundInLogAt initialSpace values) : (BinaryRoutine.branchZero idx onZero onPositive).SpaceBoundInLogAt initialSpace values

Both branches sharing one logarithmic envelope make a zero branch logarithmic, independently of which branch is selected at each input.

theorem Complexity.BinaryRoutine.SpaceBoundInLogAt.binaryFor_of_envelope {n : ℕ} {body : BinaryRoutine n} {counterIdx limitIdx : Fin n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {bound : ℕ → ℕ} (henvelope : ∀ (inputLength : ℕ), body.BinaryForSpaceEnvelope counterIdx limitIdx (initialSpace inputLength) (values inputLength) (bound inputLength)) (hbound : BigO bound fun (inputLength : ℕ) => Nat.log 2 inputLength) : (body.binaryFor counterIdx limitIdx).SpaceBoundInLogAt initialSpace values

A logarithmic pointwise envelope for all reachable comparisons, iterations, and successors proves logarithmic space for a binary loop.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.mono {n : ℕ} {routine : BinaryRoutine n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width width' : ℕ → ℕ} (hspace : routine.SpaceBoundByWidthAt initialSpace values width) (hle : ∀ (inputLength : ℕ), width inputLength ≤ width' inputLength) : routine.SpaceBoundByWidthAt initialSpace values width'

Enlarging the controlling value preserves a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.restrict {n : ℕ} {routine : BinaryRoutine n} {requires : BinaryValues n → Prop} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hspace : routine.SpaceBoundByWidthAt initialSpace values width) : (routine.restrict requires).SpaceBoundByWidthAt initialSpace values width

Strengthening a precondition preserves a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitBits {n : ℕ} (word : List Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} : (BinaryRoutine.emitBits word).SpaceBoundByWidthAt initialSpace values width

Fixed-word emission has a pointwise width certificate for every input trajectory.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.identity {n : ℕ} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} : BinaryRoutine.identity.SpaceBoundByWidthAt initialSpace values width

The routine identity has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.clear {n : ℕ} (idx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hvalue : ∀ (inputLength : ℕ), values inputLength idx ≤ width inputLength) : (BinaryRoutine.clear idx).SpaceBoundByWidthAt initialSpace values width

Clearing a value bounded by the controlling width has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.binarySucc {n : ℕ} (idx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hvalue : ∀ (inputLength : ℕ), values inputLength idx ≤ width inputLength) : (BinaryRoutine.binarySucc idx).SpaceBoundByWidthAt initialSpace values width

Successor on a value bounded by the controlling width has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryPred {n : ℕ} (idx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hvalue : ∀ (inputLength : ℕ), values inputLength idx - 1 + 1 ≤ width inputLength) : (BinaryRoutine.binaryPred idx).SpaceBoundByWidthAt initialSpace values width

Predecessor has a pointwise width certificate when its exact positive space argument is bounded by the controlling value.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryCopy {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hsrc : ∀ (inputLength : ℕ), values inputLength srcIdx ≤ width inputLength) (hdst : ∀ (inputLength : ℕ), values inputLength dstIdx ≤ width inputLength) : (BinaryRoutine.binaryCopy srcIdx dstIdx counterIdx).SpaceBoundByWidthAt initialSpace values width

Copying two width-bounded values has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.addConst {n : ℕ} (idx : Fin n) (constant : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hvalue : ∀ (inputLength : ℕ), values inputLength idx + constant ≤ width inputLength) : (BinaryRoutine.addConst idx constant).SpaceBoundByWidthAt initialSpace values width

Fixed addition has a pointwise width certificate when its result is bounded by the controlling value.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.set {n : ℕ} (idx : Fin n) (value : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hcurrent : ∀ (inputLength : ℕ), values inputLength idx ≤ width inputLength) (hvalue : ∀ (inputLength : ℕ), value ≤ width inputLength) : (BinaryRoutine.set idx value).SpaceBoundByWidthAt initialSpace values width

Setting a width-bounded value to another width-bounded value has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.add {n : ℕ} (srcIdx dstIdx counterIdx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hsrc : ∀ (inputLength : ℕ), values inputLength srcIdx ≤ width inputLength) (hsum : ∀ (inputLength : ℕ), values inputLength dstIdx + values inputLength srcIdx ≤ width inputLength) : (BinaryRoutine.add srcIdx dstIdx counterIdx).SpaceBoundByWidthAt initialSpace values width

Preserved-source addition has a pointwise width certificate when its source and result are bounded by the controlling value.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.mulAdd {n : ℕ} (leftIdx rightIdx accIdx mulCounterIdx addCounterIdx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hleft : ∀ (inputLength : ℕ), values inputLength leftIdx ≤ width inputLength) (hright : ∀ (inputLength : ℕ), values inputLength rightIdx ≤ width inputLength) (htotal : ∀ (inputLength : ℕ), values inputLength accIdx + values inputLength leftIdx * values inputLength rightIdx + values inputLength leftIdx ≤ width inputLength) : (BinaryRoutine.mulAdd leftIdx rightIdx accIdx mulCounterIdx addCounterIdx).SpaceBoundByWidthAt initialSpace values width

Multiply-add has a pointwise width certificate when both factors and the largest addition intermediate are width-bounded.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.evalPolynomial {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (p : Polynomial ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hvalue : ∀ (inputLength : ℕ), 2 * TM.binaryPolynomialValueCap p (values inputLength inputIdx) ≤ width inputLength) : (BinaryRoutine.evalPolynomial inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx p).SpaceBoundByWidthAt initialSpace values width

Fixed-polynomial evaluation has a pointwise width certificate when its explicit Horner-prefix cap is width-bounded.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitNatCode {n : ℕ} (counterIdx valueIdx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hvalue : ∀ (inputLength : ℕ), values inputLength valueIdx ≤ width inputLength) : (BinaryRoutine.emitNatCode counterIdx valueIdx).SpaceBoundByWidthAt initialSpace values width

Natural-code emission of a width-bounded value has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitRawGate {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx input₀Idx input₁Idx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hinput₀ : ∀ (inputLength : ℕ), values inputLength input₀Idx ≤ width inputLength) (hinput₁ : ∀ (inputLength : ℕ), values inputLength input₁Idx ≤ width inputLength) : (BinaryRoutine.emitRawGate op negated₀ negated₁ emitCounterIdx input₀Idx input₁Idx).SpaceBoundByWidthAt initialSpace values width

Raw-gate emission from two width-bounded references has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.emitRawGateStep {n : ℕ} (op : AndOrOp) (negated₀ negated₁ : Bool) (emitCounterIdx availableIdx input₀Idx input₁Idx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength availableIdx ≤ width inputLength) (hinput₀ : ∀ (inputLength : ℕ), values inputLength input₀Idx ≤ width inputLength) (hinput₁ : ∀ (inputLength : ℕ), values inputLength input₁Idx ≤ width inputLength) : (BinaryRoutine.emitRawGateStep op negated₀ negated₁ emitCounterIdx availableIdx input₀Idx input₁Idx).SpaceBoundByWidthAt initialSpace values width

Emitting and advancing one gate from width-bounded references and a width-bounded frontier has a pointwise width certificate.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.seq {n : ℕ} {first second : BinaryRoutine n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hfirst : first.SpaceBoundByWidthAt initialSpace values width) (hsecond : second.SpaceBoundByWidthAt initialSpace (fun (inputLength : ℕ) => first.effect (values inputLength)) width) : (first.seq second).SpaceBoundByWidthAt initialSpace values width

Sequential pointwise width certificates compose along the first phase's exact pure effect.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.seqList {n : ℕ} (routines : List (BinaryRoutine n)) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hspace : SeqListSpaceBoundByWidthAt routines initialSpace values width) : (BinaryRoutine.seqList routines).SpaceBoundByWidthAt initialSpace values width

A list of pointwise width certificates composes along its exact pure prefix effects.

theorem Complexity.BinaryRoutine.SeqListSpaceBoundByWidthAt.append {n : ℕ} (first second : List (BinaryRoutine n)) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hfirst : SeqListSpaceBoundByWidthAt first initialSpace values width) (hsecond : SeqListSpaceBoundByWidthAt second initialSpace (fun (inputLength : ℕ) => (seqList first).effect (values inputLength)) width) : SeqListSpaceBoundByWidthAt (first ++ second) initialSpace values width

Width certificates for two routine lists compose when the second list is certified along the first list's exact pure effect.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.repeatRoutine_of_invariant {n : ℕ} (count : ℕ) (routine : BinaryRoutine n) (invariant : BinaryValues n → Prop) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hvalues : ∀ (inputLength : ℕ), invariant (values inputLength)) (hspace : ∀ (trajectory : ℕ → BinaryValues n), (∀ (inputLength : ℕ), invariant (trajectory inputLength)) → routine.SpaceBoundByWidthAt initialSpace trajectory width) (heffect : ∀ (current : BinaryValues n), invariant current → invariant (routine.effect current)) : (repeatRoutine count routine).SpaceBoundByWidthAt initialSpace values width

Fixed repetition has a pointwise width certificate when one invariant both supplies the body certificate and is preserved by its pure effect.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.branchZero {n : ℕ} {onZero onPositive : BinaryRoutine n} (idx : Fin n) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hzero : onZero.SpaceBoundByWidthAt initialSpace values width) (hpositive : onPositive.SpaceBoundByWidthAt initialSpace values width) : (BinaryRoutine.branchZero idx onZero onPositive).SpaceBoundByWidthAt initialSpace values width

Pointwise width certificates for both branches certify a zero branch.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.to_log {n : ℕ} {routine : BinaryRoutine n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hspace : routine.SpaceBoundByWidthAt initialSpace values width) (hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength) (p : Polynomial ℕ) (hwidth : ∀ (inputLength : ℕ), width inputLength ≤ Polynomial.eval inputLength p) : routine.SpaceBoundInLogAt initialSpace values

A polynomial upper bound on the controlling value turns a pointwise width certificate into logarithmic space.

theorem Complexity.BinaryRoutine.SpaceBoundInLogAt.emitBits {n : ℕ} (word : List Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} (hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength) : (BinaryRoutine.emitBits word).SpaceBoundInLogAt initialSpace values

Fixed-word emission preserves logarithmic incoming space.

theorem Complexity.BinaryRoutine.SpaceBoundInLogAt.identity {n : ℕ} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} (hinitial : BigO initialSpace fun (inputLength : ℕ) => Nat.log 2 inputLength) : BinaryRoutine.identity.SpaceBoundInLogAt initialSpace values

The routine identity preserves logarithmic incoming space.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryFor_of_envelope {n : ℕ} {body : BinaryRoutine n} {counterIdx limitIdx : Fin n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (constant : ℕ) (henvelope : ∀ (inputLength : ℕ), body.BinaryForSpaceEnvelope counterIdx limitIdx (initialSpace inputLength) (values inputLength) (initialSpace inputLength + constant * (width inputLength).size + constant)) : (body.binaryFor counterIdx limitIdx).SpaceBoundByWidthAt initialSpace values width

A pointwise loop envelope of the standard width-controlled form certifies the complete binary loop without exposing its recursive maximum.

theorem Complexity.BinaryRoutine.SpaceBoundByWidthAt.binaryFor_of_clamped_body {n : ℕ} {body : BinaryRoutine n} {counterIdx limitIdx : Fin n} {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues n} {width : ℕ → ℕ} (hlimit : ∀ (inputLength : ℕ), values inputLength limitIdx ≤ width inputLength) (hcounter : ∀ (inputLength count : ℕ), count < binaryForCount counterIdx limitIdx (values inputLength) → body.binaryForValues counterIdx (values inputLength) count counterIdx ≤ width inputLength) (hbody : body.SpaceBoundByWidthAt (fun (code : ℕ) => initialSpace (Nat.unpair code).1) (body.binaryForClampedValues counterIdx limitIdx values) fun (code : ℕ) => width (Nat.unpair code).1) : (body.binaryFor counterIdx limitIdx).SpaceBoundByWidthAt initialSpace values width

A width certificate over the canonical paired-and-clamped body trajectory lifts to the complete binary loop. The limit and every reachable counter value must fit the same width; the resulting constant is uniform in both the input index and the loop iteration.

theorem Complexity.BinaryRoutine.BinaryForSpaceEnvelope.iterationSpaceMax_le {n : ℕ} {body : BinaryRoutine n} {counterIdx limitIdx : Fin n} {initialSpace : ℕ} {initial : BinaryValues n} {bound : ℕ} (envelope : body.BinaryForSpaceEnvelope counterIdx limitIdx initialSpace initial bound) : body.binaryForIterationSpaceMax counterIdx initialSpace initial (binaryForCount counterIdx limitIdx initial) ≤ bound

A pointwise envelope bounds the recursive maximum over all reachable iterations.

theorem Complexity.BinaryRoutine.BinaryForSpaceEnvelope.binaryForSpace_le {n : ℕ} {body : BinaryRoutine n} {counterIdx limitIdx : Fin n} {initialSpace : ℕ} {initial : BinaryValues n} {bound : ℕ} (envelope : body.BinaryForSpaceEnvelope counterIdx limitIdx initialSpace initial bound) : body.binaryForSpace counterIdx limitIdx initialSpace initial ≤ bound

A pointwise envelope bounds the complete comparison-plus-iteration space formula of a binary count-up loop.

theorem Complexity.BinaryRoutine.BinaryForSpaceEnvelope.spaceBound_le {n : ℕ} {body : BinaryRoutine n} {counterIdx limitIdx : Fin n} {initialSpace : ℕ} {initial : BinaryValues n} {bound : ℕ} (envelope : body.BinaryForSpaceEnvelope counterIdx limitIdx initialSpace initial bound) : (body.binaryFor counterIdx limitIdx).spaceBound initialSpace initial ≤ bound

A pointwise envelope directly bounds the advertised space budget of the corresponding proof-carrying binary loop.