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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersKZG.CommitmentScheme.arsdh_game_eq
Plain-language statement
Transition 4: the mapped game equals the ARSDH experiment
Source project: ArkLib
Person-level attribution pending.
KZG.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_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.