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,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 595 to 600 of 2,569 results.
Cslib.Crypto.Protocols.PerfectSecrecy.ciphertextIndist_of_perfectlySecret
Mathematical statement
Perfect secrecy implies ciphertext indistinguishability.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.PerfectSecrecy.perfectlySecret_iff_indep
Mathematical statement
Perfect secrecy is equivalent to message-ciphertext independence. The two formulations are related by multiplying/dividing by marginal(c).
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.PerfectSecrecy.shannonKeySpace
Project documentation
Perfect secrecy requires |K| ≥ |M| (Shannon's theorem).
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.natDegree_sharingPolynomial_le
Mathematical statement
If the tail polynomial has degree < n, then the sharing polynomial has natural degree at most n.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.SecretSharing.Shamir.Polynomial.reconstruct_eq_constantCoeff_of_eval_eq
Mathematical statement
Reconstruction recovers the constant coefficient of any low-degree polynomial from its values at distinct points.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.Crypto.Protocols.SecretSharing.Shamir.view_indist_of_tailSampler
Mathematical statement
Translation-invariant Shamir tail samplers induce secret-independent views for unauthorized coalitions.
Source project: Lean Computer Science Library
Person-level attribution pending.