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.function_binding
Plain-language statement
The KZG scheme satisfies function binding provided ARSDH holds.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.function_binding_cond_ext_output_maps_to_arsdh
Plain-language statement
A supported extended function-binding violation maps to an ARSDH-winning output.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.function_binding_conflicting_evaluations_branch_maps_to_arsdh
Plain-language statement
The conflicting-evaluations branch maps a function-binding violation to ARSDH.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.function_binding_game_ext_eq_function_binding_game
Plain-language statement
Transition 1: extending output for proofs and commitment preserves the condition
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.function_binding_game_ext_support_srs
Plain-language statement
Extract the sampled SRS equation from a supported extended function-binding game output.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.function_binding_game_ext_support_verify_all
Plain-language statement
Accepted outputs in the extended function-binding game correspond to successful KZG checks.
Source project: ArkLib
Person-level attribution pending.