Complete direct-unrolling generator -- proof internals

This file first verifies the outer transition-layer loop. Its pure trajectory keeps the step scratch convention reusable, preserves the horizon, and advances the dedicated layer counter exactly once per emitted packed step.

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepLoopIndexPolynomial {k : ℕ} (tm : NTM k) : Polynomial ℕ

Polynomial space envelope for indexing one tableau-step iteration.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepLoopEvaluatorPolynomial {k : ℕ} (tm : NTM k) : Polynomial ℕ

Polynomial space envelope for evaluating one tableau-step iteration.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepLoopEndPolynomial {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : Polynomial ℕ

Polynomial endpoint bound after the tableau-step loop.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepLoopWidthPolynomial {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : Polynomial ℕ

Polynomial work-width envelope for the complete tableau-step loop.

Equations

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

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

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.tableauTransitionSteps_spaceBoundByPolynomial_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) {initialSpace : ℕ → ℕ} : (tableauTransitionSteps tm).SpaceBoundByWidthAt initialSpace (fun (n : ℕ) => (initialization tm).effect (preambleValues tm q (BinaryRoutine.inputLengthValues Work.inputLength n))) fun (x : ℕ) => Polynomial.eval x (stepLoopWidthPolynomial tm q)

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

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

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTransitionSteps_effect_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) : (emitTransitionSteps tm).effect values = Function.update ((emitStep tm).binaryForValues Work.loop₂ values (values Work.horizon - values Work.loop₂)) Work.loop₂ 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTransitionSteps_emitted_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hloop : values Work.loop₂ = 0) : (emitTransitionSteps tm).emitted values = (emitStep tm).binaryForEmitted Work.loop₂ values (values Work.horizon)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTransitionSteps_endpoint_internal {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)) : have final := (emitTransitionSteps tm).effect values; StepClean final ∧ final Work.horizon = values Work.horizon ∧ final Work.loop₂ = 0 ∧ final Work.frontier = values Work.frontier ∧ final Work.configBase = n + values Work.horizon * directStepSize tm.toNTM (values Work.horizon) ∧ final Work.available = n + configWidth tm.toNTM (values Work.horizon) + values Work.horizon * directStepSize tm.toNTM (values Work.horizon)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitTransitionSteps_emitted_exact_internal {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)))

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

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

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.positiveTableauBody_emitted_internal {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)

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingProgram_space_bigO_log_internal {k : ℕ} (tm : TM k) (q : Polynomial ℕ) : (paddedDirectUnrollingProgram tm q).SpaceBoundInLogAt TM.binaryLengthSpace (BinaryRoutine.inputLengthValues Work.inputLength)

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

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingProgram_emitted_internal {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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.paddedDirectUnrollingGenerator_computesInSpace_internal {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))