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

1 topic

573 results

Clear filters
Project-declaredLean 4.31.0

Dvd eval of root Multiplicity zero

GuruswamiSudan.dvd_eval_of_rootMultiplicity_zero

Plain-language statement

If Q has high multiplicity at (0,0) (meaning all coefficients c_{i,j} with i+j < m are zero) and P(0)=0, then Q(X, P(X)) is divisible by X^m.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Dvd property

GuruswamiSudan.dvd_property

Plain-language statement

If QQ satisfies the weighted degree bound and vanishes to order mm at each point (ωi,fi)(\omega_i, f_i), and if PP is a codeword close enough to ff, then YP(X)Y - P(X) divides Q(X,Y)Q(X,Y).

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Exists nonzero solution

GuruswamiSudan.exists_nonzero_solution

Plain-language statement

There exists a non-zero polynomial satisfying the conditions.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Exists nonzero solution gen

GuruswamiSudan.exists_nonzero_solution_gen

Plain-language statement

Generalized existence: non-zero kernel element for arbitrary degree bound D, given numVars k D > numConstraints n m.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Gs degree bound sq gt

GuruswamiSudan.gs_degree_bound_sq_gt

Plain-language statement

Lower bound: (gs_degree_bound + 1)^2 > (m+1/2)^2 * k * n.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Gs dvd property

GuruswamiSudan.gs_dvd_property

Plain-language statement

Divisibility via the rate-corrected GS system. Uses gs_degree_bound (ρ=k/n) and gs_johnson instead of the conservative proximity_gap versions.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record