From fe32886a35bef3cbaa59e3e3dc1516326b8d43da Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:40:58 +0000 Subject: [PATCH 1/5] feat: add rational polynomial switches with Lipschitz fourth roots Supply a computable rational degree-seven transition and its rescaling, with real endpoint, monotonicity, and value/complement fourth-root Lipschitz laws. Exact rational cast lemmas connect the arithmetic definitions to the real analysis. Concrete tests cover interior values, affine rescaling, clamping, equal endpoints, and root perturbations across both transition boundaries. This advances issue #1721's fourth-moment route. The pinned primary source OpenAI2026LogSpace, atoms.tex Section 5.1 at revision 7ef5c0cc, uses the same normalized-integral construction with s = 8. This implementation specializes it to s = 4 and does not claim eighth-root regularity, complete hierarchy admissibility, or machine resource bounds. No OpenAI Lean was consulted. Validation on base 2d1638ce with the two added files: both modules compile under the repository's Lean options with warnings as errors using isolated temporary outputs and read-only existing dependencies; focused check_hygiene.py --check-simp and git diff --cached --check pass. The final documentation-only wording change was inspected after those builds. Full repository integration gates and independent review remain for coordinator integration; no aggregate file has been edited. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved source a6967d13aafee47ae16b61ac2b12f533426f9971 and freshly compiled both files. Publication adds only the generated aggregate import. Integrated strict module/test builds, hygiene and whitespace checks pass. Full gates run in PR CI. --- Complexity.lean | 4 + .../SpecialFunctions/PolynomialSwitch.lean | 299 ++++++++++++++++++ ComplexityTests/PolynomialSwitch.lean | 77 +++++ 3 files changed, 380 insertions(+) create mode 100644 Complexity/Foundations/Analysis/SpecialFunctions/PolynomialSwitch.lean create mode 100644 ComplexityTests/PolynomialSwitch.lean diff --git a/Complexity.lean b/Complexity.lean index 9a3bc3cdea..257d53cdd7 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2352,7 +2352,11 @@ public import Complexity.Foundations.Analysis.LpNorm public import Complexity.Foundations.Analysis.LpNormMeasure public import Complexity.Foundations.Analysis.MarkovBrothersInequality public import Complexity.Foundations.Analysis.RootError +public import Complexity.Foundations.Analysis.RowCompression +public import Complexity.Foundations.Analysis.RowCompression.Floors +public import Complexity.Foundations.Analysis.RowCompression.Iteration public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos +public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli public import Complexity.Foundations.BooleanAnalysis.Bonami diff --git a/Complexity/Foundations/Analysis/SpecialFunctions/PolynomialSwitch.lean b/Complexity/Foundations/Analysis/SpecialFunctions/PolynomialSwitch.lean new file mode 100644 index 0000000000..1ee62aee99 --- /dev/null +++ b/Complexity/Foundations/Analysis/SpecialFunctions/PolynomialSwitch.lean @@ -0,0 +1,299 @@ +/- +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.Init +public import Mathlib.Basic.Real.Basic +public import Mathlib.Analysis.Calculus.Deriv.Pow +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +public import Mathlib.Topology.MetricSpace.Lipschitz +import Mathlib.Analysis.Calculus.ContDiff.RCLike +import Mathlib.Analysis.Calculus.Deriv.MeanValue +import Mathlib.Analysis.Normed.MulAction +import Mathlib.Analysis.SpecialFunctions.Pow.Deriv +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.FunProp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Polynomial switches with Lipschitz fourth roots + +The fourth-moment workstream of complexitylib issue #1721 needs a monotone switch whose fourth +root and complementary fourth root are Lipschitz. The switch of [OpenAI2026LogSpace, Section 5.1] +is a rescaled normalized integral of `t^(s-1) (1-t)^(s-1)` on `[0,1]`. +For the fourth-moment route (`s = 4`), its polynomial +is `35 t^4 - 84 t^5 + 70 t^6 - 20 t^7`. + +We give that polynomial as the equivalent factored expression +`t^4 * (1 + 4(1-t) + 10(1-t)^2 + 20(1-t)^3)` and clamp its input to `[0,1]`. +The polynomial, clamped transition and rescaled switch use only field arithmetic and min/max; +their definitions also specialize to computable functions on `ℚ`. The cast lemmas identify those +exact rational evaluations with the real functions used by the analysis. They assert no machine +resource bound or rational approximation to the fourth root. + +The factor after `t^4` is at least one on `[0,1]`. Thus the fourth root is `t` times the fourth +root of a positive polynomial, which is continuously differentiable on that interval and hence +Lipschitz there. Composing with clamping gives a global Lipschitz bound. The complement follows +by reflection. These primitives do not yet provide the complete admissible hierarchy parameters, +their threshold ladder, or the regularity of the unbounded correction ramp. + +## Main definitions + +* `Cslib.transitionPolynomial4`: the polynomial whose value at zero and complement at one + vanish to fourth order. +* `Cslib.polynomialTransition4`: its clamped transition from zero to one. +* `Cslib.polynomialSwitch4`: its rescaling to an arbitrary nondegenerate interval. + +## Main results + +* `Cslib.polynomialSwitch4_nonneg`, `Cslib.polynomialSwitch4_le_one`: range bounds. +* `Cslib.polynomialSwitch4_eq_zero_iff`, `Cslib.polynomialSwitch4_eq_one_iff`: exact endpoints. +* `Cslib.monotone_polynomialSwitch4`: monotonicity. +* `Cslib.exists_lipschitzWith_polynomialSwitch4_root`, + `Cslib.exists_lipschitzWith_one_sub_polynomialSwitch4_root`: Lipschitz fourth roots. +* `Cslib.polynomialSwitch4_ratCast`: exact compatibility with rational evaluation. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 5.1 (23 September 2026, revision `7ef5c0cc`, not peer reviewed). The paper uses `s = 8`; + this module gives the same normalized-integral construction for the project's `s = 4` route. +-/ + +public section + +namespace Cslib + +/-- The normalized integral polynomial for the fourth-moment switch, in a form displaying its +fourth-order zero and a positive remaining factor on `[0,1]`. -/ +@[expose] def transitionPolynomial4 {R : Type*} [CommRing R] (t : R) : R := + t ^ 4 * (1 + 4 * (1 - t) + 10 * (1 - t) ^ 2 + 20 * (1 - t) ^ 3) + +/-- The degree-seven transition polynomial, clamped to the unit interval. Its generic definition +can be evaluated exactly on rational inputs. -/ +@[expose] def polynomialTransition4 {R : Type*} [CommRing R] [LinearOrder R] (t : R) : R := + transitionPolynomial4 (max 0 (min 1 t)) + +/-- Rescale the fourth-moment polynomial transition from `[0,1]` to `[α,β]`. The switch laws +assume `α < β`; the arithmetic expression itself is defined for all endpoints. -/ +@[expose] def polynomialSwitch4 {R : Type*} [Field R] [LinearOrder R] (α β t : R) : R := + polynomialTransition4 ((t - α) / (β - α)) + +section Polynomial + +variable {R : Type*} [CommRing R] + +theorem transitionPolynomial4_expanded (t : R) : + transitionPolynomial4 t = 35 * t ^ 4 - 84 * t ^ 5 + 70 * t ^ 6 - 20 * t ^ 7 := by + unfold transitionPolynomial4 + ring + +@[simp] theorem transitionPolynomial4_zero : transitionPolynomial4 (0 : R) = 0 := by + simp [transitionPolynomial4] + +@[simp] theorem transitionPolynomial4_one : transitionPolynomial4 (1 : R) = 1 := by + simp [transitionPolynomial4] + +/-- Reflection interchanges the transition polynomial and its complement. -/ +theorem one_sub_transitionPolynomial4 (t : R) : + 1 - transitionPolynomial4 t = transitionPolynomial4 (1 - t) := by + unfold transitionPolynomial4 + ring + +end Polynomial + +private theorem factor_pos {t : ℝ} (ht : t ≤ 1) : + 0 < 1 + 4 * (1 - t) + 10 * (1 - t) ^ 2 + 20 * (1 - t) ^ 3 := by + have h : 0 ≤ 1 - t := sub_nonneg.mpr ht + positivity + +/-- The derivative identifies the normalization of the integral `t^3 (1-t)^3`. -/ +theorem hasDerivAt_transitionPolynomial4 (t : ℝ) : + HasDerivAt transitionPolynomial4 (140 * t ^ 3 * (1 - t) ^ 3) t := by + convert (((hasDerivAt_pow 4 t).const_mul 35).sub + ((hasDerivAt_pow 5 t).const_mul 84) |>.add ((hasDerivAt_pow 6 t).const_mul 70)).sub + ((hasDerivAt_pow 7 t).const_mul 20) using 1 + · funext x + exact transitionPolynomial4_expanded x + · ring + +theorem monotoneOn_transitionPolynomial4 : + MonotoneOn (transitionPolynomial4 : ℝ → ℝ) (Set.Icc 0 1) := by + refine monotoneOn_of_deriv_nonneg (convex_Icc 0 1) + (fun x _ => (hasDerivAt_transitionPolynomial4 x).continuousAt.continuousWithinAt) + (fun x _ => (hasDerivAt_transitionPolynomial4 x).differentiableAt.differentiableWithinAt) + fun x hx => ?_ + rw [(hasDerivAt_transitionPolynomial4 x).deriv] + have hx' : x ∈ Set.Icc (0 : ℝ) 1 := interior_subset hx + have h0 : 0 ≤ x := hx'.1 + have h1 : 0 ≤ 1 - x := sub_nonneg.mpr hx'.2 + positivity + +private theorem clamp_mem (t : ℝ) : max 0 (min 1 t) ∈ Set.Icc (0 : ℝ) 1 := + ⟨le_max_left _ _, max_le zero_le_one (min_le_left _ _)⟩ + +theorem polynomialTransition4_nonneg (t : ℝ) : 0 ≤ polynomialTransition4 t := by + have h := monotoneOn_transitionPolynomial4 (Set.left_mem_Icc.mpr zero_le_one) (clamp_mem t) + (clamp_mem t).1 + simpa only [polynomialTransition4, transitionPolynomial4_zero] using h + +theorem polynomialTransition4_le_one (t : ℝ) : polynomialTransition4 t ≤ 1 := by + have h := monotoneOn_transitionPolynomial4 (clamp_mem t) (Set.right_mem_Icc.mpr zero_le_one) + (clamp_mem t).2 + simpa only [polynomialTransition4, transitionPolynomial4_one] using h + +theorem polynomialTransition4_of_nonpos {t : ℝ} (ht : t ≤ 0) : polynomialTransition4 t = 0 := by + rw [polynomialTransition4, min_eq_right (ht.trans zero_le_one), max_eq_left ht] + exact transitionPolynomial4_zero + +theorem polynomialTransition4_of_one_le {t : ℝ} (ht : 1 ≤ t) : polynomialTransition4 t = 1 := by + rw [polynomialTransition4, min_eq_left ht, max_eq_right zero_le_one] + exact transitionPolynomial4_one + +theorem polynomialTransition4_of_mem {t : ℝ} (ht : t ∈ Set.Icc 0 1) : + polynomialTransition4 t = transitionPolynomial4 t := by + rw [polynomialTransition4, min_eq_right ht.2, max_eq_right ht.1] + +theorem monotone_polynomialTransition4 : Monotone (polynomialTransition4 : ℝ → ℝ) := + fun x y hxy => monotoneOn_transitionPolynomial4 (clamp_mem x) (clamp_mem y) + (max_le_max le_rfl (min_le_min le_rfl hxy)) + +/-- Reflection interchanges the clamped transition and its complement. -/ +theorem one_sub_polynomialTransition4 (t : ℝ) : + 1 - polynomialTransition4 t = polynomialTransition4 (1 - t) := by + by_cases ht0 : t ≤ 0 + · rw [polynomialTransition4_of_nonpos ht0, + polynomialTransition4_of_one_le (by linarith : 1 ≤ 1 - t), sub_zero] + by_cases ht1 : 1 ≤ t + · rw [polynomialTransition4_of_one_le ht1, + polynomialTransition4_of_nonpos (by linarith : 1 - t ≤ 0), sub_self] + have ht : t ∈ Set.Icc (0 : ℝ) 1 := ⟨(not_le.mp ht0).le, (not_le.mp ht1).le⟩ + have ht' : 1 - t ∈ Set.Icc (0 : ℝ) 1 := ⟨by linarith [ht.2], by linarith [ht.1]⟩ + rw [polynomialTransition4_of_mem ht, polynomialTransition4_of_mem ht', + one_sub_transitionPolynomial4] + +theorem polynomialTransition4_eq_zero_iff {t : ℝ} : polynomialTransition4 t = 0 ↔ t ≤ 0 := by + refine ⟨fun h => ?_, polynomialTransition4_of_nonpos⟩ + by_contra ht + have hp : 0 < max 0 (min 1 t) := + (lt_min zero_lt_one (lt_of_not_ge ht)).trans_le (le_max_right _ _) + have hf := factor_pos (clamp_mem t).2 + have : 0 < polynomialTransition4 t := by + unfold polynomialTransition4 transitionPolynomial4 + positivity + exact this.ne' h + +theorem polynomialTransition4_eq_one_iff {t : ℝ} : polynomialTransition4 t = 1 ↔ 1 ≤ t := by + refine ⟨fun h => ?_, polynomialTransition4_of_one_le⟩ + have hz : polynomialTransition4 (1 - t) = 0 := by + rw [← one_sub_polynomialTransition4, h, sub_self] + have := polynomialTransition4_eq_zero_iff.mp hz + linarith + +/-! ## Fourth-root regularity -/ + +private theorem root_eq {t : ℝ} (ht : t ∈ Set.Icc 0 1) : + transitionPolynomial4 t ^ (4⁻¹ : ℝ) = + t * (1 + 4 * (1 - t) + 10 * (1 - t) ^ 2 + 20 * (1 - t) ^ 3) ^ (4⁻¹ : ℝ) := by + rw [transitionPolynomial4, Real.mul_rpow (pow_nonneg ht.1 _) (factor_pos ht.2).le] + congr 1 + convert Real.pow_rpow_inv_natCast ht.1 (by norm_num : (4 : ℕ) ≠ 0) using 1 + +/-- The fourth root is Lipschitz globally; the transition has fourth-order vanishing at zero. -/ +theorem exists_lipschitzWith_polynomialTransition4_root : + ∃ K, LipschitzWith K fun t : ℝ => polynomialTransition4 t ^ (4⁻¹ : ℝ) := by + have hf : ContDiffOn ℝ 1 (fun t : ℝ => + t * (1 + 4 * (1 - t) + 10 * (1 - t) ^ 2 + 20 * (1 - t) ^ 3) ^ (4⁻¹ : ℝ)) + (Set.Icc 0 1) := by + apply contDiffOn_id.mul + apply ContDiffOn.rpow_const_of_ne (by fun_prop) + exact fun t ht => (factor_pos ht.2).ne' + obtain ⟨K, hK⟩ := hf.exists_lipschitzOnWith one_ne_zero (convex_Icc 0 1) isCompact_Icc + refine ⟨K, LipschitzWith.of_dist_le_mul fun x y => ?_⟩ + have hproj := (LipschitzWith.projIcc (zero_le_one' ℝ)).dist_le_mul x y + have hb := hK.dist_le_mul _ (clamp_mem x) _ (clamp_mem y) + rw [← root_eq (clamp_mem x), ← root_eq (clamp_mem y)] at hb + refine hb.trans ?_ + simp only [Subtype.dist_eq, NNReal.coe_one, one_mul, Set.coe_projIcc] at hproj + exact mul_le_mul_of_nonneg_left hproj K.2 + +/-- The fourth root of the complement is Lipschitz, by reflection at `1/2`. -/ +theorem exists_lipschitzWith_one_sub_polynomialTransition4_root : + ∃ K, LipschitzWith K fun t : ℝ => (1 - polynomialTransition4 t) ^ (4⁻¹ : ℝ) := by + obtain ⟨K, hK⟩ := exists_lipschitzWith_polynomialTransition4_root + refine ⟨K, LipschitzWith.of_dist_le_mul fun x y => ?_⟩ + simp only [one_sub_polynomialTransition4] + simpa only [dist_sub_left] using hK.dist_le_mul (1 - x) (1 - y) + +/-! ## Rescaling and exact rational values -/ + +variable {α β t : ℝ} + +theorem polynomialSwitch4_nonneg (α β t : ℝ) : 0 ≤ polynomialSwitch4 α β t := + polynomialTransition4_nonneg _ + +theorem polynomialSwitch4_le_one (α β t : ℝ) : polynomialSwitch4 α β t ≤ 1 := + polynomialTransition4_le_one _ + +theorem polynomialSwitch4_eq_zero_iff (hαβ : α < β) : + polynomialSwitch4 α β t = 0 ↔ t ≤ α := by + rw [polynomialSwitch4, polynomialTransition4_eq_zero_iff, div_le_iff₀ (sub_pos.mpr hαβ), + zero_mul, sub_nonpos] + +theorem polynomialSwitch4_eq_one_iff (hαβ : α < β) : + polynomialSwitch4 α β t = 1 ↔ β ≤ t := by + rw [polynomialSwitch4, polynomialTransition4_eq_one_iff, one_le_div (sub_pos.mpr hαβ), + sub_le_sub_iff_right] + +theorem polynomialSwitch4_of_le (hαβ : α < β) (ht : t ≤ α) : polynomialSwitch4 α β t = 0 := + (polynomialSwitch4_eq_zero_iff hαβ).mpr ht + +theorem polynomialSwitch4_of_ge (hαβ : α < β) (ht : β ≤ t) : polynomialSwitch4 α β t = 1 := + (polynomialSwitch4_eq_one_iff hαβ).mpr ht + +theorem monotone_polynomialSwitch4 (hαβ : α ≤ β) : Monotone (polynomialSwitch4 α β) := + fun _ _ h => monotone_polynomialTransition4 + (div_le_div_of_nonneg_right (sub_le_sub_right h α) (sub_nonneg.mpr hαβ)) + +/-- Rescaled switches have Lipschitz fourth roots, even for reversed or equal endpoints. -/ +theorem exists_lipschitzWith_polynomialSwitch4_root (α β : ℝ) : + ∃ K, LipschitzWith K fun t => polynomialSwitch4 α β t ^ (4⁻¹ : ℝ) := by + obtain ⟨K, hK⟩ := exists_lipschitzWith_polynomialTransition4_root + refine ⟨K * (‖(β - α)⁻¹‖₊ * 1), ?_⟩ + simpa only [polynomialSwitch4, Function.comp_def, smul_eq_mul, sub_eq_add_neg, div_eq_mul_inv, + mul_comm] using hK.comp + ((lipschitzWith_smul (β - α)⁻¹).comp (isometry_add_right (-α)).lipschitzWith) + +/-- The complementary rescaled switches also have Lipschitz fourth roots. -/ +theorem exists_lipschitzWith_one_sub_polynomialSwitch4_root (α β : ℝ) : + ∃ K, LipschitzWith K fun t => (1 - polynomialSwitch4 α β t) ^ (4⁻¹ : ℝ) := by + obtain ⟨K, hK⟩ := exists_lipschitzWith_one_sub_polynomialTransition4_root + refine ⟨K * (‖(β - α)⁻¹‖₊ * 1), ?_⟩ + simpa only [polynomialSwitch4, Function.comp_def, smul_eq_mul, sub_eq_add_neg, div_eq_mul_inv, + mul_comm] using hK.comp + ((lipschitzWith_smul (β - α)⁻¹).comp (isometry_add_right (-α)).lipschitzWith) + +@[simp, norm_cast] +theorem transitionPolynomial4_ratCast (t : ℚ) : + transitionPolynomial4 (t : ℝ) = (transitionPolynomial4 t : ℚ) := by + simp [transitionPolynomial4] + +@[simp, norm_cast] +theorem polynomialTransition4_ratCast (t : ℚ) : + polynomialTransition4 (t : ℝ) = (polynomialTransition4 t : ℚ) := by + simp only [polynomialTransition4, ← transitionPolynomial4_ratCast, Rat.cast_max, Rat.cast_min, + Rat.cast_zero, Rat.cast_one] + +@[simp, norm_cast] +theorem polynomialSwitch4_ratCast (α β t : ℚ) : + polynomialSwitch4 (α : ℝ) β t = (polynomialSwitch4 α β t : ℚ) := by + simp only [polynomialSwitch4, ← polynomialTransition4_ratCast, Rat.cast_div, Rat.cast_sub] + +end Cslib diff --git a/ComplexityTests/PolynomialSwitch.lean b/ComplexityTests/PolynomialSwitch.lean new file mode 100644 index 0000000000..bc5f89fc93 --- /dev/null +++ b/ComplexityTests/PolynomialSwitch.lean @@ -0,0 +1,77 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch +import Mathlib.Tactic.NormNum + +/-! +# Tests for rational polynomial switches and fourth-root bounds + +These examples evaluate the transition on rational inputs, transport an exact value to the real +switch, and use the global fourth-root bounds with concrete thresholds. They concern the `s = 4` +adaptation in issue #1721, not the pinned preprint's `s = 8` choice. +-/ + +namespace ComplexityTests.PolynomialSwitch + +open Cslib +open scoped NNReal + +-- The first-quarter value tests the interior polynomial, rather than only its plateau values. +example : polynomialTransition4 (1 / 4 : ℚ) = 289 / 4096 := by + norm_num [polynomialTransition4, transitionPolynomial4] + +example : polynomialTransition4 (3 / 4 : ℚ) = 3807 / 4096 := by + norm_num [polynomialTransition4, transitionPolynomial4] + +-- A translated and rescaled interval retains the exact rational transition. +example : polynomialSwitch4 (2 : ℚ) 6 3 = 289 / 4096 := by + norm_num [polynomialSwitch4, polynomialTransition4, transitionPolynomial4] + +example : polynomialSwitch4 (2 : ℚ) 6 4 = 1 / 2 := by + norm_num [polynomialSwitch4, polynomialTransition4, transitionPolynomial4] + +example : polynomialSwitch4 (2 : ℚ) 6 (-10) = 0 ∧ polynomialSwitch4 (2 : ℚ) 6 10 = 1 := by + norm_num [polynomialSwitch4, polynomialTransition4, transitionPolynomial4] + +-- The real analysis uses exactly the same values as the rational arithmetic. +example : polynomialSwitch4 (2 : ℝ) 6 3 = 289 / 4096 := by + have h : polynomialSwitch4 (2 : ℚ) 6 3 = 289 / 4096 := by + norm_num [polynomialSwitch4, polynomialTransition4, transitionPolynomial4] + have hc := polynomialSwitch4_ratCast (2 : ℚ) 6 3 + rw [h] at hc + norm_num at hc ⊢ + exact hc + +-- A zero-width interval is defined by field division by zero, without a false endpoint law. +example (t : ℚ) : polynomialSwitch4 2 2 t = 0 := by + simp [polynomialSwitch4, polynomialTransition4] + +-- Reflection is an identity for every real input, including both plateaus. +example (t : ℝ) : + 1 - polynomialTransition4 t = polynomialTransition4 (1 - t) := + one_sub_polynomialTransition4 t + +-- The fourth-root perturbation estimate remains valid across the lower transition endpoint. +example : ∃ K : ℝ≥0, ∀ t : ℝ, + |polynomialSwitch4 2 6 t ^ (4⁻¹ : ℝ)| ≤ K * |t - 2| := by + obtain ⟨K, hK⟩ := exists_lipschitzWith_polynomialSwitch4_root 2 6 + refine ⟨K, fun t => ?_⟩ + have h := hK.dist_le_mul t 2 + rw [polynomialSwitch4_of_le (by norm_num : (2 : ℝ) < 6) le_rfl, + Real.zero_rpow (by norm_num : (4⁻¹ : ℝ) ≠ 0)] at h + simpa only [Real.dist_eq, sub_zero] using h + +-- The complementary root has the corresponding bound at the upper transition endpoint. +example : ∃ K : ℝ≥0, ∀ t : ℝ, + |(1 - polynomialSwitch4 2 6 t) ^ (4⁻¹ : ℝ)| ≤ K * |t - 6| := by + obtain ⟨K, hK⟩ := exists_lipschitzWith_one_sub_polynomialSwitch4_root 2 6 + refine ⟨K, fun t => ?_⟩ + have h := hK.dist_le_mul t 6 + rw [polynomialSwitch4_of_ge (by norm_num : (2 : ℝ) < 6) le_rfl, sub_self, + Real.zero_rpow (by norm_num : (4⁻¹ : ℝ) ≠ 0)] at h + simpa only [Real.dist_eq, sub_zero] using h + +end ComplexityTests.PolynomialSwitch From ce9a0be4205a4ec7e91ae0af544d7585e77c0479 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:44:43 +0000 Subject: [PATCH 2/5] fix(logspace): keep cutoff aggregate independent of compression Remove three aggregate imports that came from untracked source copies during integration. The polynomial switch module and tests are unchanged. Validate import targets against the committed Git tree before publication. --- Complexity.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Complexity.lean b/Complexity.lean index 257d53cdd7..bccc4b1393 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2352,9 +2352,6 @@ public import Complexity.Foundations.Analysis.LpNorm public import Complexity.Foundations.Analysis.LpNormMeasure public import Complexity.Foundations.Analysis.MarkovBrothersInequality public import Complexity.Foundations.Analysis.RootError -public import Complexity.Foundations.Analysis.RowCompression -public import Complexity.Foundations.Analysis.RowCompression.Floors -public import Complexity.Foundations.Analysis.RowCompression.Iteration public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch From 92e41efe0ccab99b797f4b22c6a8aead445564c7 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:57:57 +0000 Subject: [PATCH 3/5] feat: construct a rational correction ramp with Lipschitz fourth root Use Q(t) = a*u^4/(1+u)^3 with u = max(0,(t-theta)/a). For a>0, prove nonnegativity, the upper ramp bound, lower defect theta+3*a, monotonicity, and global Lipschitz constant one. The fourth root is globally Lipschitz with explicit constant |a^(1/4)|*|a^-1|; the proof also bounds its derivative at arbitrarily large positive inputs. Definitions use exact rational arithmetic and have real cast lemmas. This is an alternative rational witness for the correction-ramp conditions of OpenAI2026LogSpace Section 4.1 at revision 7ef5c0cc, adapted to issue #1721's fourth-moment route. The primary source uses eighth roots. Full hierarchy threshold/cutoff instantiation is a separate next component; no machine resource bound is asserted and no OpenAI Lean was consulted. Validation atop a6967d13: the module and focused tests compile with the repository Lean options and warnings as errors, using private temporary outputs and read-only existing dependencies. Tests cover exact rational values, negative and large inputs, real cast compatibility, uniform ramp bounds, ordinary perturbation, and the explicit fourth-root Lipschitz constant 8 when a=1/16. Focused hygiene --check-simp and diffcheck pass. Independent review and full integration gates remain for the coordinator. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-source-release-20261030 approved d3d62d9ff7fe1e54fabbf8b3ce779f929736f6ba. Publication preserves source/tests and adds generated import registration. Integrated strict module/test builds and hygiene/committed import checks pass. Full gates run in PR CI. --- Complexity.lean | 1 + .../SpecialFunctions/RationalRamp.lean | 253 ++++++++++++++++++ ComplexityTests/RationalRamp.lean | 65 +++++ 3 files changed, 319 insertions(+) create mode 100644 Complexity/Foundations/Analysis/SpecialFunctions/RationalRamp.lean create mode 100644 ComplexityTests/RationalRamp.lean diff --git a/Complexity.lean b/Complexity.lean index bccc4b1393..ed57380e4f 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2354,6 +2354,7 @@ public import Complexity.Foundations.Analysis.MarkovBrothersInequality public import Complexity.Foundations.Analysis.RootError public import Complexity.Foundations.Analysis.SpecialFunctions.Arccos public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch +public import Complexity.Foundations.Analysis.SpecialFunctions.RationalRamp public import Complexity.Foundations.Analysis.SpecialFunctions.SmoothSwitch public import Complexity.Foundations.BooleanAnalysis.Bernoulli public import Complexity.Foundations.BooleanAnalysis.Bonami diff --git a/Complexity/Foundations/Analysis/SpecialFunctions/RationalRamp.lean b/Complexity/Foundations/Analysis/SpecialFunctions/RationalRamp.lean new file mode 100644 index 0000000000..f4b694acae --- /dev/null +++ b/Complexity/Foundations/Analysis/SpecialFunctions/RationalRamp.lean @@ -0,0 +1,253 @@ +/- +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.Init +public import Mathlib.Basic.Real.Basic +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +public import Mathlib.Topology.MetricSpace.Lipschitz +import Mathlib.Analysis.Calculus.Deriv.MeanValue +import Mathlib.Analysis.Calculus.Deriv.Pow +import Mathlib.Analysis.Calculus.MeanValue +import Mathlib.Analysis.Normed.MulAction +import Mathlib.Analysis.SpecialFunctions.Pow.Deriv +import Mathlib.Data.Rat.Cast.Order +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# A rational correction ramp with Lipschitz fourth root + +For `a > 0`, put `u = max 0 ((t - θ) / a)` and `Q t = a * u^4 / (1 + u)^3`. +This gives a monotone, one-Lipschitz correction ramp with +`t - (θ + 3a) ≤ Q t ≤ max (t - θ) 0`. Its fourth root is globally Lipschitz. +The definitions specialize to exact rational arithmetic; this is not a machine-space bound. + +This is an alternative rational witness for the ramp conditions in +[OpenAI2026LogSpace, Section 4.1, (4.2)], adapted to the fourth-moment workstream of complexitylib +issue #1721. The pinned preprint requires eighth-root regularity and gives a piecewise-polynomial +example; this module proves fourth-root regularity for the displayed rational construction. + +## Main definitions + +* `Cslib.rationalRamp4Unit`: the normalized ramp, zero on nonpositive inputs. +* `Cslib.rationalRamp4`: translation and rescaling of the normalized ramp. + +## Main results + +* `Cslib.rationalRamp4_nonneg`, `Cslib.rationalRamp4_le`, `Cslib.le_rationalRamp4`: ramp bounds. +* `Cslib.monotone_rationalRamp4`, `Cslib.lipschitzWith_rationalRamp4`: monotonicity and Lipschitz + constant one. +* `Cslib.lipschitzWith_rationalRamp4_root`: global fourth-root regularity. +* `Cslib.rationalRamp4_ratCast`: compatibility with exact rational evaluation. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 4.1 (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib + +open scoped NNReal + +/-- The normalized rational ramp, with fourth-order vanishing at zero. -/ +@[expose] def rationalRamp4Unit {R : Type*} [Field R] [LinearOrder R] (t : R) : R := + (max 0 t) ^ 4 / (1 + max 0 t) ^ 3 + +/-- A rational correction ramp with lower support threshold `θ` and width parameter `a`. +The analytic ramp laws assume `0 < a`. -/ +@[expose] def rationalRamp4 {R : Type*} [Field R] [LinearOrder R] (θ a t : R) : R := + a * rationalRamp4Unit ((t - θ) / a) + +private theorem core_hasDerivAt {t : ℝ} (ht : 0 ≤ t) : + HasDerivAt (fun t : ℝ => t ^ 4 / (1 + t) ^ 3) + (t ^ 3 * (t + 4) / (1 + t) ^ 4) t := by + have hp : 0 < 1 + t := by positivity + convert (hasDerivAt_pow 4 t).div (((hasDerivAt_id t).const_add 1).pow 3) + (pow_ne_zero _ hp.ne') using 1 + · rfl + · simp only [Pi.pow_apply, id_eq] + field_simp + ring + +private theorem core_deriv_nonneg {t : ℝ} (ht : 0 ≤ t) : + 0 ≤ t ^ 3 * (t + 4) / (1 + t) ^ 4 := by positivity + +private theorem core_deriv_le_one {t : ℝ} (ht : 0 ≤ t) : + t ^ 3 * (t + 4) / (1 + t) ^ 4 ≤ 1 := by + apply (div_le_one (by positivity : 0 < (1 + t) ^ 4)).2 + nlinarith [sq_nonneg t] + +private theorem core_monotoneOn : + MonotoneOn (fun t : ℝ => t ^ 4 / (1 + t) ^ 3) (Set.Ici 0) := by + refine monotoneOn_of_hasDerivWithinAt_nonneg (convex_Ici 0) + (fun t ht => (core_hasDerivAt ht).continuousAt.continuousWithinAt) + (fun t ht => (core_hasDerivAt (interior_subset ht)).hasDerivWithinAt) ?_ + exact fun t ht => core_deriv_nonneg (interior_subset ht) + +private theorem core_lipschitzOnWith : + LipschitzOnWith 1 (fun t : ℝ => t ^ 4 / (1 + t) ^ 3) (Set.Ici 0) := by + refine (convex_Ici 0).lipschitzOnWith_of_nnnorm_hasDerivWithin_le + (fun t ht => (core_hasDerivAt ht).hasDerivWithinAt) ?_ + intro t ht + change |t ^ 3 * (t + 4) / (1 + t) ^ 4| ≤ (1 : ℝ) + rw [abs_of_nonneg (core_deriv_nonneg ht)] + exact core_deriv_le_one ht + +theorem rationalRamp4Unit_nonneg (t : ℝ) : 0 ≤ rationalRamp4Unit t := by + unfold rationalRamp4Unit + positivity + +theorem rationalRamp4Unit_le (t : ℝ) : rationalRamp4Unit t ≤ max 0 t := by + have hu : 0 ≤ max 0 t := le_max_left _ _ + have hpow : 0 ≤ (max 0 t) ^ 3 := by positivity + apply (div_le_iff₀ (by positivity : 0 < (1 + max 0 t) ^ 3)).2 + nlinarith [sq_nonneg (max 0 t)] + +theorem sub_three_le_rationalRamp4Unit (t : ℝ) : t - 3 ≤ rationalRamp4Unit t := by + have hu : 0 ≤ max 0 t := le_max_left _ _ + apply (le_div_iff₀ (by positivity : 0 < (1 + max 0 t) ^ 3)).2 + have h := mul_le_mul_of_nonneg_right (sub_le_sub_right (le_max_right 0 t) 3) + (show 0 ≤ (1 + max 0 t) ^ 3 by positivity) + nlinarith [sq_nonneg (max 0 t)] + +theorem rationalRamp4Unit_of_nonpos {t : ℝ} (ht : t ≤ 0) : rationalRamp4Unit t = 0 := by + simp [rationalRamp4Unit, max_eq_left ht] + +theorem monotone_rationalRamp4Unit : Monotone (rationalRamp4Unit : ℝ → ℝ) := + fun _ _ h => core_monotoneOn (le_max_left _ _) (le_max_left _ _) (max_le_max le_rfl h) + +theorem lipschitzWith_rationalRamp4Unit : LipschitzWith 1 (rationalRamp4Unit : ℝ → ℝ) := by + refine LipschitzWith.of_dist_le_mul fun x y => ?_ + have h := core_lipschitzOnWith.dist_le_mul (max 0 x) (le_max_left _ _) + (max 0 y) (le_max_left _ _) + simp only [NNReal.coe_one, one_mul] at h + have hc := (LipschitzWith.id.const_max (0 : ℝ)).dist_le_mul x y + exact h.trans hc + +/-! ## Fourth roots -/ + +private theorem core_root_eq {t : ℝ} (ht : 0 ≤ t) : + (t ^ 4 / (1 + t) ^ 3) ^ (4⁻¹ : ℝ) = t * (1 + t) ^ (-(3 / 4 : ℝ)) := by + have hfour : (t ^ 4) ^ (4⁻¹ : ℝ) = t := by + convert Real.pow_rpow_inv_natCast ht (by norm_num : (4 : ℕ) ≠ 0) using 1 + rw [Real.div_rpow (by positivity) (by positivity), hfour, + ← Real.rpow_natCast_mul (by positivity), Real.rpow_neg (by positivity), div_eq_mul_inv] + norm_num + +private theorem root_hasDerivAt {t : ℝ} (ht : 0 ≤ t) : + HasDerivAt (fun t : ℝ => t * (1 + t) ^ (-(3 / 4 : ℝ))) + ((1 + t) ^ (-(7 / 4 : ℝ)) * (1 + t / 4)) t := by + have hp : 0 < 1 + t := by positivity + have he : (1 + t) ^ (-(3 / 4 : ℝ)) = (1 + t) ^ (-(7 / 4 : ℝ)) * (1 + t) := by + rw [← Real.rpow_add_one hp.ne'] + norm_num + convert (hasDerivAt_id t).mul (((hasDerivAt_id t).const_add 1).rpow_const + (p := -(3 / 4 : ℝ)) (Or.inl hp.ne')) + using 1 + · rfl + · simp only [id_eq, one_mul] + rw [he] + norm_num + ring + +private theorem root_deriv_nonneg {t : ℝ} (ht : 0 ≤ t) : + 0 ≤ (1 + t) ^ (-(7 / 4 : ℝ)) * (1 + t / 4) := by positivity + +private theorem root_deriv_le_one {t : ℝ} (ht : 0 ≤ t) : + (1 + t) ^ (-(7 / 4 : ℝ)) * (1 + t / 4) ≤ 1 := by + have hp : 0 < 1 + t := by positivity + calc (1 + t) ^ (-(7 / 4 : ℝ)) * (1 + t / 4) ≤ + (1 + t) ^ (-(7 / 4 : ℝ)) * (1 + t) := + mul_le_mul_of_nonneg_left (by linarith) (Real.rpow_nonneg hp.le _) + _ = (1 + t) ^ (-(3 / 4 : ℝ)) := by rw [← Real.rpow_add_one hp.ne']; norm_num + _ ≤ 1 := Real.rpow_le_one_of_one_le_of_nonpos (by linarith) (by norm_num) + +private theorem root_lipschitzOnWith : + LipschitzOnWith 1 (fun t : ℝ => t * (1 + t) ^ (-(3 / 4 : ℝ))) (Set.Ici 0) := by + refine (convex_Ici 0).lipschitzOnWith_of_nnnorm_hasDerivWithin_le + (fun t ht => (root_hasDerivAt ht).hasDerivWithinAt) ?_ + intro t ht + change |(1 + t) ^ (-(7 / 4 : ℝ)) * (1 + t / 4)| ≤ (1 : ℝ) + rw [abs_of_nonneg (root_deriv_nonneg ht)] + exact root_deriv_le_one ht + +/-- The normalized ramp's fourth root has global Lipschitz constant one. -/ +theorem lipschitzWith_rationalRamp4Unit_root : + LipschitzWith 1 fun t : ℝ => rationalRamp4Unit t ^ (4⁻¹ : ℝ) := by + refine LipschitzWith.of_dist_le_mul fun x y => ?_ + have h := root_lipschitzOnWith.dist_le_mul (max 0 x) (le_max_left _ _) + (max 0 y) (le_max_left _ _) + rw [← core_root_eq (le_max_left _ _), ← core_root_eq (le_max_left _ _)] at h + simp only [NNReal.coe_one, one_mul] at h + exact h.trans ((LipschitzWith.id.const_max (0 : ℝ)).dist_le_mul x y) + +/-! ## Translation and rescaling -/ + +variable {θ a t : ℝ} + +theorem rationalRamp4_nonneg (ha : 0 ≤ a) (θ t : ℝ) : 0 ≤ rationalRamp4 θ a t := + mul_nonneg ha (rationalRamp4Unit_nonneg _) + +theorem rationalRamp4_le (ha : 0 < a) (θ t : ℝ) : + rationalRamp4 θ a t ≤ max (t - θ) 0 := by + calc rationalRamp4 θ a t ≤ a * max 0 ((t - θ) / a) := + mul_le_mul_of_nonneg_left (rationalRamp4Unit_le _) ha.le + _ = max (t - θ) 0 := by + rw [mul_max_of_nonneg _ _ ha.le, mul_zero] + simp [mul_div_cancel₀, ha.ne', max_comm] + +theorem le_rationalRamp4 (ha : 0 < a) (θ t : ℝ) : + t - (θ + 3 * a) ≤ rationalRamp4 θ a t := by + calc t - (θ + 3 * a) = a * ((t - θ) / a - 3) := by field_simp; ring + _ ≤ rationalRamp4 θ a t := + mul_le_mul_of_nonneg_left (sub_three_le_rationalRamp4Unit _) ha.le + +theorem rationalRamp4_of_le (ha : 0 < a) (ht : t ≤ θ) : rationalRamp4 θ a t = 0 := by + rw [rationalRamp4, rationalRamp4Unit_of_nonpos (div_nonpos_of_nonpos_of_nonneg + (sub_nonpos.mpr ht) ha.le), mul_zero] + +theorem monotone_rationalRamp4 (ha : 0 < a) (θ : ℝ) : Monotone (rationalRamp4 θ a) := + fun _ _ h => mul_le_mul_of_nonneg_left (monotone_rationalRamp4Unit + (div_le_div_of_nonneg_right (sub_le_sub_right h θ) ha.le)) ha.le + +/-- The scale factor cancels the input rescaling, preserving Lipschitz constant one. -/ +theorem lipschitzWith_rationalRamp4 (ha : 0 < a) (θ : ℝ) : + LipschitzWith 1 (rationalRamp4 θ a) := by + change LipschitzWith 1 (fun t : ℝ => a * rationalRamp4Unit ((t - θ) / a)) + have h := (lipschitzWith_smul a).comp (lipschitzWith_rationalRamp4Unit.comp + ((lipschitzWith_smul a⁻¹).comp (isometry_add_right (-θ)).lipschitzWith)) + simpa only [mul_one, one_mul, ← nnnorm_mul, mul_inv_cancel₀ ha.ne', nnnorm_one, + Function.comp_def, smul_eq_mul, sub_eq_add_neg, div_eq_mul_inv, mul_comm] + using h + +/-- The rescaled ramp's fourth root is globally Lipschitz, including arbitrarily large inputs. -/ +theorem lipschitzWith_rationalRamp4_root (ha : 0 < a) (θ : ℝ) : + LipschitzWith (‖a ^ (4⁻¹ : ℝ)‖₊ * ‖a⁻¹‖₊) + fun t : ℝ => rationalRamp4 θ a t ^ (4⁻¹ : ℝ) := by + have h := (lipschitzWith_smul (a ^ (4⁻¹ : ℝ))).comp (lipschitzWith_rationalRamp4Unit_root.comp + ((lipschitzWith_smul a⁻¹).comp (isometry_add_right (-θ)).lipschitzWith)) + simpa only [mul_one, one_mul, rationalRamp4, Real.mul_rpow ha.le (rationalRamp4Unit_nonneg _), + Function.comp_def, smul_eq_mul, sub_eq_add_neg, div_eq_mul_inv, mul_comm] using h + +@[simp, norm_cast] +theorem rationalRamp4Unit_ratCast (t : ℚ) : + rationalRamp4Unit (t : ℝ) = (rationalRamp4Unit t : ℚ) := by + simp [rationalRamp4Unit, Rat.cast_max] + +@[simp, norm_cast] +theorem rationalRamp4_ratCast (θ a t : ℚ) : + rationalRamp4 (θ : ℝ) a t = (rationalRamp4 θ a t : ℚ) := by + simp only [rationalRamp4, Rat.cast_mul, ← rationalRamp4Unit_ratCast, Rat.cast_div, Rat.cast_sub] + +end Cslib diff --git a/ComplexityTests/RationalRamp.lean b/ComplexityTests/RationalRamp.lean new file mode 100644 index 0000000000..f3cc6d5a2a --- /dev/null +++ b/ComplexityTests/RationalRamp.lean @@ -0,0 +1,65 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ +import Complexity.Foundations.Analysis.SpecialFunctions.RationalRamp +import Mathlib.Tactic.NormNum + +/-! +# Tests for the rational correction ramp + +Exact rational evaluations exercise the transition and large inputs. The real examples use the +proved defect, one-Lipschitz bound and the nontrivial fourth-root rescaling constant. +-/ + +namespace ComplexityTests.RationalRamp + +open Cslib + +example : rationalRamp4Unit (1 : ℚ) = 1 / 8 := by + norm_num [rationalRamp4Unit] + +example : rationalRamp4Unit (10 : ℚ) = 10000 / 1331 := by + norm_num [rationalRamp4Unit] + +example : rationalRamp4 (1 : ℚ) 2 9 = 512 / 125 := by + norm_num [rationalRamp4, rationalRamp4Unit] + +example : rationalRamp4 (1 : ℚ) 2 (-5) = 0 ∧ rationalRamp4 (1 : ℚ) 2 1 = 0 := by + norm_num [rationalRamp4, rationalRamp4Unit] + +example : rationalRamp4 (1 : ℝ) 2 9 = 512 / 125 := by + have h : rationalRamp4 (1 : ℚ) 2 9 = 512 / 125 := by + norm_num [rationalRamp4, rationalRamp4Unit] + have hc := rationalRamp4_ratCast (1 : ℚ) 2 9 + rw [h] at hc + norm_num at hc ⊢ + exact hc + +-- The upper and lower bounds are uniform on the whole real line. +example (t : ℝ) : t - 7 ≤ rationalRamp4 1 2 t ∧ rationalRamp4 1 2 t ≤ max (t - 1) 0 := by + constructor + · have h := le_rationalRamp4 (by norm_num : (0 : ℝ) < 2) 1 t + norm_num at h + exact (sub_le_iff_le_add).mpr h + · exact rationalRamp4_le (by norm_num) 1 t + +example (x y : ℝ) : |rationalRamp4 1 2 x - rationalRamp4 1 2 y| ≤ |x - y| := by + simpa only [Real.dist_eq, NNReal.coe_one, one_mul] using + (lipschitzWith_rationalRamp4 (by norm_num : (0 : ℝ) < 2) 1).dist_le_mul x y + +-- A width of `1/16` gives the explicit fourth-root Lipschitz constant `8`. +example (θ x y : ℝ) : + |rationalRamp4 θ (1 / 16) x ^ (4⁻¹ : ℝ) - + rationalRamp4 θ (1 / 16) y ^ (4⁻¹ : ℝ)| ≤ 8 * |x - y| := by + have h := (lipschitzWith_rationalRamp4_root (by norm_num : (0 : ℝ) < 1 / 16) θ).dist_le_mul x y + have hr : (1 / 16 : ℝ) ^ (4⁻¹ : ℝ) = 1 / 2 := by + rw [show (1 / 16 : ℝ) = (1 / 2) ^ 4 by norm_num] + convert Real.pow_rpow_inv_natCast (by norm_num : (0 : ℝ) ≤ 1 / 2) + (by norm_num : (4 : ℕ) ≠ 0) using 1 + rw [hr] at h + norm_num [Real.dist_eq] at h ⊢ + exact h + +end ComplexityTests.RationalRamp From 675c2e386388bec54ebfe559deb810ad320d05f2 Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:00:55 +0000 Subject: [PATCH 4/5] feat: construct hierarchy parameters with Lipschitz fourth roots Extend HierarchyParams with the strict core threshold ladder, a positive iteration count, strict copy-count inequality, monotone bounded cutoffs, row-gate closure, and root/complement regularity. Prove the strengthened bundle nonempty using an actual rational ramp and polynomial cutoffs. The construction chooses theta = 1/(128q), width 1/(384q), theta2 = 1/(64q), copy thresholds 1/(8q) and 1/(4q), then the factorial-tail iteration count, copies, and detector ranks in the primary source's dependency order. This advances #1721's fourth-moment hierarchy gap. It is an explicit s=4 adaptation of OpenAI2026LogSpace Sections 4.1-4.4 and Remark 4.6 at pinned revision 7ef5c0cc; the source uses s=8. It does not prove eighth-root regularity, every later atom/access-score margin, a recursive estimator, or a machine-space bound. Existing HierarchyParams APIs are unchanged. Validation atop d3d62d9f: new module and focused tests compile with pinned Lean and repository options, warnings as errors, using private outputs and read-only dependencies. Tests extract actual witnesses at q=2, prove nonzero ramp and exact plateau values, use row-root perturbation at its closed endpoint, and feed the underlying parameters into the existing stage API for a nonzero two-vertex matrix. Focused hygiene --check-simp and diffcheck pass. No aggregate or existing source file was modified. Independent review and full integration gates remain for the coordinator. Authored by worker codex-logspace-polynomial-cutoffs-20261030 with ChatGPT. Independent agent source/API review: codex-compression-iteration-20261030 approved c7ac6dea11574e721ded46aeb0f76c2ccaf79df9 and independently compiled both files. Publication preserves the reviewed source/tests and adds only generated import registration. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 1 + .../FourthRootHierarchyParams.lean | 261 ++++++++++++++++++ .../FourthRootHierarchyParams.lean | 76 +++++ 3 files changed, 338 insertions(+) create mode 100644 Complexity/Foundations/Probability/FourthRootHierarchyParams.lean create mode 100644 ComplexityTests/FourthRootHierarchyParams.lean diff --git a/Complexity.lean b/Complexity.lean index ed57380e4f..2fe378be1b 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2729,6 +2729,7 @@ public import Complexity.Foundations.Probability.ColumnDetector public import Complexity.Foundations.Probability.CorrectionAtom public import Complexity.Foundations.Probability.DetectedHierarchy public import Complexity.Foundations.Probability.DetectedStage +public import Complexity.Foundations.Probability.FourthRootHierarchyParams public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real public import Complexity.Foundations.Probability.Gaussian.Sheppard diff --git a/Complexity/Foundations/Probability/FourthRootHierarchyParams.lean b/Complexity/Foundations/Probability/FourthRootHierarchyParams.lean new file mode 100644 index 0000000000..0f61df732c --- /dev/null +++ b/Complexity/Foundations/Probability/FourthRootHierarchyParams.lean @@ -0,0 +1,261 @@ +/- +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.HierarchyParams +public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch +public import Complexity.Foundations.Analysis.SpecialFunctions.RationalRamp +import Mathlib.Algebra.Order.Floor.Semiring +import Mathlib.Tactic.FieldSimp +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Concrete hierarchy parameters with Lipschitz fourth roots + +This module supplies an actual regular witness extending `Matrix.HierarchyParams`. Its correction +ramp is rational, its five bounded cutoffs are polynomial switches, and all required fourth roots +and complementary fourth roots are globally Lipschitz. The strict threshold ladder is +`0 < θ < θ₂ < 1/(32q)`, `0 < δ₀ < δ₁ < θ/100`, and +`0 < η < η₂ < δ₀/3`, with copy thresholds `1/(8q)` and `1/(4q)`. + +The construction fixes `θ = 1/(128q)` and width `a = 1/(384q)`, giving +`θ₂ = θ + 3a = 1/(64q)` for the rational ramp. It then chooses a positive iteration count from +the factorial tail, the number of copies, and the detector ranks, in that order. Thus the +existence theorem proves the new conditions; they are not extra premises on an unspecified stage. +The underlying `HierarchyParams` can be passed directly to all existing stage theorems. + +This is the fourth-moment adaptation in complexitylib issue #1721 of the core hierarchy +conditions in [OpenAI2026LogSpace, Sections 4.1--4.4]. The pinned preprint uses eighth roots. +The witness does not establish eighth-root regularity, every later atom/access-score margin, +the recursive estimator, or rational-machine resource bounds. When `q` is rational, the displayed +scalar functions use only rational arithmetic and min/max; selecting the iteration count and +integer ranks here is an existence argument. + +## Main definitions + +* `Matrix.FourthRootHierarchyParams`: reduced algebraic-stage data together with the strict + core threshold ladder, monotone cutoffs, and fourth-root regularity. + +## Main results + +* `Matrix.FourthRootHierarchyParams.nonempty`: a concrete regular witness exists for `q > 0` + and `cπ > 0`. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Sections 4.1--4.4 and Remark 4.6 (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Matrix + +open Cslib + +/-- Concrete regularity requirements for the fourth-moment hierarchy, extending the existing +algebraic-stage interface. The core threshold ladder is included, but later access-score margins +are not asserted by this structure. -/ +structure FourthRootHierarchyParams (q cπ Cπ Cpair Cvar : ℝ) + extends HierarchyParams q cπ Cπ Cpair Cvar where + /-- Upper support threshold of the row gate. -/ + η₂ : ℝ + θ_lt_θ₂ : θ < θ₂ + θ₂_lt : θ₂ < 1 / (32 * q) + k_pos : 0 < k + tail_small : Real.exp (1 / θ) * (L / θ) ^ k / k.factorial ≤ 1 / (32 * q) + copies_strict : q * ((k : ℝ) + 1) < m + 1 + τ₀_eq : τ₀ = 1 / (8 * q) + τ₁_eq : τ₁ = 1 / (4 * q) + δ₀_lt_δ₁ : δ₀ < δ₁ + δ₁_lt : δ₁ < θ / 100 + η_lt_η₂ : η < η₂ + η₂_lt : η₂ < δ₀ / 3 + χ_mono : Monotone χ + ϕ_mono : Monotone ϕ + ρ_nonneg : ∀ t, 0 ≤ ρ t + ρ_antitone : Antitone ρ + ρ_zero : ∀ t, η₂ ≤ t → ρ t = 0 + κ_mono : Monotone κ + κ_one_ge : ∀ t, 1 / 2 ≤ t → κ t = 1 + Q_root : ∃ K, LipschitzWith K fun t => Q t ^ (4⁻¹ : ℝ) + cutoff_roots : ∀ F ∈ [χ, ϕ, ρ, γ, κ], + (∃ K, LipschitzWith K fun t => F t ^ (4⁻¹ : ℝ)) ∧ + (∃ K, LipschitzWith K fun t => (1 - F t) ^ (4⁻¹ : ℝ)) + +namespace FourthRootHierarchyParams + +variable {q cπ Cπ Cpair Cvar : ℝ} + +/-- A concrete hierarchy witness with a rational ramp, polynomial cutoffs, the strict core +threshold ladder, and global fourth-root regularity. -/ +theorem nonempty (hq : 0 < q) (hcπ : 0 < cπ) : + Nonempty (FourthRootHierarchyParams q cπ Cπ Cpair Cvar) := by + set θ : ℝ := 1 / (128 * q) + set a : ℝ := 1 / (384 * q) + set θ₂ : ℝ := θ + 3 * a + have hθ : 0 < θ := by positivity + have ha : 0 < a := by positivity + have hθ₂ : θ₂ = 1 / (64 * q) := by + dsimp [θ₂, θ, a] + field_simp + ring + have hθ₂small : θ₂ < 1 / (32 * q) := by + rw [hθ₂, div_lt_div_iff_of_pos_left one_pos (by positivity) (by positivity)] + linarith + have hτ : 1 / (8 * q) < 1 / (4 * q) := by + rw [div_lt_div_iff_of_pos_left one_pos (by positivity) (by positivity)] + linarith + have hτ₁ : 1 / (4 * q) ≤ 1 / q := by + rw [div_le_div_iff_of_pos_left one_pos (by positivity) hq] + linarith + set δ₀ : ℝ := θ / 400 + set δ₁ : ℝ := θ / 200 + set η : ℝ := δ₀ / 1000 + set η₂ : ℝ := δ₀ / 500 + have hδ₀ : 0 < δ₀ := by positivity + have hδ : δ₀ < δ₁ := by dsimp [δ₀, δ₁]; linarith + have hη : 0 < η := by positivity + have hη₂ : η < η₂ := by dsimp [η, η₂]; linarith + obtain ⟨k, hk⟩ := exists_factorial_bound_le θ 1 + (δ := min (1 / (32 * q)) (Real.exp (1 / θ) / 2)) (by positivity) + have htail : Real.exp (1 / θ) * (1 / θ) ^ k / k.factorial ≤ 1 / (32 * q) := + hk.trans (min_le_left _ _) + have hkpos : 0 < k := by + by_contra h + have hzero : k = 0 := Nat.eq_zero_of_not_pos h + have hb := hk.trans (min_le_right _ _) + simp only [hzero, pow_zero, Nat.factorial_zero, Nat.cast_one, mul_one, div_one] at hb + linarith [Real.exp_pos (1 / θ)] + set m : ℕ := ⌈q⌉₊ * (k + 1) + have hcopies : q * ((k : ℝ) + 1) < (m : ℝ) + 1 := by + have hqc : q ≤ ⌈q⌉₊ := Nat.le_ceil q + have hm : (m : ℝ) = ⌈q⌉₊ * ((k : ℝ) + 1) := by simp [m] + rw [hm] + nlinarith [(Nat.cast_nonneg (α := ℝ) k)] + set J : ℕ := ⌈(2 * Cπ * m * k * (k + 1)) / δ₀⌉₊ + 1 + set K : ℕ := ⌈160 * (1 + Cpair * k / η)⌉₊ + set R : ℝ := (4 * J + 40 * |Cvar|) / cπ + have hR : 4 * (J : ℝ) + 40 * |Cvar| ≤ cπ * R := by + dsimp [R] + rw [mul_div_cancel₀ _ hcπ.ne'] + have hγ : (1 / 2 : ℝ) < 4 / 5 := by norm_num + have hκ : (1 / 4 : ℝ) < 1 / 2 := by norm_num + refine ⟨{ + Q := rationalRamp4 θ a + θ := θ + θ₂ := θ₂ + L := 1 + k := k + m := m + τ₀ := 1 / (8 * q) + τ₁ := 1 / (4 * q) + χ := polynomialSwitch4 (1 / (8 * q)) (1 / (4 * q)) + δ₀ := δ₀ + δ₁ := δ₁ + ϕ := polynomialSwitch4 δ₀ δ₁ + η := η + ρ := fun t => 1 - polynomialSwitch4 η η₂ t + γ := fun t => 1 - polynomialSwitch4 (1 / 2) (4 / 5) t + κ := polynomialSwitch4 (1 / 4) (1 / 2) + J := J + K := K + R := R + Q_nonneg := rationalRamp4_nonneg ha.le θ + Q_le := rationalRamp4_le ha θ + le_Q := le_rationalRamp4 ha θ + Q_mono := monotone_rationalRamp4 ha θ + Q_lipschitz := fun s t hst => ?_ + θ_pos := hθ + L_nonneg := zero_le_one + truncation := ?_ + χ_nonneg := polynomialSwitch4_nonneg _ _ + χ_le_one := polynomialSwitch4_le_one _ _ + χ_zero := fun _ h => polynomialSwitch4_of_le hτ h + χ_one := fun _ h => polynomialSwitch4_of_ge hτ h + τ₁_le := hτ₁ + copies := ?_ + δ₀_pos := hδ₀ + ϕ_nonneg := polynomialSwitch4_nonneg _ _ + ϕ_le_one := polynomialSwitch4_le_one _ _ + ϕ_zero := fun _ h => polynomialSwitch4_of_le hδ h + ϕ_one := fun _ h => polynomialSwitch4_of_ge hδ h + η_pos := hη + ρ_le_one := fun t => sub_le_self _ (polynomialSwitch4_nonneg _ _ t) + ρ_one := fun t h => by rw [polynomialSwitch4_of_le hη₂ h, sub_zero] + γ_nonneg := fun t => sub_nonneg.mpr (polynomialSwitch4_le_one _ _ t) + γ_le_one := fun t => sub_le_self _ (polynomialSwitch4_nonneg _ _ t) + γ_antitone := fun _ _ h => sub_le_sub_left (monotone_polynomialSwitch4 hγ.le h) 1 + γ_one := fun t h => by rw [polynomialSwitch4_of_le hγ h, sub_zero] + γ_zero := fun t h => by rw [polynomialSwitch4_of_ge hγ h, sub_self] + κ_nonneg := polynomialSwitch4_nonneg _ _ + κ_le_one := polynomialSwitch4_le_one _ _ + κ_zero := fun _ h => polynomialSwitch4_of_le hκ h + κ_one := fun _ h => polynomialSwitch4_of_ge hκ h.le + J_pos := Nat.succ_pos _ + rank := ?_ + gate := Nat.le_ceil _ + R_rank := by linarith [abs_nonneg Cvar] + R_var := by linarith [le_abs_self Cvar] + η₂ := η₂ + θ_lt_θ₂ := by dsimp [θ₂]; linarith + θ₂_lt := hθ₂small + k_pos := hkpos + tail_small := htail + copies_strict := hcopies + τ₀_eq := rfl + τ₁_eq := rfl + δ₀_lt_δ₁ := hδ + δ₁_lt := by dsimp [δ₁]; linarith + η_lt_η₂ := hη₂ + η₂_lt := by dsimp [η₂]; linarith + χ_mono := monotone_polynomialSwitch4 hτ.le + ϕ_mono := monotone_polynomialSwitch4 hδ.le + ρ_nonneg := fun t => sub_nonneg.mpr (polynomialSwitch4_le_one _ _ t) + ρ_antitone := fun _ _ h => sub_le_sub_left (monotone_polynomialSwitch4 hη₂.le h) 1 + ρ_zero := fun t h => by rw [polynomialSwitch4_of_ge hη₂ h, sub_self] + κ_mono := monotone_polynomialSwitch4 hκ.le + κ_one_ge := fun _ h => polynomialSwitch4_of_ge hκ h + Q_root := ⟨_, lipschitzWith_rationalRamp4_root ha θ⟩ + cutoff_roots := ?_ }⟩ + · have h := (lipschitzWith_rationalRamp4 ha θ).dist_le_mul t s + rw [Real.dist_eq, Real.dist_eq, abs_of_nonneg (sub_nonneg.mpr hst)] at h + exact (le_abs_self _).trans h + · calc θ₂ + Real.exp (1 / θ) * (1 / θ) ^ k / k.factorial ≤ θ₂ + 1 / (32 * q) := by + linarith + _ = (3 / 64) / q := by rw [hθ₂]; field_simp; ring + _ ≤ (1 / 8) / q := div_le_div_of_nonneg_right (by norm_num) hq.le + _ = 1 / (8 * q) := by ring + · rw [div_le_div_iff₀ (by positivity) hq, one_mul] + simpa only [mul_comm] using hcopies.le + · have hJ : (2 * Cπ * m * k * (k + 1)) / δ₀ ≤ (J : ℝ) := by + dsimp [J] + push_cast + exact (Nat.le_ceil _).trans (by linarith) + have hb := (div_le_iff₀ hδ₀).mp hJ + linarith + · intro F hF + simp only [List.mem_cons, List.not_mem_nil, or_false] at hF + rcases hF with rfl | rfl | rfl | rfl | rfl + · exact ⟨exists_lipschitzWith_polynomialSwitch4_root _ _, + exists_lipschitzWith_one_sub_polynomialSwitch4_root _ _⟩ + · exact ⟨exists_lipschitzWith_polynomialSwitch4_root _ _, + exists_lipschitzWith_one_sub_polynomialSwitch4_root _ _⟩ + · refine ⟨exists_lipschitzWith_one_sub_polynomialSwitch4_root _ _, ?_⟩ + simpa only [sub_sub_cancel] using exists_lipschitzWith_polynomialSwitch4_root η η₂ + · refine ⟨exists_lipschitzWith_one_sub_polynomialSwitch4_root _ _, ?_⟩ + simpa only [sub_sub_cancel] using + exists_lipschitzWith_polynomialSwitch4_root (1 / 2) (4 / 5) + · exact ⟨exists_lipschitzWith_polynomialSwitch4_root _ _, + exists_lipschitzWith_one_sub_polynomialSwitch4_root _ _⟩ + +end FourthRootHierarchyParams + +end Matrix diff --git a/ComplexityTests/FourthRootHierarchyParams.lean b/ComplexityTests/FourthRootHierarchyParams.lean new file mode 100644 index 0000000000..83fddc6c0b --- /dev/null +++ b/ComplexityTests/FourthRootHierarchyParams.lean @@ -0,0 +1,76 @@ +/- +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.FourthRootHierarchyParams +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.FinCases +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum + +/-! +# Tests for the regular fourth-moment hierarchy witness + +The examples use the concrete existence construction at `q = 2`, derive nonzero ramp and exact +plateau values, use complementary root regularity at a closed row gate, and pass the strengthened +parameters into the existing stage API on a nonzero two-vertex transition matrix. +-/ + +namespace ComplexityTests.FourthRootHierarchyParams + +open Matrix +open scoped NNReal + +-- The actual witness has zero correction below its threshold, unbounded correction above it, +-- and the prescribed copy/row plateaus. These values use no extra cutoff assumptions. +example : ∃ P : FourthRootHierarchyParams 2 1 1 1 0, + P.Q 0 = 0 ∧ 1 ≤ P.Q (P.θ₂ + 1) ∧ P.χ (1 / 16) = 0 ∧ P.χ (1 / 8) = 1 ∧ + P.ρ P.η₂ = 0 ∧ P.κ (1 / 2) = 1 := by + obtain ⟨P⟩ := FourthRootHierarchyParams.nonempty (q := 2) (cπ := 1) (Cπ := 1) + (Cpair := 1) (Cvar := 0) (by norm_num) (by norm_num) + refine ⟨P, ?_, ?_, ?_, ?_, P.ρ_zero _ le_rfl, P.κ_one_ge _ le_rfl⟩ + · apply le_antisymm _ (P.Q_nonneg 0) + simpa only [max_eq_right (by linarith [P.θ_pos] : (0 : ℝ) - P.θ ≤ 0)] using P.Q_le 0 + · have h := P.le_Q (P.θ₂ + 1) + linarith + · apply P.χ_zero + rw [P.τ₀_eq] + norm_num + · apply P.χ_one + rw [P.τ₁_eq] + norm_num + +-- The row gate closes strictly before the detector entry factor can become nonzero. +example (P : FourthRootHierarchyParams 2 1 1 1 0) : + 3 * P.η₂ < P.δ₀ ∧ P.ϕ (3 * P.η₂) = 0 := by + have h : 3 * P.η₂ < P.δ₀ := by linarith [P.η₂_lt] + exact ⟨h, P.ϕ_zero _ h.le⟩ + +-- Root regularity gives a perturbation bound at the closed endpoint of the actual row gate. +example (P : FourthRootHierarchyParams 2 1 1 1 0) : + ∃ K : ℝ≥0, ∀ t : ℝ, |P.ρ t ^ (4⁻¹ : ℝ)| ≤ K * |t - P.η₂| := by + obtain ⟨K, hK⟩ := (P.cutoff_roots P.ρ (by simp)).1 + refine ⟨K, fun t => ?_⟩ + have h := hK.dist_le_mul t P.η₂ + rw [P.ρ_zero _ le_rfl, Real.zero_rpow (by norm_num : (4⁻¹ : ℝ) ≠ 0)] at h + simpa only [Real.dist_eq, sub_zero] using h + +/-- One edge of weight `1/2` on two vertices. -/ +private noncomputable def C : Matrix (Fin 2) (Fin 2) ℝ := !![0, 1 / 2; 0, 0] + +-- Existing stage theorems consume the parent interface directly: the constructed cutoffs give +-- a nonnegative and substochastic next transition on the copied vertices of this nonzero input. +example : ∃ P : FourthRootHierarchyParams 2 1 1 1 0, + let X : Unit → Fin 2 → Prop := fun _ _ => True + let A := P.toHierarchyParams.next X X 1 C + (∀ x y, 0 ≤ A x y) ∧ A *ᵥ 1 ≤ 1 := by + obtain ⟨P⟩ := FourthRootHierarchyParams.nonempty (q := 2) (cπ := 1) (Cπ := 1) + (Cpair := 1) (Cvar := 0) (by norm_num) (by norm_num) + have hC : ∀ x y, 0 ≤ C x y := by intro x y; fin_cases x <;> fin_cases y <;> norm_num [C] + have hC1 : C *ᵥ 1 ≤ 1 := by intro x; fin_cases x <;> norm_num [C, mulVec, dotProduct] + refine ⟨P, ?_, ?_⟩ + · exact P.toHierarchyParams.next_nonneg (by norm_num) hC + · exact P.toHierarchyParams.next_mulVec_one_le (by norm_num) hC hC1 + +end ComplexityTests.FourthRootHierarchyParams From d885c30f31306ac55c232f9811c3d240f4525d2a Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 16:30:11 +0000 Subject: [PATCH 5/5] feat(probability): construct polynomial atom cutoffs and row laws Define actual rational polynomial preparation, row-gate, auxiliary-score and broad-witness functions. Prove their range and closed threshold laws, flat rank regions, incoming-score compatibility, joint Lipschitz fourth roots, and exact rational-cast identities. Preserve the existing exponential AtomCutoffs API and Christian Reitwiessner's source credit. This is the fourth-moment adaptation for #1721 of the threshold template in OpenAI2026LogSpace (5.5), and the witness in the support-margin proof and compression-threshold table of Section 5.5, revision 7ef5c0cc. The source uses eighth roots; these degree-seven cutoffs only establish fourth-root regularity. The actual functions are proved regular, rather than an assumed regularity bundle. Normalized main outputs, access enumeration and machine-resource bounds remain separate. Validation: the new module and full focused test file compile without diagnostics with Lean 4.36.0-rc2 and repository strict options, using private outputs and read-only dependencies. Executable rational tests evaluate all three row functions to 1/4 with both switches in their transition regions. Further tests check signed inputs, closed endpoints and the witness's strict 82 > 3*27 margin, real/rational agreement, nonzero existing atomPrep and auxScore expressions on a concrete matrix, and nonconstant fourth-root variation. Focused --check-simp hygiene and staged diff checking pass. Independent review and full integration gates remain pending; aggregate regeneration belongs to the coordinator. AI assistance: implemented by worker /root/compression_review on feat/logspace-polynomial-atom-cutoffs, based on the reviewed hierarchy lane. The Stationary specialization will be a separate cross-lane change. Independent non-author source/API review by lean_environment approved exact source revision a4eae07bdd9993e038a83aea84cc3c4b31c794d9 against pinned atoms.tex, with no findings. Reviewed source files are unchanged. Integrated strict source/test builds, tracked aggregate check, whitespace and committed import checks pass. Full integration gates run in PR CI. --- Complexity.lean | 1 + .../Probability/PolynomialAtomCutoffs.lean | 294 ++++++++++++++++++ ComplexityTests/PolynomialAtomCutoffs.lean | 88 ++++++ 3 files changed, 383 insertions(+) create mode 100644 Complexity/Foundations/Probability/PolynomialAtomCutoffs.lean create mode 100644 ComplexityTests/PolynomialAtomCutoffs.lean diff --git a/Complexity.lean b/Complexity.lean index 2fe378be1b..9736efc521 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -2734,6 +2734,7 @@ public import Complexity.Foundations.Probability.Gaussian.Multivariate public import Complexity.Foundations.Probability.Gaussian.Real public import Complexity.Foundations.Probability.Gaussian.Sheppard public import Complexity.Foundations.Probability.HierarchyParams +public import Complexity.Foundations.Probability.PolynomialAtomCutoffs public import Complexity.Foundations.Probability.RootMetric public import Complexity.Foundations.Probability.SecondMoment public import Complexity.Foundations.Probability.StochasticAtom diff --git a/Complexity/Foundations/Probability/PolynomialAtomCutoffs.lean b/Complexity/Foundations/Probability/PolynomialAtomCutoffs.lean new file mode 100644 index 0000000000..52858c0ed9 --- /dev/null +++ b/Complexity/Foundations/Probability/PolynomialAtomCutoffs.lean @@ -0,0 +1,294 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Foundations.Analysis.SpecialFunctions.PolynomialSwitch +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.Positivity +import Mathlib.Tactic.Ring + +/-! +# Polynomial preparation, score, and witness cutoffs + +These are concrete polynomial versions of the atom threshold template in +[OpenAI2026LogSpace, (5.5)] and the broad witness in the proof of its support-margin lemma. +For a fixed support scale `θ > 0`, they define the preparation `hθ(v) Rθ(r)`, auxiliary score +`Iθ(v,r)`, and witness `Jθ(v,r)`. They take values in `[0,1]`, have globally Lipschitz fourth +roots jointly in the entry and rank, and use rational arithmetic when their inputs are rational. + +Their entry-zero and rank-closure thresholds `(e,g)` are respectively +`(θ/2, θ/500)`, `(θ/8, θ/50)`, and `(82θ/1000, 27θ/1000)`. Each has `3g < e`, including the +witness's strict margin `θ/1000`. All rank factors are one near zero. These are scalar laws for +the concrete row functions, suitable for the stationary-reference compression comparison. +The first argument is the full raw entry and the second is the prescribed full-row rank; +only function evaluation applies the switches' scalar clipping. + +This is the fourth-moment adaptation in complexitylib issue #1721. The pinned preprint uses +eighth roots. These polynomial cutoffs do not replace the existing exponential `AtomCutoffs` +API, which proves regularity for every positive power. Normalized main atom functions, access +enumeration, eighth-root regularity, and machine-resource bounds are separate obligations. + +## Main definitions + +* `Cslib.polynomialPrepCutoff4`, `Cslib.polynomialRowCutoff4`: the preparatory and row factors. +* `Cslib.polynomialPrepRow4`, `Cslib.polynomialAuxCutoff4`, `Cslib.polynomialWitnessCutoff4`: + the three concrete pre-incoming row functions. + +## Main results + +* The endpoint, rank-flatness, and range lemmas for each function. +* `Cslib.exists_abs_polynomialPrepRow4_root_sub_le`, + `Cslib.exists_abs_polynomialAuxCutoff4_root_sub_le`, + `Cslib.exists_abs_polynomialWitnessCutoff4_root_sub_le`: joint fourth-root bounds. +* The `*_ratCast` lemmas: exact compatibility with rational evaluation. + +## References + +* [OpenAI, *Exact Derandomization of Logarithmic Space: L = RL = BPL*][OpenAI2026LogSpace], + Section 5.1, (5.5), support-margin lemma and compression-threshold table in Section 5.5 + (23 September 2026, revision `7ef5c0cc`, not peer reviewed). +-/ + +public section + +namespace Cslib + +section Definitions + +variable {R : Type*} [Field R] [LinearOrder R] + +/-- The polynomial preparation factor with transition from `θ/2` to `3θ/4`. -/ +@[expose] def polynomialPrepCutoff4 (θ v : R) : R := + polynomialSwitch4 (θ / 2) (3 * θ / 4) v + +/-- The polynomial row gate, full through `θ/1000` and closed from `θ/500`. -/ +@[expose] def polynomialRowCutoff4 (θ r : R) : R := + 1 - polynomialSwitch4 (θ / 1000) (θ / 500) r + +/-- The actual unnormalized pre-incoming preparation `hθ(v) Rθ(r)`. -/ +@[expose] def polynomialPrepRow4 (θ v r : R) : R := + polynomialPrepCutoff4 θ v * polynomialRowCutoff4 θ r + +/-- The auxiliary score with the threshold intervals of [OpenAI2026LogSpace, (5.5)]. -/ +@[expose] def polynomialAuxCutoff4 (θ v r : R) : R := + polynomialSwitch4 (θ / 8) (θ / 4) v * + (1 - polynomialSwitch4 (θ / 100) (θ / 50) r) + +/-- The broad analytical witness `Jθ` of the support-margin lemma. Its support is not required +to have a further witness. -/ +@[expose] def polynomialWitnessCutoff4 (θ v r : R) : R := + polynomialSwitch4 (82 * θ / 1000) (90 * θ / 1000) v * + (1 - polynomialSwitch4 (26 * θ / 1000) (27 * θ / 1000) r) + +end Definitions + +variable {θ v r : ℝ} + +/-! ## Range and threshold laws -/ + +theorem polynomialPrepCutoff4_nonneg (θ v : ℝ) : 0 ≤ polynomialPrepCutoff4 θ v := + polynomialSwitch4_nonneg _ _ _ + +theorem polynomialPrepCutoff4_le_one (θ v : ℝ) : polynomialPrepCutoff4 θ v ≤ 1 := + polynomialSwitch4_le_one _ _ _ + +theorem polynomialPrepCutoff4_eq_zero (hθ : 0 < θ) (hv : v ≤ θ / 2) : + polynomialPrepCutoff4 θ v = 0 := polynomialSwitch4_of_le (by linarith) hv + +theorem polynomialPrepCutoff4_eq_one (hθ : 0 < θ) (hv : 3 * θ / 4 ≤ v) : + polynomialPrepCutoff4 θ v = 1 := polynomialSwitch4_of_ge (by linarith) hv + +theorem polynomialRowCutoff4_nonneg (θ r : ℝ) : 0 ≤ polynomialRowCutoff4 θ r := + sub_nonneg.mpr (polynomialSwitch4_le_one _ _ _) + +theorem polynomialRowCutoff4_le_one (θ r : ℝ) : polynomialRowCutoff4 θ r ≤ 1 := + sub_le_self _ (polynomialSwitch4_nonneg _ _ _) + +theorem polynomialRowCutoff4_eq_one (hθ : 0 < θ) (hr : r ≤ θ / 1000) : + polynomialRowCutoff4 θ r = 1 := by + rw [polynomialRowCutoff4, polynomialSwitch4_of_le (by linarith) hr, sub_zero] + +theorem polynomialRowCutoff4_eq_zero_iff (hθ : 0 < θ) : + polynomialRowCutoff4 θ r = 0 ↔ θ / 500 ≤ r := by + rw [polynomialRowCutoff4, sub_eq_zero, eq_comm, polynomialSwitch4_eq_one_iff (by linarith)] + +theorem polynomialRowCutoff4_eq_zero (hθ : 0 < θ) (hr : θ / 500 ≤ r) : + polynomialRowCutoff4 θ r = 0 := (polynomialRowCutoff4_eq_zero_iff hθ).mpr hr + +theorem polynomialPrepRow4_nonneg (θ v r : ℝ) : 0 ≤ polynomialPrepRow4 θ v r := + mul_nonneg (polynomialPrepCutoff4_nonneg _ _) (polynomialRowCutoff4_nonneg _ _) + +theorem polynomialPrepRow4_le_one (θ v r : ℝ) : polynomialPrepRow4 θ v r ≤ 1 := + (mul_le_of_le_one_right (polynomialPrepCutoff4_nonneg _ _) + (polynomialRowCutoff4_le_one _ _)).trans (polynomialPrepCutoff4_le_one _ _) + +theorem polynomialPrepRow4_eq_zero_of_entry_le (hθ : 0 < θ) (hv : v ≤ θ / 2) : + polynomialPrepRow4 θ v r = 0 := by + rw [polynomialPrepRow4, polynomialPrepCutoff4_eq_zero hθ hv, zero_mul] + +theorem polynomialPrepRow4_eq_zero_of_rank_ge (hθ : 0 < θ) (hr : θ / 500 ≤ r) : + polynomialPrepRow4 θ v r = 0 := by + rw [polynomialPrepRow4, polynomialRowCutoff4_eq_zero hθ hr, mul_zero] + +theorem polynomialPrepRow4_of_rank_le (hθ : 0 < θ) (hr : r ≤ θ / 1000) : + polynomialPrepRow4 θ v r = polynomialPrepCutoff4 θ v := by + rw [polynomialPrepRow4, polynomialRowCutoff4_eq_one hθ hr, mul_one] + +theorem polynomialAuxCutoff4_nonneg (θ v r : ℝ) : 0 ≤ polynomialAuxCutoff4 θ v r := + mul_nonneg (polynomialSwitch4_nonneg _ _ _) (sub_nonneg.mpr (polynomialSwitch4_le_one _ _ _)) + +theorem polynomialAuxCutoff4_le_one (θ v r : ℝ) : polynomialAuxCutoff4 θ v r ≤ 1 := + (mul_le_of_le_one_right (polynomialSwitch4_nonneg _ _ _) + (sub_le_self _ (polynomialSwitch4_nonneg _ _ _))).trans (polynomialSwitch4_le_one _ _ _) + +theorem polynomialAuxCutoff4_eq_zero_of_entry_le (hθ : 0 < θ) (hv : v ≤ θ / 8) : + polynomialAuxCutoff4 θ v r = 0 := by + rw [polynomialAuxCutoff4, polynomialSwitch4_of_le (by linarith) hv, zero_mul] + +theorem polynomialAuxCutoff4_eq_zero_of_rank_ge (hθ : 0 < θ) (hr : θ / 50 ≤ r) : + polynomialAuxCutoff4 θ v r = 0 := by + rw [polynomialAuxCutoff4, polynomialSwitch4_of_ge (by linarith) hr, sub_self, mul_zero] + +theorem polynomialAuxCutoff4_of_rank_le (hθ : 0 < θ) (hr : r ≤ θ / 100) : + polynomialAuxCutoff4 θ v r = polynomialSwitch4 (θ / 8) (θ / 4) v := by + rw [polynomialAuxCutoff4, polynomialSwitch4_of_le (by linarith) hr, sub_zero, mul_one] + +theorem polynomialAuxCutoff4_eq_one (hθ : 0 < θ) (hv : θ / 4 ≤ v) (hr : r ≤ θ / 100) : + polynomialAuxCutoff4 θ v r = 1 := by + rw [polynomialAuxCutoff4_of_rank_le hθ hr, polynomialSwitch4_of_ge (by linarith) hv] + +/-- On the support relevant to the incoming cap, the concrete auxiliary score is one. -/ +theorem polynomialAuxCutoff4_eq_one_of_rowCutoff_ne_zero (hθ : 0 < θ) (hv : θ / 4 ≤ v) + (hr : polynomialRowCutoff4 θ r ≠ 0) : polynomialAuxCutoff4 θ v r = 1 := by + have hsmall : r < θ / 500 := lt_of_not_ge fun h => hr (polynomialRowCutoff4_eq_zero hθ h) + exact polynomialAuxCutoff4_eq_one hθ hv (by linarith) + +theorem polynomialWitnessCutoff4_nonneg (θ v r : ℝ) : 0 ≤ polynomialWitnessCutoff4 θ v r := + mul_nonneg (polynomialSwitch4_nonneg _ _ _) (sub_nonneg.mpr (polynomialSwitch4_le_one _ _ _)) + +theorem polynomialWitnessCutoff4_le_one (θ v r : ℝ) : polynomialWitnessCutoff4 θ v r ≤ 1 := + (mul_le_of_le_one_right (polynomialSwitch4_nonneg _ _ _) + (sub_le_self _ (polynomialSwitch4_nonneg _ _ _))).trans (polynomialSwitch4_le_one _ _ _) + +theorem polynomialWitnessCutoff4_eq_zero_of_entry_le (hθ : 0 < θ) (hv : v ≤ 82 * θ / 1000) : + polynomialWitnessCutoff4 θ v r = 0 := by + rw [polynomialWitnessCutoff4, polynomialSwitch4_of_le (by linarith) hv, zero_mul] + +theorem polynomialWitnessCutoff4_eq_zero_of_rank_ge (hθ : 0 < θ) (hr : 27 * θ / 1000 ≤ r) : + polynomialWitnessCutoff4 θ v r = 0 := by + rw [polynomialWitnessCutoff4, polynomialSwitch4_of_ge (by linarith) hr, sub_self, mul_zero] + +theorem polynomialWitnessCutoff4_of_rank_le (hθ : 0 < θ) (hr : r ≤ 26 * θ / 1000) : + polynomialWitnessCutoff4 θ v r = polynomialSwitch4 (82 * θ / 1000) (90 * θ / 1000) v := by + rw [polynomialWitnessCutoff4, polynomialSwitch4_of_le (by linarith) hr, sub_zero, mul_one] + +theorem polynomialWitnessCutoff4_eq_one (hθ : 0 < θ) (hv : 90 * θ / 1000 ≤ v) + (hr : r ≤ 26 * θ / 1000) : polynomialWitnessCutoff4 θ v r = 1 := by + rw [polynomialWitnessCutoff4_of_rank_le hθ hr, polynomialSwitch4_of_ge (by linarith) hv] + +/-! ## Joint fourth-root regularity -/ + +private theorem exists_abs_switch_product_root_sub_le (α β γ δ : ℝ) : + ∃ C : ℝ, 0 ≤ C ∧ ∀ v r v' r', + |(polynomialSwitch4 α β v * (1 - polynomialSwitch4 γ δ r)) ^ (4⁻¹ : ℝ) - + (polynomialSwitch4 α β v' * (1 - polynomialSwitch4 γ δ r')) ^ (4⁻¹ : ℝ)| ≤ + C * (|v - v'| + |r - r'|) := by + obtain ⟨Ka, hKa⟩ := exists_lipschitzWith_polynomialSwitch4_root α β + obtain ⟨Kb, hKb⟩ := exists_lipschitzWith_one_sub_polynomialSwitch4_root γ δ + refine ⟨max (Ka : ℝ) Kb, le_max_of_le_left Ka.2, ?_⟩ + intro v r v' r' + set A : ℝ → ℝ := fun x => polynomialSwitch4 α β x ^ (4⁻¹ : ℝ) + set B : ℝ → ℝ := fun x => (1 - polynomialSwitch4 γ δ x) ^ (4⁻¹ : ℝ) + have ha0 (x : ℝ) : 0 ≤ A x := Real.rpow_nonneg (polynomialSwitch4_nonneg _ _ _) _ + have hb0 (x : ℝ) : 0 ≤ B x := + Real.rpow_nonneg (sub_nonneg.mpr (polynomialSwitch4_le_one _ _ _)) _ + have ha1 (x : ℝ) : A x ≤ 1 := + Real.rpow_le_one (polynomialSwitch4_nonneg _ _ _) (polynomialSwitch4_le_one _ _ _) + (by norm_num) + have hb1 (x : ℝ) : B x ≤ 1 := + Real.rpow_le_one (sub_nonneg.mpr (polynomialSwitch4_le_one _ _ _)) + (sub_le_self _ (polynomialSwitch4_nonneg _ _ _)) (by norm_num) + have hda : |A v - A v'| ≤ Ka * |v - v'| := by + simpa only [Real.dist_eq] using hKa.dist_le_mul v v' + have hdb : |B r - B r'| ≤ Kb * |r - r'| := by + simpa only [Real.dist_eq] using hKb.dist_le_mul r r' + rw [Real.mul_rpow (polynomialSwitch4_nonneg _ _ _) + (sub_nonneg.mpr (polynomialSwitch4_le_one _ _ _)), + Real.mul_rpow (polynomialSwitch4_nonneg _ _ _) + (sub_nonneg.mpr (polynomialSwitch4_le_one _ _ _))] + change |A v * B r - A v' * B r'| ≤ _ + have hsplit : A v * B r - A v' * B r' = + (A v - A v') * B r + A v' * (B r - B r') := by ring + rw [hsplit] + calc + _ ≤ |A v - A v'| * B r + A v' * |B r - B r'| := by + refine (abs_add_le _ _).trans_eq ?_ + rw [abs_mul, abs_mul, abs_of_nonneg (hb0 r), abs_of_nonneg (ha0 v')] + _ ≤ |A v - A v'| + |B r - B r'| := by + exact add_le_add (mul_le_of_le_one_right (abs_nonneg _) (hb1 r)) + (mul_le_of_le_one_left (abs_nonneg _) (ha1 v')) + _ ≤ (Ka : ℝ) * |v - v'| + (Kb : ℝ) * |r - r'| := add_le_add hda hdb + _ ≤ max (Ka : ℝ) Kb * (|v - v'| + |r - r'|) := by + rw [mul_add] + exact add_le_add (mul_le_mul_of_nonneg_right (le_max_left _ _) (abs_nonneg _)) + (mul_le_mul_of_nonneg_right (le_max_right _ _) (abs_nonneg _)) + +/-- The actual preparatory row function has a globally Lipschitz fourth root. -/ +theorem exists_abs_polynomialPrepRow4_root_sub_le (θ : ℝ) : + ∃ C : ℝ, 0 ≤ C ∧ ∀ v r v' r', + |polynomialPrepRow4 θ v r ^ (4⁻¹ : ℝ) - polynomialPrepRow4 θ v' r' ^ (4⁻¹ : ℝ)| ≤ + C * (|v - v'| + |r - r'|) := + exists_abs_switch_product_root_sub_le _ _ _ _ + +/-- The actual auxiliary score has a globally Lipschitz fourth root. -/ +theorem exists_abs_polynomialAuxCutoff4_root_sub_le (θ : ℝ) : + ∃ C : ℝ, 0 ≤ C ∧ ∀ v r v' r', + |polynomialAuxCutoff4 θ v r ^ (4⁻¹ : ℝ) - polynomialAuxCutoff4 θ v' r' ^ (4⁻¹ : ℝ)| ≤ + C * (|v - v'| + |r - r'|) := + exists_abs_switch_product_root_sub_le _ _ _ _ + +/-- The broad witness also has a globally Lipschitz fourth root. -/ +theorem exists_abs_polynomialWitnessCutoff4_root_sub_le (θ : ℝ) : + ∃ C : ℝ, 0 ≤ C ∧ ∀ v r v' r', + |polynomialWitnessCutoff4 θ v r ^ (4⁻¹ : ℝ) - + polynomialWitnessCutoff4 θ v' r' ^ (4⁻¹ : ℝ)| ≤ C * (|v - v'| + |r - r'|) := + exists_abs_switch_product_root_sub_le _ _ _ _ + +/-! ## Exact rational evaluation -/ + +@[simp, norm_cast] +theorem polynomialPrepCutoff4_ratCast (θ v : ℚ) : + polynomialPrepCutoff4 (θ : ℝ) v = (polynomialPrepCutoff4 θ v : ℚ) := by + simp only [polynomialPrepCutoff4, ← polynomialSwitch4_ratCast, Rat.cast_div, Rat.cast_mul, + Rat.cast_ofNat] + +@[simp, norm_cast] +theorem polynomialRowCutoff4_ratCast (θ r : ℚ) : + polynomialRowCutoff4 (θ : ℝ) r = (polynomialRowCutoff4 θ r : ℚ) := by + simp only [polynomialRowCutoff4, Rat.cast_sub, Rat.cast_one, ← polynomialSwitch4_ratCast, + Rat.cast_div, Rat.cast_ofNat] + +@[simp, norm_cast] +theorem polynomialPrepRow4_ratCast (θ v r : ℚ) : + polynomialPrepRow4 (θ : ℝ) v r = (polynomialPrepRow4 θ v r : ℚ) := by + simp only [polynomialPrepRow4, polynomialPrepCutoff4_ratCast, polynomialRowCutoff4_ratCast, + Rat.cast_mul] + +@[simp, norm_cast] +theorem polynomialAuxCutoff4_ratCast (θ v r : ℚ) : + polynomialAuxCutoff4 (θ : ℝ) v r = (polynomialAuxCutoff4 θ v r : ℚ) := by + simp only [polynomialAuxCutoff4, Rat.cast_mul, Rat.cast_sub, Rat.cast_one, + ← polynomialSwitch4_ratCast, Rat.cast_div, Rat.cast_ofNat] + +@[simp, norm_cast] +theorem polynomialWitnessCutoff4_ratCast (θ v r : ℚ) : + polynomialWitnessCutoff4 (θ : ℝ) v r = (polynomialWitnessCutoff4 θ v r : ℚ) := by + simp only [polynomialWitnessCutoff4, Rat.cast_mul, Rat.cast_sub, Rat.cast_one, + ← polynomialSwitch4_ratCast, Rat.cast_div, Rat.cast_ofNat] + +end Cslib diff --git a/ComplexityTests/PolynomialAtomCutoffs.lean b/ComplexityTests/PolynomialAtomCutoffs.lean new file mode 100644 index 0000000000..917ce9d985 --- /dev/null +++ b/ComplexityTests/PolynomialAtomCutoffs.lean @@ -0,0 +1,88 @@ +/- +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.PolynomialAtomCutoffs +import Complexity.Foundations.Probability.CorrectionAtom +import Mathlib.LinearAlgebra.Matrix.Notation +import Mathlib.Tactic.Linarith +import Mathlib.Tactic.NormNum + +/-! +# Tests for polynomial atom cutoffs + +Both switches vary in each interior example, producing exact value `1/4`. The broad witness +retains its strict entry/rank margin at its closed endpoints. Concrete existing atom and score +expressions use the new polynomial factors, and the witness's fourth-root variation forces +its Lipschitz constant to be positive. +-/ + +namespace ComplexityTests.PolynomialAtomCutoffs + +open Cslib Finset Matrix + +-- All three functions execute with rational inputs, including both transition regions. +/-- info: true -/ +#guard_msgs in +#eval [polynomialPrepRow4 (8 : ℚ) 5 (3 / 250), + polynomialAuxCutoff4 (8 : ℚ) (3 / 2) (3 / 25), + polynomialWitnessCutoff4 (1000 : ℚ) 86 (53 / 2)] == [1 / 4, 1 / 4, 1 / 4] + +private theorem witness_quarter : polynomialWitnessCutoff4 (1000 : ℚ) 86 (53 / 2) = 1 / 4 := by + norm_num [polynomialWitnessCutoff4, polynomialSwitch4, polynomialTransition4, + transitionPolynomial4] + +-- Rational evaluation is exactly the real function used by the analytic theorems. +example : polynomialWitnessCutoff4 (1000 : ℝ) 86 (53 / 2) = 1 / 4 := by + have h := polynomialWitnessCutoff4_ratCast 1000 86 (53 / 2) + norm_num only [Rat.cast_ofNat, Rat.cast_div, witness_quarter] at h + exact h + +example : polynomialPrepRow4 (8 : ℝ) (-4) (-1) = 0 ∧ + polynomialAuxCutoff4 (8 : ℝ) (-4) (-1) = 0 ∧ + polynomialWitnessCutoff4 (1000 : ℝ) (-4) (-1) = 0 := by + exact ⟨polynomialPrepRow4_eq_zero_of_entry_le (by norm_num) (by norm_num), + polynomialAuxCutoff4_eq_zero_of_entry_le (by norm_num) (by norm_num), + polynomialWitnessCutoff4_eq_zero_of_entry_le (by norm_num) (by norm_num)⟩ + +-- The exact witness margin is 82 - 3*27 = 1; closure includes both boundary points. +example : (3 : ℝ) * 27 < 82 ∧ polynomialWitnessCutoff4 (1000 : ℝ) 82 0 = 0 ∧ + polynomialWitnessCutoff4 (1000 : ℝ) 90 27 = 0 ∧ + polynomialWitnessCutoff4 (1000 : ℝ) 90 26 = 1 := by + exact ⟨by norm_num, + polynomialWitnessCutoff4_eq_zero_of_entry_le (by norm_num) (by norm_num), + polynomialWitnessCutoff4_eq_zero_of_rank_ge (by norm_num) (by norm_num), + polynomialWitnessCutoff4_eq_one (by norm_num) (by norm_num) (by norm_num)⟩ + +private noncomputable def G : Matrix (Fin 2) (Fin 2) ℝ := !![0, 8; 0, 0] + +private theorem first_row_rank : kthLargest 2 univ (fun y => G 0 y / 1) = 0 := by + norm_num [kthLargest, G, Fin.univ_succ, filter_insert, filter_singleton] + +-- This is an actual atom preparation and actual auxiliary score, not separate scalar formulas. +example : atomPrep (polynomialPrepCutoff4 8) (polynomialRowCutoff4 8) 2 1 G univ 0 1 = 1 ∧ + auxScore (polynomialAuxCutoff4 8) 2 1 G univ 0 1 = 1 := by + constructor + · rw [atomPrep, rowGate, first_row_rank] + have hv : G 0 1 / 1 = 8 := by norm_num [G] + rw [hv, polynomialPrepCutoff4_eq_one (by norm_num) (by norm_num), + polynomialRowCutoff4_eq_one (by norm_num) (by norm_num), mul_one] + · rw [auxScore, first_row_rank] + have hv : G 0 1 / 1 = 8 := by norm_num [G] + rw [hv] + exact polynomialAuxCutoff4_eq_one (by norm_num) (by norm_num) (by norm_num) + +-- The analytic constant cannot be zero: the fourth root changes from zero to one over width 8. +example : ∃ C : ℝ, 1 / 8 ≤ C ∧ ∀ v r v' r', + |polynomialWitnessCutoff4 1000 v r ^ (4⁻¹ : ℝ) - + polynomialWitnessCutoff4 1000 v' r' ^ (4⁻¹ : ℝ)| ≤ C * (|v - v'| + |r - r'|) := by + obtain ⟨C, _, hC⟩ := exists_abs_polynomialWitnessCutoff4_root_sub_le 1000 + have h := hC 90 0 82 0 + rw [polynomialWitnessCutoff4_eq_one (by norm_num) (by norm_num) (by norm_num), + polynomialWitnessCutoff4_eq_zero_of_entry_le (by norm_num) (by norm_num)] at h + norm_num at h + exact ⟨C, by linarith, hC⟩ + +end ComplexityTests.PolynomialAtomCutoffs