Project-declaredLean 4.31.0
Folded rate eq
ProximityGap.folded_rate_eq
Plain-language statement
The rate of the folded RS-code is the same.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Source-pinned research
Research proof index
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 4 research declarations. Search 10,000 more complete Mathlib declarations.
4 results
Clear filtersView proof record
Project-declaredLean 4.31.0
Folding preserves distance
ProximityGap.folding_preserves_distance
Plain-language statement
Folding preserves distance from Reed–Solomon codes. For any word f over the smooth coset FFT domain, degree parameter d, folding parameter k, and distance threshold δ satisfying 0 < δ < min (δᵣ(f, RS[d])) (1 - sqrtRate(d)), the probability over a uniformly random folding challenge r : F that the folded word is within relative distance δ of t...
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Fold Word k 1 of sq roots
ProximityGap.foldWord_k_1_of_sq_roots
Plain-language statement
An explicit formula for foldWord when k = 1 that does not use Lagrange interpolation and avoids using log.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Fold Word mem code of mem code
ProximityGap.foldWord_mem_code_of_mem_code
Plain-language statement
Perfect completeness of folding: if a word belongs to an RS-code then its foldWord belongs to a folded RS-code.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.