Exact effects of the direct packed-step generator

This file records the pure register effects of the formula and delayed-copy phases. The statements deliberately retain the exact numeric schedule sizes: they do not assume that the saved formula cursor or either gate register is initially zero.

structure Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepPhaseCleanInternal (values : BinaryValues WorkCount) : Prop

Scratch invariant retained while an outer step position limit is active.

• movedHeadClean : MovedHeadFormulaClean values
• position : values Work.position = 0

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepClean.phaseClean_forSpace_internal {values : BinaryValues WorkCount} (hclean : StepClean values) : StepPhaseCleanInternal values

Restrict the full step-clean invariant to the scratch invariant used by the step-space proof while an outer position limit is active.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepClean.caseFormulaClean_forSpace_internal {values : BinaryValues WorkCount} (hclean : StepClean values) : CaseFormulaClean values

Recover case-formula scratch cleanliness from a fully clean step entry for the internal step-space proof.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepPhaseCleanInternal.caseFormulaClean_forSpace_internal {values : BinaryValues WorkCount} (hclean : StepPhaseCleanInternal values) : CaseFormulaClean values

Recover case-formula scratch cleanliness while an outer step position limit is active.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepClean.updateOuter_forEffect_internal (values : BinaryValues WorkCount) (hclean : StepClean values) (idx : Fin WorkCount) (value : ℕ) (hidx : idx = Work.gateBound ∨ idx = Work.configBase ∨ idx = Work.gateCount ∨ idx = Work.loop₂) : StepClean (Function.update values idx value)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepPhaseCleanInternal.movedHeadClean_atPosition_forSpace_internal {values : BinaryValues WorkCount} (hclean : StepPhaseCleanInternal values) (position : ℕ) : MovedHeadFormulaClean (Function.update values Work.position position)

Recover moved-head scratch cleanliness at a position selected by an outer step loop.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.update_available_preserves_stepClean_internal {values : BinaryValues WorkCount} (hclean : StepClean values) (value : ℕ) : StepClean (Function.update values Work.available value)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.update_available_preserves_phaseClean_forSpace_internal {values : BinaryValues WorkCount} (hclean : StepPhaseCleanInternal values) (value : ℕ) : StepPhaseCleanInternal (Function.update values Work.available value)

Advancing the formula frontier preserves the scratch invariant used by the step-space proof.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.update_limit₁_preserves_phaseClean_internal {values : BinaryValues WorkCount} (hclean : StepPhaseCleanInternal values) (value : ℕ) : StepPhaseCleanInternal (Function.update values Work.limit₁ value)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateFormulas_effect_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (hclean : StepClean values) : (emitStepStateFormulas tm).effect values = Function.update values Work.available (values Work.available + (List.ofFn fun (stateIndex : Fin (Fintype.card tm.Q)) => have state := (Fintype.equivFin tm.Q).symm stateIndex; nextStateFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = state)) (effectCaseChoiceAt tm)).sum)

Exact state-formula phase effect.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellPosition_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) : (emitStepImmutableCellPosition tm tape).effect values = Function.update values Work.available (values Work.available + 4)

The four immutable-cell formulas restore scratch and add four gates.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellPosition_effect_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) : (emitStepWritableCellPosition tm tape).effect values = Function.update values Work.available (values Work.available + (List.ofFn fun (symbolIndex : Fin 4) => have symbol := symbolEquiv.symm symbolIndex; if values Work.position = 0 then 1 else nextWrittenCellFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm)).sum)

Exact four-symbol writable-cell phase effect at the current position.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headFormula_binaryForValues_effect_forSpace_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : StepPhaseCleanInternal values) (hhorizon : 0 < values Work.horizon) (count : ℕ) (hcount : count ≤ values Work.horizon + 1) : (emitNextHeadFormula tm tape).binaryForValues Work.position values count = Function.update (Function.update values Work.position count) Work.available (values Work.available + count * nextHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm))

Exact trajectory of a prefix of one tape's head-formula loop, exposed only for the internal step-space proof.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeFormulas_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : StepPhaseCleanInternal values) (hhorizon : 0 < values Work.horizon) (hlimit : values Work.limit₁ = values Work.horizon + 1) : (emitStepHeadTapeFormulas tm tape).effect values = Function.update values Work.available (values Work.available + (values Work.horizon + 1) * nextHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm))

Exact effect of the complete head-position loop for one tape.

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepCellPositionEffectSizeInternal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (T position : ℕ) : ℕ

Exact formula-gate count for one tape at one numeric cell position.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepCellPositionEffectSizeInternal tm Complexity.CircuitUnrolling.TapeSlot.input T position = 4

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.cellFormula_binaryForValues_effect_forSpace_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : StepPhaseCleanInternal values) (count : ℕ) : (match tape with | TapeSlot.input => emitStepImmutableCellPosition tm TapeSlot.input | TapeSlot.work index => emitStepWritableCellPosition tm (WritableSlot.work index) | TapeSlot.output => emitStepWritableCellPosition tm WritableSlot.output).binaryForValues Work.position values count = Function.update (Function.update values Work.position count) Work.available (values Work.available + prefixSize (stepCellPositionEffectSizeInternal tm tape (values Work.horizon)) count)

Exact trajectory of a prefix of one tape's cell-formula loop, exposed only for the internal step-space proof.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeFormulas_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : StepPhaseCleanInternal values) (hlimit : values Work.limit₁ = values Work.horizon + 2) : (emitStepCellTapeFormulas tm tape).effect values = Function.update values Work.available (values Work.available + prefixSize (stepCellPositionEffectSizeInternal tm tape (values Work.horizon)) (values Work.horizon + 2))

Exact effect of all cell-position formulas for one named tape.

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

Exact total size of the state-formula prefix.

Equations

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

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

Exact total size of all head-formula blocks.

Equations

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

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

Exact total size of all cell-formula blocks.

Equations

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

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

Exact complete forward formula-stream gate count.

Equations

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.seqList_headTapeFormulas_effect_forSpace_internal {k : ℕ} (tm : NTM k) (tapes : List (TapeSlot k)) (values : BinaryValues WorkCount) (hclean : StepPhaseCleanInternal values) (hhorizon : 0 < values Work.horizon) (hlimit : values Work.limit₁ = values Work.horizon + 1) : (BinaryRoutine.seqList (List.map (emitStepHeadTapeFormulas tm) tapes)).effect values = Function.update values Work.available (values Work.available + (List.map (fun (tape : TapeSlot k) => (values Work.horizon + 1) * nextHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm)) tapes).sum)

Exact endpoint of a finite head-tape formula prefix, exposed to the step-space proof without duplicating its phase-invariant induction.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.seqList_cellTapeFormulas_effect_forSpace_internal {k : ℕ} (tm : NTM k) (tapes : List (TapeSlot k)) (values : BinaryValues WorkCount) (hclean : StepPhaseCleanInternal values) (hlimit : values Work.limit₁ = values Work.horizon + 2) : (BinaryRoutine.seqList (List.map (emitStepCellTapeFormulas tm) tapes)).effect values = Function.update values Work.available (values Work.available + (List.map (fun (tape : TapeSlot k) => prefixSize (stepCellPositionEffectSizeInternal tm tape (values Work.horizon)) (values Work.horizon + 2)) tapes).sum)

Exact endpoint of a finite cell-tape formula prefix, exposed to the step-space proof without duplicating its phase-invariant induction.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.setStepPositionLimit_effect_local_internal (extra : ℕ) (values : BinaryValues WorkCount) : (setStepPositionLimit extra).effect values = Function.update values Work.limit₁ (values Work.horizon + extra)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepFormulas_effect_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) : (emitStepFormulas tm).effect values = Function.update values Work.available (values Work.available + stepFormulasEffectSizeInternal tm (values Work.horizon))

The complete forward formula phase restores its outer counters and advances exactly by the explicit formula schedule size.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateCopies_effect_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) : (emitStepStateCopies tm).effect values = Function.update (Function.update (Function.update (Function.update values Work.gateCount (values Work.gateCount + stepStateFormulasEffectSizeInternal tm (values Work.horizon))) Work.available (values Work.available + Fintype.card tm.Q)) Work.reference₀ 0) Work.temporary₃ 0

Exact delayed state-copy effect.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellCopies_effect_internal (values : BinaryValues WorkCount) : emitStepImmutableCellCopies.effect values = Function.update (Function.update (Function.update (Function.update values Work.gateCount (values Work.gateCount + 4)) Work.available (values Work.available + 4)) Work.reference₀ 0) Work.temporary₃ 0

Four immutable delayed copies advance the rolling cursor by four formula gates and append four packed outputs.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellCopies_effect_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (values : BinaryValues WorkCount) : (emitStepWritableCellCopies tm tape).effect values = Function.update (Function.update (Function.update (Function.update values Work.gateCount (values Work.gateCount + stepCellPositionEffectSizeInternal tm tape.toTapeSlot (values Work.horizon) (values Work.position))) Work.available (values Work.available + 4)) Work.reference₀ 0) Work.temporary₃ 0

Exact delayed writable-cell copies at the current position.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.binaryForValues_copy_succ_effect_forSpace_internal (body : BinaryRoutine WorkCount) (sizeAt : ℕ → ℕ) (outputCount : ℕ) (values : BinaryValues WorkCount) (hbody : ∀ (current : BinaryValues WorkCount), current Work.horizon = values Work.horizon → body.effect current = Function.update (Function.update (Function.update (Function.update current Work.gateCount (current Work.gateCount + sizeAt (current Work.position))) Work.available (current Work.available + outputCount)) Work.reference₀ 0) Work.temporary₃ 0) (hpositionZero : values Work.position = 0) (count : ℕ) : body.binaryForValues Work.position values (count + 1) = Function.update (Function.update (Function.update (Function.update (Function.update values Work.position (count + 1)) Work.gateCount (values Work.gateCount + prefixSize sizeAt (count + 1))) Work.available (values Work.available + outputCount * (count + 1))) Work.reference₀ 0) Work.temporary₃ 0

Exact trajectory of a nonempty packed-copy loop prefix, exposed only for the internal step-space proof.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeCopies_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hposition : values Work.position = 0) (hlimit : values Work.limit₁ = values Work.horizon + 1) : (emitStepHeadTapeCopies tm tape).effect values = Function.update (Function.update (Function.update (Function.update values Work.gateCount (values Work.gateCount + (values Work.horizon + 1) * nextHeadFormulaScheduleSize (transitionCases tm).length k (values Work.horizon) (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm))) Work.available (values Work.available + values Work.horizon + 1)) Work.reference₀ 0) Work.temporary₃ 0

Exact delayed head-copy loop effect for one tape.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeCopies_effect_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hposition : values Work.position = 0) (hlimit : values Work.limit₁ = values Work.horizon + 2) : (emitStepCellTapeCopies tm tape).effect values = Function.update (Function.update (Function.update (Function.update values Work.gateCount (values Work.gateCount + prefixSize (stepCellPositionEffectSizeInternal tm tape (values Work.horizon)) (values Work.horizon + 2))) Work.available (values Work.available + 4 * (values Work.horizon + 2))) Work.reference₀ 0) Work.temporary₃ 0

Exact delayed cell-copy effect for one named tape.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepPackedCopies_effect_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (hclean : StepClean values) : (emitStepPackedCopies tm).effect values = Function.update (Function.update (Function.update (Function.update values Work.gateCount (values Work.gateCount + stepFormulasEffectSizeInternal tm (values Work.horizon))) Work.available (values Work.available + stepAtomCount (Fintype.card tm.Q) k (values Work.horizon))) Work.reference₀ 0) Work.temporary₃ 0

The delayed-copy phase consumes exactly one output gate per configuration atom while advancing the saved formula cursor by the complete formula prefix.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_effect_explicit_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) : (emitStep tm).effect values = Function.update (Function.update (Function.update (Function.update values Work.available (values Work.available + stepFormulasEffectSizeInternal tm.toNTM (values Work.horizon) + stepAtomCount (Fintype.card tm.Q) k (values Work.horizon))) Work.configBase (values Work.available + stepFormulasEffectSizeInternal tm.toNTM (values Work.horizon))) Work.gateBound 0) Work.gateCount 0

Exact whole-step register effect, expressed using the generator's explicit formula-prefix count. The formula end is retained as the next configuration base, and both temporary gate registers are cleared.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStep_effect_stepClean_internal {k : ℕ} (tm : TM k) (values : BinaryValues WorkCount) (hclean : StepClean values) (hhorizon : 0 < values Work.horizon) : StepClean ((emitStep tm).effect values)

A complete packed step restores the reusable nested scratch convention.