Direct-unrolling read-formula generator -- definitions

This layer implements the horizon-dependent tape-read formula without a run-time syntax tree or stack. A forward loop emits the three-gate member for each possible head position. A false identity gate then seeds a stack-free right fold: reference₀ rolls backward through member outputs while the current wire frontier supplies the preceding connector.

Only the first loop pair, the position counter, both references, and temporaries zero through two are owned as scratch. In particular, temporary₃ remains available to an enclosing transition generator.

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

Clean entry state for the scratch tapes owned by read-formula emission. Arithmetic and emission counters are included because the underlying framed subroutines require them to be zero.

• position : values Work.position = 0

  The member-position counter starts at zero.

• loop₀ : values Work.loop₀ = 0

  The connector-rank counter starts at zero.

• limit₀ : values Work.limit₀ = 0

  The shared dynamic-loop limit starts at zero.

• reference₀ : values Work.reference₀ = 0

  The first prepared-reference tape starts at zero.

• reference₁ : values Work.reference₁ = 0

  The second prepared-reference tape starts at zero.

• emitCounter : values Work.emitCounter = 0

  The raw-gate emission counter is reusable.

• copyCounter : values Work.copyCounter = 0

  The framed-copy counter is reusable.

• multiplyCounter : values Work.multiplyCounter = 0

  The framed-multiplication counter is reusable.

• addCounter : values Work.addCounter = 0

  The framed-addition counter is reusable.

• temporary₀ : values Work.temporary₀ = 0

  The first arithmetic temporary starts at zero.

• temporary₁ : values Work.temporary₁ = 0

  The second arithmetic temporary starts at zero.

• temporary₂ : values Work.temporary₂ = 0

  The third arithmetic temporary starts at zero.

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

Emit the three-gate read member at the current position.

Equations

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

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

Replace limit₀ by the current horizon plus one.

Equations

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

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

Emit every read member while counting position from zero through the horizon.

Equations

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

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

Emit the false identity gate used to seed the disjunction fold.

Equations

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

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

Emit one connector from the member output held in reference₀ and the immediately preceding identity or connector gate. reference₀ is retained for the next reverse-rank iteration.

Equations

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

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

Move the rolling member reference back by one three-gate block and emit the next connector.

Equations

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

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

Emit one complete numeric read-formula schedule and restore all owned scratch tapes. The sole lasting effect under ReadFormulaClean is advancing available.

Equations

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