Numeric initialization schedule for direct tableau serialization

This definitions layer flattens the positive-input initialization fragment into state, head, and cell segments. Variable schedule data consists only of natural-number indices and positions. Machine states remain fixed finite parameters, and symbol order is baked into four-gate cell blocks.

Input cells are separated into the left marker, data positions 1, ..., n, and the blank tail. Work and output tapes share one blank-tape schedule. No run-time schedule value stores a configuration atom or formula tree.

def Complexity.CircuitUnrolling.Serializer.indexedGateBlocks (count : ℕ) : (ℕ → CircuitCode.RawCircuit) → CircuitCode.RawCircuit

Concatenate count blocks supplied by an increasing natural index.

Equations

• Complexity.CircuitUnrolling.Serializer.indexedGateBlocks 0 x✝ = []
• Complexity.CircuitUnrolling.Serializer.indexedGateBlocks count.succ x✝ = x✝ 0 ++ Complexity.CircuitUnrolling.Serializer.indexedGateBlocks count fun (index : ℕ) => x✝ (index + 1)

def Complexity.CircuitUnrolling.Serializer.directInitConstant (value : Bool) : CircuitCode.RawGate

One raw constant gate using existing wire zero.

Equations

• Complexity.CircuitUnrolling.Serializer.directInitConstant value = Complexity.CircuitCode.RawGate.constant 0 value

def Complexity.CircuitUnrolling.Serializer.directInitStartCell : CircuitCode.RawCircuit

Symbol gates for a left-marker cell, in zero/one/blank/start order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitBlankCell : CircuitCode.RawCircuit

Symbol gates for a blank cell, in zero/one/blank/start order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitDataCell (inputIndex : ℕ) : CircuitCode.RawCircuit

Symbol gates for one data cell whose source is primary wire inputIndex.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.directInitStateGates {k : ℕ} (tm : TM k) : CircuitCode.RawCircuit

Initial-state one-hot gates in the machine's fixed finite-state order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitHeadGate (position : ℕ) : CircuitCode.RawGate

One head-position gate: exactly position zero is initially active.

Equations

• Complexity.CircuitUnrolling.Serializer.directInitHeadGate position = Complexity.CircuitUnrolling.Serializer.directInitConstant (decide (position = 0))

def Complexity.CircuitUnrolling.Serializer.directInitHeadTapeGates (T : ℕ) : CircuitCode.RawCircuit

Initial head gates for one tape, at positions 0, ..., T.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitHeadGates (k T : ℕ) : CircuitCode.RawCircuit

Initial head gates in input/work/output tape-major order.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitInputDataGates (n : ℕ) : CircuitCode.RawCircuit

Input data-cell gates for positions 1, ..., n; block index i reads wire i.

Equations

• Complexity.CircuitUnrolling.Serializer.directInitInputDataGates n = Complexity.CircuitUnrolling.Serializer.indexedGateBlocks n Complexity.CircuitUnrolling.Serializer.directInitDataCell

def Complexity.CircuitUnrolling.Serializer.directInitInputBlankTailGates (T n : ℕ) : CircuitCode.RawCircuit

Blank input-cell gates for positions n + 1, ..., T + 1.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitInputCellGates (T n : ℕ) : CircuitCode.RawCircuit

Complete input-tape cell segment: marker, data, then blank tail.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitBlankTapeCellGates (T : ℕ) : CircuitCode.RawCircuit

Cell segment for one initially blank work or output tape.

Equations

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

def Complexity.CircuitUnrolling.Serializer.directInitWritableCellGates (k T : ℕ) : CircuitCode.RawCircuit

Cell gates for all work tapes followed by the output tape.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.directInitSchedule {k : ℕ} (tm : TM k) (T n : ℕ) : CircuitCode.RawCircuit

Complete direct positive-input initialization schedule.

Equations

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