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 150 research declarations. Search 10,000 more complete Mathlib declarations.
150 results
Clear filtersKEMScheme.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.
map_construction
Plain-language statement
The T-transform is natural in any oracle-semantics morphism that preserves both the plaintext-to-coins query capability and the distinguished lift of ProbComp.
Source project: VCVio
Person-level attribution pending.
MerkleTree.completeness
Project documentation
Completeness theorem for Merkle trees: for any full binary tree with 2 ^ n leaves, and for any index i, the honestly-generated opening proof verifies against the honestly-built root with probability one.
Source project: VCVio
Person-level attribution pending.
MerkleTree.functional_completeness
Project documentation
A functional completeness theorem for Merkle proofs built from buildMerkleTree_with_hash.
Source project: VCVio
Person-level attribution pending.
negligible_polynomial_mul
Project documentation
If f is negligible, then fun n => ↑(p.eval n) * f n is negligible for any polynomial p. This is the key lemma for handling polynomial-loss security reductions.
Source project: VCVio
Person-level attribution pending.
ofReal_tvDist_bind_left_le_const
Plain-language statement
ℝ≥0∞ form of tvDist_bind_left_le_const, matching the quantitative APIs: a per-a bound ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε on the support of mx lifts through the shared bind.
Source project: VCVio
Person-level attribution pending.