Numeric finalization schedule for direct tableau serialization

This module exposes a natural-number acceptance gate, exact padding and terminal-copy phase laws, and the complete literal decomposition of every normalized positive padded direct-unrolling circuit. Together with the numeric initialization schedule and canonical transition fragments, the decomposition specifies the raw gate stream without run-time configuration atoms or formulas.

Main results

• numericAcceptanceGate_eq_acceptanceGate identifies the arithmetic gate.
• directUnrollingRawCircuit_length_eq_original gives the exact unpadded count.
• paddedDirectUnrollingRawCircuit_eq_numericSchedule gives the complete raw list decomposition.

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

The numeric state/output-cell addresses literally produce the existing acceptance gate for the fixed deterministic machine.

@[simp]

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

The numeric padding phase contains exactly the closed-bound shortfall.

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

Every index in the numeric padding phase emits a dead constant-false gate.

@[simp]

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

Padding followed by the terminal copy has shortfall-plus-one gates.

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

Indices before the finalization boundary are exactly the padding phase.

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

The gate at the finalization boundary is the terminal original-output copy.

@[simp]

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

Every canonical deterministic transition fragment has the fixed numeric layer size.

@[simp]

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

The unpadded raw tableau has one initial block, T equal transition fragments, and one acceptance gate.

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

A normalized positive padded direct tableau is literally numeric initialization, canonical transition fragments, numeric acceptance, dead padding, and one terminal copy of the original acceptance output.