feat(abstracts): propose a Chor–Goldreich formal abstract and catalogue entry (#895)

abstracts/ComplexityAbstracts.lean

@@ -1,6 +1,8 @@
 import ComplexityAbstracts.BarringtonAbstract
 import ComplexityAbstracts.BarringtonBridge
 import ComplexityAbstracts.Check
+import ComplexityAbstracts.ChorGoldreichAbstract
+import ComplexityAbstracts.ChorGoldreichBridge
 import ComplexityAbstracts.CommunicationAbstract
 import ComplexityAbstracts.CommunicationBridge
 import ComplexityAbstracts.Computation

abstracts/ComplexityAbstracts/ChorGoldreichAbstract.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract library)
+
+import ComplexityAbstracts.ChorGoldreichBridge
+
+/-! # Chor–Goldreich: the inner product extracts a random bit from two weak sources
+
+A weak random source is a distribution on `n`-bit strings in which no outcome is very likely: a
+`k`-source gives every string probability at most `2 ^ (-k)`, so it has min-entropy at least `k`.
+No fixed function extracts a fair bit from every such source when `k ≤ n - 1`. Two independent
+sources suffice: if their min-entropies `k₁` and `k₂` add up to more than `n`, then the inner
+product modulo two of independent samples is nearly a fair coin, with bias at most
+`2 ^ ((n - k₁ - k₂) / 2) / 2`. The bound holds even on average after the second sample is
+revealed. The threshold is sharp: strings supported on complementary sets of positions have
+min-entropies adding up to exactly `n` and are always orthogonal.
+
+A reader only needs to inspect the definitions and theorem statements in this file to verify that
+they state the intended claims. Lean checks the proofs through `ChorGoldreichBridge`, and
+`#check_abstract` audits that every statement depends only on this file and background libraries.
+Probabilities are those of Mathlib's discrete distributions `PMF`, read as real numbers with
+`toReal`; the experiments are written in `do` notation, sampling independently in sequence.
+
+## References
+
+* [B. Chor and O. Goldreich, *Unbiased bits from sources of weak randomness and probabilistic
+  communication complexity*, Theorem 9][ChorGoldreich1988]
+* [S. Vadhan, *Pseudorandomness*, Chapter 6][Vadhan2012]
+-/
+
+namespace ComplexityAbstracts.ChorGoldreichAbstract
+
+/-- A bit string is a function assigning a Boolean to each of `n` positions. -/
+abbrev BitString (n : ℕ) := Fin n → Bool
+
+/-- A **`k`-source**: a distribution on bit strings in which every string has probability at most
+`2 ^ (-k)`, that is, of min-entropy at least `k`. The exponent `k` is a real number. -/
+def IsSource {n : ℕ} (p : PMF (BitString n)) (k : ℝ) : Prop :=
+  ∀ x, (p x).toReal ≤ 2 ^ (-k)
+
+/-- The inner product modulo two: true when an odd number of positions are true in both
+inputs. The sum below uses Boolean multiplication (AND) and addition (XOR). -/
+def innerProduct {n : ℕ} (x y : BitString n) : Bool := ∑ i, x i * y i
+
+/-- **Chor–Goldreich.** For independent samples of a `k₁`-source and a `k₂`-source of `n`-bit
+strings, the probability that their inner product is true differs from one half by at most
+`2 ^ ((n - k₁ - k₂) / 2) / 2`. This is the statistical distance of the inner product from a fair
+bit. -/
+theorem chor_goldreich {n : ℕ} {k₁ k₂ : ℝ} (p q : PMF (BitString n)) (hp : IsSource p k₁)
+    (hq : IsSource q k₂) :
+    |((do
+        let x ← p
+        let y ← q
+        return innerProduct x y) true).toReal - 1 / 2| ≤
+      2 ^ ((n - k₁ - k₂) / 2) / 2 :=
+  ChorGoldreichBridge.chorGoldreich p q hp hq
+
+/-- **Chor–Goldreich, strong form.** The same bound holds on average over the second sample `y`:
+the probability over the first source that the inner product with `y` is true differs from one
+half by at most `2 ^ ((n - k₁ - k₂) / 2) / 2` on average. Equivalently, the second sample paired
+with the inner product is that close to the second sample paired with a fair bit. -/
+theorem chor_goldreich_strong {n : ℕ} {k₁ k₂ : ℝ} (p q : PMF (BitString n))
+    (hp : IsSource p k₁) (hq : IsSource q k₂) :
+    ∑ y, (q y).toReal * |((do
+        let x ← p
+        return innerProduct x y) true).toReal - 1 / 2| ≤
+      2 ^ ((n - k₁ - k₂) / 2) / 2 :=
+  ChorGoldreichBridge.chorGoldreich_strong p q hp hq
+
+/-- **The threshold is sharp.** For every set `S` of positions, there are an `|S|`-source and an
+`(n - |S|)`-source whose independent samples have inner product true with probability zero:
+strings vanishing outside `S` are orthogonal to strings vanishing on `S`. -/
+theorem orthogonal_sources {n : ℕ} (S : Finset (Fin n)) :
+    ∃ p q : PMF (BitString n), IsSource p S.card ∧ IsSource q (n - S.card) ∧
+      ((do
+        let x ← p
+        let y ← q
+        return innerProduct x y) true).toReal = 0 :=
+  ChorGoldreichBridge.orthogonal_sources S
+
+/--
+info: 'ComplexityAbstracts.ChorGoldreichAbstract.chor_goldreich' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms chor_goldreich
+
+/--
+info: 'ComplexityAbstracts.ChorGoldreichAbstract.chor_goldreich_strong' depends on axioms:
+[propext, Classical.choice, Quot.sound]
+-/
+#guard_msgs (whitespace := lax) in
+#print axioms chor_goldreich_strong
+
+/--
+info: abstract audit passed for `ComplexityAbstracts.ChorGoldreichAbstract`: 7 root
+declarations, 73 dependencies checked
+-/
+#guard_msgs (whitespace := lax) in
+#check_abstract ComplexityAbstracts.ChorGoldreichAbstract
+
+end ComplexityAbstracts.ChorGoldreichAbstract

abstracts/ComplexityAbstracts/ChorGoldreichBridge.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: local-only (formal abstract library)
+
+import ComplexityAbstracts.Check
+import Complexity.Probability.Extractor.TwoSource
+
+/-! # Transfer of the Chor–Goldreich theorem to explicit probabilities
+
+The abstract states min-entropy as a bound on every outcome probability and statistical distance
+from a uniform bit as `|Pr[true] - 1 / 2|`. This bridge converts both to the library's
+`PMF.minEntropy` and statistical distance.
+-/
+
+namespace ComplexityAbstracts.ChorGoldreichBridge
+
+open Cslib Cslib.Probability Cslib.Probability.PMF
+
+/-- The probability that a computed bit is `true`, minus one half, is half its bias. -/
+private theorem abs_map_true_sub_half {α : Type} [Fintype α] (p : PMF α) (f : α → Bool) :
+    |((p.map f) true).toReal - 1 / 2| = |∑ a, (p a).toReal * BitString.signVal (f a)| / 2 := by
+  rw [← dist_uniformOfFintype_bool, dist_map_uniformOfFintype_bool]
+
+private theorem do_eq_bind {n : ℕ} (p q : PMF (Fin n → Bool)) :
+    (do
+        let x ← p
+        let y ← q
+        return ∑ i, x i * y i : PMF Bool) =
+      p.bind fun x => q.map fun y => x ⬝ᵥ y := by
+  simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure]
+  rfl
+
+theorem chorGoldreich {n : ℕ} {k₁ k₂ : ℝ} (p q : PMF (Fin n → Bool))
+    (hp : ∀ x, (p x).toReal ≤ 2 ^ (-k₁)) (hq : ∀ y, (q y).toReal ≤ 2 ^ (-k₂)) :
+    |((do
+        let x ← p
+        let y ← q
+        return ∑ i, x i * y i : PMF Bool) true).toReal - 1 / 2| ≤
+      2 ^ ((n - k₁ - k₂) / 2) / 2 := by
+  have h := isTwoSourceExtractor_dotProduct (ι := Fin n) k₁ k₂ p q
+    ((le_minEntropy_iff p).mpr hp) ((le_minEntropy_iff q).mpr hq)
+  rw [dist_uniformOfFintype_bool, Fintype.card_fin] at h
+  rwa [do_eq_bind]
+
+theorem chorGoldreich_strong {n : ℕ} {k₁ k₂ : ℝ} (p q : PMF (Fin n → Bool))
+    (hp : ∀ x, (p x).toReal ≤ 2 ^ (-k₁)) (hq : ∀ y, (q y).toReal ≤ 2 ^ (-k₂)) :
+    ∑ y, (q y).toReal * |((do
+        let x ← p
+        return ∑ i, x i * y i : PMF Bool) true).toReal - 1 / 2| ≤
+      2 ^ ((n - k₁ - k₂) / 2) / 2 := by
+  have h := sum_mul_abs_bias_dotProduct_le (ι := Fin n)
+    ((le_minEntropy_iff p).mpr hp) ((le_minEntropy_iff q).mpr hq)
+  rw [Fintype.card_fin] at h
+  have hmap (y : Fin n → Bool) : (do
+        let x ← p
+        return ∑ i, x i * y i : PMF Bool) = p.map fun x => x ⬝ᵥ y := by
+    simp only [PMF.monad_bind_eq_bind, PMF.monad_pure_eq_pure]
+    rfl
+  simp only [hmap, abs_map_true_sub_half, mul_div_assoc', ← Finset.sum_div]
+  gcongr
+
+theorem orthogonal_sources {n : ℕ} (S : Finset (Fin n)) :
+    ∃ p q : PMF (Fin n → Bool),
+      (∀ x, (p x).toReal ≤ 2 ^ (-(S.card : ℝ))) ∧
+      (∀ y, (q y).toReal ≤ 2 ^ (-((n : ℝ) - S.card))) ∧
+      ((do
+        let x ← p
+        let y ← q
+        return ∑ i, x i * y i : PMF Bool) true).toReal = 0 := by
+  obtain ⟨p, q, hp, hq, hconst⟩ := exists_minEntropy_bind_dotProduct_eq_pure S
+  refine ⟨p, q, (le_minEntropy_iff p).mp hp.ge, (le_minEntropy_iff q).mp ?_, ?_⟩
+  · rw [hq, Finset.card_compl, Fintype.card_fin, Nat.cast_sub (S.card_le_univ.trans_eq
+      (Fintype.card_fin n))]
+  · rw [do_eq_bind, hconst]
+    simp
+
+end ComplexityAbstracts.ChorGoldreichBridge

abstracts/catalogue.json

@@ -197,6 +197,20 @@
       ],
       "summary": "Bounded-error randomized polynomial time admits both existential–universal and universal–existential polynomial descriptions.",
       "scope": "Bit-string languages, fair independent random bits, correctness at least two thirds on every input, and total native polynomial-time tests; no derandomization assumption."
+    },
+    {
+      "id": "chor-goldreich",
+      "title": "Chor–Goldreich: the inner product extracts from two weak sources",
+      "module": "ComplexityAbstracts.ChorGoldreichAbstract",
+      "headline_theorems": [
+        "ComplexityAbstracts.ChorGoldreichAbstract.chor_goldreich",
+        "ComplexityAbstracts.ChorGoldreichAbstract.chor_goldreich_strong"
+      ],
+      "supporting_theorems": [
+        "ComplexityAbstracts.ChorGoldreichAbstract.orthogonal_sources"
+      ],
+      "summary": "Two independent weak random sources whose min-entropies add up to more than the string length give a nearly fair bit through the inner product modulo two.",
+      "scope": "Arbitrary sources with real min-entropy bounds, the exact bias bound 2^((n - k1 - k2)/2)/2 and its strong form, and sharpness at k1 + k2 = n; information-theoretic, with no running time asserted."
     }
   ]
 }