feat(testing): prove the adaptive one-sided linearity query lower bound

Complexity.lean

@@ -1987,6 +1987,7 @@ public import Complexity.Computability.Probabilistic.Selection
 public import Complexity.Computability.Probabilistic.Traverse
 public import Complexity.Computability.Probabilistic.UniformNat
 public import Complexity.Computability.PropertyTesting.Linearity
+public import Complexity.Computability.PropertyTesting.LinearityLowerBound
 public import Complexity.Computability.QueryComplexity.ApproximateDegree
 public import Complexity.Computability.QueryComplexity.ApproximateDegree.Or
 public import Complexity.Computability.QueryComplexity.Degree
@@ -2557,6 +2558,7 @@ public import Complexity.Foundations.Data.BitString.List.Vote
 public import Complexity.Foundations.Data.BitString.Parity
 public import Complexity.Foundations.Data.BitString.Parity.DotProduct
 public import Complexity.Foundations.Data.BitString.Parity.Weight
+public import Complexity.Foundations.Data.BitString.ParityInterpolation
 public import Complexity.Foundations.Data.BitString.ParityTestBounds
 public import Complexity.Foundations.Data.BitString.ParityTests
 public import Complexity.Foundations.Data.BitString.PartialAssignment

Complexity/Computability/PropertyTesting/LinearityLowerBound.lean

@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.QueryComplexity.Randomized
+public import Complexity.Foundations.Data.BitString.ParityInterpolation
+public import Mathlib.Probability.ProbabilityMassFunction.Basic
+
+/-!
+# Three queries are necessary for one-sided linearity testing
+
+A decision tree of depth at most two that accepts every parity accepts every table `f` with
+`f 0 = false`. On the path taken by `f`, at most two points are queried. Their answers agree
+with a parity, so that parity reaches the same accepting leaf, even when the second query
+depends on the first answer.
+
+Consequently, any distribution on decision trees with perfect completeness on every parity
+that rejects such a normalized table with positive probability has a supported tree making
+at least three queries. The PMF statement has no finite-support assumption. The finite-simplex
+randomized-decision-tree model has the corresponding lower bound on its worst-case depth.
+These are supportwise query bounds, with no lower bound on the expected number of queries.
+
+## Main results
+
+* `Cslib.DecisionTree.eval_eq_true_of_depth_le_two_of_parity_complete`: two adaptive queries
+  cannot reject a normalized table while accepting all parities.
+* `Cslib.DecisionTree.three_le_card_queries_of_parity_complete`: rejection requires three
+  distinct queried points on that input, even if other paths are long or queries repeat.
+* `Cslib.BitString.exists_three_le_depth_of_parity_complete`: the lower bound for an arbitrary PMF.
+* `Cslib.RandomizedDecisionTree.three_le_depth_of_parity_complete`: the lower bound in the existing
+  finitely supported randomized model.
+
+## References
+
+The two-point interpolation and indistinguishability argument is elementary and original to this
+formalization.
+-/
+
+public section
+
+namespace Cslib
+
+open Finset
+
+private theorem exists_subset_pair_of_card_le_two {α : Type*} [DecidableEq α] [Nonempty α]
+    (s : Finset α) (hs : s.card ≤ 2) : ∃ a b, s ⊆ {a, b} := by
+  classical
+  by_cases hne : s.Nonempty
+  · obtain ⟨a, ha⟩ := hne
+    have herase : (s.erase a).card ≤ 1 := by
+      rw [card_erase_of_mem ha]
+      omega
+    obtain ⟨b, hb⟩ := card_le_one_iff_subset_singleton.1 herase
+    refine ⟨a, b, ?_⟩
+    intro x hx
+    by_cases hxa : x = a
+    · exact mem_insert.2 (Or.inl hxa)
+    · exact mem_insert.2 (Or.inr (hb (mem_erase.2 ⟨hxa, hx⟩)))
+  · obtain ⟨a⟩ := ‹Nonempty α›
+    exact ⟨a, a, by rw [not_nonempty_iff_eq_empty.1 hne]; exact empty_subset _⟩
+
+namespace DecisionTree
+
+variable {ι : Type*}
+
+private theorem eval_eq_true_of_card_queries_le_two_of_parity_complete
+    (t : DecisionTree (ι → Bool) Bool)
+    (hcomplete : ∀ S : Finset ι, t.eval (parityOn S) = true)
+    {f : (ι → Bool) → Bool} (hf : f 0 = false)
+    [DecidableEq (ι → Bool)] (hcard : (t.queries f).card ≤ 2) : t.eval f = true := by
+  classical
+  obtain ⟨x, y, hqueries⟩ := exists_subset_pair_of_card_le_two (t.queries f) hcard
+  obtain ⟨S, hSx, hSy⟩ := BitString.exists_parityOn_agrees_pair hf x y
+  have hagree : ∀ z ∈ t.queries f, parityOn S z = f z := by
+    intro z hz
+    have h := hqueries hz
+    simp only [mem_insert, mem_singleton] at h
+    rcases h with rfl | rfl
+    · exact hSx
+    · exact hSy
+  rw [← t.eval_eq_of_forall_mem_queries hagree]
+  exact hcomplete S
+
+/-- A tree that accepts all parities and makes at most two adaptive queries accepts every table
+that is false at zero. -/
+theorem eval_eq_true_of_depth_le_two_of_parity_complete
+    (t : DecisionTree (ι → Bool) Bool) (hd : t.depth ≤ 2)
+    (hcomplete : ∀ S : Finset ι, t.eval (parityOn S) = true)
+    {f : (ι → Bool) → Bool} (hf : f 0 = false) : t.eval f = true := by
+  classical
+  exact t.eval_eq_true_of_card_queries_le_two_of_parity_complete hcomplete hf
+    ((t.card_queries_le_depth f).trans hd)
+
+/-- Rejecting a normalized table while accepting all parities requires three distinct queried
+points on that input. This remains true when other paths are longer or positions are repeated. -/
+theorem three_le_card_queries_of_parity_complete
+    (t : DecisionTree (ι → Bool) Bool)
+    (hcomplete : ∀ S : Finset ι, t.eval (parityOn S) = true)
+    {f : (ι → Bool) → Bool} (hf : f 0 = false) (hreject : t.eval f ≠ true)
+    [DecidableEq (ι → Bool)] : 3 ≤ (t.queries f).card := by
+  by_contra! hcard
+  exact hreject (t.eval_eq_true_of_card_queries_le_two_of_parity_complete hcomplete hf (by omega))
+
+end DecisionTree
+
+namespace BitString
+
+variable {ι : Type*}
+
+/-- Perfect completeness on parities and positive rejection of a normalized table force a
+positive-mass tree of depth at least three. No finite-support hypothesis on `μ` is needed. -/
+theorem exists_three_le_depth_of_parity_complete
+    (μ : PMF (DecisionTree (ι → Bool) Bool))
+    (hcomplete : ∀ S : Finset ι, μ.toOuterMeasure {t | t.eval (parityOn S) ≠ true} = 0)
+    {f : (ι → Bool) → Bool} (hf : f 0 = false)
+    (hreject : 0 < μ.toOuterMeasure {t | t.eval f ≠ true}) :
+    ∃ t ∈ μ.support, 3 ≤ t.depth := by
+  classical
+  by_contra! hdepth
+  have hzero : μ.toOuterMeasure {t | t.eval f ≠ true} = 0 := by
+    apply (PMF.toOuterMeasure_apply_eq_zero_iff μ _).2
+    apply Set.disjoint_left.2
+    intro t ht hfail
+    apply hfail
+    apply t.eval_eq_true_of_depth_le_two_of_parity_complete (by have := hdepth t ht; omega)
+    · intro S
+      have hdisjoint := (PMF.toOuterMeasure_apply_eq_zero_iff μ _).1 (hcomplete S)
+      by_contra hnot
+      exact Set.disjoint_left.1 hdisjoint ht hnot
+    · exact hf
+  rw [hzero] at hreject
+  exact lt_irrefl _ hreject
+
+end BitString
+
+namespace RandomizedDecisionTree
+
+variable {ι : Type*}
+
+/-- In the existing finite-simplex randomized-tree model, a perfectly complete parity tester
+rejecting a normalized table with positive probability has worst-case query depth at least three. -/
+theorem three_le_depth_of_parity_complete (μ : RandomizedDecisionTree (ι → Bool) Bool)
+    (hcomplete : ∀ S : Finset ι, μ.errorProb (fun _ => true) (parityOn S) = 0)
+    {f : (ι → Bool) → Bool} (hf : f 0 = false)
+    (hreject : 0 < μ.errorProb (fun _ => true) f) : 3 ≤ μ.depth := by
+  by_contra! hdepth
+  have hzero : μ.errorProb (fun _ => true) f = 0 := by
+    apply errorProb_eq_zero_iff.2
+    intro t ht
+    apply t.eval_eq_true_of_depth_le_two_of_parity_complete
+      ((depth_le_depth ht).trans (by omega))
+    · intro S
+      exact errorProb_eq_zero_iff.1 (hcomplete S) t ht
+    · exact hf
+  rw [hzero] at hreject
+  exact lt_irrefl _ hreject
+
+end RandomizedDecisionTree
+
+end Cslib

Complexity/Foundations/Data/BitString/ParityInterpolation.lean

@@ -0,0 +1,121 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Foundations.Data.BitString.Parity
+
+/-!
+# Interpolating two table entries by a parity
+
+The values of a Boolean table `f` with `f 0 = false` at any two points of the cube agree with
+some parity. The zero point and repeated points impose the only consistency conditions on two
+answers. The parity can be chosen on finitely many coordinates even when the coordinate type
+is infinite. This elementary interpolation lemma is proved by choosing separating coordinates.
+
+## Main results
+
+* `Cslib.BitString.exists_parityOn_agrees_pair`: a normalized table agrees with a parity at two
+  specified points.
+
+## References
+
+The interpolation argument in this module is elementary and original to this formalization.
+-/
+
+public section
+
+namespace Cslib.BitString
+
+variable {ι : Type*}
+
+private theorem exists_true_of_ne_zero {x : ι → Bool} (hx : x ≠ 0) : ∃ i, x i = true := by
+  obtain ⟨i, hi⟩ : ∃ i, x i ≠ false := by
+    by_contra! h
+    exact hx (funext h)
+  exact ⟨i, Bool.eq_true_of_not_eq_false hi⟩
+
+private theorem exists_parityOn_true_false {x y : ι → Bool} (hx : x ≠ 0) (hxy : x ≠ y) :
+    ∃ S : Finset ι, parityOn S x = true ∧ parityOn S y = false := by
+  classical
+  obtain ⟨i, hi⟩ := exists_true_of_ne_zero hx
+  by_cases hyi : y i = false
+  · exact ⟨{i}, by simpa only [parityOn_singleton] using hi,
+      by simpa only [parityOn_singleton] using hyi⟩
+  have hyi : y i = true := Bool.eq_true_of_not_eq_false hyi
+  obtain ⟨j, hj⟩ : ∃ j, x j ≠ y j := by
+    by_contra! h
+    exact hxy (funext h)
+  by_cases hxj : x j = true
+  · have hyj : y j = false := by
+      cases hy : y j
+      · rfl
+      · exact (hj (hxj.trans hy.symm)).elim
+    exact ⟨{j}, by simpa only [parityOn_singleton] using hxj,
+      by simpa only [parityOn_singleton] using hyj⟩
+  · have hxj : x j = false := Bool.eq_false_of_not_eq_true hxj
+    have hyj : y j = true := by
+      cases hy : y j
+      · exact (hj (hxj.trans hy.symm)).elim
+      · rfl
+    have hij : i ≠ j := by
+      intro h
+      subst j
+      rw [hi] at hxj
+      contradiction
+    refine ⟨{i, j}, ?_, ?_⟩
+    · simp [parityOn_insert, hij, hi, hxj]
+    · simp [parityOn_insert, hij, hyi, hyj]
+
+/-- Any two answers of a table that is false at zero extend to a parity. The two points may
+coincide or be zero; no finiteness assumption on the coordinate type is needed. -/
+theorem exists_parityOn_agrees_pair {f : (ι → Bool) → Bool} (hf : f 0 = false)
+    (x y : ι → Bool) : ∃ S : Finset ι, parityOn S x = f x ∧ parityOn S y = f y := by
+  cases hfx : f x <;> cases hfy : f y
+  · exact ⟨∅, parityOn_empty x, parityOn_empty y⟩
+  · have hy : y ≠ 0 := by
+      intro h
+      rw [h, hf] at hfy
+      contradiction
+    have hyx : y ≠ x := by
+      intro h
+      rw [h, hfx] at hfy
+      contradiction
+    obtain ⟨S, hSy, hSx⟩ := exists_parityOn_true_false hy hyx
+    exact ⟨S, hSx, hSy⟩
+  · have hx : x ≠ 0 := by
+      intro h
+      rw [h, hf] at hfx
+      contradiction
+    have hxy : x ≠ y := by
+      intro h
+      rw [h, hfy] at hfx
+      contradiction
+    obtain ⟨S, hSx, hSy⟩ := exists_parityOn_true_false hx hxy
+    exact ⟨S, hSx, hSy⟩
+  · have hx : x ≠ 0 := by
+      intro h
+      rw [h, hf] at hfx
+      contradiction
+    have hy : y ≠ 0 := by
+      intro h
+      rw [h, hf] at hfy
+      contradiction
+    have hxy : x ≠ x + y := by
+      intro h
+      apply hy
+      exact (add_left_cancel ((add_zero x).trans h)).symm
+    obtain ⟨S, hSx, hSsum⟩ := exists_parityOn_true_false hx hxy
+    refine ⟨S, hSx, ?_⟩
+    have hadd := parityOn_add S x y
+    rw [hSsum, hSx] at hadd
+    cases hSy : parityOn S y
+    · rw [hSy] at hadd
+      cases hadd
+    · rfl
+
+end Cslib.BitString

ComplexityTests/PropertyTestingLinearityLowerBound.lean

@@ -0,0 +1,88 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.PropertyTesting.LinearityLowerBound
+import Complexity.Probability.PMF.Uniform
+import ComplexityTests.BooleanAnalysisExamples
+
+/-! Concrete sharpness and probability clients for the one-sided linearity query lower bound. -/
+
+namespace ComplexityTests.PropertyTestingLinearityLowerBound
+
+open Cslib Cslib.BitString Cslib.Probability BooleanAnalysisExamples
+open scoped ENNReal
+
+private def leftPoint : Fin 2 → Bool := ![true, false]
+private def rightPoint : Fin 2 → Bool := ![false, true]
+
+-- Check the BLR equation at the two coordinate vectors: exactly three queries suffice here.
+private def checkTree : DecisionTree (Fin 2 → Bool) Bool :=
+  DecisionTree.queryAll (fun f => decide ((f leftPoint ^^ f rightPoint) =
+    f (leftPoint + rightPoint))) [leftPoint, rightPoint, leftPoint + rightPoint] fun _ => false
+
+private theorem checkTree_complete : ∀ S : Finset (Fin 2), checkTree.eval (parityOn S) = true := by
+  decide
+
+private theorem checkTree_rejects : checkTree.eval and₂ = false := by decide
+
+example : checkTree.depth = 3 := by decide
+
+example : 3 ≤ (checkTree.queries and₂).card :=
+  checkTree.three_le_card_queries_of_parity_complete checkTree_complete (by decide)
+    (by rw [checkTree_rejects]; decide)
+
+-- Conjunction satisfies the normalization and distance promise; this is a genuine no-instance.
+example : and₂ 0 = false ∧ ∀ S : Finset (Fin 2), 1 ≤ hammingDist and₂ (parityOn S) := by decide
+
+-- The interpolation statement covers a zero point and a repeated nonzero point.
+example : ∃ S : Finset (Fin 2), parityOn S 0 = and₂ 0 ∧
+    parityOn S leftPoint = and₂ leftPoint :=
+  exists_parityOn_agrees_pair (by decide) 0 leftPoint
+
+example : ∃ S : Finset (Fin 2), parityOn S leftPoint = and₂ leftPoint ∧
+    parityOn S leftPoint = and₂ leftPoint :=
+  exists_parityOn_agrees_pair (by decide) leftPoint leftPoint
+
+private def chooseTree (b : Bool) : DecisionTree (Fin 2 → Bool) Bool :=
+  if b then checkTree else .leaf true
+
+private noncomputable def coinTester : PMF (DecisionTree (Fin 2 → Bool) Bool) :=
+  (PMF.uniformOfFintype Bool).map chooseTree
+
+private theorem coinTester_complete (S : Finset (Fin 2)) :
+    coinTester.toOuterMeasure {t | t.eval (parityOn S) ≠ true} = 0 := by
+  rw [coinTester, PMF.toOuterMeasure_map_apply]
+  have hempty : chooseTree ⁻¹' {t | t.eval (parityOn S) ≠ true} = ∅ := by
+    ext b
+    cases b <;> simp [chooseTree, checkTree_complete]
+  rw [hempty]
+  simp
+
+-- The tester makes zero or three queries with equal probability and rejects conjunction with
+-- probability 1/2. The lower bound concerns a positive-mass three-query run, not expected depth.
+private theorem coinTester_rejects :
+    coinTester.toOuterMeasure {t | t.eval and₂ ≠ true} = 1 / 2 := by
+  rw [coinTester, PMF.toOuterMeasure_map_apply]
+  have hevent : chooseTree ⁻¹' {t | t.eval and₂ ≠ true} = {true} := by
+    ext b
+    cases b <;> simp [chooseTree, checkTree_rejects]
+  rw [hevent, PMF.toOuterMeasure_uniformOfFintype]
+  norm_num [Finset.filter_insert, Finset.filter_singleton]
+
+example : ∃ t ∈ coinTester.support, 3 ≤ t.depth :=
+  exists_three_le_depth_of_parity_complete coinTester coinTester_complete (f := and₂) (by decide)
+    (by rw [coinTester_rejects]; norm_num)
+
+-- The existing finite-simplex model receives the same worst-case lower bound.
+example : 3 ≤ RandomizedDecisionTree.depth (Convexity.StdSimplex.single checkTree :
+    RandomizedDecisionTree (Fin 2 → Bool) Bool) := by
+  apply RandomizedDecisionTree.three_le_depth_of_parity_complete (f := and₂)
+  · intro S
+    simp [RandomizedDecisionTree.errorProb, checkTree_complete]
+  · decide
+  · simp [RandomizedDecisionTree.errorProb, checkTree_rejects]
+
+end ComplexityTests.PropertyTestingLinearityLowerBound