Project-declaredLean 4.31.0
Johnson d le n
JohnsonBound.johnson_d_le_n
Plain-language statement
The average pairwise distance d(B) is at most n.
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 44 research declarations. Search 10,000 more complete Mathlib declarations.
44 results
Clear filtersView proof record
Project-declaredLean 4.31.0
Johnson den lb e pos
JohnsonBound.johnson_den_lb_e_pos
Plain-language statement
Lower bound on the Johnson denominator when e > 0.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Johnson denom
JohnsonBound.johnson_denom
Plain-language statement
Algebraic identity expressing the Johnson LHS as a difference of squares.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Johnson e div ne J
JohnsonBound.johnson_e_div_ne_J
Plain-language statement
The ratio e/n cannot equal J'(q, d/n) under the Johnson hypothesis.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Johnson gap frac d gt one
JohnsonBound.johnson_gap_frac_d_gt_one
Plain-language statement
When q · d / ((q-1) · n) > 1, there is a positive gap of size ≥ 1/((q-1)·n).
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Johnson unrefined
JohnsonBound.johnson_unrefined
Plain-language statement
Unrefined Johnson bound in terms of e, d, and |B|.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.