Packed circuit fragments for one Turing-machine transition

This definitions layer compiles the canonical list of next-configuration formulas into one appendable raw-circuit fragment. The formula outputs are copied into a contiguous block in configuration-atom order, so that block can serve directly as the input configuration of a later unrolled step.

noncomputable def Complexity.CircuitUnrolling.stepFormulas {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : List BoolFormula

Next-configuration formulas in the canonical configuration-atom order.

Equations

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

noncomputable def Complexity.CircuitUnrolling.stepFragmentSize {k : ℕ} (tm : NTM k) (T configBase choiceWire : ℕ) : ℕ

Exact number of gates emitted by the packed one-step fragment.

Equations

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

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

Machine-dependent coefficient in the quadratic one-step size bound.

Equations

• Complexity.CircuitUnrolling.stepSizeCoeff tm = (Fintype.card tm.Q + 5 * (k + 2)) * (24 + 3 * (Complexity.CircuitUnrolling.transitionCases tm).length * (4 * (k + 2) + 7))

noncomputable def Complexity.CircuitUnrolling.stepOutputBase {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : ℕ

First wire of the packed successor-configuration block.

Equations

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

noncomputable def Complexity.CircuitUnrolling.stepFragment {k : ℕ} (tm : NTM k) (T configBase choiceWire available : ℕ) : CircuitCode.RawCircuit

Compile one bounded transition after an existing raw-circuit prefix.

The packed outputs follow configAtoms, independently of the variable sizes of the formulas that compute them.

Equations

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