Source-pinned research
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.
573 results
Clear filtersKZG.CommitmentScheme.binding
Plain-language statement
The KZG scheme satisfies evaluation binding provided t-SDH holds.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.binding_cond_le_t_sdh_cond
Plain-language statement
Transition 2: a successful extended binding run maps to a successful t-SDH instance.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.binding_game_ext_eq_binding_game
Plain-language statement
Transition 1: extending the binding game output preserves the event.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.choose_s_conflict_alpha
Plain-language statement
The conflict point is not already included in chooseSConflict.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.choose_s_conflict_insert_eval_ne_zero
Plain-language statement
The conflict-branch adjoined vanishing product is nonzero at τ.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.choose_s_conflict_size
Plain-language statement
chooseSConflict returns exactly n elements.
Source project: ArkLib
Person-level attribution pending.