From c3f7a58ac47dd83ab36e9226c2a3a9e96840fe34 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:07:57 +0000 Subject: [PATCH 1/7] 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 From c4d5e70a57485632955a258d70d06b58a93aec6c Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:29:56 +0000 Subject: [PATCH 2/7] feat(logspace): iterate row compression and bound accumulated loss Add concrete increment-and-compression states and schedules. Prove width-independent 28^j propagation, exact restarts, a fifth-power slack bound under an explicit group-count condition, and accumulated row/default loss before overflow. This establishes the update-only part of OpenAI2026LogSpace (8.7) and the unweighted part of Lemma 8.2; weighted preloss and the final root functions remain separate. Validation on base c3f7a58ac47dd83ab36e9226c2a3a9e96840fe34: direct Lean 4.36.0-rc2 checks of both new modules with project options passed without diagnostics, using isolated output files and the parent checkout dependencies read-only. Concrete tests cover a two-group nonzero-loss execution, satisfied no-overflow bounds, an actual overflow after lowering capacity, and distinct initial-state perturbations. Focused proof hygiene including --check-simp and git diff --check passed. Aggregate regeneration and full project gates are delegated to integration. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved the library and tests at 7d08e44bbdb626b74adaa9c4d63e07faa28ce525. Publication adds only the generated aggregate import. Integrated targeted build, tests, aggregate check, hygiene and whitespace checks pass. Full gates run in PR CI. --- Complexity.lean | 1 + .../Analysis/RowCompression/Iteration.lean | 282 ++++++++++++++++++ ComplexityTests/RowCompressionIteration.lean | 109 +++++++ 3 files changed, 392 insertions(+) create mode 100644 Complexity/Foundations/Analysis/RowCompression/Iteration.lean create mode 100644 ComplexityTests/RowCompressionIteration.lean diff --git a/Complexity.lean b/Complexity.lean index 69f36f90f..4902f4c79 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2352,6 +2352,7 @@ 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.RowCompression.Iteration 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/Iteration.lean b/Complexity/Foundations/Analysis/RowCompression/Iteration.lean new file mode 100644 index 000000000..f14c8c92e --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/Iteration.lean @@ -0,0 +1,282 @@ +/- +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 +public import Mathlib.Algebra.BigOperators.Group.Finset.Defs +import Mathlib.Algebra.BigOperators.Group.Finset.Basic +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Iterated row compression + +This module iterates the concrete update of [OpenAI2026LogSpace, Section 8.2, (8.5)--(8.6)]. +At group `i`, add the increment `Δ i` to the current row, then compress using capacities +`n i`, `K i` and floor `ρ i`. The state contains the entire row and its common default, so two +calculations need not select the same exception lists. + +The stability bound is the update-only part of (8.7): an initial absolute perturbation `δ` +is at most `28 ^ j * δ` after `j` updates with the same increments. Restarting at any group +gives the same assertion for a perturbation introduced there. The paper's final root functions +are not formalized here. The optional conversion to a fifth power of a slack assumes the +explicit scheduling fact `2 ^ j ≤ d + 1`; no halving schedule is constructed in this module. + +The accumulated row loss is at most six times the sum of the actual compression thresholds. +Before the first overflow, each threshold is its floor, yielding the unweighted estimate +`6 * ∑ i < j, ρ i` in the first assertion of [OpenAI2026LogSpace, Lemma 8.2]. This does not +assert the weighted preloss estimate (8.9), the small-floor estimates (8.8), stationary-reference +preservation, or a machine-space bound. + +## Main definitions + +* `Cslib.RowCompression.State`: the default and full two-coordinate row. +* `Cslib.RowCompression.advance`, `Cslib.RowCompression.iterate`: one update and its iteration. +* `Cslib.RowCompression.inputRow`, `Cslib.RowCompression.stepThreshold`: the input and actual + threshold at each group. +* `Cslib.RowCompression.uncompressedRow`: the initial row plus the prefix sum of increments. + +## Main results + +* `Cslib.RowCompression.iterate_stability`: width-independent propagation by `28 ^ j`. +* `Cslib.RowCompression.iterate_add`: restart a calculation at any group. +* `Cslib.RowCompression.iterate_stability_from`: propagate a perturbation from any group. +* `Cslib.RowCompression.iterate_stability_of_pow_le`: a polynomial bound given a slack bound. +* `Cslib.RowCompression.abs_iterate_sub_uncompressed_le`: accumulated compression loss. +* `Cslib.RowCompression.abs_iterate_sub_uncompressed_le_of_no_overflow`: the floor-sum bound. +* `Cslib.RowCompression.iterate_defaultValue_monotone`: defaults never decrease. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 8.2--8.3, (8.7) and the unweighted assertion of Lemma 8.2 + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} + +/-- A compressed row represented by its full values and its common default. The finite +exception list is intentionally not part of the mathematical state. -/ +structure State (ι : Type*) where + /-- The first coordinate of the default entry; its second coordinate is zero. -/ + defaultValue : ℝ + /-- The full row, including values at positions represented by the default. -/ + row : ι → Fin 2 → ℝ + +/-- Add an increment and apply the concrete compression update. -/ +@[expose] noncomputable def advance (s : Finset ι) (n K : ℕ) (ρ : ℝ) + (Δ : ι → Fin 2 → ℝ) (a : State ι) : State ι := + { defaultValue := newDefault s n K ρ a.defaultValue (a.row + Δ) + row := update s n K ρ a.defaultValue (a.row + Δ) } + +/-- The state after `j` increment-and-compression groups, indexed starting at zero. -/ +@[expose] noncomputable def iterate (s : Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) : ℕ → State ι + | 0 => a + | j + 1 => advance s (n j) (K j) (ρ j) (Δ j) (iterate s n K ρ Δ a j) + +/-- The row immediately after adding group `j` and before compressing it. -/ +@[expose] noncomputable def inputRow (s : Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (j : ℕ) : ι → Fin 2 → ℝ := + (iterate s n K ρ Δ a j).row + Δ j + +/-- The actual threshold of compression group `j`, including the old default and the size rank. -/ +@[expose] noncomputable def stepThreshold (s : Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (j : ℕ) : ℝ := + threshold s (n j) (ρ j) (iterate s n K ρ Δ a j).defaultValue (inputRow s n K ρ Δ a j) + +/-- The initial row plus all increments before group `j`, with no compression. -/ +@[expose] noncomputable def uncompressedRow (Δ : ℕ → ι → Fin 2 → ℝ) + (w : ι → Fin 2 → ℝ) (j : ℕ) (y : ι) (ν : Fin 2) : ℝ := + w y ν + ∑ i ∈ range j, Δ i y ν + +variable {s : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {a b : State ι} + +@[simp] +theorem iterate_zero : iterate s n K ρ Δ a 0 = a := rfl + +theorem iterate_succ (j : ℕ) : iterate s n K ρ Δ a (j + 1) = + advance s (n j) (K j) (ρ j) (Δ j) (iterate s n K ρ Δ a j) := rfl + +@[simp] +theorem uncompressedRow_zero {w : ι → Fin 2 → ℝ} : uncompressedRow Δ w 0 = w := by + funext y ν + simp [uncompressedRow] + +theorem uncompressedRow_succ {w : ι → Fin 2 → ℝ} (j : ℕ) (y : ι) (ν : Fin 2) : + uncompressedRow Δ w (j + 1) y ν = uncompressedRow Δ w j y ν + Δ j y ν := by + simp only [uncompressedRow, sum_range_succ] + ring + +theorem stepThreshold_nonneg (j : ℕ) : 0 ≤ stepThreshold s n K ρ Δ a j := + threshold_nonneg + +theorem floor_le_stepThreshold (j : ℕ) : ρ j ≤ stepThreshold s n K ρ Δ a j := + floor_le_threshold + +/-- The one-step compression loss, before any accumulation over the schedule. -/ +theorem abs_iterate_succ_sub_inputRow_le (j : ℕ) (y : ι) (ν : Fin 2) : + |(iterate s n K ρ Δ a (j + 1)).row y ν - inputRow s n K ρ Δ a j y ν| ≤ + 6 * stepThreshold s n K ρ Δ a j := + abs_update_sub_le_six_mul y ν + +/-- Addition of the same increment cancels in the one-step stability estimate. -/ +theorem advance_stability {n K : ℕ} {ρ δ : ℝ} {Δ : ι → Fin 2 → ℝ} + (hn : 0 < n) (hK : 0 < K) (hδ : 0 ≤ δ) (hz : |a.defaultValue - b.defaultValue| ≤ δ) + (hw : ∀ y ∈ s, ∀ ν, |a.row y ν - b.row y ν| ≤ δ) : + |(advance s n K ρ Δ a).defaultValue - (advance s n K ρ Δ b).defaultValue| ≤ 28 * δ ∧ + ∀ y ∈ s, ∀ ν, |(advance s n K ρ Δ a).row y ν - + (advance s n K ρ Δ b).row y ν| ≤ 28 * δ := by + have hadd : ∀ y ∈ s, ∀ ν, |(a.row + Δ) y ν - (b.row + Δ) y ν| ≤ δ := by + intro y hy ν + simpa only [Pi.add_apply, add_sub_add_right_eq_sub] using hw y hy ν + constructor + · exact (abs_newDefault_sub_newDefault_le hn hK hδ hz hadd).trans (by linarith) + · intro y hy ν + exact abs_update_sub_update_le hn hK hδ hz hadd hy ν + +/-- An absolute perturbation of the full initial state grows by at most `28 ^ j` through +`j` compression groups with the same increments [OpenAI2026LogSpace, (8.7)]. -/ +theorem iterate_stability {δ : ℝ} (hδ : 0 ≤ δ) (hz : |a.defaultValue - b.defaultValue| ≤ δ) + (hw : ∀ y ∈ s, ∀ ν, |a.row y ν - b.row y ν| ≤ δ) (j : ℕ) + (hn : ∀ i < j, 0 < n i) (hK : ∀ i < j, 0 < K i) : + |(iterate s n K ρ Δ a j).defaultValue - (iterate s n K ρ Δ b j).defaultValue| ≤ + 28 ^ j * δ ∧ + ∀ y ∈ s, ∀ ν, |(iterate s n K ρ Δ a j).row y ν - + (iterate s n K ρ Δ b j).row y ν| ≤ 28 ^ j * δ := by + induction j with + | zero => simpa using And.intro hz hw + | succ j ih => + have h := ih (fun i hi => hn i (Nat.lt_succ_of_lt hi)) + (fun i hi => hK i (Nat.lt_succ_of_lt hi)) + have hnext := advance_stability (ρ := ρ j) (Δ := Δ j) (hn j (Nat.lt_succ_self j)) + (hK j (Nat.lt_succ_self j)) (by positivity : 0 ≤ 28 ^ j * δ) h.1 h.2 + simpa only [iterate_succ, pow_succ, mul_assoc, mul_left_comm, mul_comm] using hnext + +/-- Restarting the indexed schedule preserves exactly the same states. -/ +theorem iterate_add (i j : ℕ) : iterate s n K ρ Δ a (i + j) = + iterate s (fun k => n (i + k)) (fun k => K (i + k)) (fun k => ρ (i + k)) + (fun k => Δ (i + k)) (iterate s n K ρ Δ a i) j := by + induction j with + | zero => rfl + | succ j ih => simp only [Nat.add_succ, iterate_succ, ih] + +/-- A perturbation present after group `i` propagates through the next `j` updates with factor +at most `28 ^ j`, without requiring agreement of earlier states or exception lists. -/ +theorem iterate_stability_from (i j : ℕ) {δ : ℝ} (hδ : 0 ≤ δ) + (hz : |(iterate s n K ρ Δ a i).defaultValue - + (iterate s n K ρ Δ b i).defaultValue| ≤ δ) + (hw : ∀ y ∈ s, ∀ ν, |(iterate s n K ρ Δ a i).row y ν - + (iterate s n K ρ Δ b i).row y ν| ≤ δ) + (hn : ∀ k < j, 0 < n (i + k)) (hK : ∀ k < j, 0 < K (i + k)) : + |(iterate s n K ρ Δ a (i + j)).defaultValue - + (iterate s n K ρ Δ b (i + j)).defaultValue| ≤ 28 ^ j * δ ∧ + ∀ y ∈ s, ∀ ν, |(iterate s n K ρ Δ a (i + j)).row y ν - + (iterate s n K ρ Δ b (i + j)).row y ν| ≤ 28 ^ j * δ := by + rw [iterate_add (a := a) i j, iterate_add (a := b) i j] + exact iterate_stability hδ hz hw j hn hK + +/-- A schedule with `2 ^ j ≤ d + 1` turns the propagation factor into a polynomial in the +slack. We enlarge `28` to `2 ^ 5`, avoiding real exponents in this explicit coarse bound. -/ +theorem propagation_le_slack_pow_five {j d : ℕ} (hjd : 2 ^ j ≤ d + 1) : + (28 : ℝ) ^ j ≤ ((d : ℝ) + 1) ^ 5 := by + calc (28 : ℝ) ^ j ≤ ((2 : ℝ) ^ 5) ^ j := + pow_le_pow_left₀ (by norm_num) (by norm_num) j + _ = ((2 : ℝ) ^ j) ^ 5 := by rw [← pow_mul, ← pow_mul, Nat.mul_comm] + _ ≤ ((d : ℝ) + 1) ^ 5 := pow_le_pow_left₀ (by positivity) (by exact_mod_cast hjd) 5 + +/-- The full state has polynomial perturbation growth under the explicit logarithmic +group-count condition. The condition is a premise about the schedule, not a claimed +construction of the paper's halving schedule. -/ +theorem iterate_stability_of_pow_le {δ : ℝ} (hδ : 0 ≤ δ) + (hz : |a.defaultValue - b.defaultValue| ≤ δ) + (hw : ∀ y ∈ s, ∀ ν, |a.row y ν - b.row y ν| ≤ δ) (j d : ℕ) + (hn : ∀ i < j, 0 < n i) (hK : ∀ i < j, 0 < K i) (hjd : 2 ^ j ≤ d + 1) : + |(iterate s n K ρ Δ a j).defaultValue - (iterate s n K ρ Δ b j).defaultValue| ≤ + ((d : ℝ) + 1) ^ 5 * δ ∧ + ∀ y ∈ s, ∀ ν, |(iterate s n K ρ Δ a j).row y ν - + (iterate s n K ρ Δ b j).row y ν| ≤ ((d : ℝ) + 1) ^ 5 * δ := by + have h := iterate_stability (ρ := ρ) (Δ := Δ) hδ hz hw j hn hK + have hscale := mul_le_mul_of_nonneg_right (propagation_le_slack_pow_five hjd) hδ + exact ⟨h.1.trans hscale, fun y hy ν => (h.2 y hy ν).trans hscale⟩ + +/-- The default never decreases, independently of the increments or the capacities. -/ +theorem iterate_defaultValue_monotone : Monotone fun j => (iterate s n K ρ Δ a j).defaultValue := + monotone_nat_of_le_succ fun _ => le_newDefault + +/-- The default is nonnegative when the initial default is. -/ +theorem iterate_defaultValue_nonneg (ha : 0 ≤ a.defaultValue) (j : ℕ) : + 0 ≤ (iterate s n K ρ Δ a j).defaultValue := + ha.trans (iterate_defaultValue_monotone (Nat.zero_le j)) + +/-- The accumulated row loss is bounded by six times the sum of the actual thresholds. +The increments cancel between the compressed and uncompressed calculations. -/ +theorem abs_iterate_sub_uncompressed_le (j : ℕ) (y : ι) (ν : Fin 2) : + |(iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν| ≤ + 6 * ∑ i ∈ range j, stepThreshold s n K ρ Δ a i := by + induction j with + | zero => simp + | succ j ih => + have hstep := abs_iterate_succ_sub_inputRow_le (s := s) (n := n) (K := K) (ρ := ρ) + (Δ := Δ) (a := a) j y ν + have hdiff : |inputRow s n K ρ Δ a j y ν - uncompressedRow Δ a.row (j + 1) y ν| = + |(iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν| := by + rw [uncompressedRow_succ] + simp only [inputRow, Pi.add_apply, add_sub_add_right_eq_sub] + calc _ ≤ |(iterate s n K ρ Δ a (j + 1)).row y ν - inputRow s n K ρ Δ a j y ν| + + |inputRow s n K ρ Δ a j y ν - uncompressedRow Δ a.row (j + 1) y ν| := + abs_sub_le _ _ _ + _ ≤ 6 * stepThreshold s n K ρ Δ a j + 6 * ∑ i ∈ range j, + stepThreshold s n K ρ Δ a i := by rw [hdiff]; exact add_le_add hstep ih + _ = _ := by rw [sum_range_succ]; ring + +/-- Before the first overflow, the accumulated loss is at most six times the sum of floors +[OpenAI2026LogSpace, Lemma 8.2, unweighted assertion]. The hypothesis says precisely that no +earlier group's actual threshold exceeds its prescribed floor. -/ +theorem abs_iterate_sub_uncompressed_le_of_no_overflow (j : ℕ) + (hno : ∀ i < j, stepThreshold s n K ρ Δ a i ≤ ρ i) (y : ι) (ν : Fin 2) : + |(iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν| ≤ + 6 * ∑ i ∈ range j, ρ i := by + exact (abs_iterate_sub_uncompressed_le j y ν).trans + (mul_le_mul_of_nonneg_left (sum_le_sum fun i hi => hno i (mem_range.mp hi)) (by norm_num)) + +/-- The default has an accumulated change bound of three times the threshold sum. This also +controls the dummy positions, which receive no increments. -/ +theorem iterate_defaultValue_sub_le_three_mul_sum (ha : 0 ≤ a.defaultValue) (j : ℕ) : + (iterate s n K ρ Δ a j).defaultValue - a.defaultValue ≤ + 3 * ∑ i ∈ range j, stepThreshold s n K ρ Δ a i := by + induction j with + | zero => simp + | succ j ih => + have hz := iterate_defaultValue_nonneg (s := s) (n := n) (K := K) (ρ := ρ) (Δ := Δ) ha j + have hnew : (iterate s n K ρ Δ a (j + 1)).defaultValue ≤ + 3 * stepThreshold s n K ρ Δ a j := newDefault_le_three_mul + rw [sum_range_succ] + linarith + +/-- Before overflow, the default (and hence every dummy entry) has accumulated change at most +three times the floor sum. -/ +theorem abs_iterate_defaultValue_sub_le_of_no_overflow (ha : 0 ≤ a.defaultValue) (j : ℕ) + (hno : ∀ i < j, stepThreshold s n K ρ Δ a i ≤ ρ i) : + |(iterate s n K ρ Δ a j).defaultValue - a.defaultValue| ≤ + 3 * ∑ i ∈ range j, ρ i := by + have hmono : a.defaultValue ≤ (iterate s n K ρ Δ a j).defaultValue := + iterate_defaultValue_monotone (Nat.zero_le j) + rw [abs_of_nonneg (sub_nonneg.mpr hmono)] + exact (iterate_defaultValue_sub_le_three_mul_sum ha j).trans + (mul_le_mul_of_nonneg_left (sum_le_sum fun i hi => hno i (mem_range.mp hi)) (by norm_num)) + +end Cslib.RowCompression diff --git a/ComplexityTests/RowCompressionIteration.lean b/ComplexityTests/RowCompressionIteration.lean new file mode 100644 index 000000000..c53d2df48 --- /dev/null +++ b/ComplexityTests/RowCompressionIteration.lean @@ -0,0 +1,109 @@ +/- +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.Iteration +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.NormNum + +/-! +# Iterated compression with genuine increments and loss + +The first group adds ten and preserves it. The second subtracts ten, after which compression +introduces the new default four. Both thresholds equal their floors. Reducing the first capacity +from two to one produces an overflow, so the no-overflow hypothesis is not automatic. +-/ + +namespace ComplexityTests.RowCompressionIteration + +open Finset Cslib.RowCompression + +private def initial : State (Fin 1) := { defaultValue := 0, row := fun _ => ![0, 0] } + +private def increments (i : ℕ) : Fin 1 → Fin 2 → ℝ := + fun _ => if i = 0 then ![10, 0] else ![-10, 0] + +private def floors (i : ℕ) : ℝ := if i = 0 then 1 else 4 + +private noncomputable def run : ℕ → State (Fin 1) := + iterate univ (fun _ => 2) (fun _ => 1) floors increments initial + +private theorem first_state : (run 1).defaultValue = 3 ∧ (run 1).row 0 = ![10, 0] := by + constructor + · norm_num [run, iterate, advance, initial, increments, floors, newDefault, threshold, + kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + · funext ν + fin_cases ν <;> + norm_num [run, iterate, advance, initial, increments, floors, newDefault, threshold, + kthLargest, entrySize, update, updateEntry, radius, defaultEntry, Fin.univ_succ, + filter_insert, filter_singleton] + +private theorem second_state : (run 2).defaultValue = 4 ∧ (run 2).row 0 = ![4, 0] := by + have hrow : (run 1).row = fun _ => (![10, 0] : Fin 2 → ℝ) := by + funext y + fin_cases y + exact first_state.2 + change (advance univ 2 1 4 (increments 1) (run 1)).defaultValue = 4 ∧ + (advance univ 2 1 4 (increments 1) (run 1)).row 0 = ![4, 0] + simp only [advance, first_state.1, hrow] + constructor + · norm_num [increments, newDefault, threshold, kthLargest, entrySize, Fin.univ_succ, + filter_insert, filter_singleton] + · funext ν + fin_cases ν <;> + norm_num [increments, newDefault, threshold, kthLargest, entrySize, update, updateEntry, + radius, defaultEntry, Fin.univ_succ, filter_insert, filter_singleton] + +-- Compression has introduced a nonzero loss, although the raw increments cancel. +example : (run 2).row 0 0 - uncompressedRow increments initial.row 2 0 0 = 4 := by + rw [second_state.2] + norm_num [uncompressedRow, initial, increments, sum_range_succ] + +private theorem no_overflow (i : ℕ) (hi : i < 2) : + stepThreshold univ (fun _ => 2) (fun _ => 1) floors increments initial i ≤ floors i := by + interval_cases i + · norm_num [stepThreshold, inputRow, iterate, initial, increments, floors, threshold, + kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + · change threshold univ 2 4 (run 1).defaultValue ((run 1).row + increments 1) ≤ 4 + have hrow : (run 1).row = fun _ => (![10, 0] : Fin 2 → ℝ) := by + funext y + fin_cases y + exact first_state.2 + rw [first_state.1, hrow] + norm_num [increments, threshold, kthLargest, entrySize, Fin.univ_succ, filter_insert, + filter_singleton] + +-- The derived prefix-loss theorem applies to an actual nonzero-loss execution. +example (ν : Fin 2) : |(run 2).row 0 ν - uncompressedRow increments initial.row 2 0 ν| ≤ 30 := by + have h := abs_iterate_sub_uncompressed_le_of_no_overflow 2 no_overflow 0 ν + norm_num [floors, sum_range_succ] at h + exact h + +-- An undersized capacity causes overflow already at the first group. +example : ¬ stepThreshold univ (fun _ => 1) (fun _ => 1) floors increments initial 0 ≤ + floors 0 := by + norm_num [stepThreshold, inputRow, iterate, initial, increments, floors, threshold, + kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + +private noncomputable def perturbed : State (Fin 1) := + { defaultValue := 1 / 10, row := fun _ => ![1 / 10, 1 / 10] } + +-- The polynomial propagation estimate applies to genuinely different full initial states. +example (y : Fin 1) (ν : Fin 2) : + |(run 2).row y ν - + (iterate univ (fun _ => 2) (fun _ => 1) floors increments perturbed 2).row y ν| ≤ + 512 / 5 := by + have h := iterate_stability_of_pow_le (s := univ) (n := fun _ => 2) (K := fun _ => 1) + (ρ := floors) (Δ := increments) (a := initial) (b := perturbed) (δ := 1 / 10) + (by norm_num) (by norm_num [initial, perturbed]) + (fun y _ ν => by fin_cases ν <;> norm_num [initial, perturbed]) 2 3 + (by intros; norm_num) (by intros; norm_num) (by norm_num) + have hy := h.2 y (mem_univ y) ν + norm_num at hy + exact hy + +end ComplexityTests.RowCompressionIteration From 1edba8550d8f6051c2b4b73f4f92774f497954c2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:33:16 +0000 Subject: [PATCH 3/7] feat(logspace): construct explicit small floors for halving schedules Use decreasing power-of-two slacks and the explicit floors eta * (1/1024)^slack. Derive consecutive floor separation, both finite-sum bounds from source equation (8.8), and the local 8*rho <= eta margin. Bound propagation for the actual remaining group count, distinguishing updates after the current group from those including it. The source uses unscaled inverse powers of two; this mathematical witness explicitly scales by eta and does not choose an exponent for the full integrated estimator. Validation: direct Lean 4.36.0-rc2 checks of Floors.lean and RowCompressionFloors.lean with project options passed without diagnostics, using private outputs and parent dependencies read-only. Tests compute nonzero floors, check halving and empty schedules, and apply the sum theorem to a concrete no-overflow compression execution. Focused hygiene including --check-simp and git diff --check passed. Base is iteration milestone 7d08e44bbdb626b74adaa9c4d63e07faa28ce525; aggregate and full project validation remain integration tasks. AI assistance: ChatGPT implemented and checked the proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-source-release-20261030 approved module/tests at bd14fc247724f63e650ced31e7b0e6c4d30fcee1. Publication adds only generated import registration. Integrated strict module/test build, focused hygiene and whitespace checks pass. Full gates run in PR CI. --- Complexity.lean | 1 + .../Analysis/RowCompression/Floors.lean | 183 ++++++++++++++++++ ComplexityTests/RowCompressionFloors.lean | 87 +++++++++ 3 files changed, 271 insertions(+) create mode 100644 Complexity/Foundations/Analysis/RowCompression/Floors.lean create mode 100644 ComplexityTests/RowCompressionFloors.lean diff --git a/Complexity.lean b/Complexity.lean index 4902f4c79..0a2080c1d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2352,6 +2352,7 @@ 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.RowCompression.Floors public import Complexity.Foundations.Analysis.RowCompression.Iteration public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch diff --git a/Complexity/Foundations/Analysis/RowCompression/Floors.lean b/Complexity/Foundations/Analysis/RowCompression/Floors.lean new file mode 100644 index 000000000..fdb665828 --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/Floors.lean @@ -0,0 +1,183 @@ +/- +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.Iteration +import Mathlib.Algebra.Order.GroupWithZero.Basic +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Explicit small floors for a halving compression schedule + +For `m` groups, indexed by `i < m`, set `d_i = 2 ^ (m - (i + 1))`. These slacks halve down +to one, as in [OpenAI2026LogSpace, Section 8.1]. We construct the floors +`ρ_i = η * (1 / 1024) ^ d_i` for any fixed `η > 0`. + +The paper uses the unscaled floors `2 ^ (-c₁ * d_i)` and chooses `c₁` large depending on its +fixed sensitivity margin `η`. Our explicit witness instead uses exponent ten and scales by `η`. +It proves the two numerical inequalities in (8.8), and `8 * ρ_i ≤ η`, for every positive `η`. +It does not select `c₁` against the other exponents in the integrated compression argument. + +Consecutive floors grow by at least a factor of 1024. A finite induction therefore bounds the +sum before group `i` by `ρ_i / 1023`, and the sum over all groups by `η / 1023`. Multiplication +by six gives the two `/100` bounds, with no assumed small-sum hypothesis. + +There are `m - (i + 1)` updates after group `i`, whose power of two equals `d_i`. Counting the +current group too introduces one extra factor of 28 in the perturbation bound; this is absorbed +by the unspecified outer constant in the source's (8.7). + +## Main definitions + +* `Cslib.RowCompression.dyadicSlack`: the decreasing power-of-two slacks. +* `Cslib.RowCompression.dyadicFloor`: the explicit margin-scaled floors. + +## Main results + +* `Cslib.RowCompression.six_sum_range_dyadicFloor_le`: prior floors are small relative to the + current floor. +* `Cslib.RowCompression.six_sum_range_dyadicFloor_le_scale`: all floors are small relative to + the sensitivity margin. +* `Cslib.RowCompression.eight_mul_dyadicFloor_le`: the local margin condition. +* `Cslib.RowCompression.propagation_le_dyadicSlack`: polynomial perturbation growth for the + actual number of remaining groups. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 8.1--8.3, (8.7)--(8.8) (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +/-- The decreasing power-of-two slacks of a schedule with `m` groups. Indices `i ≥ m` are +defined too, with value one, but are not additional groups in the schedule. -/ +@[expose] def dyadicSlack (m i : ℕ) : ℕ := 2 ^ (m - (i + 1)) + +/-- An explicit floor schedule at sensitivity scale `η`. The finite schedule consists of +indices `i < m`; the total function is convenient as an argument to `iterate`. -/ +@[expose] noncomputable def dyadicFloor (η : ℝ) (m i : ℕ) : ℝ := + η * (1 / 1024) ^ dyadicSlack m i + +theorem dyadicSlack_pos (m i : ℕ) : 0 < dyadicSlack m i := by + unfold dyadicSlack + positivity + +@[simp] +theorem dyadicSlack_last (m : ℕ) : dyadicSlack (m + 1) m = 1 := by + simp [dyadicSlack] + +/-- Each slack is twice the next one while both indices are actual groups. -/ +theorem dyadicSlack_succ {m i : ℕ} (hi : i + 1 < m) : + dyadicSlack m i = 2 * dyadicSlack m (i + 1) := by + have h : m - (i + 1) = m - (i + 1 + 1) + 1 := by omega + unfold dyadicSlack + rw [h, pow_succ, Nat.mul_comm] + +theorem dyadicFloor_nonneg {η : ℝ} (hη : 0 ≤ η) (m i : ℕ) : + 0 ≤ dyadicFloor η m i := by + unfold dyadicFloor + positivity + +theorem dyadicFloor_pos {η : ℝ} (hη : 0 < η) (m i : ℕ) : + 0 < dyadicFloor η m i := by + unfold dyadicFloor + positivity + +@[simp] +theorem dyadicFloor_last (η : ℝ) (m : ℕ) : dyadicFloor η (m + 1) m = η / 1024 := by + simp [dyadicFloor, div_eq_mul_inv] + +private theorem pow_dyadicSlack_le (m i : ℕ) : + (1 / 1024 : ℝ) ^ dyadicSlack m i ≤ 1 / 1024 := by + simpa only [pow_one] using pow_le_pow_of_le_one (by norm_num : (0 : ℝ) ≤ 1 / 1024) + (by norm_num : (1 / 1024 : ℝ) ≤ 1) (dyadicSlack_pos m i) + +/-- Every floor is at most `η / 1024`, including the final floor where equality holds. -/ +theorem dyadicFloor_le_scale_div {η : ℝ} (hη : 0 ≤ η) (m i : ℕ) : + dyadicFloor η m i ≤ η / 1024 := by + simpa only [dyadicFloor, mul_one_div] using + mul_le_mul_of_nonneg_left (pow_dyadicSlack_le m i) hη + +/-- Consecutive floors are separated by a factor of at least 1024. -/ +theorem dyadicFloor_mul_le_succ {η : ℝ} (hη : 0 ≤ η) {m i : ℕ} (hi : i + 1 < m) : + 1024 * dyadicFloor η m i ≤ dyadicFloor η m (i + 1) := by + have hbase := pow_dyadicSlack_le m (i + 1) + have hnonneg := dyadicFloor_nonneg hη m (i + 1) + have hmul := mul_le_mul_of_nonneg_left hbase hnonneg + have heq : dyadicFloor η m i = + dyadicFloor η m (i + 1) * (1 / 1024) ^ dyadicSlack m (i + 1) := by + unfold dyadicFloor + rw [dyadicSlack_succ hi, two_mul, pow_add, mul_assoc] + rw [← heq] at hmul + linarith + +/-- The sum of earlier floors is bounded by the geometric factor `1 / 1023` times the +current floor. This is derived from the concrete schedule, without a small-sum premise. -/ +theorem sum_range_dyadicFloor_le {η : ℝ} (hη : 0 ≤ η) {m j : ℕ} (hj : j < m) : + ∑ i ∈ range j, dyadicFloor η m i ≤ dyadicFloor η m j / 1023 := by + induction j with + | zero => simpa using div_nonneg (dyadicFloor_nonneg hη m 0) (by norm_num : (0 : ℝ) ≤ 1023) + | succ j ih => + have hprev := ih (Nat.lt_of_succ_lt hj) + have hstep := dyadicFloor_mul_le_succ hη hj + rw [sum_range_succ] + linarith + +/-- The first small-floor estimate of [OpenAI2026LogSpace, (8.8)], for the explicit scaled +schedule: all earlier compression changes total at most one hundredth of the current floor. -/ +theorem six_sum_range_dyadicFloor_le {η : ℝ} (hη : 0 ≤ η) {m j : ℕ} (hj : j < m) : + 6 * ∑ i ∈ range j, dyadicFloor η m i ≤ dyadicFloor η m j / 100 := by + have hsum := sum_range_dyadicFloor_le hη hj + have hfloor := dyadicFloor_nonneg hη m j + linarith + +/-- The finite sum of all floors is at most `η / 1023`, uniformly in the number of groups. -/ +theorem sum_range_dyadicFloor_le_scale {η : ℝ} (hη : 0 ≤ η) (m : ℕ) : + ∑ i ∈ range m, dyadicFloor η m i ≤ η / 1023 := by + cases m with + | zero => simpa using div_nonneg hη (by norm_num : (0 : ℝ) ≤ 1023) + | succ m => + have hsum := sum_range_dyadicFloor_le hη (Nat.lt_succ_self m) + rw [sum_range_succ, dyadicFloor_last] + rw [dyadicFloor_last] at hsum + linarith + +/-- The second small-floor estimate of [OpenAI2026LogSpace, (8.8)], uniformly in the number +of groups. -/ +theorem six_sum_range_dyadicFloor_le_scale {η : ℝ} (hη : 0 ≤ η) (m : ℕ) : + 6 * ∑ i ∈ range m, dyadicFloor η m i ≤ η / 100 := by + have hsum := sum_range_dyadicFloor_le_scale hη m + linarith + +/-- Every floor satisfies the local margin condition used in the weighted preloss estimate. -/ +theorem eight_mul_dyadicFloor_le {η : ℝ} (hη : 0 ≤ η) (m i : ℕ) : + 8 * dyadicFloor η m i ≤ η := by + have hfloor := dyadicFloor_le_scale_div hη m i + linarith + +/-- The exact power-of-two count of updates strictly after the current group is its slack. -/ +theorem two_pow_remaining_eq_dyadicSlack (m i : ℕ) : + 2 ^ (m - (i + 1)) = dyadicSlack m i := rfl + +/-- Including the current group, the propagation cost is at most an extra factor 28 times a +fifth-degree polynomial in its slack [OpenAI2026LogSpace, (8.7)]. -/ +theorem propagation_le_dyadicSlack {m i : ℕ} (hi : i < m) : + (28 : ℝ) ^ (m - i) ≤ 28 * ((dyadicSlack m i : ℝ) + 1) ^ 5 := by + have hcount : m - i = m - (i + 1) + 1 := by omega + have hpow : (28 : ℝ) ^ (m - (i + 1)) ≤ ((dyadicSlack m i : ℝ) + 1) ^ 5 := + propagation_le_slack_pow_five (Nat.le_succ (dyadicSlack m i)) + rw [hcount, pow_succ] + nlinarith + +end Cslib.RowCompression diff --git a/ComplexityTests/RowCompressionFloors.lean b/ComplexityTests/RowCompressionFloors.lean new file mode 100644 index 000000000..44238a5ee --- /dev/null +++ b/ComplexityTests/RowCompressionFloors.lean @@ -0,0 +1,87 @@ +/- +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.Floors +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.NormNum + +/-! +# Concrete small-floor schedules + +Check the explicit halving slacks and nonzero floors, including the empty schedule. A two-group +compression execution with zero raw increments acquires a positive default; its no-overflow +property is checked directly, then the floor sum controls its actual compression loss. +-/ + +namespace ComplexityTests.RowCompressionFloors + +open Finset Cslib.RowCompression + +example : dyadicSlack 3 0 = 4 ∧ dyadicSlack 3 1 = 2 ∧ dyadicSlack 3 2 = 1 := by + norm_num [dyadicSlack] + +example : dyadicFloor 1 3 0 = 1 / 1099511627776 ∧ + dyadicFloor 1 3 1 = 1 / 1048576 ∧ dyadicFloor 1 3 2 = 1 / 1024 := by + norm_num [dyadicFloor, dyadicSlack] + +-- Actual nonzero previous floors satisfy the hundredth-of-current-floor estimate. +example : 6 * (dyadicFloor 1 3 0 + dyadicFloor 1 3 1) ≤ dyadicFloor 1 3 2 / 100 := by + norm_num [dyadicFloor, dyadicSlack] + +-- The total-sum theorem includes a schedule with no groups. +example : (∑ i ∈ range 0, dyadicFloor (2 / 3) 0 i) = 0 := by simp + +-- The scale need not be one, and the number of groups is arbitrary. +example (m : ℕ) : 6 * ∑ i ∈ range m, dyadicFloor (2 / 3) m i ≤ 1 / 150 := by + have h := six_sum_range_dyadicFloor_le_scale (η := 2 / 3) (by norm_num) m + norm_num at h + exact h + +private def initial : State (Fin 1) := { defaultValue := 0, row := fun _ => ![0, 0] } + +private noncomputable def run : ℕ → State (Fin 1) := + iterate univ (fun _ => 2) (fun _ => 1) (dyadicFloor 1 2) (fun _ => 0) initial + +private theorem first_state : (run 1).defaultValue = 1 / 1048576 ∧ + (run 1).row = fun _ => defaultEntry (1 / 1048576) := by + constructor + · norm_num [run, iterate, advance, initial, dyadicFloor, dyadicSlack, newDefault, threshold, + kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + · funext y ν + fin_cases y + fin_cases ν <;> + norm_num [run, iterate, advance, initial, dyadicFloor, dyadicSlack, newDefault, threshold, + kthLargest, entrySize, update, updateEntry, radius, defaultEntry, Fin.univ_succ, + filter_insert, filter_singleton] + +private theorem no_overflow (i : ℕ) (hi : i < 2) : + stepThreshold univ (fun _ => 2) (fun _ => 1) (dyadicFloor 1 2) (fun _ => 0) initial i ≤ + dyadicFloor 1 2 i := by + interval_cases i + · norm_num [stepThreshold, inputRow, iterate, initial, dyadicFloor, dyadicSlack, threshold, + kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + · change threshold univ 2 (dyadicFloor 1 2 1) (run 1).defaultValue ((run 1).row + 0) ≤ + dyadicFloor 1 2 1 + rw [first_state.1, first_state.2, add_zero] + norm_num [dyadicFloor, dyadicSlack, threshold, kthLargest, entrySize, defaultEntry, + Fin.univ_succ, filter_insert, filter_singleton] + +-- The new numerical schedule closes the small-total-loss premise for a real execution. +example (y : Fin 1) (ν : Fin 2) : |(run 2).row y ν| ≤ 1 / 100 := by + have h := abs_iterate_sub_uncompressed_le_of_no_overflow 2 no_overflow y ν + have hsum := six_sum_range_dyadicFloor_le_scale (η := 1) (by norm_num) 2 + have h' := h.trans hsum + fin_cases ν <;> simpa [uncompressedRow, initial, run] using h' + +-- There are three updates left including group one, but only two strictly after it. +example : dyadicSlack 4 1 = 4 ∧ (28 : ℝ) ^ (4 - 1) ≤ 28 * (4 + 1) ^ 5 := by + constructor + · norm_num [dyadicSlack] + · simpa [dyadicSlack] using propagation_le_dyadicSlack (m := 4) (i := 1) (by norm_num) + +end ComplexityTests.RowCompressionFloors From 90e85dbb79f6125ed1ece783a3f811233f2f51a2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:51:18 +0000 Subject: [PATCH 4/7] feat(logspace): prove weighted compression preloss Prove the weighted preloss assertion of OpenAI2026LogSpace Lemma 8.2 for the actual compression recursion, with explicit constant12(1+eta)/eta. Apply it to the concrete dyadic floors, discharging numerical small-floor conditions. Stationary-reference preservation, relative stability after overflow, and the complete estimator remain separate obligations. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved599c5e8a and the dyadic application delta4cc6581b. Published library/tests are identical to the reviewed source, with generated aggregate registration. Strict private Lean source/test checks, hygiene and whitespace checks pass. Full integration gates run in PR CI. Worker codex-compression-preloss-20261030; AI-assisted implementation and review. --- Complexity.lean | 1 + .../Analysis/RowCompression/Preloss.lean | 184 ++++++++++++++++++ ComplexityTests/RowCompressionPreloss.lean | 86 ++++++++ 3 files changed, 271 insertions(+) create mode 100644 Complexity/Foundations/Analysis/RowCompression/Preloss.lean create mode 100644 ComplexityTests/RowCompressionPreloss.lean diff --git a/Complexity.lean b/Complexity.lean index 0a2080c1d..93cdc9f6f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2354,6 +2354,7 @@ public import Complexity.Foundations.Analysis.RootError public import Complexity.Foundations.Analysis.RowCompression 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.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli diff --git a/Complexity/Foundations/Analysis/RowCompression/Preloss.lean b/Complexity/Foundations/Analysis/RowCompression/Preloss.lean new file mode 100644 index 000000000..6be76e8a3 --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/Preloss.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.Floors +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Weighted loss before a compression overflow + +The preloss estimate of [OpenAI2026LogSpace, Lemma 8.2, (8.9)] bounds the error introduced by +compression in terms of the errors of the uncompressed prefixes. At an endpoint with true first +coordinate `d ≥ η > 0`, a compression change is possible only when the current entry is small. +If the preceding compression loss is at most the current floor `ρ` and `8 * ρ ≤ η`, the raw +prefix is then at most half of `d`. Its clipped relative error is bounded below by +`η / (2 * (1 + η))`. Combining this with the local change bound `6 * ρ` charges the change to +the raw prefix error, with the explicit constant `12 * (1 + η) / η`. + +The main theorem applies this argument to the actual recursion `Cslib.RowCompression.iterate`. +It assumes that each earlier threshold is at most its floor and that +`6 * ∑ k < i, ρ k ≤ ρ i`. These hypotheses are weaker than the corresponding small-floor +conditions in (8.8). A corollary discharges both numerical hypotheses for the concrete scaled +dyadic floors constructed in `Cslib.RowCompression.dyadicFloor`. The clipped +error is (8.3), with channel indices `0, 1` and group indices starting at zero, so group `i` +uses the uncompressed prefix at `i + 1`. The argument is independent of the moment exponent. + +This module proves the weighted preloss assertion of Lemma 8.2. It does not assert preservation +of row functions by the stationary reference, stability after overflow, or a machine-space bound. + +## Main definitions + +* `Cslib.RowCompression.clippedError`: the maximum of the clipped relative first-channel error + and the clipped absolute second-channel error. + +## Main results + +* `Cslib.RowCompression.abs_update_sub_le_mul_clippedError`: the local weighted change bound. +* `Cslib.RowCompression.abs_iterate_sub_uncompressed_le_weighted`: the weighted preloss estimate + for the concrete increment-and-compression recursion. +* `Cslib.RowCompression.abs_iterate_sub_uncompressed_le_weighted_dyadic`: the same estimate with + the numerical floor conditions discharged by the explicit dyadic schedule. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, Lemma 8.2, weighted preloss assertion (8.9) + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} + +/-- The clipped endpoint error of [OpenAI2026LogSpace, (8.3)]. The first true coordinate is +nonnegative in applications; the second coordinate is measured by absolute error. -/ +@[expose] noncomputable def clippedError (d v : ℝ) (w : Fin 2 → ℝ) : ℝ := + max (min 1 (|w 0 - d| / (1 + d))) (min 1 |w 1 - v|) + +theorem clippedError_nonneg (d v : ℝ) (w : Fin 2 → ℝ) : 0 ≤ clippedError d v w := + (le_min (by norm_num) (abs_nonneg _)).trans (le_max_right _ _) + +theorem clippedError_le_one (d v : ℝ) (w : Fin 2 → ℝ) : clippedError d v w ≤ 1 := + max_le (min_le_left _ _) (min_le_left _ _) + +@[simp] +theorem clippedError_self (d v : ℝ) (w : Fin 2 → ℝ) (hd : w 0 = d) (hv : w 1 = v) : + clippedError d v w = 0 := by + simp [clippedError, hd, hv] + +private theorem le_clipped_relative_error {η d r ρ : ℝ} (hη : 0 < η) (hd : η ≤ d) + (hsmall : 8 * ρ ≤ η) (hr : r ≤ 4 * ρ) : + η / (2 * (1 + η)) ≤ min 1 (|r - d| / (1 + d)) := by + have hden : 0 < 1 + d := by linarith + have hηden : 0 < 2 * (1 + η) := by positivity + have hdiff : d ≤ 2 * |r - d| := by linarith [neg_le_abs (r - d)] + refine le_min ?_ ?_ + · apply (div_le_iff₀ hηden).2 + linarith + · apply (div_le_div_iff₀ hηden hden).2 + nlinarith [mul_nonneg (show 0 ≤ 1 + η by positivity) + (show 0 ≤ 2 * |r - d| - d by linarith)] + +/-- Before overflow, a change at a genuinely large target can be charged to the raw prefix's +clipped error. `raw` is the uncompressed prefix; `w` also includes preceding compression loss. +Only the first coordinate of that preceding loss is needed. -/ +theorem abs_update_sub_le_mul_clippedError {s : Finset ι} {n K : ℕ} {ρ z η d v : ℝ} + {w : ι → Fin 2 → ℝ} {raw : Fin 2 → ℝ} (hη : 0 < η) (hd : η ≤ d) + (hno : threshold s n ρ z w ≤ ρ) (hsmall : 8 * ρ ≤ η) {y : ι} + (hprev : |w y 0 - raw 0| ≤ ρ) (ν : Fin 2) : + |update s n K ρ z w y ν - w y ν| ≤ + (12 * (1 + η) / η) * ρ * clippedError d v raw := by + have hρ : 0 ≤ ρ := threshold_nonneg.trans hno + have hC : 0 ≤ 12 * (1 + η) / η := by positivity + by_cases hlarge : 3 * threshold s n ρ z w ≤ entrySize (w y) + · rw [update_eq_self_of_three_mul_le hlarge, sub_self, abs_zero] + exact mul_nonneg (mul_nonneg hC hρ) (clippedError_nonneg _ _ _) + have hsize : entrySize (w y) < 3 * threshold s n ρ z w := lt_of_not_ge hlarge + have hraw : raw 0 ≤ 4 * ρ := by + have hw := (le_abs_self (w y 0)).trans (abs_apply_le_entrySize (w y) 0) + have hp := (abs_le.mp hprev).1 + linarith + have he : η / (2 * (1 + η)) ≤ clippedError d v raw := + (le_clipped_relative_error hη hd hsmall hraw).trans (le_max_left _ _) + have hcancel : (12 * (1 + η) / η) * ρ * (η / (2 * (1 + η))) = 6 * ρ := by + field_simp + ring + calc |update s n K ρ z w y ν - w y ν| ≤ 6 * ρ := + (abs_update_sub_le_six_mul y ν).trans (mul_le_mul_of_nonneg_left hno (by norm_num)) + _ = (12 * (1 + η) / η) * ρ * (η / (2 * (1 + η))) := hcancel.symm + _ ≤ (12 * (1 + η) / η) * ρ * clippedError d v raw := + mul_le_mul_of_nonneg_left he (mul_nonneg hC hρ) + +/-- The weighted preloss estimate [OpenAI2026LogSpace, Lemma 8.2, (8.9)] for actual iterates. +The right-hand errors use raw prefixes, not compressed rows. No target upper bound is needed. -/ +theorem abs_iterate_sub_uncompressed_le_weighted {s : Finset ι} {n K : ℕ → ℕ} + {ρ : ℕ → ℝ} {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {η d v : ℝ} + (hη : 0 < η) (hd : η ≤ d) (j : ℕ) + (hno : ∀ i < j, stepThreshold s n K ρ Δ a i ≤ ρ i) + (hsmall : ∀ i < j, 8 * ρ i ≤ η) + (hprior : ∀ i < j, 6 * ∑ k ∈ range i, ρ k ≤ ρ i) (y : ι) (ν : Fin 2) : + |(iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν| ≤ + (12 * (1 + η) / η) * ∑ i ∈ range j, + ρ i * clippedError d v (uncompressedRow Δ a.row (i + 1) y) := by + induction j with + | zero => simp + | succ j ih => + have hj := Nat.lt_succ_self j + have hno' : ∀ i < j, stepThreshold s n K ρ Δ a i ≤ ρ i := + fun i hi => hno i (Nat.lt_succ_of_lt hi) + have hprev : |inputRow s n K ρ Δ a j y 0 - + uncompressedRow Δ a.row (j + 1) y 0| ≤ ρ j := by + rw [uncompressedRow_succ] + simp only [inputRow, Pi.add_apply, add_sub_add_right_eq_sub] + exact (abs_iterate_sub_uncompressed_le_of_no_overflow j hno' y 0).trans (hprior j hj) + have hstep := abs_update_sub_le_mul_clippedError (K := K j) (v := v) hη hd + (hno j hj) (hsmall j hj) hprev ν + have hbefore := ih hno' (fun i hi => hsmall i (Nat.lt_succ_of_lt hi)) + (fun i hi => hprior i (Nat.lt_succ_of_lt hi)) + have hdiff : |inputRow s n K ρ Δ a j y ν - uncompressedRow Δ a.row (j + 1) y ν| = + |(iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν| := by + rw [uncompressedRow_succ] + simp only [inputRow, Pi.add_apply, add_sub_add_right_eq_sub] + calc _ ≤ |(iterate s n K ρ Δ a (j + 1)).row y ν - inputRow s n K ρ Δ a j y ν| + + |inputRow s n K ρ Δ a j y ν - uncompressedRow Δ a.row (j + 1) y ν| := + abs_sub_le _ _ _ + _ ≤ (12 * (1 + η) / η) * ρ j * + clippedError d v (uncompressedRow Δ a.row (j + 1) y) + + (12 * (1 + η) / η) * ∑ i ∈ range j, + ρ i * clippedError d v (uncompressedRow Δ a.row (i + 1) y) := by + rw [hdiff] + exact add_le_add hstep hbefore + _ = _ := by rw [sum_range_succ]; ring + +/-- Weighted preloss for the concrete dyadic floors. The numerical small-floor hypotheses are +proved by the schedule; only the absence of overflow before the selected prefix remains assumed. +The parameter choice against the later estimator's noise/capacity constants is separate. -/ +theorem abs_iterate_sub_uncompressed_le_weighted_dyadic {s : Finset ι} {n K : ℕ → ℕ} + {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {η d v : ℝ} + (hη : 0 < η) (hd : η ≤ d) (m j : ℕ) (hj : j ≤ m) + (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) + (y : ι) (ν : Fin 2) : + |(iterate s n K (dyadicFloor η m) Δ a j).row y ν - uncompressedRow Δ a.row j y ν| ≤ + (12 * (1 + η) / η) * ∑ i ∈ range j, + dyadicFloor η m i * clippedError d v (uncompressedRow Δ a.row (i + 1) y) := by + apply abs_iterate_sub_uncompressed_le_weighted hη hd j hno + · exact fun i _ => eight_mul_dyadicFloor_le hη.le m i + · intro i hi + have hsum := six_sum_range_dyadicFloor_le hη.le (hi.trans_le hj) + have hfloor := dyadicFloor_nonneg hη.le m i + linarith + +end Cslib.RowCompression diff --git a/ComplexityTests/RowCompressionPreloss.lean b/ComplexityTests/RowCompressionPreloss.lean new file mode 100644 index 000000000..7b86bd280 --- /dev/null +++ b/ComplexityTests/RowCompressionPreloss.lean @@ -0,0 +1,86 @@ +/- +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.Preloss +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.IntervalCases +import Mathlib.Tactic.NormNum + +/-! +# Weighted compression preloss examples + +A two-group calculation has actual nonzero compression loss, satisfies the small-floor and +no-overflow hypotheses, and invokes the weighted theorem. Other examples check saturation, +negative raw first coordinates, and exact targets with zero error. +-/ + +namespace ComplexityTests.RowCompressionPreloss + +open Finset Cslib.RowCompression + +private def zeroState : State (Fin 1) := ⟨0, fun _ => ![0, 0]⟩ + +private noncomputable def floors (i : ℕ) : ℝ := if i = 0 then 1 / 100 else 1 / 10 + +private theorem no_overflow (i : ℕ) (hi : i < 2) : + stepThreshold univ (fun _ => 1) (fun _ => 1) floors (fun _ => 0) zeroState i ≤ + floors i := by + interval_cases i <;> + norm_num [stepThreshold, inputRow, iterate, advance, zeroState, floors, threshold, + newDefault, update, updateEntry, radius, entrySize, defaultEntry, kthLargest, Fin.univ_succ] + +-- Two genuine compression changes: the raw prefix stays zero while the stored row becomes 0.1. +example : (iterate univ (fun _ => 1) (fun _ => 1) floors (fun _ => 0) zeroState 2).row 0 0 = + 1 / 10 := by + norm_num [iterate, advance, zeroState, floors, threshold, newDefault, update, updateEntry, + radius, entrySize, defaultEntry, kthLargest, Fin.univ_succ] + +-- The theorem applies to this concrete schedule; its weighted right side is 24·(0.01+0.1)/2. +example (ν : Fin 2) : + |(iterate univ (fun _ => 1) (fun _ => 1) floors (fun _ => 0) zeroState 2).row 0 ν - + uncompressedRow (fun _ => 0) zeroState.row 2 0 ν| ≤ 33 / 25 := by + have h := abs_iterate_sub_uncompressed_le_weighted (s := univ) (n := fun _ => 1) + (K := fun _ => 1) (ρ := floors) (Δ := fun _ => 0) (a := zeroState) + (η := 1) (d := 1) (v := 0) (by norm_num) le_rfl 2 no_overflow + (by intro i hi; interval_cases i <;> norm_num [floors]) + (by intro i hi; interval_cases i <;> norm_num [floors, sum_range_succ]) 0 ν + norm_num [floors, uncompressedRow, zeroState, clippedError, sum_range_succ] at h + simpa [uncompressedRow, zeroState] using h + +-- Relative error saturates at one, and either channel can attain the maximum. +example : clippedError 1 0 (![-4, 0] : Fin 2 → ℝ) = 1 ∧ + clippedError 1 0 (![1, 2] : Fin 2 → ℝ) = 1 := by + norm_num [clippedError] + +-- Exact targets above the sensitivity floor force zero compression change in both coordinates. +example (d v : ℝ) (hd : 1 ≤ d) (w : Fin 1 → Fin 2 → ℝ) + (hw : w 0 = ![d, v]) (hno : threshold univ 2 (1 / 10) 0 w ≤ 1 / 10) (ν : Fin 2) : + update univ 2 1 (1 / 10) 0 w 0 ν = w 0 ν := by + have h := abs_update_sub_le_mul_clippedError (K := 1) (η := 1) (d := d) (v := v) + (raw := ![d, v]) (by norm_num) hd hno (by norm_num) + (by rw [hw]; norm_num) ν + have he : clippedError d v (![d, v] : Fin 2 → ℝ) = 0 := by simp [clippedError] + rw [he, mul_zero] at h + exact sub_eq_zero.mp (abs_nonpos_iff.mp h) + +-- The explicit dyadic schedule discharges all small-floor conditions, even with a real change. +example : + |(iterate univ (fun _ => 1) (fun _ => 1) (dyadicFloor 1 1) + (fun _ => 0) zeroState 1).row 0 0 - + uncompressedRow (fun _ => 0) zeroState.row 1 0 0| ≤ 3 / 256 := by + have h := abs_iterate_sub_uncompressed_le_weighted_dyadic (s := univ) + (n := fun _ => 1) (K := fun _ => 1) (Δ := fun _ => 0) (a := zeroState) + (η := 1) (d := 1) (v := 0) (by norm_num) le_rfl 1 1 le_rfl + (by + intro i hi + interval_cases i + norm_num [stepThreshold, inputRow, iterate, zeroState, dyadicFloor, dyadicSlack, + threshold, kthLargest, entrySize, Fin.univ_succ]) 0 0 + norm_num [dyadicFloor, dyadicSlack, uncompressedRow, zeroState, clippedError] at h ⊢ + exact h + +end ComplexityTests.RowCompressionPreloss From 13625a79f47c613501e2ee1ab77da3565f7993b4 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:54:01 +0000 Subject: [PATCH 5/7] feat(logspace): preserve stationary reference outputs under compression Define the padded first-coordinate rank and prove concrete threshold, default, row-bound and rank preservation results for stationary references. Above the flat region, the rank stays fixed; inside it, the rank remains in the flat region. A gated row output with separated entry support therefore survives each update and any finite zero-increment schedule with floors at most eta and capacities at least the fixed positive rank K. This formalizes the stationary-output assertion of OpenAI2026LogSpace, Section 8.3, Lemma 8.2, revision 7ef5c0cc. It does not assert equality of whole rows, a root-discrepancy estimate, or post-overflow stability. The explicit support and gate hypotheses do not assume the preservation conclusion. Validation on base 7d08e44bbdb626b74adaa9c4d63e07faa28ce525: direct Lean 4.36.0-rc2 checks of both new files passed without diagnostics, using private outputs and existing parent-checkout dependencies read-only. Tests exhibit an above-flat rank fixed at 1/2 while a zero entry moves to 3/8, an arbitrary stationary iteration retaining nonzero output 21/2, and a low rank moving from zero to 1/8 while output 41/4 is preserved. Focused proof hygiene including --check-simp and staged git diff --check passed. Aggregate regeneration and the full project gates remain integration work. AI assistance: ChatGPT implemented and checked these proofs as worker codex-compression-iteration-20261030. Independent agent source/API review: codex-logspace-polynomial-cutoffs-20261030 approved 10a516829a8cf8ea4fd0da6a65abe00147525b46. Publication changes only dependency ancestry and generated aggregate registration. Integrated strict module/test builds and committed import/hygiene checks pass. Full gates run in PR CI. --- Complexity.lean | 1 + .../Analysis/RowCompression/Reference.lean | 292 ++++++++++++++++++ ComplexityTests/RowCompressionReference.lean | 177 +++++++++++ 3 files changed, 470 insertions(+) create mode 100644 Complexity/Foundations/Analysis/RowCompression/Reference.lean create mode 100644 ComplexityTests/RowCompressionReference.lean diff --git a/Complexity.lean b/Complexity.lean index 93cdc9f6f..e492a325c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2355,6 +2355,7 @@ public import Complexity.Foundations.Analysis.RowCompression 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.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli diff --git a/Complexity/Foundations/Analysis/RowCompression/Reference.lean b/Complexity/Foundations/Analysis/RowCompression/Reference.lean new file mode 100644 index 000000000..e366049ce --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/Reference.lean @@ -0,0 +1,292 @@ +/- +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.Iteration +import Mathlib.Tactic.Linarith + +/-! +# Stationary reference rows under compression + +This module proves the stationary-output assertion of [OpenAI2026LogSpace, Lemma 8.2]. +The first coordinates of a reference row are at least `-η`, and the absolute values of its +second coordinates are at most `η`. Compression has floor at most `η` and capacity `n ≥ K`. +Write `q` for the `K`-th first-coordinate rank padded by the old default. The actual threshold, +new default and new padded rank are at most `max η q`. If `η < q`, the padded rank is preserved +exactly; otherwise both old and new ranks remain in `[0,η]`. The row bounds are preserved too. + +A row output `H(first, second, rank)` is preserved when it is zero below an entry threshold `e`, +zero above a gate-closing rank `g`, and independent of rank within `[0,η]`, where +`η < g` and `3 * g < e`. When the gate is open, entries above `e` are unchanged and entries +below `e` cannot enter the support. The theorem also iterates the concrete updates with no +increments, allowing arbitrary floors at most `η` and capacities at least the fixed rank `K`. + +This is output preservation, not equality of whole rows: defaults and small entries may move. +No root-discrepancy bound, comparison with a perturbed reference, or post-overflow error estimate +is asserted. The arithmetic rank includes zero padding; for the source's nonnegative defaults +it agrees with padding by arbitrarily many copies of the default. + +## Main definitions + +* `Cslib.RowCompression.firstRank`: the padded first-coordinate rank. + +## Main results + +* `Cslib.RowCompression.reference_threshold_le`: the actual threshold is at most `max η q`. +* `Cslib.RowCompression.reference_firstRank_eq`: ranks above `η` are preserved exactly. +* `Cslib.RowCompression.reference_update_output_eq`: a gated row output is preserved. +* `Cslib.RowCompression.reference_iterate_output_eq`: preservation through zero-increment + iteration. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, Lemma 8.2, stationary-reference assertion + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} + +/-- The first-coordinate rank, padded by the old default as well as zero. For a nonnegative +default this is the rank obtained by adjoining arbitrarily many copies of `(z,0)`. -/ +@[expose] noncomputable def firstRank (s : Finset ι) (K : ℕ) (z : ℝ) + (w : ι → Fin 2 → ℝ) : ℝ := max z (kthLargest K s fun y => w y 0) + +variable {s : Finset ι} {n K : ℕ} {ρ z η : ℝ} {w : ι → Fin 2 → ℝ} + +theorem firstRank_nonneg : 0 ≤ firstRank s K z w := + kthLargest_nonneg.trans (le_max_right _ _) + +theorem default_le_firstRank : z ≤ firstRank s K z w := le_max_left _ _ + +theorem kthLargest_le_firstRank : kthLargest K s (fun y => w y 0) ≤ firstRank s K z w := + le_max_right _ _ + +/-- With small negative first coordinates and small second coordinates, size ranks cannot +exceed the first-coordinate rank or `η`, whichever is larger. -/ +theorem reference_threshold_le (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n) + (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) : + threshold s n ρ z w ≤ max η (firstRank s K z w) := by + let Q := max η (firstRank s K z w) + have hηQ : η ≤ Q := le_max_left _ _ + have hqQ : firstRank s K z w ≤ Q := le_max_right _ _ + have hQ0 : 0 ≤ Q := hη.trans hηQ + have hrank : kthLargest n s (fun y => entrySize (w y)) ≤ Q := by + by_contra h + have hcard := (lt_kthLargest_iff (hK.trans_le hKn) hQ0).mp (lt_of_not_ge h) + have hsub : ({y ∈ s | Q < entrySize (w y)} : Finset ι) ⊆ {y ∈ s | Q < w y 0} := by + intro y hy + obtain ⟨hys, hy⟩ := mem_filter.mp hy + refine mem_filter.mpr ⟨hys, ?_⟩ + by_contra hfirstQ + have hsize : entrySize (w y) ≤ Q := + max_le (abs_le.mpr ⟨by linarith [hfirst y hys], not_lt.mp hfirstQ⟩) + ((hsecond y hys).trans hηQ) + exact (not_lt_of_ge hsize) hy + have hfirstRank : Q < kthLargest K s (fun y => w y 0) := + (lt_kthLargest_iff hK hQ0).mpr (hKn.trans (hcard.trans (card_le_card hsub))) + exact (not_lt_of_ge (kthLargest_le_firstRank.trans hqQ)) hfirstRank + exact max_le (default_le_firstRank.trans hqQ) (max_le (hρ.trans hηQ) hrank) + +/-- The new default is at most the larger of `η` and the old padded rank. -/ +theorem reference_newDefault_le (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n) + (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) : + newDefault s n K ρ z w ≤ max η (firstRank s K z w) := + max_le (reference_threshold_le hη hρ hK hKn hfirst hsecond) + ((min_le_left _ _).trans (le_max_right _ _)) + +/-- Moving coordinates toward a nonnegative first-coordinate default and zero second +coordinate preserves the reference row's small negative and second-coordinate bounds. -/ +theorem reference_update_bounds (hη : 0 ≤ η) {y : ι} + (hfirst : -η ≤ w y 0) (hsecond : |w y 1| ≤ η) : + -η ≤ update s n K ρ z w y 0 ∧ |update s n K ρ z w y 1| ≤ η := by + have h0 := update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z) (w := w) y 0 + have h1 := update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z) (w := w) y 1 + change min (w y 0) (newDefault s n K ρ z w) ≤ update s n K ρ z w y 0 ∧ + update s n K ρ z w y 0 ≤ max (w y 0) (newDefault s n K ρ z w) at h0 + change min (w y 1) 0 ≤ update s n K ρ z w y 1 ∧ + update s n K ρ z w y 1 ≤ max (w y 1) 0 at h1 + have hznew : 0 ≤ newDefault s n K ρ z w := newDefault_nonneg + refine ⟨(le_min hfirst (by linarith)).trans h0.1, abs_le.mpr ⟨?_, ?_⟩⟩ + · exact (le_min (abs_le.mp hsecond).1 (by linarith)).trans h1.1 + · exact h1.2.trans (max_le (abs_le.mp hsecond).2 hη) + +/-- The new padded rank is at most the larger of `η` and the old padded rank. -/ +theorem reference_firstRank_le (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n) + (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) : + firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w) ≤ + max η (firstRank s K z w) := by + let Q := max η (firstRank s K z w) + have hQ0 : 0 ≤ Q := hη.trans (le_max_left _ _) + have hb : newDefault s n K ρ z w ≤ Q := + reference_newDefault_le hη hρ hK hKn hfirst hsecond + refine max_le hb ?_ + by_contra h + have hcard := (lt_kthLargest_iff hK hQ0).mp (lt_of_not_ge h) + have hsub : ({y ∈ s | Q < update s n K ρ z w y 0} : Finset ι) ⊆ + {y ∈ s | Q < w y 0} := by + intro y hy + obtain ⟨hys, hy⟩ := mem_filter.mp hy + refine mem_filter.mpr ⟨hys, ?_⟩ + by_contra hfirstQ + have hu := (update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z) (w := w) y 0).2 + change update s n K ρ z w y 0 ≤ max (w y 0) (newDefault s n K ρ z w) at hu + exact (not_lt_of_ge (hu.trans (max_le (not_lt.mp hfirstQ) hb))) hy + have hfirstRank : Q < kthLargest K s (fun y => w y 0) := + (lt_kthLargest_iff hK hQ0).mpr (hcard.trans (card_le_card hsub)) + exact (not_lt_of_ge (kthLargest_le_firstRank.trans (le_max_right _ _))) hfirstRank + +/-- Above the flat rank region, the padded rank is preserved exactly. If the new default +does not already equal the old rank, all old rank witnesses lie in the identity region. -/ +theorem reference_firstRank_eq (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n) + (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) + (hq : η < firstRank s K z w) : + firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w) = firstRank s K z w := by + have hu : threshold s n ρ z w ≤ firstRank s K z w := by + simpa only [max_eq_right hq.le] using + reference_threshold_le (z := z) hη hρ hK hKn hfirst hsecond + refine le_antisymm ?_ ?_ + · simpa only [max_eq_right hq.le] using + reference_firstRank_le (z := z) hη hρ hK hKn hfirst hsecond + by_cases hqu : firstRank s K z w ≤ 3 * threshold s n ρ z w + · have hb : newDefault s n K ρ z w = firstRank s K z w := by + change max (threshold s n ρ z w) (min (firstRank s K z w) (3 * threshold s n ρ z w)) = _ + rw [min_eq_left hqu, max_eq_right hu] + exact hb ▸ (default_le_firstRank (s := s) (K := K) (z := newDefault s n K ρ z w) + (w := update s n K ρ z w)) + have h3u : 3 * threshold s n ρ z w < firstRank s K z w := lt_of_not_ge hqu + have hzq : z < firstRank s K z w := by + have hz : z ≤ threshold s n ρ z w := le_threshold + have hu0 : 0 ≤ threshold s n ρ z w := threshold_nonneg + linarith + have hqreal : firstRank s K z w ≤ kthLargest K s (fun y => w y 0) := by + have hmax := le_max_iff.mp + (show firstRank s K z w ≤ max z (kthLargest K s fun y => w y 0) from le_rfl) + exact hmax.resolve_left (not_le.mpr hzq) + have hq0 : 0 < firstRank s K z w := hη.trans_lt hq + have hcard := (le_kthLargest_iff hK hq0).mp hqreal + have hsub : ({y ∈ s | firstRank s K z w ≤ w y 0} : Finset ι) ⊆ + {y ∈ s | firstRank s K z w ≤ update s n K ρ z w y 0} := by + intro y hy + obtain ⟨hys, hy⟩ := mem_filter.mp hy + refine mem_filter.mpr ⟨hys, ?_⟩ + have hid : update s n K ρ z w y = w y := + update_eq_self_of_three_mul_le + (h3u.le.trans ((hy.trans (le_abs_self _)).trans (abs_apply_le_entrySize (w y) 0))) + rw [hid] + exact hy + exact ((le_kthLargest_iff hK hq0).mpr (hcard.trans (card_le_card hsub))).trans + kthLargest_le_firstRank + +/-- Compression preserves any row output with a separated entry support and rank gate, and +with no rank sensitivity in `[0,η]`. These are the structural hypotheses used in the +stationary-reference part of [OpenAI2026LogSpace, Lemma 8.2]. -/ +theorem reference_update_output_eq {H : ℝ → ℝ → ℝ → ℝ} {g e : ℝ} + (hη : 0 ≤ η) (hρ : ρ ≤ η) (hK : 0 < K) (hKn : K ≤ n) + (hfirst : ∀ y ∈ s, -η ≤ w y 0) (hsecond : ∀ y ∈ s, |w y 1| ≤ η) + (hηg : η < g) (hge : 3 * g < e) + (hentry : ∀ x v r, x ≤ e → H x v r = 0) + (hgate : ∀ x v r, g ≤ r → H x v r = 0) + (hflat : ∀ x v q r, q ∈ Set.Icc 0 η → r ∈ Set.Icc 0 η → H x v q = H x v r) + (y : ι) (_hy : y ∈ s) : + H (update s n K ρ z w y 0) (update s n K ρ z w y 1) + (firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w)) = + H (w y 0) (w y 1) (firstRank s K z w) := by + let q := firstRank s K z w + let q' := firstRank s K (newDefault s n K ρ z w) (update s n K ρ z w) + change H (update s n K ρ z w y 0) (update s n K ρ z w y 1) q' = H (w y 0) (w y 1) q + by_cases hclosed : g ≤ q + · have heq : q' = q := + reference_firstRank_eq hη hρ hK hKn hfirst hsecond (hηg.trans_le hclosed) + rw [heq, hgate _ _ _ hclosed, hgate _ _ _ hclosed] + have hQg : max η q < g := max_lt hηg (lt_of_not_ge hclosed) + have hg0 : 0 < g := hη.trans_lt hηg + have hu : threshold s n ρ z w ≤ max η q := + reference_threshold_le hη hρ hK hKn hfirst hsecond + have hb : newDefault s n K ρ z w ≤ max η q := + reference_newDefault_le hη hρ hK hKn hfirst hsecond + have hb_e : newDefault s n K ρ z w ≤ e := by linarith + by_cases hsmall : w y 0 ≤ e + · have hcoord := (update_mem_Icc (s := s) (n := n) (K := K) (ρ := ρ) (z := z) + (w := w) y 0).2 + change update s n K ρ z w y 0 ≤ max (w y 0) (newDefault s n K ρ z w) at hcoord + have hnew : update s n K ρ z w y 0 ≤ e := hcoord.trans (max_le hsmall hb_e) + rw [hentry _ _ _ hnew, hentry _ _ _ hsmall] + have h3u : 3 * threshold s n ρ z w < e := by linarith + have hid : update s n K ρ z w y = w y := + update_eq_self_of_three_mul_le (h3u.le.trans ((lt_of_not_ge hsmall).le.trans + ((le_abs_self _).trans (abs_apply_le_entrySize (w y) 0)))) + rw [hid] + by_cases hq : η < q + · have heq : q' = q := reference_firstRank_eq hη hρ hK hKn hfirst hsecond hq + rw [heq] + have hqη : q ≤ η := not_lt.mp hq + have hq'η : q' ≤ η := by + have h := reference_firstRank_le (z := z) hη hρ hK hKn hfirst hsecond + exact h.trans (max_le le_rfl hqη) + exact hflat _ _ _ _ ⟨firstRank_nonneg, hq'η⟩ ⟨firstRank_nonneg, hqη⟩ + +section Iteration + +variable {n : ℕ → ℕ} {ρ : ℕ → ℝ} {a : State ι} + +/-- Zero-increment compression preserves the reference row's coordinate bounds at every +stage. This uses only movement toward the nonnegative default, not rank preservation. -/ +theorem reference_iterate_bounds (hη : 0 ≤ η) + (hfirst : ∀ y ∈ s, -η ≤ a.row y 0) (hsecond : ∀ y ∈ s, |a.row y 1| ≤ η) (j : ℕ) : + (∀ y ∈ s, -η ≤ (iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 0) ∧ + ∀ y ∈ s, |(iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 1| ≤ η := by + induction j with + | zero => exact ⟨hfirst, hsecond⟩ + | succ j ih => + have h (y : ι) (hy : y ∈ s) := reference_update_bounds (s := s) (n := n j) (K := K) + (ρ := ρ j) (z := (iterate s n (fun _ => K) ρ (fun _ => 0) a j).defaultValue) + hη (ih.1 y hy) (ih.2 y hy) + constructor + · intro y hy + simpa only [iterate_succ, advance, add_zero] using (h y hy).1 + · intro y hy + simpa only [iterate_succ, advance, add_zero] using (h y hy).2 + +/-- Stationary reference outputs survive any finite zero-increment compression schedule +whose floors are at most `η` and whose capacities are at least the fixed rank `K`. +Neither the row entries, the defaults, nor the chosen exception lists need remain fixed. -/ +theorem reference_iterate_output_eq {H : ℝ → ℝ → ℝ → ℝ} {g e : ℝ} + (hη : 0 ≤ η) (hK : 0 < K) + (hfirst : ∀ y ∈ s, -η ≤ a.row y 0) (hsecond : ∀ y ∈ s, |a.row y 1| ≤ η) + (hηg : η < g) (hge : 3 * g < e) + (hentry : ∀ x v r, x ≤ e → H x v r = 0) + (hgate : ∀ x v r, g ≤ r → H x v r = 0) + (hflat : ∀ x v q r, q ∈ Set.Icc 0 η → r ∈ Set.Icc 0 η → H x v q = H x v r) + (j : ℕ) (hn : ∀ i < j, K ≤ n i) (hρ : ∀ i < j, ρ i ≤ η) (y : ι) (hy : y ∈ s) : + H ((iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 0) + ((iterate s n (fun _ => K) ρ (fun _ => 0) a j).row y 1) + (firstRank s K (iterate s n (fun _ => K) ρ (fun _ => 0) a j).defaultValue + (iterate s n (fun _ => K) ρ (fun _ => 0) a j).row) = + H (a.row y 0) (a.row y 1) (firstRank s K a.defaultValue a.row) := by + induction j with + | zero => rfl + | succ j ih => + have hb := reference_iterate_bounds (n := n) (K := K) (ρ := ρ) hη hfirst hsecond j + have hstep := reference_update_output_eq (n := n j) (K := K) (ρ := ρ j) + (z := (iterate s n (fun _ => K) ρ (fun _ => 0) a j).defaultValue) + (H := H) hη (hρ j (Nat.lt_succ_self j)) hK (hn j (Nat.lt_succ_self j)) + hb.1 hb.2 hηg hge hentry hgate hflat y hy + have hprev := ih (fun i hi => hn i (Nat.lt_succ_of_lt hi)) + (fun i hi => hρ i (Nat.lt_succ_of_lt hi)) + simpa only [iterate_succ, advance, add_zero] using hstep.trans hprev + +end Iteration + +end Cslib.RowCompression diff --git a/ComplexityTests/RowCompressionReference.lean b/ComplexityTests/RowCompressionReference.lean new file mode 100644 index 000000000..bac8284bf --- /dev/null +++ b/ComplexityTests/RowCompressionReference.lean @@ -0,0 +1,177 @@ +/- +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.Reference +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum + +/-! +# Stationary reference examples + +In the first example the padded rank is above the flat region and stays exactly `1/2`, while a +zero row entry moves to the new default `3/8`. In the second example the padded rank itself +moves from zero to `1/8`, inside the flat region. A nonzero gated output is preserved in both. +-/ + +namespace ComplexityTests.RowCompressionReference + +open Finset Cslib.RowCompression + +private theorem univ_three : (univ : Finset (Fin 3)) = {0, 1, 2} := by decide + +private noncomputable def highRow : Fin 3 → Fin 2 → ℝ := ![![10, 0], ![1 / 2, 0], ![0, 0]] + +private theorem high_rank : firstRank univ 2 0 highRow = 1 / 2 := by + have hle : kthLargest 2 univ (fun y => highRow y 0) ≤ 1 / 2 := by + refine not_lt.mp fun hlt => ?_ + have hcard := (lt_kthLargest_iff (by norm_num) + (by norm_num : (0 : ℝ) ≤ 1 / 2)).mp hlt + have hsupport : ({y | (1 / 2 : ℝ) < highRow y 0} : Finset (Fin 3)) = {0} := by + ext y + fin_cases y <;> norm_num [highRow] + rw [hsupport] at hcard + norm_num at hcard + have hge : (1 / 2 : ℝ) ≤ kthLargest 2 univ (fun y => highRow y 0) := by + apply (le_kthLargest_iff (by norm_num) (by norm_num : (0 : ℝ) < 1 / 2)).mpr + have hsupport : ({y | (1 / 2 : ℝ) ≤ highRow y 0} : Finset (Fin 3)) = {0, 1} := by + ext y + fin_cases y <;> norm_num [highRow] + rw [hsupport] + norm_num + unfold firstRank + rw [le_antisymm hle hge] + norm_num + +private theorem high_threshold : threshold univ 3 (1 / 8) 0 highRow = 1 / 8 := by + have hr : kthLargest 3 univ (fun y => entrySize (highRow 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 (highRow y)} : Finset (Fin 3)) = {0, 1} := by + ext y + fin_cases y <;> norm_num [entrySize, highRow] + rw [hsupport] at hcard + norm_num at hcard + norm_num [threshold, hr] + +private theorem high_default : newDefault univ 3 2 (1 / 8) 0 highRow = 3 / 8 := by + change max (threshold univ 3 (1 / 8) 0 highRow) + (min (firstRank univ 2 0 highRow) (3 * threshold univ 3 (1 / 8) 0 highRow)) = _ + rw [high_threshold, high_rank] + norm_num + +private theorem high_update : update univ 3 2 (1 / 8) 0 highRow = + ![![10, 0], ![1 / 2, 0], ![3 / 8, 0]] := by + unfold update + rw [high_threshold, high_default] + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [updateEntry, radius, entrySize, defaultEntry, highRow] + +private theorem high_first (y : Fin 3) (_hy : y ∈ (univ : Finset (Fin 3))) : + -(1 / 4 : ℝ) ≤ highRow y 0 := by + fin_cases y <;> norm_num [highRow] + +private theorem high_second (y : Fin 3) (_hy : y ∈ (univ : Finset (Fin 3))) : + |highRow y 1| ≤ (1 / 4 : ℝ) := by + fin_cases y <;> norm_num [highRow] + +-- The rank theorem applies to a row whose default and some actual entries really move. +example : firstRank univ 2 (newDefault univ 3 2 (1 / 8) 0 highRow) + (update univ 3 2 (1 / 8) 0 highRow) = 1 / 2 := by + have h := reference_firstRank_eq (η := 1 / 4) (by norm_num) (by norm_num : (1 / 8 : ℝ) ≤ 1 / 4) + (by norm_num : 0 < (2 : ℕ)) (by norm_num : (2 : ℕ) ≤ 3) high_first high_second + (by rw [high_rank]; norm_num) + exact h.trans high_rank + +example : update univ 3 2 (1 / 8) 0 highRow 2 0 ≠ highRow 2 0 := by + rw [high_update] + norm_num [highRow] + +private noncomputable def rowOutput (x v r : ℝ) : ℝ := + if x ≤ 4 then 0 else if 1 ≤ r then 0 else x + v + max (1 / 4) r + +private theorem output_entry (x v r : ℝ) (hx : x ≤ 4) : rowOutput x v r = 0 := by + simp [rowOutput, hx] + +private theorem output_gate (x v r : ℝ) (hr : 1 ≤ r) : rowOutput x v r = 0 := by + simp [rowOutput, hr] + +private theorem output_flat (x v q r : ℝ) (hq : q ∈ Set.Icc 0 (1 / 4 : ℝ)) + (hr : r ∈ Set.Icc 0 (1 / 4 : ℝ)) : rowOutput x v q = rowOutput x v r := by + have hq' : ¬1 ≤ q := by linarith [hq.2] + have hr' : ¬1 ≤ r := by linarith [hr.2] + simp only [rowOutput, hq', hr', ↓reduceIte, max_eq_left hq.2, max_eq_left hr.2] + +private noncomputable def initial : State (Fin 3) := { defaultValue := 0, row := highRow } + +-- An arbitrary number of zero-increment updates preserves the nonzero output 10.5. +example (j : ℕ) : + let a := iterate univ (fun _ => 3) (fun _ => 2) (fun _ => 1 / 8) (fun _ => 0) initial j + rowOutput (a.row 0 0) (a.row 0 1) (firstRank univ 2 a.defaultValue a.row) = 21 / 2 := by + have h := reference_iterate_output_eq (s := univ) (n := fun _ => 3) (K := 2) + (ρ := fun _ => 1 / 8) (a := initial) (η := 1 / 4) (H := rowOutput) (g := 1) (e := 4) + (by norm_num) (by norm_num) high_first high_second (by norm_num) (by norm_num) + output_entry output_gate output_flat j (by intros; norm_num) (by intros; norm_num) 0 + (mem_univ 0) + refine h.trans ?_ + change rowOutput 10 0 (firstRank univ 2 0 highRow) = 21 / 2 + rw [high_rank] + norm_num [rowOutput] + +private def lowRow : Fin 3 → Fin 2 → ℝ := ![![10, 0], ![0, 0], ![0, 0]] + +private theorem low_rank : firstRank univ 2 0 lowRow = 0 := by + norm_num [firstRank, kthLargest, lowRow, univ_three, filter_insert, filter_image, + filter_singleton] + +private theorem low_threshold : threshold univ 3 (1 / 8) 0 lowRow = 1 / 8 := by + norm_num [threshold, kthLargest, lowRow, entrySize, univ_three, filter_insert, + filter_image, filter_singleton] + +private theorem low_default : newDefault univ 3 2 (1 / 8) 0 lowRow = 1 / 8 := by + change max (threshold univ 3 (1 / 8) 0 lowRow) + (min (firstRank univ 2 0 lowRow) (3 * threshold univ 3 (1 / 8) 0 lowRow)) = _ + rw [low_threshold, low_rank] + norm_num + +private theorem low_update : update univ 3 2 (1 / 8) 0 lowRow = + ![![10, 0], ![1 / 8, 0], ![1 / 8, 0]] := by + unfold update + rw [low_threshold, low_default] + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [updateEntry, radius, entrySize, defaultEntry, lowRow] + +-- A low padded rank may change; the theorem requires only flat output dependence there. +example : firstRank univ 2 (newDefault univ 3 2 (1 / 8) 0 lowRow) + (update univ 3 2 (1 / 8) 0 lowRow) = 1 / 8 ∧ firstRank univ 2 0 lowRow = 0 := by + refine ⟨le_antisymm ?_ ?_, low_rank⟩ + · have h := reference_firstRank_le (s := univ) (n := 3) (K := 2) (ρ := 1 / 8) (z := 0) + (w := lowRow) (η := 1 / 8) (by norm_num) le_rfl (by norm_num) (by norm_num) + (fun y _ => by fin_cases y <;> norm_num [lowRow]) + (fun y _ => by fin_cases y <;> norm_num [lowRow]) + simpa only [low_rank, max_eq_left (by norm_num : (0 : ℝ) ≤ 1 / 8)] using h + · have h := default_le_firstRank (s := univ) (K := 2) + (z := newDefault univ 3 2 (1 / 8) 0 lowRow) (w := update univ 3 2 (1 / 8) 0 lowRow) + simpa only [low_default] using h + +example : rowOutput (update univ 3 2 (1 / 8) 0 lowRow 0 0) + (update univ 3 2 (1 / 8) 0 lowRow 0 1) + (firstRank univ 2 (newDefault univ 3 2 (1 / 8) 0 lowRow) + (update univ 3 2 (1 / 8) 0 lowRow)) = 41 / 4 := by + have h := reference_update_output_eq (s := univ) (n := 3) (K := 2) (ρ := 1 / 8) (z := 0) + (w := lowRow) (η := 1 / 4) (H := rowOutput) (g := 1) (e := 4) + (by norm_num) (by norm_num) (by norm_num) (by norm_num) + (fun y _ => by fin_cases y <;> norm_num [lowRow]) + (fun y _ => by fin_cases y <;> norm_num [lowRow]) + (by norm_num) (by norm_num) output_entry output_gate output_flat 0 (mem_univ 0) + refine h.trans ?_ + rw [low_rank] + norm_num [rowOutput, lowRow] + +end ComplexityTests.RowCompressionReference From 62a7cba7828b1b2a34cb6314543aa2701f45d355 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:13:08 +0000 Subject: [PATCH 6/7] feat(logspace): construct and compare stationary compression references Construct the reference state from the actual current default and true row plus accumulated compression preloss. Derive its small-negative and second-coordinate bounds from no-overflow dyadic floors, then preserve gated outputs through the remaining capacities and floors at their original indices with zero increments. Add a separate weighted root comparison with the true zero-padded output. Sensitive targets use the existing weighted preloss bound at eta/2; uniform small loss and lower clipping remove the low targets from the rank comparison. The theorem assumes scalar support, flatness and root-Lipschitz laws and a raw-prefix error envelope only at sensitive targets, not the final output estimate. It is exponent-parametric. Instantiating all source row functions and comparison to a subsequent incremented or post-overflow calculation remain separate. Source mapping: OpenAI2026LogSpace, Section 8.3, Lemma 8.2, revision 7ef5c0cc. This connects the reviewed Preloss and Reference layers using the documented margin-scaled dyadic witness. Existing files and aggregates are unchanged. Validation: pinned Lean 4.36.0-rc2 checked the new module and tests without diagnostics, using private outputs and read-only shared dependencies. Tests exhibit a nonzero increment, nonzero actual preloss, preserved nonzero output through the shifted remaining schedule, and a strictly positive fourth-root discrepancy. The review-requested low-target regression raises the padded rank from zero to 1/1048576 while a rank-dependent fourth-root output remains exactly one under a zero sensitive-target error envelope. Focused hygiene with --check-simp and staged diff checking pass. Full project gates and aggregate regeneration remain integration work. AI assistance: ChatGPT implemented and checked this milestone as worker codex-compression-iteration-20261030. Independent reviewer codex-logspace-polynomial-cutoffs-20261030 requested the low-target regression and is reviewing the frozen revision. Independent non-author source/API review by compression_review approved exact source revision c7873d034846fbab13b83d3d9a4d596343c9d191, including a rank-dependent low-target regression. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 1 + .../Analysis/RowCompression/Stationary.lean | 307 ++++++++++++++++ ComplexityTests/RowCompressionStationary.lean | 330 ++++++++++++++++++ 3 files changed, 638 insertions(+) create mode 100644 Complexity/Foundations/Analysis/RowCompression/Stationary.lean create mode 100644 ComplexityTests/RowCompressionStationary.lean diff --git a/Complexity.lean b/Complexity.lean index e492a325c..ee0aafd7a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2356,6 +2356,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.Stationary 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/Stationary.lean b/Complexity/Foundations/Analysis/RowCompression/Stationary.lean new file mode 100644 index 000000000..b892efd0d --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/Stationary.lean @@ -0,0 +1,307 @@ +/- +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.Preloss +public import Complexity.Foundations.Analysis.RowCompression.Reference +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Algebra.Order.Group.MinMax +import Mathlib.Tactic.Linarith + +/-! +# The stationary reference constructed from actual preloss + +At the input of zero-based group `j`, the stationary reference in +[OpenAI2026LogSpace, Lemma 8.2] has the current default and row `truth + loss`, where `loss` is +the actual compressed prefix minus its uncompressed counterpart. `stationaryState` constructs +this state from `iterate`; `stationaryContinuation` runs the remaining capacities and floors +from their original indices, with no further increments. + +For the explicit scaled dyadic floors, absence of overflow in groups `i < j ≤ m` bounds this +loss by `η / 100`. Consequently a true row with nonnegative first coordinates and second +coordinates of magnitude at most `η / 2` produces a reference with first coordinates at least +`-η` and second coordinates of magnitude at most `η`. The stationary preservation theorem then +applies to the actual remaining schedule. Its entry-support, rank-gate, and flat-region +hypotheses are scalar properties of the row output, not an assumed preservation conclusion. + +Under explicit scalar support, flatness and root-Lipschitz laws, weighted preloss also controls +the reference's discrepancy from the true zero-padded output. A lower clipping at `η` removes +the influence of targets below `η / 2`, while rank stability controls the sensitive targets. +This comparison allows any exponent satisfying the stated scalar law; instantiating those laws +for all of the paper's row functions remains a separate obligation. + +The zero-based prefix loss here is the paper's `L_{j-1}` before its group `j`. The floors are +the explicitly documented margin-scaled witness from `RowCompression.Floors`. This module +does not assert a post-overflow comparison with the incremented calculation or a machine-space +bound. + +## Main definitions + +* `Cslib.RowCompression.stationaryState`: the true row plus the actual accumulated preloss. +* `Cslib.RowCompression.stationaryContinuation`: the reference's shifted zero-increment run. + +## Main results + +* `Cslib.RowCompression.abs_stationaryState_row_sub_le_dyadic`: uniform small preloss. +* `Cslib.RowCompression.stationaryState_bounds_dyadic`: the constructed reference's shape. +* `Cslib.RowCompression.stationaryContinuation_output_eq_dyadic`: preservation along the + remaining compression schedule. +* `Cslib.RowCompression.abs_stationaryState_root_sub_le_weighted_dyadic`: a weighted + root-discrepancy bound under explicit scalar root-Lipschitz and support laws. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, Lemma 8.2, stationary-reference construction, preservation, and root comparison + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} + +/-- The reference at a prefix has the current default and the true row plus the compression +loss already accumulated by the actual calculation. -/ +@[expose] noncomputable def stationaryState (s : Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (truth : ι → Fin 2 → ℝ) (j : ℕ) : State ι := + { defaultValue := (iterate s n K ρ Δ a j).defaultValue + row := fun y ν => truth y ν + + ((iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν) } + +/-- Continue the constructed reference with the actual capacities and floors starting at +group `j`, a fixed positive rank in applications, and no further increments. -/ +@[expose] noncomputable def stationaryContinuation (s : Finset ι) (n : ℕ → ℕ) (K : ℕ) + (ρ : ℕ → ℝ) (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (truth : ι → Fin 2 → ℝ) + (j r : ℕ) : State ι := + iterate s (fun i => n (j + i)) (fun _ => K) (fun i => ρ (j + i)) (fun _ => 0) + (stationaryState s n (fun _ => K) ρ Δ a truth j) r + +variable {s : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {truth : ι → Fin 2 → ℝ} {η : ℝ} + +/-- The reference's discrepancy from truth is exactly the actual compression loss. -/ +theorem stationaryState_row_sub (j : ℕ) (y : ι) (ν : Fin 2) : + (stationaryState s n K ρ Δ a truth j).row y ν - truth y ν = + (iterate s n K ρ Δ a j).row y ν - uncompressedRow Δ a.row j y ν := by + simp only [stationaryState, add_sub_cancel_left] + +private theorem six_sum_prefix_dyadicFloor_le (hη : 0 ≤ η) {m j : ℕ} (hj : j ≤ m) : + 6 * ∑ i ∈ range j, dyadicFloor η m i ≤ η / 100 := by + have hsum : ∑ i ∈ range j, dyadicFloor η m i ≤ ∑ i ∈ range m, dyadicFloor η m i := + sum_le_sum_of_subset_of_nonneg (range_mono hj) (fun i _ _ => dyadicFloor_nonneg hη m i) + exact (mul_le_mul_of_nonneg_left hsum (by norm_num)).trans + (six_sum_range_dyadicFloor_le_scale hη m) + +/-- The constructed reference differs from truth by at most `η / 100` before overflow. +The numerical bound comes from the actual dyadic schedule, not an assumed error budget. -/ +theorem abs_stationaryState_row_sub_le_dyadic (hη : 0 ≤ η) (m j : ℕ) (hj : j ≤ m) + (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) + (y : ι) (ν : Fin 2) : + |(stationaryState s n K (dyadicFloor η m) Δ a truth j).row y ν - truth y ν| ≤ η / 100 := by + rw [stationaryState_row_sub] + exact (abs_iterate_sub_uncompressed_le_of_no_overflow j hno y ν).trans + (six_sum_prefix_dyadicFloor_le hη hj) + +/-- The true-row bounds and the proved preloss bound imply the shape needed by stationary +compression preservation. The reference row itself need not be nonnegative. -/ +theorem stationaryState_bounds_dyadic (hη : 0 ≤ η) (m j : ℕ) (hj : j ≤ m) + (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) + (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2) : + (∀ y ∈ s, -η ≤ (stationaryState s n K (dyadicFloor η m) Δ a truth j).row y 0) ∧ + ∀ y ∈ s, |(stationaryState s n K (dyadicFloor η m) Δ a truth j).row y 1| ≤ η := by + constructor + · intro y hy + have h := (abs_le.mp (abs_stationaryState_row_sub_le_dyadic (truth := truth) + hη m j hj hno y 0)).1 + linarith [hfirst y hy] + · intro y hy + have h := abs_le.mp (abs_stationaryState_row_sub_le_dyadic (truth := truth) + hη m j hj hno y 1) + have ht := abs_le.mp (hsecond y hy) + exact abs_le.mpr ⟨by linarith, by linarith⟩ + +/-- A small initial default remains below the flat-rank threshold before overflow. This is +useful when comparing the padded reference rank to the true row's zero-padded rank. -/ +theorem stationaryState_defaultValue_le_dyadic (hη : 0 ≤ η) + (ha : 0 ≤ a.defaultValue) (haη : a.defaultValue ≤ η / 2) (m j : ℕ) (hj : j ≤ m) + (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) : + (stationaryState s n K (dyadicFloor η m) Δ a truth j).defaultValue ≤ η := by + have h := le_of_abs_le (abs_iterate_defaultValue_sub_le_of_no_overflow ha j hno) + have hsum := six_sum_prefix_dyadicFloor_le hη hj + change (iterate s n K (dyadicFloor η m) Δ a j).defaultValue ≤ η + linarith + +/-- The stationary reference constructed from actual preloss preserves its output through +any initial segment of the remaining schedule. Only earlier groups must avoid overflow. -/ +theorem stationaryContinuation_output_eq_dyadic {K : ℕ} {H : ℝ → ℝ → ℝ → ℝ} {g e : ℝ} + (hη : 0 ≤ η) (hK : 0 < K) (m j r : ℕ) (hr : j + r ≤ m) + (hno : ∀ i < j, + stepThreshold s n (fun _ => K) (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) + (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2) + (hn : ∀ i, j ≤ i → i < m → K ≤ n i) (hηg : η < g) (hge : 3 * g < e) + (hentry : ∀ x v q, x ≤ e → H x v q = 0) + (hgate : ∀ x v q, g ≤ q → H x v q = 0) + (hflat : ∀ x v q q', q ∈ Set.Icc 0 η → q' ∈ Set.Icc 0 η → H x v q = H x v q') + (y : ι) (hy : y ∈ s) : + let b := stationaryState s n (fun _ => K) (dyadicFloor η m) Δ a truth j + let c := stationaryContinuation s n K (dyadicFloor η m) Δ a truth j r + H (c.row y 0) (c.row y 1) (firstRank s K c.defaultValue c.row) = + H (b.row y 0) (b.row y 1) (firstRank s K b.defaultValue b.row) := by + have hj : j ≤ m := (Nat.le_add_right j r).trans hr + have hb := stationaryState_bounds_dyadic hη m j hj hno hfirst hsecond + apply reference_iterate_output_eq hη hK hb.1 hb.2 hηg hge hentry hgate hflat r + · intro i hi + exact hn (j + i) (Nat.le_add_right _ _) (by omega) + · intro i _ + have h := dyadicFloor_le_scale_div hη m (j + i) + linarith + · exact hy + +/-! ## Weighted discrepancy from the true output -/ + +/-- Weighted preloss applies at the smaller sensitivity threshold `η / 2` while using the +same floors scaled by `η`. Their explicit size also proves this stronger local margin. -/ +theorem abs_stationaryState_row_sub_le_weighted_dyadic (hη : 0 < η) (m j : ℕ) (hj : j ≤ m) + (hno : ∀ i < j, stepThreshold s n K (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) + (y : ι) (hd : η / 2 ≤ truth y 0) (ν : Fin 2) : + |(stationaryState s n K (dyadicFloor η m) Δ a truth j).row y ν - truth y ν| ≤ + (12 * (1 + η / 2) / (η / 2)) * ∑ i ∈ range j, + dyadicFloor η m i * + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) := by + rw [stationaryState_row_sub] + apply abs_iterate_sub_uncompressed_le_weighted (by linarith : 0 < η / 2) hd j hno + · intro i _ + have h := dyadicFloor_le_scale_div hη.le m i + linarith + · intro i hi + have hsum := six_sum_range_dyadicFloor_le hη.le (hi.trans_le hj) + have hfloor := dyadicFloor_nonneg hη.le m i + linarith + +private theorem max_rank_le_add_of_clipped {K : ℕ} {f g : ι → ℝ} {δ : ℝ} + (hK : 0 < K) (hη : 0 ≤ η) (hδ : 0 ≤ δ) + (h : ∀ y ∈ s, max η (f y) ≤ max η (g y) + δ) : + max η (kthLargest K s f) ≤ max η (kthLargest K s g) + δ := by + have ht : 0 ≤ max η (kthLargest K s g) := hη.trans (le_max_left _ _) + refine max_le (by linarith [le_max_left η (kthLargest K s g)]) ?_ + by_contra hrank + have hc := (lt_kthLargest_iff hK (add_nonneg ht hδ)).mp (lt_of_not_ge hrank) + have hsub : ({y ∈ s | max η (kthLargest K s g) + δ < f y} : Finset ι) ⊆ + {y ∈ s | max η (kthLargest K s g) < g y} := by + intro y hy + obtain ⟨hys, hy⟩ := mem_filter.mp hy + refine mem_filter.mpr ⟨hys, ?_⟩ + have hmax : max η (kthLargest K s g) < max η (g y) := by + linarith [h y hys, le_max_right η (f y)] + exact (lt_max_iff.mp hmax).resolve_left (not_lt_of_ge (le_max_left _ _)) + have hg := (lt_kthLargest_iff hK ht).mpr (hc.trans (card_le_card hsub)) + exact (not_lt_of_ge (le_max_right _ _)) hg + +private theorem abs_clipped_firstRank_sub_le {K : ℕ} {z z' δ : ℝ} + {w w' : ι → Fin 2 → ℝ} (hK : 0 < K) (hη : 0 ≤ η) (hδ : 0 ≤ δ) + (hz : z ≤ η) (hz' : z' ≤ η) + (h : ∀ y ∈ s, |max η (w y 0) - max η (w' y 0)| ≤ δ) : + |max η (firstRank s K z w) - max η (firstRank s K z' w')| ≤ δ := by + simp only [firstRank, ← max_assoc, max_eq_left hz, max_eq_left hz'] + rw [abs_sub_le_iff] + constructor + · exact sub_le_iff_le_add'.mpr (max_rank_le_add_of_clipped hK hη hδ fun y hy => + sub_le_iff_le_add'.mp (le_of_abs_le (h y hy))) + · exact sub_le_iff_le_add'.mpr (max_rank_le_add_of_clipped hK hη hδ fun y hy => + sub_le_iff_le_add'.mp (le_of_abs_le ((abs_sub_comm _ _).trans_le (h y hy)))) + +private theorem output_eq_lowerClipped {H : ℝ → ℝ → ℝ → ℝ} (hη : 0 ≤ η) + (hentry : ∀ x v q, x ≤ η → H x v q = 0) + (hflat : ∀ x v q q', q ∈ Set.Icc 0 η → q' ∈ Set.Icc 0 η → H x v q = H x v q') + (x v q : ℝ) (hq : 0 ≤ q) : H x v q = H (max η x) v (max η q) := by + by_cases hx : x ≤ η + · rw [max_eq_left hx, hentry _ _ _ hx, hentry _ _ _ le_rfl] + rw [max_eq_right (not_le.mp hx).le] + by_cases hqη : q ≤ η + · rw [max_eq_left hqη] + exact hflat x v q η ⟨hq, hqη⟩ ⟨hη, le_rfl⟩ + rw [max_eq_right (not_le.mp hqη).le] + +/-- A weighted discrepancy bound between the constructed stationary reference and truth. + +`ε i` bounds the clipped errors of the actual uncompressed prefix at endpoints with true first +coordinate at least `η / 2`. +The scalar root output is assumed Lipschitz on the clipped first-coordinate and rank region; +this is a regularity hypothesis about `H`, independent of the compression calculation. +Targets below `η / 2` remain below entry support by the proved uniform loss bound. Their +possibly larger relative errors therefore do not enter the weighted rank comparison. + +This theorem supplies the comparison at the start of the stationary calculation. Combined with +`stationaryContinuation_output_eq_dyadic`, it gives the same bound after its remaining updates. +Verifying these scalar laws for particular row functions is a separate obligation. -/ +theorem abs_stationaryState_root_sub_le_weighted_dyadic {K : ℕ} + {H : ℝ → ℝ → ℝ → ℝ} {p C : ℝ} {ε : ℕ → ℝ} + (hη : 0 < η) (hK : 0 < K) (hC : 0 ≤ C) + (ha : 0 ≤ a.defaultValue) (haη : a.defaultValue ≤ η / 2) + (m j : ℕ) (hj : j ≤ m) + (hno : ∀ i < j, + stepThreshold s n (fun _ => K) (dyadicFloor η m) Δ a i ≤ dyadicFloor η m i) + (hε : ∀ i < j, 0 ≤ ε i) + (herr : ∀ i < j, ∀ y ∈ s, η / 2 ≤ truth y 0 → + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) ≤ ε i) + (hentry : ∀ x v q, x ≤ η → H x v q = 0) + (hflat : ∀ x v q q', q ∈ Set.Icc 0 η → q' ∈ Set.Icc 0 η → H x v q = H x v q') + (hroot : ∀ x v q x' v' q', η ≤ x → η ≤ x' → η ≤ q → η ≤ q' → + |H x v q ^ p - H x' v' q' ^ p| ≤ + C * (|x - x'| + |v - v'| + |q - q'|)) (y : ι) (hy : y ∈ s) : + let b := stationaryState s n (fun _ => K) (dyadicFloor η m) Δ a truth j + |H (b.row y 0) (b.row y 1) (firstRank s K b.defaultValue b.row) ^ p - + H (truth y 0) (truth y 1) (firstRank s K 0 truth) ^ p| ≤ + 3 * C * ((12 * (1 + η / 2) / (η / 2)) * ∑ i ∈ range j, dyadicFloor η m i * ε i) := by + let b := stationaryState s n (fun _ => K) (dyadicFloor η m) Δ a truth j + let B := (12 * (1 + η / 2) / (η / 2)) * ∑ i ∈ range j, dyadicFloor η m i * ε i + change |H (b.row y 0) (b.row y 1) (firstRank s K b.defaultValue b.row) ^ p - + H (truth y 0) (truth y 1) (firstRank s K 0 truth) ^ p| ≤ 3 * C * B + have hcoef : 0 ≤ 12 * (1 + η / 2) / (η / 2) := by positivity + have hB : 0 ≤ B := mul_nonneg hcoef (sum_nonneg fun i hi => + mul_nonneg (dyadicFloor_nonneg hη.le m i) (hε i (mem_range.mp hi))) + have huniform (y : ι) (ν : Fin 2) : |b.row y ν - truth y ν| ≤ η / 100 := + abs_stationaryState_row_sub_le_dyadic hη.le m j hj hno y ν + have hweighted (y : ι) (hy : y ∈ s) (hd : η / 2 ≤ truth y 0) (ν : Fin 2) : + |b.row y ν - truth y ν| ≤ B := by + refine (abs_stationaryState_row_sub_le_weighted_dyadic hη m j hj hno y hd ν).trans ?_ + exact mul_le_mul_of_nonneg_left (sum_le_sum fun i hi => + mul_le_mul_of_nonneg_left (herr i (mem_range.mp hi) y hy hd) + (dyadicFloor_nonneg hη.le m i)) hcoef + have hlow (y : ι) (hy : truth y 0 < η / 2) : b.row y 0 ≤ η ∧ truth y 0 ≤ η := by + have h := le_of_abs_le (huniform y 0) + constructor <;> linarith + have hclipped (y : ι) (hy : y ∈ s) : |max η (b.row y 0) - max η (truth y 0)| ≤ B := by + by_cases hd : η / 2 ≤ truth y 0 + · exact (abs_max_sub_max_le_max _ _ _ _).trans + (max_le (by simpa using hB) (hweighted y hy hd 0)) + · have hl := hlow y (not_le.mp hd) + simpa only [max_eq_left hl.1, max_eq_left hl.2, sub_self, abs_zero] using hB + have hrank : |max η (firstRank s K b.defaultValue b.row) - + max η (firstRank s K 0 truth)| ≤ B := + abs_clipped_firstRank_sub_le hK hη.le hB + (stationaryState_defaultValue_le_dyadic hη.le ha haη m j hj hno) hη.le hclipped + by_cases hd : η / 2 ≤ truth y 0 + · rw [output_eq_lowerClipped hη.le hentry hflat _ _ _ firstRank_nonneg, + output_eq_lowerClipped hη.le hentry hflat _ _ _ firstRank_nonneg] + calc _ ≤ C * (|max η (b.row y 0) - max η (truth y 0)| + |b.row y 1 - truth y 1| + + |max η (firstRank s K b.defaultValue b.row) - max η (firstRank s K 0 truth)|) := + hroot _ _ _ _ _ _ (le_max_left _ _) (le_max_left _ _) (le_max_left _ _) (le_max_left _ _) + _ ≤ C * (B + B + B) := mul_le_mul_of_nonneg_left + (add_le_add (add_le_add (hclipped y hy) (hweighted y hy hd 1)) hrank) hC + _ = 3 * C * B := by ring + · have hl := hlow y (not_le.mp hd) + rw [hentry _ _ _ hl.1, hentry _ _ _ hl.2, sub_self, abs_zero] + positivity + +end Cslib.RowCompression diff --git a/ComplexityTests/RowCompressionStationary.lean b/ComplexityTests/RowCompressionStationary.lean new file mode 100644 index 000000000..71a159bfa --- /dev/null +++ b/ComplexityTests/RowCompressionStationary.lean @@ -0,0 +1,330 @@ +/- +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.Stationary +import Mathlib.Algebra.Order.Group.MinMax +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum +import Mathlib.Tactic.Ring + +/-! +# Constructed stationary-reference examples + +The first of two dyadic groups has a nonzero increment and actual nonzero compression loss. +The reference adds that loss to a different true row and retains the actual current default. +The remaining group preserves a nonzero gated output. A fourth-power ramp exhibits a strictly +positive fourth-root discrepancy and satisfies the weighted comparison theorem's scalar laws. +-/ + +namespace ComplexityTests.RowCompressionStationary + +open Finset Cslib.RowCompression + +private def initial : State (Fin 2) := { defaultValue := 0, row := ![![20, 0], ![0, 0]] } + +private def truth : Fin 2 → Fin 2 → ℝ := ![![20, 0], ![2, 0]] + +private noncomputable def increments (i : ℕ) : Fin 2 → Fin 2 → ℝ := + if i = 0 then ![![0, 0], ![1 / 2097152, 0]] else 0 + +private noncomputable def rawRow : Fin 2 → Fin 2 → ℝ := ![![20, 0], ![1 / 2097152, 0]] + +private theorem floor_zero : dyadicFloor 1 2 0 = 1 / 1048576 := by + norm_num [dyadicFloor, dyadicSlack] + +private theorem raw_rank_le : kthLargest 2 univ (fun y => rawRow y 0) ≤ 1 / 1048576 := by + refine not_lt.mp fun hlt => ?_ + have hcard := (lt_kthLargest_iff (by norm_num) + (by norm_num : (0 : ℝ) ≤ 1 / 1048576)).mp hlt + have hsupport : ({y | (1 / 1048576 : ℝ) < rawRow y 0} : Finset (Fin 2)) = {0} := by + ext y + fin_cases y <;> norm_num [rawRow] + rw [hsupport] at hcard + norm_num at hcard + +private theorem raw_threshold : threshold univ 2 (1 / 1048576) 0 rawRow = 1 / 1048576 := by + have hs : (fun y => entrySize (rawRow y)) = fun y => rawRow y 0 := by + funext y + fin_cases y <;> norm_num [entrySize, rawRow] + refine le_antisymm ?_ floor_le_threshold + unfold threshold + rw [hs] + exact max_le (by norm_num) (max_le le_rfl raw_rank_le) + +private theorem raw_default : newDefault univ 2 2 (1 / 1048576) 0 rawRow = 1 / 1048576 := by + unfold newDefault + rw [raw_threshold] + exact max_eq_left ((min_le_left _ _).trans (max_le (by norm_num) raw_rank_le)) + +private theorem raw_one : uncompressedRow increments initial.row 1 = rawRow := by + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [uncompressedRow, initial, increments, rawRow] + +private theorem actual_one : + iterate univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial 1 = + { defaultValue := 1 / 1048576, row := ![![20, 0], ![1 / 1048576, 0]] } := by + have hin : initial.row + increments 0 = rawRow := by + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [initial, increments, rawRow] + change advance univ 2 2 (dyadicFloor 1 2 0) (increments 0) initial = _ + unfold advance + rw [hin, floor_zero] + change State.mk (newDefault univ 2 2 (1 / 1048576) 0 rawRow) + (update univ 2 2 (1 / 1048576) 0 rawRow) = _ + rw [raw_default] + congr 1 + unfold update + rw [raw_threshold, raw_default] + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [updateEntry, radius, entrySize, defaultEntry, rawRow] + +private theorem no_overflow : ∀ i < 1, + stepThreshold univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial i ≤ + dyadicFloor 1 2 i := by + intro i hi + have hi0 : i = 0 := by omega + subst i + have hin : inputRow univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial 0 = + rawRow := by + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [inputRow, initial, increments, rawRow] + unfold stepThreshold + rw [hin, iterate_zero, floor_zero] + exact raw_threshold.le + +private noncomputable def reference : State (Fin 2) := + stationaryState univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial truth 1 + +private theorem reference_eq : reference = + { defaultValue := 1 / 1048576, row := ![![20, 0], ![2 + 1 / 2097152, 0]] } := by + unfold reference stationaryState + rw [actual_one, raw_one] + congr 1 + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [truth, rawRow] + +-- The state is constructed from a nonzero increment and a strictly positive actual preloss. +example : increments 0 1 0 = 1 / 2097152 ∧ + reference.row 1 0 - truth 1 0 = 1 / 2097152 ∧ + reference.defaultValue = + (iterate univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) + increments initial 1).defaultValue := by + rw [reference_eq, actual_one] + norm_num [increments, truth] + +private theorem reference_rank : firstRank univ 2 reference.defaultValue reference.row = + 2 + 1 / 2097152 := by + have hle : kthLargest 2 univ (fun y => reference.row y 0) ≤ 2 + 1 / 2097152 := by + refine not_lt.mp fun hlt => ?_ + have hc := (lt_kthLargest_iff (by norm_num) + (by norm_num : (0 : ℝ) ≤ 2 + 1 / 2097152)).mp hlt + have hs : ({y | (2 + 1 / 2097152 : ℝ) < reference.row y 0} : Finset (Fin 2)) = {0} := by + ext y + rw [reference_eq] + fin_cases y <;> norm_num + rw [hs] at hc + norm_num at hc + have hge : (2 + 1 / 2097152 : ℝ) ≤ kthLargest 2 univ (fun y => reference.row y 0) := by + apply (le_kthLargest_iff (by norm_num) (by norm_num : (0 : ℝ) < 2 + 1 / 2097152)).mpr + have hs : ({y | (2 + 1 / 2097152 : ℝ) ≤ reference.row y 0} : Finset (Fin 2)) = univ := by + ext y + rw [reference_eq] + fin_cases y <;> norm_num + rw [hs] + norm_num + exact le_antisymm (max_le (by rw [reference_eq]; norm_num) hle) + (hge.trans kthLargest_le_firstRank) + +private noncomputable def gatedOutput (x v r : ℝ) : ℝ := + if x ≤ 10 then 0 else if 3 ≤ r then 0 else x + v + max 1 r + +private theorem gate_flat (x v q r : ℝ) (hq : q ∈ Set.Icc 0 (1 : ℝ)) + (hr : r ∈ Set.Icc 0 (1 : ℝ)) : gatedOutput x v q = gatedOutput x v r := by + have hq' : ¬3 ≤ q := by linarith [hq.2] + have hr' : ¬3 ≤ r := by linarith [hr.2] + simp only [gatedOutput, hq', hr', ↓reduceIte, max_eq_left hq.2, max_eq_left hr.2] + +-- The actual remaining schedule preserves a nonzero output of the constructed reference. +example : + let c := stationaryContinuation univ (fun _ => 2) 2 (dyadicFloor 1 2) + increments initial truth 1 1 + gatedOutput (c.row 0 0) (c.row 0 1) (firstRank univ 2 c.defaultValue c.row) = + 22 + 1 / 2097152 := by + have h := stationaryContinuation_output_eq_dyadic (s := univ) (n := fun _ => 2) (K := 2) + (Δ := increments) (a := initial) (truth := truth) (η := 1) (H := gatedOutput) + (g := 3) (e := 10) (by norm_num) (by norm_num) 2 1 1 (by norm_num) no_overflow + (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun y _ => by fin_cases y <;> norm_num [truth]) (by intros; norm_num) + (by norm_num) (by norm_num) (fun _ _ _ hx => by simp [gatedOutput, hx]) + (fun _ _ _ hr => by simp [gatedOutput, hr]) gate_flat 0 (mem_univ 0) + refine h.trans ?_ + change gatedOutput (reference.row 0 0) (reference.row 0 1) + (firstRank univ 2 reference.defaultValue reference.row) = _ + rw [reference_rank, reference_eq] + norm_num [gatedOutput] + +private noncomputable def fourthPowerRamp (x _v _r : ℝ) : ℝ := (max 0 (x - 1)) ^ 4 + +private theorem ramp_root (x v r : ℝ) : + fourthPowerRamp x v r ^ (4⁻¹ : ℝ) = max 0 (x - 1) := by + exact Real.pow_rpow_inv_natCast (le_max_left _ _) (by norm_num : (4 : ℕ) ≠ 0) + +private theorem ramp_root_lipschitz (x v q x' v' q' : ℝ) : + |fourthPowerRamp x v q ^ (4⁻¹ : ℝ) - fourthPowerRamp x' v' q' ^ (4⁻¹ : ℝ)| ≤ + 1 * (|x - x'| + |v - v'| + |q - q'|) := by + rw [ramp_root, ramp_root] + have hm := abs_max_sub_max_le_max (0 : ℝ) (x - 1) 0 (x' - 1) + have he : (x - 1) - (x' - 1) = x - x' := by ring + simp only [sub_self, abs_zero, he, max_eq_right (abs_nonneg (x - x'))] at hm + linarith [abs_nonneg (v - v'), abs_nonneg (q - q')] + +-- The root discrepancy really is positive, rather than an equality between identical rows. +example : + |fourthPowerRamp (reference.row 1 0) (reference.row 1 1) + (firstRank univ 2 reference.defaultValue reference.row) ^ (4⁻¹ : ℝ) - + fourthPowerRamp (truth 1 0) (truth 1 1) (firstRank univ 2 0 truth) ^ (4⁻¹ : ℝ)| = + 1 / 2097152 := by + rw [ramp_root, ramp_root, reference_eq] + norm_num [truth] + +-- A constant-one raw-prefix envelope is valid, and the theorem gives a concrete finite bound. +example : + |fourthPowerRamp (reference.row 1 0) (reference.row 1 1) + (firstRank univ 2 reference.defaultValue reference.row) ^ (4⁻¹ : ℝ) - + fourthPowerRamp (truth 1 0) (truth 1 1) (firstRank univ 2 0 truth) ^ (4⁻¹ : ℝ)| ≤ + 27 / 262144 := by + have h := abs_stationaryState_root_sub_le_weighted_dyadic (s := univ) (n := fun _ => 2) + (K := 2) (Δ := increments) (a := initial) (truth := truth) (η := 1) + (H := fourthPowerRamp) (p := (4⁻¹ : ℝ)) (C := 1) (ε := fun _ => 1) + (by norm_num) (by norm_num) (by norm_num) (by norm_num [initial]) (by norm_num [initial]) + 2 1 (by norm_num) no_overflow (by intros; norm_num) + (fun _ _ _ _ _ => clippedError_le_one _ _ _) + (fun x _ _ hx => by simp [fourthPowerRamp, max_eq_left (by linarith : x - 1 ≤ 0)]) + (by intros; rfl) (fun x v q x' v' q' _ _ _ _ => ramp_root_lipschitz x v q x' v' q') + 1 (mem_univ 1) + norm_num [sum_range_succ, floor_zero] at h ⊢ + exact h + +/-! The sensitivity clipping also handles low targets without charging their prefix errors. -/ + +private noncomputable def unitCutoff (x : ℝ) : ℝ := min 1 (max 0 (x - 1)) + +private theorem cutoff_nonneg (x : ℝ) : 0 ≤ unitCutoff x := + le_min zero_le_one (le_max_left _ _) + +private theorem cutoff_le_one (x : ℝ) : unitCutoff x ≤ 1 := min_le_left _ _ + +private theorem cutoff_zero {x : ℝ} (hx : x ≤ 1) : unitCutoff x = 0 := by + simp [unitCutoff, max_eq_left (by linarith : x - 1 ≤ 0)] + +private theorem cutoff_lipschitz (x x' : ℝ) : |unitCutoff x - unitCutoff x'| ≤ |x - x'| := by + have hmax := abs_max_sub_max_le_max (0 : ℝ) (x - 1) 0 (x' - 1) + have he : (x - 1) - (x' - 1) = x - x' := by ring + simp only [sub_self, abs_zero, he, max_eq_right (abs_nonneg (x - x'))] at hmax + have hmin := abs_min_sub_min_le_max (1 : ℝ) (max 0 (x - 1)) 1 (max 0 (x' - 1)) + simp only [sub_self, abs_zero, + max_eq_right (abs_nonneg (max 0 (x - 1) - max 0 (x' - 1)))] at hmin + exact hmin.trans hmax + +private noncomputable def rankOutput (x _v r : ℝ) : ℝ := + (unitCutoff x * (1 + unitCutoff r)) ^ 4 + +private theorem rank_output_root (x v r : ℝ) : + rankOutput x v r ^ (4⁻¹ : ℝ) = unitCutoff x * (1 + unitCutoff r) := by + exact Real.pow_rpow_inv_natCast + (mul_nonneg (cutoff_nonneg x) (add_nonneg zero_le_one (cutoff_nonneg r))) + (by norm_num : (4 : ℕ) ≠ 0) + +private theorem rank_output_lipschitz (x v q x' v' q' : ℝ) : + |rankOutput x v q ^ (4⁻¹ : ℝ) - rankOutput x' v' q' ^ (4⁻¹ : ℝ)| ≤ + 2 * (|x - x'| + |v - v'| + |q - q'|) := by + rw [rank_output_root, rank_output_root] + have hp : 0 ≤ 1 + unitCutoff q' := add_nonneg zero_le_one (cutoff_nonneg q') + have he : unitCutoff x * (1 + unitCutoff q) - unitCutoff x' * (1 + unitCutoff q') = + unitCutoff x * (unitCutoff q - unitCutoff q') + + (unitCutoff x - unitCutoff x') * (1 + unitCutoff q') := by ring + calc + _ ≤ |unitCutoff x * (unitCutoff q - unitCutoff q')| + + |(unitCutoff x - unitCutoff x') * (1 + unitCutoff q')| := by + rw [he] + exact abs_add_le _ _ + _ = unitCutoff x * |unitCutoff q - unitCutoff q'| + + |unitCutoff x - unitCutoff x'| * (1 + unitCutoff q') := by + rw [abs_mul, abs_mul, abs_of_nonneg (cutoff_nonneg x), abs_of_nonneg hp] + _ ≤ 1 * |q - q'| + |x - x'| * 2 := add_le_add + (mul_le_mul (cutoff_le_one x) (cutoff_lipschitz q q') (abs_nonneg _) zero_le_one) + (mul_le_mul (cutoff_lipschitz x x') (by linarith [cutoff_le_one q']) hp (abs_nonneg _)) + _ ≤ 2 * (|x - x'| + |v - v'| + |q - q'|) := by + linarith [abs_nonneg (q - q'), abs_nonneg (v - v')] + +-- This output is rank-flat on [0,1], but it really depends on ranks above that interval. +example : rankOutput 20 0 0 = 1 ∧ rankOutput 20 0 2 = 16 := by + norm_num [rankOutput, unitCutoff] + +private noncomputable def lowReference : State (Fin 2) := + stationaryState univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) + increments initial initial.row 1 + +private theorem low_reference_eq : lowReference = + { defaultValue := 1 / 1048576, row := rawRow } := by + unfold lowReference stationaryState + rw [actual_one, raw_one] + congr 1 + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [initial, rawRow] + +private theorem low_reference_rank : firstRank univ 2 lowReference.defaultValue lowReference.row = + 1 / 1048576 := by + rw [low_reference_eq] + exact max_eq_left raw_rank_le + +private theorem true_rank_zero : firstRank univ 2 0 initial.row = 0 := by + norm_num [firstRank, kthLargest, initial, Fin.univ_succ, filter_insert, filter_singleton] + +-- The low true target receives nonzero preloss and raises the padded rank within [0,eta]. +example : lowReference.row 1 0 - initial.row 1 0 = 1 / 2097152 ∧ + firstRank univ 2 0 initial.row = 0 ∧ + 0 < firstRank univ 2 lowReference.defaultValue lowReference.row ∧ + firstRank univ 2 lowReference.defaultValue lowReference.row ≤ 1 := by + rw [low_reference_rank, true_rank_zero, low_reference_eq] + norm_num [initial, rawRow] + +-- Zero prefix error at every sensitive target suffices despite nonzero error at the low target. +-- The rank-dependent fourth root at the high endpoint remains exactly one. +example : rankOutput (lowReference.row 0 0) (lowReference.row 0 1) + (firstRank univ 2 lowReference.defaultValue lowReference.row) ^ (4⁻¹ : ℝ) = 1 := by + have herr : ∀ i < 1, ∀ y ∈ (univ : Finset (Fin 2)), (1 : ℝ) / 2 ≤ initial.row y 0 → + clippedError (initial.row y 0) (initial.row y 1) + (uncompressedRow increments initial.row (i + 1) y) ≤ 0 := by + intro i hi y _ hd + have hi0 : i = 0 := by omega + subst i + rw [raw_one] + fin_cases y + · norm_num [clippedError, initial, rawRow] + · norm_num [initial] at hd + have h := abs_stationaryState_root_sub_le_weighted_dyadic (s := univ) (n := fun _ => 2) + (K := 2) (Δ := increments) (a := initial) (truth := initial.row) (η := 1) + (H := rankOutput) (p := (4⁻¹ : ℝ)) (C := 2) (ε := fun _ => 0) + (by norm_num) (by norm_num) (by norm_num) (by norm_num [initial]) (by norm_num [initial]) + 2 1 (by norm_num) no_overflow (by intros; norm_num) herr + (fun x _ _ hx => by simp [rankOutput, cutoff_zero hx]) + (fun _ _ _ _ hq hr => by simp only [rankOutput, cutoff_zero hq.2, cutoff_zero hr.2]) + (fun x v q x' v' q' _ _ _ _ => rank_output_lipschitz x v q x' v' q') 0 (mem_univ 0) + have heq : rankOutput (lowReference.row 0 0) (lowReference.row 0 1) + (firstRank univ 2 lowReference.defaultValue lowReference.row) ^ (4⁻¹ : ℝ) = + rankOutput (initial.row 0 0) (initial.row 0 1) + (firstRank univ 2 0 initial.row) ^ (4⁻¹ : ℝ) := by + simp only [mul_zero, sum_const_zero] at h + apply sub_eq_zero.mp + exact abs_eq_zero.mp (le_antisymm h (abs_nonneg _)) + rw [heq, rank_output_root, true_rank_zero] + norm_num [initial, unitCutoff] + +end ComplexityTests.RowCompressionStationary From 0cbb2f1bcf5bc00008e98352973a9f10462209a2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:47:13 +0000 Subject: [PATCH 7/7] feat(logspace): charge false overflows to actual prefix errors Prove uniqueness of the first-overflow index, a signed light-target error lower bound, the explicit 2^(p+1)/(n*rho^p) moment charge, and its specialization to the actual dyadic iterate with previous default and preloss bounds derived. Conditional heavy-count rarity, relative post-overflow stability and integrated compression remain open under #1721 and #1444. Strict isolated Lean compilation with warningAsError=true and empty diagnostics passed for the module and a signed two-group run with nonzero preloss. Focused hygiene and whitespace checks passed. AI-assisted implementation; independent review pending before publication. Independent non-author source/API review by lean_environment approved exact source revision e0066c8a1015c2270c0a9ffaec1a3209225b2ce3 against pinned compression.tex Section 8.4, with no findings. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 1 + .../RowCompression/FalseOverflow.lean | 198 ++++++++++++++++++ .../RowCompressionFalseOverflow.lean | 113 ++++++++++ 3 files changed, 312 insertions(+) create mode 100644 Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean create mode 100644 ComplexityTests/RowCompressionFalseOverflow.lean diff --git a/Complexity.lean b/Complexity.lean index ee0aafd7a..a11b5860a 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2352,6 +2352,7 @@ 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.RowCompression.FalseOverflow public import Complexity.Foundations.Analysis.RowCompression.Floors public import Complexity.Foundations.Analysis.RowCompression.Iteration public import Complexity.Foundations.Analysis.RowCompression.Preloss diff --git a/Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean b/Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean new file mode 100644 index 000000000..35d292f0d --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/FalseOverflow.lean @@ -0,0 +1,198 @@ +/- +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.Preloss +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Charging a first overflow to errors at light targets + +At the first group whose compression threshold exceeds its floor, sufficiently many real entries +exceed that floor: the preceding default is too small to cause the overflow. If fewer than half +as many true endpoints are heavy, at least half the overflowing entries are light. At each light +endpoint, a large input and small preceding compression loss force a large raw-prefix error. + +This module proves the deterministic counting and charging assertion of +[OpenAI2026LogSpace, Section 8.4, (8.12)]. For a floor `0 < ρ ≤ 1`, a true first coordinate in +`[0, ρ / 4]`, a zero true second coordinate, and preloss at most `ρ / 100`, an input of size +greater than `ρ` has clipped error at least `ρ / 2`. Thus a false-type overflow satisfies +`1 ≤ 2 ^ (p + 1) / (n * ρ ^ p) * ∑ y, error y ^ p`, for every natural moment exponent `p`. + +The final theorem applies this to the actual iterated compression with the explicit dyadic +floors and zero initial default. It derives the previous-default and preloss bounds from the +absence of earlier overflow. The error is taken from the uncompressed prefix at `j + 1`, not +from the compressed row. The first-overflow index is also proved unique. + +This is the pointwise false-overflow charge. Conditional rarity of true heavy counts, stability +after overflow, and the integrated compression theorem remain separate obligations. + +## Main results + +* `Cslib.RowCompression.IsFirstOverflow.unique`: first-overflow events are disjoint. +* `Cslib.RowCompression.half_floor_le_clippedError`: a large light entry forces raw-prefix error. +* `Cslib.RowCompression.one_le_sum_clippedError_pow_of_overflow`: the explicit moment charge. +* `Cslib.RowCompression.one_le_sum_clippedError_pow_of_firstOverflow_dyadic`: the charge for the + actual compression recursion, with numerical floor conditions discharged. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.4, equation labelled `buf-false-charge` + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} + +/-- Group `j` is the first whose actual threshold exceeds its prescribed floor. -/ +@[expose] def IsFirstOverflow (s : Finset ι) (n K : ℕ → ℕ) (ρ : ℕ → ℝ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (j : ℕ) : Prop := + (∀ i < j, stepThreshold s n K ρ Δ a i ≤ ρ i) ∧ ρ j < stepThreshold s n K ρ Δ a j + +/-- A run cannot have two different first-overflow groups. -/ +theorem IsFirstOverflow.unique {s : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {j k : ℕ} + (hj : IsFirstOverflow s n K ρ Δ a j) (hk : IsFirstOverflow s n K ρ Δ a k) : j = k := by + rcases lt_trichotomy j k with h | h | h + · exact False.elim (not_lt_of_ge (hk.1 j h) hj.2) + · exact h + · exact False.elim (not_lt_of_ge (hj.1 k h) hk.2) + +/-- A light true target cannot produce a large compression input without a large raw error. +Both input channels may have either sign. -/ +theorem half_floor_le_clippedError {ρ d v : ℝ} {w raw : Fin 2 → ℝ} + (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) (hd : 0 ≤ d) (hdρ : d ≤ ρ / 4) (hv : v = 0) + (hprev : ∀ ν, |w ν - raw ν| ≤ ρ / 100) (hsize : ρ < entrySize w) : + ρ / 2 ≤ clippedError d v raw := by + have hsmall : ρ / 2 ≤ 1 := by linarith + rcases lt_max_iff.mp hsize with hfirst | hsecond + · have hraw : |w 0| ≤ ρ / 100 + (|raw 0 - d| + d) := by + calc + _ ≤ |w 0 - raw 0| + |raw 0| := by + simpa only [sub_zero] using abs_sub_le (w 0) (raw 0) 0 + _ ≤ ρ / 100 + (|raw 0 - d| + d) := by + apply add_le_add (hprev 0) + simpa only [sub_zero, abs_of_nonneg hd] using abs_sub_le (raw 0) d 0 + have hden : 0 < 1 + d := by linarith + have hrel : ρ / 2 ≤ |raw 0 - d| / (1 + d) := by + apply (le_div_iff₀ hden).2 + calc + _ ≤ (ρ / 2) * (5 / 4) := mul_le_mul_of_nonneg_left (by linarith) (by positivity) + _ ≤ _ := by linarith + exact (le_min hsmall hrel).trans (le_max_left _ _) + · have hraw : |w 1| ≤ ρ / 100 + |raw 1| := by + have h : |w 1| ≤ |w 1 - raw 1| + |raw 1| := by + simpa only [sub_zero] using abs_sub_le (w 1) (raw 1) 0 + exact h.trans (add_le_add (hprev 1) le_rfl) + have hrel : ρ / 2 ≤ |raw 1 - v| := by rw [hv, sub_zero]; linarith + exact (le_min hsmall hrel).trans (le_max_right _ _) + +/-- If the old default is below the floor, an overflow needs at least `n` real large entries. -/ +theorem le_card_large_of_overflow {s : Finset ι} {n : ℕ} {ρ z : ℝ} + {w : ι → Fin 2 → ℝ} (hn : 0 < n) (hρ : 0 ≤ ρ) (hz : z ≤ ρ) + (hover : ρ < threshold s n ρ z w) : + n ≤ #{y ∈ s | ρ < entrySize (w y)} := by + apply (lt_kthLargest_iff hn hρ).mp + unfold threshold at hover + rcases lt_max_iff.mp hover with h | h + · exact False.elim (not_lt_of_ge hz h) + · simpa only [lt_max_iff, lt_self_iff_false, false_or] using h + +/-- The moment sum pays for an overflow unless at least half its capacity is truly heavy. +The constant is explicit, and the bound allows arbitrary dependence between entries. -/ +theorem one_le_sum_clippedError_pow_of_overflow {s : Finset ι} {n : ℕ} {ρ z : ℝ} + {w raw truth : ι → Fin 2 → ℝ} (hn : 0 < n) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) + (hz : z ≤ ρ) (hover : ρ < threshold s n ρ z w) + (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) + (hsecond : ∀ y ∈ s, truth y 0 ≤ ρ / 4 → truth y 1 = 0) + (hprev : ∀ y ∈ s, ∀ ν, |w y ν - raw y ν| ≤ ρ / 100) + (hheavy : 2 * #{y ∈ s | ρ / 4 < truth y 0} < n) (p : ℕ) : + 1 ≤ (2 : ℝ) ^ (p + 1) / ((n : ℝ) * ρ ^ p) * + ∑ y ∈ s, clippedError (truth y 0) (truth y 1) (raw y) ^ p := by + classical + let large := {y ∈ s | ρ < entrySize (w y)} + let heavy := {y ∈ s | ρ / 4 < truth y 0} + let light := {y ∈ large | truth y 0 ≤ ρ / 4} + have hnlarge : n ≤ #large := le_card_large_of_overflow hn hρ.le hz hover + have hcover : large ⊆ light ∪ heavy := by + intro y hy + by_cases hd : truth y 0 ≤ ρ / 4 + · exact mem_union_left _ (mem_filter.mpr ⟨hy, hd⟩) + · exact mem_union_right _ (mem_filter.mpr ⟨(mem_filter.mp hy).1, lt_of_not_ge hd⟩) + have hcount : n ≤ 2 * #light := by + have hcard := (card_le_card hcover).trans (card_union_le light heavy) + change 2 * #heavy < n at hheavy + omega + have hhalf : (n : ℝ) / 2 ≤ #light := by + have hc : (n : ℝ) ≤ 2 * (#light : ℝ) := by exact_mod_cast hcount + linarith + have hsubset : light ⊆ s := fun _ hy => (mem_filter.mp (mem_filter.mp hy).1).1 + have hsum : (#light : ℝ) * (ρ / 2) ^ p ≤ + ∑ y ∈ s, clippedError (truth y 0) (truth y 1) (raw y) ^ p := by + calc + _ = ∑ _y ∈ light, (ρ / 2) ^ p := by simp + _ ≤ ∑ y ∈ light, clippedError (truth y 0) (truth y 1) (raw y) ^ p := by + apply sum_le_sum + intro y hy + have hys := hsubset hy + exact pow_le_pow_left₀ (by positivity) (half_floor_le_clippedError hρ hρ1 + (hfirst y hys) (mem_filter.mp hy).2 (hsecond y hys (mem_filter.mp hy).2) + (hprev y hys) (mem_filter.mp (mem_filter.mp hy).1).2) p + _ ≤ _ := sum_le_sum_of_subset_of_nonneg hsubset fun y _ _ => + pow_nonneg (clippedError_nonneg _ _ _) _ + have hcharge := (mul_le_mul_of_nonneg_right hhalf + (pow_nonneg (by positivity : 0 ≤ ρ / 2) p)).trans hsum + have hn' : (0 : ℝ) < n := by exact_mod_cast hn + have hden : 0 < (n : ℝ) / 2 * (ρ / 2) ^ p := by positivity + calc + 1 ≤ (∑ y ∈ s, clippedError (truth y 0) (truth y 1) (raw y) ^ p) / + ((n : ℝ) / 2 * (ρ / 2) ^ p) := (le_div_iff₀ hden).2 (by simpa using hcharge) + _ = _ := by + rw [div_pow, pow_succ] + field_simp + +/-- The false-overflow charge for the actual dyadic compression run. Earlier non-overflow and +the explicit floor separation imply all default and preloss hypotheses of the local charge. -/ +theorem one_le_sum_clippedError_pow_of_firstOverflow_dyadic {s : Finset ι} + {n K : ℕ → ℕ} {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {truth : ι → Fin 2 → ℝ} + {η : ℝ} (hη : 0 < η) (hη1 : η ≤ 1) (ha : a.defaultValue = 0) + (m j : ℕ) (hj : j < m) (hn : 0 < n j) + (hover : IsFirstOverflow s n K (dyadicFloor η m) Δ a j) + (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) + (hsecond : ∀ y ∈ s, truth y 0 ≤ dyadicFloor η m j / 4 → truth y 1 = 0) + (hheavy : 2 * #{y ∈ s | dyadicFloor η m j / 4 < truth y 0} < n j) (p : ℕ) : + 1 ≤ (2 : ℝ) ^ (p + 1) / ((n j : ℝ) * dyadicFloor η m j ^ p) * + ∑ y ∈ s, clippedError (truth y 0) (truth y 1) + (uncompressedRow Δ a.row (j + 1) y) ^ p := by + have hρ := dyadicFloor_pos hη m j + have hρ1 : dyadicFloor η m j ≤ 1 := by + have h := dyadicFloor_le_scale_div hη.le m j + linarith + have hsum := six_sum_range_dyadicFloor_le hη.le hj + have hzabs := abs_iterate_defaultValue_sub_le_of_no_overflow + (show 0 ≤ a.defaultValue by rw [ha]) j hover.1 + rw [ha, sub_zero] at hzabs + have hz : (iterate s n K (dyadicFloor η m) Δ a j).defaultValue ≤ dyadicFloor η m j := by + have h := le_abs_self (iterate s n K (dyadicFloor η m) Δ a j).defaultValue + linarith + apply one_le_sum_clippedError_pow_of_overflow hn hρ hρ1 hz hover.2 hfirst hsecond ?_ hheavy p + intro y _ ν + rw [uncompressedRow_succ] + simp only [inputRow, Pi.add_apply, add_sub_add_right_eq_sub] + exact (abs_iterate_sub_uncompressed_le_of_no_overflow j hover.1 y ν).trans hsum + +end Cslib.RowCompression diff --git a/ComplexityTests/RowCompressionFalseOverflow.lean b/ComplexityTests/RowCompressionFalseOverflow.lean new file mode 100644 index 000000000..55ef176c1 --- /dev/null +++ b/ComplexityTests/RowCompressionFalseOverflow.lean @@ -0,0 +1,113 @@ +/- +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.FalseOverflow +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Tests for charging false overflows + +An actual two-group run first compresses a zero row to a nonzero default, then receives a negative +first-channel increment at one endpoint and a positive second-channel increment at another. +The first overflow is group one. Neither true target is heavy, and the charge is verified using +the actual raw prefix, despite the nonzero preceding compression loss. +-/ + +namespace ComplexityTests.RowCompressionFalseOverflow + +open Finset Cslib.RowCompression + +-- A negative first channel can cause the light-target error just as a positive one can. +example : (1 / 2 : ℝ) ≤ clippedError (1 / 4) 0 ![-2, 0] := by + apply half_floor_le_clippedError (w := ![-2, 0]) (by norm_num) le_rfl + (by norm_num) le_rfl rfl + · intro ν + norm_num + · norm_num [entrySize] + +-- The second-channel case does not rely on the first coordinate being large. +example : (1 / 2 : ℝ) ≤ clippedError 0 0 ![0, -2] := by + apply half_floor_le_clippedError (w := ![0, -2]) (by norm_num) le_rfl + le_rfl (by norm_num) rfl + · intro ν + norm_num + · norm_num [entrySize] + +private def initial : State (Fin 2) := { defaultValue := 0, row := 0 } + +private noncomputable def increments (i : ℕ) (y : Fin 2) : Fin 2 → ℝ := + if i = 0 then 0 else if y = 0 then ![-1 / 512, 0] else ![0, 1 / 512] + +private noncomputable def run : ℕ → State (Fin 2) := + iterate univ (fun _ => 2) (fun _ => 1) (dyadicFloor 1 2) increments initial + +private theorem first_state : (run 1).defaultValue = 1 / 1048576 ∧ + (run 1).row = fun _ => defaultEntry (1 / 1048576) := by + constructor + · norm_num [run, iterate, advance, initial, increments, dyadicFloor, dyadicSlack, + newDefault, threshold, kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + · funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [run, iterate, advance, initial, increments, dyadicFloor, dyadicSlack, + newDefault, threshold, kthLargest, entrySize, update, updateEntry, radius, defaultEntry, + Fin.univ_succ, filter_insert, filter_singleton] + +private theorem first_overflow : + IsFirstOverflow univ (fun _ => 2) (fun _ => 1) (dyadicFloor 1 2) increments initial 1 := by + constructor + · intro i hi + have hi0 : i = 0 := by omega + subst i + norm_num [stepThreshold, inputRow, iterate, initial, increments, dyadicFloor, dyadicSlack, + threshold, kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + · change dyadicFloor 1 2 1 < threshold univ 2 (dyadicFloor 1 2 1) + (run 1).defaultValue ((run 1).row + increments 1) + rw [first_state.1, first_state.2] + have hlarge : ∀ y ∈ (univ : Finset (Fin 2)), dyadicFloor 1 2 1 < + entrySize (defaultEntry (1 / 1048576) + increments 1 y) := by + intro y _ + fin_cases y <;> norm_num [increments, dyadicFloor, dyadicSlack, entrySize, defaultEntry] + have hcard : 2 ≤ #{y ∈ (univ : Finset (Fin 2)) | dyadicFloor 1 2 1 < + entrySize (defaultEntry (1 / 1048576) + increments 1 y)} := by + rw [filter_eq_self.mpr hlarge] + norm_num + have hrank := (lt_kthLargest_iff (by norm_num : 0 < 2) + (dyadicFloor_nonneg (by norm_num : (0 : ℝ) ≤ 1) 2 1)).mpr hcard + exact hrank.trans_le ((le_max_right _ _).trans (le_max_right _ _)) + +-- There is genuine preloss at the previous group, so the zero-loss case is insufficient. +example : (run 1).row 0 0 - uncompressedRow increments initial.row 1 0 0 = 1 / 1048576 := by + rw [first_state.2] + norm_num [uncompressedRow, increments, initial, defaultEntry] + +-- First-overflow events are disjoint for this concrete run as well. +example (j : ℕ) + (hj : IsFirstOverflow univ (fun _ => 2) (fun _ => 1) (dyadicFloor 1 2) increments initial j) : + j = 1 := hj.unique first_overflow + +-- The actual moment theorem applies, discharging every earlier-threshold and light-target premise. +example : 1 ≤ (2 : ℝ) ^ (4 + 1) / (2 * dyadicFloor 1 2 1 ^ 4) * + ∑ y : Fin 2, clippedError 0 0 (uncompressedRow increments initial.row 2 y) ^ 4 := by + apply one_le_sum_clippedError_pow_of_firstOverflow_dyadic (truth := fun _ => 0) + (by norm_num) le_rfl rfl 2 1 (by norm_num) (by norm_num) first_overflow + · intro y _ + exact le_rfl + · intro y _ _ + rfl + · norm_num [dyadicFloor, dyadicSlack] + +-- Both endpoints contribute exactly (1/512)^4; the error is measured before compression. +example : (∑ y : Fin 2, + clippedError 0 0 (uncompressedRow increments initial.row 2 y) ^ 4) = 1 / 34359738368 := by + norm_num [uncompressedRow, increments, initial, clippedError, Fin.sum_univ_two, sum_range_succ] + +example : (2 : ℝ) ^ (4 + 1) / (2 * dyadicFloor 1 2 1 ^ 4) * + ∑ y : Fin 2, clippedError 0 0 (uncompressedRow increments initial.row 2 y) ^ 4 = 512 := by + norm_num [uncompressedRow, increments, initial, clippedError, dyadicFloor, dyadicSlack, + Fin.sum_univ_two, sum_range_succ] + +end ComplexityTests.RowCompressionFalseOverflow