Verified direct-tableau generator

This module exposes the complete append-only generator for the regularly padded direct-unrolling family. Its concrete binary routine is sound, emits exactly the family's tagged circuit code (including the separate zero-length member), and has a verified logarithmic all-prefix auxiliary-space bound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTransitionSteps_sound {k : ℕ} (tm : TM k) : (emitTransitionSteps tm).Sound

Emitting all transition layers and restoring the outer counter is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTransitionSteps_requires {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hloop : values Work.loop₂ = 0) (hhorizon : 0 < values Work.horizon) : (emitTransitionSteps tm).requires values

A clean positive-horizon entry with a clear layer counter satisfies the complete transition loop's domain.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.tableauTransitionSteps_sound {k : ℕ} (tm : TM k) : (tableauTransitionSteps tm).Sound

The compact transition-layer wrapper is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.tableauFinalization_sound {k : ℕ} (tm : TM k) : (tableauFinalization tm).Sound

The compact finalization wrapper is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTransitionSteps_emitted {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) (n : ℕ) (hloop : values Work.loop₂ = 0) (hconfigBase : values Work.configBase = n) (havailable : values Work.available = n + configWidth tm.toNTM (values Work.horizon)) : (emitTransitionSteps tm).emitted values = List.flatMap CircuitCode.RawGate.encode (List.flatMap (tm.directStepFragment (values Work.horizon) n) (List.finRange (values Work.horizon)))

From the canonical initial configuration base and frontier, the complete transition loop emits exactly the canonical flattened step stream.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveTableauBody_sound {k : ℕ} (tm : TM k) : (positiveTableauBody tm).Sound

The complete positive tableau body is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveTableauBody_requires {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) (hn : 0 < n) : (positiveTableauBody tm).requires (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n))

Every positive canonical input-length vector satisfies the tableau body's compact entry contract after the polynomial/header preamble.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveTableauBody_emitted {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) [NeZero n] (hn : 0 < n) : (positiveTableauBody tm).emitted (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n)) = List.flatMap CircuitCode.RawGate.encode (tm.paddedDirectUnrollingRawCircuit (fun (x : ℕ) => Polynomial.eval x (TM.directSerializerHorizonPolynomial q)) n)

On a positive input length, the tableau body emits exactly the encoded raw gate stream of the padded direct-unrolling member.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingProgram_sound {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (paddedDirectUnrollingProgram tm q).Sound

The complete zero/positive padded-tableau generator is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingProgram_requires_inputLengthValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (paddedDirectUnrollingProgram tm q).requires (BinaryRoutine.inputLengthValues Work.inputLength n)

The complete program's compact domain holds on every canonical input-length vector, including length zero.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingProgram_emitted {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (paddedDirectUnrollingProgram tm q).emitted (BinaryRoutine.inputLengthValues Work.inputLength n) = tm.paddedDirectUnrollingCode (fun (x : ℕ) => Polynomial.eval x (TM.directSerializerHorizonPolynomial q)) n

The complete generator emits exactly the regularly padded direct family code at every input length.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingGenerator_computesInSpace {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (BinaryRoutine.afterInputLength Work.inputLength (paddedDirectUnrollingProgram tm q)).ComputesInSpace (fun (input : List Bool) => tm.paddedDirectUnrollingCode (fun (x : ℕ) => Polynomial.eval x (TM.directSerializerHorizonPolynomial q)) input.length) (BinaryRoutine.afterInputLengthSpace Work.inputLength (paddedDirectUnrollingProgram tm q))

Counting the fresh input length and running the verified serializer gives a total transducer for the once-normalized padded code map, with the exact compositional all-prefix space bound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingGenerator_space_bigO_log {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : BigO (BinaryRoutine.afterInputLengthSpace Work.inputLength (paddedDirectUnrollingProgram tm q)) fun (n : ℕ) => Nat.log 2 n

The complete fresh-input serializer uses logarithmic auxiliary space. Its output may have polynomial length, but the one-way output tape is never charged as reusable workspace.