Exact output of the direct packed-step generator

This file proves that the direct generator emits the canonical numeric step schedule byte for byte. The intermediate results identify each nested enumeration with its contiguous slice of the global configuration-atom order.

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

The canonical formula-block size function specialized to one machine.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepFormulaBlockSpecializedInternal {k : ℕ} (tm : NTM k) (T configBase available atomIndex : ℕ) : CircuitCode.RawCircuit

One canonical formula block specialized to one machine and choice wire zero.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepPackedCopySpecializedInternal {k : ℕ} (tm : NTM k) (T available atomIndex : ℕ) : CircuitCode.RawGate

One canonical delayed packed-copy gate specialized to one machine.

Equations

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.indexedGateBlocks_group_internal (width count : ℕ) (blockAt : ℕ → CircuitCode.RawCircuit) : indexedGateBlocks (width * count) blockAt = indexedGateBlocks count fun (group : ℕ) => indexedGateBlocks width fun (offset : ℕ) => blockAt (width * group + offset)

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

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepFormulaSizeAtSpecialized_state_forSpace_internal {k : ℕ} (tm : NTM k) (T : ℕ) (index : Fin (Fintype.card tm.Q)) : stepFormulaSizeAtSpecializedInternal tm T ↑index = nextStateFormulaScheduleSize (transitionCases tm).length k T (effectCaseSelectedAt tm fun (effect : TransitionEffect tm) => decide (effect.nextState = (Fintype.equivFin tm.Q).symm index)) (effectCaseChoiceAt tm)

The specialized numeric size oracle agrees with the state-formula polynomial at every canonical state index.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateFormulas_emitted_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (hclean : StepClean values) : (emitStepStateFormulas tm).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (Fintype.card tm.Q) fun (atomIndex : ℕ) => stepFormulaBlockSpecializedInternal tm (values Work.horizon) (values Work.configBase) (values Work.available) atomIndex)

Exact encoded prefix for the state-atom formula subroutine.

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

First flattened configuration index for the four symbols at a tape cell.

Equations

• Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepCellStart tm T tape position = Fintype.card tm.Q + (k + 2) * (T + 1) + (↑tape.index * (T + 2) + position) * 4

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeFormulas_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hhorizon : 0 < values Work.horizon) (hposition : values Work.position = 0) (hlimit : values Work.limit₁ = values Work.horizon + 1) (stepAvailable : ℕ) (havailable : values Work.available = stepAvailable + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) (Fintype.card tm.Q + ↑tape.index * (values Work.horizon + 1))) : (emitStepHeadTapeFormulas tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (values Work.horizon + 1) fun (position : ℕ) => stepFormulaBlockSpecializedInternal tm (values Work.horizon) (values Work.configBase) stepAvailable (Fintype.card tm.Q + ↑tape.index * (values Work.horizon + 1) + position))

Exact global atom slice for one tape's head-formula loop.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellPosition_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hposition : values Work.position < values Work.horizon + 2) (hcopy : tape = TapeSlot.input ∨ values Work.position = 0) (stepAvailable : ℕ) (havailable : values Work.available = stepAvailable + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + (↑tape.index * (values Work.horizon + 2) + values Work.position) * 4)) : (emitStepImmutableCellPosition tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks 4 fun (symbolIndex : ℕ) => stepFormulaBlockSpecializedInternal tm (values Work.horizon) (values Work.configBase) stepAvailable (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + (↑tape.index * (values Work.horizon + 2) + values Work.position) * 4 + symbolIndex))

Exact four-atom slice for one immutable cell position.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellPosition_emitted_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hposition : values Work.position < values Work.horizon + 2) (stepAvailable : ℕ) (havailable : values Work.available = stepAvailable + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + (↑tape.toTapeSlot.index * (values Work.horizon + 2) + values Work.position) * 4)) : (emitStepWritableCellPosition tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks 4 fun (symbolIndex : ℕ) => stepFormulaBlockSpecializedInternal tm (values Work.horizon) (values Work.configBase) stepAvailable (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + (↑tape.toTapeSlot.index * (values Work.horizon + 2) + values Work.position) * 4 + symbolIndex))

Exact four-atom slice for one writable cell position.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepStateCopies_emitted_internal {k : ℕ} (tm : NTM k) (values : BinaryValues WorkCount) (stepAvailable : ℕ) (hgateCount : values Work.gateCount = stepAvailable) (hreference : values Work.reference₀ = 0) (htemporary : values Work.temporary₃ = 0) : (emitStepStateCopies tm).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (Fintype.card tm.Q) fun (atomIndex : ℕ) => [stepPackedCopySpecializedInternal tm (values Work.horizon) stepAvailable atomIndex])

Exact packed-copy prefix for the state atoms.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepImmutableCellCopies_emitted_internal (values : BinaryValues WorkCount) (sizeAt : ℕ → ℕ) (start stepAvailable : ℕ) (hgateCount : values Work.gateCount = stepAvailable + prefixSize sizeAt start) (hreference : values Work.reference₀ = 0) (htemporary : values Work.temporary₃ = 0) (hsize : ∀ (index : Fin 4), sizeAt (start + ↑index) = 1) : emitStepImmutableCellCopies.emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks 4 fun (index : ℕ) => [CircuitCode.RawGate.copy (stepAvailable + prefixSize sizeAt (start + index + 1) - 1)])

Four fixed one-gate delayed copies traverse four consecutive formulas.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepWritableCellCopies_emitted_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (values : BinaryValues WorkCount) (hposition : values Work.position < values Work.horizon + 2) (stepAvailable : ℕ) (hgateCount : values Work.gateCount = stepAvailable + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) (stepCellStart tm (values Work.horizon) tape.toTapeSlot (values Work.position))) (hreference : values Work.reference₀ = 0) (htemporary : values Work.temporary₃ = 0) : (emitStepWritableCellCopies tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks 4 fun (index : ℕ) => [stepPackedCopySpecializedInternal tm (values Work.horizon) stepAvailable (stepCellStart tm (values Work.horizon) tape.toTapeSlot (values Work.position) + index)])

Exact four-copy slice for one writable cell position.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeFormulas_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hclean : MovedHeadFormulaClean values) (hpositionZero : values Work.position = 0) (hlimit : values Work.limit₁ = values Work.horizon + 2) (stepAvailable : ℕ) (havailable : values Work.available = stepAvailable + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + ↑tape.index * (values Work.horizon + 2) * 4)) : (emitStepCellTapeFormulas tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (4 * (values Work.horizon + 2)) fun (offset : ℕ) => stepFormulaBlockSpecializedInternal tm (values Work.horizon) (values Work.configBase) stepAvailable (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + ↑tape.index * (values Work.horizon + 2) * 4 + offset))

Exact global atom slice for one tape's cell-formula loop.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepHeadTapeCopies_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hposition : values Work.position = 0) (hlimit : values Work.limit₁ = values Work.horizon + 1) (stepAvailable : ℕ) (hgateCount : values Work.gateCount = stepAvailable + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) (Fintype.card tm.Q + ↑tape.index * (values Work.horizon + 1))) (hreference : values Work.reference₀ = 0) (htemporary : values Work.temporary₃ = 0) : (emitStepHeadTapeCopies tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (values Work.horizon + 1) fun (position : ℕ) => [stepPackedCopySpecializedInternal tm (values Work.horizon) stepAvailable (Fintype.card tm.Q + ↑tape.index * (values Work.horizon + 1) + position)])

Exact delayed-copy slice for one tape's head atoms.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStepCellTapeCopies_emitted_internal {k : ℕ} (tm : NTM k) (tape : TapeSlot k) (values : BinaryValues WorkCount) (hposition : values Work.position = 0) (hlimit : values Work.limit₁ = values Work.horizon + 2) (stepAvailable : ℕ) (hgateCount : values Work.gateCount = stepAvailable + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + ↑tape.index * (values Work.horizon + 2) * 4)) (hreference : values Work.reference₀ = 0) (htemporary : values Work.temporary₃ = 0) : (emitStepCellTapeCopies tm tape).emitted values = List.flatMap CircuitCode.RawGate.encode (indexedGateBlocks (4 * (values Work.horizon + 2)) fun (offset : ℕ) => [stepPackedCopySpecializedInternal tm (values Work.horizon) stepAvailable (Fintype.card tm.Q + (k + 2) * (values Work.horizon + 1) + ↑tape.index * (values Work.horizon + 2) * 4 + offset)])

Exact delayed-copy slice for one tape's cell atoms.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.tapeSlotEquiv_symm_index_internal {k : ℕ} (index : Fin (k + 2)) : ↑((tapeSlotEquiv k).symm index).index = ↑index

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.headPrefixBlock_internal {k : ℕ} (tm : NTM k) (T : ℕ) (tape : TapeSlot k) : prefixSize (stepFormulaSizeAtSpecializedInternal tm T) (Fintype.card tm.Q + ↑tape.index * (T + 1) + (T + 1)) = prefixSize (stepFormulaSizeAtSpecializedInternal tm T) (Fintype.card tm.Q + ↑tape.index * (T + 1)) + (T + 1) * nextHeadFormulaScheduleSize (transitionCases tm).length k T (movedHeadCaseSelectedAt tm tape) (effectCaseChoiceAt tm)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.cellPrefixBlock_internal {k : ℕ} (tm : NTM k) (T : ℕ) (tape : TapeSlot k) : prefixSize (stepFormulaSizeAtSpecializedInternal tm T) (Fintype.card tm.Q + (k + 2) * (T + 1) + ↑tape.index * (T + 2) * 4 + 4 * (T + 2)) = prefixSize (stepFormulaSizeAtSpecializedInternal tm T) (Fintype.card tm.Q + (k + 2) * (T + 1) + ↑tape.index * (T + 2) * 4) + prefixSize (stepCellPositionEffectSizeInternal tm tape T) (T + 2)

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepStateFormulasEffectSize_eq_prefixSize_internal {k : ℕ} (tm : NTM k) (T : ℕ) : stepStateFormulasEffectSizeInternal tm T = prefixSize (stepFormulaSizeAtSpecializedInternal tm T) (Fintype.card tm.Q)

The explicit state-phase count is its canonical numeric prefix.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepFormulasEffectSize_eq_prefixSize_internal {k : ℕ} (tm : NTM k) (T : ℕ) : stepFormulasEffectSizeInternal tm T = prefixSize (stepFormulaSizeAtSpecializedInternal tm T) (stepAtomCount (Fintype.card tm.Q) k T)

The explicit effect count is the canonical numeric formula prefix.