Binary input-length counter — proof internals

The exact run proof scans the read-only input and lifts one proved binarySuccTM run per symbol. The space proof separately tracks every reachable driver/body phase so input length is never charged as work space.

def Complexity.TM.binaryLengthStartedBlank : Tape

A blank tape parked immediately to the right of its start marker.

Equations

• Complexity.TM.binaryLengthStartedBlank = (Complexity.Tape.init []).move Complexity.Dir3.right

def Complexity.TM.binaryLengthInput (x : List Bool) (head : ℕ) : Tape

The immutable input tape for x, with its head at head.

Equations

• Complexity.TM.binaryLengthInput x head = { head := head, cells := (Complexity.Tape.init (List.map Complexity.Γ.ofBool x)).cells }

def Complexity.TM.binaryLengthCounterTape (value : ℕ) : Tape

The canonical binary counter tape representing value.

Equations

• Complexity.TM.binaryLengthCounterTape value = (Complexity.Tape.init (List.map Complexity.Γ.ofBool value.bits)).move Complexity.Dir3.right

def Complexity.TM.binaryLengthWork {n : ℕ} (counterIdx : Fin n) (value : ℕ) : Fin n → Tape

Work tapes with value on the selected counter tape and blank tapes elsewhere.

Equations

• Complexity.TM.binaryLengthWork counterIdx value = Function.update (fun (x : Fin n) => Complexity.TM.binaryLengthStartedBlank) counterIdx (Complexity.TM.binaryLengthCounterTape value)

def Complexity.TM.binaryLengthDoneCfg {n : ℕ} (x : List Bool) (counterIdx : Fin n) : Cfg n (binaryLengthTM counterIdx).Q

Canonical halted configuration produced after measuring x.

Equations

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

Public-theorem internals

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

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

theorem Complexity.TM.binaryLengthTM_reachesIn_internal {n : ℕ} (counterIdx : Fin n) (x : List Bool) : (binaryLengthTM counterIdx).reachesIn (binaryLengthTime x.length) ((binaryLengthTM counterIdx).initCfg x) (binaryLengthDoneCfg x counterIdx)

theorem Complexity.TM.binaryLengthTM_reachesIn_frame_internal {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

theorem Complexity.TM.binaryLengthTM_hoareTime_internal {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)

theorem Complexity.TM.binaryLengthTM_hoareTimeSpace_internal {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)

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

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