diff --git a/Complexity.lean b/Complexity.lean index 603e806a12..fcbd744101 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2480,6 +2480,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.ClippedError public import Complexity.Foundations.Analysis.RowCompression.FalseOverflow public import Complexity.Foundations.Analysis.RowCompression.Floors public import Complexity.Foundations.Analysis.RowCompression.GateClosure @@ -2723,6 +2724,7 @@ public import Complexity.Foundations.Data.Finset.Average public import Complexity.Foundations.Data.Finset.Expect public import Complexity.Foundations.Data.Finset.Finpartition public import Complexity.Foundations.Data.Finset.KthLargest +public import Complexity.Foundations.Data.Finset.KthLargest.Truncation public import Complexity.Foundations.Data.Finset.Markov public import Complexity.Foundations.Data.Finset.OrderGlue public import Complexity.Foundations.Data.Finset.OrderedFilter @@ -2922,9 +2924,12 @@ 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.ClippedError public import Complexity.Foundations.Probability.PolynomialAtomRows.FirstOverflow +public import Complexity.Foundations.Probability.PolynomialAtomRows.NoOverflow public import Complexity.Foundations.Probability.PolynomialAtomRows.Relative public import Complexity.Foundations.Probability.PolynomialAtomRows.RootError +public import Complexity.Foundations.Probability.PolynomialAtomRows.Saturation 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/ClippedError.lean b/Complexity/Foundations/Analysis/RowCompression/ClippedError.lean new file mode 100644 index 0000000000..fce89c9059 --- /dev/null +++ b/Complexity/Foundations/Analysis/RowCompression/ClippedError.lean @@ -0,0 +1,41 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Analysis.RowCompression.Preloss +import Mathlib.Tactic.Linarith + +/-! +# Recovering coordinate bounds from small clipped errors + +Below one, the maximum of the clipped relative first-channel error and clipped absolute +second-channel error bounds both original errors. This shared fact is used by the static +polynomial comparison and by the adjacent-prefix sentinel estimates. + +## Main results + +* `Cslib.RowCompression.abs_sub_le_of_clippedError_le`: small clipped error gives the actual + relative first-coordinate and absolute second-coordinate bounds. +-/ + +public section + +namespace Cslib.RowCompression + +/-- Below one, clipping discards no information. The first target may be arbitrarily large. -/ +theorem abs_sub_le_of_clippedError_le {d v ε : ℝ} {w : Fin 2 → ℝ} + (hd : 0 ≤ d) (hε : ε < 1) (he : clippedError d v w ≤ ε) : + |w 0 - d| ≤ (1 + d) * ε ∧ |w 1 - v| ≤ ε := by + have hfirst : |w 0 - d| / (1 + d) ≤ ε := + (min_le_iff.mp ((le_max_left _ _).trans he)).resolve_left (not_le.mpr hε) + have hsecond : |w 1 - v| ≤ ε := + (min_le_iff.mp ((le_max_right _ _).trans he)).resolve_left (not_le.mpr hε) + refine ⟨?_, hsecond⟩ + simpa only [mul_comm] using (div_le_iff₀ (by linarith : 0 < 1 + d)).mp hfirst + +end Cslib.RowCompression diff --git a/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean b/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean index 1bbb1fdc5b..8e21861a90 100644 --- a/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean +++ b/Complexity/Foundations/Analysis/RowCompression/SentinelRelative.lean @@ -8,7 +8,7 @@ module -- upstream: candidate public import Complexity.Foundations.Analysis.RowCompression.Perturbation -public import Complexity.Foundations.Analysis.RowCompression.Preloss +public import Complexity.Foundations.Analysis.RowCompression.ClippedError public import Complexity.Foundations.Analysis.RowCompression.SentinelIteration import Mathlib.Algebra.BigOperators.Ring.Finset import Mathlib.Algebra.Order.BigOperators.Group.Finset @@ -50,8 +50,6 @@ devices, not objects stored by the compression algorithm. ## 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 @@ -72,17 +70,6 @@ namespace Cslib.RowCompression open Finset -/-- Below one, clipping discards no information. The first target may be arbitrarily large. -/ -theorem abs_sub_le_of_clippedError_le {d v ε : ℝ} {w : Fin 2 → ℝ} - (hd : 0 ≤ d) (hε : ε < 1) (he : clippedError d v w ≤ ε) : - |w 0 - d| ≤ (1 + d) * ε ∧ |w 1 - v| ≤ ε := by - have hfirst : |w 0 - d| / (1 + d) ≤ ε := - (min_le_iff.mp ((le_max_left _ _).trans he)).resolve_left (not_le.mpr hε) - have hsecond : |w 1 - v| ≤ ε := - (min_le_iff.mp ((le_max_right _ _).trans he)).resolve_left (not_le.mpr hε) - refine ⟨?_, hsecond⟩ - simpa only [mul_comm] using (div_le_iff₀ (by linarith : 0 < 1 + d)).mp hfirst - /-- 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 : ι} diff --git a/Complexity/Foundations/Data/Finset/KthLargest/Truncation.lean b/Complexity/Foundations/Data/Finset/KthLargest/Truncation.lean new file mode 100644 index 0000000000..7c197e2a3f --- /dev/null +++ b/Complexity/Foundations/Data/Finset/KthLargest/Truncation.lean @@ -0,0 +1,55 @@ +/- +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 + +/-! +# Upper truncation of zero-padded order statistics + +Capping every value at a nonnegative threshold caps the positive-order `k`-th largest value +at the same threshold. Nonnegativity of the cap preserves the zero padding. Input values may +be negative, and the retained cardinality may be smaller than the requested rank. + +## Main results + +* `Finset.kthLargest_min`: upper truncation commutes with the padded order statistic. +-/ + +public section + +namespace Finset + +variable {α R : Type*} [LinearOrder R] [Zero R] {s : Finset α} {k : ℕ} {f : α → R} {t : R} + +/-- An upper cap that preserves zero commutes with every positive-order padded rank. -/ +theorem kthLargest_min (hk : 0 < k) (ht : 0 ≤ t) : + kthLargest k s (fun x => min t (f x)) = min t (kthLargest k s f) := by + classical + apply le_antisymm + · refine le_min (kthLargest_le ht fun _ _ => min_le_left _ _) ?_ + refine not_lt.mp fun hlt => ?_ + have hc := (lt_kthLargest_iff hk kthLargest_nonneg).mp hlt + have hs : ({x ∈ s | kthLargest k s f < min t (f x)} : Finset α) ⊆ + {x ∈ s | kthLargest k s f < f x} := by + intro x hx + exact mem_filter.mpr ⟨(mem_filter.mp hx).1, + (mem_filter.mp hx).2.trans_le (min_le_right _ _)⟩ + exact lt_irrefl _ ((lt_kthLargest_iff hk kthLargest_nonneg).mpr + (hc.trans (card_le_card hs))) + · by_cases hzero : min t (kthLargest k s f) ≤ 0 + · exact hzero.trans kthLargest_nonneg + have hpos : 0 < min t (kthLargest k s f) := not_le.mp hzero + apply (le_kthLargest_iff hk hpos).mpr + have hc := (le_kthLargest_iff hk hpos).mp (min_le_right t (kthLargest k s f)) + apply hc.trans (card_le_card ?_) + intro x hx + exact mem_filter.mpr ⟨(mem_filter.mp hx).1, + le_min (min_le_left _ _) (mem_filter.mp hx).2⟩ + +end Finset diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows/ClippedError.lean b/Complexity/Foundations/Probability/PolynomialAtomRows/ClippedError.lean new file mode 100644 index 0000000000..52cecd6122 --- /dev/null +++ b/Complexity/Foundations/Probability/PolynomialAtomRows/ClippedError.lean @@ -0,0 +1,134 @@ +/- +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.Probability.PolynomialAtomRows.Saturation +public import Complexity.Foundations.Analysis.RowCompression.ClippedError +import Complexity.Foundations.Data.Finset.KthLargest.Truncation +import Mathlib.Algebra.Order.Group.MinMax +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity + +/-! +# Static polynomial row comparison from clipped raw error + +Compare a raw row and the true row after adding the same bounded first-coordinate loss and +using the same arbitrary default. Their actual polynomial fourth-root outputs differ by at +most a fixed coefficient times the clipped raw-error envelope. The coefficient depends only +on the concrete function and support scale, independently of the largest true entry. + +Upper entry saturation and gate closure let us cap entries and padded ranks at `θ` without +changing any output. For error at most `1/2`, entries with true first coordinate above +`4 * (θ + 1)` cap to the same value; every other capped discrepancy is at most +`(4 * θ + 5) * ε`. Capping commutes with the zero-padded order statistic, so the same bound +controls the capped rank. Larger errors are handled by the proved output range. + +This is the static final-prefix comparison used in the no-overflow bound following Lemma 8.2 +of [OpenAI2026LogSpace, Section 8.3]. No threshold bound, count branch, compression schedule, or +assumed final-output estimate occurs in this module. + +## Main results + +* `Cslib.PolynomialAtomRow.eval_eq_upperCapped`: actual output is invariant under upper caps + on its entry and rank arguments. +* `Cslib.PolynomialAtomRow.exists_commonLoss_root_bound`: actual clipped raw error controls + output-root error after a common bounded first-coordinate loss and arbitrary common default. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, the no-overflow comparison following Lemma 8.2 + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.PolynomialAtomRow + +open Finset RowCompression + +variable (kind : PolynomialAtomRow) {θ : ℝ} + +/-- Capping either scalar argument at the support scale leaves the actual output unchanged. -/ +theorem eval_eq_upperCapped (hθ : 0 < θ) (v r : ℝ) : + kind.eval θ v r = kind.eval θ (min θ v) (min θ r) := by + have hentry : kind.eval θ v r = kind.eval θ (min θ v) r := by + by_cases hv : v ≤ θ + · rw [min_eq_right hv] + · rw [min_eq_left (not_le.mp hv).le] + exact kind.eval_eq_of_entry_ge hθ (not_le.mp hv).le le_rfl + apply hentry.trans + by_cases hr : r ≤ θ + · rw [min_eq_right hr] + · rw [min_eq_left (not_le.mp hr).le] + exact (kind.eval_eq_zero_of_rank_ge hθ + ((kind.gateThreshold_le_scale hθ).trans (not_le.mp hr).le)).trans + (kind.eval_eq_zero_of_rank_ge hθ (kind.gateThreshold_le_scale hθ)).symm + +private theorem abs_min_add_sub_min_add_le {d raw loss ε : ℝ} (hθ : 0 < θ) + (hε : 0 ≤ ε) (hεsmall : ε ≤ 1 / 2) + (hraw : |raw - d| ≤ (1 + d) * ε) (hloss : |loss| ≤ θ) : + |min θ (raw + loss) - min θ (d + loss)| ≤ (4 * θ + 5) * ε := by + have hδ : 0 ≤ (4 * θ + 5) * ε := by positivity + by_cases hdlarge : d ≤ 4 * (θ + 1) + · apply (abs_min_sub_min_le_max _ _ _ _).trans + refine max_le (by simpa only [sub_self, abs_zero] using hδ) ?_ + simp only [add_sub_add_right_eq_sub] + exact hraw.trans (mul_le_mul_of_nonneg_right (by linarith) hε) + · have hproduct := mul_le_mul_of_nonneg_left hεsmall (by linarith [not_le.mp hdlarge] : 0 ≤ 1 + d) + have hrawlo := (abs_le.mp hraw).1 + have hlosslo := (abs_le.mp hloss).1 + have hcapraw : θ ≤ raw + loss := by nlinarith [not_le.mp hdlarge] + have hcaptruth : θ ≤ d + loss := by linarith [not_le.mp hdlarge] + simpa only [min_eq_left hcapraw, min_eq_left hcaptruth, sub_self, abs_zero] using hδ + +/-- A clipped raw-error envelope controls the actual polynomial root outputs after a common +loss. Only the first loss coordinate is bounded; second coordinates and the common default +are unrestricted. The final coefficient is independent of all row data and entry magnitudes. -/ +theorem exists_commonLoss_root_bound (hθ : 0 < θ) : + ∃ C : ℝ, 0 ≤ C ∧ ∀ {ι : Type*} (s : Finset ι) (K : ℕ) (z : ℝ) + (truth raw loss : ι → Fin 2 → ℝ), 0 < K → + (∀ y ∈ s, 0 ≤ truth y 0) → (∀ y ∈ s, |loss y 0| ≤ θ) → + ∀ (ε : ℝ), 0 ≤ ε → + (∀ y ∈ s, clippedError (truth y 0) (truth y 1) (raw y) ≤ ε) → + ∀ y ∈ s, + |kind.stateRootError θ s K ⟨z, raw + loss⟩ ⟨z, truth + loss⟩ y| ≤ C * ε := by + obtain ⟨A, hA, hroot⟩ := kind.exists_abs_eval_root_sub_le θ + let B := 4 * θ + 5 + have hB : 0 ≤ B := by dsimp only [B]; positivity + refine ⟨2 + 2 * A * B, by positivity, ?_⟩ + intro ι s K z truth raw loss hK hfirst hloss ε hε herr y hy + by_cases hsmall : ε ≤ 1 / 2 + · have hcap (x : ι) (hx : x ∈ s) : + |min θ ((raw + loss) x 0) - min θ ((truth + loss) x 0)| ≤ B * ε := + abs_min_add_sub_min_add_le hθ hε hsmall + (abs_sub_le_of_clippedError_le (hfirst x hx) (by linarith : ε < 1) (herr x hx)).1 + (hloss x hx) + have hq : |min θ (firstRank s K z (raw + loss)) - + min θ (firstRank s K z (truth + loss))| ≤ B * ε := by + simp only [firstRank, min_max_distrib_left] + rw [← kthLargest_min (f := fun x => (raw + loss) x 0) hK hθ.le, + ← kthLargest_min (f := fun x => (truth + loss) x 0) hK hθ.le] + exact (abs_max_sub_max_le_max _ _ _ _).trans (max_le + (by simpa only [sub_self, abs_zero] using mul_nonneg hB hε) + (abs_kthLargest_sub_kthLargest_le hK (mul_nonneg hB hε) hcap)) + unfold stateRootError + rw [kind.eval_eq_upperCapped hθ ((raw + loss) y 0) (firstRank s K z (raw + loss)), + kind.eval_eq_upperCapped hθ ((truth + loss) y 0) (firstRank s K z (truth + loss))] + calc + _ ≤ A * (|min θ ((raw + loss) y 0) - min θ ((truth + loss) y 0)| + + |min θ (firstRank s K z (raw + loss)) - + min θ (firstRank s K z (truth + loss))|) := hroot _ _ _ _ + _ ≤ A * (B * ε + B * ε) := mul_le_mul_of_nonneg_left (add_le_add (hcap y hy) hq) hA + _ ≤ (2 + 2 * A * B) * ε := by nlinarith + · apply (kind.abs_stateRootError_le_one θ s K ⟨z, raw + loss⟩ ⟨z, truth + loss⟩ y).trans + have hlarge : 1 / 2 < ε := not_le.mp hsmall + nlinarith [mul_nonneg (mul_nonneg hA hB) hε] + +end Cslib.PolynomialAtomRow diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows/NoOverflow.lean b/Complexity/Foundations/Probability/PolynomialAtomRows/NoOverflow.lean new file mode 100644 index 0000000000..175bcc1a9a --- /dev/null +++ b/Complexity/Foundations/Probability/PolynomialAtomRows/NoOverflow.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 +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Probability.PolynomialAtomRows.ClippedError +import Mathlib.Tactic.Linarith + +/-! +# Actual polynomial row errors when no overflow occurs + +For an actual dyadic compression run with no overflow, the final polynomial fourth-root error +is bounded by the weighted preloss sum plus the final raw-prefix error. The final-error +coefficient depends only on the chosen concrete row function and support scale and is fixed +before the compression scale. The preloss coefficient may also depend on that scale. + +The comparison uses the actual common preloss: the final compressed row is the final raw row +plus this loss, while the stationary reference is the true row plus the same loss and has the +same actual default. The static capped comparison bounds the first discrepancy. The proved +stationary comparison, with no remaining updates, bounds the second by weighted preloss. + +The result includes the empty schedule and imposes no capacity lower bound: there are no +reference continuation updates. All errors concern actual raw prefixes; no final-output bound, +small-error premise, count branch, or bound on the largest true entry is assumed. + +This supplies the deterministic no-overflow comparison in [OpenAI2026LogSpace, Section 8.3] +for the concrete preparation, auxiliary-score, and witness functions with fourth roots. +Integrated probabilities, normalized atoms, and the recursive estimator remain separate. + +## Main results + +* `Cslib.PolynomialAtomRow.exists_noOverflow_root_bound`: the all-horizon actual-to-truth + comparison with separate weighted-preloss and final-prefix terms. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 8.3, the no-overflow comparison following Lemma 8.2 + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib.PolynomialAtomRow + +open Finset RowCompression + +variable (kind : PolynomialAtomRow) {θ : ℝ} + +/-- **No-overflow actual-to-truth comparison.** The final-prefix coefficient is fixed before +choosing `η`. Weighted preloss needs prefix envelopes only at true first targets at least +`η / 2`; the independent final-prefix envelope covers every retained endpoint. The horizon +may be zero, and no capacity lower bound or small-error premise is needed. -/ +theorem exists_noOverflow_root_bound (hθ : 0 < θ) : + ∃ Cfinal : ℝ, 0 ≤ Cfinal ∧ ∀ (η : ℝ), 0 < η → η ≤ θ / 10000 → + ∃ Cpre : ℝ, 0 ≤ Cpre ∧ ∀ {ι : Type*} (s : Finset ι) (n : ℕ → ℕ) + (Δ : ℕ → ι → Fin 2 → ℝ) (a : State ι) (truth : ι → Fin 2 → ℝ) (K : ℕ), + 0 < K → a.defaultValue = 0 → ∀ (m : ℕ), + (∀ i < m, stepThreshold s n (fun _ => K) (dyadicFloor η m) Δ a i ≤ + dyadicFloor η m i) → + (∀ y ∈ s, 0 ≤ truth y 0) → (∀ y ∈ s, |truth y 1| ≤ η / 2) → + ∀ (ε : ℕ → ℝ), (∀ i < m, 0 ≤ ε i) → + (∀ i < m, ∀ y ∈ s, η / 2 ≤ truth y 0 → + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row (i + 1) y) ≤ ε i) → + ∀ (εfinal : ℝ), 0 ≤ εfinal → + (∀ y ∈ s, + clippedError (truth y 0) (truth y 1) (uncompressedRow Δ a.row m y) ≤ εfinal) → + ∀ y ∈ s, + |kind.stateRootError θ s K (iterate s n (fun _ => K) (dyadicFloor η m) Δ a m) + ⟨0, truth⟩ y| ≤ Cpre * ∑ i ∈ range m, dyadicFloor η m i * ε i + Cfinal * εfinal := by + obtain ⟨Cfinal, hCfinal, hfinal⟩ := kind.exists_commonLoss_root_bound hθ + refine ⟨Cfinal, hCfinal, ?_⟩ + 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 hno hfirst hsecond ε hε herr εfinal hεfinal herrfinal y hy + let actual := iterate s n (fun _ => K) (dyadicFloor η m) Δ a m + let raw := uncompressedRow Δ a.row m + let loss := fun y ν => actual.row y ν - raw y ν + let reference := stationaryState s n (fun _ => K) (dyadicFloor η m) Δ a truth m + have hloss (x : ι) (_hx : x ∈ s) : |loss x 0| ≤ θ := by + have h := abs_stationaryState_row_sub_le_dyadic (truth := truth) hη.le m m (le_refl m) + hno x 0 + rw [stationaryState_row_sub] at h + change |loss x 0| ≤ η / 100 at h + linarith + have hrow : raw + loss = actual.row := by + funext x ν + simp [loss] + have hactual := hfinal s K actual.defaultValue truth raw loss hK hfirst hloss + εfinal hεfinal herrfinal y hy + rw [hrow] at hactual + change |kind.stateRootError θ s K actual reference y| ≤ Cfinal * εfinal at hactual + have hreference := hpre s n Δ a truth K hK (by rw [ha]) (by rw [ha]; linarith) + m m 0 (by omega) hno hfirst hsecond (by intro i hi hi'; omega) ε hε herr y hy + change |kind.stateRootError θ s K reference ⟨0, truth⟩ y| ≤ + Cpre * ∑ i ∈ range m, dyadicFloor η m i * ε i at hreference + calc + _ ≤ |kind.stateRootError θ s K actual reference y| + + |kind.stateRootError θ s K reference ⟨0, truth⟩ y| := abs_sub_le _ _ _ + _ ≤ Cfinal * εfinal + Cpre * ∑ i ∈ range m, dyadicFloor η m i * ε i := + add_le_add hactual hreference + _ = _ := add_comm _ _ + +end Cslib.PolynomialAtomRow diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows/Relative.lean b/Complexity/Foundations/Probability/PolynomialAtomRows/Relative.lean index 29f54fba94..c3ac65f309 100644 --- a/Complexity/Foundations/Probability/PolynomialAtomRows/Relative.lean +++ b/Complexity/Foundations/Probability/PolynomialAtomRows/Relative.lean @@ -8,6 +8,7 @@ module -- upstream: candidate public import Complexity.Foundations.Probability.PolynomialAtomRows.RootError +public import Complexity.Foundations.Probability.PolynomialAtomRows.Saturation public import Complexity.Foundations.Analysis.RowCompression.GateClosure public import Complexity.Foundations.Analysis.RowCompression.SentinelRelative import Mathlib.Algebra.Order.Group.MinMax @@ -31,7 +32,6 @@ ceiling, or scalar regularity assumption is passed to the public comparison theo ## 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. @@ -50,25 +50,6 @@ 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) : diff --git a/Complexity/Foundations/Probability/PolynomialAtomRows/Saturation.lean b/Complexity/Foundations/Probability/PolynomialAtomRows/Saturation.lean new file mode 100644 index 0000000000..bcad6939d5 --- /dev/null +++ b/Complexity/Foundations/Probability/PolynomialAtomRows/Saturation.lean @@ -0,0 +1,53 @@ +/- +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 + +/-! +# Common saturation and gate bounds for polynomial rows + +Every concrete polynomial entry factor has saturated by its support scale `θ`, and every rank +gate has closed by the same bound. These scalar facts are shared by the static clipped-error +comparison and the iterated sentinel comparison. They do not involve compression schedules. + +## Main results + +* `Cslib.PolynomialAtomRow.eval_eq_of_entry_ge`: any two first entries at least `θ` give the + same output at a fixed rank. +* `Cslib.PolynomialAtomRow.gateThreshold_le_scale`: `θ` bounds every rank-gate close threshold. +-/ + +public section + +namespace Cslib.PolynomialAtomRow + +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')] + +/-- The common support scale is above every concrete rank-gate closure threshold. -/ +theorem gateThreshold_le_scale (hθ : 0 < θ) : kind.gateThreshold θ ≤ θ := by + cases kind <;> dsimp only [gateThreshold] <;> linarith + +end Cslib.PolynomialAtomRow diff --git a/ComplexityTests/PolynomialAtomNoOverflow.lean b/ComplexityTests/PolynomialAtomNoOverflow.lean new file mode 100644 index 0000000000..1db615da86 --- /dev/null +++ b/ComplexityTests/PolynomialAtomNoOverflow.lean @@ -0,0 +1,202 @@ +/- +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.NoOverflow +import Complexity.Foundations.Data.Finset.KthLargest.Truncation +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.NormNum + +/-! +# Static clipped comparison and no-overflow boundary cases + +A small raw perturbation crosses the preparation support boundary. The static comparison +allows a negative common default and arbitrarily large signed second-coordinate loss. The +empty-schedule theorem retains the same strictly positive output error and has no preloss term. + +A nonempty run uses size capacity one and rank two, so `K ≤ n` is false. Every raw input is +zero and the run has no overflow, yet its true preparation is one. The no-overflow comparison +applies with final envelope one, covering the range fallback and the absent capacity premise. +The separate `PolynomialAtomRows` regression exercises nonzero preloss with final raw error zero. +-/ + +namespace ComplexityTests.PolynomialAtomNoOverflow + +open Finset Cslib Cslib.RowCompression + +private noncomputable def truth : Fin 2 → Fin 2 → ℝ := ![![1 / 2, 0], ![0, 0]] + +private noncomputable def raw : Fin 2 → Fin 2 → ℝ := ![![1 / 2 + 1 / 100000000, 0], ![0, 0]] + +private noncomputable def signedLoss : Fin 2 → Fin 2 → ℝ := ![![0, 1000], ![0, -1000]] + +private theorem second_rank_zero {v : Fin 2 → ℝ} (hv : v 1 = 0) : kthLargest 2 univ v = 0 := by + apply le_antisymm _ kthLargest_nonneg + refine not_lt.mp fun hlt => ?_ + have hc := (lt_kthLargest_iff (by norm_num) (le_refl (0 : ℝ))).mp hlt + have hs : ({y | 0 < v y} : Finset (Fin 2)) ⊆ {0} := by + intro y hy + fin_cases y + · simp + · simp [hv] at hy + have hb := hc.trans (card_le_card hs) + norm_num at hb + +private theorem boundary_error (y : Fin 2) : + clippedError (truth y 0) (truth y 1) (raw y) ≤ 1 / 10000000 := by + fin_cases y <;> norm_num [truth, raw, clippedError] + +private theorem positive_boundary_error (z : ℝ) (hz : z ≤ 0) (loss : Fin 2 → Fin 2 → ℝ) + (hloss : ∀ y, loss y 0 = 0) : + 0 < PolynomialAtomRow.preparation.stateRootError 1 univ 2 + ⟨z, raw + loss⟩ ⟨z, truth + loss⟩ 0 := by + have hq : firstRank univ 2 z (raw + loss) = 0 := by + unfold firstRank + rw [second_rank_zero (by simp [raw, hloss])] + exact max_eq_right hz + have ha : PolynomialAtomRow.preparation.eval 1 ((raw + loss) 0 0) + (firstRank univ 2 z (raw + loss)) = + polynomialSwitch4 (1 / 2) (3 / 4) (1 / 2 + 1 / 100000000) := by + rw [hq] + have hv : (raw + loss) 0 0 = 1 / 2 + 1 / 100000000 := by simp [raw, hloss] + rw [hv] + change polynomialPrepRow4 1 (1 / 2 + 1 / 100000000) 0 = _ + rw [polynomialPrepRow4_of_rank_le (by norm_num) (by norm_num)] + norm_num [polynomialPrepCutoff4] + have hb : PolynomialAtomRow.preparation.eval 1 ((truth + loss) 0 0) + (firstRank univ 2 z (truth + loss)) = 0 := + polynomialPrepRow4_eq_zero_of_entry_le (by norm_num) (by simp [truth, hloss]) + 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 _ + +-- A negative common default and large signed second-coordinate losses are admissible, while +-- the actual polynomial root error is strictly positive. +example : signedLoss 0 1 = 1000 ∧ signedLoss 1 1 = -1000 ∧ + ∃ C : ℝ, 0 ≤ C ∧ + 0 < PolynomialAtomRow.preparation.stateRootError 1 univ 2 + ⟨-7, raw + signedLoss⟩ ⟨-7, truth + signedLoss⟩ 0 ∧ + |PolynomialAtomRow.preparation.stateRootError 1 univ 2 + ⟨-7, raw + signedLoss⟩ ⟨-7, truth + signedLoss⟩ 0| ≤ C / 10000000 := by + refine ⟨by norm_num [signedLoss], by norm_num [signedLoss], ?_⟩ + obtain ⟨C, hC, hbound⟩ := PolynomialAtomRow.preparation.exists_commonLoss_root_bound + (θ := 1) (by norm_num) + refine ⟨C, hC, positive_boundary_error (-7) (by norm_num) signedLoss + (fun y => by fin_cases y <;> norm_num [signedLoss]), ?_⟩ + have h := hbound univ 2 (-7) truth raw signedLoss (by norm_num) + (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun y _ => by fin_cases y <;> norm_num [signedLoss]) + (1 / 10000000) (by norm_num) (fun y _ => boundary_error y) 0 (mem_univ 0) + simpa only [div_eq_mul_inv, one_mul] using h + +-- Upper capping also preserves zero padding when the rank exceeds the retained cardinality +-- and an uncapped input is negative. +example : kthLargest 3 univ (fun y : Fin 2 => min (1 : ℝ) ((![-4, 1000] : Fin 2 → ℝ) y)) = 0 := by + rw [kthLargest_min (by norm_num) (by norm_num)] + norm_num [kthLargest, Fin.univ_succ, filter_insert, filter_singleton] + +-- The empty schedule has a positive final-prefix output error and an exactly zero preloss sum. +example : ∃ C : ℝ, 0 ≤ C ∧ + 0 < PolynomialAtomRow.preparation.stateRootError 1 univ 2 ⟨0, raw⟩ ⟨0, truth⟩ 0 ∧ + |PolynomialAtomRow.preparation.stateRootError 1 univ 2 ⟨0, raw⟩ ⟨0, truth⟩ 0| ≤ + C / 10000000 := by + obtain ⟨Cfinal, hCfinal, hscales⟩ := PolynomialAtomRow.preparation.exists_noOverflow_root_bound + (θ := 1) (by norm_num) + obtain ⟨Cpre, _, hbound⟩ := hscales (1 / 20000) (by norm_num) (by norm_num) + refine ⟨Cfinal, hCfinal, ?_, ?_⟩ + · simpa only [add_zero] using positive_boundary_error 0 (le_refl 0) 0 (by intros; rfl) + · have h := hbound univ (fun _ => 0) (fun _ => 0) ⟨0, raw⟩ truth 2 (by norm_num) rfl 0 + (by simp) (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun y _ => by fin_cases y <;> norm_num [truth]) (fun _ => 0) (by simp) (by simp) + (1 / 10000000) (by norm_num) + (fun y _ => by simpa only [uncompressedRow_zero] using boundary_error y) 0 (mem_univ 0) + simpa only [iterate_zero, sum_range_zero, mul_zero, zero_add, div_eq_mul_inv, one_mul] using h + +private noncomputable def smallCapacityTruth : Fin 2 → Fin 2 → ℝ := ![![1, 0], ![0, 0]] + +private noncomputable def smallCapacityActual : State (Fin 2) := + iterate univ (fun _ => 1) (fun _ => 2) (dyadicFloor (1 / 20000) 1) + (fun _ => 0) ⟨0, 0⟩ 1 + +private theorem smallCapacity_threshold : + threshold (univ : Finset (Fin 2)) 1 (dyadicFloor (1 / 20000) 1 0) 0 0 = 1 / 20480000 := by + norm_num [threshold, kthLargest, dyadicFloor, dyadicSlack, entrySize] + +private theorem smallCapacity_default : + newDefault (univ : Finset (Fin 2)) 1 2 (dyadicFloor (1 / 20000) 1 0) 0 0 = + 1 / 20480000 := by + rw [newDefault, smallCapacity_threshold] + norm_num [kthLargest] + +private theorem smallCapacity_state : smallCapacityActual = + ⟨1 / 20480000, fun _ => defaultEntry (1 / 20480000)⟩ := by + change advance univ 1 2 (dyadicFloor (1 / 20000) 1 0) 0 ⟨0, 0⟩ = _ + simp only [advance, add_zero, smallCapacity_default] + congr 1 + funext y + rw [← smallCapacity_default] + apply update_eq_default_of_size_le + rw [smallCapacity_threshold] + norm_num [entrySize] + +private theorem smallCapacity_no_overflow : ∀ i < 1, + stepThreshold (univ : Finset (Fin 2)) (fun _ => 1) (fun _ => 2) (dyadicFloor (1 / 20000) 1) + (fun _ => 0) ⟨0, 0⟩ i ≤ dyadicFloor (1 / 20000) 1 i := by + intro i hi + have hi0 : i = 0 := by omega + subst i + simp only [stepThreshold, inputRow, iterate_zero, add_zero] + rw [smallCapacity_threshold] + norm_num [dyadicFloor, dyadicSlack] + +private theorem smallCapacity_error : + |PolynomialAtomRow.preparation.stateRootError 1 univ 2 smallCapacityActual + ⟨0, smallCapacityTruth⟩ 0| = 1 := by + have ha : PolynomialAtomRow.preparation.eval 1 (smallCapacityActual.row 0 0) + (firstRank univ 2 smallCapacityActual.defaultValue smallCapacityActual.row) = 0 := by + apply polynomialPrepRow4_eq_zero_of_entry_le (by norm_num) + rw [smallCapacity_state] + norm_num [defaultEntry] + have hq : firstRank univ 2 0 smallCapacityTruth = 0 := by + rw [firstRank, second_rank_zero (by norm_num [smallCapacityTruth])] + norm_num + have hb : PolynomialAtomRow.preparation.eval 1 (smallCapacityTruth 0 0) + (firstRank univ 2 0 smallCapacityTruth) = 1 := by + rw [hq] + change polynomialPrepRow4 1 1 0 = 1 + rw [polynomialPrepRow4_of_rank_le (by norm_num) (by norm_num)] + exact polynomialPrepCutoff4_eq_one (by norm_num) (by norm_num) + unfold PolynomialAtomRow.stateRootError + rw [ha, hb, Real.zero_rpow (by norm_num : (4⁻¹ : ℝ) ≠ 0), Real.one_rpow] + norm_num + +-- This positive-error, nonempty no-overflow run has n=1 1) (fun _ => 0) ⟨0, 0⟩ smallCapacityTruth 2 + (by norm_num) rfl 1 smallCapacity_no_overflow + (fun y _ => by fin_cases y <;> norm_num [smallCapacityTruth]) + (fun y _ => by fin_cases y <;> norm_num [smallCapacityTruth]) (fun _ => 1) + (by intros; norm_num) (fun _ _ _ _ _ => clippedError_le_one _ _ _) + 1 (by norm_num) (fun _ _ => clippedError_le_one _ _ _) 0 (mem_univ 0) + change |PolynomialAtomRow.preparation.stateRootError 1 univ 2 smallCapacityActual + ⟨0, smallCapacityTruth⟩ 0| ≤ _ at h + rw [smallCapacity_error] at h + norm_num [dyadicFloor, dyadicSlack] at h + simpa only [div_eq_mul_inv, one_mul] using h + +end ComplexityTests.PolynomialAtomNoOverflow diff --git a/ComplexityTests/PolynomialAtomRows.lean b/ComplexityTests/PolynomialAtomRows.lean index 2b2fe09c9c..82e5a11bd5 100644 --- a/ComplexityTests/PolynomialAtomRows.lean +++ b/ComplexityTests/PolynomialAtomRows.lean @@ -5,9 +5,11 @@ Authors: Samuel Schlesinger -/ import Complexity.Foundations.Probability.PolynomialAtomRows.FirstOverflow +import Complexity.Foundations.Probability.PolynomialAtomRows.NoOverflow import Mathlib.LinearAlgebra.Matrix.Notation import Mathlib.Tactic.FinCases import Mathlib.Tactic.Linarith +import Mathlib.Tactic.IntervalCases import Mathlib.Tactic.NormNum /-! @@ -20,6 +22,8 @@ The remaining group raises the default and erases a second-coordinate value of ` 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. +Increasing the size capacity to three gives a second completion with no overflow at all. Its +final raw error is zero and the same positive witness error is paid entirely by weighted preloss. -/ namespace ComplexityTests.PolynomialAtomRows @@ -359,4 +363,143 @@ example : ∃ C : ℝ, 0 ≤ C ∧ 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 +private theorem third_rank_zero (v : Fin 2 → ℝ) : kthLargest 3 univ v = 0 := by + apply le_antisymm _ kthLargest_nonneg + refine not_lt.mp fun hlt => ?_ + have hc := (lt_kthLargest_iff (by norm_num) (le_refl (0 : ℝ))).mp hlt + have hb := card_filter_le (s := (univ : Finset (Fin 2))) (p := fun y => 0 < v y) + norm_num at hb + omega + +private noncomputable def spaciousRun : ℕ → State (Fin 2) := + iterate univ (fun _ => 3) (fun _ => 2) (dyadicFloor 1 2) completingIncrements initial + +private theorem spacious_one : spaciousRun 1 = + ⟨1 / 1048576, ![![900, 0], ![1 / 1048576, 0]]⟩ := by + have ht : threshold univ 3 (1 / 1048576) 0 rawRow = 1 / 1048576 := by + rw [threshold, third_rank_zero] + norm_num + have hd : newDefault univ 3 2 (1 / 1048576) 0 rawRow = 1 / 1048576 := by + unfold newDefault + rw [ht] + exact max_eq_left ((min_le_left _ _).trans (max_le (by norm_num) raw_rank_le)) + have hin : initial.row + completingIncrements 0 = rawRow := by + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [initial, completingIncrements, increments, rawRow] + change advance univ 3 2 (dyadicFloor 1 2 0) (completingIncrements 0) initial = _ + unfold advance + rw [hin, floor_zero] + change State.mk (newDefault univ 3 2 (1 / 1048576) 0 rawRow) + (update univ 3 2 (1 / 1048576) 0 rawRow) = _ + rw [hd] + congr 1 + unfold update + rw [ht, hd] + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [rawRow, updateEntry, radius, entrySize, defaultEntry] + +private theorem spacious_input_one : + inputRow univ (fun _ => 3) (fun _ => 2) (dyadicFloor 1 2) + completingIncrements initial 1 = reference.row := by + change (spaciousRun 1).row + completingIncrements 1 = reference.row + rw [spacious_one, reference_eq] + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [completingIncrements, truth, rawRow] + +private theorem spacious_no_overflow : ∀ i < 2, + stepThreshold univ (fun _ => 3) (fun _ => 2) (dyadicFloor 1 2) + completingIncrements initial i ≤ dyadicFloor 1 2 i := by + intro i hi + interval_cases i + · simp only [stepThreshold, iterate_zero, initial, threshold, third_rank_zero] + norm_num [dyadicFloor, dyadicSlack] + · unfold stepThreshold + rw [spacious_input_one] + change threshold univ 3 (dyadicFloor 1 2 1) (spaciousRun 1).defaultValue reference.row ≤ _ + rw [spacious_one] + simp only [threshold, third_rank_zero] + norm_num [dyadicFloor, dyadicSlack] + +private theorem reference_kth : kthLargest 2 univ (fun y => reference.row y 0) = + 260 + 1 / 2097152 := by + have hz : reference.defaultValue < 260 + 1 / 2097152 := by rw [reference_eq]; norm_num + have hle : 260 + 1 / 2097152 ≤ + max reference.defaultValue (kthLargest 2 univ fun y => reference.row y 0) := reference_rank.ge + exact le_antisymm (kthLargest_le_firstRank.trans reference_rank.le) + ((le_max_iff.mp hle).resolve_left (not_le.mpr hz)) + +private theorem spacious_two : spaciousRun 2 = ⟨3 / 1024, reference.row⟩ := by + have ht : threshold univ 3 (1 / 1024) (1 / 1048576) reference.row = 1 / 1024 := by + rw [threshold, third_rank_zero] + norm_num + have hd : newDefault univ 3 2 (1 / 1024) (1 / 1048576) reference.row = 3 / 1024 := by + unfold newDefault + rw [ht, reference_kth] + norm_num + change advance univ 3 2 (dyadicFloor 1 2 1) (completingIncrements 1) (spaciousRun 1) = _ + have hrow : (spaciousRun 1).row + completingIncrements 1 = reference.row := spacious_input_one + unfold advance + rw [hrow, spacious_one, show dyadicFloor (1 : ℝ) 2 1 = 1 / 1024 by + norm_num [dyadicFloor, dyadicSlack], hd] + congr 1 + unfold update + rw [ht, hd, reference_eq] + funext y ν + fin_cases y <;> fin_cases ν <;> norm_num [updateEntry, radius, entrySize, defaultEntry] + +private theorem spacious_output : PolynomialAtomRow.witness.eval 10000 + ((spaciousRun 2).row 0 0) (firstRank univ 2 (spaciousRun 2).defaultValue (spaciousRun 2).row) = + output reference := by + have hq : firstRank univ 2 (3 / 1024) reference.row = 260 + 1 / 2097152 := by + unfold firstRank + rw [reference_kth] + norm_num + rw [spacious_two] + change PolynomialAtomRow.witness.eval 10000 (reference.row 0 0) + (firstRank univ 2 (3 / 1024) reference.row) = output reference + rw [hq] + unfold output + rw [reference_rank] + +-- Two actual compression groups avoid overflow, but the first group's nonzero preloss shifts +-- the final witness rank. The final raw prefix is exactly truth, so the final-error term is zero. +example : (∀ i < 2, stepThreshold univ (fun _ => 3) (fun _ => 2) (dyadicFloor 1 2) + completingIncrements initial i ≤ dyadicFloor 1 2 i) ∧ + uncompressedRow completingIncrements initial.row 2 = truth ∧ + (spaciousRun 1).row 1 0 - rawRow 1 0 = 1 / 2097152 ∧ + 0 < |PolynomialAtomRow.witness.stateRootError 10000 univ 2 (spaciousRun 2) ⟨0, truth⟩ 0| := by + refine ⟨spacious_no_overflow, completing_raw_two, ?_, ?_⟩ + · rw [spacious_one] + norm_num [rawRow] + · unfold PolynomialAtomRow.stateRootError + rw [spacious_output, 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)))) + +example : ∃ C : ℝ, 0 ≤ C ∧ + |PolynomialAtomRow.witness.stateRootError 10000 univ 2 (spaciousRun 2) ⟨0, truth⟩ 0| ≤ + C / 1048576 := by + obtain ⟨Cfinal, _, hscales⟩ := PolynomialAtomRow.witness.exists_noOverflow_root_bound + (θ := 10000) (by norm_num) + obtain ⟨Cpre, hCpre, hbound⟩ := hscales 1 (by norm_num) (by norm_num) + refine ⟨Cpre, hCpre, ?_⟩ + have h := hbound univ (fun _ => 3) completingIncrements initial truth 2 (by norm_num) rfl + 2 spacious_no_overflow + (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun y _ => by fin_cases y <;> norm_num [truth]) + (fun i => if i = 0 then 1 else 0) (by intro i _; split_ifs <;> norm_num) + (by + intro i hi y _ _ + interval_cases i + · simpa only [↓reduceIte] using clippedError_le_one (truth y 0) (truth y 1) + (uncompressedRow completingIncrements initial.row 1 y) + · change clippedError (truth y 0) (truth y 1) + (uncompressedRow completingIncrements initial.row 2 y) ≤ 0 + rw [completing_raw_two, clippedError_self _ _ _ rfl rfl]) + 0 (le_refl 0) (by + intro y _ + rw [completing_raw_two, clippedError_self _ _ _ rfl rfl]) 0 (mem_univ 0) + norm_num [sum_range_succ, floor_zero] at h + simpa only [div_eq_mul_inv, one_mul, spaciousRun] using h + end ComplexityTests.PolynomialAtomRows