diff --git a/Complexity.lean b/Complexity.lean index 650146df25..d68c060e8c 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2464,11 +2464,13 @@ 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.GateClosure public import Complexity.Foundations.Analysis.RowCompression.Iteration public import Complexity.Foundations.Analysis.RowCompression.NoiseDecay public import Complexity.Foundations.Analysis.RowCompression.OverflowBudget public import Complexity.Foundations.Analysis.RowCompression.OverflowNoise public import Complexity.Foundations.Analysis.RowCompression.Perturbation +public import Complexity.Foundations.Analysis.RowCompression.PreloadedIteration public import Complexity.Foundations.Analysis.RowCompression.Preloss public import Complexity.Foundations.Analysis.RowCompression.Reference public import Complexity.Foundations.Analysis.RowCompression.Sentinel @@ -2900,6 +2902,9 @@ public import Complexity.Foundations.Probability.HierarchyParams public import Complexity.Foundations.Probability.PolynomialAtomCutoffs public import Complexity.Foundations.Probability.PolynomialAtomFalseOverflow public import Complexity.Foundations.Probability.PolynomialAtomRows +public import Complexity.Foundations.Probability.PolynomialAtomRows.FirstOverflow +public import Complexity.Foundations.Probability.PolynomialAtomRows.Relative +public import Complexity.Foundations.Probability.PolynomialAtomRows.RootError public import Complexity.Foundations.Probability.ProductError public import Complexity.Foundations.Probability.RootMetric public import Complexity.Foundations.Probability.RootMetric.Minkowski diff --git a/Complexity/Foundations/Analysis/RowCompression/GateClosure.lean b/Complexity/Foundations/Analysis/RowCompression/GateClosure.lean new file mode 100644 index 0000000000..c2d016e208 --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/GateClosure.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Analysis.RowCompression.Reference +import Mathlib.Tactic.Linarith + +/-! +# Persistent closure of the rank gate + +A marked collection whose actual raw first coordinates stay above `3 * G` has two possible +behaviors. As long as the default remains below `G`, every marked entry stays in the identity +region of compression and follows its raw prefix exactly. Once a threshold reaches `G`, the +new default reaches `G` and can never fall below it. With at least `K` marked retained entries, +the actual default-padded first rank is therefore at least `G` throughout the calculation. + +This is the large-heavy-set branch in [OpenAI2026LogSpace, Section 8.3, Lemma 8.3]. The raw +lower bound is an explicit hypothesis here; the concrete polynomial-row client derives it +from small clipped-prefix errors and large true first entries. Neither an upper bound on the +thresholds nor agreement of exception lists is required. + +## Main results + +* `Cslib.RowCompression.gate_le_default_or_iterate_row_eq`: either the default closes the + gate, or every marked compressed entry still equals its raw prefix. +* `Cslib.RowCompression.le_iterate_firstRank_of_raw_large`: enough such entries force the + actual padded rank above the gate threshold. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, proof of Lemma 8.3, the branch with at least `K` entries above `L₀` + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} {s D : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {G : ℝ} + +/-- A large raw entry is preserved until a threshold raises the default to the gate level. +Both channels are preserved, even when the second channel is signed. -/ +theorem gate_le_default_or_iterate_row_eq (m : ℕ) + (hraw : ∀ i ≤ m, ∀ y ∈ D, 3 * G ≤ uncompressedRow Δ a.row i y 0) : + G ≤ (iterate s n K ρ Δ a m).defaultValue ∨ + ∀ y ∈ D, (iterate s n K ρ Δ a m).row y = uncompressedRow Δ a.row m y := by + induction m with + | zero => exact Or.inr fun _ _ => (congrFun uncompressedRow_zero _).symm + | succ m ih => + by_cases hu : G ≤ stepThreshold s n K ρ Δ a m + · exact Or.inl (hu.trans threshold_le_newDefault) + · have hprevious : ∀ y ∈ D, (iterate s n K ρ Δ a m).row y = + uncompressedRow Δ a.row m y := by + rcases ih (fun i hi => hraw i (hi.trans (Nat.le_succ m))) with hz | hw + · exact False.elim (hu (hz.trans le_threshold)) + · exact hw + refine Or.inr fun y hy => ?_ + have hinput : inputRow s n K ρ Δ a m y = uncompressedRow Δ a.row (m + 1) y := by + funext ν + rw [uncompressedRow_succ] + change (iterate s n K ρ Δ a m).row y ν + Δ m y ν = _ + rw [hprevious y hy] + have hlarge : 3 * stepThreshold s n K ρ Δ a m ≤ + entrySize (inputRow s n K ρ Δ a m y) := by + have hr := hraw (m + 1) (le_refl _) y hy + have hv := (le_abs_self (inputRow s n K ρ Δ a m y 0)).trans + (abs_apply_le_entrySize (inputRow s n K ρ Δ a m y) 0) + rw [hinput] + rw [hinput] at hv + linarith [not_le.mp hu] + change update s (n m) (K m) (ρ m) (iterate s n K ρ Δ a m).defaultValue + (inputRow s n K ρ Δ a m) y = _ + rw [update_eq_self_of_three_mul_le hlarge] + exact hinput + +/-- At least `k` large raw first entries close the actual padded rank gate. The compression +capacities may vary independently; no threshold upper bound is assumed. -/ +theorem le_iterate_firstRank_of_raw_large {k : ℕ} (hG : 0 < G) (hk : 0 < k) + (hDs : D ⊆ s) (hcard : k ≤ #D) (m : ℕ) + (hraw : ∀ i ≤ m, ∀ y ∈ D, 3 * G ≤ uncompressedRow Δ a.row i y 0) : + G ≤ firstRank s k (iterate s n K ρ Δ a m).defaultValue + (iterate s n K ρ Δ a m).row := by + classical + rcases gate_le_default_or_iterate_row_eq m hraw with hz | hw + · exact hz.trans default_le_firstRank + · apply le_trans _ kthLargest_le_firstRank + apply (le_kthLargest_iff hk hG).mpr + apply hcard.trans (card_le_card ?_) + intro y hy + apply mem_filter.mpr ⟨hDs hy, ?_⟩ + rw [hw y hy] + linarith [hraw m (le_refl _) y hy] + +end Cslib.RowCompression diff --git a/Complexity/Foundations/Analysis/RowCompression/PreloadedIteration.lean b/Complexity/Foundations/Analysis/RowCompression/PreloadedIteration.lean new file mode 100644 index 0000000000..391587c6fd --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/PreloadedIteration.lean @@ -0,0 +1,168 @@ +/- +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.SentinelRelative +public import Mathlib.Order.Interval.Finset.Nat +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Algebra.Order.BigOperators.Group.Finset +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Restarting compression from an already-added group input + +At a first overflow in group `j`, the available error estimate concerns the raw input after +adding group `j`, not the preceding raw prefix. Start the local calculation from the actual +`inputRow` and use zero as its first increment. The local calculation agrees exactly with the +original calculation after every positive number of updates. + +The corresponding local error sequence repeats the overflow group's error at indices zero and +one. Its adjacent-prefix propagation budget is at most four times the usual weighted tail sum. +Only errors from group `j` onward occur in this bound. These are exact indexing and finite-sum +identities; they require no overflow event, row bounds, or probabilistic hypotheses. + +## Main definitions + +* `Cslib.RowCompression.preloadedIncrement`: the remaining increment schedule with its first + increment already added to the initial state. +* `Cslib.RowCompression.preloadedError`: the error envelope at the resulting local raw prefixes. + +## Main results + +* `Cslib.RowCompression.iterate_preloadedIncrement`: equality of the restarted and original + compressed calculations after a positive number of updates. +* `Cslib.RowCompression.uncompressedRow_preloadedIncrement`: equality of the corresponding + raw prefixes after a positive number of local increments. +* `Cslib.RowCompression.prefixErrorBudget_preloadedError_le`: the adjacent-prefix budget is + bounded by four times the original weighted tail sum. +-/ + +public section + +namespace Cslib.RowCompression + +open Finset + +variable {ι : Type*} + +/-- Restart at group `j` after its increment has already been added. The first local increment +is zero; later local increments are the actual subsequent increments. -/ +@[expose] def preloadedIncrement (Δ : ℕ → ι → Fin 2 → ℝ) (j : ℕ) : + ℕ → ι → Fin 2 → ℝ + | 0 => 0 + | i + 1 => Δ (j + i + 1) + +@[simp] +theorem preloadedIncrement_zero (Δ : ℕ → ι → Fin 2 → ℝ) (j : ℕ) : + preloadedIncrement Δ j 0 = 0 := rfl + +@[simp] +theorem preloadedIncrement_succ (Δ : ℕ → ι → Fin 2 → ℝ) (j i : ℕ) : + preloadedIncrement Δ j (i + 1) = Δ (j + i + 1) := rfl + +/-- Both local prefixes zero and one use the already-added group `j` input. Later local +prefixes use the errors of the subsequent groups. -/ +@[expose] def preloadedError (ε : ℕ → ℝ) (j : ℕ) : ℕ → ℝ + | 0 => ε j + | i + 1 => ε (j + i) + +@[simp] +theorem preloadedError_zero (ε : ℕ → ℝ) (j : ℕ) : preloadedError ε j 0 = ε j := rfl + +@[simp] +theorem preloadedError_succ (ε : ℕ → ℝ) (j i : ℕ) : + preloadedError ε j (i + 1) = ε (j + i) := rfl + +/-- A restart from the already-added input gives exactly the original compressed state after +any positive number of updates. Group `j` is compressed once, with no duplicated increment. -/ +theorem iterate_preloadedIncrement {s : Finset ι} {n K : ℕ → ℕ} {ρ : ℕ → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} (j : ℕ) {r : ℕ} (hr : 0 < r) : + iterate s (fun i => n (j + i)) (fun i => K (j + i)) (fun i => ρ (j + i)) + (preloadedIncrement Δ j) + ⟨(iterate s n K ρ Δ a j).defaultValue, inputRow s n K ρ Δ a j⟩ r = + iterate s n K ρ Δ a (j + r) := by + cases r with + | zero => omega + | succ r => + clear hr + induction r with + | zero => + simp [iterate_succ, advance, inputRow] + | succ r ih => + rw [iterate_succ, ih] + simp only [preloadedIncrement_succ, Nat.add_succ, iterate_succ] + +/-- Raw prefixes after the preloaded restart agree with the original raw prefixes. At local +index zero the initial row is already global raw prefix `j + 1`. -/ +theorem uncompressedRow_preloadedIncrement {Δ : ℕ → ι → Fin 2 → ℝ} + {raw₀ : ι → Fin 2 → ℝ} (j : ℕ) {r : ℕ} (hr : 0 < r) : + uncompressedRow (preloadedIncrement Δ j) (uncompressedRow Δ raw₀ (j + 1)) r = + uncompressedRow Δ raw₀ (j + r) := by + cases r with + | zero => omega + | succ r => + clear hr + induction r with + | zero => + funext y ν + simp only [uncompressedRow_succ, uncompressedRow_zero, preloadedIncrement_zero, + Pi.zero_apply, add_zero] + | succ r ih => + funext y ν + rw [uncompressedRow_succ, ih] + simp only [preloadedIncrement_succ, Nat.add_succ, uncompressedRow_succ] + +/-- The adjacent-prefix budget for a preloaded restart is at most four times the original +weighted tail budget. The estimate does not require any error bound before group `j`. -/ +theorem prefixErrorBudget_preloadedError_le {ε : ℕ → ℝ} (j : ℕ) {r : ℕ} + (hr : 0 < r) (hε : ∀ i ∈ Ico j (j + r), 0 ≤ ε i) : + prefixErrorBudget (preloadedError ε j) r ≤ + 4 * ∑ i ∈ Ico j (j + r), 28 ^ (j + r - i) * ε i := by + cases r with + | zero => omega + | succ r => + let T : ℝ := ∑ i ∈ range (r + 1), 28 ^ (r + 1 - i) * ε (j + i) + have hnonneg (i : ℕ) (hi : i < r + 1) : 0 ≤ ε (j + i) := + hε (j + i) (mem_Ico.mpr ⟨Nat.le_add_right _ _, Nat.add_lt_add_left hi _⟩) + have htail : (∑ i ∈ Ico j (j + (r + 1)), (28 : ℝ) ^ (j + (r + 1) - i) * ε i) = + T := by + rw [sum_Ico_eq_sum_range] + simp only [Nat.add_sub_cancel_left, Nat.add_sub_add_left] + rfl + have hfirst : (28 : ℝ) ^ (r + 1) * ε j ≤ T := by + have h := single_le_sum (s := range (r + 1)) + (f := fun i => (28 : ℝ) ^ (r + 1 - i) * ε (j + i)) + (fun i hi => mul_nonneg (by positivity) (hnonneg i (mem_range.mp hi))) + (mem_range.mpr (Nat.zero_lt_succ r)) + simpa only [Nat.sub_zero, Nat.add_zero] using h + have hback : + (∑ i ∈ range r, (28 : ℝ) ^ (r - i) * ε (j + i)) ≤ T := by + calc + _ ≤ ∑ i ∈ range r, (28 : ℝ) ^ (r + 1 - i) * ε (j + i) := by + refine sum_le_sum fun i hi => mul_le_mul_of_nonneg_right + (pow_le_pow_right₀ (by norm_num) (Nat.sub_le_sub_right (Nat.le_succ r) i)) ?_ + exact hnonneg i ((mem_range.mp hi).trans_le (Nat.le_succ r)) + _ ≤ T := sum_le_sum_of_subset_of_nonneg (range_mono (Nat.le_succ r)) + (fun i hi _ => mul_nonneg (by positivity) (hnonneg i (mem_range.mp hi))) + have hbefore : + (∑ i ∈ range (r + 1), (28 : ℝ) ^ (r + 1 - i) * preloadedError ε j i) ≤ 2 * T := by + rw [sum_range_succ'] + simp only [preloadedError_succ, preloadedError_zero, Nat.add_sub_add_right, Nat.sub_zero] + linarith + have hafter : + (∑ i ∈ range (r + 1), (28 : ℝ) ^ (r + 1 - i) * preloadedError ε j (i + 1)) = T := by + simp only [preloadedError_succ] + rfl + rw [htail] + unfold prefixErrorBudget + simp only [mul_add, sum_add_distrib, preloadedError_zero] + rw [hafter] + linarith + +end Cslib.RowCompression diff --git a/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean b/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean index e7d4293220..1bbb1fdc5b 100644 --- a/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean +++ b/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean @@ -39,14 +39,23 @@ Both the initial and first local prefix errors then concern the overflow group's This does not require an error estimate for the preceding global prefix. This supplies the small-heavy-set sentinel comparison in the proof of -[OpenAI2026LogSpace, Section 8.3, Lemma 8.3]. Upper saturation and the row-output comparison, -the case of at least `K` large true entries, and the full relative-stability estimate remain -separate. Sentinels are analytical devices, not objects stored by the compression algorithm. +[OpenAI2026LogSpace, Section 8.3, Lemma 8.3]. The concrete output comparison, including upper +saturation and the branch with at least `K` large true entries, is supplied by +`Complexity.Foundations.Probability.PolynomialAtomRows.Relative`. Sentinels are analytical +devices, not objects stored by the compression algorithm. + +## Main definitions + +* `Cslib.RowCompression.prefixErrorBudget`: the finite adjacent-prefix propagation budget. ## Main results * `Cslib.RowCompression.abs_sub_le_of_clippedError_le`: small clipped errors give the actual relative first-channel and absolute second-channel bounds. +* `Cslib.RowCompression.abs_increment_le_of_clippedError_le`: adjacent prefix errors bound + the actual two-channel increment. +* `Cslib.RowCompression.iterate_sentinelState_stability_of_clippedError_le`: quantitative + comparison of the two modified schedules, independent of the heavy-count branch. * `Cslib.RowCompression.iterate_sentinelState_of_clippedError_le`: actual sentinel coupling from clipped prefix budgets and a strict true-heavy-count bound. @@ -74,18 +83,41 @@ theorem abs_sub_le_of_clippedError_le {d v ε : ℝ} {w : Fin 2 → ℝ} refine ⟨?_, hsecond⟩ simpa only [mul_comm] using (div_le_iff₀ (by linarith : 0 < 1 + d)).mp hfirst -private def budget (ε : ℕ → ℝ) (m : ℕ) : ℝ := +/-- Adjacent small clipped-prefix errors control the actual increment in both channels. -/ +theorem abs_increment_le_of_clippedError_le {ι : Type*} {Δ : ℕ → ι → Fin 2 → ℝ} + {raw₀ : ι → Fin 2 → ℝ} {truth : Fin 2 → ℝ} {ε ε' : ℝ} {i : ℕ} {y : ι} + (hd : 0 ≤ truth 0) (hε : ε < 1) (hε' : ε' < 1) + (hbefore : clippedError (truth 0) (truth 1) (uncompressedRow Δ raw₀ i y) ≤ ε) + (hafter : clippedError (truth 0) (truth 1) (uncompressedRow Δ raw₀ (i + 1) y) ≤ ε') : + |Δ i y 0| ≤ (1 + truth 0) * (ε + ε') ∧ |Δ i y 1| ≤ ε + ε' := by + have hb := abs_sub_le_of_clippedError_le hd hε hbefore + have ha := abs_sub_le_of_clippedError_le hd hε' hafter + have heq (ν : Fin 2) : Δ i y ν = + (uncompressedRow Δ raw₀ (i + 1) y ν - truth ν) - + (uncompressedRow Δ raw₀ i y ν - truth ν) := by + rw [uncompressedRow_succ] + ring + constructor + · rw [heq 0] + exact (abs_sub _ _).trans (by linarith [hb.1, ha.1]) + · rw [heq 1] + exact (abs_sub _ _).trans (by linarith [hb.2, ha.2]) + +/-- The finite `28`-weighted error budget for an initial raw prefix and subsequent prefixes. -/ +@[expose] def prefixErrorBudget (ε : ℕ → ℝ) (m : ℕ) : ℝ := 28 ^ m * ε 0 + ∑ i ∈ range m, 28 ^ (m - i) * (ε i + ε (i + 1)) -private theorem budget_nonneg {ε : ℕ → ℝ} {m : ℕ} (hε : ∀ i ≤ m, 0 ≤ ε i) : - 0 ≤ budget ε m := by +/-- A nonnegative prefix envelope gives a nonnegative propagation budget. -/ +theorem prefixErrorBudget_nonneg {ε : ℕ → ℝ} {m : ℕ} (hε : ∀ i ≤ m, 0 ≤ ε i) : + 0 ≤ prefixErrorBudget ε m := by apply add_nonneg (mul_nonneg (by positivity) (hε 0 (Nat.zero_le m))) refine sum_nonneg fun i hi => mul_nonneg (by positivity) (add_nonneg ?_ ?_) · exact hε i (mem_range.mp hi).le · exact hε (i + 1) (mem_range.mp hi) -private theorem budget_mono {ε : ℕ → ℝ} {j m : ℕ} - (hε : ∀ i ≤ m, 0 ≤ ε i) (hj : j ≤ m) : budget ε j ≤ budget ε m := by +/-- Extending a nonnegative prefix envelope can only increase its propagated budget. -/ +theorem prefixErrorBudget_mono {ε : ℕ → ℝ} {j m : ℕ} + (hε : ∀ i ≤ m, 0 ≤ ε i) (hj : j ≤ m) : prefixErrorBudget ε j ≤ prefixErrorBudget ε m := by apply add_le_add · exact mul_le_mul_of_nonneg_right (pow_le_pow_right₀ (by norm_num) hj) (hε 0 (Nat.zero_le m)) @@ -99,18 +131,20 @@ private theorem budget_mono {ε : ℕ → ℝ} {j m : ℕ} mul_nonneg (by positivity) (add_nonneg (hε i (mem_range.mp hi).le) (hε (i + 1) (mem_range.mp hi))) -private theorem sum_errors_le_budget {ε : ℕ → ℝ} {m : ℕ} +/-- The propagation budget controls initial error plus total adjacent-prefix variation. -/ +theorem sum_add_le_prefixErrorBudget {ε : ℕ → ℝ} {m : ℕ} (hε : ∀ i ≤ m, 0 ≤ ε i) : - ε 0 + ∑ i ∈ range m, (ε i + ε (i + 1)) ≤ budget ε m := by + ε 0 + ∑ i ∈ range m, (ε i + ε (i + 1)) ≤ prefixErrorBudget ε m := by apply add_le_add · exact le_mul_of_one_le_left (hε 0 (Nat.zero_le m)) (one_le_pow₀ (by norm_num)) · exact sum_le_sum fun i hi => le_mul_of_one_le_left (add_nonneg (hε i (mem_range.mp hi).le) (hε (i + 1) (mem_range.mp hi))) (one_le_pow₀ (by norm_num)) -private theorem error_le_budget {ε : ℕ → ℝ} {m i : ℕ} - (hε : ∀ i ≤ m, 0 ≤ ε i) (hi : i ≤ m) : ε i ≤ budget ε m := by - have hsum := sum_errors_le_budget hε +/-- Every individual prefix error is bounded by the propagated budget. -/ +theorem le_prefixErrorBudget {ε : ℕ → ℝ} {m i : ℕ} + (hε : ∀ i ≤ m, 0 ≤ ε i) (hi : i ≤ m) : ε i ≤ prefixErrorBudget ε m := by + have hsum := sum_add_le_prefixErrorBudget hε have hs0 : 0 ≤ ∑ k ∈ range m, (ε k + ε (k + 1)) := sum_nonneg fun k hk => add_nonneg (hε k (mem_range.mp hk).le) (hε (k + 1) (mem_range.mp hk)) @@ -124,11 +158,12 @@ private theorem error_le_budget {ε : ℕ → ℝ} {m i : ℕ} have h00 := hε 0 (Nat.zero_le m) linarith -private theorem input_budget_le {ε : ℕ → ℝ} {m i : ℕ} +/-- The budget before an update plus its adjacent-prefix error is controlled by the final budget. -/ +theorem prefixErrorBudget_add_le {ε : ℕ → ℝ} {m i : ℕ} (hε : ∀ k ≤ m, 0 ≤ ε k) (hi : i < m) : - budget ε i + (ε i + ε (i + 1)) ≤ budget ε m := by - apply le_trans (b := budget ε (i + 1)) _ (budget_mono hε hi) - unfold budget + prefixErrorBudget ε i + (ε i + ε (i + 1)) ≤ prefixErrorBudget ε m := by + apply le_trans (b := prefixErrorBudget ε (i + 1)) _ (prefixErrorBudget_mono hε hi) + unfold prefixErrorBudget rw [sum_range_succ] simp only [Nat.add_sub_cancel_left, pow_one] conv_rhs => rw [← add_assoc] @@ -194,40 +229,29 @@ private theorem sentinel_reference_bounds {s : Finset ι} {K : ℕ} {η L₀ z : exact (not_le.mpr hcount) (hcard.trans (card_le_card hsub)) open Classical in -/-- **Sentinel coupling from actual clipped-prefix budgets.** The threshold and variation -conditions of the removal induction follow from the true heavy-count branch and the weighted -prefix budget. `loss` is the common initial preloss; it is not a final-error hypothesis. - -Only marked first increments are cleared. Both original marked channels follow their actual -raw prefixes, and all positive-prefix padded ranks agree exactly. -/ -theorem iterate_sentinelState_of_clippedError_le {s : Finset ι} {n : ℕ → ℕ} {K : ℕ} - {ρ : ℕ → ℝ} {η L₀ z : ℝ} {truth raw₀ loss : ι → Fin 2 → ℝ} - {Δ : ℕ → ι → Fin 2 → ℝ} {ε : ℕ → ℝ} (m : ℕ) - (hη : 0 ≤ η) (hL₀ : η ≤ L₀) (hzη : z ≤ η) (hK : 0 < K) - (hKn : ∀ i < m, K ≤ n i) (hρ : ∀ i < m, ρ i ≤ η) - (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2) - (hloss : ∀ y ∈ s, ∀ ν, |loss y ν| ≤ η / 2) - (hcount : #{y ∈ s | L₀ < truth y 0} < K) - (hε : ∀ i ≤ m, 0 ≤ ε i) +/-- Quantitative comparison after a common sentinel replacement. Actual clipped prefix errors +control the modified increments, both defaults, and all retained coordinates. The reference +has the true row plus the same initial loss and zero increments. No count or threshold ceiling +is required here. -/ +theorem iterate_sentinelState_stability_of_clippedError_le {s : Finset ι} {n : ℕ → ℕ} + {K : ℕ} {ρ : ℕ → ℝ} {L z : ℝ} {truth raw₀ loss : ι → Fin 2 → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {ε : ℕ → ℝ} (m : ℕ) (hL : 0 ≤ L) (hK : 0 < K) + (hn : ∀ i < m, 0 < n i) (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) + (hε : ∀ i ≤ m, 0 ≤ ε i) (hεlt : ∀ i ≤ m, ε i < 1) (herr : ∀ i ≤ m, ∀ y ∈ s, - clippedError (truth y 0) (truth y 1) (uncompressedRow Δ raw₀ i y) ≤ ε i) - (hsmall : (1 + 16 * (L₀ + 1)) * - (28 ^ m * ε 0 + ∑ i ∈ range m, 28 ^ (m - i) * (ε i + ε (i + 1))) ≤ 1 / 8) : - let L := 16 * (L₀ + 1) - let R := 2 * L₀ + 1 + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ raw₀ i y) ≤ ε i) : let marked := {y ∈ s | L < truth y 0} let a : State ι := ⟨z, raw₀ + loss⟩ - let original := iterate s n (fun _ => K) ρ Δ a - let modified := iterate s n (fun _ => K) ρ - (fun i => sentinelFirst marked 0 (Δ i)) (sentinelState marked L a) - ∀ j ≤ m, modified j = sentinelState marked L (original j) ∧ - (∀ y ∈ marked, (original j).row y = uncompressedRow Δ a.row j y) ∧ - (0 < j → firstRank s K (original j).defaultValue (original j).row = - firstRank s K (modified j).defaultValue (modified j).row ∧ - firstRank s K (modified j).defaultValue (modified j).row ≤ R) := by + let b : State ι := ⟨z, truth + loss⟩ + let Δ' := fun i => sentinelFirst marked 0 (Δ i) + let A := iterate s n (fun _ => K) ρ Δ' (sentinelState marked L a) + let B := iterate s n (fun _ => K) ρ (fun _ => 0) (sentinelState marked L b) + (∀ i < m, ∀ y ∈ s, ∀ ν, |Δ' i y ν| ≤ (1 + L) * (ε i + ε (i + 1))) ∧ + ∀ j ≤ m, |(A j).defaultValue - (B j).defaultValue| ≤ + (1 + L) * prefixErrorBudget ε j ∧ + ∀ y ∈ s, ∀ ν, |(A j).row y ν - (B j).row y ν| ≤ + (1 + L) * prefixErrorBudget ε j := by classical - let L := 16 * (L₀ + 1) - let R := 2 * L₀ + 1 let c := 1 + L let marked := {y ∈ s | L < truth y 0} let a : State ι := ⟨z, raw₀ + loss⟩ @@ -237,37 +261,17 @@ theorem iterate_sentinelState_of_clippedError_le {s : Finset ι} {n : ℕ → let Δ' := fun i => sentinelFirst marked 0 (Δ i) let A := iterate s n (fun _ => K) ρ Δ' a' let B := iterate s n (fun _ => K) ρ (fun _ => 0) b' - have hL₀0 : 0 ≤ L₀ := hη.trans hL₀ - have hc1 : 1 ≤ c := by dsimp only [c, L]; linarith + have hc1 : 1 ≤ c := le_add_of_nonneg_right hL have hc0 : 0 ≤ c := (by norm_num : (0 : ℝ) ≤ 1).trans hc1 - have hR : 0 ≤ R := by dsimp only [R]; positivity - have hL : 3 * R < L := by dsimp only [R, L]; linarith - have hmarked : marked ⊆ s := filter_subset _ _ - have hsmall' : c * budget ε m ≤ 1 / 8 := hsmall - have hE : budget ε m ≤ 1 / 8 := - (le_mul_of_one_le_left (budget_nonneg hε) hc1).trans hsmall' - have hεlt (i : ℕ) (hi : i ≤ m) : ε i < 1 := by - have h := (error_le_budget hε hi).trans hE - linarith have hraw (i : ℕ) (hi : i ≤ m) (y : ι) (hy : y ∈ s) : |uncompressedRow Δ raw₀ i y 0 - truth y 0| ≤ (1 + truth y 0) * ε i ∧ |uncompressedRow Δ raw₀ i y 1 - truth y 1| ≤ ε i := abs_sub_le_of_clippedError_le (hfirst y hy) (hεlt i hi) (herr i hi y hy) have hincr (i : ℕ) (hi : i < m) (y : ι) (hy : y ∈ s) : |Δ i y 0| ≤ (1 + truth y 0) * (ε i + ε (i + 1)) ∧ - |Δ i y 1| ≤ ε i + ε (i + 1) := by - have hbefore := hraw i hi.le y hy - have hafter := hraw (i + 1) hi y hy - have heq (ν : Fin 2) : Δ i y ν = - (uncompressedRow Δ raw₀ (i + 1) y ν - truth y ν) - - (uncompressedRow Δ raw₀ i y ν - truth y ν) := by - rw [uncompressedRow_succ] - ring - constructor - · rw [heq 0] - exact (abs_sub _ _).trans (by linarith [hbefore.1, hafter.1]) - · rw [heq 1] - exact (abs_sub _ _).trans (by linarith [hbefore.2, hafter.2]) + |Δ i y 1| ≤ ε i + ε (i + 1) := + abs_increment_le_of_clippedError_le (truth := truth y) (hfirst y hy) + (hεlt i hi.le) (hεlt (i + 1) hi) (herr i hi.le y hy) (herr (i + 1) hi y hy) have hoff (y : ι) (hy : y ∈ s) (hm : y ∉ marked) : truth y 0 ≤ L := by exact not_lt.mp fun h => hm (mem_filter.mpr ⟨hy, h⟩) have hinit (y : ι) (hy : y ∈ s) (ν : Fin 2) : |a'.row y ν - b'.row y ν| ≤ c * ε 0 := by @@ -305,24 +309,21 @@ theorem iterate_sentinelState_of_clippedError_le {s : Finset ι} {n : ℕ → · change |sentinelFirst marked 0 (Δ i) y 1| ≤ _ rw [sentinelFirst_one] exact (hincr i hi y hy).2.trans (le_mul_of_one_le_left hsum0 hc1) - have hreference := sentinel_reference_bounds hη hL₀ hK hzη hfirst hsecond hloss hcount - change (∀ y ∈ s, -η ≤ b'.row y 0) ∧ (∀ y ∈ s, |b'.row y 1| ≤ η) ∧ - firstRank s K b'.defaultValue b'.row ≤ 2 * L₀ at hreference have hstates (i : ℕ) (hi : i ≤ m) : - |(A i).defaultValue - (B i).defaultValue| ≤ c * budget ε i ∧ - ∀ y ∈ s, ∀ ν, |(A i).row y ν - (B i).row y ν| ≤ c * budget ε i := by + |(A i).defaultValue - (B i).defaultValue| ≤ c * prefixErrorBudget ε i ∧ + ∀ y ∈ s, ∀ ν, |(A i).row y ν - (B i).row y ν| ≤ c * prefixErrorBudget ε i := by have hz' : |a'.defaultValue - b'.defaultValue| ≤ c * ε 0 := by change |z - z| ≤ _ simpa only [sub_self, abs_zero] using mul_nonneg hc0 (hε 0 (Nat.zero_le m)) have hs := iterate_stability_of_increment_error (ρ := ρ) (mul_nonneg hc0 (hε 0 (Nat.zero_le m))) hz' hinit i - (fun k hk => hK.trans_le (hKn k (hk.trans_le hi))) (fun _ _ => hK) + (fun k hk => hn k (hk.trans_le hi)) (fun _ _ => hK) (fun k hk => mul_nonneg hc0 (add_nonneg (hε k (hk.le.trans hi)) (hε (k + 1) (hk.trans_le hi)))) (fun k hk => hΔ' k (hk.trans_le hi)) have heq : (28 : ℝ) ^ i * (c * ε 0) + - ∑ k ∈ range i, 28 ^ (i - k) * (c * (ε k + ε (k + 1))) = c * budget ε i := by - simp only [budget, mul_add, mul_sum] + ∑ k ∈ range i, 28 ^ (i - k) * (c * (ε k + ε (k + 1))) = c * prefixErrorBudget ε i := by + simp only [prefixErrorBudget, mul_add, mul_sum] congr 1 · ring · apply sum_congr rfl @@ -330,28 +331,103 @@ theorem iterate_sentinelState_of_clippedError_le {s : Finset ι} {n : ℕ → ring rw [heq] at hs exact hs + exact ⟨fun i hi y hy ν => by simpa only [Pi.zero_apply, sub_zero] using hΔ' i hi y hy ν, + hstates⟩ + +open Classical in +/-- **Sentinel coupling from actual clipped-prefix budgets.** The threshold and variation +conditions of the removal induction follow from the true heavy-count branch and the weighted +prefix budget. `loss` is the common initial preloss; it is not a final-error hypothesis. + +Only marked first increments are cleared. Both original marked channels follow their actual +raw prefixes, and all positive-prefix padded ranks agree exactly. -/ +theorem iterate_sentinelState_of_clippedError_le {s : Finset ι} {n : ℕ → ℕ} {K : ℕ} + {ρ : ℕ → ℝ} {η L₀ z : ℝ} {truth raw₀ loss : ι → Fin 2 → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {ε : ℕ → ℝ} (m : ℕ) + (hη : 0 ≤ η) (hL₀ : η ≤ L₀) (hzη : z ≤ η) (hK : 0 < K) + (hKn : ∀ i < m, K ≤ n i) (hρ : ∀ i < m, ρ i ≤ η) + (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2) + (hloss : ∀ y ∈ s, ∀ ν, |loss y ν| ≤ η / 2) + (hcount : #{y ∈ s | L₀ < truth y 0} < K) + (hε : ∀ i ≤ m, 0 ≤ ε i) + (herr : ∀ i ≤ m, ∀ y ∈ s, + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ raw₀ i y) ≤ ε i) + (hsmall : (1 + 16 * (L₀ + 1)) * + (28 ^ m * ε 0 + ∑ i ∈ range m, 28 ^ (m - i) * (ε i + ε (i + 1))) ≤ 1 / 8) : + let L := 16 * (L₀ + 1) + let R := 2 * L₀ + 1 + let marked := {y ∈ s | L < truth y 0} + let a : State ι := ⟨z, raw₀ + loss⟩ + let original := iterate s n (fun _ => K) ρ Δ a + let modified := iterate s n (fun _ => K) ρ + (fun i => sentinelFirst marked 0 (Δ i)) (sentinelState marked L a) + ∀ j ≤ m, modified j = sentinelState marked L (original j) ∧ + (∀ y ∈ marked, (original j).row y = uncompressedRow Δ a.row j y) ∧ + (0 < j → firstRank s K (original j).defaultValue (original j).row = + firstRank s K (modified j).defaultValue (modified j).row ∧ + firstRank s K (modified j).defaultValue (modified j).row ≤ R) := by + classical + let L := 16 * (L₀ + 1) + let R := 2 * L₀ + 1 + let c := 1 + L + let marked := {y ∈ s | L < truth y 0} + let a : State ι := ⟨z, raw₀ + loss⟩ + let b : State ι := ⟨z, truth + loss⟩ + let a' := sentinelState marked L a + let b' := sentinelState marked L b + let Δ' := fun i => sentinelFirst marked 0 (Δ i) + let A := iterate s n (fun _ => K) ρ Δ' a' + let B := iterate s n (fun _ => K) ρ (fun _ => 0) b' + have hL₀0 : 0 ≤ L₀ := hη.trans hL₀ + have hc1 : 1 ≤ c := by dsimp only [c, L]; linarith + have hc0 : 0 ≤ c := (by norm_num : (0 : ℝ) ≤ 1).trans hc1 + have hR : 0 ≤ R := by dsimp only [R]; positivity + have hL : 3 * R < L := by dsimp only [R, L]; linarith + have hmarked : marked ⊆ s := filter_subset _ _ + have hsmall' : c * prefixErrorBudget ε m ≤ 1 / 8 := hsmall + have hE : prefixErrorBudget ε m ≤ 1 / 8 := + (le_mul_of_one_le_left (prefixErrorBudget_nonneg hε) hc1).trans hsmall' + have hεlt (i : ℕ) (hi : i ≤ m) : ε i < 1 := by + have h := (le_prefixErrorBudget hε hi).trans hE + linarith + have hraw (i : ℕ) (hi : i ≤ m) (y : ι) (hy : y ∈ s) : + |uncompressedRow Δ raw₀ i y 0 - truth y 0| ≤ (1 + truth y 0) * ε i ∧ + |uncompressedRow Δ raw₀ i y 1 - truth y 1| ≤ ε i := + abs_sub_le_of_clippedError_le (hfirst y hy) (hεlt i hi) (herr i hi y hy) + have hincr (i : ℕ) (hi : i < m) (y : ι) (hy : y ∈ s) : + |Δ i y 0| ≤ (1 + truth y 0) * (ε i + ε (i + 1)) ∧ + |Δ i y 1| ≤ ε i + ε (i + 1) := + abs_increment_le_of_clippedError_le (truth := truth y) (hfirst y hy) + (hεlt i hi.le) (hεlt (i + 1) hi) (herr i hi.le y hy) (herr (i + 1) hi y hy) + have hreference := sentinel_reference_bounds hη hL₀ hK hzη hfirst hsecond hloss hcount + change (∀ y ∈ s, -η ≤ b'.row y 0) ∧ (∀ y ∈ s, |b'.row y 1| ≤ η) ∧ + firstRank s K b'.defaultValue b'.row ≤ 2 * L₀ at hreference + obtain ⟨hΔbound, hstates⟩ := iterate_sentinelState_stability_of_clippedError_le + (ρ := ρ) (z := z) (loss := loss) (L := L) m (by dsimp only [L]; positivity) hK + (fun i hi => hK.trans_le (hKn i hi)) hfirst hε hεlt herr + change ∀ i ≤ m, |(A i).defaultValue - (B i).defaultValue| ≤ c * prefixErrorBudget ε i ∧ + ∀ y ∈ s, ∀ ν, |(A i).row y ν - (B i).row y ν| ≤ c * prefixErrorBudget ε i at hstates have hceil (i : ℕ) (hi : i < m) : firstRank s K (A i).defaultValue (inputRow s n (fun _ => K) ρ Δ' a' i) ≤ R ∧ stepThreshold s n (fun _ => K) ρ Δ' a' i ≤ R := by - let D := c * (budget ε i + (ε i + ε (i + 1))) + let D := c * (prefixErrorBudget ε i + (ε i + ε (i + 1))) have hD0 : 0 ≤ D := mul_nonneg hc0 (add_nonneg - (budget_nonneg fun k hk => hε k (hk.trans hi.le)) + (prefixErrorBudget_nonneg fun k hk => hε k (hk.trans hi.le)) (add_nonneg (hε i hi.le) (hε (i + 1) hi))) have hD : D ≤ 1 / 8 := - (mul_le_mul_of_nonneg_left (input_budget_le hε hi) hc0).trans hsmall' + (mul_le_mul_of_nonneg_left (prefixErrorBudget_add_le hε hi) hc0).trans hsmall' have hs := hstates i hi.le have hzD : |(A i).defaultValue - (B i).defaultValue| ≤ D := hs.1.trans (mul_le_mul_of_nonneg_left (le_add_of_nonneg_right (add_nonneg (hε i hi.le) (hε (i + 1) hi))) hc0) have hwD (y : ι) (hy : y ∈ s) (ν : Fin 2) : |inputRow s n (fun _ => K) ρ Δ' a' i y ν - (B i).row y ν| ≤ D := by - have hd := hΔ' i hi y hy ν - simp only [Pi.zero_apply, sub_zero] at hd + have hd := hΔbound i hi y hy ν change |(A i).row y ν + Δ' i y ν - (B i).row y ν| ≤ _ calc _ = |((A i).row y ν - (B i).row y ν) + Δ' i y ν| := by congr 1; ring _ ≤ |(A i).row y ν - (B i).row y ν| + |Δ' i y ν| := abs_add_le _ _ - _ ≤ c * budget ε i + c * (ε i + ε (i + 1)) := add_le_add (hs.2 y hy ν) hd + _ ≤ c * prefixErrorBudget ε i + c * (ε i + ε (i + 1)) := add_le_add (hs.2 y hy ν) hd _ = D := by dsimp only [D]; ring have hqref : firstRank s K (B i).defaultValue (B i).row ≤ 2 * L₀ := reference_iterate_firstRank_le hη (by linarith) hK hreference.1 hreference.2.1 @@ -396,7 +472,7 @@ theorem iterate_sentinelState_of_clippedError_le {s : Finset ι} {n : ℕ → exact sum_le_sum fun i hi => (hincr i (mem_range.mp hi) y hys).1 have he : (1 + truth y 0) * (ε 0 + ∑ i ∈ range m, (ε i + ε (i + 1))) ≤ (1 + truth y 0) / 8 := by - have h := mul_le_mul_of_nonneg_left ((sum_errors_le_budget hε).trans hE) + have h := mul_le_mul_of_nonneg_left ((sum_add_le_prefixErrorBudget hε).trans hE) (by linarith [hfirst y hys] : 0 ≤ 1 + truth y 0) linarith change 3 * R + ∑ i ∈ range m, |Δ i y 0| < raw₀ y 0 + loss y 0 diff --git a/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean b/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean index e49cb3ee83..f9b4ba8580 100644 --- a/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean +++ b/Complexity/Foundations/Probability/PolynomialAtomFalseOverflow.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger module -- upstream: candidate -public import Complexity.Foundations.Probability.PolynomialAtomRows +public import Complexity.Foundations.Probability.PolynomialAtomRows.RootError public import Complexity.Foundations.Probability.HeavyCount public import Complexity.Foundations.Probability.RootMetric public import Complexity.Foundations.Analysis.RowCompression.FalseOverflow @@ -33,14 +33,8 @@ This is the bounded-output integration of `buf-false-charge` in the proof of It does not supply prefix mean/noise budgets, sum their geometric costs, prove post-overflow relative stability, or assert the complete integrated compression estimate. -## Main definitions - -* `Cslib.PolynomialAtomRow.stateRootError`: the actual fourth-root output discrepancy, using - both states' padded ranks and defaults. - ## Main results -* `Cslib.PolynomialAtomRow.sum_stateRootError_pow_four_le`: a width-independent support bound. * `Cslib.PolynomialAtomRow.rowNormPow_falseFirstOverflow_le`: the normalized false-overflow output charge at a specified group. * `Cslib.PolynomialAtomRow.rowNormPow_falseFirstOverflowBefore_le`: the finite union over @@ -62,61 +56,6 @@ open scoped BigOperators variable {ι : Type*} (kind : PolynomialAtomRow) -/-- The actual fourth-root discrepancy of two row states, with their own padded ranks. -/ -@[expose] noncomputable def stateRootError (θ : ℝ) (S : Finset ι) (K : ℕ) - (a b : State ι) (y : ι) : ℝ := - kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) ^ (4⁻¹ : ℝ) - - kind.eval θ (b.row y 0) (firstRank S K b.defaultValue b.row) ^ (4⁻¹ : ℝ) - -/-- Both actual output roots lie in `[0,1]`, for every input row and default. -/ -theorem abs_stateRootError_le_one (θ : ℝ) (S : Finset ι) (K : ℕ) - (a b : State ι) (y : ι) : |kind.stateRootError θ S K a b y| ≤ 1 := by - have ha0 := Real.rpow_nonneg (kind.eval_nonneg θ (a.row y 0) - (firstRank S K a.defaultValue a.row)) (4⁻¹ : ℝ) - have hb0 := Real.rpow_nonneg (kind.eval_nonneg θ (b.row y 0) - (firstRank S K b.defaultValue b.row)) (4⁻¹ : ℝ) - have ha1 := Real.rpow_le_one (kind.eval_nonneg θ (a.row y 0) _) - (kind.eval_le_one θ (a.row y 0) (firstRank S K a.defaultValue a.row)) - (by norm_num : (0 : ℝ) ≤ 4⁻¹) - have hb1 := Real.rpow_le_one (kind.eval_nonneg θ (b.row y 0) _) - (kind.eval_le_one θ (b.row y 0) (firstRank S K b.defaultValue b.row)) - (by norm_num : (0 : ℝ) ≤ 4⁻¹) - unfold stateRootError - apply abs_sub_le_iff.mpr - constructor <;> linarith - -/-- The discrepancy is supported on the union of the two actual supports. Neither the -ambient cardinality nor a bound on the row entries occurs in its fourth-power sum. -/ -theorem sum_stateRootError_pow_four_le {θ : ℝ} (hθ : 0 < θ) (S : Finset ι) {K : ℕ} - (hK : 0 < K) (a b : State ι) : - ∑ y ∈ S, |kind.stateRootError θ S K a b y| ^ 4 ≤ 2 * (K : ℝ) := by - classical - let A := {y ∈ S | kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) ≠ 0} - let B := {y ∈ S | kind.eval θ (b.row y 0) (firstRank S K b.defaultValue b.row) ≠ 0} - let D := {y ∈ S | kind.stateRootError θ S K a b y ≠ 0} - have hsub : D ⊆ A ∪ B := by - intro y hy - obtain ⟨hyS, hy⟩ := mem_filter.mp hy - by_cases ha : kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) = 0 - · apply mem_union_right - refine mem_filter.mpr ⟨hyS, fun hb => hy ?_⟩ - simp [stateRootError, ha, hb] - · exact mem_union_left _ (mem_filter.mpr ⟨hyS, ha⟩) - have hcard : #D ≤ 2 * K := by - have hA : #A < K := kind.card_filter_eval_ne_zero_lt hθ hK - have hB : #B < K := kind.card_filter_eval_ne_zero_lt hθ hK - have h := (card_le_card hsub).trans (card_union_le A B) - omega - rw [← sum_filter_of_ne (p := fun y => kind.stateRootError θ S K a b y ≠ 0) - fun y _ h hy => h (by rw [hy, abs_zero, zero_pow (by decide)])] - calc - _ ≤ ∑ _y ∈ D, (1 : ℝ) := by - refine sum_le_sum fun y _ => ?_ - simpa using pow_le_pow_left₀ (abs_nonneg (kind.stateRootError θ S K a b y)) - (kind.abs_stateRootError_le_one θ S K a b y) 4 - _ = (#D : ℝ) := by simp - _ ≤ 2 * (K : ℝ) := by exact_mod_cast hcard - private theorem sum_stateRootError_pow_four_le_of_false {θ η : ℝ} (hθ : 0 < θ) {S : Finset ι} {n : ℕ → ℕ} {K : ℕ} (hK : 0 < K) {Δ : ℕ → ι → Fin 2 → ℝ} {a : State ι} {truth : ι → Fin 2 → ℝ} diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows/FirstOverflow.lean b/Complexity/Foundations/Probability/PolynomialAtomRows/FirstOverflow.lean new file mode 100644 index 0000000000..a8a37093d4 --- /dev/null +++ b/Complexity/Foundations/Probability/PolynomialAtomRows/FirstOverflow.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 +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.PolynomialAtomRows.Relative +public import Complexity.Foundations.Analysis.RowCompression.FalseOverflow +import Complexity.Foundations.Analysis.RowCompression.PreloadedIteration +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Polynomial row comparison after the actual first overflow + +The local relative-stability estimate is applied at the actual first overflow in group `j`. +Its initial state is the already-added input of group `j`, with a zero first local increment. +The error hypotheses therefore concern precisely the raw group inputs from `j` onward. No +error bound for the preceding global prefix is required. The local adjacent-prefix budget is +bounded by four times the `28`-weighted tail sum, without a horizon factor. + +The reference is the constructed stationary continuation: it has the true row plus the +actual pre-overflow compression loss, the actual default at group `j`, the remaining real +capacities and floors, and zero further increments. A separate corollary adds the proved +weighted preloss comparison to the true output. Its tail coefficient depends only on the +chosen row function and support scale; its preloss coefficient may also depend on the +compression scale. + +These are the relative-stability and weighted-preloss portions of +[OpenAI2026LogSpace, Section 8.3] for the concrete polynomial fourth-root family. Normalized +main atoms, the full estimator's recursive moment bound, and machine-space certificates are +separate obligations. + +## Main results + +* `Cslib.PolynomialAtomRow.exists_firstOverflow_root_bound`: actual-to-reference root error + is bounded using only the actual raw input errors at and after the first overflow. +* `Cslib.PolynomialAtomRow.exists_firstOverflow_truth_root_bound`: actual-to-truth comparison + combines that tail estimate with the weighted preloss sum. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, Lemmas 8.2--8.3, specialized to the polynomial fourth-root family + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.PolynomialAtomRow + +open Finset RowCompression + +variable (kind : PolynomialAtomRow) {θ : ℝ} + +/-- **Relative stability from the actual first overflow.** The coefficient depends only on +the concrete function and `θ`. All error hypotheses are confined to groups `j ≤ i < m`; in +particular the raw prefix before adding group `j` needs no error estimate. -/ +theorem exists_firstOverflow_root_bound (hθ : 0 < θ) : + ∃ C : ℝ, 0 ≤ C ∧ ∀ {ι : Type*} (s : Finset ι) (n : ℕ → ℕ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (truth : ι → Fin 2 → ℝ) (η : ℝ) (K : ℕ), + 0 < η → η ≤ θ / 10000 → 0 < K → a.defaultValue = 0 → + ∀ (m j : ℕ), j < m → + IsFirstOverflow s n (fun _ => K) (dyadicFloor η m) Δ a j → + (∀ y ∈ s, 0 ≤ truth y 0) → (∀ y ∈ s, |truth y 1| ≤ η / 2) → + (∀ i, j ≤ i → i < m → K ≤ n i) → + ∀ (ε : ℕ → ℝ), (∀ i, j ≤ i → i < m → 0 ≤ ε i) → + (∀ i, j ≤ i → i < m → ∀ y ∈ s, + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) ≤ ε i) → + ∀ y ∈ s, + |kind.stateRootError θ s K (iterate s n (fun _ => K) (dyadicFloor η m) Δ a m) + (stationaryContinuation s n K (dyadicFloor η m) Δ a truth j (m - j)) y| ≤ + C * ∑ i ∈ Ico j m, 28 ^ (m - i) * ε i := by + obtain ⟨C, hC, hbound⟩ := kind.exists_iterate_root_bound hθ + refine ⟨4 * C, by positivity, ?_⟩ + intro ι s n Δ a truth η K hη hmargin hK ha m j hj hover hfirst hsecond hn ε hε herr y hy + let ρ := dyadicFloor η m + let run := iterate s n (fun _ => K) ρ Δ a + let raw₀ := uncompressedRow Δ a.row (j + 1) + let loss := fun y ν => (run j).row y ν - uncompressedRow Δ a.row j y ν + let z := (run j).defaultValue + have hr : 0 < m - j := Nat.sub_pos_of_lt hj + have hjr : j + (m - j) = m := Nat.add_sub_of_le hj.le + have hz : z ≤ η := stationaryState_defaultValue_le_dyadic (truth := truth) hη.le + (by rw [ha]) (by rw [ha]; linarith) m j hj.le hover.1 + have hloss (y : ι) (_hy : y ∈ s) (ν : Fin 2) : |loss y ν| ≤ η / 2 := by + have h := abs_stationaryState_row_sub_le_dyadic (truth := truth) hη.le m j hj.le + hover.1 y ν + rw [stationaryState_row_sub] at h + change |loss y ν| ≤ η / 100 at h + linarith + have hlocalε (i : ℕ) (hi : i ≤ m - j) : 0 ≤ preloadedError ε j i := by + cases i with + | zero => exact hε j (le_refl j) hj + | succ i => exact hε (j + i) (Nat.le_add_right _ _) (by omega) + have hlocalerr (i : ℕ) (hi : i ≤ m - j) (y : ι) (hy : y ∈ s) : + clippedError (truth y 0) (truth y 1) + (uncompressedRow (preloadedIncrement Δ j) raw₀ i y) ≤ preloadedError ε j i := by + cases i with + | zero => + simpa only [uncompressedRow_zero, preloadedError_zero, raw₀] using + (herr j (le_refl j) hj y hy) + | succ i => + dsimp only [raw₀] + rw [uncompressedRow_preloadedIncrement j (Nat.succ_pos i), preloadedError_succ] + simpa only [Nat.add_assoc] using herr (j + i) (Nat.le_add_right _ _) (by omega) y hy + have hrow : raw₀ + loss = inputRow s n (fun _ => K) ρ Δ a j := by + funext y ν + dsimp only [raw₀, loss, run, inputRow, Pi.add_apply] + rw [uncompressedRow_succ] + ring + have hactual : iterate s (fun i => n (j + i)) (fun _ => K) (fun i => ρ (j + i)) + (preloadedIncrement Δ j) ⟨z, raw₀ + loss⟩ (m - j) = run m := by + rw [hrow] + simpa only [hjr] using iterate_preloadedIncrement (s := s) (n := n) (K := fun _ => K) + (ρ := ρ) (Δ := Δ) (a := a) j hr + have hlocal := hbound s (fun i => n (j + i)) (fun i => ρ (j + i)) + (preloadedIncrement Δ j) truth raw₀ loss z η K hη hmargin hz hK (m - j) hr + (fun i hi => hn (j + i) (Nat.le_add_right _ _) (by omega)) + (fun i _ => by have h := dyadicFloor_le_scale_div hη.le m (j + i); dsimp only [ρ]; linarith) + hfirst hsecond hloss (preloadedError ε j) hlocalε hlocalerr y hy + rw [hactual] at hlocal + have hbudget := prefixErrorBudget_preloadedError_le j hr + (fun i hi => hε i (mem_Ico.mp hi).1 (by have := (mem_Ico.mp hi).2; omega)) + rw [hjr] at hbudget + calc + _ ≤ C * prefixErrorBudget (preloadedError ε j) (m - j) := hlocal + _ ≤ C * (4 * ∑ i ∈ Ico j m, 28 ^ (m - i) * ε i) := + mul_le_mul_of_nonneg_left hbudget hC + _ = (4 * C) * ∑ i ∈ Ico j m, 28 ^ (m - i) * ε i := by ring + +/-- The actual compressed output is compared with the true zero-padded row by adding the +weighted preloss estimate to the relative tail estimate. The tail coefficient is fixed before +choosing the compression scale. Before overflow only true first entries at least `η / 2` +need a clipped-error bound; after overflow the retained-row envelope is used. -/ +theorem exists_firstOverflow_truth_root_bound (hθ : 0 < θ) : + ∃ Ctail : ℝ, 0 ≤ Ctail ∧ ∀ (η : ℝ), 0 < η → η ≤ θ / 10000 → + ∃ Cpre : ℝ, 0 ≤ Cpre ∧ ∀ {ι : Type*} (s : Finset ι) (n : ℕ → ℕ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (truth : ι → Fin 2 → ℝ) (K : ℕ), + 0 < K → a.defaultValue = 0 → ∀ (m j : ℕ), j < m → + IsFirstOverflow s n (fun _ => K) (dyadicFloor η m) Δ a j → + (∀ y ∈ s, 0 ≤ truth y 0) → (∀ y ∈ s, |truth y 1| ≤ η / 2) → + (∀ i, j ≤ i → i < m → K ≤ n i) → + ∀ (ε : ℕ → ℝ), (∀ i < m, 0 ≤ ε i) → + (∀ i < j, ∀ y ∈ s, η / 2 ≤ truth y 0 → + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) ≤ ε i) → + (∀ i, j ≤ i → i < m → ∀ y ∈ s, + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) ≤ ε i) → + ∀ y ∈ s, + |kind.stateRootError θ s K (iterate s n (fun _ => K) (dyadicFloor η m) Δ a m) + ⟨0, truth⟩ y| ≤ Cpre * ∑ i ∈ range j, dyadicFloor η m i * ε i + + Ctail * ∑ i ∈ Ico j m, 28 ^ (m - i) * ε i := by + obtain ⟨Ctail, hCtail, htail⟩ := kind.exists_firstOverflow_root_bound hθ + refine ⟨Ctail, hCtail, ?_⟩ + intro η hη hmargin + obtain ⟨Cpre, hCpre, hpre⟩ := kind.exists_stationaryContinuation_root_bound hθ hη hmargin + refine ⟨Cpre, hCpre, ?_⟩ + intro ι s n Δ a truth K hK ha m j hj hover hfirst hsecond hn ε hε herrpre herrtail y hy + let c := stationaryContinuation s n K (dyadicFloor η m) Δ a truth j (m - j) + have hrelative := htail s n Δ a truth η K hη hmargin hK ha m j hj hover + hfirst hsecond hn ε (fun i _ hi => hε i hi) herrtail y hy + have hreference := hpre s n Δ a truth K hK (by rw [ha]) (by rw [ha]; linarith) + m j (m - j) (by omega) hover.1 hfirst hsecond hn ε + (fun i hi => hε i (hi.trans hj)) herrpre y hy + change |kind.stateRootError θ s K c ⟨0, truth⟩ y| ≤ _ at hreference + calc + _ ≤ |kind.stateRootError θ s K (iterate s n (fun _ => K) (dyadicFloor η m) Δ a m) c y| + + |kind.stateRootError θ s K c ⟨0, truth⟩ y| := abs_sub_le _ _ _ + _ ≤ Ctail * ∑ i ∈ Ico j m, 28 ^ (m - i) * ε i + + Cpre * ∑ i ∈ range j, dyadicFloor η m i * ε i := add_le_add hrelative hreference + _ = _ := add_comm _ _ + +end Cslib.PolynomialAtomRow diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows/Relative.lean b/Complexity/Foundations/Probability/PolynomialAtomRows/Relative.lean new file mode 100644 index 0000000000..29f54fba94 --- /dev/null +++ b/Complexity/Foundations/Probability/PolynomialAtomRows/Relative.lean @@ -0,0 +1,268 @@ +/- +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.Probability.PolynomialAtomRows.RootError +public import Complexity.Foundations.Analysis.RowCompression.GateClosure +public import Complexity.Foundations.Analysis.RowCompression.SentinelRelative +import Mathlib.Algebra.Order.Group.MinMax +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Relative stability of actual polynomial row outputs + +The preparation, auxiliary score, and witness have a uniform fourth-root comparison between +the actual compression schedule and the zero-increment reference with the same initial loss. +The coefficient depends only on the chosen function and its support scale. It does not depend +on entry magnitudes, retained width, capacities, horizon, compression scale, or errors. + +The proof treats every error budget. A large budget uses the concrete output range. For a +small budget, at least `K` large true entries close both actual padded-rank gates. Otherwise, +common sentinel replacement gives quantitative state stability; upper entry saturation and +exact rank coupling transfer it back to the actual outputs. No final-error, count, threshold +ceiling, or scalar regularity assumption is passed to the public comparison theorem. + +## Main results + +* `Cslib.PolynomialAtomRow.eval_eq_of_entry_ge`: upper entry saturation for all three functions. +* `Cslib.PolynomialAtomRow.exists_iterate_root_bound`: uniform relative fourth-root stability + for the actual calculation and its stationary reference, for every error budget. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, Lemma 8.3, specialized to the concrete polynomial fourth-root family + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.PolynomialAtomRow + +open Finset RowCompression + +variable (kind : PolynomialAtomRow) {θ η : ℝ} + +/-- All three entry factors have saturated by the common sufficient bound `θ`. -/ +theorem eval_eq_of_entry_ge {v v' r : ℝ} (hθ : 0 < θ) (hv : θ ≤ v) (hv' : θ ≤ v') : + kind.eval θ v r = kind.eval θ v' r := by + cases kind + · simp only [eval, polynomialPrepRow4, + polynomialPrepCutoff4_eq_one hθ (by linarith : 3 * θ / 4 ≤ v), + polynomialPrepCutoff4_eq_one hθ (by linarith : 3 * θ / 4 ≤ v')] + · simp only [eval, polynomialAuxCutoff4, + polynomialSwitch4_of_ge (by linarith : θ / 8 < θ / 4) (by linarith : θ / 4 ≤ v), + polynomialSwitch4_of_ge (by linarith : θ / 8 < θ / 4) (by linarith : θ / 4 ≤ v')] + · simp only [eval, polynomialWitnessCutoff4, + polynomialSwitch4_of_ge (by linarith : 82 * θ / 1000 < 90 * θ / 1000) + (by linarith : 90 * θ / 1000 ≤ v), + polynomialSwitch4_of_ge (by linarith : 82 * θ / 1000 < 90 * θ / 1000) + (by linarith : 90 * θ / 1000 ≤ v')] + +private theorem gateThreshold_le_scale (hθ : 0 < θ) : kind.gateThreshold θ ≤ θ := by + cases kind <;> dsimp only [gateThreshold] <;> linarith + +private theorem three_mul_scale_le_of_small_error {d e raw loss : ℝ} + (hθ : 0 < θ) (hmargin : η ≤ θ / 10000) (hd : 16 * (θ + 1) < d) + (he : e ≤ 1 / 8) (hraw : |raw - d| ≤ (1 + d) * e) (hloss : |loss| ≤ η / 2) : + 3 * θ ≤ raw + loss := by + have hd0 : 0 ≤ 1 + d := by linarith + have he' := mul_le_mul_of_nonneg_left he hd0 + have hr := (abs_le.mp hraw).1 + have hl := (abs_le.mp hloss).1 + nlinarith + +private theorem eval_iterate_eq_sentinel {ι : Type*} {s : Finset ι} {n : ℕ → ℕ} + {K : ℕ} {ρ : ℕ → ℝ} {z : ℝ} {truth raw₀ loss : ι → Fin 2 → ℝ} + {Δ : ℕ → ι → Fin 2 → ℝ} {ε : ℕ → ℝ} (hθ : 0 < θ) (hη : 0 ≤ η) + (hmargin : η ≤ θ / 10000) (hz : z ≤ η) (hK : 0 < K) (m : ℕ) (hm : 0 < m) + (hKn : ∀ i < m, K ≤ n i) (hρ : ∀ i < m, ρ i ≤ η) + (hfirst : ∀ y ∈ s, 0 ≤ truth y 0) (hsecond : ∀ y ∈ s, |truth y 1| ≤ η / 2) + (hloss : ∀ y ∈ s, ∀ ν, |loss y ν| ≤ η / 2) + (hcount : #{y ∈ s | 16 * (θ + 1) < truth y 0} < K) + (hε : ∀ i ≤ m, 0 ≤ ε i) + (herr : ∀ i ≤ m, ∀ y ∈ s, + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ raw₀ i y) ≤ ε i) + (hsmall : (1 + 16 * (16 * (θ + 1) + 1)) * prefixErrorBudget ε m ≤ 1 / 8) + (y : ι) (hy : y ∈ s) : + let L := 16 * (16 * (θ + 1) + 1) + let marked := {y ∈ s | L < truth y 0} + let a : State ι := ⟨z, raw₀ + loss⟩ + let actual := iterate s n (fun _ => K) ρ Δ a m + let modified := iterate s n (fun _ => K) ρ + (fun i => sentinelFirst marked 0 (Δ i)) (sentinelState marked L a) m + kind.eval θ (actual.row y 0) (firstRank s K actual.defaultValue actual.row) = + kind.eval θ (modified.row y 0) (firstRank s K modified.defaultValue modified.row) := by + classical + let L := 16 * (16 * (θ + 1) + 1) + let marked := {y ∈ s | L < truth y 0} + let a : State ι := ⟨z, raw₀ + loss⟩ + let actual := iterate s n (fun _ => K) ρ Δ a m + let modified := iterate s n (fun _ => K) ρ + (fun i => sentinelFirst marked 0 (Δ i)) (sentinelState marked L a) m + have hc := iterate_sentinelState_of_clippedError_le (L₀ := 16 * (θ + 1)) m hη + (by linarith) hz hK hKn hρ hfirst hsecond hloss hcount hε herr hsmall m (le_refl m) + change modified = sentinelState marked L actual ∧ + (∀ y ∈ marked, actual.row y = uncompressedRow Δ a.row m y) ∧ + (0 < m → firstRank s K actual.defaultValue actual.row = + firstRank s K modified.defaultValue modified.row ∧ + firstRank s K modified.defaultValue modified.row ≤ 2 * (16 * (θ + 1)) + 1) at hc + change kind.eval θ (actual.row y 0) (firstRank s K actual.defaultValue actual.row) = + kind.eval θ (modified.row y 0) (firstRank s K modified.defaultValue modified.row) + rw [(hc.2.2 hm).1, hc.1] + by_cases hmarked : y ∈ marked + · have hE : prefixErrorBudget ε m ≤ 1 / 8 := + (le_mul_of_one_le_left (prefixErrorBudget_nonneg hε) + (by dsimp only [L]; linarith : 1 ≤ 1 + L)).trans hsmall + have he : ε m ≤ 1 / 8 := (le_prefixErrorBudget hε (le_refl _)).trans hE + have hraw := (abs_sub_le_of_clippedError_le (hfirst y hy) (by linarith : ε m < 1) + (herr m (le_refl m) y hy)).1 + have hd : 16 * (θ + 1) < truth y 0 := by + have hd := (mem_filter.mp hmarked).2 + dsimp only [L] at hd + linarith + have hlarge := three_mul_scale_le_of_small_error hθ hmargin hd he hraw (hloss y hy 0) + have hv : θ ≤ actual.row y 0 := by + rw [hc.2.1 y hmarked] + change θ ≤ uncompressedRow Δ (raw₀ + loss) m y 0 + have heq : uncompressedRow Δ (raw₀ + loss) m y 0 = + uncompressedRow Δ raw₀ m y 0 + loss y 0 := by + simp only [uncompressedRow, Pi.add_apply] + ring + rw [heq] + linarith + change kind.eval θ (actual.row y 0) _ = + kind.eval θ (sentinelFirst marked L actual.row y 0) _ + rw [sentinelFirst_zero_of_mem hmarked] + exact kind.eval_eq_of_entry_ge hθ hv (by dsimp only [L]; linarith) + · change kind.eval θ (actual.row y 0) _ = + kind.eval θ (sentinelFirst marked L actual.row y 0) _ + rw [sentinelFirst_of_not_mem hmarked] + +/-- **Relative stability for the concrete fourth-root family.** The constant is uniform in +all calculation data, including the compression scale. The actual schedule is compared with +the zero-increment reference having the same initial loss. There is no small-error or +heavy-count premise: both count branches and every nonnegative error budget are covered. -/ +theorem exists_iterate_root_bound (hθ : 0 < θ) : + ∃ C : ℝ, 0 ≤ C ∧ ∀ {ι : Type*} (s : Finset ι) (n : ℕ → ℕ) (ρ : ℕ → ℝ) + (Δ : ℕ → ι → Fin 2 → ℝ) (truth raw₀ loss : ι → Fin 2 → ℝ) (z η : ℝ) (K : ℕ), + 0 < η → η ≤ θ / 10000 → z ≤ η → 0 < K → + ∀ (m : ℕ), 0 < m → (∀ i < m, K ≤ n i) → (∀ i < m, ρ i ≤ η) → + (∀ y ∈ s, 0 ≤ truth y 0) → (∀ y ∈ s, |truth y 1| ≤ η / 2) → + (∀ y ∈ s, ∀ ν, |loss y ν| ≤ η / 2) → + ∀ (ε : ℕ → ℝ), (∀ i ≤ m, 0 ≤ ε i) → + (∀ i ≤ m, ∀ y ∈ s, + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ raw₀ i y) ≤ ε i) → + ∀ y ∈ s, + |kind.stateRootError θ s K + (iterate s n (fun _ => K) ρ Δ ⟨z, raw₀ + loss⟩ m) + (iterate s n (fun _ => K) ρ (fun _ => 0) ⟨z, truth + loss⟩ m) y| ≤ + C * prefixErrorBudget ε m := by + classical + obtain ⟨A, hA, hroot⟩ := kind.exists_abs_eval_root_sub_le θ + let L := 16 * (16 * (θ + 1) + 1) + let c := 1 + L + have hc1 : 1 ≤ c := by dsimp only [c, L]; linarith + have hc0 : 0 ≤ c := by linarith + refine ⟨(8 + 2 * A) * c, mul_nonneg (by positivity) hc0, ?_⟩ + intro ι s n ρ Δ truth raw₀ loss z η K hη hmargin hz hK m hm hKn hρ + hfirst hsecond hloss ε hε herr y hy + let a : State ι := ⟨z, raw₀ + loss⟩ + let b : State ι := ⟨z, truth + loss⟩ + let actual := iterate s n (fun _ => K) ρ Δ a m + let reference := iterate s n (fun _ => K) ρ (fun _ => 0) b m + let E := prefixErrorBudget ε m + have hE0 : 0 ≤ E := prefixErrorBudget_nonneg hε + change |kind.stateRootError θ s K actual reference y| ≤ (8 + 2 * A) * c * E + by_cases hsmall : c * E ≤ 1 / 8 + · have hE : E ≤ 1 / 8 := (le_mul_of_one_le_left hE0 hc1).trans hsmall + have he (i : ℕ) (hi : i ≤ m) : ε i ≤ 1 / 8 := + (le_prefixErrorBudget hε hi).trans hE + have hεlt (i : ℕ) (hi : i ≤ m) : ε i < 1 := by linarith [he i hi] + by_cases hcount : #{y ∈ s | 16 * (θ + 1) < truth y 0} < K + · let marked := {y ∈ s | L < truth y 0} + let modified := iterate s n (fun _ => K) ρ + (fun i => sentinelFirst marked 0 (Δ i)) (sentinelState marked L a) m + let modifiedReference := iterate s n (fun _ => K) ρ + (fun _ => 0) (sentinelState marked L b) m + have ha := kind.eval_iterate_eq_sentinel hθ hη.le hmargin hz hK m hm hKn hρ + hfirst hsecond hloss hcount hε herr hsmall y hy + change kind.eval θ (actual.row y 0) (firstRank s K actual.defaultValue actual.row) = + kind.eval θ (modified.row y 0) (firstRank s K modified.defaultValue modified.row) at ha + have hb := kind.eval_iterate_eq_sentinel (Δ := fun _ => 0) (raw₀ := truth) + (ε := fun _ => 0) hθ hη.le hmargin hz hK m hm hKn hρ + hfirst hsecond hloss hcount (by intros; norm_num) + (by intros; simp [uncompressedRow, clippedError]) + (by simp [prefixErrorBudget]) y hy + have hzero (D : Finset ι) : sentinelFirst D 0 (0 : ι → Fin 2 → ℝ) = 0 := by + funext y ν + simp [sentinelFirst] + dsimp only at hb + rw [hzero] at hb + change kind.eval θ (reference.row y 0) (firstRank s K reference.defaultValue reference.row) = + kind.eval θ (modifiedReference.row y 0) + (firstRank s K modifiedReference.defaultValue modifiedReference.row) at hb + have hs := (iterate_sentinelState_stability_of_clippedError_le + (ρ := ρ) (L := L) (z := z) (loss := loss) m + (by dsimp only [L]; linarith) hK (fun i hi => hK.trans_le (hKn i hi)) + hfirst hε hεlt herr).2 m (le_refl m) + change |modified.defaultValue - modifiedReference.defaultValue| ≤ c * E ∧ + ∀ y ∈ s, ∀ ν, |modified.row y ν - modifiedReference.row y ν| ≤ c * E at hs + have hq : |firstRank s K modified.defaultValue modified.row - + firstRank s K modifiedReference.defaultValue modifiedReference.row| ≤ c * E := + (abs_max_sub_max_le_max _ _ _ _).trans (max_le hs.1 + (abs_kthLargest_sub_kthLargest_le hK (mul_nonneg hc0 hE0) + (fun y hy => hs.2 y hy 0))) + unfold stateRootError + rw [ha, hb] + calc + _ ≤ A * (|modified.row y 0 - modifiedReference.row y 0| + + |firstRank s K modified.defaultValue modified.row - + firstRank s K modifiedReference.defaultValue modifiedReference.row|) := hroot _ _ _ _ + _ ≤ A * (c * E + c * E) := mul_le_mul_of_nonneg_left + (add_le_add (hs.2 y hy 0) hq) hA + _ ≤ (8 + 2 * A) * c * E := by nlinarith [mul_nonneg hc0 hE0] + · let D := {y ∈ s | 16 * (θ + 1) < truth y 0} + have hDs : D ⊆ s := filter_subset _ _ + have hcard : K ≤ #D := not_lt.mp hcount + have hraw (i : ℕ) (hi : i ≤ m) (y : ι) (hy : y ∈ D) : + 3 * θ ≤ uncompressedRow Δ a.row i y 0 := by + have hys := hDs hy + have hd := (mem_filter.mp hy).2 + have hr := (abs_sub_le_of_clippedError_le (hfirst y hys) (hεlt i hi) + (herr i hi y hys)).1 + have hlarge := three_mul_scale_le_of_small_error hθ hmargin hd (he i hi) hr + (hloss y hys 0) + change 3 * θ ≤ uncompressedRow Δ (raw₀ + loss) i y 0 + simpa only [uncompressedRow, Pi.add_apply, add_assoc, add_comm, add_left_comm] using hlarge + have hreference (i : ℕ) (_hi : i ≤ m) (y : ι) (hy : y ∈ D) : + 3 * θ ≤ uncompressedRow (fun _ => 0) b.row i y 0 := by + have hd := (mem_filter.mp hy).2 + have hl := (abs_le.mp (hloss y (hDs hy) 0)).1 + simp only [uncompressedRow, Pi.zero_apply, sum_const_zero, add_zero] + change 3 * θ ≤ truth y 0 + loss y 0 + linarith + have hqa := le_iterate_firstRank_of_raw_large (s := s) (n := n) + (K := fun _ => K) (ρ := ρ) hθ hK hDs hcard m hraw + have hqb := le_iterate_firstRank_of_raw_large (s := s) (n := n) + (K := fun _ => K) (ρ := ρ) hθ hK hDs hcard m hreference + have ha := kind.eval_eq_zero_of_rank_ge (v := actual.row y 0) hθ + ((kind.gateThreshold_le_scale hθ).trans hqa) + have hb := kind.eval_eq_zero_of_rank_ge (v := reference.row y 0) hθ + ((kind.gateThreshold_le_scale hθ).trans hqb) + unfold stateRootError + rw [ha, hb, sub_self, abs_zero] + positivity + · apply (kind.abs_stateRootError_le_one θ s K actual reference y).trans + have hlarge := not_le.mp hsmall + have hpositive := mul_nonneg hA (mul_nonneg hc0 hE0) + nlinarith + +end Cslib.PolynomialAtomRow diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows/RootError.lean b/Complexity/Foundations/Probability/PolynomialAtomRows/RootError.lean new file mode 100644 index 0000000000..2322099240 --- /dev/null +++ b/Complexity/Foundations/Probability/PolynomialAtomRows/RootError.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 +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.PolynomialAtomRows +import Mathlib.Tactic.Linarith + +/-! +# Fourth-root errors of concrete polynomial row outputs + +The shared discrepancy compares the actual polynomial outputs of two row states, using each +state's own default-padded rank. Each entry's root error has magnitude at most one. The sum of +its fourth powers over retained endpoints is at most `2 * K`, independently of the row width +and all entry magnitudes. These are the range and support facts used in the false-overflow +charge and the relative-stability comparison in [OpenAI2026LogSpace, Sections 8.3--8.4]. + +## Main definitions + +* `Cslib.PolynomialAtomRow.stateRootError`: the actual fourth-root output discrepancy. + +## Main results + +* `Cslib.PolynomialAtomRow.abs_stateRootError_le_one`: the pointwise range bound. +* `Cslib.PolynomialAtomRow.sum_stateRootError_pow_four_le`: the width-independent support bound. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 8.3--8.4, bounded-output comparisons for row functions + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.PolynomialAtomRow + +open Finset RowCompression +open scoped BigOperators + +variable {ι : Type*} (kind : PolynomialAtomRow) + +/-- The actual fourth-root discrepancy of two row states, with their own padded ranks. -/ +@[expose] noncomputable def stateRootError (θ : ℝ) (S : Finset ι) (K : ℕ) + (a b : State ι) (y : ι) : ℝ := + kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) ^ (4⁻¹ : ℝ) - + kind.eval θ (b.row y 0) (firstRank S K b.defaultValue b.row) ^ (4⁻¹ : ℝ) + +/-- Both actual output roots lie in `[0,1]`, for every input row and default. -/ +theorem abs_stateRootError_le_one (θ : ℝ) (S : Finset ι) (K : ℕ) + (a b : State ι) (y : ι) : |kind.stateRootError θ S K a b y| ≤ 1 := by + have ha0 := Real.rpow_nonneg (kind.eval_nonneg θ (a.row y 0) + (firstRank S K a.defaultValue a.row)) (4⁻¹ : ℝ) + have hb0 := Real.rpow_nonneg (kind.eval_nonneg θ (b.row y 0) + (firstRank S K b.defaultValue b.row)) (4⁻¹ : ℝ) + have ha1 := Real.rpow_le_one (kind.eval_nonneg θ (a.row y 0) _) + (kind.eval_le_one θ (a.row y 0) (firstRank S K a.defaultValue a.row)) + (by norm_num : (0 : ℝ) ≤ 4⁻¹) + have hb1 := Real.rpow_le_one (kind.eval_nonneg θ (b.row y 0) _) + (kind.eval_le_one θ (b.row y 0) (firstRank S K b.defaultValue b.row)) + (by norm_num : (0 : ℝ) ≤ 4⁻¹) + unfold stateRootError + apply abs_sub_le_iff.mpr + constructor <;> linarith + +/-- The discrepancy is supported on the union of the two actual supports. Neither the +ambient cardinality nor a bound on the row entries occurs in its fourth-power sum. -/ +theorem sum_stateRootError_pow_four_le {θ : ℝ} (hθ : 0 < θ) (S : Finset ι) {K : ℕ} + (hK : 0 < K) (a b : State ι) : + ∑ y ∈ S, |kind.stateRootError θ S K a b y| ^ 4 ≤ 2 * (K : ℝ) := by + classical + let A := {y ∈ S | kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) ≠ 0} + let B := {y ∈ S | kind.eval θ (b.row y 0) (firstRank S K b.defaultValue b.row) ≠ 0} + let D := {y ∈ S | kind.stateRootError θ S K a b y ≠ 0} + have hsub : D ⊆ A ∪ B := by + intro y hy + obtain ⟨hyS, hy⟩ := mem_filter.mp hy + by_cases ha : kind.eval θ (a.row y 0) (firstRank S K a.defaultValue a.row) = 0 + · apply mem_union_right + refine mem_filter.mpr ⟨hyS, fun hb => hy ?_⟩ + simp [stateRootError, ha, hb] + · exact mem_union_left _ (mem_filter.mpr ⟨hyS, ha⟩) + have hcard : #D ≤ 2 * K := by + have hA : #A < K := kind.card_filter_eval_ne_zero_lt hθ hK + have hB : #B < K := kind.card_filter_eval_ne_zero_lt hθ hK + have h := (card_le_card hsub).trans (card_union_le A B) + omega + rw [← sum_filter_of_ne (p := fun y => kind.stateRootError θ S K a b y ≠ 0) + fun y _ h hy => h (by rw [hy, abs_zero, zero_pow (by decide)])] + calc + _ ≤ ∑ _y ∈ D, (1 : ℝ) := by + refine sum_le_sum fun y _ => ?_ + simpa using pow_le_pow_left₀ (abs_nonneg (kind.stateRootError θ S K a b y)) + (kind.abs_stateRootError_le_one θ S K a b y) 4 + _ = (#D : ℝ) := by simp + _ ≤ 2 * (K : ℝ) := by exact_mod_cast hcard + +end Cslib.PolynomialAtomRow diff --git a/ComplexityTests/PolynomialAtomRelative.lean b/ComplexityTests/PolynomialAtomRelative.lean new file mode 100644 index 0000000000..98c8b02c0b --- /dev/null +++ b/ComplexityTests/PolynomialAtomRelative.lean @@ -0,0 +1,375 @@ +/- +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.Probability.PolynomialAtomRows.FirstOverflow +import Complexity.Foundations.Analysis.RowCompression.PreloadedIteration +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Actual polynomial relative-stability regressions + +The small-count example has one true entry above the sentinel, a second entry perturbed across +the preparation support boundary, and a low entry with a negative second channel. An actual +first overflow raises the default and erases that signed channel. Its polynomial root output +error is strictly positive, yet every post-addition raw error is at most `10⁻⁷`. The preceding +global prefix has large error, so the tail-only indexing of the theorem is essential. + +The same calculation also exercises an error envelope above one. Further examples distinguish +gate closure by a large retained rank from persistent closure after the default becomes large. +-/ + +namespace ComplexityTests.PolynomialAtomRelative + +open Finset Cslib Cslib.RowCompression + +private noncomputable def truth : Fin 3 → Fin 2 → ℝ := ![![1000, 0], ![1 / 2, 0], ![0, 0]] + +private noncomputable def raw : Fin 3 → Fin 2 → ℝ := + ![![1000, -1 / 40000000], ![1 / 2 + 1 / 100000000, 0], + ![1 / 10000000, -1 / 20000000]] + +private def initial : State (Fin 3) := ⟨0, 0⟩ + +private noncomputable def increments (i : ℕ) : Fin 3 → Fin 2 → ℝ := + if i = 0 then raw else 0 + +private noncomputable def actual : State (Fin 3) := + iterate univ (fun _ => 3) (fun _ => 3) (dyadicFloor (1 / 20000) 1) increments initial 1 + +private noncomputable def reference : State (Fin 3) := + stationaryContinuation univ (fun _ => 3) 3 (dyadicFloor (1 / 20000) 1) + increments initial truth 0 1 + +private theorem rank_three {v : Fin 3 → ℝ} {u : ℝ} (hu : 0 ≤ u) + (h0 : u < v 0) (h1 : u < v 1) (h2 : v 2 = u) : kthLargest 3 univ v = u := by + apply le_antisymm + · refine not_lt.mp fun hlt => ?_ + have hc := (lt_kthLargest_iff (by norm_num) hu).mp hlt + have hs : ({y | u < v y} : Finset (Fin 3)) = {0, 1} := by + ext y + fin_cases y + · simp [h0] + · simp [h1] + · simp [h2] + rw [hs] at hc + norm_num at hc + · rcases eq_or_lt_of_le hu with rfl | hu + · exact kthLargest_nonneg + · apply (le_kthLargest_iff (by norm_num) hu).mpr + have hs : ({y | u ≤ v y} : Finset (Fin 3)) = univ := by + ext y + fin_cases y + · simp [h0.le] + · simp [h1.le] + · simp [h2] + rw [hs] + norm_num + +private theorem floor_zero : dyadicFloor (1 / 20000) 1 0 = 1 / 20480000 := by + norm_num [dyadicFloor, dyadicSlack] + +private theorem raw_threshold : + threshold univ 3 (1 / 20480000) 0 raw = 1 / 10000000 := by + unfold threshold + rw [rank_three (v := fun y => entrySize (raw y)) (u := 1 / 10000000) + (by norm_num) (by norm_num [raw, entrySize]) (by norm_num [raw, entrySize]) + (by norm_num [raw, entrySize])] + norm_num + +private theorem raw_default : + newDefault univ 3 3 (1 / 20480000) 0 raw = 1 / 10000000 := by + unfold newDefault + rw [raw_threshold, rank_three (v := fun y => raw y 0) (u := 1 / 10000000) + (by norm_num) (by norm_num [raw]) (by norm_num [raw]) (by norm_num [raw])] + norm_num + +private theorem actual_state : actual = + ⟨1 / 10000000, ![![1000, -1 / 40000000], ![1 / 2 + 1 / 100000000, 0], + ![1 / 10000000, 0]]⟩ := by + change advance univ 3 3 (dyadicFloor (1 / 20000) 1 0) (increments 0) initial = _ + simp only [advance, increments, initial, ↓reduceIte, zero_add, floor_zero] + rw [raw_default] + congr 1 + unfold update + rw [raw_threshold, raw_default] + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [raw, updateEntry, radius, entrySize, defaultEntry] + +private theorem truth_rank : kthLargest 3 univ (fun y => truth y 0) = 0 := + rank_three (by norm_num) (by norm_num [truth]) (by norm_num [truth]) (by norm_num [truth]) + +private theorem truth_threshold : threshold univ 3 (1 / 20480000) 0 truth = 1 / 20480000 := by + have hs : (fun y => entrySize (truth y)) = fun y => truth y 0 := by + funext y + fin_cases y <;> norm_num [truth, entrySize] + norm_num [threshold, hs, truth_rank] + +private theorem truth_default : newDefault univ 3 3 (1 / 20480000) 0 truth = 1 / 20480000 := by + norm_num [newDefault, truth_threshold, truth_rank] + +private theorem reference_state : reference = + ⟨1 / 20480000, ![![1000, 0], ![1 / 2, 0], ![1 / 20480000, 0]]⟩ := by + have hs : stationaryState univ (fun _ => 3) (fun _ => 3) (dyadicFloor (1 / 20000) 1) + increments initial truth 0 = ⟨0, truth⟩ := by + simp [stationaryState, initial] + unfold reference stationaryContinuation + rw [hs] + change advance univ 3 3 (dyadicFloor (1 / 20000) 1 (0 + 0)) 0 ⟨0, truth⟩ = _ + simp only [advance, floor_zero, add_zero] + rw [truth_default] + congr 1 + unfold update + rw [truth_threshold, truth_default] + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [truth, updateEntry, radius, entrySize, defaultEntry] + +private theorem actual_rank : firstRank univ 3 actual.defaultValue actual.row = 1 / 10000000 := by + rw [actual_state] + unfold firstRank + rw [rank_three (u := 1 / 10000000) (by norm_num) (by norm_num) (by norm_num) (by norm_num)] + norm_num + +private theorem reference_rank : firstRank univ 3 reference.defaultValue reference.row = + 1 / 20480000 := by + rw [reference_state] + unfold firstRank + rw [rank_three (u := 1 / 20480000) (by norm_num) (by norm_num) (by norm_num) (by norm_num)] + norm_num + +private theorem first_overflow : IsFirstOverflow univ (fun _ => 3) (fun _ => 3) + (dyadicFloor (1 / 20000) 1) increments initial 0 := by + refine ⟨by simp, ?_⟩ + simp only [stepThreshold, inputRow, iterate_zero, initial, increments, ↓reduceIte, + zero_add, floor_zero, raw_threshold] + norm_num + +private theorem prefix_error (y : Fin 3) : + clippedError (truth y 0) (truth y 1) (raw y) ≤ 1 / 10000000 := by + fin_cases y <;> norm_num [truth, raw, clippedError] + +private theorem raw_one : uncompressedRow increments initial.row 1 = raw := by + funext y ν + simp [uncompressedRow, initial, increments] + +-- Compression has a real effect and the global prefix before the first input is inaccurate. +example : IsFirstOverflow univ (fun _ => 3) (fun _ => 3) (dyadicFloor (1 / 20000) 1) + increments initial 0 ∧ actual.defaultValue = 1 / 10000000 ∧ + raw 2 1 = -1 / 20000000 ∧ actual.row 2 1 = 0 ∧ + 1 / 10000000 < clippedError (truth 0 0) (truth 0 1) + (uncompressedRow increments initial.row 0 0) := by + refine ⟨first_overflow, ?_⟩ + rw [actual_state] + norm_num [raw, truth, initial, clippedError] + +-- This instance exercises the small-count, small-budget branch, including a marked large entry. +example : ({y | (528 : ℝ) < truth y 0} : Finset (Fin 3)) = {0} ∧ + #{y : Fin 3 | (32 : ℝ) < truth y 0} < 3 ∧ + 529 * prefixErrorBudget (fun _ => 1 / 10000000) 1 ≤ 1 / 8 := by + have hs : ({y | (528 : ℝ) < truth y 0} : Finset (Fin 3)) = {0} := by + ext y + fin_cases y <;> norm_num [truth] + refine ⟨hs, ?_, ?_⟩ + · have hc : ({y | (32 : ℝ) < truth y 0} : Finset (Fin 3)) = {0} := by + ext y + fin_cases y <;> norm_num [truth] + rw [hc] + norm_num + · norm_num [prefixErrorBudget] + +private theorem positive_error : + 0 < PolynomialAtomRow.preparation.stateRootError 1 univ 3 actual reference 1 := by + have ha : PolynomialAtomRow.preparation.eval 1 (actual.row 1 0) + (firstRank univ 3 actual.defaultValue actual.row) = + polynomialSwitch4 (1 / 2) (3 / 4) (1 / 2 + 1 / 100000000) := by + rw [actual_rank, actual_state] + change polynomialPrepRow4 1 (1 / 2 + 1 / 100000000) (1 / 10000000) = _ + rw [polynomialPrepRow4_of_rank_le (by norm_num) (by norm_num)] + norm_num [polynomialPrepCutoff4] + have hb : PolynomialAtomRow.preparation.eval 1 (reference.row 1 0) + (firstRank univ 3 reference.defaultValue reference.row) = 0 := by + rw [reference_state] + exact polynomialPrepRow4_eq_zero_of_entry_le (by norm_num) (by norm_num) + have hp : 0 < polynomialSwitch4 (1 / 2 : ℝ) (3 / 4) (1 / 2 + 1 / 100000000) := by + have hn : polynomialSwitch4 (1 / 2 : ℝ) (3 / 4) (1 / 2 + 1 / 100000000) ≠ 0 := by + rw [ne_eq, polynomialSwitch4_eq_zero_iff (by norm_num)] + norm_num + exact lt_of_le_of_ne (polynomialSwitch4_nonneg _ _ _) (Ne.symm hn) + unfold PolynomialAtomRow.stateRootError + rw [ha, hb, Real.zero_rpow (by norm_num : (4⁻¹ : ℝ) ≠ 0), sub_zero] + exact Real.rpow_pos_of_pos hp _ + +-- The final root error is positive and bounded by the actual post-addition raw-prefix envelope. +example : ∃ C : ℝ, 0 ≤ C ∧ + 0 < PolynomialAtomRow.preparation.stateRootError 1 univ 3 actual reference 1 ∧ + |PolynomialAtomRow.preparation.stateRootError 1 univ 3 actual reference 1| ≤ + C * (7 / 2500000) := by + obtain ⟨C, hC, hbound⟩ := PolynomialAtomRow.preparation.exists_firstOverflow_root_bound + (θ := 1) (by norm_num) + refine ⟨C, hC, positive_error, ?_⟩ + have h := hbound univ (fun _ => 3) increments initial truth (1 / 20000) 3 + (by norm_num) (by norm_num) (by norm_num) rfl 1 0 (by norm_num) first_overflow + (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun y _ => by fin_cases y <;> norm_num [truth]) (by intros; norm_num) + (fun _ => 1 / 10000000) (by intros; norm_num) + (by + intro i _ hi y _ + have hi0 : i = 0 := by omega + subst i + change clippedError (truth y 0) (truth y 1) (uncompressedRow increments initial.row 1 y) ≤ _ + rw [raw_one] + exact prefix_error y) 1 (mem_univ 1) + norm_num [sum_Ico_eq_sum_range] at h + exact h + +-- The same positive-error calculation is accepted with an envelope above one. The bound uses +-- output range in that case; the endpoint does not assume a small propagation budget. +example : (1 / 8 : ℝ) < 529 * prefixErrorBudget (fun _ => 2) 1 ∧ + ∃ C : ℝ, 0 ≤ C ∧ + |PolynomialAtomRow.preparation.stateRootError 1 univ 3 actual reference 1| ≤ C * 168 := by + constructor + · norm_num [prefixErrorBudget] + · obtain ⟨C, hC, hbound⟩ := PolynomialAtomRow.preparation.exists_iterate_root_bound + (θ := 1) (by norm_num) + refine ⟨C, hC, ?_⟩ + have h := hbound univ (fun _ => 3) (dyadicFloor (1 / 20000) 1) (fun _ => 0) + truth raw 0 0 (1 / 20000) 3 (by norm_num) (by norm_num) (by norm_num) (by norm_num) + 1 (by norm_num) (by intros; norm_num) + (by + intro i hi + have hi0 : i = 0 := by omega + subst i + rw [floor_zero] + norm_num) + (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun y _ => by fin_cases y <;> norm_num [truth]) (by intros; norm_num) + (fun _ => 2) (by intros; norm_num) + (fun _ _ _ _ => (clippedError_le_one _ _ _).trans (by norm_num)) 1 (mem_univ 1) + have hactual : iterate univ (fun _ => 3) (fun _ => 3) (dyadicFloor (1 / 20000) 1) + (fun _ => 0) ⟨0, raw⟩ 1 = actual := by + simp [actual, iterate_succ, advance, increments, initial] + have href : iterate univ (fun _ => 3) (fun _ => 3) (dyadicFloor (1 / 20000) 1) + (fun _ => 0) ⟨0, truth⟩ 1 = reference := by + simp [reference, stationaryContinuation, stationaryState, initial] + simpa only [add_zero, hactual, href, + show prefixErrorBudget (fun _ => (2 : ℝ)) 1 = 168 by norm_num [prefixErrorBudget]] using h + +private noncomputable def highTruth : Fin 2 → Fin 2 → ℝ := ![![1000, 0], ![0, 0]] + +private noncomputable def highRaw : Fin 2 → Fin 2 → ℝ := + ![![1000 + 1 / 100000000, -1 / 100000000], ![0, 0]] + +private noncomputable def highRun : ℕ → State (Fin 2) := + iterate univ (fun _ => 2) (fun _ => 1) (fun _ => 1 / 1000000000) + (fun _ => 0) ⟨0, highRaw⟩ + +private noncomputable def highReference : ℕ → State (Fin 2) := + iterate univ (fun _ => 2) (fun _ => 1) (fun _ => 1 / 1000000000) + (fun _ => 0) ⟨0, highTruth⟩ + +private theorem high_rank (m : ℕ) : + 1 ≤ firstRank univ 1 (highRun m).defaultValue (highRun m).row := by + apply le_iterate_firstRank_of_raw_large (D := {0}) (by norm_num) (by norm_num) + (subset_univ _) (by norm_num) m + intro i _ y hy + have hy0 : y = 0 := by simpa using hy + subst y + norm_num [uncompressedRow, highRaw] + +private theorem high_default : (highRun 1).defaultValue = 3 / 1000000000 := by + norm_num [highRun, iterate_succ, advance, newDefault, threshold, kthLargest, highRaw, + entrySize, Fin.univ_succ, filter_insert, filter_singleton] + +-- The ≥K branch is nonempty. Here the default is still below the gate: the retained first +-- rank closes every concrete output, while a perturbed signed high entry is preserved. +example : 1 ≤ #{y : Fin 2 | (32 : ℝ) < highTruth y 0} ∧ + (highRun 1).defaultValue < 1 ∧ (highRun 1).row 0 = highRaw 0 ∧ + ∀ (kind : PolynomialAtomRow) (y : Fin 2), + kind.eval 1 ((highRun 1).row y 0) + (firstRank univ 1 (highRun 1).defaultValue (highRun 1).row) = 0 := by + have hs : ({y | (32 : ℝ) < highTruth y 0} : Finset (Fin 2)) = {0} := by + ext y + fin_cases y <;> norm_num [highTruth] + have hd : (highRun 1).defaultValue < 1 := by rw [high_default]; norm_num + refine ⟨by rw [hs]; norm_num, hd, ?_, ?_⟩ + · have hp := gate_le_default_or_iterate_row_eq (s := (univ : Finset (Fin 2))) + (n := fun _ => 2) (K := fun _ => 1) (ρ := fun _ => 1 / 1000000000) + (Δ := fun _ => 0) (a := ⟨0, highRaw⟩) (D := {0}) (G := 1) 1 (by + intro i _ y hy + have hy0 : y = 0 := by simpa using hy + subst y + norm_num [uncompressedRow, highRaw]) + rcases hp with hz | hw + · exact False.elim (not_le.mpr hd hz) + · have h := hw 0 (by simp) + have hp : uncompressedRow (fun _ => 0) highRaw 1 = highRaw := by + funext y ν + simp [uncompressedRow] + rw [hp] at h + exact h + · intro kind y + apply kind.eval_eq_zero_of_rank_ge (by norm_num) + have hg : kind.gateThreshold (1 : ℝ) ≤ 1 := by + cases kind <;> norm_num [PolynomialAtomRow.gateThreshold] + exact hg.trans (high_rank 1) + +-- Apply the complete local endpoint in that large-count branch with a small, nonzero error. +example (kind : PolynomialAtomRow) : ∃ C : ℝ, 0 ≤ C ∧ ∀ y : Fin 2, + |kind.stateRootError 1 univ 1 (highRun 1) (highReference 1) y| ≤ C * (21 / 2500000) := by + obtain ⟨C, hC, hbound⟩ := kind.exists_iterate_root_bound (θ := 1) (by norm_num) + refine ⟨C, hC, ?_⟩ + intro y + have h := hbound univ (fun _ => 2) (fun _ => 1 / 1000000000) (fun _ => 0) + highTruth highRaw 0 0 (1 / 20000) 1 + (by norm_num) (by norm_num) (by norm_num) (by norm_num) 1 (by norm_num) + (by intros; norm_num) (by intros; norm_num) + (fun y _ => by fin_cases y <;> norm_num [highTruth]) + (fun y _ => by fin_cases y <;> norm_num [highTruth]) (by intros; norm_num) + (fun _ => 1 / 10000000) (by intros; norm_num) (by + intro i _ y _ + have hp : uncompressedRow (fun _ => 0) highRaw i = highRaw := by + funext y ν + simp [uncompressedRow] + rw [hp] + fin_cases y <;> norm_num [highTruth, highRaw, clippedError]) y (mem_univ y) + simpa only [add_zero, highRun, highReference, + show prefixErrorBudget (fun _ => (1 / 10000000 : ℝ)) 1 = 21 / 2500000 by + norm_num [prefixErrorBudget]] using h + +private noncomputable def closingInitial : State (Fin 1) := ⟨0, ![![1000, 0]]⟩ + +private noncomputable def closingIncrements (i : ℕ) : Fin 1 → Fin 2 → ℝ := + if i = 1 then ![![-10000, 0]] else 0 + +private noncomputable def closingRun : ℕ → State (Fin 1) := + iterate univ (fun _ => 1) (fun _ => 1) (fun _ => 1 / 1000000000) + closingIncrements closingInitial + +private theorem closing_default : (closingRun 1).defaultValue = 1000 := by + norm_num [closingRun, iterate_succ, advance, closingIncrements, closingInitial, newDefault, + threshold, kthLargest, entrySize, Fin.univ_succ, filter_insert, filter_singleton] + +-- Once a threshold raises the default above the gate, a later large negative raw increment +-- cannot reopen it. The raw lower-bound hypothesis itself is false at this later prefix. +example : uncompressedRow closingIncrements closingInitial.row 2 0 0 < 0 ∧ + 1000 ≤ (closingRun 2).defaultValue ∧ + ∀ (kind : PolynomialAtomRow), kind.eval 1 ((closingRun 2).row 0 0) + (firstRank univ 1 (closingRun 2).defaultValue (closingRun 2).row) = 0 := by + have hmono : (closingRun 1).defaultValue ≤ (closingRun 2).defaultValue := + iterate_defaultValue_monotone (by norm_num : 1 ≤ 2) + rw [closing_default] at hmono + refine ⟨?_, hmono, ?_⟩ + · norm_num [uncompressedRow, closingIncrements, closingInitial, sum_range_succ] + · intro kind + apply kind.eval_eq_zero_of_rank_ge (by norm_num) + have hg : kind.gateThreshold (1 : ℝ) ≤ 1000 := by + cases kind <;> norm_num [PolynomialAtomRow.gateThreshold] + exact (hg.trans hmono).trans default_le_firstRank + +end ComplexityTests.PolynomialAtomRelative diff --git a/ComplexityTests/PolynomialAtomRows.lean b/ComplexityTests/PolynomialAtomRows.lean index d60379331b..2b2fe09c9c 100644 --- a/ComplexityTests/PolynomialAtomRows.lean +++ b/ComplexityTests/PolynomialAtomRows.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Samuel Schlesinger -/ -import Complexity.Foundations.Probability.PolynomialAtomRows +import Complexity.Foundations.Probability.PolynomialAtomRows.FirstOverflow import Mathlib.LinearAlgebra.Matrix.Notation import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith @@ -17,7 +17,9 @@ A nonzero first increment incurs actual preloss `1/2097152`. Adding it to a true of `260` moves the witness rank strictly into its transition interval `(260,270)`. The true high-endpoint witness is one, while the reference witness lies strictly between zero and one. The remaining group raises the default and erases a second-coordinate value of `1/4`, yet -preserves that nonzero witness. Its fourth-root error satisfies the new weighted bound. +preserves that nonzero witness. Its fourth-root error satisfies the weighted bound. +Completing the second actual raw input to truth then gives a real first overflow at group one, +zero tail error, and a strictly positive actual-to-truth error paid entirely by weighted preloss. -/ namespace ComplexityTests.PolynomialAtomRows @@ -251,4 +253,110 @@ example (G : Matrix (Fin 2) (Fin 2) ℝ) (x y : Fin 2) : rw [Matrix.auxScore_polynomial_eq, PolynomialAtomRow.eval_firstRank_zero] simp only [div_one] +private noncomputable def completingIncrements (i : ℕ) : Fin 2 → Fin 2 → ℝ := + if i = 0 then increments 0 else if i = 1 then truth - rawRow else 0 + +private noncomputable def completedRun : ℕ → State (Fin 2) := + iterate univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) completingIncrements initial + +private theorem completing_zero : completingIncrements 0 = increments 0 := by + simp [completingIncrements] + +private theorem completed_one : completedRun 1 = + iterate univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) increments initial 1 := by + change advance univ 2 2 (dyadicFloor 1 2 0) (completingIncrements 0) initial = _ + rw [completing_zero] + rfl + +private theorem completing_raw_two : + uncompressedRow completingIncrements initial.row 2 = truth := by + funext y ν + fin_cases y <;> fin_cases ν <;> + norm_num [uncompressedRow, completingIncrements, increments, initial, truth, rawRow, + sum_range_succ] + +private theorem completing_input_one : + inputRow univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) + completingIncrements initial 1 = reference.row := by + change (completedRun 1).row + completingIncrements 1 = reference.row + rw [completed_one, actual_one, reference_eq] + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [completingIncrements, truth, rawRow] + +private theorem completed_two : completedRun 2 = continued := by + have hrow : (completedRun 1).row + completingIncrements 1 = reference.row := completing_input_one + have hdefault : (completedRun 1).defaultValue = reference.defaultValue := by + rw [completed_one, actual_one, reference_eq] + change advance univ 2 2 (dyadicFloor 1 2 1) (completingIncrements 1) (completedRun 1) = + advance univ 2 2 (dyadicFloor 1 2 1) 0 reference + unfold advance + rw [hrow, hdefault, add_zero] + +private theorem completing_first_overflow : IsFirstOverflow univ (fun _ => 2) (fun _ => 2) + (dyadicFloor 1 2) completingIncrements initial 1 := by + constructor + · intro i hi + have hi0 : i = 0 := by omega + subst i + simpa only [stepThreshold, inputRow, iterate_zero, completing_zero] using + no_overflow 0 (by norm_num) + · change dyadicFloor 1 2 1 < threshold univ 2 (dyadicFloor 1 2 1) + (completedRun 1).defaultValue + (inputRow univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) completingIncrements initial 1) + rw [completing_input_one] + have hr : dyadicFloor 1 2 1 < kthLargest 2 univ (fun y => entrySize (reference.row y)) := by + apply (lt_kthLargest_iff (by norm_num) (dyadicFloor_nonneg (by norm_num) 2 1)).mpr + have hs : ({y | dyadicFloor 1 2 1 < entrySize (reference.row y)} : + Finset (Fin 2)) = univ := by + ext y + rw [reference_eq] + fin_cases y <;> norm_num [dyadicFloor, dyadicSlack, entrySize] + rw [hs] + norm_num + exact hr.trans_le ((le_max_right _ _).trans (le_max_right _ _)) + +-- An actual first overflow with zero tail error still has a positive output error: the +-- preceding nonzero compression loss moved the witness rank into its transition interval. +example : IsFirstOverflow univ (fun _ => 2) (fun _ => 2) (dyadicFloor 1 2) + completingIncrements initial 1 ∧ + clippedError (truth 1 0) (truth 1 1) + (uncompressedRow completingIncrements initial.row 2 1) = 0 := by + rw [completing_raw_two] + exact ⟨completing_first_overflow, clippedError_self _ _ _ rfl rfl⟩ + +example : ∃ C : ℝ, 0 ≤ C ∧ + 0 < |PolynomialAtomRow.witness.stateRootError 10000 univ 2 (completedRun 2) ⟨0, truth⟩ 0| ∧ + |PolynomialAtomRow.witness.stateRootError 10000 univ 2 (completedRun 2) ⟨0, truth⟩ 0| ≤ + C / 1048576 := by + obtain ⟨Ctail, _, hscales⟩ := PolynomialAtomRow.witness.exists_firstOverflow_truth_root_bound + (θ := 10000) (by norm_num) + obtain ⟨Cpre, hCpre, hbound⟩ := hscales 1 (by norm_num) (by norm_num) + refine ⟨Cpre, hCpre, ?_, ?_⟩ + · rw [completed_two] + change 0 < |output continued ^ (4⁻¹ : ℝ) - + PolynomialAtomRow.witness.eval 10000 (truth 0 0) (firstRank univ 2 0 truth) ^ (4⁻¹ : ℝ)| + rw [preserved, true_output, Real.one_rpow] + exact abs_pos.mpr (sub_ne_zero.mpr (ne_of_lt (Real.rpow_lt_one + output_between.1.le output_between.2 (by norm_num)))) + · have h := hbound univ (fun _ => 2) completingIncrements initial truth 2 (by norm_num) rfl + 2 1 (by norm_num) completing_first_overflow + (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun y _ => by fin_cases y <;> norm_num [truth]) (by intros; norm_num) + (fun i => if i = 0 then 1 else 0) (by intro i _; split_ifs <;> norm_num) + (by + intro i hi y _ _ + have hi0 : i = 0 := by omega + subst i + simpa only [↓reduceIte] using clippedError_le_one (truth y 0) (truth y 1) + (uncompressedRow completingIncrements initial.row 1 y)) + (by + intro i hi hi' y _ + have hi1 : i = 1 := by omega + subst i + change clippedError (truth y 0) (truth y 1) + (uncompressedRow completingIncrements initial.row 2 y) ≤ 0 + rw [completing_raw_two, clippedError_self _ _ _ rfl rfl]) 0 (mem_univ 0) + norm_num [sum_range_succ, sum_Ico_eq_sum_range, floor_zero] at h + simpa only [div_eq_mul_inv, one_mul, completedRun] using h + end ComplexityTests.PolynomialAtomRows