Noun Polynomial Representation (NPR) #
The paper's succinct polynomial representation of nouns and its collision-soundness bounds
(main.tex:1162–1226). A noun n = (dt, w) (main.tex:1164) is a leaf array dt ∈ 𝔽^λ
together with a Dyck word w ∈ {0,1}^{2(λ−1)} fixing the tree shape. The leaf array is
Noun.leafList and the Dyck word Noun.dyckWord (both from Nock/Dyck.lean), cast into a
field K at this layer.
Contents:
Φ(main.tex:1170–1173) — the NPR: a noun ↦ triple of univariate polynomialsΦ(dt,w) = ( X^{|dt|}, Σ dtᵢ X^{i−1}, Σ wᵢ X^{i−1} ).fn(def:ion_univariate,main.tex:1180–1184) — the fingerprintfn(n; r) = Φ(dt,w)[r,r,r] = (r^{|dt|}, F_d(r), F_w(r)),r ∈ K.NPR_decomp(Lem:NPR_decomp,main.tex:1218–1226) — the threeconsconcatenation identities (with the corrected Φ₃ exponents; see the section header).collision_card_le/collision_prob_le(lem:ion_univariate_sec,main.tex:1188) — distinct nouns collide underfnfor at most2(2Λ−1)values ofr.collision_table_card_le/collision_table_prob_le(corr:ion_single_security,main.tex:1197) — union bound overknouns:Pr ≤ ε · k(k−1)/2.
Everything is proved over an ARBITRARY finite field K ([Field K] [Fintype K] [DecidableEq K]): no concrete field, no primality axiom. "Pr_{r∈K}[…]" is the counting
measure (satisfying r count divided by |K| = Fintype.card K); the core results are the
exact cardinality bounds (…_card_le), with …_prob_le dividing by |K| in ℚ.
Schwartz–Zippel is Polynomial.card_roots' via card_eval_zero_le.
Coefficient-vector polynomials #
cpoly f n = Σ_{i<n} f i · X^i: the polynomial with coefficient vector (f 0,…,f (n−1)).
Equations
- Nock.NPR.cpoly f n = ∑ i ∈ Finset.range n, Polynomial.C (f i) * Polynomial.X ^ i
Instances For
List-indexed polynomials #
The polynomial whose coefficient vector is the list l (default 0 past the end).
Equations
- Nock.NPR.listPoly l = Nock.NPR.cpoly (fun (i : ℕ) => l.getD i 0) l.length
Instances For
Concatenation identities for listPoly (the algebraic backbone of Lem:NPR_decomp). #
These express how a list-indexed polynomial factors when its coefficient list is split.
They are what turn the DFS/Dyck concatenation of nouns under `cell` into the polynomial
identities of `Lem:NPR_decomp` (main.tex:1218).
The NPR and the fingerprint #
The Noun Polynomial Representation (main.tex:1170–1173).
Φ(dt,w) = ( X₁^{|dt|}, Σ dtᵢ X₂^{i−1}, Σ wᵢ X₃^{i−1} ) — represented as a triple of
univariate polynomials (each in its own indeterminate X).
Equations
Instances For
The fingerprint (def:ion_univariate, main.tex:1180–1184).
fn(n; r) = Φ(dt,w)[r,r,r] = (r^{|dt|}, F_d(r), F_w(r)), evaluated at r ∈ K.
Equations
- Nock.NPR.fn n r = (r ^ n.leaves, Polynomial.eval r (Nock.NPR.listPoly (Nock.NPR.leafF n)), Polynomial.eval r (Nock.NPR.listPoly (Nock.NPR.dyckBits n)))
Instances For
The fingerprint is Φ evaluated at (r,r,r) (main.tex:1183).
Lem:NPR_decomp — the memory-table backbone (main.tex:1218) #
How the three NPR polynomials concatenate under `cons`. We first record the two
structural concatenation lemmas (leaf array in DFS order; Dyck word by the grammar
`w = 0·w_L·1·w_R`), then read off the three `Φ`-identities.
⚠ **FAITHFULNESS — the Φ₃ (Dyck) exponents (main.tex:1223).** The paper prints
`Φ(n)₃ = Φ(nL)₃ + X^{2(λL−1)} + X^{2λL−1}·Φ(nR)₃`.
Derived carefully against `Dyck.encode`'s grammar `w = 0·w_L·1·w_R` and the paper's own
`F_w(X) = Σ_i w_i X^{i−1}` (`listPoly`), the CORRECT identity is
`Φ(n)₃ = X·Φ(nL)₃ + X^{2λL−1} + X^{2λL}·Φ(nR)₃`.
The paper's form is off by one global factor of `X` (equivalently: it drops the leading
open-delimiter bit's `X`-shift), i.e. paper-RHS `= X⁻¹·(correct RHS)`. Concretely, for
`n = cons(atom,atom)` the Dyck word is `[0,1]`, so `F_w(n) = X`, which the correct
identity yields (`X·0 + X^{2·1−1} + X^{2·1}·0 = X`) but the paper's yields `1`
(`0 + X^{2(1−1)} + X^{2·1−1}·0`). We prove and use the correct identity `Phi3_cons`
and flag this deviation.
Lem:NPR_decomp, Φ₃ (main.tex:1223), CORRECTED exponents (see the section header):
Φ(cons(l,r))₃ = X·Φ(l)₃ + X^{2λL−1} + X^{2λL}·Φ(r)₃.
Lem:NPR_decomp (main.tex:1218). The three algebraic identities characterizing
cons. We state the paper's ↔ n = cons(nL,nR) as Φ n = Φ (cons nL nR) — field-noun
equality: Φ n = Φ n' is equality of the pair (leaf-count, leaf polynomial, Dyck polynomial),
i.e. of the (dyck word, 𝔽-valued leaf array), which is the paper's notion of noun equality
over 𝔽 (the paper's nouns are field-valued, main.tex:347–349, 1023). (Structural
n = cell nL nR implies it via congrArg, NPR_decomp_of_cons; the converse to structural
Nat equality does NOT hold — distinct Nat leaves congruent mod the characteristic give the
same field-noun (compiled counterexample RedTeam.Batch5.b5_npr_decomp_field_not_structural
over ZMod 5), the "same field-noun"
phenomenon also underlying collision_card_le. This module does not prove Φ injective on
field-nouns; that is the paper's ion property, whose soundness error is bounded by
collision_prob_le.)
Fingerprint-level cons composition (the constraint form) #
`Lem:NPR_decomp` characterizes `cons` at the polynomial level. A zkVM AIR never carries
the polynomials — a trace row carries only the *evaluated* fingerprints `fn(·; x) ∈ K³` —
so a cons gadget states the same identities as field arithmetic on fingerprint components.
These are the evaluations of `Phi1_cons`/`Phi2_cons`/`Phi3_cons` at `x`, plus an
inverse-free multiplied-through form of the Dyck identity (`fn_cons_dyck_constraint`).
That form is a **completeness** identity for honest `fn` values (no `x⁻¹` in the
statement). It is **not** a proved soundness theorem for committed columns, and at
`x = 0` it degenerates to `0 = 0` (every noun has ≥1 leaf, so `fn₁(l;0) = 0`), constraining
nothing — useful as an AIR-style equation only for nonzero challenges.
⚠ **Orientation.** This layer's `fn` / `fnHorner` evaluate with the FIRST leaf/Dyck
symbol at the constant coefficient (`listPoly`). A different Horner convention that
places the first symbol at the highest power would need mirrored cons identities; those
mirrored equations are **not** theorems in this file. `fnHorner_eq_fn` ties the running
code to the non-mirrored orientation proved here.
fn₃ (Dyck fingerprint) composes under cons with the delimiter power made explicit
(evaluation of the corrected Phi3_cons):
fn₃(cons(l,r)) = x·fn₃(l) + x^{2λL−1} + x^{2λL}·fn₃(r).
Fingerprint cons composition (fn_cons) — fn(cons(l,r); x) as field arithmetic
over the children's fingerprints, with the Dyck delimiter power explicit.
Inverse-free (AIR-constraint) form of the Dyck composition. Multiplying
fn_cons_dyck through by x replaces the loose power with fingerprint components —
x·x^{2λL−1} = x^{2λL} = fn₁(l)² — so every term is a product of components and x:
`x·fn₃(cons(l,r)) = x²·fn₃(l) + fn₁(l)² + x·fn₁(l)²·fn₃(r)`.
Completeness identity for honest fingerprints (no x⁻¹ in the statement). Not a
soundness theorem for committed columns; at x = 0 both sides are 0, so the equation
constrains nothing there.
Schwartz–Zippel / root counting #
A nonzero polynomial of natDegree d vanishes at at most d points of K.
The collision-soundness bound (lem:ion_univariate_sec, main.tex:1188) #
ε_col^{Λ,𝔽} — the single-instance collision-soundness error (main.tex:1204).
The paper names the collision error ε^{Λ,𝔽}_col := ε(Λ,K) (main.tex:1204) where
ε(Λ,K) = 2·(2Λ−1)/|K| is the bound of Lem:ion_univariate_sec (main.tex:1192).
We name it here as a standalone constant. (2·Λ−1 uses ℕ truncated subtraction; over
the operative range Λ ≥ 1 — always forced by Noun.one_le_leaves in every use below —
it agrees with the paper's 2(2Λ−1); see epsCol_eq for the real-arithmetic form.)
Equations
- Nock.NPR.epsCol Λ = ↑(2 * (2 * Λ - 1)) / ↑(Fintype.card K)
Instances For
lem:ion_univariate_sec (main.tex:1188), cardinality form — tight bound.
For distinct field-nouns of length ≤ Λ, the fingerprint fn collides for at most
2Λ − 1 values of r ∈ K.
"distinct field-nouns" (the paper's n₁ ≠ n₂ in 𝒩^{λ≤Λ}(𝔽), main.tex:1181) is the
hypothesis hne: the NPR data (dt, w) = (leafF, dyckBits) differ. (Operationally
distinct Nouns that agree after casting leaves into K are the same field-noun and
genuinely have equal fingerprints, so this is exactly the right premise.)
Proof = univariate Schwartz–Zippel: at least one of the three difference polynomials
X^{λ₁}−X^{λ₂}, F_{d₁}−F_{d₂}, F_{w₁}−F_{w₂} is nonzero of natDegree ≤ 2Λ−1, and a
collision forces r to be its root.
lem:ion_univariate_sec (main.tex:1188), cardinality form — paper's stated bound.
The collision set has size ≤ 2(2Λ−1) (the constant printed in the paper; the tight
bound collision_card_le_tight gives 2Λ−1).
lem:ion_univariate_sec (main.tex:1188), probability form. With the counting-measure
convention, Pr_{r∈K}[fn n₁ = fn n₂] ≤ 2(2Λ−1)/|K| = ε(Λ,K).
lem:ion_univariate_sec (main.tex:1192), probability form in terms of ε_col.
Restatement of collision_prob_le against the named constant epsCol (main.tex:1204):
Pr_{r∈K}[fn n₁ = fn n₂; n₁ ≠ n₂] ≤ ε_col^{Λ,𝔽}.
Union bound over a table of nouns (corr:ion_single_security, main.tex:1197) #
corr:ion_single_security (main.tex:1197), cardinality form. For a table of k = |s|
nouns of length ≤ Λ, the number of r ∈ K for which some pair of distinct nouns
collides is ≤ k(k−1)·(2Λ−1). (Union bound over ordered distinct index pairs, each
contributing ≤ 2Λ−1 by collision_card_le_tight.)
corr:ion_single_security (main.tex:1197), probability form — union bound. With
ε := ε_col = 2(2Λ−1)/|K|, the probability that some pair among k = |s| nouns collides
is ≤ ε · k(k−1)/2. This is the paper's second (union-bound) inequality, main.tex:1200.
⚠ The paper's FIRST (tight) inequality Pr ≤ 1 − (1−ε)^{k(k−1)/2} is NOT proven here,
and is not soundly provable in this model. The paper's proof (main.tex:2361) obtains it
by asserting "the probability of no table collisions is (1−p)^{k(k−1)/2}", i.e. by
treating the k(k−1)/2 pairwise collision events as independent. In our (and the
paper's real) probability model those events all share the SAME random r ∈ K, so they
are NOT independent, and a product/independence bound is unavailable: the only estimate the
root-counting machinery yields is the ADDITIVE union bound (card_biUnion_le), giving the
≤ ε·k(k−1)/2 below. The product form is moreover genuinely FALSE in the worst case
admitted by our per-pair root-count bounds: for m := k(k−1)/2 pairwise collision sets
that are pairwise disjoint (each of the maximal 2Λ−1 roots) and together partition K,
the collision probability is 1, which exceeds 1−(1−ε)^m < 1. Consistently, our proven
union bound ε·m is ≥ the tight 1−(1−ε)^m (Bernoulli, one_sub_one_sub_pow_le; equality
only in the degenerate ε = 0 / m ≤ 1 cases, strict for m ≥ 2, ε > 0), so the tight
expression is a stronger claim that this model cannot license. The union bound below is the
rigorous, model-faithful claim; the paper describes a "non-optimal but easier to show" bound
(main.tex:2361) which is what we prove here.
corr:ion_single_security (main.tex:1197), union bound in terms of ε_col.
Restatement of collision_table_prob_le against the named constant epsCol
(main.tex:1204): Pr[∃ colliding pair] ≤ ε_col^{Λ,𝔽} · k(k−1)/2.
Bernoulli's inequality (the paper's 1 − (1−ε)^m < ε·m step, main.tex:1200/2361).
For any ε ≤ 2 and m : ℕ, 1 − (1−ε)^m ≤ m·ε. This is the pure real inequality
relating the paper's two collision-error expressions: the tight
1 − (1−ε)^{k(k−1)/2} and the union bound ε·k(k−1)/2 (m = k(k−1)/2).
NOTE: this lemma establishes only the arithmetic relation tight ≤ union. It does
NOT (and cannot, in this shared-randomness model) establish that the collision
probability is bounded by the tight expression — see the ⚠ note on
collision_table_prob_le. It is exactly what shows the union bound we DO prove is the
weaker (larger) of the paper's two stated bounds, faithfully reproducing the paper's
< chain.