sumcheck-lean4

A Lean 4 monorepo with two formalised sub-projects: the sumcheck protocol and the BCGM25 mutual-correlated-agreement (MCA) framework for linear codes (with a runnable Reed-Solomon encoder backing it).

What you import

import SumcheckProtocol     -- the sumcheck protocol
import LinearCodes  -- LinearCode typeclass, Reed-Solomon, BCGM25 MCA framework

The two sub-trees

SumcheckProtocol/ — sumcheck protocol

Machine-checked completeness and soundness for the canonical sumcheck protocol on multivariate polynomials, built on CMvPolynomial. Prover, verifier, and transcript generation are fully computable (#eval-able end-to-end). Inner-product sumcheck specialisation with a multilinear soundness-error bound of n · 2 / |𝔽|. 0 sorry, 0 axioms, enforced by CI. See SumcheckProtocol/README.md and stability tiers at SumcheckProtocol/doc/stability.md.

LinearCodes/ — linear codes + MCA framework

A LinearCode typeclass, a runnable Reed-Solomon encoder with seven proved properties (length, additivity, scalar-multiplicativity, Singleton-MDS distance, injectivity, Johnson list-decoding radius, encoder↔Polynomial.eval bridge), and the BCGM25 MCA capstones (Theorems 6.1, 6.2, 9.2) proved end-to-end at the integer-tight BCH+25 bound. 0 sorry, 0 axioms, enforced by CI. See LinearCodes/README.md. Quick tour for new users: LinearCodes/doc/getting-started.md.

License

Apache License 2.0. See LICENSE.