Fixed transition-schedule size polynomials -- definitions

Once a machine, atom kind, and finite transition selection table are fixed, every nested transition-formula size is affine in the tableau horizon. These polynomials let the executable serializer recover dynamic recent-wire offsets with the verified binary polynomial evaluator instead of replaying a formula tree or counting emitted gates.

noncomputable def Complexity.CircuitUnrolling.Serializer.readSchedulePolynomial : Polynomial ℕ

Gate count of one read-formula schedule as a polynomial in the horizon.

Equations

• Complexity.CircuitUnrolling.Serializer.readSchedulePolynomial = Polynomial.C 4 * (Polynomial.X + Polynomial.C 1) + Polynomial.C 1

noncomputable def Complexity.CircuitUnrolling.Serializer.caseSchedulePolynomial (workCount : ℕ) (choiceValue : Bool) : Polynomial ℕ

Gate count of one fixed transition-case schedule.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectCasePolynomial (workCount : ℕ) (selected choiceValue : Bool) : Polynomial ℕ

Gate count of one selected or unselected effect member.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.effectSchedulePolynomial (caseCount workCount : ℕ) (selectedAt choiceAt : ℕ → Bool) : Polynomial ℕ

Gate count of one fixed effect-formula schedule.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.predecessorHeadSchedulePolynomial : Polynomial ℕ

Gate count of one predecessor-head schedule.

Equations

• Complexity.CircuitUnrolling.Serializer.predecessorHeadSchedulePolynomial = Polynomial.C 2 * (Polynomial.X + Polynomial.C 1) + Polynomial.C 1

noncomputable def Complexity.CircuitUnrolling.Serializer.movedHeadMemberPolynomial (caseCount workCount : ℕ) (selectedAt choiceAt : ℕ → Bool) : Polynomial ℕ

Gate count of one fixed moved-head direction member.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.movedHeadSchedulePolynomial (caseCount workCount : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : Polynomial ℕ

Gate count of a complete three-direction moved-head schedule.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.writtenCellSchedulePolynomial (caseCount workCount : ℕ) (selectedAt choiceAt : ℕ → Bool) : Polynomial ℕ

Gate count of a complete positive writable-cell schedule.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.CircuitUnrolling.Serializer.nextSchedulePolynomial (caseCount workCount atomKind : ℕ) (selectedAt : ℕ → ℕ → Bool) (choiceAt : ℕ → Bool) : Polynomial ℕ

Gate count of a complete next-atom schedule for fixed numeric atom and selection data.

Equations

• One or more equations did not get rendered due to their size.