Skip to main content

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 2,569 research declarations. Search 10,000 more complete Mathlib declarations.

All topics

Showing 511 to 516 of 2,569 results.

Project-declaredLean 4.31.0

Rel Dist From Code le iff dist From Code le

Code.relDistFromCode_le_iff_distFromCode_le

Mathematical 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

Mathematical 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

Mathematical 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

Mathematical 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

Mathematical 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