Relative Unique Decoding Radius RS eq
ReedSolomon.relativeUniqueDecodingRadius_RS_eq
Plain-language statement
Relative unique decoding radius for RS code with arbitrary finite index type ι.
Source project: ArkLib
Person-level attribution pending.
Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersReedSolomon.relativeUniqueDecodingRadius_RS_eq
Plain-language statement
Relative unique decoding radius for RS code with arbitrary finite index type ι.
Source project: ArkLib
Person-level attribution pending.
ReedSolomon.toPolynomial_mem_lt_deg
Plain-language statement
The polynomials corresponding to Reed-Solomon codewords are of degree smaller than deg.
Source project: ArkLib
Person-level attribution pending.
RingSwitching.SumcheckPhase.coreInteraction_perfectCompleteness
Plain-language statement
Perfect completeness for large-field reduction (Sumcheck ++ FinalSum)
Source project: ArkLib
Person-level attribution pending.
RoundConsistency.generalised_round_consistency_completeness
Plain-language statement
Completeness of the round consistency check. Given a polynomial f, challenge γ, and n-th roots of unity ω, when f is honestly evaluated at the scaled points {ω i * s₀}, the round consistency check succeeds with the value (foldNth n f γ).eval (s₀^n). This establishes that the Lagrange interpolant through the evaluation points matches the n-wa...
Source project: ArkLib
Person-level attribution pending.
schwartz_zippel_counting
Plain-language statement
For a nonzero multivariate polynomial f of total degree at most d, evaluated over a product of finite subsets of a field F, each of cardinality at least m, the number of roots is at most d / m multiplied by the side of the product set.
Source project: ArkLib
Person-level attribution pending.
SendChallenge.oracleVerifier_toVerifier_run
Plain-language statement
The pure verifier's underlying non-oracle verifier returns the statement together with the sampled challenge (read off the transcript), with the oracle statements passed through.
Source project: ArkLib
Person-level attribution pending.