Numeric initialization schedule for direct tableau serialization

This module exposes the state, head, input-cell, and writable-cell segments of the direct deterministic initialization fragment. Its variable indices are natural numbers; machine states and symbols occur only as fixed finite parameters or in proof adapters.

The final equality is intentionally literal equality of raw gate lists. It does not yet construct a Turing machine that emits those gates.

Main results

• length_directInitSchedule gives the exact configuration-block width.
• getElem_directInitSchedule_configIndex identifies every scheduled gate.
• directInitSchedule_eq_initFragment identifies the schedule with the existing positive-input initialization fragment.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_indexedGateBlocks (count width : ℕ) (blockAt : ℕ → CircuitCode.RawCircuit) (hlen : ∀ index < count, List.length (blockAt index) = width) : List.length (indexedGateBlocks count blockAt) = count * width

An indexed concatenation of fixed-width blocks has the expected length.

theorem Complexity.CircuitUnrolling.Serializer.getElem_indexedGateBlocks (count width : ℕ) (blockAt : ℕ → CircuitCode.RawCircuit) (hlen : ∀ index < count, List.length (blockAt index) = width) (blockIndex offset : ℕ) (hblock : blockIndex < count) (hoffset : offset < width) : (indexedGateBlocks count blockAt)[blockIndex * width + offset] = (blockAt blockIndex)[offset]

A numeric block index and in-block offset recover the corresponding gate.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitStartCell : List.length directInitStartCell = 4

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitBlankCell : List.length directInitBlankCell = 4

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitDataCell (inputIndex : ℕ) : List.length (directInitDataCell inputIndex) = 4

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitStateGates {k : ℕ} (tm : TM k) : List.length (directInitStateGates tm) = Fintype.card tm.Q

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitHeadTapeGates (T : ℕ) : List.length (directInitHeadTapeGates T) = T + 1

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitHeadGates (k T : ℕ) : List.length (directInitHeadGates k T) = (k + 2) * (T + 1)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitInputDataGates (n : ℕ) : List.length (directInitInputDataGates n) = 4 * n

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitInputBlankTailGates (T n : ℕ) : List.length (directInitInputBlankTailGates T n) = 4 * (T + 1 - n)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitInputCellGates (T n : ℕ) (hn : n ≤ T + 1) : List.length (directInitInputCellGates T n) = 4 * (T + 2)

The marker, data, and blank-tail input ranges cover exactly one tape.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitBlankTapeCellGates (T : ℕ) : List.length (directInitBlankTapeCellGates T) = 4 * (T + 2)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitWritableCellGates (k T : ℕ) : List.length (directInitWritableCellGates k T) = 4 * (k + 1) * (T + 2)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_directInitSchedule {k : ℕ} (tm : TM k) (T n : ℕ) (hn : n ≤ T + 1) : List.length (directInitSchedule tm T n) = configWidth tm.toNTM T

The four concatenated ranges occupy exactly one configuration block.

theorem Complexity.CircuitUnrolling.Serializer.getElem_directInitSchedule_configIndex {k : ℕ} (tm : TM k) (T n : ℕ) [NeZero n] (hn : n ≤ T + 1) (atom : ConfigAtom tm.toNTM T) : (directInitSchedule tm T n)[configIndex tm.toNTM T atom] = (initSource tm.toNTM T n n (deterministicInputWires T n) atom).gate

Every canonical configuration index selects its intended initialization gate. ConfigAtom is used only to state the proof adapter, not as schedule run-time state.

theorem Complexity.CircuitUnrolling.Serializer.directInitSchedule_eq_initFragment {k : ℕ} (tm : TM k) (T n : ℕ) [NeZero n] (hn : n + 1 ≤ T) : directInitSchedule tm T n = initFragment tm.toNTM T n n (deterministicInputWires T n)

Under the normalized positive-input horizon bound, the numeric schedule is literally the existing initialization fragment's raw gate list.