Numeric schedules for streaming tableau serialization

This definitions layer isolates two variable-length pieces of raw formula compilation as schedules driven only by natural-number counters and a numeric size oracle. A future Turing-machine serializer can recompute that oracle from its fixed formula templates; it never needs to store a BoolFormula, a raw circuit, or a run-time syntax stack.

The right-fold schedule counts connector ranks upward while visiting source members in reverse order. The batch-copy schedule counts source formulas forward and reconstructs each delayed output reference from a prefix-size sum.

def Complexity.CircuitUnrolling.Serializer.prefixSize (sizeAt : ℕ → ℕ) : ℕ → ℕ

Sum the first count values of a numeric size oracle.

Equations

• Complexity.CircuitUnrolling.Serializer.prefixSize sizeAt 0 = 0
• Complexity.CircuitUnrolling.Serializer.prefixSize sizeAt count.succ = Complexity.CircuitUnrolling.Serializer.prefixSize sizeAt count + sizeAt count

def Complexity.CircuitUnrolling.Serializer.reverseMember (count rank : ℕ) : ℕ

Source-member index visited at an upward-counting reverse rank.

Equations

• Complexity.CircuitUnrolling.Serializer.reverseMember count rank = count - rank - 1

def Complexity.CircuitUnrolling.Serializer.indexedRightFoldConnector (op : AndOrOp) (available count : ℕ) (sizeAt : ℕ → ℕ) (rank : ℕ) : CircuitCode.RawGate

Connector emitted at rank in a stack-free right-fold suffix.

For an in-range rank, member = count - rank - 1. The first input is the member formula's output, while the second is the identity gate at rank zero or the preceding connector thereafter.

Equations

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

def Complexity.CircuitUnrolling.Serializer.indexedRightFoldConnectors (op : AndOrOp) (available count : ℕ) (sizeAt : ℕ → ℕ) : CircuitCode.RawCircuit

Reverse connector suffix, indexed by an increasing natural rank.

Equations

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

def Complexity.CircuitUnrolling.Serializer.indexedBatchCopy (available : ℕ) (sizeAt : ℕ → ℕ) (index : ℕ) : CircuitCode.RawGate

Delayed packed-output copy for the formula at a forward source index.

Equations

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

def Complexity.CircuitUnrolling.Serializer.indexedBatchCopies (available count : ℕ) (sizeAt : ℕ → ℕ) : CircuitCode.RawCircuit

Delayed batch-copy suffix, indexed in forward source-formula order.

Equations

• Complexity.CircuitUnrolling.Serializer.indexedBatchCopies available count sizeAt = List.map (Complexity.CircuitUnrolling.Serializer.indexedBatchCopy available sizeAt) (List.range count)