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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersKZG.CommitmentScheme.query_ne_tau_of_find_query_with_srs_power_none
Plain-language statement
If no query matches the second SRS power, then no query is equal to τ.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.queryReps_exists
Plain-language statement
Every query value is represented by some index in queryReps.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.t_sdh_cond_of_two_valid_openings
Project documentation
The algebraic core of evaluation binding: two valid KZG openings of the same commitment at the same point, but to different values, yield a t-SDH solution with challenge c = -query. This lemma is intentionally isolated from the probabilistic (game-based) binding game. The proof of binding_cond_le_t_sdh_cond only needs to extract hsrs and the two `ve...
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.t_sdh_denominator_ne_zero_of_opening_equations
Plain-language statement
If two accepted openings at the same query give different responses, the t-SDH denominator τ + (-query) cannot vanish. This is the small algebraic contradiction used to avoid a separate query = τ branch in the binding reduction.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.t_sdh_game_eq
Plain-language statement
Transition 4: the mapped extended binding game is the t-SDH experiment.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.zmod_eq_of_srs_power_eq
Plain-language statement
Equality with the second SRS power identifies a field element as the trapdoor.
Source project: ArkLib
Person-level attribution pending.