Streamable deterministic unrolling families — definitions

The nonuniform unrolling family fixes the choice prefix of tm.toNTM by repeated typed-circuit hardwiring. That construction has convenient semantics, but its serialized syntax is needlessly difficult for a log-space generator to reproduce.

For a deterministic machine, the embedded NTM ignores every choice bit. At positive input lengths this module therefore reuses primary input wire zero for all choice positions and leaves the ordinary data wires in place. The resulting typed circuit is reconstructed directly from acceptanceRawCircuit, so erasing it recovers exactly that raw list.

The verified log-space generator (TM.paddedDirectUnrollingCode_mem_FL) emits TM.paddedDirectUnrollingCode, which pads this raw list to a closed gate bound. No theorem places the unpadded TM.directUnrollingCode map in FL.

def Complexity.CircuitUnrolling.deterministicInputWires (T n : ℕ) [NeZero n] : InputWires T n n

Positive-arity input layout for deterministic unrolling. Data bit i remains primary input i; every semantically irrelevant choice position reuses primary input zero.

Equations

• Complexity.CircuitUnrolling.deterministicInputWires T n = { choice := fun (x : Fin T) => ⟨0, ⋯⟩, data := fun (i : Fin n) => i }

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

The exact raw circuit underlying the streamable positive-length member.

Equations

• tm.directUnrollingRawCircuit f n = Complexity.CircuitUnrolling.acceptanceRawCircuit tm.toNTM (f n) n n (Complexity.CircuitUnrolling.deterministicInputWires (f n) n)

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

Total tagged code specification for the direct family. The zero-length case is the explicit answer bit; every positive case is the literal raw tableau encoding. The verified log-space generator emits the padded TM.paddedDirectUnrollingCode instead; this unpadded map is not known to be in FL.

Equations

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

noncomputable def Complexity.TM.directUnrollingCircuitFamily {k : ℕ} (tm : TM k) (f : ℕ → ℕ) : CircuitFamily Basis.andOr2

A deterministic unrolling family whose positive members are reconstructed directly from their raw tableau circuits. Unlike the older fixed-prefix family, its canonical serialization has no intervening hardwiring transformation.

Equations

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