Direct binary counter resource certificates

The original borrow and leading-zero normalization folds compute the predecessor. Its time is quadratic and its charged workspace linear in the binary input length. The successor's certificate here is a weakening of the streaming transducer computableInTimeAndSpace_succ; the carry rounds remain as the shared step of binary addition. The zero test uses the existing empty-word machine. All round certificates are plain; normalization occurs only when the internal machine combinators construct the fold.

Main results

• ComputableInO.succStep, ComputableInO.succFinish: shared linear carry-round certificates for binary addition.
• ComputableInO.natSucc, ComputableInO.natPred: quadratic-time, linear-space binary counters.
• ComputableInO.natIsZero: linear zero testing.

theorem Turing.MultiTapeTM.ComputableInO.succStep : ComputableInO (fun (p : (Bool × List Bool) × Bool) => NatSucc.succStep p.1 p.2) (encPair (encPair encBool encBits) encBool) (encPair encBool encBits) (fun (p : (Bool × List Bool) × Bool) => ((encPair (encPair encBool encBits) encBool) p).length) fun (p : (Bool × List Bool) × Bool) => ((encPair (encPair encBool encBits) encBool) p).length

One consuming carry round has linear time and charged workspace.

theorem Turing.MultiTapeTM.ComputableInO.succFinish : ComputableInO NatSucc.succFinish (encPair encBool encBits) encBits (fun (p : Bool × List Bool) => ((encPair encBool encBits) p).length) fun (p : Bool × List Bool) => ((encPair encBool encBits) p).length

Appending the final carry has linear time and charged workspace.

theorem Turing.MultiTapeTM.ComputableInO.foldl_bits {β : Type} {encB : β ↪ List Bool} {init : β} {step : β → Bool → β} (hstep : ComputableInO (fun (p : β × Bool) => step p.1 p.2) (encPair encB encBool) encB (fun (p : β × Bool) => ((encPair encB encBool) p).length) fun (p : β × Bool) => ((encPair encB encBool) p).length) (b : ℕ) (hb : ∀ (l : List Bool) (i : ℕ), (encB (List.foldl step init (List.take i l))).length ≤ l.length + b) : ComputableInO (fun (l : List Bool) => List.foldl step init l) encBits encB (fun (l : List Bool) => (l.length + 1) ^ 2) fun (l : List Bool) => l.length + 1

A fold over binary words retains quadratic time and linear charged workspace when its reachable encoded prefix states have length at most the original word length plus a constant.

theorem Turing.MultiTapeTM.ComputableInO.natSucc : ComputableInO (fun (x : ℕ) => x + 1) encNat encNat (fun (n : ℕ) => ((encNat n).length + 1) ^ 2) fun (n : ℕ) => (encNat n).length + 1

Binary successor within the quadratic clock and linear charged workspace used by its clients, weakened from the linear-time, zero-work-space transducer certificate computableInTimeAndSpace_succ.

theorem Turing.MultiTapeTM.ComputableInO.natPred : ComputableInO (fun (x : ℕ) => x - 1) encNat encNat (fun (n : ℕ) => ((encNat n).length + 1) ^ 2) fun (n : ℕ) => (encNat n).length + 1

Binary predecessor keeps zero at zero and preserves the original independent resource bounds.

theorem Turing.MultiTapeTM.ComputableInO.natIsZero : ComputableInO (fun (n : ℕ) => decide (n = 0)) encNat encBool (fun (n : ℕ) => (encNat n).length) fun (n : ℕ) => (encNat n).length

Zero testing is linear in both resources; the output charge remains explicit.