Numeric initialization schedule -- proof internals

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

theorem Complexity.CircuitUnrolling.Serializer.getElem_indexedGateBlocks_internal (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]

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

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

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

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

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

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

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

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

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

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

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

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

theorem Complexity.CircuitUnrolling.Serializer.getElem_directInitSchedule_configIndex_internal {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

theorem Complexity.CircuitUnrolling.Serializer.directInitSchedule_eq_initFragment_internal {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)