From fe32886a35bef3cbaa59e3e3dc1516326b8d43da Mon Sep 17 00:00:00 2001 From: Samuel Schlesinger Date: Fri, 30 Oct 2026 15:40:58 +0000 Subject: [PATCH 1/3] 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 9a3bc3cde..257d53cdd 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 000000000..1ee62aee9 --- /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 000000000..bc5f89fc9 --- /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/3] 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 257d53cdd..bccc4b139 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/3] 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 bccc4b139..ed57380e4 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 000000000..f4b694aca --- /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 000000000..f3cc6d5a2 --- /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