Numeric direct-tableau finalization -- proof internals

theorem Complexity.CircuitUnrolling.Serializer.numericAcceptanceGate_eq_acceptanceGate_internal {k : ℕ} (tm : TM k) (T finalConfigBase : ℕ) : numericAcceptanceGate (Fintype.card tm.Q) (stateIndex tm.toNTM tm.qhalt) (k + 2) T finalConfigBase = acceptanceGate tm.toNTM T finalConfigBase

theorem Complexity.CircuitUnrolling.Serializer.length_directPaddingSchedule_internal (originalRawGateCount closedBound : ℕ) : List.length (directPaddingSchedule originalRawGateCount closedBound) = closedBound - originalRawGateCount

theorem Complexity.CircuitUnrolling.Serializer.getElem_directPaddingSchedule_internal (originalRawGateCount closedBound : ℕ) (index : Fin (closedBound - originalRawGateCount)) : (directPaddingSchedule originalRawGateCount closedBound)[↑index] = CircuitCode.RawGate.constant 0 false

theorem Complexity.CircuitUnrolling.Serializer.length_directFinalizationSuffix_internal (n originalRawGateCount closedBound : ℕ) : List.length (directFinalizationSuffix n originalRawGateCount closedBound) = closedBound - originalRawGateCount + 1

theorem Complexity.CircuitUnrolling.Serializer.getElem_directFinalizationSuffix_padding_internal (n originalRawGateCount closedBound : ℕ) (index : Fin (closedBound - originalRawGateCount)) : (directFinalizationSuffix n originalRawGateCount closedBound)[↑index] = CircuitCode.RawGate.constant 0 false

theorem Complexity.CircuitUnrolling.Serializer.getElem_directFinalizationSuffix_terminal_internal (n originalRawGateCount closedBound : ℕ) : (directFinalizationSuffix n originalRawGateCount closedBound)[closedBound - originalRawGateCount] = directTerminalCopyGate n originalRawGateCount

theorem Complexity.CircuitUnrolling.Serializer.directStepFragment_length_internal {k : ℕ} (tm : TM k) (T n : ℕ) (index : Fin T) : List.length (tm.directStepFragment T n index) = directStepSize tm.toNTM T

theorem Complexity.CircuitUnrolling.Serializer.directUnrollingRawCircuit_length_eq_original_internal {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : List.length (tm.directUnrollingRawCircuit f n) = directOriginalRawGateCount tm (f n)

theorem Complexity.CircuitUnrolling.Serializer.paddedDirectUnrollingRawCircuit_eq_numericSchedule_internal {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] (hn : n + 1 ≤ f n) : tm.paddedDirectUnrollingRawCircuit f n = directInitSchedule tm (f n) n ++ List.flatMap (tm.directStepFragment (f n) n) (List.finRange (f n)) ++ [numericAcceptanceGate (Fintype.card tm.Q) (stateIndex tm.toNTM tm.qhalt) (k + 2) (f n) (n + f n * directStepSize tm.toNTM (f n))] ++ directPaddingSchedule (directOriginalRawGateCount tm (f n)) (tm.directUnrollingGateBound f n) ++ [directTerminalCopyGate n (directOriginalRawGateCount tm (f n))]