Direct-unrolling transition-case generator

Exact contracts for the forward stream of a fixed transition case, together with soundness of the complete case-formula emitter.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_sound (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) : (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).Sound

Complete fixed transition-case emission is sound.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_spaceBoundByWidth (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), CaseFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hinputSymbol : inputSymbolIndex < 4) (houtputSymbol : outputSymbolIndex < 4) (hworkSymbols : ∀ index < workCount, workSymbolIndexAt index < 4) (hcap : ∀ (inputLength tapeIndex symbolIndex position : ℕ), tapeIndex ≤ workCount + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon → values inputLength Work.available + caseFormulaScheduleSize workCount (values inputLength Work.horizon) choiceValue + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef stateCount (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef stateCount (workCount + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (workCount + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + values inputLength Work.horizon ≤ width inputLength) : (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).SpaceBoundByWidthAt initialSpace values width

Complete fixed-case emission has an all-prefix width certificate under one bounded-selector arithmetic envelope. The symbol-selector hypotheses are the semantic ranges of transition-table data; the cap simultaneously covers the wire frontier, absolute references, and the read-size arithmetic scratch.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_requires (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).requires values

A clean case-formula entry state satisfies every framed arithmetic, reference, and gate-emission precondition of the complete emitter.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_effect (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).effect values = Function.update values Work.available (values Work.available + caseFormulaScheduleSize workCount (values Work.horizon) choiceValue)

Complete case emission restores every owned scratch register and advances the wire frontier by exactly the canonical case-schedule size.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseFormula_emitted (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitCaseFormula stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).emitted values = List.flatMap CircuitCode.RawGate.encode (caseFormulaSchedule stateCount workCount (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt)

Complete case emission is byte-for-byte the canonical numeric transition case schedule, not merely a circuit with the same gate count.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers_requires (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitCaseMembers stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).requires values

The clean-entry contract suffices for the forward member stream.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers_effect (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitCaseMembers stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).effect values = Function.update (Function.update (Function.update values Work.tapeIndex (workCount + 1)) Work.symbolIndex outputSymbolIndex) Work.available (values Work.available + caseFormulaMembersSize workCount (values Work.horizon) choiceValue)

The forward member stream restores its owned reference scratch and only retains the final tape and symbol selectors while advancing the wire frontier.

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitCaseMembers_emitted (stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex : ℕ) (choiceValue : Bool) (workSymbolIndexAt : ℕ → ℕ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) : (emitCaseMembers stateCount workCount stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt).emitted values = List.flatMap CircuitCode.RawGate.encode (caseFormulaMemberGates stateCount workCount (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) stateIndex inputSymbolIndex outputSymbolIndex choiceValue workSymbolIndexAt)

The forward member stream is exactly the canonical numeric member schedule in choice, state, input, work-tape, and output order.