therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 8 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

8 results

Clear filters
Project-declaredLean 4.31.0

T sdh denominator ne zero of opening equations

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.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

T sdh game eq

KZG.CommitmentScheme.t_sdh_game_eq

Plain-language statement

Transition 4: the mapped extended binding game is the t-SDH experiment.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record