diff --git a/ComplexityTests.lean b/ComplexityTests.lean index 6026c26181..5dc9531506 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -2,7 +2,9 @@ import ComplexityTests.AWPPAmplification import ComplexityTests.AWPPLowness import ComplexityTests.Abstracts.All import ComplexityTests.Abstracts.CheckTests +import ComplexityTests.Abstracts.CommunicationTests import ComplexityTests.Abstracts.InputLayouts +import ComplexityTests.Abstracts.SipserLautemannTests import ComplexityTests.AdaptivePPT import ComplexityTests.Advice import ComplexityTests.AffineController diff --git a/ComplexityTests/Abstracts/CommunicationTests.lean b/ComplexityTests/Abstracts/CommunicationTests.lean new file mode 100644 index 0000000000..1a72a79b97 --- /dev/null +++ b/ComplexityTests/Abstracts/CommunicationTests.lean @@ -0,0 +1,57 @@ +/- +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 tests) + +import ComplexityAbstracts.CommunicationAbstract + +/-! # Concrete clients of the communication abstract + +Check that its cost/error conditions admit actual protocols and that its finite disjointness +bound excludes a small communication budget. +-/ + +namespace ComplexityTests.Abstracts.CommunicationTests + +open ComplexityAbstracts.CommunicationAbstract + +/-- Alice sends her bit, and Bob sends the equality verdict. -/ +def oneBitEquality : Protocol 1 := + .alice (fun x => x 0) + (.bob (fun y => !y 0) (.output false) (.output true)) + (.bob (fun y => y 0) (.output false) (.output true)) + +example : cost oneBitEquality = 2 := rfl + +example : ∀ x y, answer oneBitEquality x y = decide (x = y) := by decide + +example : (∃ p : Protocol 1, + (∀ x y, answer p x y = decide (x = y)) ∧ cost p ≤ 1) ↔ False := by + rw [equality (by decide)] + decide + +-- On zero positions, disjointness is true and the inner product is false. +example (x y : Input 0) : disjoint x y = true ∧ innerProduct x y = false := by + simp [disjoint, innerProduct, Bool.zero_eq_false] + +/-- A point mass on an explicit correct tree meets both public conditions. -/ +example : CostAtMost (PMF.pure oneBitEquality) 2 ∧ + ErrorAtMost (PMF.pure oneBitEquality) (fun x y => decide (x = y)) 0 := by + constructor + · intro p hp + rw [(PMF.mem_support_pure_iff _ _).mp hp] + exact le_rfl + · intro x y + have h : answer oneBitEquality x y = decide (x = y) := by decide +revert + simp [PMF.toOuterMeasure_pure_apply, h] + +-- This finite consequence is nontrivial despite the large disjointness constants. +example (μ : RandomizedProtocol (2 ^ 20)) (hc : CostAtMost μ 15) + (he : ErrorAtMost μ disjoint (1 / 3)) : False := by + have h := disjointness_lower_bound μ hc he + norm_num at h + +end ComplexityTests.Abstracts.CommunicationTests diff --git a/ComplexityTests/Abstracts/SipserLautemannTests.lean b/ComplexityTests/Abstracts/SipserLautemannTests.lean new file mode 100644 index 0000000000..9e66916bf4 --- /dev/null +++ b/ComplexityTests/Abstracts/SipserLautemannTests.lean @@ -0,0 +1,73 @@ +/- +Copyright (c) 2026 Bolton Bailey, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey, Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract tests) + +import ComplexityAbstracts.SipserLautemannAbstract +import ComplexityTests.SipserLautemann + +/-! # Concrete clients of the public Sipser–Lautemann abstract + +The head-bit language has both yes- and no-instances. A two-bit randomized test has error +exactly one quarter on each input; its native polynomial-time certificate witnesses the public +BPP definition, and the public containment supplies both alternating descriptions. A deterministic +version also checks the boundary convention that zero random bits means one possible seed. +-/ + +namespace ComplexityTests.Abstracts.SipserLautemannTests + +open ComplexityAbstracts.SipserLautemannAbstract +open Cslib.Complexity.Tests.SipserLautemann + (noisyHeadVerifier noisyHeadVerifier_polyTime noisyHeadVerifier_decides) + +/-- The language of strings whose first bit is true; the empty string is rejected. -/ +def HeadLanguage : Set (List Bool) := {x | x.headD false = true} + +example : [true] ∈ HeadLanguage := rfl +example : [] ∉ HeadLanguage := by + change ¬ false = true + decide + +/-- Exactly one of the four fair two-bit seeds flips the answer, for either answer. -/ +example (x : List Bool) : + (Finset.univ.filter fun r : Fin 2 → Bool => + noisyHeadVerifier (x, List.ofFn r) ≠ x.headD false).card = 1 := by + cases h : x.headD false <;> simp only [noisyHeadVerifier, h] <;> decide + +/-- The existing total two-bit test satisfies the public native-machine predicate. -/ +theorem noisyHead_polyTime : PolyTimePredicate noisyHeadVerifier := + CookLevinBridge.computableInPolyTime_iff_tidy.mpr noisyHeadVerifier_polyTime + +/-- A genuinely randomized witness for the public BPP definition, on a nonconstant language. -/ +theorem head_mem_BPP : HeadLanguage ∈ BPP := by + refine ⟨Polynomial.C 2, noisyHeadVerifier, noisyHead_polyTime, ?_⟩ + exact noisyHeadVerifier_decides + +/-- Both alternating descriptions follow from the abstract's public theorem. -/ +example : HeadLanguage ∈ SigmaTwo ∩ PiTwo := sipserLautemann head_mem_BPP + +/-- A deterministic test of the same nonconstant language. -/ +def headVerifier (z : List Bool × List Bool) : Bool := z.1.headD false + +private theorem headVerifier_polyTime : PolyTimePredicate headVerifier := by + apply CookLevinBridge.computableInPolyTime_iff_tidy.mpr + change Turing.MultiTapeTM.ComputableTidilyInPolyTime headVerifier + (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encBits Turing.MultiTapeTM.encBits) + Turing.MultiTapeTM.encBool + unfold headVerifier + fun_prop + +-- There is exactly one random seed of length zero, rather than no seeds. +example : Fintype.card (Fin 0 → Bool) = 1 := by decide + +/-- Zero random bits also give a valid public BPP witness: the unique empty seed is correct. -/ +example : HeadLanguage ∈ BPP := by + refine ⟨0, headVerifier, headVerifier_polyTime, ?_⟩ + intro x + cases h : x.headD false <;> + simp only [HeadLanguage, Set.mem_ofPred_eq, headVerifier, Polynomial.eval_zero, h] <;> simp + +end ComplexityTests.Abstracts.SipserLautemannTests diff --git a/README.md b/README.md index 0bb026d2c8..96c5095df5 100644 --- a/README.md +++ b/README.md @@ -57,6 +57,8 @@ the selection is not an exhaustive API reference. * [Formula lower bounds: parity and Andreev](abstracts/ComplexityAbstracts/FormulaBoundsAbstract.lean): Tree-shaped computation pays for repeated work: parity requires quadratic leaf size, and Andreev gives a stronger explicit bound. * [One-way functions yield pseudorandom generators and adaptive functions](abstracts/ComplexityAbstracts/CryptographyAbstract.lean): One-wayness yields pseudorandomness, from an extra output bit to functions secure against adaptive oracle queries. * [Haken: pigeonhole formulas require long resolution proofs](abstracts/ComplexityAbstracts/ResolutionAbstract.lean): The pigeonhole principle has short CNF statements but requires exponentially many resolution lines. +* [Communication: disjointness and inner product resist randomness](abstracts/ComplexityAbstracts/CommunicationAbstract.lean): Both problems require linearly many communicated bits even with shared randomness and bounded error. +* [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](abstracts/ComplexityAbstracts/SipserLautemannAbstract.lean): Bounded-error polynomial time admits both existential–universal and universal–existential polynomial descriptions. ## Build and use diff --git a/abstracts/ComplexityAbstracts.lean b/abstracts/ComplexityAbstracts.lean index c860060203..2420fb9883 100644 --- a/abstracts/ComplexityAbstracts.lean +++ b/abstracts/ComplexityAbstracts.lean @@ -1,6 +1,8 @@ import ComplexityAbstracts.BarringtonAbstract import ComplexityAbstracts.BarringtonBridge import ComplexityAbstracts.Check +import ComplexityAbstracts.CommunicationAbstract +import ComplexityAbstracts.CommunicationBridge import ComplexityAbstracts.Computation import ComplexityAbstracts.ConstantDepthAbstract import ComplexityAbstracts.ConstantDepthBridge @@ -23,6 +25,8 @@ import ComplexityAbstracts.SavitchAbstract import ComplexityAbstracts.SavitchBridge import ComplexityAbstracts.ShamirAbstract import ComplexityAbstracts.ShamirBridge +import ComplexityAbstracts.SipserLautemannAbstract +import ComplexityAbstracts.SipserLautemannBridge import ComplexityAbstracts.SubsetSumAbstract import ComplexityAbstracts.SubsetSumBridge import ComplexityAbstracts.TQBFAbstract diff --git a/abstracts/ComplexityAbstracts/CommunicationAbstract.lean b/abstracts/ComplexityAbstracts/CommunicationAbstract.lean new file mode 100644 index 0000000000..90b816cce0 --- /dev/null +++ b/abstracts/ComplexityAbstracts/CommunicationAbstract.lean @@ -0,0 +1,117 @@ +/- +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.CommunicationBridge + +/-! # Communication: randomness cannot eliminate the need to exchange information + +Alice and Bob each hold an `n`-bit string and exchange bits to compute a joint answer. +Disjointness and parity of the intersection both require linearly many communicated bits, +even with shared randomness and error at most one third on every input pair. + +Local computation is free. Cost is the worst case over inputs and coins; protocols may be +chosen separately at each input length. Both players learn the answer, so exact deterministic +equality costs `n + 1` bits for `n > 0`: Alice sends her input and Bob replies with the answer. + +The only allowlisted model is the binary protocol tree described below. Cost and per-input +error are defined here. Lean checks the bridge proofs; `#check_abstract` audits their statement +dependencies. The disjointness constants are not optimized. + +## References + +* [B. Kalyanasundaram, G. Schnitger, *The probabilistic communication complexity of set + intersection*][KalyanasundaramSchnitger1992] +* [A. Razborov, *On the distributional complexity of disjointness*][Razborov1992] +* [E. Kushilevitz, N. Nisan, *Communication Complexity*, Chapters 1–4][KushilevitzNisan1997] +-/ + +namespace ComplexityAbstracts.CommunicationAbstract + +/-- A bit string is a function assigning a Boolean to each of `n` positions. -/ +abbrev Input (n : ℕ) := Fin n → Bool + +/-- A finite binary tree: `output b` is a leaf announcing `b`; `alice send p₀ p₁` branches +on the bit `send x` of Alice's input, and `bob` branches on Bob's input. The transcript +determines the current node, so messages may depend on all earlier messages. -/ +abbrev Protocol (n : ℕ) := Cslib.Communication.Protocol (Input n) (Input n) Bool + +/-- Follow the sent bits from the root to a leaf and return its announced answer. -/ +def answer {n : ℕ} (p : Protocol n) (x y : Input n) : Bool := p.run x y + +/-- Tree depth: leaves cost zero, and sending one bit costs one plus the larger branch cost. -/ +def cost {n : ℕ} (p : Protocol n) : ℕ := p.depth + +/-- Shared randomness selects a deterministic tree independently of the inputs. +`PMF` is a probability distribution with total mass one. -/ +abbrev RandomizedProtocol (n : ℕ) := PMF (Protocol n) + +/-- Every tree with positive probability has depth at most `c`, bounding all its branches. -/ +def CostAtMost {n : ℕ} (μ : RandomizedProtocol n) (c : ℕ) : Prop := + ∀ p ∈ μ.support, cost p ≤ c + +/-- On each input pair separately, the probability of a wrong answer is at most `ε`. +The measure sums the probabilities of trees giving a wrong answer; `toReal` returns a real. -/ +def ErrorAtMost {n : ℕ} (μ : RandomizedProtocol n) + (f : Input n → Input n → Bool) (ε : ℝ) : Prop := + ∀ x y, (μ.toOuterMeasure {p | answer p x y ≠ f x y}).toReal ≤ ε + +/-- The sets of true positions are disjoint exactly when no position is true in both inputs. -/ +def disjoint {n : ℕ} (x y : Input n) : Bool := + decide (∀ i, (x i && y i) = false) + +/-- 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 : Input n) : Bool := ∑ i, x i * y i + +/-- **Exact equality.** A deterministic protocol deciding equality within `c` bits exists +exactly when `n + 1 ≤ c`, for positive input length. At length zero, the constant true +answer costs no communication. -/ +theorem equality {n c : ℕ} (hn : 0 < n) : + (∃ p : Protocol n, (∀ x y, answer p x y = decide (x = y)) ∧ cost p ≤ c) ↔ n + 1 ≤ c := + CommunicationBridge.equality hn + +/-- **Kalyanasundaram–Schnitger / Razborov.** Even with shared randomness and error at most +one third, disjointness needs linear communication: `n ≤ 65536*c + 4096`. +The proof uses Razborov's corruption method, with a variant of his hard distribution. -/ +theorem disjointness_lower_bound {n c : ℕ} (μ : RandomizedProtocol n) + (hc : CostAtMost μ c) (he : ErrorAtMost μ disjoint (1 / 3)) : + n ≤ 2 ^ 16 * c + 2 ^ 12 := + CommunicationBridge.disjointness μ hc he + +/-- **Inner product.** Even with shared randomness and error at most one third, +computing parity of the intersection requires `n ≤ 2*c + 3`. The proof bounds the +discrepancy of the inner-product sign matrix using its orthogonal rows. -/ +theorem innerProduct_lower_bound {n c : ℕ} (μ : RandomizedProtocol n) + (hc : CostAtMost μ c) (he : ErrorAtMost μ innerProduct (1 / 3)) : + n ≤ 2 * c + 3 := + CommunicationBridge.innerProduct μ hc he + +/-- +info: 'ComplexityAbstracts.CommunicationAbstract.disjointness_lower_bound' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms disjointness_lower_bound + +/-- +info: 'ComplexityAbstracts.CommunicationAbstract.innerProduct_lower_bound' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms innerProduct_lower_bound + +/-- +info: abstract audit passed for `ComplexityAbstracts.CommunicationAbstract`: 12 root +declarations, 95 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityAbstracts.CommunicationAbstract allowing [ + Complexity.Computability.Communication.Protocol +] + +end ComplexityAbstracts.CommunicationAbstract diff --git a/abstracts/ComplexityAbstracts/CommunicationBridge.lean b/abstracts/ComplexityAbstracts/CommunicationBridge.lean new file mode 100644 index 0000000000..6caa82a034 --- /dev/null +++ b/abstracts/ComplexityAbstracts/CommunicationBridge.lean @@ -0,0 +1,72 @@ +/- +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.Computability.Communication.Disjointness +import Complexity.Computability.Communication.Discrepancy + +/-! # Transfer of communication lower bounds to individual protocols + +The abstract uses the elementary deterministic protocol tree, but defines its own worst-case +cost and per-input error conditions. No communication-complexity infimum occurs in its statements. +-/ + +namespace ComplexityAbstracts.CommunicationBridge + +open Cslib.Communication + +theorem equality {n c : ℕ} (hn : 0 < n) : + (∃ p : Protocol (Fin n → Bool) (Fin n → Bool) Bool, + (∀ x y, p.run x y = decide (x = y)) ∧ p.depth ≤ c) ↔ n + 1 ≤ c := by + have h := Protocol.ecomplexityFun_le_iff + (f := fun x y : Fin n → Bool => decide (x = y)) (k := c) + rw [show Protocol.ecomplexityFun (fun x y : Fin n → Bool => decide (x = y)) = n + 1 from + ecomplexity_equality hn] at h + norm_cast at h + simpa only [funext_iff] using h.symm + +/-- Convert the public cost and error conditions to the library's infimum bound. -/ +theorem complexity_le {n c : ℕ} + (μ : PMF (Protocol (Fin n → Bool) (Fin n → Bool) Bool)) + (f : (Fin n → Bool) → (Fin n → Bool) → Bool) + (hc : ∀ p ∈ μ.support, p.depth ≤ c) + (he : ∀ x y, (μ.toOuterMeasure {p | p.run x y ≠ f x y}).toReal ≤ (1 : ℝ) / 3) : + PublicCoin.ecomplexityFun (1 / 3) f ≤ c := by + apply (PublicCoin.ecomplexity_le_depth (μ := μ) ?_).trans + (PublicCoin.depth_le_iff.mpr fun p hp => by exact_mod_cast hc p hp) + intro x _ y _ + simpa only [PublicCoin.errorProb, ne_comm] using he x y + +theorem disjointness {n c : ℕ} + (μ : PMF (Protocol (Fin n → Bool) (Fin n → Bool) Bool)) + (hc : ∀ p ∈ μ.support, p.depth ≤ c) + (he : ∀ x y, (μ.toOuterMeasure + {p | p.run x y ≠ decide (∀ i, (x i && y i) = false)}).toReal ≤ (1 : ℝ) / 3) : + n ≤ 2 ^ 16 * c + 2 ^ 12 := by + have h := PublicCoin.le_mul_ecomplexityFun_disjointness_add n + have hf : Cslib.Communication.disjointness = + (fun x y : Fin n → Bool => decide (∀ i, (x i && y i) = false)) := by + funext x y + simp only [Cslib.Communication.disjointness, decide_eq_decide] + rw [hf] at h + have hcost := complexity_le μ _ hc he + have hbound : (n : ℕ∞) ≤ 2 ^ 16 * (c : ℕ∞) + 2 ^ 12 := + h.trans (by gcongr) + exact_mod_cast hbound + +theorem innerProduct {n c : ℕ} + (μ : PMF (Protocol (Fin n → Bool) (Fin n → Bool) Bool)) + (hc : ∀ p ∈ μ.support, p.depth ≤ c) + (he : ∀ x y, (μ.toOuterMeasure {p | p.run x y ≠ x ⬝ᵥ y}).toReal ≤ (1 : ℝ) / 3) : + n ≤ 2 * c + 3 := by + have h := PublicCoin.le_two_mul_ecomplexityFun_dotProduct_add_three n + have hcost := complexity_le μ (fun x y => x ⬝ᵥ y) hc he + have hbound : (n : ℕ∞) ≤ 2 * (c : ℕ∞) + 3 := h.trans (by gcongr) + exact_mod_cast hbound + +end ComplexityAbstracts.CommunicationBridge diff --git a/abstracts/ComplexityAbstracts/SipserLautemannAbstract.lean b/abstracts/ComplexityAbstracts/SipserLautemannAbstract.lean new file mode 100644 index 0000000000..686b7cf0c5 --- /dev/null +++ b/abstracts/ComplexityAbstracts/SipserLautemannAbstract.lean @@ -0,0 +1,114 @@ +/- +Copyright (c) 2026 Bolton Bailey, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey, Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract library) + +import ComplexityAbstracts.Check +import ComplexityAbstracts.SipserLautemannBridge + +/-! # Sipser–Lautemann: bounded-error randomness lies in the second polynomial level + +Every bounded-error randomized polynomial-time language admits both existential–universal +and universal–existential descriptions by polynomially long binary blocks and a deterministic +polynomial-time test: BPP ⊆ Σ₂ ∩ Π₂. + +Lautemann's proof amplifies the randomized algorithm. For a yes-instance, polynomially many +xor shifts of its accepting seeds cover every seed; for a no-instance, no such cover exists. +Guessing the shifts and checking every seed yields the existential–universal description. +Complement closure yields the reverse order. + +Lean checks the proof bridge and audits the abstract's statement dependencies. + +## References + +* [M. Sipser, *A complexity theoretic approach to randomness*][Sipser1983]. +* [C. Lautemann, *BPP and the polynomial hierarchy*][Lautemann1983]. +* [S. Arora, B. Barak, *Computational Complexity: A Modern Approach*][AroraBarak09], Theorem 7.15. +-/ + +namespace ComplexityAbstracts.SipserLautemannAbstract + +/-! ## Bit strings and deterministic polynomial-time tests + +Inputs are bit strings. A test reads an instance `x` and a second string `w` of random bits +or certificates. Encode the pair by framing each bit `b` of `x` as `[true, b]`, terminating +with `[false]`, then appending `w`. The separator preserves the boundary. + +-/ + +/-- Encode a pair `(x, w)` by the self-delimiting frame of `x`, followed by `w`. -/ +def encodeInput (z : List Bool × List Bool) : List Bool := + z.1.flatMap (fun b => [true, b]) ++ [false] ++ z.2 + +theorem encodeInput_injective : Function.Injective encodeInput := + SipserLautemannBridge.encInput.injective + +/-- Injective binary encoding of the two input strings. -/ +def encInput : (List Bool × List Bool) ↪ List Bool := ⟨encodeInput, encodeInput_injective⟩ + +/-- A Boolean answer is encoded as its single bit. -/ +def encAnswer : Bool ↪ List Bool := ⟨fun b => [b], by intro a b h; injection h⟩ + +/-- One deterministic binary multi-tape machine halts on every encoded pair and writes +`V`'s answer, within time and work-space bounds polynomial in the pair's encoded length. +`Cslib.PolynomiallyBounded` means bounded above by a polynomial. -/ +def PolyTimePredicate (V : List Bool × List Bool → Bool) : Prop := + ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ + Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength V encInput encAnswer t s + +/-! ## Randomness and two quantifier blocks -/ + +/-- BPP languages have a polynomial-time test with `p(|x|)` fair independent random bits, +correct on at least two thirds of seeds for each input. The inequalities count correct seeds +out of `2 ^ p(|x|)`. A function `Fin m → Bool` represents an `m`-bit seed; +`List.ofFn` lists its bits. -/ +def BPP : Set (Set (List Bool)) := + {A | ∃ (p : Polynomial ℕ) (V : List Bool × List Bool → Bool), + PolyTimePredicate V ∧ ∀ x, + (x ∈ A → 2 * 2 ^ p.eval x.length ≤ + 3 * (Finset.univ.filter fun r : Fin (p.eval x.length) → Bool => + V (x, List.ofFn r) = true).card) ∧ + (x ∉ A → 2 * 2 ^ p.eval x.length ≤ + 3 * (Finset.univ.filter fun r : Fin (p.eval x.length) → Bool => + V (x, List.ofFn r) = false).card)} + +/-- Σ₂ uses an existential block `u` followed by a universal block `v`, with polynomial lengths +and a total polynomial-time test of `u ++ v`. Block lengths depend only on the input length. -/ +def SigmaTwo : Set (Set (List Bool)) := + {A | ∃ (p q : Polynomial ℕ) (V : List Bool × List Bool → Bool), + PolyTimePredicate V ∧ ∀ x, x ∈ A ↔ + ∃ u : List Bool, u.length = p.eval x.length ∧ + ∀ v : List Bool, v.length = q.eval x.length → V (x, u ++ v) = true} + +/-- Π₂ reverses the order: every polynomial-length block `u` has a polynomial-length response +`v` passing the test. The response may depend on the instance and `u`. The two classes may +use different tests and length polynomials. -/ +def PiTwo : Set (Set (List Bool)) := + {A | ∃ (p q : Polynomial ℕ) (V : List Bool × List Bool → Bool), + PolyTimePredicate V ∧ ∀ x, x ∈ A ↔ + ∀ u : List Bool, u.length = p.eval x.length → + ∃ v : List Bool, v.length = q.eval x.length ∧ V (x, u ++ v) = true} + +/-- **Sipser–Gács–Lautemann.** Every bounded-error randomized polynomial-time language has both +polynomial two-block descriptions: BPP ⊆ Σ₂ ∩ Π₂. -/ +theorem sipserLautemann : BPP ⊆ SigmaTwo ∩ PiTwo := + SipserLautemannBridge.sipserLautemann + +/-- +info: 'ComplexityAbstracts.SipserLautemannAbstract.sipserLautemann' depends on axioms: +[propext, Classical.choice, Quot.sound] +-/ +#guard_msgs (whitespace := lax) in +#print axioms sipserLautemann + +/-- +info: abstract audit passed for `ComplexityAbstracts.SipserLautemannAbstract`: 10 root +declarations, 67 dependencies checked +-/ +#guard_msgs (whitespace := lax) in +#check_abstract ComplexityAbstracts.SipserLautemannAbstract + +end ComplexityAbstracts.SipserLautemannAbstract diff --git a/abstracts/ComplexityAbstracts/SipserLautemannBridge.lean b/abstracts/ComplexityAbstracts/SipserLautemannBridge.lean new file mode 100644 index 0000000000..16dfd0aa41 --- /dev/null +++ b/abstracts/ComplexityAbstracts/SipserLautemannBridge.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2026 Bolton Bailey, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bolton Bailey, Samuel Schlesinger +-/ + +-- upstream: local-only (formal abstract proof bridge) + +import ComplexityAbstracts.CookLevinBridge +import Complexity.Computability.Complexity.Classes.PH.SipserLautemann + +/-! # Proof bridge for the Sipser–Lautemann formal abstract + +Transfer bounded-error computation and two polynomial quantifier blocks to native deterministic +Turing-machine bounds. The public abstract states all class semantics explicitly. +-/ + +namespace ComplexityAbstracts.SipserLautemannBridge + +open ComplexityTests.Abstracts +open Turing.MultiTapeTM + +/-- The framed encoding of an instance followed by a seed or quantified certificate. -/ +def encInput : (List Bool × List Bool) ↪ List Bool := + CookLevinBridge.encPair (Function.Embedding.refl _) (Function.Embedding.refl _) + +/-- A Boolean answer occupies one bit. -/ +def encAnswer : Bool ↪ List Bool := + ⟨fun b => [b], by intro a b h; injection h⟩ + +/-- Total polynomial-time predicates, using plain upstream machine bounds. -/ +def PolyTimePredicate (V : List Bool × List Bool → Bool) : Prop := + ∃ t s : ℕ → ℕ, Cslib.PolynomiallyBounded t ∧ Cslib.PolynomiallyBounded s ∧ + ComputableInTimeAndSpaceOfLength V encInput encAnswer t s + +/-- Bounded-error computation with fair binary seeds. -/ +def BPP : Set (Set (List Bool)) := + {A | ∃ (p : Polynomial ℕ) (V : List Bool × List Bool → Bool), + PolyTimePredicate V ∧ ∀ x, + (x ∈ A → 2 * 2 ^ p.eval x.length ≤ + 3 * (Finset.univ.filter fun r : Fin (p.eval x.length) → Bool => + V (x, List.ofFn r) = true).card) ∧ + (x ∉ A → 2 * 2 ^ p.eval x.length ≤ + 3 * (Finset.univ.filter fun r : Fin (p.eval x.length) → Bool => + V (x, List.ofFn r) = false).card)} + +/-- A polynomial existential block followed by a polynomial universal block. -/ +def SigmaTwo : Set (Set (List Bool)) := + {A | ∃ (p q : Polynomial ℕ) (V : List Bool × List Bool → Bool), + PolyTimePredicate V ∧ ∀ x, x ∈ A ↔ + ∃ u : List Bool, u.length = p.eval x.length ∧ + ∀ v : List Bool, v.length = q.eval x.length → V (x, u ++ v) = true} + +/-- A polynomial universal block followed by a polynomial existential block. -/ +def PiTwo : Set (Set (List Bool)) := + {A | ∃ (p q : Polynomial ℕ) (V : List Bool × List Bool → Bool), + PolyTimePredicate V ∧ ∀ x, x ∈ A ↔ + ∀ u : List Bool, u.length = p.eval x.length → + ∃ v : List Bool, v.length = q.eval x.length ∧ V (x, u ++ v) = true} + +private theorem polyTimePredicate_iff {V : List Bool × List Bool → Bool} : + PolyTimePredicate V ↔ ComputableInPolyTime V + (encPair encBits encBits) encBool := + Iff.rfl + +private theorem mem_BPP_iff {A : Set (List Bool)} : + A ∈ BPP ↔ A ∈ Cslib.Complexity.BPP encBits := by + simp only [BPP, Set.mem_ofPred_eq, Cslib.Complexity.BPP, + Cslib.Complexity.DecidesWithBoundedError, polyTimePredicate_iff] + rfl + +private theorem sigmaTwo_of_mem {A : Set (List Bool)} + (hA : A ∈ Cslib.Complexity.SigmaP 2 encBits) : A ∈ SigmaTwo := by + obtain ⟨ps, V, hlen, hV, hA⟩ := hA + obtain ⟨p, q, rfl⟩ := List.length_eq_two.mp hlen + refine ⟨p, q, V, polyTimePredicate_iff.mpr hV, ?_⟩ + simpa only [Cslib.Complexity.IsAlternatingVerifier, List.map_cons, List.map_nil, + Cslib.Complexity.alternation_true_cons, Cslib.Complexity.alternation_false_cons, + Cslib.Complexity.alternation_nil, List.append_nil, encBits, + Function.Embedding.refl_apply] using hA + +private theorem piTwo_of_mem {A : Set (List Bool)} + (hA : A ∈ Cslib.Complexity.PiP 2 encBits) : A ∈ PiTwo := by + obtain ⟨ps, V, hlen, hV, hA⟩ := hA + obtain ⟨p, q, rfl⟩ := List.length_eq_two.mp hlen + refine ⟨p, q, V, polyTimePredicate_iff.mpr hV, ?_⟩ + simpa only [Cslib.Complexity.IsAlternatingVerifier, List.map_cons, List.map_nil, + Cslib.Complexity.alternation_true_cons, Cslib.Complexity.alternation_false_cons, + Cslib.Complexity.alternation_nil, List.append_nil, encBits, + Function.Embedding.refl_apply] using hA + +/-- The Sipser–Gács–Lautemann containment, with both quantifier prefixes exposed. -/ +theorem sipserLautemann : BPP ⊆ SigmaTwo ∩ PiTwo := by + intro A hA + have h := Cslib.Complexity.BPP_subset_SigmaP_two_inter_PiP_two (mem_BPP_iff.mp hA) + exact ⟨sigmaTwo_of_mem h.1, piTwo_of_mem h.2⟩ + +end ComplexityAbstracts.SipserLautemannBridge diff --git a/abstracts/README.md b/abstracts/README.md index 5fed338d1d..a295111e7d 100644 --- a/abstracts/README.md +++ b/abstracts/README.md @@ -1,6 +1,6 @@ # Selected formal abstracts -The catalogue promotes twelve major result groups. Each has a checked Lean abstract with the +The catalogue promotes fourteen major result groups. Each has a checked Lean abstract with the definitions needed to understand its statement, a bridge to the library proof, and an audited dependency boundary. Some abstracts also allowlist a few library modules for foundational models (for example circuit signatures or oracle runs); each such abstract names them in its docstring, and @@ -43,6 +43,8 @@ former paper/TeX index is retired; Git history retains its sources. | [Formula lower bounds: parity and Andreev](ComplexityAbstracts/FormulaBoundsAbstract.lean) · [PDF](https://github.com/cslib-community/complexitylib/releases/download/formal-abstracts/formula-bounds.pdf) | De Morgan formulas, literal leaves, explicit block indexing and finite quantitative bounds; no general-circuit lower bound. | | [One-way functions yield pseudorandom generators and adaptive functions](ComplexityAbstracts/CryptographyAbstract.lean) · [PDF](https://github.com/cslib-community/complexitylib/releases/download/formal-abstracts/cryptography.pdf) | Uniform probabilistic polynomial time with explicit native evaluators, negligible advantage and full stateful oracle semantics; asymptotic security, not a concrete implementation audit. | | [Haken: pigeonhole formulas require long resolution proofs](ComplexityAbstracts/ResolutionAbstract.lean) · [PDF](https://github.com/cslib-community/complexitylib/releases/download/formal-abstracts/resolution.pdf) | The non-onto pigeonhole formula and a line-based resolution rule, with bound 2^(floor(n/24)); proof size is not solver runtime. | +| [Communication: disjointness and inner product resist randomness](ComplexityAbstracts/CommunicationAbstract.lean) · [PDF](https://github.com/cslib-community/complexitylib/releases/download/formal-abstracts/communication.pdf) | Shared randomness, per-input error at most one third and explicit linear bounds; exact deterministic equality records the final-answer convention. | +| [Sipser–Gács–Lautemann: BPP lies in the second polynomial level](ComplexityAbstracts/SipserLautemannAbstract.lean) · [PDF](https://github.com/cslib-community/complexitylib/releases/download/formal-abstracts/sipser-lautemann.pdf) | Fair random bits, explicit quantifier blocks and total native polynomial-time tests. | ## Generate and review PDFs diff --git a/abstracts/catalogue.json b/abstracts/catalogue.json index a3d85d1613..b0fa453058 100644 --- a/abstracts/catalogue.json +++ b/abstracts/catalogue.json @@ -159,6 +159,30 @@ "ComplexityTests.Abstracts.ResolutionAbstract.pigeonhole_satisfiable" ], "namespace": "ComplexityTests.Abstracts.ResolutionAbstract" + }, + { + "id": "communication", + "title": "Communication: disjointness and inner product resist randomness", + "module": "ComplexityAbstracts.CommunicationAbstract", + "headline_theorems": [ + "ComplexityAbstracts.CommunicationAbstract.disjointness_lower_bound", + "ComplexityAbstracts.CommunicationAbstract.innerProduct_lower_bound" + ], + "supporting_theorems": [ + "ComplexityAbstracts.CommunicationAbstract.equality" + ], + "summary": "Disjointness and parity of intersection require linear communication even with shared randomness and bounded error.", + "scope": "Binary protocol trees, worst-case cost and error at most one third on every input pair; explicit finite bounds and the final-answer convention." + }, + { + "id": "sipser-lautemann", + "title": "Sipser–Gács–Lautemann: BPP lies in the second polynomial level", + "module": "ComplexityAbstracts.SipserLautemannAbstract", + "headline_theorems": [ + "ComplexityAbstracts.SipserLautemannAbstract.sipserLautemann" + ], + "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." } ] } diff --git a/scripts/abstract_to_tex.py b/scripts/abstract_to_tex.py index f176217ecc..3a88458eee 100644 --- a/scripts/abstract_to_tex.py +++ b/scripts/abstract_to_tex.py @@ -56,6 +56,7 @@ "·": r"\cdot", "ℓ": r"\ell", "Σ": r"\Sigma", + "Π": r"\Pi", "α": r"\alpha", "β": r"\beta", "γ": r"\gamma", @@ -92,6 +93,7 @@ "’": "'", "“": "``", "”": "''", + "á": r"\'{a}", "é": r"\'{e}", "É": r"\'{E}", "ő": r"\H{o}",