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 filtersKEMScheme.IND_CPA_Game_eq_IND_CCA_Game_toIND_CCA
Plain-language statement
The one-stage IND-CPA game is exactly the IND-CCA game instantiated with the trivial CPA-to-CCA embedding (toIND_CCA) that never uses the decryption oracle.
Source project: VCVio
Person-level attribution pending.
KEMScheme.ind_cpa_one_time_bias_advantage_compose_with_dem_le
Plain-language statement
Proof-ladders A1 reduction statement: the one-time IND-CPA advantage of textbook KEM+DEM is bounded by two KEM IND-CPA advantages plus one DEM IND-CPA advantage, using the canonical left/right and DEM reductions defined above. The runtime coherence hypotheses require runtime.evalDist to be a monad morphism (preserves pure and distributes >>=) and to...
Source project: VCVio
Person-level attribution pending.
KEMScheme.perfectlyCorrect_composeWithDEM
Plain-language statement
If a KEM and externally keyed DEM are both perfectly correct in the concrete probabilistic semantics of m, then their composition is also perfectly correct.
Source project: VCVio
Person-level attribution pending.
KZG.commit_eq
Plain-language statement
The commitment to a mathlib polynomial poly of maximum degree n is equal to g₁ ^ (poly.1.eval a).val
Source project: ArkLib
Person-level attribution pending.
KZG.commit_eq_c_polynomial
Plain-language statement
The commitment to a computable polynomial (CPolynomial) poly of maximum degree n is equal to g₁ ^ (poly.eval a).val.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.arsdh_game_eq
Plain-language statement
Transition 4: the mapped game equals the ARSDH experiment
Source project: ArkLib
Person-level attribution pending.