Source-pinned research

Research proof index

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.

1 topic

573 results

Clear filters
Project-declaredLean 4.31.0

Rel Dist From Code le iff dist From Code le

Code.relDistFromCode_le_iff_distFromCode_le

Plain-language statement

A word u is relatively close to a code C within an relative error bound δ if and only if it is relatively close within the equivalent absolute error bound ⌊δ * n⌋.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

UDR close iff exists unique close codeword

Code.UDR_close_iff_exists_unique_close_codeword

Plain-language statement

A word u is within the uniqueDecodingRadius of a code C if and only if there exists exactly one codeword v in C that is that close.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

UDR close iff rel URD close

Code.UDR_close_iff_relURD_close

Plain-language statement

A word u is close to a code C within the absolute unique decoding radius if and only if it is close within the relative unique decoding radius.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Binding Advantage to Commitment le keyed CRAdvantage

CollisionResistance.bindingAdvantage_toCommitment_le_keyedCRAdvantage

Plain-language statement

Binding ≤ keyed-CR (standard model): for any binding adversary A against the hash-based commitment scheme H.toCommitment, the binding advantage is bounded by the keyed-CR advantage of H against the natural reduction adversary bindingAdv_toCRAdv A. A binding-game win has m₁ ≠ m₂ together with both openings verifying: `H k (m₁, s₁) = c = H k (...

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Rom CRAdvantage le birthday

CollisionResistance.romCRAdvantage_le_birthday

Plain-language statement

ROM Collision Resistance birthday bound: for any t-query ROM-CR adversary A over a hash range Y, the advantage is bounded by (t+2) * (t+1) / (2 * |Y|) (a vacuous bound when |Y| = 0). The two extra queries account for the experiment's verification queries, which share the adversary's cache.

program verificationseparation logiccryptography

Source project: VCVio

Person-level attribution pending.

View proof record
Project-declaredLean 4.31.0

Combine eq cases

Combine.combine_eq_cases

Project documentation

Definition 4.11.2 Combine(d*, r, (f_0, d_0), …, (f_{m-1}, d_{m-1}))(x) := if (r * φ(x)) = 1 then sum_{i < m} r_i * f_i(x) * (dstar - degree + 1) else sum_{i < m} r_i * f_i(x) * (1 - r * φ(x)^(dstar - degree + 1)) / (1 - r * φ(x))

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record