Computable noun fingerprint

NPR.fn (Nock/NPR.lean, def:ion_univariate, main.tex:1180–1184) evaluates the noun polynomials with Mathlib's Polynomial, which is noncomputable. This module gives the extractable Horner evaluation fnHorner and proves it equals NPR.fn (fnHorner_eq_fn), so the collision-soundness bounds of Nock/NPR.lean apply to the code that actually runs. Instantiated at a concrete prime field ZMod q (with [Fact (Nat.Prime q)] supplied by the caller — never as an axiom), fnHorner compiles and evaluates.

def Nock.NPR.hornerEval {K : Type u_1} [Semiring K] (r : K) : List K → K

Horner evaluation of a coefficient list: hornerEval r [a₀,…,aₙ] = a₀ + r·(a₁ + r·(…)), i.e. Σᵢ aᵢ rⁱ. Computable (no Polynomial); the extractable core of the fingerprint.

Equations

• Nock.NPR.hornerEval r [] = 0
• Nock.NPR.hornerEval r (a :: l) = a + r * Nock.NPR.hornerEval r l

theorem Nock.NPR.hornerEval_eq_listPoly_eval {K : Type u_1} [Field K] (r : K) (l : List K) : hornerEval r l = Polynomial.eval r (listPoly l)

Horner = polynomial evaluation. hornerEval r l = (listPoly l).eval r: the computable Horner scheme agrees with evaluating the coefficient polynomial Σᵢ lᵢ Xⁱ at r.

def Nock.NPR.fnHorner {K : Type u_1} [Field K] (r : K) (n : Noun) : K × K × K

The computable fingerprint (def:ion_univariate, main.tex:1180–1184). fnHorner r n = (r^{|dt|}, Σ dtᵢ rⁱ, Σ wᵢ rⁱ) via Horner, with no Polynomial. Equal to NPR.fn (fnHorner_eq_fn), so it inherits the collision bounds.

Equations

• Nock.NPR.fnHorner r n = (r ^ n.leaves, Nock.NPR.hornerEval r (Nock.NPR.leafF n), Nock.NPR.hornerEval r (Nock.NPR.dyckBits n))

theorem Nock.NPR.fnHorner_eq_fn {K : Type u_1} [Field K] (n : Noun) (r : K) : fnHorner r n = fn n r

fnHorner computes NPR.fn. The extractable Horner fingerprint equals the polynomial fingerprint fn (main.tex:1180–1184), so lem:ion_univariate_sec / corr:ion_single_security (Nock/NPR.lean) transfer verbatim to the running code.