A Provably Sound Closed-Form Error Bound for Reed-Solomon Proximity Testing via Hamming Association Schemes, Delsarte's Duality, and Krawtchouk Polynomials in Lean 4 and Comparator.
security cryptography information-theory polynomials coding-theory comparator fiat-shamir interactive-theorem-proving mathlib zero-knowledge-proofs reed-solomon-codes hyperspherical lean4 hamming-space krawtchouk interactive-oracle-proofs delsarte-linear-programming-duality hamming-association-scheme johnson-radius random-folding-operators
-
Updated
Sep 23, 2026 - Lean