Project-declaredLean 4.31.0
E le dist over 3
ProximityToRS.e_le_dist_over_3
Plain-language statement
Lemma 4.4, [AHIV22] (mutual-exclusion corollary). Either all points on the affine line are e-close to the ReedāSolomon code, or at most āRSāā points are. The assumptions v ā 0 and āRSāā < |F| are necessary for mutual exclusion: if v = 0, the affine line degenerates to a singleton and the two branches can hold simultaneously.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.