feat(logspace): prove exact sentinel compression invariance

Complexity.lean

@@ -2425,6 +2425,7 @@ public import Complexity.Foundations.Analysis.RowCompression.Floors
 public import Complexity.Foundations.Analysis.RowCompression.Iteration
 public import Complexity.Foundations.Analysis.RowCompression.Preloss
 public import Complexity.Foundations.Analysis.RowCompression.Reference
+public import Complexity.Foundations.Analysis.RowCompression.Sentinel
 public import Complexity.Foundations.Analysis.RowCompression.Stationary
 public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos
 public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch

Complexity/Foundations/Analysis/RowCompression/Sentinel.lean

@@ -0,0 +1,184 @@
+/-
+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.Analysis.RowCompression.Reference
+import Mathlib.Tactic.Linarith
+
+/-!
+# Exact sentinel replacement under row compression
+
+Replace the first coordinate at a finite set of marked endpoints by one common positive
+sentinel, leaving every second coordinate unchanged. When the modified first rank and size
+threshold are at most `R ≥ 0`, and both old and sentinel first coordinates at marked endpoints
+are strictly above `3R`, the original and modified calculations have identical ranks, thresholds,
+and new defaults. Compression is identity in both channels at marked endpoints, and sentinel
+replacement commutes with the actual update on every retained endpoint.
+
+The proof uses `Finset.kthLargest_eq_of_eq_or_gt`, including its boundary case where a rank equals
+the ceiling. It preserves actual padded ranks, rather than only clipped ranks. No bound on the
+largest original entry is needed. The modified first-rank bound also implies that fewer than
+`K` retained endpoints can be marked.
+
+This is the exact rank and update step in the sentinel argument of [OpenAI2026LogSpace,
+Lemma 8.3], when the proof removes its modification of first coordinates above `L₁`. It does not
+identify or store sentinels in the algorithm. Maintaining the large-coordinate bounds through
+later increments, iterating the comparison, upper saturation of row outputs, and the full
+post-overflow stability estimate remain separate. No root exponent or machine-resource bound
+is asserted here.
+
+## Main definitions
+
+* `Cslib.RowCompression.sentinelFirst`: change only the marked first coordinates.
+
+## Main results
+
+* `Cslib.RowCompression.firstRank_eq_sentinelFirst`,
+  `Cslib.RowCompression.threshold_eq_sentinelFirst`,
+  `Cslib.RowCompression.newDefault_eq_sentinelFirst`: exact invariance below the ceiling.
+* `Cslib.RowCompression.update_eq_self_of_mem_sentinelFirst`: both channels at marked endpoints
+  are in the actual compression identity region.
+* `Cslib.RowCompression.sentinelFirst_update`: one-step commutation on retained endpoints.
+
+## References
+
+* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace],
+  Section 8.3, proof of Lemma 8.3, the sentinel replacement and its removal
+  (23 September 2026, revision `7ef5c0cc`, not peer reviewed).
+-/
+
+public section
+
+namespace Cslib.RowCompression
+
+open Finset
+
+variable {ι : Type*}
+
+open scoped Classical in
+/-- Replace marked first coordinates by one sentinel, keeping every second coordinate. -/
+@[expose] noncomputable def sentinelFirst (marked : Finset ι) (L : ℝ)
+    (w : ι → Fin 2 → ℝ) (y : ι) (ν : Fin 2) : ℝ :=
+  if y ∈ marked ∧ ν = 0 then L else w y ν
+
+variable {s marked : Finset ι} {n K : ℕ} {ρ z R L : ℝ} {w : ι → Fin 2 → ℝ} {y : ι}
+
+theorem sentinelFirst_zero_of_mem (hy : y ∈ marked) : sentinelFirst marked L w y 0 = L := by
+  simp [sentinelFirst, hy]
+
+theorem sentinelFirst_one : sentinelFirst marked L w y 1 = w y 1 := by
+  simp [sentinelFirst]
+
+theorem sentinelFirst_of_not_mem (hy : y ∉ marked) : sentinelFirst marked L w y = w y := by
+  funext ν
+  simp [sentinelFirst, hy]
+
+/-- A padded first rank below the ceiling is unchanged by replacing larger first coordinates. -/
+theorem firstRank_eq_sentinelFirst (hK : 0 < K) (hR : 0 ≤ R) (hL : R < L)
+    (hw : ∀ y ∈ s, y ∈ marked → R < w y 0)
+    (hq : firstRank s K z (sentinelFirst marked L w) ≤ R) :
+    firstRank s K z w = firstRank s K z (sentinelFirst marked L w) := by
+  have hrank : kthLargest K s (fun y => w y 0) =
+      kthLargest K s (fun y => sentinelFirst marked L w y 0) := by
+    apply kthLargest_eq_of_eq_or_gt hK hR _ (kthLargest_le_firstRank.trans hq)
+    intro y hy
+    by_cases hm : y ∈ marked
+    · exact Or.inr ⟨hw y hy hm, by rwa [sentinelFirst_zero_of_mem hm]⟩
+    · exact Or.inl (congrFun (sentinelFirst_of_not_mem hm) 0).symm
+  exact congrArg (max z) hrank
+
+/-- The actual size threshold is unchanged, including its floor and old-default terms. -/
+theorem threshold_eq_sentinelFirst (hn : 0 < n) (hR : 0 ≤ R) (hL : R < L)
+    (hw : ∀ y ∈ s, y ∈ marked → R < w y 0)
+    (hu : threshold s n ρ z (sentinelFirst marked L w) ≤ R) :
+    threshold s n ρ z w = threshold s n ρ z (sentinelFirst marked L w) := by
+  have hrank : kthLargest n s (fun y => entrySize (w y)) =
+      kthLargest n s (fun y => entrySize (sentinelFirst marked L w y)) := by
+    apply kthLargest_eq_of_eq_or_gt hn hR _
+      (((le_max_right _ _).trans (le_max_right _ _)).trans hu)
+    intro y hy
+    by_cases hm : y ∈ marked
+    · refine Or.inr ⟨(hw y hy hm).trans_le
+        ((le_abs_self _).trans (abs_apply_le_entrySize _ 0)), ?_⟩
+      have hs : R < sentinelFirst marked L w y 0 := by rwa [sentinelFirst_zero_of_mem hm]
+      exact hs.trans_le ((le_abs_self _).trans (abs_apply_le_entrySize _ 0))
+    · exact Or.inl (congrArg entrySize (sentinelFirst_of_not_mem hm)).symm
+  exact congrArg (fun q => max z (max ρ q)) hrank
+
+/-- Both actual rank quantities, and consequently the new default, agree exactly. -/
+theorem newDefault_eq_sentinelFirst (hn : 0 < n) (hK : 0 < K) (hR : 0 ≤ R) (hL : R < L)
+    (hw : ∀ y ∈ s, y ∈ marked → R < w y 0)
+    (hq : firstRank s K z (sentinelFirst marked L w) ≤ R)
+    (hu : threshold s n ρ z (sentinelFirst marked L w) ≤ R) :
+    newDefault s n K ρ z w = newDefault s n K ρ z (sentinelFirst marked L w) := by
+  change max (threshold s n ρ z w) (min (firstRank s K z w) (3 * threshold s n ρ z w)) =
+    max (threshold s n ρ z (sentinelFirst marked L w))
+      (min (firstRank s K z (sentinelFirst marked L w))
+        (3 * threshold s n ρ z (sentinelFirst marked L w)))
+  rw [threshold_eq_sentinelFirst hn hR hL hw hu, firstRank_eq_sentinelFirst hK hR hL hw hq]
+
+/-- The bounded modified first rank itself forces strict cardinality of the marked set. -/
+theorem card_marked_lt_of_sentinelFirst (hK : 0 < K) (hR : 0 ≤ R) (hL : R < L)
+    (hmarked : marked ⊆ s) (hq : firstRank s K z (sentinelFirst marked L w) ≤ R) :
+    #marked < K := by
+  classical
+  refine not_le.mp fun hc => ?_
+  have hsub : marked ⊆ {y ∈ s | R < sentinelFirst marked L w y 0} := by
+    intro y hy
+    exact mem_filter.mpr ⟨hmarked hy, by rwa [sentinelFirst_zero_of_mem hy]⟩
+  have hlt := (lt_kthLargest_iff hK hR).mpr (hc.trans (card_le_card hsub))
+  exact (not_lt_of_ge (kthLargest_le_firstRank.trans hq)) hlt
+
+/-- Original and sentinel entries are both in the identity region at every marked retained ID.
+The second coordinate is untouched, even if it is signed or large. -/
+theorem update_eq_self_of_mem_sentinelFirst (hn : 0 < n) (hR : 0 ≤ R) (hL : 3 * R < L)
+    (hw : ∀ y ∈ s, y ∈ marked → 3 * R < w y 0)
+    (hu : threshold s n ρ z (sentinelFirst marked L w) ≤ R)
+    (hy : y ∈ s) (hm : y ∈ marked) :
+    update s n K ρ z w y = w y ∧
+      update s n K ρ z (sentinelFirst marked L w) y = sentinelFirst marked L w y := by
+  have hL' : R < L := by linarith
+  have hw' : ∀ y ∈ s, y ∈ marked → R < w y 0 := by
+    intro y hy hm
+    linarith [hw y hy hm]
+  have hu' : threshold s n ρ z w ≤ R :=
+    (threshold_eq_sentinelFirst hn hR hL' hw' hu).trans_le hu
+  constructor
+  · apply update_eq_self_of_three_mul_le
+    exact (by linarith [hw y hy hm] : 3 * threshold s n ρ z w ≤ w y 0).trans
+      ((le_abs_self _).trans (abs_apply_le_entrySize _ 0))
+  · apply update_eq_self_of_three_mul_le
+    have hfirst : 3 * R < sentinelFirst marked L w y 0 := by
+      rwa [sentinelFirst_zero_of_mem hm]
+    exact (by linarith : 3 * threshold s n ρ z (sentinelFirst marked L w) ≤
+      sentinelFirst marked L w y 0).trans ((le_abs_self _).trans (abs_apply_le_entrySize _ 0))
+
+/-- Sentinel replacement commutes with the concrete compression update on every retained ID.
+This also gives equality of both channels off the marked set; it assumes no row-output law. -/
+theorem sentinelFirst_update (hK : 0 < K) (hKn : K ≤ n) (hR : 0 ≤ R) (hL : 3 * R < L)
+    (hw : ∀ y ∈ s, y ∈ marked → 3 * R < w y 0)
+    (hq : firstRank s K z (sentinelFirst marked L w) ≤ R)
+    (hu : threshold s n ρ z (sentinelFirst marked L w) ≤ R) (hy : y ∈ s) :
+    sentinelFirst marked L (update s n K ρ z w) y =
+      update s n K ρ z (sentinelFirst marked L w) y := by
+  have hn : 0 < n := hK.trans_le hKn
+  by_cases hm : y ∈ marked
+  · obtain ⟨ho, hs⟩ := update_eq_self_of_mem_sentinelFirst hn hR hL hw hu hy hm
+    rw [hs]
+    funext ν
+    simp only [sentinelFirst, ho]
+  · have hL' : R < L := by linarith
+    have hw' : ∀ y ∈ s, y ∈ marked → R < w y 0 := by
+      intro y hy hm
+      linarith [hw y hy hm]
+    rw [sentinelFirst_of_not_mem hm]
+    unfold update
+    rw [threshold_eq_sentinelFirst hn hR hL' hw' hu,
+      newDefault_eq_sentinelFirst hn hK hR hL' hw' hq hu, sentinelFirst_of_not_mem hm]
+
+end Cslib.RowCompression

Complexity/Foundations/Data/Finset/KthLargest.lean

@@ -1,7 +1,7 @@
 /-
-Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Christian Reitwiessner
+Authors: Christian Reitwiessner, Samuel Schlesinger
 -/
 
 module
@@ -32,6 +32,7 @@ is at least `t` exactly when at least `k` values are at least `t` (`Finset.le_kt
 
 * `Finset.kthLargest_nonneg`, `Finset.kthLargest_le`: bounds.
 * `Finset.lt_kthLargest_iff`, `Finset.le_kthLargest_iff`: the threshold characterizations.
+* `Finset.kthLargest_eq_of_eq_or_gt`: replacing values strictly above a bounded rank preserves it.
 * `Finset.kthLargest_le_kthLargest_add`, `Finset.abs_kthLargest_sub_kthLargest_le`: stability
   under perturbation of the values.
 
@@ -116,6 +117,35 @@ theorem le_kthLargest_iff (hk : 0 < k) (ht : 0 < t) :
     obtain ⟨x, hxs, htx, hkx⟩ := exists_le_card hk (t ≤ ·) hcard
     exact htx.trans (le_kthLargest_of_le_card hxs hkx)
 
+/-- Changing only values strictly above a nonnegative ceiling preserves every positive-order
+rank at most that ceiling. The bound may be an equality, and other values may be negative. -/
+theorem kthLargest_eq_of_eq_or_gt {f g : α → R} (hk : 0 < k) (ht : 0 ≤ t)
+    (h : ∀ x ∈ s, f x = g x ∨ (t < f x ∧ t < g x))
+    (hg : kthLargest k s g ≤ t) : kthLargest k s f = kthLargest k s g := by
+  classical
+  have hfilter (a : R) (ha : a ≤ t) :
+      ({x ∈ s | a < f x} : Finset α) = {x ∈ s | a < g x} := by
+    ext x
+    by_cases hx : x ∈ s
+    · rcases h x hx with heq | ⟨hf, hg⟩
+      · simp [heq]
+      · simp [hx, ha.trans_lt hf, ha.trans_lt hg]
+    · simp [hx]
+  have hf : kthLargest k s f ≤ t := by
+    refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff hk ht).mp hlt
+    rw [hfilter t le_rfl] at hc
+    exact (not_lt_of_ge hg) ((lt_kthLargest_iff hk ht).mpr hc)
+  apply le_antisymm
+  · refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff hk kthLargest_nonneg).mp hlt
+    rw [hfilter _ hg] at hc
+    exact lt_irrefl _ ((lt_kthLargest_iff hk kthLargest_nonneg).mpr hc)
+  · refine not_lt.mp fun hlt => ?_
+    have hc := (lt_kthLargest_iff hk kthLargest_nonneg).mp hlt
+    rw [← hfilter _ hf] at hc
+    exact lt_irrefl _ ((lt_kthLargest_iff hk kthLargest_nonneg).mpr hc)
+
 section Stability
 
 variable {R : Type*} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] {k : ℕ}

ComplexityTests/RowCompressionSentinel.lean

@@ -0,0 +1,131 @@
+/-
+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.Foundations.Analysis.RowCompression.Sentinel
+import Mathlib.LinearAlgebra.Matrix.Notation
+import Mathlib.Tactic.FinCases
+import Mathlib.Tactic.NormNum
+
+/-!
+# Exact sentinel compression examples
+
+Replacing the first entry `1000000` by `100` preserves a third rank and size threshold exactly
+at their ceiling `2`. The old default is positive. Compression changes smaller signed entries,
+while the marked entry's negative second coordinate `-17` is unchanged in both calculations.
+Further cases check zero padding and why changing values exactly at the ceiling is excluded.
+-/
+
+namespace ComplexityTests.RowCompressionSentinel
+
+open Finset Cslib.RowCompression
+
+private def original : Fin 4 → Fin 2 → ℝ := ![![1000000, -17], ![4, 0], ![2, -1], ![-1, 1]]
+
+private noncomputable def modified : Fin 4 → Fin 2 → ℝ := sentinelFirst {0} 100 original
+
+private theorem modified_rank : firstRank univ 3 (1 / 2) modified = 2 := by
+  norm_num [firstRank, kthLargest, modified, original, sentinelFirst, Fin.univ_succ,
+    filter_insert, filter_singleton]
+
+private theorem modified_threshold : threshold univ 3 1 (1 / 2) modified = 2 := by
+  norm_num [threshold, kthLargest, entrySize, modified, original, sentinelFirst, Fin.univ_succ,
+    filter_insert, filter_singleton]
+
+private theorem marked_high : ∀ y ∈ (univ : Finset (Fin 4)), y ∈ ({0} : Finset (Fin 4)) →
+    (3 : ℝ) * 2 < original y 0 := by
+  intro y _ hy
+  have hy0 : y = 0 := mem_singleton.mp hy
+  subst y
+  norm_num [original]
+
+private theorem marked_above : ∀ y ∈ (univ : Finset (Fin 4)), y ∈ ({0} : Finset (Fin 4)) →
+    (2 : ℝ) < original y 0 := by
+  intro y _ hy
+  have hy0 : y = 0 := mem_singleton.mp hy
+  subst y
+  norm_num [original]
+
+private theorem original_rank : firstRank univ 3 (1 / 2) original = 2 := by
+  rw [firstRank_eq_sentinelFirst (marked := {0}) (L := 100) (R := 2)
+    (by norm_num) (by norm_num) (by norm_num) marked_above modified_rank.le]
+  exact modified_rank
+
+private theorem original_threshold : threshold univ 3 1 (1 / 2) original = 2 := by
+  rw [threshold_eq_sentinelFirst (marked := {0}) (L := 100) (R := 2)
+    (by norm_num) (by norm_num) (by norm_num) marked_above modified_threshold.le]
+  exact modified_threshold
+
+private theorem modified_default : newDefault univ 3 3 1 (1 / 2) modified = 2 := by
+  change max (threshold univ 3 1 (1 / 2) modified)
+    (min (firstRank univ 3 (1 / 2) modified) (3 * threshold univ 3 1 (1 / 2) modified)) = 2
+  rw [modified_threshold, modified_rank]
+  norm_num
+
+private theorem original_default : newDefault univ 3 3 1 (1 / 2) original = 2 := by
+  rw [newDefault_eq_sentinelFirst (marked := {0}) (L := 100) (R := 2)
+    (by norm_num) (by norm_num) (by norm_num) (by norm_num)
+    marked_above modified_rank.le modified_threshold.le]
+  exact modified_default
+
+-- Both ranks meet the ceiling exactly; the old default is neither zero nor the new default.
+example : firstRank univ 3 (1 / 2) original = 2 ∧
+    threshold univ 3 1 (1 / 2) original = 2 ∧
+    newDefault univ 3 3 1 (1 / 2) original = 2 :=
+  ⟨original_rank, original_threshold, original_default⟩
+
+-- This is the actual commutation theorem, with every structural hypothesis discharged.
+example (y : Fin 4) : sentinelFirst {0} 100 (update univ 3 3 1 (1 / 2) original) y =
+    update univ 3 3 1 (1 / 2) modified y := by
+  exact sentinelFirst_update (R := 2) (by norm_num) (by norm_num) (by norm_num)
+    (by norm_num) marked_high modified_rank.le modified_threshold.le (mem_univ y)
+
+-- Both channels of the marked entry survive, even though its second coordinate is negative.
+example : update univ 3 3 1 (1 / 2) original 0 = ![1000000, -17] ∧
+    update univ 3 3 1 (1 / 2) modified 0 = ![100, -17] := by
+  have h := update_eq_self_of_mem_sentinelFirst (K := 3) (R := 2)
+    (by norm_num) (by norm_num) (by norm_num) marked_high modified_threshold.le
+    (mem_univ 0) (mem_singleton_self 0)
+  refine ⟨h.1, h.2.trans ?_⟩
+  funext ν
+  fin_cases ν <;> norm_num [sentinelFirst, original]
+
+-- The step is not identity on the whole row: these signed coordinates really change.
+example : original 2 1 = -1 ∧ original 3 0 = -1 ∧
+    update univ 3 3 1 (1 / 2) original 2 = ![2, 0] ∧
+    update univ 3 3 1 (1 / 2) original 3 = ![2, 0] := by
+  have h2 : update univ 3 3 1 (1 / 2) original 2 = ![2, 0] := by
+    unfold update
+    rw [original_threshold, original_default]
+    funext ν
+    fin_cases ν <;> norm_num [updateEntry, radius, entrySize, defaultEntry, original]
+  have h3 : update univ 3 3 1 (1 / 2) original 3 = ![2, 0] := by
+    unfold update
+    rw [original_threshold, original_default]
+    funext ν
+    fin_cases ν <;> norm_num [updateEntry, radius, entrySize, defaultEntry, original]
+  exact ⟨by norm_num [original], by norm_num [original], h2, h3⟩
+
+-- The rank bound proves the strict capacity of the marked set, rather than assuming it.
+example : #({0} : Finset (Fin 4)) < 3 :=
+  card_marked_lt_of_sentinelFirst (R := 2) (w := original) (by norm_num) (by norm_num)
+    (by norm_num : (2 : ℝ) < 100) (subset_univ _) modified_rank.le
+
+-- Arbitrarily large positive replacement values cannot defeat zero padding when K > #s.
+example : kthLargest 3 univ (![(-4 : ℝ), 1000000] : Fin 2 → ℝ) = 0 := by
+  have h := kthLargest_eq_of_eq_or_gt (k := 3) (s := univ) (t := (0 : ℝ))
+    (f := (![-4, 1000000] : Fin 2 → ℝ)) (g := (![-4, 10] : Fin 2 → ℝ))
+    (by norm_num) (by norm_num)
+    (fun y _ => by fin_cases y <;> norm_num)
+    (by norm_num [kthLargest, Fin.univ_succ, filter_insert, filter_singleton])
+  rw [h]
+  norm_num [kthLargest, Fin.univ_succ, filter_insert, filter_singleton]
+
+-- Strictness above the ceiling matters: replacing a value by the ceiling can change the rank.
+example : kthLargest 1 univ (![(5 : ℝ), 4] : Fin 2 → ℝ) = 5 ∧
+    kthLargest 1 univ (![(4 : ℝ), 4] : Fin 2 → ℝ) = 4 := by
+  norm_num [kthLargest, Fin.univ_succ, filter_insert, filter_singleton]
+
+end ComplexityTests.RowCompressionSentinel