The Boolean-kernel basis: FRI folding that acts directly on tables of values, a multilinear commitment scheme built on it, and machine-checked proofs.
Over smooth multiplicative domains the classical FRI fold acts on monomial coefficients, so a prover that holds a multilinear polynomial as a table of values must convert it first. In kernel coordinates the conversion disappears: one normalised fold is exactly one sumcheck restriction.
even/odd split of U = Σb λ(b) Kb, one FRI step
fix the first variable of the table at r, one sumcheck step
Coefficients of pfoldr(Σ λ(b)Kb), degree < 4
Coefficients of Σ resr(λ)(b′)Kb′, degree < 4
Computed live in your browser over 𝔽17. The identity holds for every field of odd characteristic and every r: Theorem 5.3 in the paper, fold_dictionary in Lean.
Every result specific to the paper is proved in the paper. The only external results used are the correlated-agreement theorem for Reed–Solomon codes and the BCS theorem for interactive oracle reductions.
The kernel polynomials form a basis of 𝔽[X]<2n. The change of basis to monomials is a Kronecker power of a 2×2 matrix and costs (n/2)·2n additions.
A normalised FRI fold is the restriction of one variable. Folding the committed codeword ℓ times evaluates the multilinear extension at the challenges.
Low degree in kernel coordinates is a sign condition on the table; univariate evaluation is a scaled multilinear evaluation.
A BaseFold-style commitment in the kernel encoding. Sound and evaluation binding in the unique-decoding regime, with error εfold + 2ℓ/|𝔽| + (1−δ)κ.
With an explicit decoding extractor, and a witness bound to the commitment through the fibre distance.
The relaxed round-by-round notion of Chiesa, Di, Hu and Zheng, including partial strings produced by their extractor. Their theorem then gives straightline extraction in the quantum random oracle model, with explicit bounds.
The committed word, the sumcheck table and the folds are the same restricted table at each level. Each round halves the domain, the codeword and the table with one shared challenge.
The mathematics of Sections 2–7 is formalised against Mathlib and rebuilt from scratch on every commit by continuous integration.
| Part of the paper | Proof | Lean | Main declarations |
|---|---|---|---|
| Multilinear toolkit, smooth domains, Reed–Solomon codes (§2) | proved | formalised | mle_res, RS_unique_decoding |
| IOPs, round-by-round soundness, sumcheck (§3) | proved | formalised | rbr_knowledge_overall, sumcheck_sound_iop |
| Kernel basis, low degree, evaluation (§4) | proved | formalised | ofCoordsLin_bijective, lowDegree_iff |
| Fold dictionary, word folds (§5) | proved | formalised | fold_dictionary, codeword_fold |
| Completeness (§6) | proved | formalised | completeness |
| Soundness, binding, round-by-round knowledge (§7.1–7.6) | proved | formalised · uses axiom | soundness_far, eval_binding, rbr_knowledge |
| Relaxed RBR knowledge with erasures (§7.7) | proved | formalised · uses axiom | rrbr_round, rrbr_final, cr_unique_core |
| BCS for IORs in the QROM (Theorem 3.16) | quoted, specialised | not formalised | external: CDHZ, ePrint 2025/2166 |
The one axiom is bciks_unique: correlated agreement for Reed–Solomon codes in the unique-decoding regime (Ben-Sasson, Carmon, Ishai, Kopparty, Saraf, Theorem 4.1). Completeness, the basis theorem and the fold dictionary do not use it.
Remark 7.28, computed in exact rational arithmetic by cargo run --example pq_params.
| Parameter | Value | Role |
|---|---|---|
| Adversary queries Q | 2^64 | quantum queries to the random oracle |
| Rate ρ, proximity δ | 1/4, 3/8 | unique-decoding radius (1−ρ)/2 |
| Queries κ | 248 | (5/8)^248 = 2^−168.16 |
| Challenge field | 𝔽_p[ι]/(ι⁴−7) | Goldilocks quartic extension, |𝔽| > 2^255.99 |
| Hash output λH | 256 | salted Merkle commitments |
| Extraction error | < 2^−31.8 | dominated by 320·Q²·εrr |
The dictionary is a structural fact about folding, not a single scheme. These are the directions it opens.
Scope. The analysis covers one opening per proof in the unique-decoding regime. The post-quantum corollary applies to the compiler of CDHZ (Construction 11.7); the current Rust code is research code that does not yet implement that compiler. No speed advantage over BaseFold or DeepFold is claimed.
@misc{Mkhida2026KBFold,
author = {Abdelali Mkhida},
title = {Post-Quantum Multilinear Polynomial Commitments from {FRI} Folding
in the {Boolean}-Kernel Basis},
year = {2026},
note = {Paper, Lean 4 formalisation and Rust implementation},
howpublished = {\url{https://github.com/qoosmo/kbfold}}
}