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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersKZG.CommitmentScheme.function_binding_interpolation_branch_maps_to_arsdh
Plain-language statement
The interpolation branch maps a function-binding violation to ARSDH.
Source project: ArkLib
Person-level attribution pending.
KZG.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.