Numeric transition-formula schedules

This definitions layer flattens the two position-indexed formulas used most often by transition serialization. Every run-time parameter is a natural number: state and tape counts, layout bases, tape/symbol indices, positions, and a three-valued movement code. No formula tree, configuration atom, or bounded index occurs in the schedule state.

A read member always occupies three gates: copies of its head and cell wires, then their conjunction. A predecessor-head member occupies one gate: either a head-wire copy or false. Both streams finish with the existing numeric right-fold disjunction suffix.

def Complexity.CircuitUnrolling.Serializer.fixedWidthSizeAt (count width index : ℕ) : ℕ

Constant fixed-width size oracle on the first count indices.

Equations

• Complexity.CircuitUnrolling.Serializer.fixedWidthSizeAt count width index = if index < count then width else 0

def Complexity.CircuitUnrolling.Serializer.transitionHeadRef (stateCount T configBase tapeIndex position : ℕ) : ℕ

Absolute head-wire reference reconstructed from numeric layout data.

Equations

• Complexity.CircuitUnrolling.Serializer.transitionHeadRef stateCount T configBase tapeIndex position = configBase + (stateCount + tapeIndex * (T + 1) + position)

def Complexity.CircuitUnrolling.Serializer.transitionCellRef (stateCount tapeCount T configBase tapeIndex position symbolIndex : ℕ) : ℕ

Absolute cell-wire reference reconstructed from numeric layout data.

Equations

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

def Complexity.CircuitUnrolling.Serializer.readFormulaMemberBlock (stateCount tapeCount T configBase available tapeIndex symbolIndex position : ℕ) : CircuitCode.RawCircuit

Three-gate fragment for one candidate head position in a read formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.readFormulaMemberGates (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) : CircuitCode.RawCircuit

Forward, position-indexed member stream of a read formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.readFormulaSchedule (stateCount tapeCount T configBase available tapeIndex symbolIndex : ℕ) : CircuitCode.RawCircuit

Complete raw schedule for a read formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadPositionCode (position directionCode : ℕ) : ℕ

Move a natural head position according to a numeric direction code: 0 = left, 1 = right, and every other code means stay.

Equations

• Complexity.CircuitUnrolling.Serializer.movedHeadPositionCode position directionCode = if directionCode = 0 then position - 1 else if directionCode = 1 then position + 1 else position

def Complexity.CircuitUnrolling.Serializer.predecessorHeadMemberGate (stateCount T configBase tapeIndex target directionCode source : ℕ) : CircuitCode.RawGate

One gate for a candidate predecessor head position.

Equations

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

def Complexity.CircuitUnrolling.Serializer.predecessorHeadMemberGates (stateCount T configBase tapeIndex target directionCode : ℕ) : CircuitCode.RawCircuit

Forward, source-indexed member stream of a predecessor-head formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.predecessorHeadFormulaSchedule (stateCount T configBase available tapeIndex target directionCode : ℕ) : CircuitCode.RawCircuit

Complete raw schedule for a predecessor-head formula.

Equations

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