Numeric schedules for written-cell formulas

A written-cell formula contains one variable-size selected-write effect and a fixed Boolean wrapper. This layer places the effect schedule after one numeric head-at-cell gate, then emits six fixed suffix gates by an increasing natural phase counter. Layout addresses, phase bases, and the effect descriptors are all natural numbers or Booleans.

The fixed machine, writable tape, and symbol are used only to derive the compile-time selection oracle. No run-time schedule value contains a formula, bounded index, transition case, tape slot, symbol, or list cursor.

noncomputable def Complexity.CircuitUnrolling.Serializer.writtenCellEffectSelectedAt {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) : ℕ → Bool

Compile-time selection oracle for cases writing symbol on tape.

Equations

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

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

Gate count of the selected-write effect nested in a written-cell formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.writtenCellLeftAndGate (available effectSize : ℕ) : CircuitCode.RawGate

Left conjunct gate combining atHead with the selected-write effect.

Equations

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

def Complexity.CircuitUnrolling.Serializer.writtenCellNegatedHeadGate (available effectSize : ℕ) : CircuitCode.RawGate

Negation gate following the second copy of atHead.

Equations

• Complexity.CircuitUnrolling.Serializer.writtenCellNegatedHeadGate available effectSize = Complexity.CircuitCode.RawGate.copy (available + effectSize + 2) true

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

Old-cell variable gate reconstructed from numeric layout indices.

Equations

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

def Complexity.CircuitUnrolling.Serializer.writtenCellRightAndGate (available effectSize : ℕ) : CircuitCode.RawGate

Right conjunct gate combining not atHead with the old cell value.

Equations

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

def Complexity.CircuitUnrolling.Serializer.writtenCellFinalOrGate (available effectSize : ℕ) : CircuitCode.RawGate

Final disjunction gate combining the write and preservation branches.

Equations

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

def Complexity.CircuitUnrolling.Serializer.writtenCellSuffixGate (stateCount tapeCount T configBase available tapeIndex position symbolIndex effectSize phase : ℕ) : CircuitCode.RawGate

One of the six fixed suffix gates, selected by a natural phase code. Codes 0, ..., 5 mean left AND, second head test, head negation, old value, right AND, and final OR respectively.

Equations

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

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

Six-gate fixed suffix driven by an increasing natural phase counter.

Equations

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

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

Complete numeric schedule for a written-cell formula.

Equations

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

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

Exact gate count of the complete numeric written-cell schedule.

Equations

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