Verified direct-unrolling initialization generator

This module exposes soundness, logarithmic all-prefix space, exact pure effects, exact raw-gate emission, and the positive-input entry contract for the direct initialization phase.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate_sound (value : Bool) : (emitConstantGate value).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate_sound (reference : Fin WorkCount) (negated : Bool) : (emitCopyGate reference negated).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitConstantGate_spaceBoundByWidth (value : Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength Work.reference₀ ≤ width inputLength) : (emitConstantGate value).SpaceBoundByWidthAt initialSpace values width

Emitting a constant gate has a pointwise width certificate when the first-unused-wire frontier and the shared constant reference fit the width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCopyGate_spaceBoundByWidth (reference : Fin WorkCount) (negated : Bool) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (havailable : ∀ (inputLength : ℕ), values inputLength Work.available ≤ width inputLength) (hreference : ∀ (inputLength : ℕ), values inputLength reference ≤ width inputLength) : (emitCopyGate reference negated).SpaceBoundByWidthAt initialSpace values width

Emitting a copy gate has a pointwise width certificate when the first-unused-wire frontier and copied reference fit the width.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStartCell_sound : emitStartCell.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankCell_sound : emitBlankCell.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputDataCell_sound : emitInputDataCell.Sound

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setHorizonLimit_sound : setHorizonLimit.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setInputLimit_sound : setInputLimit.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadPosition_sound : emitHeadPosition.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadTape_sound : emitHeadTape.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitInputCells_sound : emitInputCells.Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitBlankTape_sound : emitBlankTape.Sound

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_space_bigO_log {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (initialization tm).SpaceBoundInLogAt TM.binaryLengthSpace fun (inputLength : ℕ) => preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength inputLength)

Direct initialization uses logarithmic all-prefix space after the positive polynomial preamble has prepared its numeric work-vector entry state.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_effect {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) (hinput : values Work.inputLength ≤ values Work.horizon + 1) : (initialization tm).effect values = Function.update (Function.update values Work.available (values Work.available + Fintype.card tm.Q + (values Work.horizon + 1) * (k + 2) + 4 + 4 * (values Work.horizon + 1) + (4 + 4 * (values Work.horizon + 1)) * (k + 1))) Work.limit₀ 0

Exact work-vector effect of initialization on its natural value-level domain. In particular, loop₀ is restored and limit₀ is cleared.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_emitted {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) (hloop : values Work.loop₀ = 0) (hinput : values Work.inputLength ≤ values Work.horizon + 1) : (initialization tm).emitted values = List.flatMap CircuitCode.RawGate.encode (directInitSchedule tm (values Work.horizon) (values Work.inputLength))

Exact encoded raw-gate stream emitted by initialization.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_effect_preambleValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : have values := preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n); have T := Polynomial.eval n (TM.directSerializerHorizonPolynomial q); (initialization tm).effect values = Function.update (Function.update values Work.available (n + Fintype.card tm.Q + (T + 1) * (k + 2) + 4 + 4 * (T + 1) + (4 + 4 * (T + 1)) * (k + 1))) Work.limit₀ 0

Exact endpoint after the verified positive preamble.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_emitted_preambleValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (initialization tm).emitted (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n)) = List.flatMap CircuitCode.RawGate.encode (directInitSchedule tm (Polynomial.eval n (TM.directSerializerHorizonPolynomial q)) n)

The positive preamble causes initialization to emit exactly the numeric direct-initialization schedule at the normalized horizon.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_loop_restored_preambleValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (initialization tm).effect (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n)) Work.loop₀ = 0

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.initialization_limit_restored_preambleValues {k : ℕ} (tm : TM k) (q : Polynomial ℕ) (n : ℕ) : (initialization tm).effect (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n)) Work.limit₀ = 0

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

The normalized horizon bound discharges every initialization leaf and loop obligation at positive-input entry.