Verified direct predecessor-head formula generation

This module exposes the executable predecessor-head generator together with its exact entry domain, restored work-vector effect, and encoded numeric schedule. Direction codes zero and one mean left and right; all other codes mean stay, matching movedHeadPositionCode.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_sound (stateCount directionCode : ℕ) : (emitPredecessorHeadFormula stateCount directionCode).Sound

Direct predecessor-head generation is sound on its explicit clean domain.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_requires (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) : (emitPredecessorHeadFormula stateCount directionCode).requires values ↔ PredecessorHeadClean values ∧ 0 < values Work.horizon ∧ values Work.position ≤ values Work.horizon

The generator's domain is exactly clean owned scratch, a positive horizon, and an in-range target position.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_spaceBoundByWidth (stateCount directionCode : ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), PredecessorHeadClean (values inputLength)) (hhorizon : ∀ (inputLength : ℕ), 0 < values inputLength Work.horizon) (htarget : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hfrontier : ∀ (inputLength : ℕ), values inputLength Work.available + movedHeadPredecessorSize (values inputLength Work.horizon) ≤ width inputLength) (hcap : ∀ (inputLength : ℕ), transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) (values inputLength Work.tapeIndex) (values inputLength Work.horizon + 1) + values inputLength Work.tapeIndex + values inputLength Work.horizon + 1 + 2 * (values inputLength Work.horizon + 2) ≤ width inputLength) : (emitPredecessorHeadFormula stateCount directionCode).SpaceBoundByWidthAt initialSpace values width

Complete predecessor-head emission has an all-prefix pointwise width certificate on its natural clean domain. The frontier premise covers every emitted wire; the single arithmetic cap covers both absolute head references and the dynamic reverse-fold offset.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_effect (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitPredecessorHeadFormula stateCount directionCode).effect values = Function.update values Work.available (values Work.available + movedHeadPredecessorSize (values Work.horizon))

The generator restores every owned scratch register and advances the wire frontier by exactly the predecessor-head schedule size.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula_emitted (stateCount directionCode : ℕ) (values : BinaryValues WorkCount) (hclean : PredecessorHeadClean values) (hhorizon : 0 < values Work.horizon) (htarget : values Work.position ≤ values Work.horizon) : (emitPredecessorHeadFormula stateCount directionCode).emitted values = List.flatMap CircuitCode.RawGate.encode (predecessorHeadFormulaSchedule stateCount (values Work.horizon) (values Work.configBase) (values Work.available) (values Work.tapeIndex) (values Work.position) directionCode)

The emitted word is exactly the encoded numeric predecessor-head schedule at the run-time layout, target, and horizon.