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 research declarations. Search 10,000 more complete Mathlib declarations.
2 results
Clear filtersFiatShamirWithAbort.sign_expectedQueries_eq_sum_abortPrefixProbabilities
Plain-language statement
The expected number of signing queries is the sum, over prefixes of the retry loop, of the probability that every attempt in the prefix aborts.
Source project: VCVio
Person-level attribution pending.
FiatShamirWithAbort.verify_expectedQueryCost_eq
Plain-language statement
Verification has expected weighted query cost equal to the cost of the single verification query when a signature is present, and 0 when the signature is none.
Source project: VCVio
Person-level attribution pending.