Canonical binary evaluation of a fixed natural polynomial — proof internals

Each Horner layer is verified compositionally from multiply-add, fixed-constant addition, and clearing. The list proof alternates accumulator roles and carries a common polynomial value cap; consequently all layers fit one width-based space budget independent of their (potentially much larger) running time.

def Complexity.TM.binaryPolynomialNatTape (value : ℕ) : Tape

Canonical parked tape encoding of a natural for polynomial evaluation.

Equations

• Complexity.TM.binaryPolynomialNatTape value = (Complexity.Tape.init (List.map Complexity.Γ.ofBool value.bits)).move Complexity.Dir3.right

@[reducible, inline]

abbrev Complexity.TM.binaryPolynomialFramePred {n : ℕ} (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) : TapePred n

Predicate fixing the tapes framing a binary polynomial evaluation.

Equations

• Complexity.TM.binaryPolynomialFramePred inp₀ work₀ out₀ inp work out = (inp = inp₀ ∧ work = work₀ ∧ out = out₀)

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

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

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

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

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

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

theorem Complexity.TM.binaryPolynomialEvalTM_hoareTimeSpace_frame_internal {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 (binaryPolynomialFramePred inp₀ work₀ out₀) (binaryPolynomialFramePred inp₀ (Function.update work₀ resultIdx (binaryPolynomialNatTape (Polynomial.eval inputValue p))) out₀) (binaryPolynomialTime p inputValue) inputLength (binaryPolynomialSpace initialSpace p inputValue)

theorem Complexity.TM.binaryPolynomialEvalTM_hoareTime_frame_internal {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 (binaryPolynomialFramePred inp₀ work₀ out₀) (binaryPolynomialFramePred inp₀ (Function.update work₀ resultIdx (binaryPolynomialNatTape (Polynomial.eval inputValue p))) out₀) (binaryPolynomialTime p inputValue)

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

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

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