Streamable deterministic unrolling arithmetic — definitions

This definitions layer isolates the numeric data needed by a future streaming serializer. Formula tree sizes do not depend on the absolute wire numbers stored at their leaves, so one canonical choice of incoming bases determines the size of every transition formula and of every packed transition layer.

The direct deterministic prefix build fixes the primary-wire layout used by TM.directUnrollingRawCircuit. It remains a proof-level circuit construction; no Turing-machine generator is defined here.

noncomputable def Complexity.CircuitUnrolling.directStepFormulaSize {k : ℕ} (tm : NTM k) (T : ℕ) (atom : ConfigAtom tm T) : ℕ

Canonical tree size of the next-configuration formula for one atom.

The zero wire bases are only representatives: the surface theorem size_nextFormula_eq_directStepFormulaSize proves that every choice of absolute configuration and choice wires has this size.

Equations

• Complexity.CircuitUnrolling.directStepFormulaSize tm T atom = (Complexity.CircuitUnrolling.nextFormula tm T 0 0 atom).size

noncomputable def Complexity.CircuitUnrolling.directStepSize {k : ℕ} (tm : NTM k) (T : ℕ) : ℕ

Exact gate count of one packed transition layer, expressed without incoming wire bases. The first summand compiles every next-configuration formula; the configuration-width summand copies their outputs into the packed successor block.

Equations

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

noncomputable def Complexity.TM.directPrefixTraceBuild {k : ℕ} (tm : TM k) (T n i : ℕ) [NeZero n] : CircuitUnrolling.TraceBuild

Canonical deterministic trace prefix used by the direct-unrolling family. All semantically irrelevant nondeterministic-choice wires reuse primary wire zero.

Equations

• tm.directPrefixTraceBuild T n i = Complexity.CircuitUnrolling.prefixTraceBuild tm.toNTM T n n i (Complexity.CircuitUnrolling.deterministicInputWires T n)

noncomputable def Complexity.TM.directStepFragment {k : ℕ} (tm : TM k) (T n : ℕ) (i : Fin T) : CircuitCode.RawCircuit

The deterministic transition fragment at canonical layer i, with all absolute bases replaced by their closed forms.

Equations

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