Direct-unrolling transition-effect generator -- definitions

An effect formula is a fixed disjunction over the finite transition table. Selected cases use the executable case-formula routine; unselected cases emit one false gate. The suffix traverses the hardwired case table in reverse and rolls one output reference backward by each intervening case size.

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectCaseAt {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (caseIndex : ℕ) : BinaryRoutine WorkCount

Emit one numeric transition-table member, selected or replaced by false at generator-definition time.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectMembersFrom {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) (start : ℕ) : ℕ → BinaryRoutine WorkCount

Emit count consecutive forward effect members beginning at the numeric case index start.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectMembersFrom tm selects start 0 = Complexity.BinaryRoutine.identity

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectMembers {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : BinaryRoutine WorkCount

Emit every forward case member of one fixed effect formula.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.prepareEffectCaseSize (workCount : ℕ) (selected choiceValue : Bool) : BinaryRoutine WorkCount

Prepare the gate count of one effect member in temporary₃. Selected case sizes are affine in the run-time horizon; unselected members have size one.

Equations

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

def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnector (workCount : ℕ) (selected choiceValue : Bool) : BinaryRoutine WorkCount

Roll the retained case-output reference back by one complete member and emit the next disjunction connector.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnectorsCount {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : ℕ → BinaryRoutine WorkCount

Emit count predecessor connectors, crossing case members with numeric indices count, ..., 1. Index zero is omitted because no member precedes the original first case.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnectorsCount tm selects 0 = Complexity.BinaryRoutine.identity

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitPreviousEffectConnectors {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : BinaryRoutine WorkCount

Reverse connector routines in the exact numeric right-fold order. A table of m cases crosses the m - 1 predecessor boundaries.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectConnectors {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : BinaryRoutine WorkCount

Emit the connector suffix for a nonempty case table, or the routine identity for the vacuous disjunction.

Equations

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

noncomputable def Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitEffectFormula {k : ℕ} (tm : NTM k) (selects : TransitionEffect tm → Bool) : BinaryRoutine WorkCount

Emit one complete transition-effect schedule.

Equations

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