Fixed transition-schedule size polynomials

This module exposes literal evaluation theorems for the fixed polynomials that measure nested transition schedules as functions of the tableau horizon.

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

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

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

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

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

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

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

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

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