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 filtersCWSSStructure.toShape_seqCompose
Plain-language statement
The shape induced by finite sequential CWSS data is the generic sequential composition of the component shapes.
Source project: ArkLib
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.
dist_affineCombination_le_dist_interleaved₂
Plain-language statement
Lemma: Distance of Affine Combination is Bounded by Interleaved Distance
Source project: ArkLib
Person-level attribution pending.
dist_interleaved_code_to_code_lb
Plain-language statement
Lemma 4.3, [AHIV22] (row-span lower bound). If the interleaved word U⋆ is more than e far from the interleaved code L^⋈κ, then the row-span of U⋆ contains a word more than e far from L. The additional field-size assumption |F| > e is needed: for small fields one can have a linear subspace of F^ι consisting entirely of e-sparse vector...
Source project: ArkLib
Person-level attribution pending.