Binary input-length counter

This module exposes a read-only input scan that counts every Boolean input symbol in canonical little-endian binary on one designated work tape. The machine preserves input cells; output and unrelated work tapes remain blank and finish with their heads initialized at cell one.

The resource contracts are deliberately separate: the runtime theorem gives an n · size(n)-shaped bound, while the all-reachable auxiliary-space proof reuses the local successor bound at each iteration and is formally O(log n).

Main results

• TM.binaryLengthTM_reachesIn_frame — exact endpoint and complete tape frame.
• TM.binaryLengthTM_hoareTimeSpace — time-bounded and all-reachable space contract.
• TM.binaryLengthSpace_bigO_log — the explicit space budget is logarithmic.
• TM.Experimental.binaryLengthRoutine_transducerSafe — the experimental routine is structurally output-safe.
• TM.binaryLengthTM_isTransducer — the output head never moves left.

theorem Complexity.TM.binaryLengthTime_le (length : ℕ) : binaryLengthTime length ≤ 2 + length * (2 * length.size + 4)

The exact binary-length-counter runtime has a concrete O(n log n)-shaped upper bound.

theorem Complexity.TM.binaryLengthSpace_bigO_log : BigO binaryLengthSpace fun (length : ℕ) => Nat.log 2 length

The explicit all-reachable auxiliary-space budget is logarithmic.

theorem Complexity.TM.binaryLengthTM_reachesIn_frame {n : ℕ} (counterIdx : Fin n) (x : List Bool) : ∃ (c' : Cfg n (binaryLengthTM counterIdx).Q), (binaryLengthTM counterIdx).reachesIn (binaryLengthTime x.length) ((binaryLengthTM counterIdx).initCfg x) c' ∧ (binaryLengthTM counterIdx).halted c' ∧ c'.input.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ c'.input.head = x.length + 1 ∧ (c'.work counterIdx).HasBinaryNat x.length ∧ (∀ (i : Fin n), i ≠ counterIdx → c'.work i = (Tape.init []).move Dir3.right) ∧ c'.output = (Tape.init []).move Dir3.right

From fresh tapes, the machine halts after exactly binaryLengthTime transitions with the canonical binary input length on counterIdx. Input cells are preserved exactly; output and unrelated work tapes remain blank and finish with their heads at cell one.

theorem Complexity.TM.binaryLengthTM_hoareTime {n : ℕ} (counterIdx : Fin n) (x : List Bool) : (binaryLengthTM counterIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin n) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = x.length + 1 ∧ (work counterIdx).HasBinaryNat x.length ∧ (∀ (i : Fin n), i ≠ counterIdx → work i = (Tape.init []).move Dir3.right) ∧ out = (Tape.init []).move Dir3.right) (binaryLengthTime x.length)

Fresh-start time-bounded Hoare contract for binary length counting.

theorem Complexity.TM.binaryLengthTM_hoareTimeSpace {n : ℕ} (counterIdx : Fin n) (x : List Bool) : (binaryLengthTM counterIdx).HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin n) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.cells = (Tape.init (List.map Γ.ofBool x)).cells ∧ inp.head = x.length + 1 ∧ (work counterIdx).HasBinaryNat x.length ∧ (∀ (i : Fin n), i ≠ counterIdx → work i = (Tape.init []).move Dir3.right) ∧ out = (Tape.init []).move Dir3.right) (binaryLengthTime x.length) x.length (binaryLengthSpace x.length)

Time-bounded and honest all-reachable auxiliary-space contract. In particular, this does not derive space from the total runtime.

theorem Complexity.TM.Experimental.binaryLengthRoutine_transducerSafe {n : ℕ} (counterIdx : Fin n) : (binaryLengthRoutine counterIdx).TransducerSafe

Binary length counting is assembled only from transducer-safe routine constructors and calls.

theorem Complexity.TM.binaryLengthTM_isTransducer {n : ℕ} (counterIdx : Fin n) : (binaryLengthTM counterIdx).IsTransducer

binaryLengthTM is safe for append-only-output composition.