Machine emission of terminated-unary natural codes — definitions

This module defines a small circuit-serialization consumer of TM.binaryForTM. A canonical binary scratch counter starts at zero, a distinct canonical tape stores the preserved value, and the loop emits one true bit per counter value below the limit. The final phases clear the scratch tape back to canonical zero and emit the terminating false bit.

The resulting output suffix is exactly NatCode.encode value; input, the preserved limit, the restored scratch counter, and every unrelated work tape are intended to be preserved literally.

def Complexity.CircuitCode.Machine.emitNatCodeLoopTM {n : ℕ} (counterIdx limitIdx : Fin n) : TM n

Emit the unary body of a natural-number code while counting on a canonical binary scratch tape.

Equations

• Complexity.CircuitCode.Machine.emitNatCodeLoopTM counterIdx limitIdx = (Complexity.TM.emitBitsTM [true]).binaryForTM counterIdx limitIdx

def Complexity.CircuitCode.Machine.emitNatCodeTM {n : ℕ} (counterIdx limitIdx : Fin n) : TM n

Emit NatCode.encode value from a canonical binary limit.

After the binary loop emits value one-bits, the machine clears the scratch counter to canonical zero and appends the terminating zero-bit.

Equations

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

def Complexity.CircuitCode.Machine.emitNatCodeLoopTime (value : ℕ) : ℕ

Exact running time of the binary loop that emits the unary body.

Equations

• Complexity.CircuitCode.Machine.emitNatCodeLoopTime value = Complexity.TM.binaryForLoopTime (fun (x : ℕ) => 1) value 0 value

def Complexity.CircuitCode.Machine.emitNatCodeTime (value : ℕ) : ℕ

Concrete time bound for terminated-unary emission, including the two sequential-composition seams and scratch clearing.

Equations

• Complexity.CircuitCode.Machine.emitNatCodeTime value = Complexity.CircuitCode.Machine.emitNatCodeLoopTime value + 2 * value.size + 8

def Complexity.CircuitCode.Machine.emitNatCodeSpace (initialSpace value : ℕ) : ℕ

Auxiliary-space bound for natural-code emission from a configuration already fitting in initialSpace.

Equations

• Complexity.CircuitCode.Machine.emitNatCodeSpace initialSpace value = initialSpace + 2 * value.size + 5