Direct-unrolling written-cell generator -- proof internals

This dependency-independent layer verifies the bounded numeric head test used on both sides of a written-cell formula. The enclosing effect-formula proof is intentionally deferred until that generator's public contracts are available.

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.WrittenCellFormulaClean.headAtCurrentCellClean_internal {values : BinaryValues WorkCount} (hclean : WrittenCellFormulaClean values) : HeadAtCurrentCellClean values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCellGate_sound_internal (stateCount : ℕ) : (emitHeadAtCurrentCellGate stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCellGate_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hadd : values Work.addCounter = 0) (hmultiply : values Work.multiplyCounter = 0) (hemit : values Work.emitCounter = 0) : (emitHeadAtCurrentCellGate stateCount).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCellGate_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (htemporary : values Work.temporary₀ = 0) (hreference : values Work.reference₀ = 0) : (emitHeadAtCurrentCellGate stateCount).effect values = Function.update values Work.available (values Work.available + 1)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCellGate_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hreference : values Work.reference₀ = 0) : (emitHeadAtCurrentCellGate stateCount).emitted values = (if values Work.temporary₃ = 0 then CircuitCode.RawGate.constant 0 false else CircuitCode.RawGate.copy (transitionHeadRef stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position))).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCell_sound_internal (stateCount : ℕ) : (emitHeadAtCurrentCell stateCount).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCell_requires_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : HeadAtCurrentCellClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitHeadAtCurrentCell stateCount).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCell_effect_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : HeadAtCurrentCellClean values) : (emitHeadAtCurrentCell stateCount).effect values = Function.update values Work.available (values Work.available + 1)

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitHeadAtCurrentCell_emitted_internal (stateCount : ℕ) (values : BinaryValues WorkCount) (hclean : HeadAtCurrentCellClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitHeadAtCurrentCell stateCount).emitted values = (headAtCellFormulaGate stateCount (values Work.horizon) (values Work.configBase) (values Work.tapeIndex) (values Work.position)).encode

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellEffect_sound_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) : (emitWrittenCellEffect tm tape symbol).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_sound_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) : (emitWrittenCellFormula tm tape symbol).Sound

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellEffect_requires_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitWrittenCellEffect tm tape symbol).requires values

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellEffect_effect_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitWrittenCellEffect tm tape symbol).effect values = Function.update values Work.available (values Work.available + writtenCellEffectSize (transitionCases tm).length k (values Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm))

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellEffect_emitted_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : CaseFormulaClean values) (havailable : 1 ≤ values Work.available) : (emitWrittenCellEffect tm tape symbol).emitted values = List.flatMap CircuitCode.RawGate.encode (effectFormulaSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_requires_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitWrittenCellFormula tm tape symbol).requires values

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_effect_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) : (emitWrittenCellFormula tm tape symbol).effect values = Function.update values Work.available (values Work.available + writtenCellScheduleSize (transitionCases tm).length k (values Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm))

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_emitted_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) (values : BinaryValues WorkCount) (hclean : WrittenCellFormulaClean values) (hposition : values Work.position ≤ values Work.horizon + 1) : (emitWrittenCellFormula tm tape symbol).emitted values = List.flatMap CircuitCode.RawGate.encode (writtenCellSchedule (transitionCases tm).length (Fintype.card tm.Q) k (values Work.horizon) (values Work.configBase) (values Work.reference₀) (values Work.available) (↑tape.toTapeSlot.index) (values Work.position) (↑(symbolIndex symbol)) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) (effectCaseStateIndexAt tm) (effectCaseInputSymbolIndexAt tm) (effectCaseOutputSymbolIndexAt tm) (effectCaseWorkSymbolIndexAt tm))

Pointwise all-prefix width certificates

theorem Complexity.CircuitUnrolling.Serializer.DirectGenerator.emitWrittenCellFormula_spaceBoundByWidth_internal {k : ℕ} (tm : NTM k) (tape : WritableSlot k) (symbol : Γ) {initialSpace : ℕ → ℕ} {values : ℕ → BinaryValues WorkCount} {width : ℕ → ℕ} (hclean : ∀ (inputLength : ℕ), WrittenCellFormulaClean (values inputLength)) (hvalues : ∀ (inputLength : ℕ) (index : Fin WorkCount), values inputLength index ≤ width inputLength) (hposition : ∀ (inputLength : ℕ), values inputLength Work.position ≤ values inputLength Work.horizon + 1) (hcap : ∀ (inputLength stateIndex tapeIndex symbolIndex position : ℕ), stateIndex < Fintype.card tm.Q → tapeIndex ≤ k + 1 → symbolIndex < 4 → position ≤ values inputLength Work.horizon + 1 → values inputLength Work.available + writtenCellScheduleSize (transitionCases tm).length k (values inputLength Work.horizon) (writtenCellEffectSelectedAt tm tape symbol) (effectCaseChoiceAt tm) + transitionStateRef (values inputLength Work.configBase) stateIndex + (transitionHeadRef (Fintype.card tm.Q) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position + tapeIndex + values inputLength Work.horizon + 1) + (transitionCellRef (Fintype.card tm.Q) (k + 2) (values inputLength Work.horizon) (values inputLength Work.configBase) tapeIndex position symbolIndex + (tapeIndex * (values inputLength Work.horizon + 2) + position) + (values inputLength Work.horizon + 2) + (k + 2) + tapeIndex + 4) + caseReadSize (values inputLength Work.horizon) + values inputLength Work.horizon ≤ width inputLength) : (emitWrittenCellFormula tm tape symbol).SpaceBoundByWidthAt initialSpace values width