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 filtersArkLib.Lattices.Hachi.tensorG1_coord_diff
Project documentation
Coordinate isolation at k = 1 (Hachi Lemma 8, case (C), the c4 subtract-and-divide crux): if c ≡ⱼ c', then tensorG1 (c − c') ŵ = (cⱼ − c'ⱼ) · wⱼ where w := G_blocks *ᵥ ŵ is the recomposed carrier.
Source project: ArkLib
Person-level attribution pending.
AsymmEncAlg.IND_CPA_advantage_toReal_le_sum_step_signedAdvantageReal_abs
Plain-language statement
Planned generic one-time-to-many-time lift: bounded multi-query IND-CPA advantage is at most the sum of the extracted one-time signed advantages over the first q fresh LR queries.
Source project: VCVio
Person-level attribution pending.
AsymmEncAlg.IND_CPA_LR_hybridGame_q_evalDist_eq_left_of_MakesAtMostQueries
Plain-language statement
If an adversary makes at most q fresh LR queries, then the leftUntil = q LR-hybrid is the all-left endpoint game.
Source project: VCVio
Person-level attribution pending.
AsymmEncAlg.IND_CPA_run'_evalDist_eq_queryImpl'_of_bounded_eq
Plain-language statement
If a counted IND-CPA hybrid implementation agrees with the counted real implementation through the first q fresh LR queries, then any adversary making at most q LR queries sees the same output distribution as in the real IND-CPA game.
Source project: VCVio
Person-level attribution pending.
AsymmEncAlg.IND_CPA_stepAdversary_signedAdvantageReal_eq_hybridDiff_half
Plain-language statement
Planned adjacent-gap characterization for the extracted step adversary. Once IND_CPA_stepAdversary_game_eq_hybridBranch is proved, this is just the one-time analogue of IND_CPA_signedAdvantageReal_eq_lrDiff_half.
Source project: VCVio
Person-level attribution pending.
BCIKS20AppendixA.canonicalRepOf𝒪_mk
Plain-language statement
Canonical representatives of quotient constructors are computed by modByMonic.
Source project: ArkLib
Person-level attribution pending.