Numeric schedules for moved-head formulas -- definitions

A moved-head formula is a three-member disjunction, one member for each head direction. Each member consists of an effect-formula schedule, a numeric predecessor-head schedule, and one conjunction gate. The complete stream then adds the false identity and three reverse disjunction connectors.

The schedule state is entirely natural-number and Boolean data. Machine cases, tape slots, directions, bounded indices, formula trees, and list cursors occur only in the compile-time extractor or the proof adapter.

def Complexity.CircuitUnrolling.Serializer.movedHeadDirectionCount : ℕ

Number of fixed movement directions in left/right/stay order.

Equations

• Complexity.CircuitUnrolling.Serializer.movedHeadDirectionCount = 3

noncomputable def Complexity.CircuitUnrolling.Serializer.movedHeadCaseSelectedAt {k : ℕ} (tm : NTM k) (tape : TapeSlot k) : ℕ → ℕ → Bool

Compile-time case-selection oracle, indexed by a numeric direction code and then by a numeric transition-case index.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.Serializer.movedHeadCaseSelectedAt tm tape x✝ = fun (x : ℕ) => false

def Complexity.CircuitUnrolling.Serializer.movedHeadPredecessorSize (T : ℕ) : ℕ

Gate count of every predecessor-head child.

Equations

• Complexity.CircuitUnrolling.Serializer.movedHeadPredecessorSize T = 2 * (T + 1) + 1

def Complexity.CircuitUnrolling.Serializer.movedHeadEffectSizeAt (caseCount workCount T : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (directionCode : ℕ) : ℕ

Gate count of the effect child for one numeric direction.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadMemberSizeAt (caseCount workCount T : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (directionCode : ℕ) : ℕ

Total size oracle for the three conjunction members.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadMemberAvailable (caseCount workCount T available : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (directionCode : ℕ) : ℕ

First gate position of one direction member.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadPredecessorAvailable (caseCount workCount T available : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (directionCode : ℕ) : ℕ

First gate position of one direction's predecessor-head child.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadConjunctionGate (caseCount workCount T available : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (directionCode : ℕ) : CircuitCode.RawGate

Final conjunction gate of one direction member.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadMemberBlock (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) (directionCode : ℕ) : CircuitCode.RawCircuit

Numeric raw fragment for one left/right/stay conjunction member.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadMemberGates (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Forward stream of the three direction-member blocks.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadFormulaSchedule (caseCount stateCount workCount T configBase choiceWire available tapeIndex target : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) (stateIndexAt inputSymbolIndexAt outputSymbolIndexAt : ℕ → ℕ) (workSymbolIndexAt : ℕ → ℕ → ℕ) : CircuitCode.RawCircuit

Complete numeric raw schedule for a moved-head formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.movedHeadFormulaScheduleSize (caseCount workCount T : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : ℕ

Exact gate count of the complete moved-head schedule.

Equations

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