feat(Probability): affine retention channels satisfy the detector interface

Complexity.lean

@@ -2558,6 +2558,7 @@ public import Complexity.Foundations.Data.Fin.Tuple
 public import Complexity.Foundations.Data.Finset.Average
 public import Complexity.Foundations.Data.Finset.Expect
 public import Complexity.Foundations.Data.Finset.Finpartition
+public import Complexity.Foundations.Data.Finset.KthLargest
 public import Complexity.Foundations.Data.Finset.Markov
 public import Complexity.Foundations.Data.Finset.OrderGlue
 public import Complexity.Foundations.Data.Finset.OrderedFilter
@@ -2689,6 +2690,7 @@ public import Complexity.Foundations.LinearAlgebra.Matrix.Kronecker
 public import Complexity.Foundations.LinearAlgebra.Matrix.Lindsey
 public import Complexity.Foundations.LinearAlgebra.Matrix.ListProd
 public import Complexity.Foundations.LinearAlgebra.Matrix.Moore
+public import Complexity.Foundations.LinearAlgebra.Matrix.PilotCorrection
 public import Complexity.Foundations.LinearAlgebra.Matrix.Rank
 public import Complexity.Foundations.LinearAlgebra.Matrix.RectPermanent
 public import Complexity.Foundations.LinearAlgebra.Matrix.SchurComplement
@@ -2711,6 +2713,8 @@ public import Complexity.Foundations.NumberTheory.SqrtPrimeWindow
 public import Complexity.Foundations.Order.BooleanSubalgebra
 public import Complexity.Foundations.Order.Changes
 public import Complexity.Foundations.Order.UpperLower
+public import Complexity.Foundations.Probability.ColumnDetector
+public import Complexity.Foundations.Probability.DetectedStage
 public import Complexity.Foundations.Probability.Gaussian.Multivariate
 public import Complexity.Foundations.Probability.Gaussian.Real
 public import Complexity.Foundations.Probability.Gaussian.Sheppard
@@ -2978,6 +2982,7 @@ public import Complexity.Probability.PMF.UniformSubset
 public import Complexity.Probability.PairwiseIndependent
 public import Complexity.Probability.PairwiseIndependentHash
 public import Complexity.Probability.PairwiseIndependentHash.Affine
+public import Complexity.Probability.PairwiseIndependentHash.DetectorChannels
 public import Complexity.Probability.PairwiseIndependentHash.Retention
 public import Complexity.Probability.PairwiseIndependentHash.RetentionChannel
 public import Complexity.Probability.PairwiseIndependentHash.Shift

Complexity/Foundations/Data/Finset/KthLargest.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Init
+public import Mathlib.Data.Finset.Max
+
+/-!
+# The `k`-th largest value, padded with zeros
+
+`Finset.kthLargest k s h` is the `k`-th largest member of the multiset of values `h x`, `x ∈ s`,
+padded with infinitely many zeros. It is the largest value `h x` that is reached or exceeded by at
+least `k` of the values, or `0` if that is larger. So it is nonnegative, and it is `0` when fewer
+than `k` of the values are positive. This is the order statistic `rank_k` of the detectors in the
+OpenAI preprint [OpenAI2026LogSpace, Section 4.2].
+
+It is characterized by threshold counts: for `0 < k` and `0 ≤ t`, the `k`-th largest value exceeds
+`t` exactly when at least `k` values exceed `t` (`Finset.lt_kthLargest_iff`), and for `0 < t` it
+is at least `t` exactly when at least `k` values are at least `t` (`Finset.le_kthLargest_iff`).
+
+## Main definitions
+
+* `Finset.kthLargest`: the `k`-th largest value, padded with zeros.
+
+## Main results
+
+* `Finset.kthLargest_nonneg`, `Finset.kthLargest_le`: bounds.
+* `Finset.lt_kthLargest_iff`, `Finset.le_kthLargest_iff`: the threshold characterizations.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 4.2 (preprint, not peer reviewed)
+-/
+
+public section
+
+namespace Finset
+
+variable {α R : Type*} [LinearOrder R] [Zero R]
+
+/-- The **`k`-th largest value** of `h` on `s`, padded with zeros: the largest value `h x`,
+`x ∈ s`, that at least `k` values `h w`, `w ∈ s`, reach or exceed, or `0` if that is larger. -/
+@[expose] def kthLargest (k : ℕ) (s : Finset α) (h : α → R) : R :=
+  (insert 0 ((s.filter fun x => k ≤ #{w ∈ s | h x ≤ h w}).image h)).max' (insert_nonempty _ _)
+
+variable {k : ℕ} {s : Finset α} {h : α → R} {t : R}
+
+theorem kthLargest_nonneg : 0 ≤ kthLargest k s h :=
+  le_max' _ _ (mem_insert_self _ _)
+
+/-- The `k`-th largest value is at most any nonnegative upper bound of the values. -/
+theorem kthLargest_le (ht : 0 ≤ t) (hh : ∀ x ∈ s, h x ≤ t) : kthLargest k s h ≤ t := by
+  refine max'_le _ _ _ fun a ha => ?_
+  rcases mem_insert.mp ha with rfl | ha
+  · exact ht
+  · obtain ⟨x, hx, rfl⟩ := mem_image.mp ha
+    exact hh x (mem_filter.mp hx).1
+
+/-- A value of `s` reached or exceeded by at least `k` values is at most the `k`-th largest. -/
+private theorem le_kthLargest_of_le_card {x : α} (hx : x ∈ s)
+    (hk : k ≤ #{w ∈ s | h x ≤ h w}) : h x ≤ kthLargest k s h :=
+  le_max' _ _ (mem_insert_of_mem (mem_image_of_mem h (mem_filter.mpr ⟨hx, hk⟩)))
+
+omit [Zero R] in
+/-- If at least `k > 0` values satisfy a threshold condition, so does the smallest of them, which
+is reached or exceeded by all of them. -/
+private theorem exists_le_card (hk : 0 < k) (p : R → Prop) [DecidablePred p]
+    (hp : k ≤ #{x ∈ s | p (h x)}) :
+    ∃ x ∈ s, p (h x) ∧ k ≤ #{w ∈ s | h x ≤ h w} := by
+  have hne : ({x ∈ s | p (h x)} : Finset α).Nonempty := card_pos.mp (hk.trans_le hp)
+  obtain ⟨x, hx, hmin⟩ := exists_min_image _ h hne
+  obtain ⟨hxs, hpx⟩ := mem_filter.mp hx
+  refine ⟨x, hxs, hpx, hp.trans (card_le_card fun w hw => ?_)⟩
+  exact mem_filter.mpr ⟨(mem_filter.mp hw).1, hmin w hw⟩
+
+/-- **The `k`-th largest value exceeds `t ≥ 0`** exactly when at least `k > 0` values do. -/
+theorem lt_kthLargest_iff (hk : 0 < k) (ht : 0 ≤ t) :
+    t < kthLargest k s h ↔ k ≤ #{x ∈ s | t < h x} := by
+  constructor
+  · intro hlt
+    obtain ⟨a, ha, hta⟩ : ∃ a ∈ _, t < a := ⟨_, max'_mem _ _, hlt⟩
+    rcases mem_insert.mp ha with rfl | ha
+    · exact absurd ht (not_le.mpr hta)
+    obtain ⟨x, hx, rfl⟩ := mem_image.mp ha
+    obtain ⟨-, hkx⟩ := mem_filter.mp hx
+    exact hkx.trans (card_le_card fun w hw => by
+      obtain ⟨hws, hxw⟩ := mem_filter.mp hw
+      exact mem_filter.mpr ⟨hws, hta.trans_le hxw⟩)
+  · intro hcard
+    obtain ⟨x, hxs, htx, hkx⟩ := exists_le_card hk (t < ·) hcard
+    exact htx.trans_le (le_kthLargest_of_le_card hxs hkx)
+
+/-- **The `k`-th largest value is at least `t > 0`** exactly when at least `k > 0` values are. -/
+theorem le_kthLargest_iff (hk : 0 < k) (ht : 0 < t) :
+    t ≤ kthLargest k s h ↔ k ≤ #{x ∈ s | t ≤ h x} := by
+  constructor
+  · intro hle
+    obtain ⟨a, ha, hta⟩ : ∃ a ∈ _, t ≤ a := ⟨_, max'_mem _ _, hle⟩
+    rcases mem_insert.mp ha with rfl | ha
+    · exact absurd ht (not_lt.mpr hta)
+    obtain ⟨x, hx, rfl⟩ := mem_image.mp ha
+    obtain ⟨-, hkx⟩ := mem_filter.mp hx
+    exact hkx.trans (card_le_card fun w hw => by
+      obtain ⟨hws, hxw⟩ := mem_filter.mp hw
+      exact mem_filter.mpr ⟨hws, hta.trans hxw⟩)
+  · intro hcard
+    obtain ⟨x, hxs, htx, hkx⟩ := exists_le_card hk (t ≤ ·) hcard
+    exact htx.trans (le_kthLargest_of_le_card hxs hkx)
+
+end Finset

Complexity/Foundations/LinearAlgebra/Matrix/CopyStage.lean

@@ -8,6 +8,7 @@ module
 -- upstream: candidate
 
 public import Complexity.Foundations.LinearAlgebra.Matrix.FactorialTruncation
+import Complexity.Foundations.LinearAlgebra.Matrix.PilotCorrection
 import Mathlib.Algebra.BigOperators.Fin
 
 /-!
@@ -95,73 +96,33 @@ variable {V : Type*} [Fintype V] {φ : V → ℝ → ℝ} {C : Matrix V V ℝ} {
 variable (hC0 : ∀ x y, 0 ≤ C x y) (hφ0 : ∀ y t, 0 ≤ φ y t)
   (hφθ : ∀ y t, φ y t ≤ max (t - θ * f) 0) (hθf : 0 ≤ θ * f)
 
-omit [Fintype V] in
-include hφθ hθf in
-private theorem cutoff_le_self' (y : V) {t : ℝ} (ht : 0 ≤ t) : φ y t ≤ t :=
-  (hφθ y t).trans (max_le (by linarith) ht)
-
 omit [Fintype V] in
 include hφ0 hφθ hθf in
 private theorem cutoff_zero (y : V) : φ y 0 = 0 :=
   le_antisymm ((hφθ y 0).trans (max_le (by linarith) le_rfl)) (hφ0 y 0)
 
-include hC0 hφ0 hφθ hθf in
-private theorem iter_succ_le_input (k : ℕ) (x y : V) :
-    cutoffCorrectionIter φ C (k + 1) x y ≤ (C + cutoffCorrectionIter φ C k * C) x y := by
-  rw [cutoffCorrectionIter_succ]
-  exact cutoff_le_self' hφθ hθf y <| add_nonneg (hC0 x y) <| Finset.sum_nonneg fun z _ =>
-    mul_nonneg (cutoffCorrectionIter_nonneg hφ0 k x z) (hC0 z y)
-
 include hC0 hφ0 hφθ hθf in
 /-- **Row sums of the iterates**: the `k`-th iterate of a cutoff correction of a substochastic
 `C` has row sums at most `k` [OpenAI2026LogSpace, Lemma 4.2]. -/
 theorem cutoffCorrectionIter_sum_le (hC1 : C *ᵥ 1 ≤ 1) (k : ℕ) (x : V) :
-    ∑ y, cutoffCorrectionIter φ C k x y ≤ k := by
-  have hrow : ∀ z, ∑ y, C z y ≤ 1 := fun z => by simpa [mulVec, dotProduct] using hC1 z
-  induction k with
-  | zero => simp [cutoffCorrectionIter]
-  | succ k ih =>
-    set F := cutoffCorrectionIter φ C k
-    calc ∑ y, cutoffCorrectionIter φ C (k + 1) x y ≤ ∑ y, (C + F * C) x y :=
-          Finset.sum_le_sum fun y _ => iter_succ_le_input hC0 hφ0 hφθ hθf k x y
-      _ = ∑ y, C x y + ∑ z, F x z * ∑ y, C z y := by
-          simp only [Matrix.add_apply, Matrix.mul_apply, Finset.sum_add_distrib, Finset.mul_sum]
-          rw [Finset.sum_comm]
-      _ ≤ 1 + ∑ z, F x z * 1 := add_le_add (hrow x) (Finset.sum_le_sum fun z _ =>
-          mul_le_mul_of_nonneg_left (hrow z) (cutoffCorrectionIter_nonneg hφ0 k x z))
-      _ ≤ (k + 1 : ℕ) := by simp only [mul_one]; push_cast; linarith
-
-include hC0 hφ0 hφθ hθf in
-/-- The input `(C + E_k C) x y` of the `(k + 1)`-th step is at most `(k + 1) f`. -/
-private theorem input_le (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f) (hC1 : C *ᵥ 1 ≤ 1) (k : ℕ)
-    (x y : V) : (C + cutoffCorrectionIter φ C k * C) x y ≤ (k + 1) * f := by
-  have hsum := cutoffCorrectionIter_sum_le hC0 hφ0 hφθ hθf hC1 k x
-  calc (C + cutoffCorrectionIter φ C k * C) x y
-      = C x y + ∑ z, cutoffCorrectionIter φ C k x z * C z y := rfl
-    _ ≤ f + ∑ z, cutoffCorrectionIter φ C k x z * f := add_le_add (hCf x y)
-        (Finset.sum_le_sum fun z _ =>
-          mul_le_mul_of_nonneg_left (hCf z y) (cutoffCorrectionIter_nonneg hφ0 k x z))
-    _ ≤ (k + 1) * f := by rw [← Finset.sum_mul]; nlinarith
+    ∑ y, cutoffCorrectionIter φ C k x y ≤ k :=
+  (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).sum_le hC1 k x
 
 include hC0 hφ0 hφθ hθf in
 /-- **Entries of the iterates**: the `k`-th iterate has entries at most `k f`
 [OpenAI2026LogSpace, Lemma 4.2]. -/
 theorem cutoffCorrectionIter_le_mul (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f) (hC1 : C *ᵥ 1 ≤ 1)
-    (k : ℕ) (x y : V) : cutoffCorrectionIter φ C k x y ≤ k * f := by
-  cases k with
-  | zero => simp [cutoffCorrectionIter]
-  | succ k =>
-    push_cast
-    exact (iter_succ_le_input hC0 hφ0 hφθ hθf k x y).trans
-      (input_le hC0 hφ0 hφθ hθf hCf hf hC1 k x y)
+    (k : ℕ) (x y : V) : cutoffCorrectionIter φ C k x y ≤ k * f :=
+  (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).le_mul hCf hf hC1 k x y
 
 include hC0 hφ0 hφθ hθf in
 /-- **The residual entry bound**: `C - E_k + E_k C` has entries at most `(k + 1) f`
 [OpenAI2026LogSpace, Lemma 4.4]. -/
 theorem cutoffCorrection_residual_le_mul (hCf : ∀ x y, C x y ≤ f) (hf : 0 ≤ f)
     (hC1 : C *ᵥ 1 ≤ 1) (k : ℕ) (x y : V) :
     (C - cutoffCorrectionIter φ C k + cutoffCorrectionIter φ C k * C) x y ≤ (k + 1) * f := by
-  have h := input_le hC0 hφ0 hφθ hθf hCf hf hC1 k x y
+  have h := (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).input_le_mul hCf hf hC1 k
+    x y
   have h0 := cutoffCorrectionIter_nonneg (C := C) hφ0 k x y
   simp only [Matrix.add_apply, Matrix.sub_apply] at h ⊢
   linarith
@@ -180,12 +141,13 @@ theorem cutoffCorrection_residual_dominates (hCf : ∀ x y, C x y ≤ f) (hf : 0
   have ha0 : 0 ≤ (C + cutoffCorrectionIter φ C k * C) x y :=
     add_nonneg (hC0 x y) (Finset.sum_nonneg fun z _ =>
       mul_nonneg (cutoffCorrectionIter_nonneg hφ0 k x z) (hC0 z y))
-  have ha := input_le hC0 hφ0 hφθ hθf hCf hf hC1 k x y
+  have ha := (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).input_le_mul hCf hf hC1 k
+    x y
   have hEa : cutoffCorrectionIter φ C (k + 1) x y =
       φ y ((C + cutoffCorrectionIter φ C k * C) x y) := by
     rw [cutoffCorrectionIter_succ]; rfl
   have he0 := cutoffCorrectionIter_nonneg (C := C) hφ0 (k + 1) x y
-  have hea := iter_succ_le_input hC0 hφ0 hφθ hθf k x y
+  have hea := (isCorrectionSeq_cutoffCorrectionIter hC0 hφ0 hφθ hθf).le_input k x y
   have hFE : (cutoffCorrectionIter φ C k * C) x y ≤ (cutoffCorrectionIter φ C (k + 1) * C) x y :=
     Finset.sum_le_sum fun z _ =>
       mul_le_mul_of_nonneg_right (cutoffCorrectionIter_le_succ hC0 hφ0 hφm k x z) (hC0 z y)