Research proof index

Coordinate isolation (Hachi Lemma 8, case (C), the c5 subtract-and-divide crux): if c ≡ⱼ c', the challenge-difference sum collapses to the j-th block, tensorG (c − c') x = (cⱼ − c'ⱼ) •ᵥ (G_k *ᵥ xⱼ).

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.

Example usage of AssocFullyRightAssociate -/ theorem Assoc4 {G : Type _} [Magma G] (assoc : Equation4512 G) : ∀ x y z w : G, ((x ◇ y) ◇ z) ◇ w = x ◇ (y ◇ (z ◇ w)) := fun x y z w ↦ AssocFullyRightAssociate assoc (fun | 0 => x | 1 => y | 2 => z | 3 => w : Fin 4 → G) (((Lf 0 ⋆ Lf 1) ⋆ Lf 2) ⋆ Lf 3) inductive FreeSemigroup (α : Type _) | Singleton : α → FreeS...

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.

If an adversary makes at most q fresh LR queries, then the leftUntil = q LR-hybrid is the all-left endpoint game.

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.