noncomputable def PolyEquivProb.agreementProb {F : Type u_1} [CommRing F] [IsDomain F] [Fintype F] [DecidableEq F] {m : ℕ} (p₁ p₂ : MvPolynomial (Fin m) F) : ℚ≥0

The probability that two multivariate polynomials p₁, p₂ ∈ F[X_1, …, X_m] agree on a uniformly random point in F^m, defined as the number of points where eval r p₁ = eval r p₂ divided by |F|^m.

theorem PolyEquivProb.equiv_agreement_prob_eq_one {F : Type u_1} [CommRing F] [IsDomain F] [Fintype F] [DecidableEq F] {m : ℕ} (p₁ p₂ : MvPolynomial (Fin m) F) (heq : p₁ = p₂) : agreementProb p₁ p₂ = 1

If p₁ = p₂ as polynomials then their agreement probability is 1: they agree on every point of F^m.

theorem PolyEquivProb.nonequiv_agreement_prob_le_third {F : Type u_1} [CommRing F] [IsDomain F] [Fintype F] [DecidableEq F] {m : ℕ} (p₁ p₂ : MvPolynomial (Fin m) F) (hne : p₁ ≠ p₂) (hdeg : ∀ (i : Fin m), MvPolynomial.degreeOf i (p₁ - p₂) ≤ 1) (hF : 3 * m ≤ Fintype.card F) : agreementProb p₁ p₂ ≤ 1 / 3

Schwartz–Zippel-style bound: if p₁ ≠ p₂ are multilinear (degree ≤ 1 in each variable) and |F| ≥ 3m, then the probability that p₁ and p₂ agree on a uniformly random point of F^m is at most 1/3.

noncomputable def PolyEquivProb.boolToField {m : ℕ} {F : Type u_1} [CommRing F] (v : Fin m → Bool) : Fin m → F

Embeds a Boolean assignment v : Fin m → Bool into a field point Fin m → F by sending true ↦ 1 and false ↦ 0.

def PolyEquivProb.boolSupport {m : ℕ} (v : Fin m → Bool) : Finset (Fin m)

The support of a Boolean vector v : Fin m → Bool, i.e. the set of indices where v i = true.

noncomputable def PolyEquivProb.multilinearExtension {m : ℕ} {F : Type u_1} [CommRing F] (f : (Fin m → Bool) → F) : MvPolynomial (Fin m) F

The (unique) multilinear extension of a Boolean function f : {0,1}^m → F to a multivariate polynomial over F. For each subset S ⊆ Fin m we form the indicator polynomial (∏_{i ∈ S} X_i) · (∏_{i ∉ S} (1 - X_i)), weight it by f(1_S), and sum over all subsets.

theorem PolyEquivProb.indicator_eval_eq_ite {m : ℕ} {F : Type u_1} [CommRing F] (S : Finset (Fin m)) (v : Fin m → Bool) : (∏ i ∈ S, if v i = true then 1 else 0) * ∏ i ∈ Finset.univ \ S, (1 - if v i = true then 1 else 0) = if S = boolSupport v then 1 else 0

Evaluating the indicator polynomial for the subset S at the Boolean point v yields 1 if S equals the support of v and 0 otherwise.

theorem PolyEquivProb.boolVec_boolSupport {m : ℕ} (v : Fin m → Bool) : (fun (i : Fin m) => decide (i ∈ boolSupport v)) = v

The indicator function of boolSupport v agrees with v itself.

theorem PolyEquivProb.eval_multilinearExtension {m : ℕ} {F : Type u_1} [CommRing F] (f : (Fin m → Bool) → F) (v : Fin m → Bool) : (MvPolynomial.eval (boolToField v)) (multilinearExtension f) = f v

Interpolation property: the multilinear extension of f evaluates to f v at every Boolean point v.

theorem PolyEquivProb.degreeOf_indicator_term_le {m : ℕ} {F : Type u_1} [CommRing F] [IsDomain F] (S : Finset (Fin m)) (n : Fin m) (c : F) : MvPolynomial.degreeOf n ((MvPolynomial.C c * ∏ i ∈ S, MvPolynomial.X i) * ∏ i ∈ Finset.univ \ S, (1 - MvPolynomial.X i)) ≤ 1

Each term c · (∏_{i ∈ S} X_i) · (∏_{i ∉ S} (1 - X_i)) in the multilinear extension has degree at most 1 in every variable n.

theorem PolyEquivProb.multilinearExtension_degreeOf_le {m : ℕ} {F : Type u_1} [CommRing F] [IsDomain F] (f : (Fin m → Bool) → F) (n : Fin m) : MvPolynomial.degreeOf n (multilinearExtension f) ≤ 1

The multilinear extension is, indeed, multilinear: it has degree at most 1 in every variable.

noncomputable def PolyEquivProb.arithmetize {m : ℕ} {F : Type u_1} [CommRing F] (bp : BranchingPrograms.BranchingProgram m) : MvPolynomial (Fin m) F

Arithmetization of a (read-once) branching program: produce the multilinear extension of its Boolean evaluation function, viewed as a polynomial over F.

theorem PolyEquivProb.arithmetize_eq_of_equiv {m : ℕ} {F : Type u_1} [CommRing F] (bp₁ bp₂ : BranchingPrograms.BranchingProgram m) (h : BranchingPrograms.BPEquiv bp₁ bp₂) : arithmetize bp₁ = arithmetize bp₂

Equivalent branching programs (those computing the same Boolean function) arithmetize to the same multilinear polynomial.

theorem PolyEquivProb.equiv_of_arithmetize_eq {m : ℕ} {F : Type u_1} [CommRing F] [IsDomain F] (bp₁ bp₂ : BranchingPrograms.BranchingProgram m) (h : arithmetize bp₁ = arithmetize bp₂) : BranchingPrograms.BPEquiv bp₁ bp₂

Conversely, if two branching programs arithmetize to the same polynomial (over an integral domain), they are equivalent as Boolean functions.

theorem PolyEquivProb.arithmetize_ne_of_not_equiv {m : ℕ} {F : Type u_1} [CommRing F] [IsDomain F] (bp₁ bp₂ : BranchingPrograms.BranchingProgram m) (h : ¬BranchingPrograms.BPEquiv bp₁ bp₂) : arithmetize bp₁ ≠ arithmetize bp₂

Contrapositive of equiv_of_arithmetize_eq: inequivalent branching programs have distinct arithmetizations.

theorem PolyEquivProb.arithmetize_degreeOf_le {m : ℕ} {F : Type u_1} [CommRing F] [IsDomain F] (bp : BranchingPrograms.BranchingProgram m) (n : Fin m) : MvPolynomial.degreeOf n (arithmetize bp) ≤ 1

The arithmetization of a branching program is multilinear: degree at most 1 in every variable.

theorem PolyEquivProb.arithmetize_diff_degreeOf_le {m : ℕ} {F : Type u_1} [CommRing F] [IsDomain F] (bp₁ bp₂ : BranchingPrograms.BranchingProgram m) (n : Fin m) : MvPolynomial.degreeOf n (arithmetize bp₁ - arithmetize bp₂) ≤ 1

The difference of two arithmetizations is still multilinear (degree ≤ 1 in each variable), as needed to apply the Schwartz–Zippel bound.

theorem PolyEquivProb.equiv_robp_agreement_prob_eq_one {F : Type u_1} [CommRing F] [IsDomain F] [Fintype F] [DecidableEq F] {m : ℕ} (bp₁ bp₂ : BranchingPrograms.BranchingProgram m) (hequiv : BranchingPrograms.BPEquiv bp₁ bp₂) : agreementProb (arithmetize bp₁) (arithmetize bp₂) = 1

Completeness of the randomized equivalence test for branching programs: equivalent programs always yield agreement probability 1 between their arithmetizations.

theorem PolyEquivProb.nonequiv_robp_agreement_prob_le_third {F : Type u_1} [CommRing F] [IsDomain F] [Fintype F] [DecidableEq F] {m : ℕ} (bp₁ bp₂ : BranchingPrograms.BranchingProgram m) (hne : ¬BranchingPrograms.BPEquiv bp₁ bp₂) (hF : 3 * m ≤ Fintype.card F) : agreementProb (arithmetize bp₁) (arithmetize bp₂) ≤ 1 / 3

Soundness of the randomized equivalence test: when two branching programs are inequivalent and |F| ≥ 3m, their arithmetizations agree on a random point with probability at most 1/3.

theorem PolyEquivProb.robp_agreement_claim {F : Type u_1} [CommRing F] [IsDomain F] [Fintype F] [DecidableEq F] {m : ℕ} (bp₁ bp₂ : BranchingPrograms.BranchingProgram m) (hF : 3 * m ≤ Fintype.card F) : (BranchingPrograms.BPEquiv bp₁ bp₂ → agreementProb (arithmetize bp₁) (arithmetize bp₂) = 1) ∧ (¬BranchingPrograms.BPEquiv bp₁ bp₂ → agreementProb (arithmetize bp₁) (arithmetize bp₂) ≤ 1 / 3)

The combined completeness/soundness statement underlying the BPP algorithm for EQ_ROBP: with |F| ≥ 3m, equivalent branching programs yield agreement probability 1, while inequivalent ones yield agreement probability ≤ 1/3.