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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,513 to 1,518 of 2,569 results.
KZG.CommitmentScheme.query_ne_tau_of_find_query_with_srs_power_none
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical statement
Equality with the second SRS power identifies a field element as the trapdoor.
Source project: ArkLib
Person-level attribution pending.