Numeric schedules for streaming tableau serialization

This module exposes exact, machine-oriented schedules for the two variable-length suffixes used by formula compilation. Both schedules are driven by natural counters and a numeric size oracle: no formula tree or raw circuit appears in their run-time state.

For a right-associated conjunction or disjunction, connector rank zero visits the final source member and references the identity gate; later ranks move backward through source members and reference the preceding connector. For a compiled batch, copy indices move forward and reconstruct each delayed formula output from a prefix-size sum.

These are proof-level schedule identities, not yet a Turing-machine serializer. They isolate the exact arithmetic that the later finite controller must realize.

Main results

• rightFoldConnectors_eq_indexed identifies the existing recursive connector list with the upward-counting numeric schedule.
• compileRaw_conjs_eq_indexed and compileRaw_disjs_eq_indexed expose exact finite-fold compilation in the numeric order.
• compileRawOutputs_copies_eq_indexed identifies delayed batch copies.
• compileRawBatch_eq_indexed exposes formula compilation followed by that numeric copy schedule.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_zero (sizeAt : ℕ → ℕ) : prefixSize sizeAt 0 = 0

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_succ (sizeAt : ℕ → ℕ) (count : ℕ) : prefixSize sizeAt (count + 1) = prefixSize sizeAt count + sizeAt count

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_eq_sum_range (sizeAt : ℕ → ℕ) (count : ℕ) : prefixSize sizeAt count = (List.map sizeAt (List.range count)).sum

Prefix-size accumulation is an ordinary sum over an increasing counter.

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_eq_sum_ofFn (sizeAt : ℕ → ℕ) (count : ℕ) : prefixSize sizeAt count = (List.ofFn fun (index : Fin count) => sizeAt ↑index).sum

A numeric schedule prefix is the sum over its canonical finite index.

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_mono (sizeAt : ℕ → ℕ) {first second : ℕ} (hbound : first ≤ second) : prefixSize sizeAt first ≤ prefixSize sizeAt second

Extending a numeric schedule can only increase its accumulated size.

theorem Complexity.CircuitUnrolling.Serializer.reverseMember_lt {count rank : ℕ} (hrank : rank < count) : reverseMember count rank < count

An in-range reverse rank selects an in-range source member.

theorem Complexity.CircuitUnrolling.Serializer.reverseMember_add_rank {count rank : ℕ} (hrank : rank < count) : reverseMember count rank + rank + 1 = count

A reverse member and its upward rank partition the source count.

theorem Complexity.CircuitUnrolling.Serializer.prefixSize_formulaSizes (formulas : List BoolFormula) : prefixSize (fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0) formulas.length = (List.map BoolFormula.size formulas).sum

The total of the formula-size oracle is the sum of all formula sizes.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_indexedRightFoldConnectors (op : AndOrOp) (available count : ℕ) (sizeAt : ℕ → ℕ) : List.length (indexedRightFoldConnectors op available count sizeAt) = count

theorem Complexity.CircuitUnrolling.Serializer.getElem_indexedRightFoldConnectors (op : AndOrOp) (available count : ℕ) (sizeAt : ℕ → ℕ) (rank : Fin count) : (indexedRightFoldConnectors op available count sizeAt)[↑rank] = indexedRightFoldConnector op available count sizeAt ↑rank

Rank lookup in the numeric right-fold connector schedule.

theorem Complexity.CircuitUnrolling.Serializer.rightFoldConnectors_eq_indexed (op : AndOrOp) (available : ℕ) (formulas : List BoolFormula) : BoolFormula.rightFoldConnectors op available formulas = indexedRightFoldConnectors op available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

Literal equality between recursive formula connectors and their natural-index schedule. Formula syntax appears only here as the proof adapter supplying sizes.

theorem Complexity.CircuitUnrolling.Serializer.compileRawRightFold_eq_indexed (op : AndOrOp) (identity : Bool) (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRawRightFold op identity available formulas = (BoolFormula.compileRawOutputs available formulas).circuit ++ [CircuitCode.RawGate.constant 0 identity] ++ indexedRightFoldConnectors op available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

A finite Boolean fold is forward member compilation, one identity gate, and the natural-index reverse connector schedule.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_conjs_eq_indexed (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRaw available (BoolFormula.conjs formulas) = (BoolFormula.compileRawOutputs available formulas).circuit ++ [CircuitCode.RawGate.constant 0 true] ++ indexedRightFoldConnectors AndOrOp.and available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

Exact conjunction compilation using the natural-index connector schedule.

theorem Complexity.CircuitUnrolling.Serializer.compileRaw_disjs_eq_indexed (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRaw available (BoolFormula.disjs formulas) = (BoolFormula.compileRawOutputs available formulas).circuit ++ [CircuitCode.RawGate.constant 0 false] ++ indexedRightFoldConnectors AndOrOp.or available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

Exact disjunction compilation using the natural-index connector schedule.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.length_indexedBatchCopies (available count : ℕ) (sizeAt : ℕ → ℕ) : List.length (indexedBatchCopies available count sizeAt) = count

theorem Complexity.CircuitUnrolling.Serializer.getElem_indexedBatchCopies (available count : ℕ) (sizeAt : ℕ → ℕ) (index : Fin count) : (indexedBatchCopies available count sizeAt)[↑index] = indexedBatchCopy available sizeAt ↑index

Index lookup in the forward delayed-copy schedule.

theorem Complexity.CircuitUnrolling.Serializer.compileRawOutputs_copies_eq_indexed (available : ℕ) (formulas : List BoolFormula) : List.map (fun (input : ℕ) => CircuitCode.RawGate.copy input) (BoolFormula.compileRawOutputs available formulas).outputs = indexedBatchCopies available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

The batch compiler's recorded output wires become exactly the numeric forward copy schedule after applying RawGate.copy.

theorem Complexity.CircuitUnrolling.Serializer.compileRawBatch_eq_indexed (available : ℕ) (formulas : List BoolFormula) : BoolFormula.compileRawBatch available formulas = (BoolFormula.compileRawOutputs available formulas).circuit ++ indexedBatchCopies available formulas.length fun (index : ℕ) => (List.map BoolFormula.size formulas)[index]?.getD 0

Batch compilation is all formula fragments followed by the numeric delayed copy schedule in source-formula order.