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 350 research declarations. Search 10,000 more complete Mathlib declarations.
350 results
Clear filterscompile_well_typed_on_wf_expr
Plain-language statement
Compiling a well-typed expression should produce a term of the corresponding TermType, assuming that the expression is well-formed in the symbolic environment.
Source project: Cedar Specification
Person-level attribution pending.
compile_well_typed_or_and
Plain-language statement
Combined case for or and and
Source project: Cedar Specification
Person-level attribution pending.
decrypt_usesAtMostOneQuery
Plain-language statement
T-transform decryption makes at most one hash-oracle query under unit-cost instrumentation.
Source project: VCVio
Person-level attribution pending.
DiffieHellman.dlogSuccess_sq_le_cdhSuccess_dlogToCDHReduction
Plain-language statement
Concrete form of the hardness implication CDH ⇒ DLog: if a DLog adversary succeeds with probability p, the induced CDH adversary succeeds with probability at least p^2.
Source project: VCVio
Person-level attribution pending.
DiffieHellman.probOutput_ddhExpRand_cdhToDDHReduction_eq_uniformScalar
Plain-language statement
In the random DDH game, the CDH-to-DDH reduction only matches the target with the uniform baseline probability. The bijectivity assumption identifies scalar samples with uniformly sampled group elements in the subgroup generated by g.
Source project: VCVio
Person-level attribution pending.
eagerRandomOracle_evalDist_generateSeed_bind
Plain-language statement
The eager random oracle, averaged over a uniformly sampled seed, matches the fresh independent-query semantics of evalDist. This is because the pre-sampled seed values are i.i.d. uniform, exactly matching fresh oracle queries. This is the analog of seededOracle.evalDist_liftComp_generateSeed_bind_simulateQ_run' but for eagerRandomOracle (which falls...
Source project: VCVio
Person-level attribution pending.