Project-declaredLean 4.31.0
Find s card
KZG.CommitmentScheme.find_s_card
Mathematical statement
A successful findS result has cardinality n + 1.
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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,495 to 1,500 of 2,569 results.
View proof record
Project-declaredLean 4.31.0
Find s existence
KZG.CommitmentScheme.find_s_existence
Mathematical statement
Some n + 1 subset has interpolation value at τ different from c.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Find s subset
KZG.CommitmentScheme.find_s_subset
Mathematical statement
A successful findS result is a subset of the input set.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Find s successful
KZG.CommitmentScheme.find_s_successful
Mathematical statement
Under the degree hypotheses, findS finds a diverging subset.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Finset card gt of interpolate degree ge
KZG.CommitmentScheme.finset_card_gt_of_interpolate_degree_ge
Mathematical statement
A high interpolation degree forces the interpolation set to have more than n + 1 points.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.
Project-declaredLean 4.31.0
Function binding
KZG.CommitmentScheme.function_binding
Mathematical statement
The KZG scheme satisfies function binding provided ARSDH holds.
cryptographyproof systemscoding theory
Source project: ArkLib
Person-level attribution pending.