structure Probabilistic.GraphPairDesc : Type 1

A formal description of a pair of finite simple graphs (G, H), packaged together with the decidability and finiteness instances needed to manipulate them constructively. Used as the underlying mathematical object for the graph isomorphism problem ISO.

• V : Type
• instFintypeV : Fintype self.V
• instDecEqV : DecidableEq self.V
• G : SimpleGraph self.V
• instDecRelG : DecidableRel self.G.Adj
• W : Type
• instFintypeW : Fintype self.W
• instDecEqW : DecidableEq self.W
• H : SimpleGraph self.W
• instDecRelH : DecidableRel self.H.Adj

def Probabilistic.GraphPairDesc.isIsomorphic (d : GraphPairDesc) : Prop

A graph-pair description d is isomorphic if there exists a graph isomorphism d.G ≃g d.H. This is the property defining membership in ISO.

structure Probabilistic.GraphPairEncoding (Γ : Type) : Type 1

A faithful encoding of graph-pair descriptions as strings over alphabet Γ, specified by an injective encode function and a decode function that inverts it. Used to turn the mathematical object GraphPairDesc into the language ISO ⊆ List Γ.

• encode : GraphPairDesc → List Γ
• decode : List Γ → Option GraphPairDesc
• encode_injective : Function.Injective self.encode
• decode_encode (d : GraphPairDesc) : self.decode (self.encode d) = some d

def Probabilistic.ISO {Γ : Type} (enc : GraphPairEncoding Γ) : Set (List Γ)

The graph isomorphism language

ISO = {⟨G, H⟩ ∣ G and H are isomorphic graphs},

defined here as the set of strings s over alphabet Γ that encode some graph-pair description d for which d.G ≃g d.H.

theorem Probabilistic.polynomial_roots_le_degree {F : Type u_1} [Field F] (p : Polynomial F) (hp : p ≠ 0) : ↑p.roots.card ≤ p.degree

Polynomial Lemma. A non-zero univariate polynomial p : F[X] over a field has at most deg p roots: the cardinality of its root multiset is bounded by its degree.

theorem Probabilistic.distinct_poly_agree_le_degree {F : Type u_1} [Field F] (p₁ p₂ : Polynomial F) (d : ℕ) (hd₁ : p₁.natDegree ≤ d) (hd₂ : p₂.natDegree ≤ d) (_hne : p₁ ≠ p₂) : (p₁ - p₂).roots.card ≤ d

Corollary of the Polynomial Lemma. If p₁, p₂ : F[X] both have degree ≤ d and p₁ ≠ p₂, then they agree on at most d points: equivalently, the difference p₁ - p₂ has at most d roots.

theorem Probabilistic.poly_root_count_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : Polynomial F) (hp : p ≠ 0) (d : ℕ) (hd : p.natDegree ≤ d) : {r : F | p.IsRoot r}.card ≤ d

Over a finite field F, a non-zero polynomial of degree ≤ d has at most d roots inside F: the cardinality of {r ∈ F ∣ p(r) = 0} is bounded by d.

theorem Probabilistic.poly_root_prob_le {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (p : Polynomial F) (hp : p ≠ 0) (d : ℕ) (hd : p.natDegree ≤ d) : ↑{r : F | p.IsRoot r}.card / ↑(Fintype.card F) ≤ ↑d / ↑(Fintype.card F)

Univariate Schwartz-Zippel (probability form). If p ∈ F[X] is non-zero with degree ≤ d and r is chosen uniformly at random from a finite field F, then Pr[p(r) = 0] ≤ d / |F|.

theorem Probabilistic.schwartz_zippel_book {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m : ℕ} {p : MvPolynomial (Fin m) F} (hp : p ≠ 0) (d : ℕ) (hd : ∀ (i : Fin m), MvPolynomial.degreeOf i p ≤ d) : ↑{r : Fin m → F | (MvPolynomial.eval r) p = 0}.card / ↑(Fintype.card F) ^ m ≤ ↑d * ↑m / ↑(Fintype.card F)

Schwartz-Zippel Lemma (Sipser textbook form). If p(x₁, …, xₘ) ∈ F[x₁, …, xₘ] is a non-zero multivariate polynomial of degree ≤ d in each variable and r₁, …, rₘ are chosen uniformly at random from a finite field F, then

Pr[p(r₁, …, rₘ) = 0] ≤ dm / |F|.

def TuringMachine.InBPPWithError {Γ : Type} [DecidableEq Γ] (ε : ℚ) (A : Set (List Γ)) : Prop

A language A ⊆ Σ* is in BPP with error ε if some polynomial-time probabilistic Turing machine M decides A with two-sided error ε: there exist Q, M, an exponent k, and a runtime bound t' such that M runs in time t', t' = O(nᵏ), and M.decidesWithError A ε t' holds. The class BPP itself corresponds to ε = 1/3.

theorem TuringMachine.decidesWithError_mono {Q : Type} [DecidableEq Q] {Γ : Type} [DecidableEq Γ] (M : PTM Q Γ) (A : Set (List Γ)) (ε₁ ε₂ : ℚ) (t : ℕ → ℕ) (hle : ε₁ ≤ ε₂) (hε₂ : 0 ≤ ε₂) (hDec : M.decidesWithError A ε₁ t) : M.decidesWithError A ε₂ t

Monotonicity of decidesWithError: if a PTM M decides A with error at most ε₁ and ε₁ ≤ ε₂, then it also decides A with error at most ε₂.

theorem TuringMachine.one_step_majority_vote (Γ : Type) [DecidableEq Γ] (A : Set (List Γ)) (ε : ℚ) (hε_pos : 0 < ε) (hε_lt : ε < 1 / 2) (hA : InBPPWithError ε A) : InBPPWithError (ε ^ 2 * (3 - 2 * ε)) A

One-step majority vote for BPP. If A ∈ BPP with error ε ∈ (0, 1/2), then running the original PTM three independent times and taking the majority yields a new BPP machine with error at most ε² (3 - 2ε) < ε. This is the inductive step of the Amplification Lemma.

theorem TuringMachine.error_reduction_lt (ε : ℚ) (hε_pos : 0 < ε) (hε_lt : ε < 1 / 2) : ε ^ 2 * (3 - 2 * ε) < ε

Arithmetic fact: for 0 < ε < 1/2, the majority-vote error update ε ↦ ε² (3 - 2ε) strictly decreases ε.

theorem TuringMachine.error_reduction_pos (ε : ℚ) (hε_pos : 0 < ε) (hε_lt : ε < 1 / 2) : 0 < ε ^ 2 * (3 - 2 * ε)

Arithmetic fact: for 0 < ε < 1/2, the majority-vote error update ε² (3 - 2ε) is strictly positive.

theorem TuringMachine.error_reduction_lt_half (ε : ℚ) (hε_pos : 0 < ε) (hε_lt : ε < 1 / 2) : ε ^ 2 * (3 - 2 * ε) < 1 / 2

Arithmetic fact: the majority-vote error update stays in (0, 1/2), i.e. ε² (3 - 2ε) < 1/2 whenever 0 < ε < 1/2.

noncomputable def TuringMachine.iterError (ε₁ : ℚ) : ℕ → ℚ

The sequence of error bounds obtained by iterating the majority-vote update: iterError ε₁ 0 = ε₁, and iterError ε₁ (n+1) = e² (3 - 2e) where e = iterError ε₁ n. Each step corresponds to amplifying the BPP machine by a three-fold majority vote.

theorem TuringMachine.iterError_pos_and_lt_half (ε₁ : ℚ) (hε₁_pos : 0 < ε₁) (hε₁_lt : ε₁ < 1 / 2) (n : ℕ) : 0 < iterError ε₁ n ∧ iterError ε₁ n < 1 / 2

Joint invariant: every iterate iterError ε₁ n stays strictly between 0 and 1/2, provided the initial error ε₁ does.

theorem TuringMachine.iterError_pos (ε₁ : ℚ) (hε₁_pos : 0 < ε₁) (hε₁_lt : ε₁ < 1 / 2) (n : ℕ) : 0 < iterError ε₁ n

Positivity of the iterated error: iterError ε₁ n > 0 for all n, given 0 < ε₁ < 1/2.

theorem TuringMachine.iterError_lt_half (ε₁ : ℚ) (hε₁_pos : 0 < ε₁) (hε₁_lt : ε₁ < 1 / 2) (n : ℕ) : iterError ε₁ n < 1 / 2

Upper bound on the iterated error: iterError ε₁ n < 1/2 for all n, given 0 < ε₁ < 1/2.

theorem TuringMachine.iterated_majority_vote {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) (ε₁ : ℚ) (hε₁_pos : 0 < ε₁) (hε₁_lt : ε₁ < 1 / 2) (hA : InBPPWithError ε₁ A) (n : ℕ) : InBPPWithError (iterError ε₁ n) A

Iterating majority vote: if A ∈ BPP with initial error ε₁ ∈ (0, 1/2), then for every n there is a BPP machine deciding A with error iterError ε₁ n.

theorem TuringMachine.iterError_eventually_le (ε₁ ε₂ : ℚ) (hε₁_pos : 0 < ε₁) (hε₁_lt : ε₁ < 1 / 2) (hε₂_pos : 0 < ε₂) : ∃ (n : ℕ), iterError ε₁ n ≤ ε₂

Convergence of the iterated error to zero: for any target ε₂ > 0 there exists some iteration count n with iterError ε₁ n ≤ ε₂. The proof bounds iterError ε₁ n ≤ ε₁ · rⁿ for r = ε₁(3 - 2ε₁) < 1 and uses that geometric sequences with ratio < 1 shrink below any positive threshold.

theorem TuringMachine.amplification_lemma {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) (ε₁ ε₂ : ℚ) (hε₁_pos : 0 < ε₁) (hε₁_lt : ε₁ < 1 / 2) (hε₂_pos : 0 < ε₂) (hε₂_lt : ε₂ < 1 / 2) (hA : InBPPWithError ε₁ A) : InBPPWithError ε₂ A

Amplification Lemma for BPP (Sipser, Lecture 23). If M₁ is a polynomial-time PTM deciding A with error ε₁ < 1/2, then for any 0 < ε₂ < 1/2 there is an equivalent polynomial-time PTM M₂ deciding A with error ε₂. The proof iterates one_step_majority_vote until the error drops below ε₂.

theorem TuringMachine.amplification_lemma_exp {Γ : Type} [DecidableEq Γ] (A : Set (List Γ)) (ε₁ : ℚ) (hε₁_pos : 0 < ε₁) (hε₁_lt : ε₁ < 1 / 2) (hA : InBPPWithError ε₁ A) (p : ℕ → ℕ) : ∃ (Q : Type) (x : DecidableEq Q) (M : PTM Q Γ) (k : ℕ) (t' : ℕ → ℕ), M.runsInTime t' ∧ (IsBigO t' fun (n : ℕ) => n ^ k) ∧ ∀ (w : List Γ), (w ∈ A → M.rejectProb w (t' w.length) ≤ 1 / 2 ^ p w.length) ∧ (w ∉ A → M.acceptProb w (t' w.length) ≤ 1 / 2 ^ p w.length)

Strong Amplification Lemma for BPP. Starting from a PTM with error ε₁ < 1/2, one can produce a polynomial-time PTM whose two-sided error is at most 2^(-p(n)) for any prescribed polynomial-time-computable polynomial p. This is the ε₂ < 2^(-poly(n)) strengthening from Sipser's Lecture 23.

inductive BranchingPrograms.BPNode (m N : ℕ) : Type

A node of a branching program with m input variables and N total nodes. A node is either a query on variable var : Fin m with two successors zero, one : Fin N (followed depending on whether the bit is 0 or 1), or an output leaf carrying a Boolean answer.

• query {m N : ℕ} (var : Fin m) (zero one : Fin N) : BPNode m N
• output {m N : ℕ} (val : Bool) : BPNode m N

structure BranchingPrograms.BranchingProgram (m : ℕ) : Type

A branching program on m Boolean input variables. It has numNodes nodes (with node 0 being the start node) and a nodes table assigning each index a BPNode.

• numNodes : ℕ
• numNodes_pos : 0 < self.numNodes
• nodes : Fin self.numNodes → BPNode m self.numNodes

def BranchingPrograms.BranchingProgram.eval {m : ℕ} (bp : BranchingProgram m) (assignment : Fin m → Bool) : Bool

Evaluate a branching program bp on a Boolean assignment. Execution starts at node 0 and follows query edges according to the assignment; the recursion is bounded by bp.numNodes units of fuel via the inner go.

def BranchingPrograms.BranchingProgram.eval.go {m : ℕ} (bp : BranchingProgram m) (assignment : Fin m → Bool) (node : Fin bp.numNodes) : ℕ → Bool

def BranchingPrograms.BPEquiv {m : ℕ} (bp₁ bp₂ : BranchingProgram m) : Prop

Two branching programs are equivalent (B₁ ≡ B₂) if they compute the same Boolean function: bp₁.eval a = bp₂.eval a for every assignment a.

def BranchingPrograms.BranchingProgram.isReadOnce {m : ℕ} (bp : BranchingProgram m) : Prop

A branching program is read-once if, along any computation path, each input variable is queried at most once. Formally: for every list of nodes path along which the program might step, any two indices i, j whose nodes both query the same variable v must coincide.

structure BranchingPrograms.ROBPPairDesc : Type

A description of a pair (B₁, B₂) of read-once branching programs on the same number of variables, together with proofs that each is read-once. This is the mathematical object whose equivalence problem is EQ_ROBP.

• numVars : ℕ
• B₁ : BranchingProgram self.numVars
• B₂ : BranchingProgram self.numVars
• B₁_readOnce : self.B₁.isReadOnce
• B₂_readOnce : self.B₂.isReadOnce

def BranchingPrograms.ROBPPairDesc.isEquivalent (d : ROBPPairDesc) : Prop

The semantic equivalence relation on ROBPPairDesc: d.B₁ ≡ d.B₂ as Boolean functions.

structure BranchingPrograms.ROBPPairEncoding (Γ : Type) : Type

A faithful encoding of ROBPPairDesc as strings over alphabet Γ, used to turn the abstract equivalence problem into a language EQ_ROBP ⊆ List Γ.

• encode : ROBPPairDesc → List Γ
• decode : List Γ → Option ROBPPairDesc
• encode_injective : Function.Injective self.encode
• decode_encode (d : ROBPPairDesc) : self.decode (self.encode d) = some d

def BranchingPrograms.EQ_ROBP {Γ : Type} (enc : ROBPPairEncoding Γ) : Set (List Γ)

The language of equivalent read-once branching programs:

EQ_ROBP = {⟨B₁, B₂⟩ ∣ B₁ ≡ B₂ as ROBPs},

with the pair encoded as a string over Γ using enc. Membership in BPP is proved in EQ_ROBP_in_BPP.

def BranchingPrograms.eqROBP_numBits (n : ℕ) : ℕ

Number of random bits used by the EQ_ROBP BPP decider on inputs of length n: a polynomial budget of n² + 1 bits, enough to sample a random field element per variable.

theorem BranchingPrograms.eqROBP_numBits_poly : TuringMachine.IsBigO eqROBP_numBits fun (n : ℕ) => n ^ 2

The random-bit budget eqROBP_numBits n = n² + 1 is polynomial in n, specifically O(n²).

theorem BranchingPrograms.eqROBP_soundness_bound {Γ : Type} [DecidableEq Γ] (enc : ROBPPairEncoding Γ) (w : List Γ) (d : ROBPPairDesc) (hdec : enc.decode w = some d) (hvalid : enc.encode d = w) (hne : ¬BPEquiv d.B₁ d.B₂) (q : ℕ) (hq_prime : Nat.Prime q) (hq_ge : 3 * d.numVars ≤ q) (extractPt : (Fin (eqROBP_numBits w.length) → Bool) → Fin d.numVars → ZMod q) (rd_decide : (Fin (eqROBP_numBits w.length) → Bool) → Bool) (h_rd : ∀ (bits : Fin (eqROBP_numBits w.length) → Bool), rd_decide bits = true ↔ (MvPolynomial.eval (extractPt bits)) (∑ a : Fin d.numVars → Bool with d.B₁.eval a = true, ∏ i : Fin d.numVars, if a i = true then MvPolynomial.X i else 1 - MvPolynomial.X i) = (MvPolynomial.eval (extractPt bits)) (∑ a : Fin d.numVars → Bool with d.B₂.eval a = true, ∏ i : Fin d.numVars, if a i = true then MvPolynomial.X i else 1 - MvPolynomial.X i)) : ↑{bits : Fin (eqROBP_numBits w.length) → Bool | rd_decide bits = true}.card / 2 ^ eqROBP_numBits w.length ≤ 1 / 3

Soundness bound for the EQ_ROBP randomized decider. On a no-instance (B₁, B₂) (with B₁ ≢ B₂), the probability that the verifier accepts is at most 1/3. This is the Schwartz-Zippel-based bound from Sipser Lecture 24: when the arithmetizations p₁, p₂ (each of total degree ≤ numVars in every variable) disagree, Pr[p₁(r) = p₂(r)] ≤ d·m/q ≤ 1/3 for q ≥ 3·numVars.

theorem BranchingPrograms.eqROBP_random_decider {Γ : Type} [DecidableEq Γ] (enc : ROBPPairEncoding Γ) : ∃ (rd : TuringMachine.RandomDecider Γ), rd.isPolyTime ∧ rd.decidesWithBoundedError (EQ_ROBP enc)

Existence of the EQ_ROBP random decider. There is a polynomial-time RandomDecider for EQ_ROBP with two-sided error ≤ 1/3: it samples a random point r ∈ (ℤ/q)^m (with q prime, q ≥ 3m) using the input random bits, arithmetizes both branching programs to multivariate polynomials, and accepts iff the two polynomials agree at r. Completeness follows because equivalent ROBPs arithmetize to equal polynomials; soundness uses eqROBP_soundness_bound.

theorem BranchingPrograms.EQ_ROBP_in_BPP {Γ : Type} [DecidableEq Γ] (enc : ROBPPairEncoding Γ) : TuringMachine.InBPP (EQ_ROBP enc)

EQ_ROBP ∈ BPP (Sipser, Lecture 23/24, Read-once Branching Programs). The equivalence problem for read-once branching programs is in BPP: package the polynomial-time random decider produced by eqROBP_random_decider into a PTM via InBPP_of_random_decider.

noncomputable def BranchingPrograms.edgeFactor {m : ℕ} (R : Type u_1) [CommRing R] (i : Fin m) (b : Bool) : MvPolynomial (Fin m) R

The arithmetization "edge factor" for variable i and bit b: returns the multivariate polynomial Xᵢ when b = true and 1 - Xᵢ when b = false. Evaluated at a Boolean point, this factor is 1 iff xᵢ = b.

@[simp]

theorem BranchingPrograms.edgeFactor_true {m : ℕ} {R : Type u_1} [CommRing R] (i : Fin m) : edgeFactor R i true = MvPolynomial.X i

Simp lemma: edgeFactor R i true = Xᵢ.

@[simp]

theorem BranchingPrograms.edgeFactor_false {m : ℕ} {R : Type u_1} [CommRing R] (i : Fin m) : edgeFactor R i false = 1 - MvPolynomial.X i

Simp lemma: edgeFactor R i false = 1 - Xᵢ.

noncomputable def BranchingPrograms.pathMonomial {m : ℕ} (R : Type u_1) [CommRing R] (a : Fin m → Bool) : MvPolynomial (Fin m) R

The monomial associated to a Boolean assignment a : Fin m → Bool: ∏ᵢ edgeFactor R i (a i), i.e. the product ∏ᵢ Xᵢ^{aᵢ} (1 - Xᵢ)^{1 - aᵢ}. Over a Boolean point x, this is the indicator [x = a].

noncomputable def BranchingPrograms.arithmetizeFn {m : ℕ} (R : Type u_1) [CommRing R] (f : (Fin m → Bool) → Bool) : MvPolynomial (Fin m) R

Arithmetization of a Boolean function f : 2^m → 2 as a multilinear polynomial: sum of pathMonomial R a over all assignments a with f a = true. On Boolean inputs this evaluates to 1 iff f a = true.

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

Arithmetization of a branching program bp: the multivariate polynomial representing the Boolean function bp.eval. Two equivalent ROBPs arithmetize to equal polynomials, which is the algebraic core of the EQ_ROBP ∈ BPP proof.

theorem BranchingPrograms.degreeOf_X_le_one' {m : ℕ} {R : Type u_1} [CommRing R] (i j : Fin m) : MvPolynomial.degreeOf j (MvPolynomial.X i) ≤ 1

The degree of any single variable Xⱼ in the monomial Xᵢ is at most 1 (it is 1 when i = j and 0 otherwise).

theorem BranchingPrograms.degreeOf_edgeFactor_le {m : ℕ} {R : Type u_1} [CommRing R] (i j : Fin m) (b : Bool) : MvPolynomial.degreeOf j (edgeFactor R i b) ≤ 1

Every variable appears with degree at most 1 in the edge factor edgeFactor R i b (which is Xᵢ or 1 - Xᵢ).

theorem BranchingPrograms.degreeOf_X_of_ne' {m : ℕ} {R : Type u_1} [CommRing R] (i j : Fin m) (hij : j ≠ i) : MvPolynomial.degreeOf j (MvPolynomial.X i) = 0

A different variable does not appear: degreeOf j Xᵢ = 0 whenever j ≠ i.

theorem BranchingPrograms.degreeOf_edgeFactor_of_ne {m : ℕ} {R : Type u_1} [CommRing R] (i j : Fin m) (b : Bool) (hij : j ≠ i) : MvPolynomial.degreeOf j (edgeFactor R i b) = 0

An unrelated variable does not appear in an edge factor: degreeOf j (edgeFactor R i b) = 0 whenever j ≠ i.

theorem BranchingPrograms.degreeOf_pathMonomial_le {m : ℕ} {R : Type u_1} [CommRing R] (a : Fin m → Bool) (j : Fin m) : MvPolynomial.degreeOf j (pathMonomial R a) ≤ 1

Each path monomial is multilinear: every variable j appears with degree at most 1 in pathMonomial R a.

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

The arithmetization of any branching program is multilinear: each variable appears with degree at most 1 in arithmetize R bp. This is the degree bound that feeds into Schwartz-Zippel for the EQ_ROBP soundness argument.