Freivalds' algorithm

DefinitionFreivalds trial#✓fully proved

Given \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{F}_2 = \mathbb{Z}/2\), stored as arrays of rows, and a seed \(r \in \mathbb{F}_2^n\), the trial computes the column vectors \(Br\), \(A(Br)\) and \(Cr\), each by accumulating matrix products into a zero column, and returns true exactly when \(A(Br) = Cr\). Its cost is the pair (number of scalar multiplications, number of scalar additions), each multiply-add step counting one of each.

The coefficient domain is \(\mathbb{F}_2\) by intentional specialization, not by a restriction in the cited source.

public def freivaldsTrial {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (r : Fin n → ZMod 2) : TimeM (Nat × Nat) Bool := do
  let column := seedColumn r
  let initial := zeroColumn n
  let br ← rectangularMatrixAccumulate B column initial
  let abr ← rectangularMatrixAccumulate A br initial
  let cr ← rectangularMatrixAccumulate C column initial
  pure (decide (abr = cr))

Uses 1 · Used by 20

Statement usesRectangular matrix accumulation

Used byRepeated Freivalds test on fixed seeds · Acceptance of the repeated Freivalds test on fixed seeds · Counting accepted histories of repeated Freivalds trials · Completeness of the repeated Freivalds test on fixed seeds · Acceptance probability of repeated Freivalds trials · Cost of the repeated Freivalds test on fixed seeds · Repeated Freivalds test with no trials · Acceptance via the product discrepancy · Acceptance criterion of the Freivalds trial · Soundness of the Freivalds trial · Completeness of the Freivalds trial · Freivalds trial on empty matrices · Freivalds trial law · Acceptance probability of the Freivalds trial as a seed count · The Freivalds trial accepts a correct product with probability one · The sharp Freivalds example is accepted with probability one half · The Freivalds trial accepts a wrong product with probability at most one half · The sharp Freivalds example accepts exactly the zero seed · The sharp Freivalds example has exactly one accepted seed · Cost of the Freivalds trial

TheoremCost of the Freivalds trial#✓fully proved

For \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{F}_2\) and every seed \(r \in \mathbb{F}_2^n\), the Freivalds trial performs exactly \(3n^2\) scalar multiplications and exactly \(3n^2\) scalar additions.

These counts belong to the same run that returns the acceptance bit and include the additions into the zero-initialized accumulators.

theorem freivaldsTrial_time {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (r : Fin n → ZMod 2) :
    (freivaldsTrial A B C r).time = (3 * n ^ 2, 3 * n ^ 2)

Uses 3 · Used by 2

Statement usesFreivalds trial

Proof usesRectangular matrix accumulation · Operation count of rectangular matrix accumulation

Used byCost of the repeated Freivalds test on fixed seeds · Freivalds trial on empty matrices

DefinitionMatrix of a Freivalds input#✓fully proved

An \(n \times n\) array \(A\) of rows over \(\mathbb{F}_2 = \mathbb{Z}/2\) determines the \(n \times n\) matrix over \(\mathbb{F}_2\) whose \((i, j)\) entry is entry \(j\) of row \(i\) of \(A\).

public def freivaldsMatrix {n : Nat}
    (A : _root_.Vector (_root_.Vector (ZMod 2) n) n) :
    _root_.Matrix (Fin n) (Fin n) (ZMod 2) :=
  _root_.Matrix.of fun i j => (A.get i).get j

Used by 13

Used byThe sharp Freivalds example has a wrong product · Completeness of the repeated Freivalds test on fixed seeds · Repeated Freivalds test on empty matrices · Completeness of repeated Freivalds trials · Soundness of repeated Freivalds trials · Acceptance via the product discrepancy · Acceptance criterion of the Freivalds trial · Soundness of the Freivalds trial · Completeness of the Freivalds trial · Freivalds trial on empty matrices · The Freivalds trial accepts a correct product with probability one · The Freivalds trial accepts a wrong product with probability at most one half · The sharp Freivalds example accepts exactly the zero seed

TheoremAcceptance criterion of the Freivalds trial#✓fully proved

For \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{F}_2\) and every seed \(r \in \mathbb{F}_2^n\), the Freivalds trial on \(A\), \(B\), \(C\), \(r\) returns true if and only if \(A(Br) = Cr\).

theorem freivaldsTrial_accept_iff {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (r : Fin n → ZMod 2) :
    (freivaldsTrial A B C r).ret = true ↔
      (freivaldsMatrix A).mulVec ((freivaldsMatrix B).mulVec r) =
        (freivaldsMatrix C).mulVec r

Uses 4 · Used by 2

Statement usesMatrix of a Freivalds input · Freivalds trial

Proof usesRectangular matrix accumulation · Entries of rectangular matrix accumulation

Used byAcceptance via the product discrepancy · The sharp Freivalds example accepts exactly the zero seed

TheoremAcceptance via the product discrepancy#✓fully proved

For \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{F}_2\) and every seed \(r \in \mathbb{F}_2^n\), the Freivalds trial on \(A\), \(B\), \(C\), \(r\) returns true if and only if \((AB - C)r = 0\).

theorem freivaldsTrial_accept_discrepancy_iff {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (r : Fin n → ZMod 2) :
    (freivaldsTrial A B C r).ret = true ↔
      (freivaldsMatrix A * freivaldsMatrix B - freivaldsMatrix C).mulVec r = 0

Uses 3 · Used by 2

Statement usesMatrix of a Freivalds input · Freivalds trial

Proof usesAcceptance criterion of the Freivalds trial

Used bySoundness of the Freivalds trial · Completeness of the Freivalds trial

TheoremCompleteness of the Freivalds trial#✓fully proved

Let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\mathbb{F}_2\) with \(AB = C\). Then for every seed \(r \in \mathbb{F}_2^n\) the Freivalds trial on \(A\), \(B\), \(C\), \(r\) returns true. This includes the case \(n = 0\).

theorem freivaldsTrial_complete {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (h : freivaldsMatrix A * freivaldsMatrix B = freivaldsMatrix C)
    (r : Fin n → ZMod 2) :
    (freivaldsTrial A B C r).ret = true

Uses 3 · Used by 3

Statement usesMatrix of a Freivalds input · Freivalds trial

Proof usesAcceptance via the product discrepancy

Used byCompleteness of the repeated Freivalds test on fixed seeds · Freivalds trial on empty matrices · The Freivalds trial accepts a correct product with probability one

TheoremFreivalds trial on empty matrices#✓fully proved

For \(0 \times 0\) matrices \(A\), \(B\), \(C\) over \(\mathbb{F}_2\) and the empty seed \(r\), the Freivalds trial returns true at zero cost: it performs no scalar multiplications and no scalar additions.

theorem freivaldsTrial_empty
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) 0) 0)
    (r : Fin 0 → ZMod 2) :
    freivaldsTrial A B C r = pure true

Uses 4

Statement usesFreivalds trial

Proof usesMatrix of a Freivalds input · Completeness of the Freivalds trial · Cost of the Freivalds trial

TheoremSoundness of the Freivalds trial#✓fully proved

Let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\mathbb{F}_2\) with \(AB \ne C\). Then twice the number of seeds \(r \in \mathbb{F}_2^n\) on which the Freivalds trial returns true is at most the number of all seeds in \(\mathbb{F}_2^n\); that is, at most half of the seeds accept.

Acceptance is the return value of the same charged run whose cost is counted.

theorem freivaldsTrial_acceptanceCard_bound {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (wrong : freivaldsMatrix A * freivaldsMatrix B ≠ freivaldsMatrix C) :
    2 * Fintype.card {r : Fin n → ZMod 2 // (freivaldsTrial A B C r).ret = true} ≤
      Fintype.card (Fin n → ZMod 2)

Uses 3 · Used by 1

Statement usesMatrix of a Freivalds input · Freivalds trial

Proof usesAcceptance via the product discrepancy

Used byThe Freivalds trial accepts a wrong product with probability at most one half

DefinitionFreivalds trial law#✓fully proved

For \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\), given as arrays, the Freivalds trial law is the probability distribution on \(\{\mathrm{true}, \mathrm{false}\}\) of the value returned by the Freivalds trial on \(A\), \(B\), \(C\) with seed \(r\), where \(r\) is drawn uniformly from \(\mathbb{F}_2^n\).

The seeds are exactly uniform; no pseudorandom generator or assumed error probability is involved.

noncomputable def freivaldsTrialLaw {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n) : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype (Fin n → ZMod 2)).map
    fun r => (freivaldsTrial A B C r).ret

Uses 1 · Used by 8

Statement usesFreivalds trial

Used byAcceptance probability of repeated Freivalds trials · Completeness of repeated Freivalds trials · Exact acceptance probability of repeated trials on the sharp Freivalds example · Soundness of repeated Freivalds trials · Acceptance probability of the Freivalds trial as a seed count · The Freivalds trial accepts a correct product with probability one · The sharp Freivalds example is accepted with probability one half · The Freivalds trial accepts a wrong product with probability at most one half

TheoremUniform mass of a Freivalds seed#✓fully proved

Let \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\). For every \(n\) and every vector \(r \in \mathbb{F}_2^n\), the uniform probability distribution on \(\mathbb{F}_2^n\) assigns to \(r\) the probability \((2^n)^{-1}\).

theorem freivaldsSeed_pointMass {n : Nat} (r : Fin n → ZMod 2) :
    Cslib.Probability.PMF.uniformOfFintype (Fin n → ZMod 2) r = ((2 : ℝ≥0∞) ^ n)⁻¹

TheoremAcceptance probability of the Freivalds trial as a seed count#✓fully proved

Let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\), given as arrays. The probability that the Freivalds trial law of \(A\), \(B\), \(C\) returns true equals the number of seeds \(r \in \mathbb{F}_2^n\) on which the Freivalds trial on \(A\), \(B\), \(C\) with seed \(r\) accepts, divided by the number \(|\mathbb{F}_2^n|\) of all seeds.

theorem freivaldsTrialLaw_acceptance {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n) :
    freivaldsTrialLaw A B C true =
      (Fintype.card {r : Fin n → ZMod 2 // (freivaldsTrial A B C r).ret = true} : ℝ≥0∞) /
        Fintype.card (Fin n → ZMod 2)

Uses 2 · Used by 4

Statement usesFreivalds trial · Freivalds trial law

Used byAcceptance probability of repeated Freivalds trials · The Freivalds trial accepts a correct product with probability one · The sharp Freivalds example is accepted with probability one half · The Freivalds trial accepts a wrong product with probability at most one half

TheoremThe Freivalds trial accepts a correct product with probability one#✓fully proved

Let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\), given as arrays. If \(AB = C\), then the Freivalds trial law of \(A\), \(B\), \(C\) returns true with probability \(1\). This includes the case \(n = 0\) of empty matrices.

theorem freivaldsTrialLaw_complete {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (correct : freivaldsMatrix A * freivaldsMatrix B = freivaldsMatrix C) :
    freivaldsTrialLaw A B C true = 1

Uses 5 · Used by 1

Statement usesMatrix of a Freivalds input · Freivalds trial law

Proof usesFreivalds trial · Acceptance probability of the Freivalds trial as a seed count · Completeness of the Freivalds trial

Used byCompleteness of repeated Freivalds trials

TheoremThe Freivalds trial accepts a wrong product with probability at most one half#✓fully proved

Let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\mathbb{F}_2 = \mathbb{Z}/2\mathbb{Z}\), given as arrays. If \(AB \ne C\), then the Freivalds trial law of \(A\), \(B\), \(C\) returns true with probability at most \(1/2\).

theorem freivaldsTrialLaw_sound {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (wrong : freivaldsMatrix A * freivaldsMatrix B ≠ freivaldsMatrix C) :
    freivaldsTrialLaw A B C true ≤ (1 / 2 : ℝ≥0∞)

Uses 5 · Used by 1

Statement usesMatrix of a Freivalds input · Freivalds trial law

Proof usesFreivalds trial · Acceptance probability of the Freivalds trial as a seed count · Soundness of the Freivalds trial

Used bySoundness of repeated Freivalds trials

DefinitionRepeated Freivalds test on fixed seeds#✓fully proved

Given \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{Z}/2\) and seeds \(r_0, \dots, r_{k-1} \in (\mathbb{Z}/2)^n\), run the Freivalds trial on \(A\), \(B\), \(C\) with each seed \(r_0, \dots, r_{k-1}\) in order, including the trials after a rejection, and return the conjunction of their results (true when \(k = 0\)). The arithmetic cost of the run is the sum of the costs of the \(k\) trials.

public def freivaldsRepeat {n k : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (history : Fin k → Fin n → ZMod 2) : TimeM (Nat × Nat) Bool :=
  (List.ofFn history).foldlM (repeatStep A B C) true

Uses 1 · Used by 8

Statement usesFreivalds trial

Used byAcceptance of the repeated Freivalds test on fixed seeds · Counting accepted histories of repeated Freivalds trials · Completeness of the repeated Freivalds test on fixed seeds · Repeated Freivalds test on empty matrices · Output distribution of repeated Freivalds trials · Acceptance probability of repeated Freivalds trials · Cost of the repeated Freivalds test on fixed seeds · Repeated Freivalds test with no trials

TheoremCost of the repeated Freivalds test on fixed seeds#✓fully proved

For \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{Z}/2\) and seeds \(r_0, \dots, r_{k-1} \in (\mathbb{Z}/2)^n\), the repeated Freivalds test on these seeds performs exactly \(3kn^2\) scalar multiplications and \(3kn^2\) scalar additions.

theorem freivaldsRepeat_time {n k : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (history : Fin k → Fin n → ZMod 2) :
    (freivaldsRepeat A B C history).time = (3 * k * n ^ 2, 3 * k * n ^ 2)

Uses 3 · Used by 2

Statement usesRepeated Freivalds test on fixed seeds

Proof usesFreivalds trial · Cost of the Freivalds trial

Used byRepeated Freivalds test on empty matrices · Repeated Freivalds test with no trials

TheoremAcceptance of the repeated Freivalds test on fixed seeds#✓fully proved

For \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{Z}/2\) and seeds \(r_0, \dots, r_{k-1} \in (\mathbb{Z}/2)^n\), the repeated Freivalds test on these seeds accepts if and only if, for every \(i < k\), the Freivalds trial on \(A\), \(B\), \(C\) with seed \(r_i\) accepts.

theorem freivaldsRepeat_accept_iff {n k : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (history : Fin k → Fin n → ZMod 2) :
    (freivaldsRepeat A B C history).ret = true ↔
      ∀ i, (freivaldsTrial A B C (history i)).ret = true

Uses 2 · Used by 3

Statement usesRepeated Freivalds test on fixed seeds · Freivalds trial

Used byCounting accepted histories of repeated Freivalds trials · Completeness of the repeated Freivalds test on fixed seeds · Repeated Freivalds test with no trials

TheoremCompleteness of the repeated Freivalds test on fixed seeds#✓fully proved

Let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\mathbb{Z}/2\) with \(AB = C\). Then for every \(k\), including \(k = 0\), and all seeds \(r_0, \dots, r_{k-1} \in (\mathbb{Z}/2)^n\), the repeated Freivalds test on these seeds accepts.

theorem freivaldsRepeat_complete {n k : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (correct : freivaldsMatrix A * freivaldsMatrix B = freivaldsMatrix C)
    (history : Fin k → Fin n → ZMod 2) :
    (freivaldsRepeat A B C history).ret = true

Uses 5 · Used by 1

Statement usesMatrix of a Freivalds input · Repeated Freivalds test on fixed seeds

Proof usesAcceptance of the repeated Freivalds test on fixed seeds · Freivalds trial · Completeness of the Freivalds trial

Used byRepeated Freivalds test on empty matrices

TheoremRepeated Freivalds test with no trials#✓fully proved

For \(n \times n\) matrices \(A\), \(B\), \(C\) over \(\mathbb{Z}/2\), the repeated Freivalds test on the empty list of seeds (\(k = 0\)) accepts and performs no scalar multiplications or additions.

theorem freivaldsRepeat_zero {n : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (history : Fin 0 → Fin n → ZMod 2) :
    freivaldsRepeat A B C history = pure true

Uses 4

Statement usesRepeated Freivalds test on fixed seeds

Proof usesAcceptance of the repeated Freivalds test on fixed seeds · Cost of the repeated Freivalds test on fixed seeds · Freivalds trial

TheoremRepeated Freivalds test on empty matrices#✓fully proved

For \(0 \times 0\) matrices \(A\), \(B\), \(C\) over \(\mathbb{Z}/2\) and any number \(k\) of seeds (each the empty vector), the repeated Freivalds test accepts and performs no scalar multiplications or additions.

theorem freivaldsRepeat_empty {k : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) 0) 0)
    (history : Fin k → Fin 0 → ZMod 2) :
    freivaldsRepeat A B C history = pure true

Uses 4

Statement usesRepeated Freivalds test on fixed seeds

Proof usesMatrix of a Freivalds input · Completeness of the repeated Freivalds test on fixed seeds · Cost of the repeated Freivalds test on fixed seeds

DefinitionOutput distribution of repeated Freivalds trials#✓fully proved

For natural numbers \(n, k\) and \(n \times n\) matrices \(A, B, C\) over \(\mathbb{F}_2\), this is the probability distribution on \(\{\mathrm{true}, \mathrm{false}\}\) of the result returned by the repeated Freivalds executor on \(A, B, C\) when its history of \(k\) seeds is drawn uniformly from \((\mathbb{F}_2^n)^k\).

noncomputable def freivaldsRepeatLaw {n : Nat} (k : Nat)
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n) : PMF Bool :=
  (Cslib.Probability.PMF.uniformOfFintype (Fin k → Fin n → ZMod 2)).map fun history =>
    (freivaldsRepeat A B C history).ret

Uses 1 · Used by 4

Statement usesRepeated Freivalds test on fixed seeds

Used byAcceptance probability of repeated Freivalds trials · Completeness of repeated Freivalds trials · Exact acceptance probability of repeated trials on the sharp Freivalds example · Soundness of repeated Freivalds trials

TheoremUniform mass of a Freivalds seed history#✓fully proved

For all natural numbers \(n\) and \(k\), under the uniform distribution on histories of \(k\) seeds, that is, on \((\mathbb{F}_2^n)^k\), every history has probability exactly \((2^{nk})^{-1}\). This includes the cases \(k = 0\) and \(n = 0\).

theorem freivaldsHistory_pointMass {n k : Nat} (history : Fin k → Fin n → ZMod 2) :
    Cslib.Probability.PMF.uniformOfFintype (Fin k → Fin n → ZMod 2) history =
      ((2 : ℝ≥0∞) ^ (n * k))⁻¹

TheoremCounting accepted histories of repeated Freivalds trials#✓fully proved

Let \(n, k\) be natural numbers and let \(A, B, C\) be \(n \times n\) matrices over \(\mathbb{F}_2\). The number of histories \((r_1, \dots, r_k)\) of seeds \(r_i \in \mathbb{F}_2^n\) on which the repeated Freivalds executor accepts equals \(a^k\), where \(a\) is the number of seeds \(r \in \mathbb{F}_2^n\) on which a single Freivalds trial accepts.

theorem freivaldsRepeat_acceptanceCard {n k : Nat}
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n) :
    Fintype.card {history : Fin k → Fin n → ZMod 2 //
      (freivaldsRepeat A B C history).ret = true} =
      (Fintype.card {r : Fin n → ZMod 2 // (freivaldsTrial A B C r).ret = true}) ^ k

Uses 3 · Used by 1

Statement usesRepeated Freivalds test on fixed seeds · Freivalds trial

Proof usesAcceptance of the repeated Freivalds test on fixed seeds

Used byAcceptance probability of repeated Freivalds trials

TheoremAcceptance probability of repeated Freivalds trials#✓fully proved

Let \(n, k\) be natural numbers and let \(A, B, C\) be \(n \times n\) matrices over \(\mathbb{F}_2\). If the history of \(k\) seeds is drawn uniformly from \((\mathbb{F}_2^n)^k\), the probability that the repeated Freivalds executor accepts is \(p^k\), where \(p\) is the probability that a single Freivalds trial accepts on a seed drawn uniformly from \(\mathbb{F}_2^n\).

theorem freivaldsRepeatLaw_acceptance_power {n : Nat} (k : Nat)
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n) :
    freivaldsRepeatLaw k A B C true = (freivaldsTrialLaw A B C true) ^ k

Uses 6 · Used by 3

Statement usesOutput distribution of repeated Freivalds trials · Freivalds trial law

Proof usesRepeated Freivalds test on fixed seeds · Counting accepted histories of repeated Freivalds trials · Freivalds trial · Acceptance probability of the Freivalds trial as a seed count

Used byCompleteness of repeated Freivalds trials · Exact acceptance probability of repeated trials on the sharp Freivalds example · Soundness of repeated Freivalds trials

TheoremCompleteness of repeated Freivalds trials#✓fully proved

Let \(n, k\) be natural numbers and let \(A, B, C\) be \(n \times n\) matrices over \(\mathbb{F}_2\) with \(AB = C\). If the history of \(k\) seeds is drawn uniformly from \((\mathbb{F}_2^n)^k\), then the repeated Freivalds executor accepts with probability \(1\).

theorem freivaldsRepeatLaw_complete {n : Nat} (k : Nat)
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (correct : freivaldsMatrix A * freivaldsMatrix B = freivaldsMatrix C) :
    freivaldsRepeatLaw k A B C true = 1

Uses 5

Statement usesMatrix of a Freivalds input · Output distribution of repeated Freivalds trials

Proof usesAcceptance probability of repeated Freivalds trials · Freivalds trial law · The Freivalds trial accepts a correct product with probability one

TheoremSoundness of repeated Freivalds trials#✓fully proved

Let \(n, k\) be natural numbers and let \(A, B, C\) be \(n \times n\) matrices over \(\mathbb{F}_2\) with \(AB \ne C\). If the history of \(k\) seeds is drawn uniformly from \((\mathbb{F}_2^n)^k\), then the repeated Freivalds executor accepts with probability at most \((2^k)^{-1}\).

theorem freivaldsRepeatLaw_sound {n : Nat} (k : Nat)
    (A B C : _root_.Vector (_root_.Vector (ZMod 2) n) n)
    (wrong : freivaldsMatrix A * freivaldsMatrix B ≠ freivaldsMatrix C) :
    freivaldsRepeatLaw k A B C true ≤ ((2 : ℝ≥0∞) ^ k)⁻¹

Uses 5

Statement usesMatrix of a Freivalds input · Output distribution of repeated Freivalds trials

Proof usesAcceptance probability of repeated Freivalds trials · Freivalds trial law · The Freivalds trial accepts a wrong product with probability at most one half

TheoremThe sharp Freivalds example has a wrong product#✓fully proved

Let \(A = B = (1)\) and \(C = (0)\) be \(1 \times 1\) matrices over \(\mathbb{Z}/2\mathbb{Z}\). Then \(AB \neq C\).

theorem freivalds_one_wrong :
    freivaldsMatrix
        (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2))) *
      freivaldsMatrix
        (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2))) ≠
      freivaldsMatrix
        (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (0 : ZMod 2)))

Uses 1

Statement usesMatrix of a Freivalds input

TheoremThe sharp Freivalds example accepts exactly the zero seed#✓fully proved

Let \(A = B = (1)\) and \(C = (0)\) be \(1 \times 1\) matrices over \(\mathbb{Z}/2\mathbb{Z}\). For every seed \(r \in (\mathbb{Z}/2\mathbb{Z})^1\), the Freivalds trial on \(A\), \(B\), \(C\) with seed \(r\), which compares \(A(Br)\) with \(Cr\), accepts if and only if the single entry \(r_0\) of \(r\) is \(0\).

theorem freivaldsTrial_one_accept_iff (r : Fin 1 → ZMod 2) :
    (freivaldsTrial
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (0 : ZMod 2))) r).ret = true ↔
        r 0 = 0

Uses 3 · Used by 1

Statement usesFreivalds trial

Proof usesMatrix of a Freivalds input · Acceptance criterion of the Freivalds trial

Used byThe sharp Freivalds example has exactly one accepted seed

TheoremThe sharp Freivalds example has exactly one accepted seed#✓fully proved

Let \(A = B = (1)\) and \(C = (0)\) be \(1 \times 1\) matrices over \(\mathbb{Z}/2\mathbb{Z}\). Exactly one seed \(r \in (\mathbb{Z}/2\mathbb{Z})^1\) is accepted by the Freivalds trial on \(A\), \(B\), \(C\).

theorem freivaldsTrial_one_acceptanceCard :
    Fintype.card {r : Fin 1 → ZMod 2 //
      (freivaldsTrial
        (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
        (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
        (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (0 : ZMod 2))) r).ret = true} =
      1

Uses 2 · Used by 1

Statement usesFreivalds trial

Proof usesThe sharp Freivalds example accepts exactly the zero seed

Used byThe sharp Freivalds example is accepted with probability one half

TheoremThe sharp Freivalds example is accepted with probability one half#✓fully proved

Let \(A = B = (1)\) and \(C = (0)\) be \(1 \times 1\) matrices over \(\mathbb{Z}/2\mathbb{Z}\). When the seed is drawn uniformly from \((\mathbb{Z}/2\mathbb{Z})^1\), the Freivalds trial on \(A\), \(B\), \(C\) accepts with probability exactly \(1/2\).

Since \(AB \neq C\), this shows that the bound \(1/2\) on the probability that one trial accepts a wrong product cannot be improved.

theorem freivaldsTrialLaw_one_sharp :
    freivaldsTrialLaw
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (0 : ZMod 2))) true =
        (1 : ℝ≥0∞) / 2

Uses 4 · Used by 1

Statement usesFreivalds trial law

Proof usesFreivalds trial · Acceptance probability of the Freivalds trial as a seed count · The sharp Freivalds example has exactly one accepted seed

Used byExact acceptance probability of repeated trials on the sharp Freivalds example

TheoremExact acceptance probability of repeated trials on the sharp Freivalds example#✓fully proved

Let \(A = B = (1)\) and \(C = (0)\) be \(1 \times 1\) matrices over \(\mathbb{Z}/2\mathbb{Z}\), and let \(k\) be a natural number. Run \(k\) Freivalds trials on \(A\), \(B\), \(C\) with seeds drawn independently and uniformly from \((\mathbb{Z}/2\mathbb{Z})^1\), accepting exactly when every trial accepts. Then the run accepts with probability exactly \(2^{-k}\).

Since \(AB \neq C\), the bound \(2^{-k}\) on the probability that \(k\) trials accept a wrong product cannot be improved.

theorem freivaldsRepeatLaw_one_sharp (k : Nat) :
    freivaldsRepeatLaw k
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (1 : ZMod 2)))
      (_root_.Vector.replicate 1 (_root_.Vector.replicate 1 (0 : ZMod 2))) true =
        ((2 : ℝ≥0∞) ^ k)⁻¹

Uses 4

Statement usesOutput distribution of repeated Freivalds trials

Proof usesAcceptance probability of repeated Freivalds trials · Freivalds trial law · The sharp Freivalds example is accepted with probability one half

30 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.