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 199 research declarations. Search 10,000 more complete Mathlib declarations.
199 results
Clear filtersCslib.Crypto.Protocols.PerfectSecrecy.perfectlySecret_iff_indep
Plain-language 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
Plain-language 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
Plain-language 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
Plain-language statement
Translation-invariant Shamir tail samplers induce secret-independent views for unauthorized coalitions.
Source project: Lean Computer Science Library
Person-level attribution pending.
Cslib.FLP.AdmissibleRun.fault_zero
Plain-language statement
Specialize the definition of Algorithm.AdmissibleRun to the case of zero fault.
Source project: Lean Computer Science Library
Person-level attribution pending.