Fixed transition-schedule size polynomials -- proof internals

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.readSchedulePolynomial_eval_internal (T : ℕ) : Polynomial.eval T readSchedulePolynomial = caseReadSize T

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.caseSchedulePolynomial_eval_internal (workCount T : ℕ) (choiceValue : Bool) : Polynomial.eval T (caseSchedulePolynomial workCount choiceValue) = caseFormulaScheduleSize workCount T choiceValue

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.effectCasePolynomial_eval_internal (workCount T : ℕ) (selected choiceValue : Bool) : Polynomial.eval T (effectCasePolynomial workCount selected choiceValue) = effectFormulaCaseSize workCount T selected choiceValue

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.effectSchedulePolynomial_eval_internal (caseCount workCount T : ℕ) (selectedAt choiceAt : ℕ → Bool) : Polynomial.eval T (effectSchedulePolynomial caseCount workCount selectedAt choiceAt) = effectFormulaScheduleSize caseCount workCount T selectedAt choiceAt

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.predecessorHeadSchedulePolynomial_eval_internal (T : ℕ) : Polynomial.eval T predecessorHeadSchedulePolynomial = movedHeadPredecessorSize T

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.movedHeadMemberPolynomial_eval_internal (caseCount workCount T : ℕ) (selectedAt choiceAt : ℕ → Bool) : Polynomial.eval T (movedHeadMemberPolynomial caseCount workCount selectedAt choiceAt) = effectFormulaScheduleSize caseCount workCount T selectedAt choiceAt + movedHeadPredecessorSize T + 1

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.movedHeadSchedulePolynomial_eval_internal (caseCount workCount T : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : Polynomial.eval T (movedHeadSchedulePolynomial caseCount workCount selectedAt choiceAt) = movedHeadFormulaScheduleSize caseCount workCount T selectedAt choiceAt

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.writtenCellSchedulePolynomial_eval_internal (caseCount workCount T : ℕ) (selectedAt choiceAt : ℕ → Bool) : Polynomial.eval T (writtenCellSchedulePolynomial caseCount workCount selectedAt choiceAt) = writtenCellScheduleSize caseCount workCount T selectedAt choiceAt

@[simp]

theorem Complexity.CircuitUnrolling.Serializer.nextSchedulePolynomial_eval_internal (caseCount workCount T atomKind : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : Polynomial.eval T (nextSchedulePolynomial caseCount workCount atomKind selectedAt choiceAt) = nextFormulaScheduleSize caseCount workCount T atomKind selectedAt choiceAt