Common packed-step width helpers #
This module supplies the shared list-trajectory and position-limit certificates used to assemble the auxiliary-space proof for direct packed-step generation.
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.stepScheduleSize_eq_formulas_add_atoms_internal
{k : ℕ}
(tm : NTM k)
(T : ℕ)
:
stepScheduleSize (transitionCases tm).length (Fintype.card tm.Q) k T (stepAtomKindAt tm T)
(stepAtomEffectSelectedAt tm T) (effectCaseChoiceAt tm) = stepFormulasEffectSizeInternal tm T + stepAtomCount (Fintype.card tm.Q) k T
The complete step schedule is the formula frontier followed by one packed copy for every configuration atom.
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepWidthEnvelope.formulaFrontier_le_internal
{k : ℕ}
{tm : NTM k}
{values : BinaryValues WorkCount}
{width : ℕ}
(henvelope : StepWidthEnvelope tm values width)
:
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepWidthEnvelope.finalFrontier_le_internal
{k : ℕ}
{tm : NTM k}
{values : BinaryValues WorkCount}
{width : ℕ}
(henvelope : StepWidthEnvelope tm values width)
:
values Work.available + stepFormulasEffectSizeInternal tm (values Work.horizon) + stepAtomCount (Fintype.card tm.Q) k (values Work.horizon) ≤ width
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepWidthEnvelope.horizon_add_two_le_internal
{k : ℕ}
{tm : NTM k}
{values : BinaryValues WorkCount}
{width : ℕ}
(henvelope : StepWidthEnvelope tm values width)
:
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.StepWidthEnvelope.formulaPrefix_le_internal
{k : ℕ}
{tm : NTM k}
{values : BinaryValues WorkCount}
{width count : ℕ}
(henvelope : StepWidthEnvelope tm values width)
(hcount : count ≤ stepAtomCount (Fintype.card tm.Q) k (values Work.horizon))
:
values Work.available + prefixSize (stepFormulaSizeAtSpecializedInternal tm (values Work.horizon)) count ≤ width
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.seqList_ofFn_spaceBoundByWidthAt_internal
{n : ℕ}
(count : ℕ)
(routineAt : Fin count → BinaryRoutine n)
(trajectory : ℕ → ℕ → BinaryValues n)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues n}
{width : ℕ → ℕ}
(hzero : trajectory 0 = values)
(hspace : ∀ (index : Fin count), (routineAt index).SpaceBoundByWidthAt initialSpace (trajectory ↑index) width)
(hstep :
∀ (index : Fin count) (inputLength : ℕ),
(routineAt index).effect (trajectory (↑index) inputLength) = trajectory (↑index + 1) inputLength)
:
BinaryRoutine.SeqListSpaceBoundByWidthAt (List.ofFn routineAt) initialSpace values width
A finite family of routines has a sequential width certificate when each routine is certified along an explicit trajectory and its effect advances that trajectory by one step.
theorem
Complexity.CircuitUnrolling.Serializer.DirectGenerator.setStepPositionLimit_spaceBoundByWidthAt_internal
(extra : ℕ)
{initialSpace : ℕ → ℕ}
{values : ℕ → BinaryValues WorkCount}
{width : ℕ → ℕ}
(hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength)
(hresult : ∀ (inputLength : ℕ), values inputLength Work.horizon + extra ≤ width inputLength)
:
(setStepPositionLimit extra).SpaceBoundByWidthAt initialSpace values width
Replacing the outer position limit by horizon + extra preserves a common
width bound when the input vector and the replacement value fit that width.