Canonical binary evaluation of a fixed natural polynomial

This module exposes a finite Horner program compiled from a fixed polynomial. It preserves the input, writes the polynomial value to the designated result tape in canonical binary, and restores the scratch accumulator and both counters to canonical zero. Its all-prefix space bound depends on value width, not runtime, and is logarithmic in the input value for every fixed polynomial.

Main results

• binaryHornerFold_polyCoeffs identifies the compiled Horner coefficients.
• binaryPolynomialEvalTM_hoareTime_frame gives the endpoint and time bound.
• binaryPolynomialEvalTM_hoareTimeSpace_frame bounds every execution prefix.
• binaryPolynomialSpace_bigO proves the fixed-polynomial logarithmic bound.
• binaryPolynomialEvalTM_isTransducer proves append-only-output safety.

@[simp]

theorem Complexity.TM.binaryPolynomialCoeffs_length (p : Polynomial ℕ) : (binaryPolynomialCoeffs p).length = p.natDegree + 1

A fixed polynomial contributes exactly one coefficient for each degree through its natural degree, including explicit zero coefficients.

theorem Complexity.TM.binaryPolynomialCoeffs_ne_nil (p : Polynomial ℕ) : binaryPolynomialCoeffs p ≠ []

The compiled coefficient list is never empty, including for the zero polynomial.

@[simp]

theorem Complexity.TM.binaryHornerFold_nil (x acc : ℕ) : binaryHornerFold x [] acc = acc

Horner evaluation leaves an accumulator unchanged at the empty list.

theorem Complexity.TM.binaryHornerFold_cons (x coeff acc : ℕ) (coeffs : List ℕ) : binaryHornerFold x (coeff :: coeffs) acc = binaryHornerFold x coeffs (acc * x + coeff)

One Horner step multiplies the accumulator by the input and adds the next coefficient.

theorem Complexity.TM.binaryHornerFold_polyCoeffs (p : Polynomial ℕ) (x : ℕ) : binaryHornerFold x (binaryPolynomialCoeffs p) 0 = Polynomial.eval x p

The high-degree-first coefficient list computes the polynomial's ordinary evaluation when Horner evaluation starts from zero.

theorem Complexity.TM.binaryPolynomial_eval_le_valueCap (p : Polynomial ℕ) (x : ℕ) : Polynomial.eval x p ≤ binaryPolynomialValueCap p x

Ordinary polynomial evaluation is bounded by the explicit cap used for every intermediate value of the compiled Horner routine.

theorem Complexity.TM.binaryPolynomialEvalTM_hoareTime_frame {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (hdistinct : BinaryPolynomialDistinct inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx) (p : Polynomial ℕ) (inputValue : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinput : (work₀ inputIdx).HasBinaryNat inputValue) (hresult : (work₀ resultIdx).HasBinaryNat 0) (hscratch : (work₀ scratchIdx).HasBinaryNat 0) (hmulCounter : (work₀ mulCounterIdx).HasBinaryNat 0) (haddCounter : (work₀ addCounterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ inputIdx → i ≠ resultIdx → i ≠ scratchIdx → i ≠ mulCounterIdx → i ≠ addCounterIdx → Parked (work₀ i)) (hout : Parked out₀) : (binaryPolynomialEvalTM inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx p).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ resultIdx ((Tape.init (List.map Γ.ofBool (Polynomial.eval inputValue p).bits)).move Dir3.right) ∧ out = out₀) (binaryPolynomialTime p inputValue)

Evaluating a fixed polynomial changes only the result tape. The input is preserved literally, and the scratch accumulator and both internal counters are restored to their initial canonical-zero tapes.

theorem Complexity.TM.binaryPolynomialEvalTM_hoareTimeSpace_frame {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (hdistinct : BinaryPolynomialDistinct inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx) (p : Polynomial ℕ) (inputValue inputLength initialSpace : ℕ) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinput : (work₀ inputIdx).HasBinaryNat inputValue) (hresult : (work₀ resultIdx).HasBinaryNat 0) (hscratch : (work₀ scratchIdx).HasBinaryNat 0) (hmulCounter : (work₀ mulCounterIdx).HasBinaryNat 0) (haddCounter : (work₀ addCounterIdx).HasBinaryNat 0) (hinp : Parked inp₀) (hother : ∀ (i : Fin n), i ≠ inputIdx → i ≠ resultIdx → i ≠ scratchIdx → i ≠ mulCounterIdx → i ≠ addCounterIdx → Parked (work₀ i)) (hout : Parked out₀) (hworkSpace : ∀ (i : Fin n), (work₀ i).head ≤ initialSpace) (hinputSpace : inp₀.head ≤ inputLength + initialSpace + 1) : (binaryPolynomialEvalTM inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx p).HoareTimeSpace (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = Function.update work₀ resultIdx ((Tape.init (List.map Γ.ofBool (Polynomial.eval inputValue p).bits)).move Dir3.right) ∧ out = out₀) (binaryPolynomialTime p inputValue) inputLength (binaryPolynomialSpace initialSpace p inputValue)

Every prefix of fixed-polynomial evaluation respects a common bound based on the width of a polynomial cap for all Horner intermediate values.

theorem Complexity.TM.binaryPolynomialSpace_bigO (initialSpace : ℕ) (p : Polynomial ℕ) : BigO (fun (inputValue : ℕ) => binaryPolynomialSpace initialSpace p inputValue) fun (inputValue : ℕ) => Nat.log 2 inputValue

For every fixed polynomial and initial-space allowance, the public all-prefix space bound is logarithmic in the numeric input.

@[simp]

theorem Complexity.TM.binaryPolynomialSpaceWidthPolynomial_eval (p : Polynomial ℕ) (inputValue : ℕ) : Polynomial.eval inputValue (binaryPolynomialSpaceWidthPolynomial p) = 2 * binaryPolynomialValueCap p inputValue

Evaluation of the explicit width polynomial is exactly twice the Horner-prefix value cap.

theorem Complexity.TM.binaryPolynomialEvalTM_isTransducer {n : ℕ} (inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx : Fin n) (p : Polynomial ℕ) : (binaryPolynomialEvalTM inputIdx resultIdx scratchIdx mulCounterIdx addCounterIdx p).IsTransducer

Fixed-polynomial evaluation never moves its output head left.