Direct predecessor-head formula generation -- definitions

The member phase exploits the three fixed movement cases instead of testing source/target equality at every position. Constant runs surround at most two head-wire copies. The right-fold suffix uses a dynamic recent-wire offset 2 + 2 * rank, which directly selects reverse member outputs while the fixed offset one selects the preceding identity or connector.

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

Clean scratch contract for predecessor-head formula emission. The target position itself is deliberately not scratch and is preserved.

• loop₀ : values Work.loop₀ = 0
• limit₀ : values Work.limit₀ = 0
• loop₁ : values Work.loop₁ = 0
• reference₀ : values Work.reference₀ = 0
• reference₁ : values Work.reference₁ = 0
• emitCounter : values Work.emitCounter = 0
• copyCounter : values Work.copyCounter = 0
• multiplyCounter : values Work.multiplyCounter = 0
• addCounter : values Work.addCounter = 0
• temporary₀ : values Work.temporary₀ = 0
• temporary₃ : values Work.temporary₃ = 0

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.setPredecessorHorizonLimit : BinaryRoutine WorkCount

Replace limit₀ by horizon + 1.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorFalseRange : BinaryRoutine WorkCount

Emit false constants while loop₀ < limit₀, then restore loop₀.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitStayPredecessorMembers (stateCount : ℕ) : BinaryRoutine WorkCount

Stay-direction member stream: false prefix, target head copy, false suffix.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightZeroPredecessorMembers : BinaryRoutine WorkCount

Right movement at target zero has no predecessor.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPositivePredecessorMembers (stateCount : ℕ) : BinaryRoutine WorkCount

Right movement at a positive target has source target - 1.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitRightPredecessorMembers (stateCount : ℕ) : BinaryRoutine WorkCount

Complete right-direction member stream, branching only at target zero.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftZeroPredecessorMembers (stateCount : ℕ) : BinaryRoutine WorkCount

Left movement at target zero has the two boundary predecessors zero and one, followed by a false suffix.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.preparePredecessorHorizonGap : BinaryRoutine WorkCount

Compute horizon - position in temporary₃, restoring loop₀.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorTail (stateCount : ℕ) : BinaryRoutine WorkCount

Finish a positive-target left member stream from the prepared horizon gap. A zero gap means the preceding false prefix already filled the stream.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPositivePredecessorMembers (stateCount : ℕ) : BinaryRoutine WorkCount

Positive-target left movement emits target + 1 false members and then uses the horizon gap to decide whether a source target + 1 exists.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitLeftPredecessorMembers (stateCount : ℕ) : BinaryRoutine WorkCount

Complete left-direction member stream, branching only at target zero.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadMembers (stateCount directionCode : ℕ) : BinaryRoutine WorkCount

Forward predecessor members for one fixed direction code. Codes zero and one are left and right; every other code follows the schedule's stay case.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadConnector : BinaryRoutine WorkCount

Emit one reverse-rank OR connector, then advance its dynamic member offset by two for the next rank.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPredecessorHeadFormula (stateCount directionCode : ℕ) : BinaryRoutine WorkCount

Emit the complete predecessor-head member stream, false identity, and right-fold connector suffix, restoring every owned scratch tape.

Equations

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