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 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic
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.

View proof record