Numeric finalization schedule for direct tableau serialization

This definitions layer describes the acceptance, padding, and terminal-copy tail of a positive padded direct-unrolling circuit using natural-number addresses and counts. The machine and its distinguished halt state remain fixed compile-time parameters in the bridge theorems; no run-time schedule value contains a configuration atom or formula tree.

def Complexity.CircuitUnrolling.Serializer.numericAcceptanceGate (stateCount haltStateIndex tapeCount T finalConfigBase : ℕ) : CircuitCode.RawGate

Acceptance gate addressed by state count, halt-state index, tape count, horizon, and the base of the final packed configuration.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.directOriginalRawGateCount {k : ℕ} (tm : TM k) (T : ℕ) : ℕ

Exact gate count of an unpadded direct tableau with horizon T.

Equations

• Complexity.CircuitUnrolling.Serializer.directOriginalRawGateCount tm T = Complexity.CircuitUnrolling.configWidth tm.toNTM T + T * Complexity.CircuitUnrolling.directStepSize tm.toNTM T + 1

def Complexity.CircuitUnrolling.Serializer.directPaddingSchedule (originalRawGateCount closedBound : ℕ) : CircuitCode.RawCircuit

Dead constant-false padding determined only by the original and closed gate counts.

Equations

• Complexity.CircuitUnrolling.Serializer.directPaddingSchedule originalRawGateCount closedBound = List.replicate (closedBound - originalRawGateCount) (Complexity.CircuitCode.RawGate.constant 0 false)

def Complexity.CircuitUnrolling.Serializer.directTerminalCopyGate (n originalRawGateCount : ℕ) : CircuitCode.RawGate

Final output gate copying the original raw circuit's last wire.

Equations

• Complexity.CircuitUnrolling.Serializer.directTerminalCopyGate n originalRawGateCount = Complexity.CircuitCode.RawGate.copy (n + originalRawGateCount - 1)

def Complexity.CircuitUnrolling.Serializer.directFinalizationSuffix (n originalRawGateCount closedBound : ℕ) : CircuitCode.RawCircuit

Numeric tail following the original raw circuit: dead padding, then its terminal output copy.

Equations

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