Research proof index

Proof that the BN254 base field characteristic is prime

NOTE: This could be generalized to 2 * N instead of 2 ^ (ϑ + 1). Also, this can be proved for ↔ instead of →.

Output-only projection corollary of fst_map_run_simulateQ.

Lemma 3.3 (Part 2): Bound on agreeing cells inside D For any column j that is in the disagreement set D, there is at most one parameter r in R* such that the columns Uᵣ j and Vᵣ j agree. Therefore, the total number of agreeing cells (r, j) with j ∈ D is at most |D|.

Lemma 3.3 (Part 1): Bound on agreeing cells outside D The set of agreeing cells (r, j) where j ∉ D is exactly the Cartesian product of R* and Dᶜ (the columns not in D).

The number of elements in ∀ i, ↥(S i) satisfying eval (↑·) f = 0 equals the number of elements in Fintype.piFinset (fun i => (S i).toFinset) satisfying eval · f = 0.