From c3f7a58ac47dd83ab36e9226c2a3a9e96840fe34 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:07:57 +0000 Subject: [PATCH 1/3] 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/3] 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/3] 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