From c3f7a58ac47dd83ab36e9226c2a3a9e96840fe34 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:07:57 +0000 Subject: [PATCH] feat(logspace): prove the local row compression lemma The Phase 4 estimator needs to retain only a bounded list of exceptions without losing stability when that list changes. Formalize the native two-coordinate compression update of OpenAI2026LogSpace Section 8.2, equations (8.5)-(8.6), and all conclusions of Lemma 8.1. Prove small-entry replacement, signed large-entry preservation, coordinatewise interpolation, monotone defaults, strict candidate capacity and containment, and uniform 28-Lipschitz stability. Also prove the local 6u change bound used by the subsequent preloss argument. Add concrete tests of partial clipping, signed values, positive-default padding, empty rows, candidate selection and perturbations. This advances #1721 and #1444. Iterated propagation and its slack conversion (8.7), rarity estimates, recursive estimation and machine-space realization remain open. No selected formal abstract or roadmap endpoint changes. Validation on Lean v4.36.0-rc2, based on main ef811c832d4ac280d1655cf4b8d89d32f5c39da0: - Strict focused build of the module and concrete tests passed. - scripts/check.sh passed all six gates: strict full build, mk_all check, strict full tests (including the global axiom audit), lint, lint-style, and checkInitImports. - check_changed_files.py, check_tidy_surface.py, and check_hygiene.py passed. - Focused hygiene with --check-simp and git diff --check passed. Independent non-author review: Codex agent /root/compression_review approved source tree e70d93b914c6cef421eb3ee4171e40daae6073b4, including primary-source correspondence, APIs, boundary cases, tests and the one-step change bound. No requested fixes remain. This is agent review, not human approval. Worker: codex-row-compression-20261030, branch feat/logspace-compression-update. AI assistance: OpenAI Codex implementation and independent Codex review. --- Complexity.lean | 1 + .../Foundations/Analysis/RowCompression.lean | 369 ++++++++++++++++++ ComplexityTests/RowCompression.lean | 102 +++++ 3 files changed, 472 insertions(+) create mode 100644 Complexity/Foundations/Analysis/RowCompression.lean create mode 100644 ComplexityTests/RowCompression.lean diff --git a/Complexity.lean b/Complexity.lean index e9ed8c9a2..69f36f90f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2351,6 +2351,7 @@ public import Complexity.Foundations.Analysis.LpNorm public import Complexity.Foundations.Analysis.LpNormMeasure public import Complexity.Foundations.Analysis.MarkovBrothersInequality public import Complexity.Foundations.Analysis.RootError +public import Complexity.Foundations.Analysis.RowCompression public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli diff --git a/Complexity/Foundations/Analysis/RowCompression.lean b/Complexity/Foundations/Analysis/RowCompression.lean new file mode 100644 index 000000000..6e5dd8611 --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression.lean @@ -0,0 +1,369 @@ +/- +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.Finset.KthLargest +public import Mathlib.Basic.Real.Basic +import Mathlib.Algebra.Order.Group.MinMax +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Compression of two-coordinate rows + +The local update of [OpenAI2026LogSpace, Section 8.2, (8.5)--(8.6), Lemma 8.1] replaces a +real row by a common default and a bounded number of exceptions. This is the deterministic +compression step of the logspace estimator; no probability or machine-space bound is asserted. + +For an old default `(z, 0)`, a floor `ρ`, and an input row `w`, put +`m y = max |w y 0| |w y 1|` and `u = max z (max ρ (rank_n m))`. The new default is +`z' = max u (min (max z (rank_K (w · 0))) (3 * u))`. Every displacement from `(z', 0)` +is clipped to radius `7 * max (m y - 2 * u) 0`. + +`Finset.kthLargest` pads with zeros. For a nonnegative old default `z`, taking `max z` of this +rank accounts for the paper's dummy copies of `(z, 0)`. In the size rank this maximum is already +absorbed by `u`. The finite set `s` consists of real endpoint IDs; dummy positions never enter +the support count. Input coordinates may be negative. Positive `n` and `K` suffice for stability; +the later condition `K ≤ n` is not needed for this local result. + +## Main definitions + +* `Cslib.RowCompression.threshold`, `Cslib.RowCompression.newDefault`: the thresholds. +* `Cslib.RowCompression.update`: the compressed row, as a mathematical function. +* `Cslib.RowCompression.candidates`: a list of possible exceptions, selected by input size. + +## Main results + +* `Cslib.RowCompression.update_eq_default_of_size_le`: small entries become default. +* `Cslib.RowCompression.update_eq_self_of_three_mul_le`: large entries are unchanged. +* `Cslib.RowCompression.update_mem_Icc`: each coordinate lies between input and default. +* `Cslib.RowCompression.abs_update_sub_le_six_mul`: one update changes a coordinate by at most + six times its threshold, the local bound used in the subsequent preloss argument. +* `Cslib.RowCompression.le_newDefault`: defaults are nondecreasing. +* `Cslib.RowCompression.card_candidates_lt`: fewer than `n` candidates suffice. +* `Cslib.RowCompression.update_eq_default_of_not_mem_candidates`: the candidate set represents + the entire row on `s`. +* `Cslib.RowCompression.candidates_subset`: candidates come from the previous list and new IDs. +* `Cslib.RowCompression.abs_update_sub_update_le`: the full update is uniformly 28-Lipschitz. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.2, (8.5)--(8.6), Lemma 8.1 (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} + +/-- The sup norm of a two-coordinate entry. -/ +@[expose] noncomputable def entrySize (w : Fin 2 → ℝ) : ℝ := max |w 0| |w 1| + +/-- The common default entry `(z, 0)`. -/ +@[expose] def defaultEntry (z : ℝ) (ν : Fin 2) : ℝ := if ν = 0 then z else 0 + +/-- The clipping radius for an entry at threshold `u`. -/ +@[expose] noncomputable def radius (u : ℝ) (w : Fin 2 → ℝ) : ℝ := + 7 * max (entrySize w - 2 * u) 0 + +/-- Clip each displacement from `(z, 0)` to the entry's radius. -/ +@[expose] noncomputable def updateEntry (u z : ℝ) (w : Fin 2 → ℝ) (ν : Fin 2) : ℝ := + defaultEntry z ν + max (-radius u w) (min (w ν - defaultEntry z ν) (radius u w)) + +/-- The size threshold, with dummy copies of the old default included in its rank. -/ +@[expose] noncomputable def threshold (s : Finset ι) (n : ℕ) (ρ z : ℝ) + (w : ι → Fin 2 → ℝ) : ℝ := + max z (max ρ (kthLargest n s fun y => entrySize (w y))) + +/-- The new nonnegative default; `max z` accounts for dummy copies in the first-coordinate rank. +For nonnegative `z` this is exactly (8.5) of [OpenAI2026LogSpace]. -/ +@[expose] noncomputable def newDefault (s : Finset ι) (n K : ℕ) (ρ z : ℝ) + (w : ι → Fin 2 → ℝ) : ℝ := + max (threshold s n ρ z w) + (min (max z (kthLargest K s fun y => w y 0)) (3 * threshold s n ρ z w)) + +/-- The compression update of [OpenAI2026LogSpace, (8.6)]. -/ +@[expose] noncomputable def update (s : Finset ι) (n K : ℕ) (ρ z : ℝ) + (w : ι → Fin 2 → ℝ) (y : ι) : Fin 2 → ℝ := + updateEntry (threshold s n ρ z w) (newDefault s n K ρ z w) (w y) + +/-- A coarse candidate list: every non-default output has input size greater than `u`. -/ +@[expose] noncomputable def candidates (s : Finset ι) (n : ℕ) (ρ z : ℝ) + (w : ι → Fin 2 → ℝ) : Finset ι := + {y ∈ s | threshold s n ρ z w < entrySize (w y)} + +variable {s : Finset ι} {n K : ℕ} {ρ z : ℝ} {w : ι → Fin 2 → ℝ} + +theorem entrySize_nonneg (v : Fin 2 → ℝ) : 0 ≤ entrySize v := + (abs_nonneg _).trans (le_max_left _ _) + +theorem abs_apply_le_entrySize (v : Fin 2 → ℝ) (ν : Fin 2) : |v ν| ≤ entrySize v := by + fin_cases ν + · exact le_max_left _ _ + · exact le_max_right _ _ + +@[simp] +theorem entrySize_defaultEntry (hz : 0 ≤ z) : entrySize (defaultEntry z) = z := by + simp [entrySize, defaultEntry, abs_of_nonneg hz, hz] + +theorem radius_nonneg (u : ℝ) (v : Fin 2 → ℝ) : 0 ≤ radius u v := by + unfold radius + positivity + +theorem threshold_nonneg : 0 ≤ threshold s n ρ z w := + kthLargest_nonneg.trans ((le_max_right _ _).trans (le_max_right _ _)) + +theorem le_threshold : z ≤ threshold s n ρ z w := le_max_left _ _ + +theorem floor_le_threshold : ρ ≤ threshold s n ρ z w := + (le_max_left _ _).trans (le_max_right _ _) + +theorem threshold_le_newDefault : threshold s n ρ z w ≤ newDefault s n K ρ z w := + le_max_left _ _ + +theorem newDefault_le_three_mul : newDefault s n K ρ z w ≤ 3 * threshold s n ρ z w := + max_le (by linarith [threshold_nonneg (s := s) (n := n) (ρ := ρ) (z := z) (w := w)]) + (min_le_right _ _) + +theorem le_newDefault : z ≤ newDefault s n K ρ z w := + le_threshold.trans threshold_le_newDefault + +theorem newDefault_nonneg : 0 ≤ newDefault s n K ρ z w := + threshold_nonneg.trans threshold_le_newDefault + +theorem updateEntry_eq_default_of_size_le {u b : ℝ} {v : Fin 2 → ℝ} + (hv : entrySize v ≤ 2 * u) : updateEntry u b v = defaultEntry b := by + funext ν + simp [updateEntry, radius, max_eq_right (sub_nonpos.mpr hv)] + +theorem updateEntry_eq_self_of_three_mul_le {u b : ℝ} {v : Fin 2 → ℝ} + (hu : 0 ≤ u) (hb : 0 ≤ b) (hb' : b ≤ 3 * u) (hv : 3 * u ≤ entrySize v) : + updateEntry u b v = v := by + have hr : radius u v = 7 * (entrySize v - 2 * u) := by + rw [radius, max_eq_left (by linarith)] + funext ν + have hν := abs_apply_le_entrySize v ν + have hd : |defaultEntry b ν| ≤ 3 * u := by + unfold defaultEntry + split_ifs + · simpa [abs_of_nonneg hb] using hb' + · simpa using mul_nonneg (by norm_num : (0 : ℝ) ≤ 3) hu + have hdiff : |v ν - defaultEntry b ν| ≤ radius u v := by + calc |v ν - defaultEntry b ν| ≤ |v ν| + |defaultEntry b ν| := abs_sub _ _ + _ ≤ radius u v := by rw [hr]; linarith + rw [updateEntry, min_eq_left (abs_le.mp hdiff).2, + max_eq_right (abs_le.mp hdiff).1, add_sub_cancel] + +private theorem add_clip_mem_Icc (b x r : ℝ) (hr : 0 ≤ r) : + b + max (-r) (min (x - b) r) ∈ Set.Icc (min x b) (max x b) := by + rcases le_total x b with h | h + · rw [min_eq_left h, max_eq_right h, min_eq_left (by linarith : x - b ≤ r)] + exact ⟨by linarith [le_max_right (-r) (x - b)], + by have := max_le (by linarith : -r ≤ 0) (sub_nonpos.mpr h); linarith⟩ + · rw [min_eq_right h, max_eq_left h] + have hlo : 0 ≤ max (-r) (min (x - b) r) := + (le_min (sub_nonneg.mpr h) hr).trans (le_max_right _ _) + have hhi : max (-r) (min (x - b) r) ≤ x - b := + max_le (by linarith) (min_le_left _ _) + exact ⟨by linarith, by linarith⟩ + +theorem updateEntry_mem_Icc (u b : ℝ) (v : Fin 2 → ℝ) (ν : Fin 2) : + updateEntry u b v ν ∈ Set.Icc (min (v ν) (defaultEntry b ν)) + (max (v ν) (defaultEntry b ν)) := + add_clip_mem_Icc _ _ _ (radius_nonneg _ _) + +/-- Clipping toward the default changes a coordinate by no more than its distance to it. -/ +theorem abs_updateEntry_sub_le (u b : ℝ) (v : Fin 2 → ℝ) (ν : Fin 2) : + |updateEntry u b v ν - v ν| ≤ |v ν - defaultEntry b ν| := by + have h := updateEntry_mem_Icc u b v ν + rcases le_total (v ν) (defaultEntry b ν) with hle | hle + · rw [min_eq_left hle, max_eq_right hle] at h + rw [abs_of_nonneg (sub_nonneg.mpr h.1), abs_of_nonpos (sub_nonpos.mpr hle)] + linarith [h.2] + · rw [min_eq_right hle, max_eq_left hle] at h + rw [abs_of_nonpos (sub_nonpos.mpr h.2), abs_of_nonneg (sub_nonneg.mpr hle)] + linarith [h.1] + +/-- Entries of size at most twice the threshold become the new default. -/ +theorem update_eq_default_of_size_le {y : ι} + (hy : entrySize (w y) ≤ 2 * threshold s n ρ z w) : + update s n K ρ z w y = defaultEntry (newDefault s n K ρ z w) := + updateEntry_eq_default_of_size_le hy + +/-- Entries of size at least three times the threshold are preserved, including signed entries. -/ +theorem update_eq_self_of_three_mul_le {y : ι} + (hy : 3 * threshold s n ρ z w ≤ entrySize (w y)) : update s n K ρ z w y = w y := + updateEntry_eq_self_of_three_mul_le threshold_nonneg newDefault_nonneg newDefault_le_three_mul hy + +/-- Compression moves each coordinate toward the new default without overshooting. -/ +theorem update_mem_Icc (y : ι) (ν : Fin 2) : + update s n K ρ z w y ν ∈ Set.Icc (min (w y ν) (defaultEntry (newDefault s n K ρ z w) ν)) + (max (w y ν) (defaultEntry (newDefault s n K ρ z w) ν)) := + updateEntry_mem_Icc _ _ _ _ + +/-- The local change bound used before the first overflow in [OpenAI2026LogSpace, Section 8.3]. +When the threshold equals the prescribed floor `ρ`, each coordinate changes by at most `6 * ρ`. +This does not yet sum changes over a schedule or prove the later weighted preloss estimate. -/ +theorem abs_update_sub_le_six_mul (y : ι) (ν : Fin 2) : + |update s n K ρ z w y ν - w y ν| ≤ 6 * threshold s n ρ z w := by + by_cases hy : 3 * threshold s n ρ z w ≤ entrySize (w y) + · rw [update_eq_self_of_three_mul_le hy, sub_self, abs_zero] + exact mul_nonneg (by norm_num) threshold_nonneg + have hm : entrySize (w y) < 3 * threshold s n ρ z w := lt_of_not_ge hy + have hb : |defaultEntry (newDefault s n K ρ z w) ν| ≤ 3 * threshold s n ρ z w := by + unfold defaultEntry + split_ifs + · rw [abs_of_nonneg newDefault_nonneg] + exact newDefault_le_three_mul + · simpa using mul_nonneg (by norm_num : (0 : ℝ) ≤ 3) + (threshold_nonneg (s := s) (n := n) (ρ := ρ) (z := z) (w := w)) + calc |update s n K ρ z w y ν - w y ν| + ≤ |w y ν - defaultEntry (newDefault s n K ρ z w) ν| := abs_updateEntry_sub_le _ _ _ _ + _ ≤ |w y ν| + |defaultEntry (newDefault s n K ρ z w) ν| := abs_sub _ _ + _ ≤ 6 * threshold s n ρ z w := by linarith [abs_apply_le_entrySize (w y) ν] + +/-- The coarse candidate list is strictly smaller than the capacity, hence also at most `n`. -/ +theorem card_candidates_lt (hn : 0 < n) : #(candidates s n ρ z w) < n := by + apply Nat.lt_of_not_ge + intro h + have hlt := (lt_kthLargest_iff hn threshold_nonneg).mpr h + exact (not_lt_of_ge ((le_max_right _ _).trans (le_max_right _ _))) hlt + +/-- Outside the candidate list every real endpoint has the new default value. -/ +theorem update_eq_default_of_not_mem_candidates {y : ι} (hy : y ∈ s) + (hnot : y ∉ candidates s n ρ z w) : + update s n K ρ z w y = defaultEntry (newDefault s n K ρ z w) := by + have hle : entrySize (w y) ≤ threshold s n ρ z w := by + simpa only [candidates, mem_filter, hy, true_and, not_lt] using hnot + have hnonneg : 0 ≤ threshold s n ρ z w := threshold_nonneg + exact update_eq_default_of_size_le (by linarith) + +open scoped Classical in +/-- The exact exception set is smaller than `n`, regardless of coincidences with the default. -/ +theorem card_exceptions_lt (hn : 0 < n) : + #{y ∈ s | update s n K ρ z w y ≠ defaultEntry (newDefault s n K ρ z w)} < n := by + refine (card_le_card ?_).trans_lt (card_candidates_lt (s := s) (ρ := ρ) (z := z) (w := w) hn) + intro y hy + simp only [mem_filter] at hy + by_contra h + exact hy.2 (update_eq_default_of_not_mem_candidates hy.1 h) + +/-- Candidates can be selected entirely from any set containing the non-default input IDs. +Use the union of the previous exception list and the newly touched IDs for that set. -/ +theorem candidates_subset (hz : 0 ≤ z) (t : Finset ι) + (hw : ∀ y ∈ s, y ∉ t → w y = defaultEntry z) : candidates s n ρ z w ⊆ t := by + intro y hy + obtain ⟨hys, hy⟩ := mem_filter.mp hy + by_contra hyt + rw [hw y hys hyt, entrySize_defaultEntry hz] at hy + exact (not_lt_of_ge le_threshold) hy + +/-! ## Stability independent of the row width -/ + +private theorem abs_max_sub_max_le {a b c d ε : ℝ} (ha : |a - c| ≤ ε) + (hb : |b - d| ≤ ε) : |max a b - max c d| ≤ ε := + (abs_max_sub_max_le_max _ _ _ _).trans (max_le ha hb) + +private theorem abs_min_sub_min_le {a b c d ε : ℝ} (ha : |a - c| ≤ ε) + (hb : |b - d| ≤ ε) : |min a b - min c d| ≤ ε := + (abs_min_sub_min_le_max _ _ _ _).trans (max_le ha hb) + +theorem abs_entrySize_sub_entrySize_le {v v' : Fin 2 → ℝ} {δ : ℝ} + (h : ∀ ν, |v ν - v' ν| ≤ δ) : |entrySize v - entrySize v'| ≤ δ := + abs_max_sub_max_le ((abs_abs_sub_abs_le _ _).trans (h 0)) + ((abs_abs_sub_abs_le _ _).trans (h 1)) + +theorem abs_defaultEntry_sub_defaultEntry_le {b b' δ : ℝ} (hδ : 0 ≤ δ) + (hb : |b - b'| ≤ δ) (ν : Fin 2) : |defaultEntry b ν - defaultEntry b' ν| ≤ δ := by + unfold defaultEntry + split_ifs + · exact hb + · simpa using hδ + +variable {z' δ : ℝ} {w' : ι → Fin 2 → ℝ} + +/-- The threshold varies by at most the sup perturbation of the row and old default. -/ +theorem abs_threshold_sub_threshold_le (hn : 0 < n) (hδ : 0 ≤ δ) (hz : |z - z'| ≤ δ) + (hw : ∀ y ∈ s, ∀ ν, |w y ν - w' y ν| ≤ δ) : + |threshold s n ρ z w - threshold s n ρ z' w'| ≤ δ := by + refine abs_max_sub_max_le hz (abs_max_sub_max_le (by simpa using hδ) ?_) + exact abs_kthLargest_sub_kthLargest_le hn hδ fun y hy => + abs_entrySize_sub_entrySize_le (hw y hy) + +/-- The default has Lipschitz constant three, uniformly in the capacities and row width. -/ +theorem abs_newDefault_sub_newDefault_le (hn : 0 < n) (hK : 0 < K) (hδ : 0 ≤ δ) + (hz : |z - z'| ≤ δ) (hw : ∀ y ∈ s, ∀ ν, |w y ν - w' y ν| ≤ δ) : + |newDefault s n K ρ z w - newDefault s n K ρ z' w'| ≤ 3 * δ := by + have hu := abs_threshold_sub_threshold_le (ρ := ρ) hn hδ hz hw + have hq : |max z (kthLargest K s fun y => w y 0) - + max z' (kthLargest K s fun y => w' y 0)| ≤ δ := + abs_max_sub_max_le hz (abs_kthLargest_sub_kthLargest_le hK hδ fun y hy => hw y hy 0) + refine abs_max_sub_max_le (hu.trans (by linarith)) + (abs_min_sub_min_le (hq.trans (by linarith)) ?_) + rw [← mul_sub, abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 3)] + exact mul_le_mul_of_nonneg_left hu (by norm_num) + +/-- The radius is 21-Lipschitz jointly in the entry and the threshold. -/ +theorem abs_radius_sub_radius_le {u u' : ℝ} {v v' : Fin 2 → ℝ} (hδ : 0 ≤ δ) + (hu : |u - u'| ≤ δ) (hv : ∀ ν, |v ν - v' ν| ≤ δ) : + |radius u v - radius u' v'| ≤ 21 * δ := by + have hm := abs_entrySize_sub_entrySize_le hv + have hsub : |(entrySize v - 2 * u) - (entrySize v' - 2 * u')| ≤ 3 * δ := by + calc |(entrySize v - 2 * u) - (entrySize v' - 2 * u')| + = |(entrySize v - entrySize v') - 2 * (u - u')| := by congr 1; ring + _ ≤ |entrySize v - entrySize v'| + |2 * (u - u')| := abs_sub _ _ + _ ≤ 3 * δ := by rw [abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 2)]; linarith + have hmax := abs_max_sub_max_le (b := 0) (d := 0) hsub + (by simpa using (show 0 ≤ 3 * δ by positivity)) + unfold radius + rw [← mul_sub, abs_mul, abs_of_pos (by norm_num : (0 : ℝ) < 7)] + linarith + +/-- The update is 28-Lipschitz in the row and old default, with the floor and capacities fixed. +The estimate is on real endpoints `y ∈ s`; it is independent of their number and magnitudes. -/ +theorem abs_update_sub_update_le (hn : 0 < n) (hK : 0 < K) (hδ : 0 ≤ δ) + (hz : |z - z'| ≤ δ) (hw : ∀ y ∈ s, ∀ ν, |w y ν - w' y ν| ≤ δ) + {y : ι} (hy : y ∈ s) (ν : Fin 2) : + |update s n K ρ z w y ν - update s n K ρ z' w' y ν| ≤ 28 * δ := by + have hu := abs_threshold_sub_threshold_le (ρ := ρ) hn hδ hz hw + have hb := abs_newDefault_sub_newDefault_le (ρ := ρ) hn hK hδ hz hw + have hbν := abs_defaultEntry_sub_defaultEntry_le (by positivity : 0 ≤ 3 * δ) hb ν + have hr := abs_radius_sub_radius_le hδ hu (hw y hy) + have hd : |(w y ν - defaultEntry (newDefault s n K ρ z w) ν) - + (w' y ν - defaultEntry (newDefault s n K ρ z' w') ν)| ≤ 4 * δ := by + calc _ = |(w y ν - w' y ν) - + (defaultEntry (newDefault s n K ρ z w) ν - + defaultEntry (newDefault s n K ρ z' w') ν)| := by congr 1; ring + _ ≤ |w y ν - w' y ν| + |defaultEntry (newDefault s n K ρ z w) ν - + defaultEntry (newDefault s n K ρ z' w') ν| := abs_sub _ _ + _ ≤ 4 * δ := by linarith [hw y hy ν] + have hneg : |-radius (threshold s n ρ z w) (w y) - + -radius (threshold s n ρ z' w') (w' y)| ≤ 21 * δ := by + simpa only [neg_sub_neg, abs_sub_comm] using hr + have hclip := abs_max_sub_max_le hneg + (abs_min_sub_min_le (hd.trans (by linarith : 4 * δ ≤ 21 * δ)) hr) + unfold update updateEntry + calc _ ≤ |defaultEntry (newDefault s n K ρ z w) ν - + defaultEntry (newDefault s n K ρ z' w') ν| + + |max (-radius (threshold s n ρ z w) (w y)) + (min (w y ν - defaultEntry (newDefault s n K ρ z w) ν) + (radius (threshold s n ρ z w) (w y))) - + max (-radius (threshold s n ρ z' w') (w' y)) + (min (w' y ν - defaultEntry (newDefault s n K ρ z' w') ν) + (radius (threshold s n ρ z' w') (w' y)))| := by + rw [add_sub_add_comm] + exact abs_add_le _ _ + _ ≤ 28 * δ := by linarith + +end Cslib.RowCompression diff --git a/ComplexityTests/RowCompression.lean b/ComplexityTests/RowCompression.lean new file mode 100644 index 000000000..a071786ea --- /dev/null +++ b/ComplexityTests/RowCompression.lean @@ -0,0 +1,102 @@ +/- +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 +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Concrete compression updates + +These examples exercise a preserved large entry, actual partial clipping between the two size +thresholds, negative inputs, dummy padding with a positive default, and the exception capacity. +-/ + +namespace ComplexityTests.RowCompression + +open Finset Cslib.RowCompression + +private def largeRow : Fin 2 → Fin 2 → ℝ := ![![10, 0], ![0, 0]] + +private theorem large_threshold : threshold univ 2 1 0 largeRow = 1 := by + norm_num [threshold, kthLargest, entrySize, largeRow, Fin.univ_succ, filter_insert, + filter_singleton] + +private theorem large_default : newDefault univ 2 1 1 0 largeRow = 3 := by + unfold newDefault + rw [large_threshold] + norm_num [kthLargest, largeRow, Fin.univ_succ, filter_insert, filter_singleton] + +-- A large entry survives and the small entry becomes the new default. +example : update univ 2 1 1 0 largeRow = ![![10, 0], ![3, 0]] := by + unfold update + rw [large_threshold, large_default] + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [updateEntry, defaultEntry, radius, entrySize, largeRow] + +-- The list really has one exception, strictly fewer than the capacity two. +example : candidates univ 2 1 0 largeRow = {0} := by + unfold candidates + rw [large_threshold] + ext y + fin_cases y <;> norm_num [entrySize, largeRow] + +private noncomputable def transitionRow : Fin 2 → Fin 2 → ℝ := ![![0, 21 / 10], ![0, 0]] + +private theorem transition_threshold : threshold univ 2 1 0 transitionRow = 1 := by + have hr : kthLargest 2 univ (fun y => entrySize (transitionRow y)) = 0 := by + refine le_antisymm (not_lt.mp fun hlt => ?_) kthLargest_nonneg + have hcard := (lt_kthLargest_iff (by norm_num) le_rfl).mp hlt + have hsupport : ({y | 0 < entrySize (transitionRow y)} : Finset (Fin 2)) = {0} := by + ext y + fin_cases y <;> norm_num [entrySize, transitionRow] + rw [hsupport] at hcard + norm_num at hcard + norm_num [threshold, hr] + +private theorem transition_default : newDefault univ 2 1 1 0 transitionRow = 1 := by + unfold newDefault + rw [transition_threshold] + norm_num [kthLargest, transitionRow, Fin.univ_succ, filter_insert, filter_singleton] + +-- Size 2.1 is in the transition band (2,3); radius 0.7 clips both coordinates. +example : update univ 2 1 1 0 transitionRow = ![![3 / 10, 7 / 10], ![1, 0]] := by + unfold update + rw [transition_threshold, transition_default] + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [updateEntry, defaultEntry, radius, entrySize, transitionRow] + +-- Large signed entries are preserved; no nonnegativity premise on row entries is hidden. +example : updateEntry 1 3 (![(-10), -4] : Fin 2 → ℝ) = ![-10, -4] := by + apply updateEntry_eq_self_of_three_mul_le <;> norm_num [entrySize] + +-- The old default exceeds the floor, and K exceeds the number of real positions. +-- The dummy padding still gives default two, with no candidate IDs. +example : newDefault (univ : Finset (Fin 1)) 2 3 1 2 (fun _ => defaultEntry 2) = 2 ∧ + candidates (univ : Finset (Fin 1)) 2 1 2 (fun _ => defaultEntry 2) = ∅ := by + norm_num [newDefault, candidates, threshold, kthLargest, entrySize, defaultEntry, + Fin.univ_succ] + +-- The empty real row also has a well-defined default; dummies are not counted as real IDs. +example : newDefault (∅ : Finset (Fin 2)) 1 1 1 2 largeRow = 2 ∧ + candidates (∅ : Finset (Fin 2)) 1 1 2 largeRow = ∅ := by + norm_num [newDefault, candidates, threshold, kthLargest] + +-- A concrete perturbation invokes the width-independent stability theorem. +example (y : Fin 2) (ν : Fin 2) : + |update univ 2 1 1 0 largeRow y ν - + update univ 2 1 1 (1 / 10) (fun y ν => largeRow y ν + 1 / 10) y ν| ≤ 14 / 5 := by + have h := abs_update_sub_update_le (s := univ) (n := 2) (K := 1) (ρ := 1) + (z := 0) (z' := 1 / 10) (δ := 1 / 10) (w := largeRow) + (w' := fun y ν => largeRow y ν + 1 / 10) (by norm_num) (by norm_num) (by norm_num) + (by norm_num) (fun y _ ν => by norm_num) (mem_univ y) ν + norm_num at h ⊢ + exact h + +end ComplexityTests.RowCompression