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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersKZG.CommitmentScheme.function_binding_query_eq_tau_branch_maps_to_arsdh
Plain-language statement
The branch that finds a query equal to τ maps to ARSDH.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.h1_zs_eq_h2_prime
Plain-language statement
The interpolation-branch output satisfies the ARSDH exponent equation.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.interpolate_degree_ge_of_no_data
Plain-language statement
If no degree-n coefficient vector fits the data, interpolation has degree at least n + 1.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.lagrange_zs_conversion
Plain-language statement
Barycentric conversion for interpolation divided by the vanishing polynomial at τ.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.nat_cast_range_card_zmod_of_le
Plain-language statement
Casting the first k ≤ p natural numbers into ZMod p is injective.
Source project: ArkLib
Person-level attribution pending.
KZG.CommitmentScheme.no_data_queryReps_of_function_binding_cond
Plain-language statement
Function-binding failure rules out fitting the deduplicated query representatives.
Source project: ArkLib
Person-level attribution pending.