Regularly padded deterministic unrolling families -- definitions

The direct tableau circuit has a polynomial upper bound on its gate count, but its exact length depends on the compiled machine. Padding every positive member to that bound and adding one final output copy makes the gate-count header a closed expression of the time horizon while retaining the original acceptance wire.

noncomputable def Complexity.TM.directUnrollingGateBound {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) : ℕ

Closed gate-count bound used to regularize a direct tableau member.

Equations

• tm.directUnrollingGateBound f n = Complexity.CircuitUnrolling.acceptanceSizeCoeff tm.toNTM * (f n + 2) ^ 3

noncomputable def Complexity.TM.paddedDirectUnrollingRawCircuit {k : ℕ} (tm : TM k) (f : ℕ → ℕ) (n : ℕ) [NeZero n] : CircuitCode.RawCircuit

A positive direct-unrolling raw circuit padded to its cubic gate bound.

The padding gates are constant false and are semantically dead. The final gate copies the original last gate, so it remains the designated output after the padding is appended.

Equations

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

noncomputable def Complexity.TM.paddedDirectUnrollingCode {k : ℕ} (tm : TM k) (f : ℕ → ℕ) : ℕ → List Bool

Total tagged code of the regularly padded direct family. The zero-length member retains the explicit bounded-run answer used by the direct family.

Equations

• tm.paddedDirectUnrollingCode f 0 = [false, Complexity.CircuitUnrolling.boundedAcceptanceBit tm.toNTM (f 0) (fun (i : Fin 0) => i.elim0) fun (x : Fin (f 0)) => false]
• tm.paddedDirectUnrollingCode f n.succ = true :: (tm.paddedDirectUnrollingRawCircuit f (n + 1)).encode