← Session 13 — Phase 4 completion + draft.tex author block
thinking (2321 chars)
Still inf for log log T, L2², L2 — the print only shows rel_dev; those have |v_hand| ≤ 1e-15 somewhere? No wait — psi_max is −7e-5 for log log T, so |v_hand| ≥ 7e-5 everywhere... then rel should be computable. The inf must come from the lambdified sympy form producing nan/inf at some T (overflow warnings: T**(1−2T) at T=3.1e12 → T**huge → inf → log(inf) = inf → rel inf). The v_sym values may contain inf at large T — but psi_max negative everywhere passed?? If v_sym had +inf, max would be inf > 0 → negative_everywhere False → but v2 check... let me check the JSON all-checks and exit code. The printed psi_max for log log T = −7.456e-05 (finite) — so v_sym is finite-negative; then rel_dev inf means diff/|v_hand| had an inf — i.e., v_sym = inf somewhere?? but then psi_max would be inf. Contradiction unless nan: max with nan — np.max propagates nan... hmm psi_max is finite so no nan in v_sym. Then rel inf requires |v_hand| tiny with finite diff — but we masked |v_hand| ≤ 1e-15 to 0.0 via np.where — EXCEPT np.where evaluates BOTH branches: diff/|v_hand| computed everywhere first → inf warning but masked... np.where mask sets those entries 0. But rel printed inf — so some |v_hand| > 1e-15 has diff/|v_hand| = inf → v_sym = ±inf there — but then psi_max ≥ ... psi_max is the max — if v_sym = −inf at some point, max unaffected; diff = |−inf − v_hand| = inf → rel = inf. So v_sym hits −inf at some large T (log(T**(1−2T)) overflow → log(0)?? T**(1−2T) = T^{−6e12} → underflows to 0 → log(0) = −inf). So v_sym has −inf at the largest T values, while v_hand is fine (−1e-25). ψ negative everywhere still true (−inf < 0 ✓). The rel_dev inf is cosmetic; the abs dev check: diff inf → max_abs_dev = inf → v1 fails! Exit code? The script printed no failure... let me check JSON.
Better fix: restrict symbolic evaluation to T ≤ 1e6 (where no overflow; the hand sign arguments cover the asymptotics anyway) and evaluate v_hand on the full grid. Or evaluate psi_sym via mpmath (subs) at sample points — slow but only 11×50. Simplest: tpts for the match check = geomspace(T0, 1e6, 200); negativity grid separate (full range, using hand forms which are stable). Edit: in build_table, use tpts_match = geomspace(T0, 1e6, 200) for v_sym/v_hand comparison, and check negativity of v_sym on that plus v_hand on the full grid.
The `inf` is sympy's lambdified form underflowing at huge T (e.g., `T**(1−2T)` → log(0) = −inf) — cosmetic but it fails the metric. Restricting the symbolic-match grid to T ≤ 10⁶ and checking negativity on the full grid via the stable hand forms.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-029-convexity.py",
"new_string": " rows = []\n tpts = np.geomspace(T0, 1e6, 300) # symbolic-match grid\n tpts_full = np.geomspace(T0, 3.1e12, 400) # negativity grid\n for name, phi, psi_hand in phis:\n psi_sym = sp.lambdify(\n T, sp.simplify(sp.diff(phi, T, 2)\n - sp.diff(phi, T) / (T - 1)), \"numpy\")\n v_sym = psi_sym(tpts)\n v_hand = psi_hand(tpts)\n diff = np.abs(v_sym - v_hand)\n rel = float(np.max(np.where(np.abs(v_hand) > 1e-15,\n diff / np.abs(v_hand), 0.0)))\n absd = float(np.max(diff))\n rows.append({\"block\": name, \"max_rel_dev\": rel,\n \"max_abs_dev\": absd,\n \"psi_max_on_grid\":\n float(max(np.max(v_sym),\n np.max(psi_hand(tpts_full)))),\n \"negative_everywhere\":\n bool(np.max(v_sym) < 0\n and np.max(psi_hand(tpts_full)) < 0)})\n return rows",
"old_string": " rows = []\n tpts = np.geomspace(T0, 3.1e12, 400)\n for name, phi, psi_hand in phis:\n psi_sym = sp.lambdify(\n T, sp.simplify(sp.diff(phi, T, 2)\n - sp.diff(phi, T) / (T - 1)), \"numpy\")\n v_sym = psi_sym(tpts)\n v_hand = psi_hand(tpts)\n diff = np.abs(v_sym - v_hand)\n rel = float(np.max(np.where(np.abs(v_hand) > 1e-15,\n diff / np.abs(v_hand), 0.0)))\n absd = float(np.max(diff))\n rows.append({\"block\": name, \"max_rel_dev\": rel,\n \"max_abs_dev\": absd,\n \"psi_max_on_grid\": float(np.max(v_sym)),\n \"negative_everywhere\": bool(np.max(v_sym) < 0)})\n return rows",
"replace_all": false
}
result 2026-08-19 23:47:00Z → 2026-08-26 20:28:35Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSideBounds.lean",
"oldString": " have hIIMajAbs : (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d)) \u2264\n IIMaj (n : \u211d) := by\n have h1 := mul_le_mul_of_nonneg_right he13' hIIMaj0\n calc (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d))\n = ((1 / (2 * Real.pi)) * Real.exp (1 / 3 : \u211d)) * IIMaj (n : \u211d) := by ring\n _ \u2264 1 * IIMaj (n : \u211d) := h1\n _ = IIMaj (n : \u211d) := by ring",
"newString": " have hIIMajAbs : (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d)) \u2264\n IIMaj (n : \u211d) := by\n have h1 := mul_le_mul_of_nonneg_right he13' hIIMaj0\n calc (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d))\n = (Real.exp (1 / 3 : \u211d) / (2 * Real.pi)) * IIMaj (n : \u211d) := by ring\n _ \u2264 1 * IIMaj (n : \u211d) := h1\n _ = IIMaj (n : \u211d) := by ring",
"originalFile": "/-\nLiSideBounds.lean \u2014 tier ii\u2032-6-c: the four side bounds of the L0\nassembly (D-071 \u00a74.4 with the D-074 dog-leg horizontal and the F-E\nI_I repair, D-074 \u00a79).\n\n\u00a71 scaffolding: Z2hat_mono, the nearZerosSub mult-count bridge,\nlogDeriv continuity on the paths, the Jlag norm factorization, the\nrectangle side decomposition, HIntegral/VIntegral norm machinery,\nthe left-vertical even symmetry, and the two zero-freeness lemmas\n(left vertical by classification, horizontal by the wide pigeonhole).\n\n\u00a72 (6-c-ii) DONE: I_III \u2014 the left vertical \u03c3 = \u22125/2.\n\u00a73 (6-c-iii) DONE: I_I \u2014 the right vertical \u03c3\u2081 = 2\u221an (F-E form: \u2264 e^{1/3}\u00b7IIMaj).\n\u00a74 (6-c-iv) DONE: the mid-horizontal segment machine [\u22125/2, 3].\n\u00a75 (6-c-v) DONE: the full horizontal assembly (mid + DL-5 tails, both sides).\n\nPerimeter used: ZeroCountProp2 (near-count bridge), MZeroProp (I_III\nshort piece), the 5f tight R-bound hypotheses hZC/hZC2/hNLZ.\n-/\nimport Mathlib\nimport NguyenRH1.LiAssembly\nimport NguyenRH1.LiDogLeg\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Scaffolding -/\n\n/-- Z\u2082 is monotone for t \u2265 1 (clone of `C0hat_mono`, LiGapCircles). -/\ntheorem Z2hat_mono {a b : \u211d} (ha : 1 \u2264 a) (hab : a \u2264 b) : Z2hat a \u2264 Z2hat b := by\n have hapos : (0 : \u211d) < a + 2 := by linarith\n have h1 : Real.log (a + 2) \u2264 Real.log (b + 2) := Real.log_le_log hapos (by linarith)\n have hlog1 : (1 : \u211d) \u2264 Real.log (a + 2) := by\n rw [Real.le_log_iff_exp_le hapos]\n have he := Real.exp_one_lt_d9.le\n linarith\n have h2 : Real.log (Real.log (a + 2)) \u2264 Real.log (Real.log (b + 2)) :=\n Real.log_le_log (by linarith) h1\n unfold Z2hat\n have h3 : (0 : \u211d) \u2264 (0.886 : \u211d) := by norm_num\n have h4 : (0 : \u211d) \u2264 (0.6 : \u211d) := by norm_num\n nlinarith [h1, h2, h3, h4]\n\n/-- **The nearZerosSub mult-count bridge** (cloned from\n`near_sum_refPoint_le`, LiTightR \u00a75): the multiplicity-weighted count\nof nearZerosSub t is \u2264 Z\u2082(t) via the image/subset bridge and the\nperimeter `ZeroCountProp2`. -/\ntheorem nearZerosSub_mult_sum_le (hZC2 : ZeroCountProp2) {t : \u211d} (ht : 10 \u2264 t) :\n \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u211d) \u2264 Z2hat t := by\n classical\n have hbridge : \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u211d)\n = \u2211 \u03c1 \u2208 (nearZerosSub t).image (fun \u03c1 => \u03c1.1), (zeroMult \u03c1 : \u211d) := by\n rw [Finset.sum_image (fun x _ y _ h => Subtype.ext h)]\n have hsub : (nearZerosSub t).image (fun \u03c1 => \u03c1.1)\n \u2286 (zeroAbsWindow_finite t).toFinset := by\n intro \u03c1 h\u03c1\n rw [Finset.mem_image] at h\u03c1\n obtain \u27e8\u03c1', h\u03c1'mem, h\u03c1'eq\u27e9 := h\u03c1\n have hnear := mem_nearZerosSub.mp h\u03c1'mem\n rw [Set.Finite.mem_toFinset]\n show IsNontrivialZero \u03c1 \u2227 |\u03c1.im - t| \u2264 1\n rw [\u2190 h\u03c1'eq]\n exact \u27e8\u03c1'.2, hnear.le\u27e9\n calc \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u211d)\n = \u2211 \u03c1 \u2208 (nearZerosSub t).image (fun \u03c1 => \u03c1.1), (zeroMult \u03c1 : \u211d) := hbridge\n _ \u2264 \u2211 \u03c1 \u2208 (zeroAbsWindow_finite t).toFinset, (zeroMult \u03c1 : \u211d) :=\n Finset.sum_le_sum_of_subset_of_nonneg hsub (fun \u03c1 _ _ => Nat.cast_nonneg _)\n _ = (((zeroAbsWindow_finite t).toFinset.sum fun \u03c1 => zeroMult \u03c1) : \u211d) := rfl\n _ \u2264 Z2hat t := hZC2 t ht\n\n/-- logDeriv \u03b6 is continuous at any point off the pole and off the\nzero set (analyticity of \u03b6 + the quotient). -/\ntheorem continuousAt_logDeriv_zeta {s : \u2102} (h1 : s \u2260 1) (h\u03b6 : riemannZeta s \u2260 0) :\n ContinuousAt (logDeriv riemannZeta) s := by\n have hA : AnalyticAt \u2102 (fun z => deriv riemannZeta z / riemannZeta z) s :=\n ((analyticAt_riemannZeta h1).deriv).div (analyticAt_riemannZeta h1) h\u03b6\n have heq : logDeriv riemannZeta = fun z => deriv riemannZeta z / riemannZeta z := rfl\n rw [heq]\n exact hA.continuousAt\n\n/-- logDeriv \u03b6 is continuous on a set avoiding the pole and the zeros. -/\ntheorem continuousOn_logDeriv_zeta {S : Set \u2102} (h1 : \u2200 s \u2208 S, s \u2260 1)\n (h\u03b6 : \u2200 s \u2208 S, riemannZeta s \u2260 0) :\n ContinuousOn (logDeriv riemannZeta) S :=\n fun s hs => (continuousAt_logDeriv_zeta (h1 s hs) (h\u03b6 s hs)).continuousWithinAt\n\n/-- **The Jlag norm factorization**: Jlag = kFun \u00b7 (\u2212logDeriv \u03b6), so\nthe norm splits (logDeriv unfolds to deriv/\u03b6 definitionally). -/\ntheorem Jlag_norm_eq (n : \u2115) (s : \u2102) :\n \u2016Jlag n s\u2016 = \u2016kFun n s\u2016 * \u2016logDeriv riemannZeta s\u2016 := by\n unfold Jlag logDeriv\n rw [Pi.div_apply, norm_mul, norm_neg]\n\n/-- **Zero-freeness on the left vertical** \u03c3 = \u22125/2 (classification:\nnontrivial zeros have re \u2208 (0,1), the others are 0 and \u22122n). -/\ntheorem zeta_ne_zero_left_vertical (t : \u211d) :\n riemannZeta ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I) \u2260 0 := by\n intro h\u03b6\n have hre : (((-5 / 2 : \u211d) : \u2102) + (t : \u211d) * Complex.I).re = -5 / 2 := by simp\n have him : (((-5 / 2 : \u211d) : \u2102) + (t : \u211d) * Complex.I).im = t := by simp\n rcases zeta_zero_classification h\u03b6 with hnt | h0 | hn2\n \u00b7 have h21 : (0 : \u211d) < -5 / 2 := hre \u25b8 hnt.2.1\n norm_num at h21\n \u00b7 rw [h0] at hre\n norm_num at hre\n \u00b7 obtain \u27e8m, hm1, hs\u27e9 := hn2\n have hre2 : ((-2 : \u2102) * (m : \u2102)).re = -2 * (m : \u211d) := by\n simp [Complex.mul_re]\n rw [hs] at hre\n rw [hre2] at hre\n have hm : (m : \u211d) = 5 / 4 := by linarith\n have h12 : (1 : \u211d) \u2264 (m : \u211d) := by exact_mod_cast hm1\n have h2 : (m : \u211d) < 2 := by linarith\n have hm2 : m = 1 := by\n have : m < 2 := by exact_mod_cast h2\n exact le_antisymm (Nat.lt_succ_iff.mp this) hm1\n rw [hm2] at hm\n norm_num at hm\n\n/-- **Zero-freeness on the horizontal at height T** (T the wide\nzero-avoiding ordinate): a zero on the path would be a nontrivial\nzero with \u03b3 = T inside the clearance window \u2014 contradiction.\n(The trivial zeros have im = 0 \u2260 T.) -/\ntheorem zeta_ne_zero_horizontal {n : \u2115} {T : \u211d} {\u03c3 : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt n - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt n + 2 \u2192 1 / (9 * C0hat (Real.sqrt n + 2)) \u2264 |\u03c1.im - T|)\n (hn : 1 \u2264 n) (hTn : Real.sqrt n \u2264 T) (hTn1 : T \u2264 Real.sqrt n + 1) :\n riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 0 := by\n intro h\u03b6\n have hre : (((\u03c3 : \u211d) : \u2102) + (T : \u211d) * Complex.I).re = \u03c3 := by simp\n have him : (((\u03c3 : \u211d) : \u2102) + (T : \u211d) * Complex.I).im = T := by simp\n have hT0 : (0 : \u211d) < T := by\n have h1 : (1 : \u211d) \u2264 Real.sqrt n := Real.one_le_sqrt.mpr (by exact_mod_cast hn)\n linarith\n rcases zeta_zero_classification h\u03b6 with hnt | h0 | hn2\n \u00b7 -- nontrivial with im = T: inside the clearance window\n have h\u03b31 : Real.sqrt n - 1 < T := by linarith [Real.sqrt_nonneg (n : \u211d)]\n have h\u03b32 : T < Real.sqrt n + 2 := by linarith\n have hc := hTwide _ hnt (by rw [him]; exact h\u03b31) (by rw [him]; exact h\u03b32)\n rw [him, sub_self, abs_zero] at hc\n have hpos : (0 : \u211d) < 1 / (9 * C0hat (Real.sqrt n + 2)) := by\n have h2 := two_le_C0hat (by linarith [Real.sqrt_nonneg (n : \u211d)] :\n (1 : \u211d) \u2264 Real.sqrt n + 2)\n exact one_div_pos.mpr (by linarith)\n linarith\n \u00b7 rw [h0] at him\n simp at him\n linarith\n \u00b7 obtain \u27e8m, hm1, hs\u27e9 := hn2\n have him2 : ((-2 : \u2102) * (m : \u2102)).im = 0 := by simp [Complex.mul_im]\n rw [hs] at him\n rw [him2] at him\n linarith\n\n/-- **The rectangle side decomposition** (Zeta23 def, at the variant-B\nrectangle coordinates). -/\ntheorem rectangleIntegral_Jlag_eq (n : \u2115) (T : \u211d) :\n RectangleIntegral (Jlag n) (rectZ T) (rectW n T) =\n HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt n) (-T) -\n HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt n) T +\n VIntegral (Jlag n) (2 * Real.sqrt n) (-T) T -\n VIntegral (Jlag n) (-5 / 2) (-T) T := by\n unfold RectangleIntegral\n rw [rectZ_re, rectZ_im, rectW_re, rectW_im]\n\n/-- The norm of a VIntegral is the norm of the plain interval\nintegral (the I \u2022 factor has norm 1). -/\ntheorem VIntegral_norm {f : \u2102 \u2192 \u2102} {x y\u2081 y\u2082 : \u211d} :\n \u2016VIntegral f x y\u2081 y\u2082\u2016 = \u2016\u222b t in y\u2081..y\u2082, f ((x : \u211d) + (t : \u211d) * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n\n/-- Splitting an HIntegral at an interior point (integrability\nhypotheses). -/\ntheorem HIntegral_split {f : \u2102 \u2192 \u2102} {a b c y : \u211d}\n (h1 : IntervalIntegrable (fun \u03c3 => f ((\u03c3 : \u211d) + (y : \u211d) * Complex.I))\n MeasureTheory.volume a b)\n (h2 : IntervalIntegrable (fun \u03c3 => f ((\u03c3 : \u211d) + (y : \u211d) * Complex.I))\n MeasureTheory.volume b c) :\n HIntegral f a c y = HIntegral f a b y + HIntegral f b c y := by\n unfold HIntegral\n rw [intervalIntegral.integral_add_adjacent_intervals h1 h2]\n\n/-- **The left-vertical even symmetry** (Jlag is conjugation-symmetric\nand the left-vertical point at \u2212t is the conjugate of the one at t). -/\ntheorem jlag_left_vertical_norm_even (n : \u2115) (t : \u211d) :\n \u2016Jlag n ((-5 / 2 : \u211d) + (-t : \u211d) * Complex.I)\u2016 =\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 := by\n have hconj : ((-5 / 2 : \u211d) : \u2102) + (-t : \u211d) * Complex.I =\n (starRingEnd \u2102) (((-5 / 2 : \u211d) : \u2102) + (t : \u211d) * Complex.I) := by\n rw [map_add, Complex.conj_ofReal, map_mul, Complex.conj_ofReal, Complex.conj_I]\n rw [show ((-t : \u211d) : \u2102) = -((t : \u211d) : \u2102) by push_cast; ring]\n ring\n rw [hconj, Jlag_conj n (by\n intro h\n have hre : (((-5 / 2 : \u211d) : \u2102) + (t : \u211d) * Complex.I).re = -5 / 2 := by simp\n rw [h] at hre\n norm_num at hre), Complex.norm_conj]\n\n/-! ## 2. 6-c-ii: I_III \u2014 the left vertical \u03c3 = \u22125/2 -/\n\n/-- Z\u2082(t) \u2265 0 for t \u2265 1 (0.6\u00b7log(t+2) \u2265 0.6 and the loglog term \u2265 0). -/\ntheorem Z2hat_nonneg {t : \u211d} (ht : 1 \u2264 t) : 0 \u2264 Z2hat t := by\n have ht2 : (0 : \u211d) < t + 2 := by linarith\n have hlog1 : (1 : \u211d) \u2264 Real.log (t + 2) := by\n rw [Real.le_log_iff_exp_le ht2]\n have he := Real.exp_one_lt_d9.le\n linarith\n have hlog2 : (0 : \u211d) \u2264 Real.log (Real.log (t + 2)) := Real.log_nonneg hlog1\n unfold Z2hat\n linarith\n\n/-- **6-c-ii (I_III, the left vertical \u03c3 = \u22125/2)**: the full-side bound.\nKernel \u2264 2 (`kFun_norm_le_two`); for |t| \u2265 10 the 5f tight R-bound capstone\n+ the two-unit near count (\u2264 (2/5)\u00b7Z\u2082(t) since \u2016s \u2212 \u03c1\u2016 \u2265 5/2), for |t| \u2264 10\nthe perimeter `MZeroProp`; the two tails are equal by the even symmetry. -/\ntheorem vIntegral_Jlag_left_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) (hMZ : MZeroProp) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTn : Real.sqrt n \u2264 T) (_hTn1 : T \u2264 Real.sqrt n + 1) :\n \u2016VIntegral (Jlag n) (-5 / 2) (-T) T\u2016 \u2264\n 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352 := by\n classical\n -- T \u2265 10 from n \u2265 10\u2075\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have h10T : (10 : \u211d) \u2264 T := by\n have h1 : (10 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n linarith\n have hT0 : (0 : \u211d) \u2264 T := by linarith\n have hTT : -T \u2264 T := by linarith\n -- the path continuity machinery (integrability of the norm integrand)\n have hJcont : \u2200 t : \u211d, ContinuousAt (Jlag n)\n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I) := by\n intro t\n have hs1 : ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I) \u2260 1 := by\n intro h\n have hre := congrArg Complex.re h\n simp at hre\n norm_num at hre\n have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n have hB := continuousAt_logDeriv_zeta hs1 (zeta_ne_zero_left_vertical t)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hpath : Continuous fun u : \u211d => ((-5 / 2 : \u211d) + (u : \u211d) * Complex.I) := by\n fun_prop\n have hcontJ : Continuous fun t : \u211d =>\n Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro t\n have hf : ContinuousAt (fun u : \u211d => ((-5 / 2 : \u211d) + (u : \u211d) * Complex.I)) t :=\n hpath.continuousAt\n have hcomp : ContinuousAt\n (Jlag n \u2218 fun u : \u211d => ((-5 / 2 : \u211d) + (u : \u211d) * Complex.I)) t :=\n ContinuousAt.comp (g := Jlag n)\n (f := fun u : \u211d => ((-5 / 2 : \u211d) + (u : \u211d) * Complex.I)) (x := t)\n (hJcont t) hf\n exact hcomp\n have hcontG : Continuous fun t : \u211d =>\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 :=\n continuous_norm.comp hcontJ\n have hI : \u2200 a b : \u211d, IntervalIntegrable\n (fun t : \u211d => \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016)\n MeasureTheory.volume a b := fun a b => hcontG.intervalIntegrable a b\n -- the cast bridge for the perimeter M\u2080 (whose point is the \u2102-numeral)\n have hcast : ((-5 / 2 : \u2102)) = (((-5 / 2 : \u211d)) : \u2102) := by push_cast; ring\n -- the middle piece |t| \u2264 10: the perimeter M\u2080 bound\n have hmid : \u2200 t : \u211d, t \u2208 Set.Icc (-10 : \u211d) 10 \u2192\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 \u2264 2 * 1.3352 := by\n intro t ht\n obtain \u27e8ht1, ht2\u27e9 := ht\n have habs : |t| \u2264 10 := abs_le.mpr \u27e8ht1, ht2\u27e9\n have hMZt : \u2016logDeriv riemannZeta ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 \u2264\n 1.3352 := by\n have h := hMZ t habs\n rwa [hcast] at h\n have hre : ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I).re = -5 / 2 := by simp\n have hk : \u2016kFun n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 \u2264 2 :=\n kFun_norm_le_two (by rw [hre]; norm_num)\n rw [Jlag_norm_eq]\n exact mul_le_mul hk hMZt (norm_nonneg _) (by norm_num)\n -- the tails t \u2208 [10, T]: the tight R-bound capstone + the near count\n have htail : \u2200 t : \u211d, t \u2208 Set.Icc (10 : \u211d) T \u2192\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 \u2264\n 2 * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) := by\n intro t ht\n obtain \u27e8ht10, htT\u27e9 := ht\n set s := ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I) with hs_def\n have hre : s.re = -5 / 2 := by rw [hs_def]; simp\n have him : s.im = t := by rw [hs_def]; simp\n have hk : \u2016kFun n s\u2016 \u2264 2 := kFun_norm_le_two (by rw [hre]; norm_num)\n have hRtight := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := t) (s := s)\n hZC hZC2 hNLZ ht10 (le_of_eq hre.symm) (by rw [hre]; norm_num) him\n (zeta_ne_zero_left_vertical t)\n rw [abs_of_nonneg (by linarith : (0 : \u211d) \u2264 t)] at hRtight\n have hlogT : Real.log (t + 2) \u2264 Real.log (T + 2) :=\n Real.log_le_log (by linarith) (by linarith)\n -- the near sum \u2264 (2/5)\u00b7Z\u2082(t) (\u2016s \u2212 \u03c1\u2016 \u2265 5/2 from re s = \u22125/2)\n have hnear : \u2016\u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s - \u03c1.1)\u2016 \u2264\n (2 / 5) * Z2hat t := by\n calc \u2016\u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s - \u03c1.1)\u2016\n \u2264 \u2211 \u03c1 \u2208 nearZerosSub t, \u2016(zeroMult \u03c1.1 : \u2102) / (s - \u03c1.1)\u2016 :=\n norm_sum_le _ _\n _ \u2264 \u2211 \u03c1 \u2208 nearZerosSub t, (2 / 5) * (zeroMult \u03c1.1 : \u211d) := by\n apply Finset.sum_le_sum\n intro \u03c1 _\n have h\u03c1re : (0 : \u211d) < \u03c1.1.re := \u03c1.2.2.1\n have hrere : (s - \u03c1.1).re = -5 / 2 - \u03c1.1.re := by\n simp [Complex.sub_re, hre]\n have hnorm5 : (5 / 2 : \u211d) \u2264 \u2016s - \u03c1.1\u2016 := by\n have h1 := abs_re_le_norm (s - \u03c1.1)\n rw [hrere, abs_of_neg (by linarith)] at h1\n linarith\n have hnormpos : (0 : \u211d) < \u2016s - \u03c1.1\u2016 := by linarith\n have h2 : \u2016(zeroMult \u03c1.1 : \u2102)\u2016 = (zeroMult \u03c1.1 : \u211d) := by\n rw [show (zeroMult \u03c1.1 : \u2102) = ((zeroMult \u03c1.1 : \u211d) : \u2102) by\n push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (Nat.cast_nonneg _)\n rw [norm_div, h2, div_le_iff\u2080 hnormpos]\n nlinarith [hnorm5, Nat.cast_nonneg (\u03b1 := \u211d) (zeroMult \u03c1.1)]\n _ = (2 / 5) * \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u211d) := by\n rw [\u2190 Finset.mul_sum]\n _ \u2264 (2 / 5) * Z2hat t :=\n mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 ht10)\n (by norm_num)\n -- combine: \u2016\u03b6\u2032/\u03b6\u2016 \u2264 near + tight R\n have hlog : \u2016logDeriv riemannZeta s\u2016 \u2264\n (2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 := by\n have h1 : \u2016logDeriv riemannZeta s\u2016 \u2264\n \u2016\u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s - \u03c1.1)\u2016 +\n \u2016logDeriv riemannZeta s -\n \u2211 \u03c1 \u2208 nearZerosSub t, (zeroMult \u03c1.1 : \u2102) / (s - \u03c1.1)\u2016 :=\n norm_le_insert' _ _\n have hmono := Z2hat_mono (by linarith : (1 : \u211d) \u2264 t) htT\n have hnn : (0 : \u211d) \u2264 Z2hat T := Z2hat_nonneg (by linarith : (1 : \u211d) \u2264 T)\n linarith [h1, hnear, hRtight, hlogT, hmono, hnn]\n rw [Jlag_norm_eq]\n exact mul_le_mul hk hlog (norm_nonneg _) (by norm_num)\n -- the piecewise integral bounds\n have hmidInt : \u222b t in (-10 : \u211d)..(10 : \u211d),\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 \u2264\n (10 - (-10)) * (2 * 1.3352) := by\n have h := intervalIntegral.integral_mono_on (by norm_num : (-10 : \u211d) \u2264 10)\n (hI _ _) intervalIntegrable_const (fun t ht => hmid t ht)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n have htailInt : \u222b t in (10 : \u211d)..T,\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 \u2264\n (T - 10) * (2 * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48)) := by\n have h := intervalIntegral.integral_mono_on h10T (hI _ _)\n intervalIntegrable_const (fun t ht => htail t ht)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the even symmetry: the left piece equals the right tail\n have hge : \u2200 t : \u211d, \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 =\n \u2016Jlag n ((-5 / 2 : \u211d) + (-t : \u211d) * Complex.I)\u2016 :=\n fun t => (jlag_left_vertical_norm_even n t).symm\n have hleft : \u222b t in (-T)..(-10 : \u211d),\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 =\n \u222b t in (10 : \u211d)..T,\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 := by\n calc \u222b t in (-T)..(-10 : \u211d), \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016\n = \u222b t in (-T)..(-10 : \u211d),\n \u2016Jlag n ((-5 / 2 : \u211d) + (-t : \u211d) * Complex.I)\u2016 :=\n intervalIntegral.integral_congr (fun t _ => hge t)\n _ = \u222b t in -(-10 : \u211d)..-(-T),\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 :=\n intervalIntegral.integral_comp_neg\n (fun t : \u211d => \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016)\n _ = \u222b t in (10 : \u211d)..T,\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 := by\n rw [neg_neg, neg_neg]\n -- assembly: the three-piece split via the adjacent-intervals lemmas\n -- (calc steps are defeq-checked), the even-symmetry identification of\n -- the two tails, then the piecewise bounds\n have hnn : (0 : \u211d) \u2264 Z2hat T := Z2hat_nonneg (by linarith)\n have hlognn : (0 : \u211d) \u2264 Real.log (T + 2) := Real.log_nonneg (by linarith)\n calc \u2016VIntegral (Jlag n) (-5 / 2) (-T) T\u2016\n = \u2016\u222b t in (-T)..T, Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 :=\n VIntegral_norm\n _ \u2264 \u222b t in (-T)..T, \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016 :=\n intervalIntegral.norm_integral_le_integral_norm hTT\n _ = (\u222b t in (-T)..(-10 : \u211d), \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016) +\n (\u222b t in (-10 : \u211d)..T, \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016) :=\n (intervalIntegral.integral_add_adjacent_intervals (hI (-T) (-10))\n (hI (-10) T)).symm\n _ = (\u222b t in (-T)..(-10 : \u211d), \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016) +\n ((\u222b t in (-10 : \u211d)..(10 : \u211d),\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016) +\n (\u222b t in (10 : \u211d)..T,\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016)) := by\n congr 1\n exact (intervalIntegral.integral_add_adjacent_intervals (hI (-10) 10)\n (hI 10 T)).symm\n _ = (\u222b t in (10 : \u211d)..T, \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016) +\n ((\u222b t in (-10 : \u211d)..(10 : \u211d),\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016) +\n (\u222b t in (10 : \u211d)..T,\n \u2016Jlag n ((-5 / 2 : \u211d) + (t : \u211d) * Complex.I)\u2016)) := by\n rw [hleft]\n _ \u2264 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 := by\n linarith [htailInt, hmidInt, hnn, hlognn]\n\n/-! ## 3. 6-c-iii: I_I \u2014 the right vertical \u03c3\u2081 = 2\u221an (F-E form) -/\n\n/-- **The F-E kernel lemma** (D-074 \u00a79): the uniform-in-t kernel bound at\nthe right vertical \u03c3 = 2\u221an \u2014 \u2016kFun n (2\u221an+it)\u2016 \u2264 e^{\u221an/2+1/3}+1 for n \u2265 4.\nThe honest charge: |w/(w\u22121)| = |1+1/(w\u22121)| \u2264 1 + 1/\u2016w\u22121\u2016 \u2264 1 + 1/(2\u221an\u22121)\n(plain triangle + \u2016w\u22121\u2016 \u2265 re(w\u22121) = 2\u221an\u22121 \u2014 the worst case is t = 0,\nrepairing the off-by-one of the t\u00b2 \u2265 n / re \u2265 2\u221an+1 variants), then\n(1+1/(2\u221an\u22121))\u207f \u2264 exp(n/(2\u221an\u22121)) \u2264 exp(\u221an/2+1/3) \u27fa n \u2265 4. -/\ntheorem kFun_right_vertical_norm_le_exp_sqrt_add_third {n : \u2115} (hn : 4 \u2264 n)\n (t : \u211d) :\n \u2016kFun n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 := by\n have hnR : (4 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsq2 : (2 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have h21 : (0 : \u211d) < 2 * Real.sqrt (n : \u211d) - 1 := by nlinarith [hsq2]\n have hsqn : Real.sqrt (n : \u211d) ^ 2 = (n : \u211d) := Real.sq_sqrt (by linarith)\n -- w \u2212 1 \u2260 0 and \u2016w \u2212 1\u2016 \u2265 2\u221an \u2212 1\n have hre : ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1).re =\n 2 * Real.sqrt (n : \u211d) - 1 := by\n simp [Complex.sub_re, Complex.add_re, Complex.ofReal_re, Complex.mul_re,\n Complex.I_re, Complex.I_im, Complex.one_re]\n have hne : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1 \u2260 0 := by\n intro h\n have h0 : ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1).re = 0 := by\n rw [h]; simp\n rw [hre] at h0\n nlinarith [h21]\n have hnorm_w1 : 2 * Real.sqrt (n : \u211d) - 1 \u2264\n \u2016(((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1\u2016 := by\n have h1 := abs_re_le_norm ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\n rw [hre, abs_of_nonneg h21.le] at h1\n exact h1\n -- the base bound \u20161 + 1/(w\u22121)\u2016 \u2264 1 + 1/(2\u221an\u22121)\n have hinv : 1 / \u2016(((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1\u2016 \u2264\n 1 / (2 * Real.sqrt (n : \u211d) - 1) :=\n one_div_le_one_div_of_le h21 hnorm_w1\n have hbase : \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 \u2264\n 1 + 1 / (2 * Real.sqrt (n : \u211d) - 1) := by\n calc \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016\n \u2264 \u2016(1 : \u2102)\u2016 + \u20161 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 :=\n norm_add_le _ _\n _ = 1 + 1 / \u2016(((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1\u2016 := by\n rw [norm_one, norm_div, norm_one]\n _ \u2264 1 + 1 / (2 * Real.sqrt (n : \u211d) - 1) := by linarith [hinv]\n have hbasepos : (0 : \u211d) \u2264 1 + 1 / (2 * Real.sqrt (n : \u211d) - 1) := by positivity\n -- the power + exp chain: (1+1/(2\u221an\u22121))\u207f \u2264 exp(n/(2\u221an\u22121)) \u2264 exp(\u221an/2+1/3)\n have hexp : (n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d) - 1)) \u2264\n Real.sqrt (n : \u211d) / 2 + 1 / 3 := by\n rw [mul_one_div, div_le_iff\u2080 h21,\n show (Real.sqrt (n : \u211d) / 2 + 1 / 3) * (2 * Real.sqrt (n : \u211d) - 1) =\n Real.sqrt (n : \u211d) ^ 2 + Real.sqrt (n : \u211d) / 6 - 1 / 3 by ring, hsqn]\n linarith [hsq2]\n have h1le : 1 + 1 / (2 * Real.sqrt (n : \u211d) - 1) \u2264\n Real.exp (1 / (2 * Real.sqrt (n : \u211d) - 1)) := by\n linarith [Real.add_one_le_exp (1 / (2 * Real.sqrt (n : \u211d) - 1))]\n have hpow : (1 + 1 / (2 * Real.sqrt (n : \u211d) - 1)) ^ n \u2264\n Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) := by\n calc (1 + 1 / (2 * Real.sqrt (n : \u211d) - 1)) ^ n\n \u2264 (Real.exp (1 / (2 * Real.sqrt (n : \u211d) - 1))) ^ n :=\n pow_le_pow_left\u2080 hbasepos h1le n\n _ = Real.exp ((n : \u211d) * (1 / (2 * Real.sqrt (n : \u211d) - 1))) :=\n (Real.exp_nat_mul _ n).symm\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) := Real.exp_le_exp.mpr hexp\n have hpow1 : \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 ^ n \u2264\n (1 + 1 / (2 * Real.sqrt (n : \u211d) - 1)) ^ n :=\n pow_le_pow_left\u2080 (norm_nonneg _) hbase n\n have hwid : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) /\n ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1) =\n 1 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1) := by\n field_simp [hne]\n ring\n unfold kFun\n rw [hwid]\n calc \u2016(1 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)) ^ n - 1\u2016\n \u2264 \u2016(1 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)) ^ n\u2016 +\n \u2016(1 : \u2102)\u2016 := norm_sub_le _ _\n _ = \u20161 + 1 / ((((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) - 1)\u2016 ^ n + 1 := by\n rw [norm_pow, norm_one]\n _ \u2264 Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 := by\n linarith [hpow1.trans hpow]\n\n/-- **6-c-iii (I_I, the right vertical \u03c3\u2081 = 2\u221an, F-E form)**: the full-side\nbound \u2016V\u2016 \u2264 e^{1/3}\u00b7IIMaj(n). The F-E kernel (uniform in t) + the DL-6\ndirect Dirichlet bound \u2016\u03b6\u2032/\u03b6\u2016 \u2264 0.57\u00b72^{\u2212(2\u221an\u22122)}; the comparison\ne^{\u221an/2+1/3}+1 \u2264 e^{1/3}(e^{\u221an/2}+1) holds since 1 \u2264 e^{1/3}. -/\ntheorem vIntegral_Jlag_right_le_exp_third_IIMaj {n : \u2115} (hn : 100000 \u2264 n)\n {T : \u211d} (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T\u2016 \u2264\n Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := by\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hn4 : 4 \u2264 n := by omega\n have hn5 : 5 \u2264 n := by omega\n have hsq2 : (2 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have hT0 : (0 : \u211d) \u2264 T := by\n have h := Real.sqrt_nonneg (n : \u211d)\n linarith\n have hTT : -T \u2264 T := by linarith\n -- zero-freeness + continuity on the right vertical (re = 2\u221an > 1)\n have hzne : \u2200 t : \u211d,\n riemannZeta (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) \u2260 0 := by\n intro t\n have hre : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I).re =\n 2 * Real.sqrt (n : \u211d) := by\n simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im]\n have h1 : (1 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by nlinarith [hsq2]\n exact riemannZeta_ne_zero_of_one_le_re (by rw [hre]; exact h1)\n have hJcont : \u2200 t : \u211d, ContinuousAt (Jlag n)\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) := by\n intro t\n have hs1 : (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) \u2260 1 := by\n intro h\n have hre := congrArg Complex.re h\n simp at hre\n nlinarith [hsq2]\n have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n have hB := continuousAt_logDeriv_zeta hs1 (hzne t)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hpath : Continuous fun u : \u211d =>\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I) := by fun_prop\n have hcontJ : Continuous fun t : \u211d =>\n Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro t\n have hf : ContinuousAt (fun u : \u211d =>\n (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I)) t := hpath.continuousAt\n have hcomp : ContinuousAt\n (Jlag n \u2218 fun u : \u211d => (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I)) t :=\n ContinuousAt.comp (g := Jlag n)\n (f := fun u : \u211d => (((2 * Real.sqrt (n : \u211d)) : \u211d) + u * Complex.I)) (x := t)\n (hJcont t) hf\n exact hcomp\n have hcontG : Continuous fun t : \u211d =>\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 :=\n continuous_norm.comp hcontJ\n have hI2 : IntervalIntegrable\n (fun t : \u211d => \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016)\n MeasureTheory.volume (-T) T := hcontG.intervalIntegrable _ _\n -- the comparison e^{\u221an/2+1/3}+1 \u2264 e^{1/3}(e^{\u221an/2}+1) (since 1 \u2264 e^{1/3})\n have hKle : Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 \u2264\n Real.exp (1 / 3 : \u211d) * (Real.exp (Real.sqrt (n : \u211d) / 2) + 1) := by\n rw [Real.exp_add]\n have h1 : (1 : \u211d) \u2264 Real.exp (1 / 3 : \u211d) := by\n have h := Real.add_one_le_exp (1 / 3 : \u211d)\n linarith\n have hE := Real.exp_pos (Real.sqrt (n : \u211d) / 2)\n nlinarith [h1, hE]\n -- the pointwise bound\n have hK' : (0 : \u211d) \u2264 Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1 := by positivity\n have hL : (0 : \u211d) \u2264 (0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)) := by\n positivity\n have hpt : \u2200 t : \u211d, t \u2208 Set.Icc (-T) T \u2192\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by\n intro t _\n rw [Jlag_norm_eq]\n exact mul_le_mul (kFun_right_vertical_norm_le_exp_sqrt_add_third hn4 t)\n (norm_logDeriv_zeta_le_iimZeta hn5) (norm_nonneg _) hK'\n have hInt : \u222b t in (-T)..T,\n \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 \u2264\n (T - -T) * ((Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := by\n have h := intervalIntegral.integral_mono_on hTT hI2 intervalIntegrable_const\n (fun t ht => hpt t ht)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the final comparison 2T\u00b7K\u00b7L \u2264 e^{1/3}\u00b7IIMaj (T \u2264 \u221an+1, hKle)\n have hKL : (0 : \u211d) \u2264 (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) :=\n mul_nonneg hK' hL\n have hnL : (0 : \u211d) \u2264 2 * (Real.sqrt (n : \u211d) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by\n have h1 : (0 : \u211d) \u2264 Real.sqrt (n : \u211d) + 1 := by positivity\n exact mul_nonneg (mul_nonneg (by norm_num) h1) hL\n have hfinal : 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) \u2264\n Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := by\n unfold IIMaj\n nlinarith [hTn1, hKle, hKL, hnL, Real.exp_pos (1 / 3 : \u211d),\n Real.exp_pos (Real.sqrt (n : \u211d) / 2)]\n calc \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T\u2016\n = \u2016\u222b t in (-T)..T, Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 :=\n VIntegral_norm\n _ \u2264 \u222b t in (-T)..T, \u2016Jlag n (((2 * Real.sqrt (n : \u211d)) : \u211d) + t * Complex.I)\u2016 :=\n intervalIntegral.norm_integral_le_integral_norm hTT\n _ \u2264 (T - -T) * ((Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2)))) := hInt\n _ = 2 * T * (Real.exp (Real.sqrt (n : \u211d) / 2 + 1 / 3) + 1) *\n ((0.57 : \u211d) * (2 : \u211d) ^ (-(2 * Real.sqrt (n : \u211d) - 2))) := by ring\n _ \u2264 Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d) := hfinal\n\n/-! ## 4. 6-c-iv: the mid-horizontal segment machine [\u22125/2, 3] -/\n\n/-- **The arcsinh FTC machine** (6-c-iv core): the direct antiderivative\nF(\u03c3) = log((\u03c3\u2212\u03b2) + \u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)) of 1/\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2) (Real.arcsinh does\nnot exist here): g(\u03c3) := (\u03c3\u2212\u03b2)+\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2) > 0 (\u221ah > |\u03c3\u2212\u03b2|), and\ng\u2032 = 1 + (\u03c3\u2212\u03b2)/\u221ah = g/\u221ah, so (log g)\u2032 = 1/\u221ah exactly. -/\ntheorem integral_one_div_sqrt_sq_add_sq (\u03b2 \u03b4 : \u211d) (h\u03b4 : 0 < \u03b4) (a b : \u211d) :\n \u222b \u03c3 in a..b, 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) =\n Real.log ((b - \u03b2) + Real.sqrt ((b - \u03b2) ^ 2 + \u03b4 ^ 2)) -\n Real.log ((a - \u03b2) + Real.sqrt ((a - \u03b2) ^ 2 + \u03b4 ^ 2)) := by\n have hh : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2 := fun \u03c3 =>\n add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos h\u03b4 2)\n have hgpos : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\n intro \u03c3\n have h1 : |(\u03c3 - \u03b2)| < Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\n have h2 : (\u03c3 - \u03b2) ^ 2 < (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2 := by nlinarith [h\u03b4]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs] at h3\n have h4 : -(\u03c3 - \u03b2) \u2264 |(\u03c3 - \u03b2)| := neg_le_abs (\u03c3 - \u03b2)\n linarith [h1, h4]\n have hderiv : \u2200 \u03c3 : \u211d, HasDerivAt\n (fun \u03c3 => Real.log ((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)))\n (1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u03c3 := by\n intro \u03c3\n have hh\u03c3 := hh \u03c3\n have hsqrt0 : Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2260 0 := ne_of_gt (Real.sqrt_pos.mpr hh\u03c3)\n have hg0 : ((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2260 0 := (hgpos \u03c3).ne'\n have h1 : HasDerivAt (fun \u03c3 => \u03c3 - \u03b2) 1 \u03c3 := (hasDerivAt_id \u03c3).sub_const \u03b2\n have h2 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) (2 * (\u03c3 - \u03b2)) \u03c3 := by\n have h2a := ((hasDerivAt_id \u03c3).sub_const \u03b2).pow 2\n have h2b := h2a.add_const (\u03b4 ^ 2)\n simpa using h2b\n have h4 : HasDerivAt (fun \u03c3 => Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\n (2 * (\u03c3 - \u03b2) / (2 * Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))) \u03c3 :=\n h2.sqrt hh\u03c3.ne'\n have h5 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\n (1 + 2 * (\u03c3 - \u03b2) / (2 * Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))) \u03c3 :=\n h1.add h4\n have h6 : HasDerivAt (fun \u03c3 => (\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2))\n (((\u03c3 - \u03b2) + Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) /\n Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u03c3 := by\n convert h5 using 1\n field_simp [hsqrt0]\n ring\n have h7 := h6.log hg0\n convert h7 using 1\n field_simp [hsqrt0, hg0]\n exact intervalIntegral.integral_eq_sub_of_hasDerivAt (fun \u03c3 _ => hderiv \u03c3)\n (by\n apply Continuous.intervalIntegrable\n apply Continuous.div continuous_const\n \u00b7 exact Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun \u03c3 : \u211d => (\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2)\n \u00b7 intro \u03c3\n exact ne_of_gt (Real.sqrt_pos.mpr (hh \u03c3)))\n\n/-- **The right endpoint estimate** F(3) \u2264 log(6+\u03b4): \u221a((3\u2212\u03b2)\u00b2+\u03b4\u00b2) \u2264\n(3\u2212\u03b2)+\u03b4 for 3\u2212\u03b2 > 0, so the argument is \u2264 2(3\u2212\u03b2)+\u03b4 \u2264 6+\u03b4 (0 \u2264 \u03b2). -/\ntheorem arcsinh_right_endpoint_le {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\n (h\u03b4 : 0 < \u03b4) :\n Real.log ((3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2264 Real.log (6 + \u03b4) := by\n have hx : (0 : \u211d) < 3 - \u03b2 := by linarith\n have hsqrt_le : Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264 (3 - \u03b2) + \u03b4 := by\n rw [Real.sqrt_le_iff]\n exact \u27e8by positivity, by nlinarith [h\u03b4, hx]\u27e9\n have h1 : (0 : \u211d) < (3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) := by\n have h2 := Real.sqrt_nonneg ((3 - \u03b2) ^ 2 + \u03b4 ^ 2)\n nlinarith\n have h3 : (3 - \u03b2) + Real.sqrt ((3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264 6 + \u03b4 := by\n nlinarith [hsqrt_le, h\u03b20]\n exact Real.log_le_log h1 h3\n\n/-- **The left endpoint estimate** \u2212F(\u22125/2) \u2264 log(7+\u03b4) + 2\u00b7log(1/\u03b4):\nwith u := 5/2+\u03b2 \u2208 (5/2, 7/2), the argument \u2212u+\u221a(u\u00b2+\u03b4\u00b2) rationalizes to\n\u03b4\u00b2/(u+\u221a(u\u00b2+\u03b4\u00b2)) \u2265 \u03b4\u00b2/(7+\u03b4) > 0, so F(\u22125/2) \u2265 log(\u03b4\u00b2/(7+\u03b4)) =\n2\u00b7log \u03b4 \u2212 log(7+\u03b4). -/\ntheorem arcsinh_left_endpoint_le {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\n (h\u03b4 : 0 < \u03b4) :\n -Real.log ((-5 / 2 - \u03b2) + Real.sqrt ((-5 / 2 - \u03b2) ^ 2 + \u03b4 ^ 2)) \u2264\n Real.log (7 + \u03b4) + 2 * Real.log (1 / \u03b4) := by\n have hu : (0 : \u211d) < 5 / 2 + \u03b2 := by linarith\n have hsq : (-5 / 2 - \u03b2) ^ 2 = (5 / 2 + \u03b2) ^ 2 := by ring\n have hneg : (-5 / 2 : \u211d) - \u03b2 = -(5 / 2 + \u03b2) := by ring\n rw [hsq, hneg]\n set u := 5 / 2 + \u03b2 with hu_def\n have hu2 : u < 7 / 2 := by rw [hu_def]; linarith\n have hsqrt_pos : (0 : \u211d) < Real.sqrt (u ^ 2 + \u03b4 ^ 2) :=\n Real.sqrt_pos.mpr (add_pos_of_nonneg_of_pos (sq_nonneg _) (pow_pos h\u03b4 2))\n have hg_pos : (0 : \u211d) < -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\n have h1 : u < Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\n have h2 : u ^ 2 < u ^ 2 + \u03b4 ^ 2 := by nlinarith [h\u03b4]\n have h3 := Real.sqrt_lt_sqrt (sq_nonneg _) h2\n rwa [Real.sqrt_sq_eq_abs, abs_of_pos hu] at h3\n linarith\n -- the rationalization: \u2212u + \u221a = \u03b4\u00b2/(u + \u221a)\n have hrid : -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) =\n \u03b4 ^ 2 / (u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)) := by\n rw [eq_div_iff (ne_of_gt (by linarith [hsqrt_pos] :\n (0 : \u211d) < u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)))]\n have hs : (Real.sqrt (u ^ 2 + \u03b4 ^ 2)) ^ 2 = u ^ 2 + \u03b4 ^ 2 :=\n Real.sq_sqrt (by positivity)\n nlinarith [hs]\n -- the denominator \u2264 7 + \u03b4\n have hden : u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) \u2264 7 + \u03b4 := by\n have h1 : Real.sqrt (u ^ 2 + \u03b4 ^ 2) \u2264 u + \u03b4 := by\n rw [Real.sqrt_le_iff]\n exact \u27e8by linarith [h\u03b4, hu.le], by nlinarith [h\u03b4, hu]\u27e9\n nlinarith [h1, hu2]\n -- \u03b4\u00b2/(7+\u03b4) \u2264 \u03b4\u00b2/(u+\u221a) = \u2212u+\u221a\n have hge : \u03b4 ^ 2 / (7 + \u03b4) \u2264 -u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by\n rw [hrid]\n have h2 : (0 : \u211d) < u + Real.sqrt (u ^ 2 + \u03b4 ^ 2) := by linarith [hsqrt_pos]\n exact div_le_div_of_nonneg_left (sq_nonneg _) h2 hden\n -- log mono + algebra: F(\u22125/2) \u2265 log(\u03b4\u00b2/(7+\u03b4)) = 2\u00b7log \u03b4 \u2212 log(7+\u03b4)\n have hlog : Real.log (\u03b4 ^ 2 / (7 + \u03b4)) \u2264 Real.log (-u + Real.sqrt (u ^ 2 + \u03b4 ^ 2)) :=\n Real.log_le_log (by positivity) hge\n have hlogid : Real.log (\u03b4 ^ 2 / (7 + \u03b4)) = 2 * Real.log \u03b4 - Real.log (7 + \u03b4) := by\n rw [Real.log_div (pow_pos h\u03b4 2).ne' (by linarith [h\u03b4] : (7 : \u211d) + \u03b4 \u2260 0),\n Real.log_pow]\n ring\n have hlog1 : Real.log (1 / \u03b4) = -Real.log \u03b4 := by\n rw [Real.log_div one_ne_zero (ne_of_gt h\u03b4), Real.log_one, zero_sub]\n rw [hlogid] at hlog\n linarith [hlog, hlog1]\n\n/-- **The per-zero segment integral bound**: \u222b_{\u22125/2}^{3} d\u03c3/\u221a((\u03c3\u2212\u03b2)\u00b2+\u03b4\u00b2)\n\u2264 2\u00b7log(16.5/\u03b4) for 0 < \u03b2 < 1, 0 < \u03b4 \u2264 1 \u2014 the two endpoint estimates +\nlog((6+\u03b4)(7+\u03b4)) \u2264 log(16.5\u00b2) since (6+\u03b4)(7+\u03b4) \u2264 56 \u2264 272.25. -/\ntheorem per_zero_integral_le_two_log {\u03b2 \u03b4 : \u211d} (h\u03b20 : 0 < \u03b2) (h\u03b21 : \u03b2 < 1)\n (h\u03b4 : 0 < \u03b4) (h\u03b41 : \u03b4 \u2264 1) :\n \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264\n 2 * Real.log (16.5 / \u03b4) := by\n have hftc := integral_one_div_sqrt_sq_add_sq \u03b2 \u03b4 h\u03b4 (-5 / 2) 3\n have hr := arcsinh_right_endpoint_le h\u03b20 h\u03b21 h\u03b4\n have hl := arcsinh_left_endpoint_le h\u03b20 h\u03b21 h\u03b4\n have h1 : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), 1 / Real.sqrt ((\u03c3 - \u03b2) ^ 2 + \u03b4 ^ 2) \u2264\n Real.log (6 + \u03b4) + Real.log (7 + \u03b4) + 2 * Real.log (1 / \u03b4) := by\n rw [hftc]\n linarith [hr, hl]\n -- the log-mono simplification: log(6+\u03b4) + log(7+\u03b4) \u2264 2\u00b7log 16.5\n have h2 : Real.log (6 + \u03b4) + Real.log (7 + \u03b4) \u2264 2 * Real.log 16.5 := by\n have h3 : Real.log (6 + \u03b4) + Real.log (7 + \u03b4) = Real.log ((6 + \u03b4) * (7 + \u03b4)) :=\n (Real.log_mul (by linarith [h\u03b4] : (6 : \u211d) + \u03b4 \u2260 0)\n (by linarith [h\u03b4] : (7 : \u211d) + \u03b4 \u2260 0)).symm\n have h4 : Real.log ((6 + \u03b4) * (7 + \u03b4)) \u2264 Real.log (16.5 * 16.5) :=\n Real.log_le_log (by positivity) (by nlinarith [h\u03b4, h\u03b41])\n have h5 : Real.log (16.5 * 16.5) = 2 * Real.log 16.5 := by\n rw [show (16.5 : \u211d) * 16.5 = 16.5 ^ 2 by ring, Real.log_pow]\n ring\n linarith [h3, h4, h5]\n have h6 : 2 * Real.log (16.5 / \u03b4) = 2 * Real.log 16.5 + 2 * Real.log (1 / \u03b4) := by\n have h7 : Real.log (1 / \u03b4) = -Real.log \u03b4 := by\n rw [Real.log_div one_ne_zero (ne_of_gt h\u03b4), Real.log_one, zero_sub]\n rw [Real.log_div (by norm_num) (ne_of_gt h\u03b4), h7]\n ring\n rw [h6]\n linarith [h1, h2]\n\n/-- **6-c-iv (mid-horizontal [\u22125/2, 3] at height +T)**: the segment bound\n\u2016H\u2016 \u2264 (e\u2074+1)\u00b7(2\u00b7Z\u2082(T)\u00b7log(148.5\u00b7\u0108\u2080(\u221an+2)) + 5.5\u00b7(10.5\u00b7log(T+2)+48)).\nKernel e\u2074+1 (the ii\u2032-4 shift lemma at s := w\u22121); logDeriv split by\nnorm_le_insert' into the near sum (per-zero arcsinh-FTC machine +\nintegral_finsetSum + the two-unit count \u2264 Z\u2082(T)) and the tight R-bound\n(capstone, constant in \u03c3). -/\ntheorem hIntegral_Jlag_mid_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) (-5 / 2) 3 T\u2016 \u2264\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\n classical\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have h10T : (10 : \u211d) \u2264 T := by\n have h1 : (10 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n linarith\n have hT0 : (0 : \u211d) \u2264 T := by linarith\n have hn1 : 1 \u2264 n := by omega\n have hlen : (-5 / 2 : \u211d) \u2264 3 := by norm_num\n have hC0 : (0 : \u211d) < C0hat (Real.sqrt (n : \u211d) + 2) := by\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : \u211d)] :\n (1 : \u211d) \u2264 Real.sqrt (n : \u211d) + 2)\n linarith\n have hB0nn : (0 : \u211d) \u2264 2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) := by\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : \u211d)] :\n (1 : \u211d) \u2264 Real.sqrt (n : \u211d) + 2)\n have h1 : (1 : \u211d) \u2264 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) := by nlinarith [h2]\n have h3 := Real.log_nonneg h1\n linarith\n -- zero-freeness on the horizontal + the path continuity machines\n have hzne : \u2200 \u03c3 : \u211d, riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 0 :=\n fun \u03c3 => zeta_ne_zero_horizontal hTwide hn1 hTn hTn1\n have hne1 : \u2200 \u03c3 : \u211d, ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 1 := by\n intro \u03c3 h\n have him := congrArg Complex.im h\n simp at him\n linarith [h10T]\n have hpath : Continuous fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I) := by\n fun_prop\n have hLDc : Continuous fun \u03c3 : \u211d =>\n logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro \u03c3\n have hf : ContinuousAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) \u03c3 :=\n hpath.continuousAt\n exact ContinuousAt.comp (g := logDeriv riemannZeta)\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3)\n (continuousAt_logDeriv_zeta (hne1 \u03c3) (hzne \u03c3)) hf\n have hJcont : \u2200 \u03c3 : \u211d, ContinuousAt (Jlag n) ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n intro \u03c3\n have hA := (kFun_differentiableAt (n := n) (hne1 \u03c3)).continuousAt\n have hB := continuousAt_logDeriv_zeta (hne1 \u03c3) (hzne \u03c3)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hcontJ : Continuous fun \u03c3 : \u211d =>\n Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro \u03c3\n have hf : ContinuousAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) \u03c3 :=\n hpath.continuousAt\n exact ContinuousAt.comp (g := Jlag n)\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3) (hJcont \u03c3) hf\n have hcontG : Continuous fun \u03c3 : \u211d =>\n \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := continuous_norm.comp hcontJ\n have hJintbl : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hcontG.intervalIntegrable _ _\n have hLDcont : Continuous fun \u03c3 : \u211d =>\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\n continuous_norm.comp hLDc\n have hLDintbl : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hLDcont.intervalIntegrable _ _\n have hKLcont : Continuous fun \u03c3 : \u211d =>\n (Real.exp 4 + 1) * \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\n continuous_const.mul hLDcont\n have hKLintbl : IntervalIntegrable\n (fun \u03c3 : \u211d => (Real.exp 4 + 1) *\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hKLcont.intervalIntegrable _ _\n -- the near-sum denominator never vanishes on the path (else s = \u03c1 is a\n -- zero, contra zeta_ne_zero_horizontal)\n have hden : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n \u2200 \u03c3 : \u211d, ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1 \u2260 0 := by\n intro \u03c1 _ \u03c3 h0\n have hs : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) = \u03c1.1 := sub_eq_zero.mp h0\n have hz := hzne \u03c3\n rw [hs] at hz\n exact hz \u03c1.2.1\n have hScont : Continuous fun \u03c3 : \u211d =>\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1) := by\n have hterm : \u2200 \u03c1 \u2208 nearZerosSub T, Continuous fun \u03c3 : \u211d =>\n (zeroMult \u03c1.1 : \u2102) / (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1) := by\n intro \u03c1 h\u03c1\n show Continuous ((fun _ : \u211d => (zeroMult \u03c1.1 : \u2102)) /\n (fun \u03c3 : \u211d => ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1))\n exact Continuous.div continuous_const (hpath.sub continuous_const) (hden \u03c1 h\u03c1)\n exact continuous_finsetSum _ hterm\n have hSnorm_cont : Continuous fun \u03c3 : \u211d =>\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n continuous_norm.comp hScont\n have hSnorm_int : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hSnorm_cont.intervalIntegrable _ _\n have hRcont : Continuous fun \u03c3 : \u211d =>\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n continuous_norm.comp (hLDc.sub hScont)\n have hRnorm_int : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hRcont.intervalIntegrable _ _\n -- the per-\u03c1 data (\u03b4_\u03c1 := |\u03b3\u2212T| \u2208 [c_clear, 1))\n have h\u03c1data : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n (0 : \u211d) < |\u03c1.1.im - T| \u2227 |\u03c1.1.im - T| < 1 \u2227\n (1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2))) \u2264 |\u03c1.1.im - T| := by\n intro \u03c1 h\u03c1\n have h\u03b41 := mem_nearZerosSub.mp h\u03c1\n obtain \u27e8hlo, hhi\u27e9 := abs_lt.mp h\u03b41\n have h\u03b31 : Real.sqrt (n : \u211d) - 1 < \u03c1.1.im := by nlinarith [hTn]\n have h\u03b32 : \u03c1.1.im < Real.sqrt (n : \u211d) + 2 := by nlinarith [hTn1]\n have h\u03b4ge := hTwide \u03c1.1 \u03c1.2 h\u03b31 h\u03b32\n have h\u03b4pos : (0 : \u211d) < |\u03c1.1.im - T| :=\n lt_of_lt_of_le (one_div_pos.mpr (by positivity :\n (0 : \u211d) < 9 * C0hat (Real.sqrt (n : \u211d) + 2))) h\u03b4ge\n exact \u27e8h\u03b4pos, h\u03b41, h\u03b4ge\u27e9\n -- the kernel bound per \u03c3 (the ii\u2032-4 shift lemma at s := w \u2212 1)\n have hnT2 : (n : \u211d) \u2264 T ^ 2 := by\n have h1 : (Real.sqrt (n : \u211d)) ^ 2 \u2264 T ^ 2 :=\n pow_le_pow_left\u2080 (Real.sqrt_nonneg _) hTn 2\n rwa [Real.sq_sqrt (by positivity : (0 : \u211d) \u2264 (n : \u211d))] at h1\n have hker : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016kFun n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264 Real.exp 4 + 1 := by\n intro \u03c3 h\u03c3\n obtain \u27e8h\u03c31, h\u03c32\u27e9 := h\u03c3\n have hre : (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1).re = \u03c3 - 1 := by simp\n have him : (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1).im = T := by simp\n have h1 := kFun_shift_norm_le_exp_four_add_one (n := n)\n (s := (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - 1))\n (by rw [hre]; linarith [h\u03c32]) (by rw [him]; exact hnT2)\n rwa [sub_add_cancel] at h1\n -- pointwise Jlag \u2264 (e\u2074+1)\u00b7\u2016logDeriv\u2016\n have hptJ : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n (Real.exp 4 + 1) * \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := by\n intro \u03c3 h\u03c3\n rw [Jlag_norm_eq]\n exact mul_le_mul (hker \u03c3 h\u03c3) le_rfl (norm_nonneg _) (by positivity)\n have hJint : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n (Real.exp 4 + 1) * \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := by\n have h := intervalIntegral.integral_mono_on hlen hJintbl hKLintbl\n (fun \u03c3 h\u03c3 => hptJ \u03c3 h\u03c3)\n rwa [intervalIntegral.integral_const_mul] at h\n -- the logDeriv split: \u2016logDeriv\u2016 \u2264 \u2016\u03a3\u2016 + \u2016logDeriv \u2212 \u03a3\u2016\n have hsumcont : Continuous fun \u03c3 : \u211d =>\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n hSnorm_cont.add hRcont\n have hsum_intbl : IntervalIntegrable\n (fun \u03c3 : \u211d => \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)\n MeasureTheory.volume (-5 / 2) 3 := hsumcont.intervalIntegrable _ _\n have hsplit : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) +\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) := by\n have hpt2 : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 \u2264\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 +\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n fun \u03c3 _ => norm_le_insert' _ _\n have h := intervalIntegral.integral_mono_on hlen hLDintbl hsum_intbl\n (fun \u03c3 h\u03c3 => hpt2 \u03c3 h\u03c3)\n rwa [intervalIntegral.integral_add hSnorm_int hRnorm_int] at h\n -- the R-part integral (the 5f capstone, constant in \u03c3)\n have hR : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n 10.5 * Real.log (T + 2) + 48 := by\n intro \u03c3 h\u03c3\n obtain \u27e8h\u03c31, h\u03c32\u27e9 := h\u03c3\n have hre : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).re = \u03c3 := by simp\n have him : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).im = T := by simp\n have h := logDeriv_riemannZeta_sub_nearZeros_le_tight (t := T)\n (s := ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)) hZC hZC2 hNLZ h10T\n (by rw [hre]; exact h\u03c31) (by rw [hre]; exact h\u03c32) him (hzne \u03c3)\n rwa [abs_of_nonneg hT0] at h\n have hRint : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) := by\n have h := intervalIntegral.integral_mono_on hlen hRnorm_int intervalIntegrable_const\n (fun \u03c3 h\u03c3 => hR \u03c3 h\u03c3)\n rwa [intervalIntegral.integral_const, smul_eq_mul] at h\n -- the near-sum integral: the per-zero arcsinh-FTC machine + the swap\n have hnormid : \u2200 \u03c3 : \u211d, \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1},\n \u2016((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1\u2016 =\n Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2) := by\n intro \u03c3 \u03c1\n have h1 : Complex.normSq (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1) =\n (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n symm\n rw [Real.sqrt_eq_iff_eq_sq (by positivity) (norm_nonneg _),\n \u2190 Complex.normSq_eq_norm_sq]\n exact h1.symm\n have htermcont : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n Continuous fun \u03c3 : \u211d => (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n intro \u03c1 h\u03c1\n obtain \u27e8h\u03b4pos, -, -\u27e9 := h\u03c1data \u03c1 h\u03c1\n have hh : \u2200 \u03c3 : \u211d, (0 : \u211d) < (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2 := by\n intro \u03c3\n have h3 : \u03c1.1.im - T \u2260 0 := abs_pos.mp h\u03b4pos\n have h4 : T - \u03c1.1.im \u2260 0 := by\n intro h5\n apply h3\n linarith [h5]\n exact add_pos_of_nonneg_of_pos (sq_nonneg _) (sq_pos_of_ne_zero h4)\n have hsqrtc : Continuous fun \u03c3 : \u211d =>\n Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2) :=\n Real.continuous_sqrt.comp (by fun_prop :\n Continuous fun \u03c3 : \u211d => (\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)\n have hsqrt0 : \u2200 \u03c3 : \u211d,\n Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2) \u2260 0 :=\n fun \u03c3 => ne_of_gt (Real.sqrt_pos.mpr (hh \u03c3))\n show Continuous ((fun _ : \u211d => (zeroMult \u03c1.1 : \u211d)) *\n ((fun _ : \u211d => (1 : \u211d)) /\n (fun \u03c3 : \u211d => Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2))))\n exact Continuous.mul continuous_const\n (Continuous.div continuous_const hsqrtc hsqrt0)\n -- pointwise: \u2016\u03a3\u2016 \u2264 \u03a3 mult\u00b7(1/\u221a)\n have hpt : \u2200 \u03c3 : \u211d, \u03c3 \u2208 Set.Icc (-5 / 2 : \u211d) 3 \u2192\n \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n intro \u03c3 _\n calc \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016\n \u2264 \u2211 \u03c1 \u2208 nearZerosSub T, \u2016(zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 :=\n norm_sum_le _ _\n _ = \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) /\n \u2016((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1\u2016 := by\n apply Finset.sum_congr rfl\n intro \u03c1 _\n rw [norm_div]\n have h2 : \u2016(zeroMult \u03c1.1 : \u2102)\u2016 = (zeroMult \u03c1.1 : \u211d) := by\n rw [show (zeroMult \u03c1.1 : \u2102) = ((zeroMult \u03c1.1 : \u211d) : \u2102) by\n push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (Nat.cast_nonneg _)\n rw [h2]\n _ = \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n apply Finset.sum_congr rfl\n intro \u03c1 _\n rw [hnormid \u03c3 \u03c1, mul_one_div]\n -- the swap \u222b\u03a3 = \u03a3\u222b\n have hswap : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n (\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2))) =\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n rw [intervalIntegral.integral_finsetSum\n (fun \u03c1 h\u03c1 => (htermcont \u03c1 h\u03c1).intervalIntegrable _ _)]\n apply Finset.sum_congr rfl\n intro \u03c1 _\n exact intervalIntegral.integral_const_mul _ _\n -- per-\u03c1: the integral \u2264 2\u00b7log(148.5\u00b7\u0108\u2080(\u221an+2))\n have hper : \u2200 \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, \u03c1 \u2208 nearZerosSub T \u2192\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) \u2264\n 2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) := by\n intro \u03c1 h\u03c1\n obtain \u27e8h\u03b4pos, h\u03b41, h\u03b4ge\u27e9 := h\u03c1data \u03c1 h\u03c1\n have hsq : (T - \u03c1.1.im) ^ 2 = |\u03c1.1.im - T| ^ 2 := by\n rw [sq_abs (\u03c1.1.im - T)]\n ring\n have hmain := per_zero_integral_le_two_log \u03c1.2.2.1 \u03c1.2.2.2 h\u03b4pos h\u03b41.le\n rw [hsq]\n have hinv : 1 / |\u03c1.1.im - T| \u2264 9 * C0hat (Real.sqrt (n : \u211d) + 2) := by\n have h := one_div_le_one_div_of_le (one_div_pos.mpr (by positivity :\n (0 : \u211d) < 9 * C0hat (Real.sqrt (n : \u211d) + 2))) h\u03b4ge\n rwa [one_div_one_div] at h\n have h1 : (16.5 : \u211d) * (1 / |\u03c1.1.im - T|) \u2264\n 16.5 * (9 * C0hat (Real.sqrt (n : \u211d) + 2)) :=\n mul_le_mul_of_nonneg_left hinv (by norm_num)\n have h2 : (16.5 : \u211d) / |\u03c1.1.im - T| \u2264 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) := by\n rw [mul_one_div, show (16.5 : \u211d) * (9 * C0hat (Real.sqrt (n : \u211d) + 2)) =\n 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) by ring] at h1\n exact h1\n have h3 : Real.log (16.5 / |\u03c1.1.im - T|) \u2264\n Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) :=\n Real.log_le_log (by positivity) h2\n linarith [hmain, h3]\n -- the sum bound: \u03a3 mult\u00b7\u222b \u2264 (2\u00b7log(148.5\u00b7\u0108\u2080))\u00b7Z\u2082(T)\n have hsum : \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) \u2264\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T := by\n calc \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n 1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2))\n \u2264 \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) := by\n apply Finset.sum_le_sum\n intro \u03c1 h\u03c1\n exact mul_le_mul_of_nonneg_left (hper \u03c1 h\u03c1) (Nat.cast_nonneg _)\n _ = (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) *\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) := by\n rw [\u2190 Finset.sum_mul, mul_comm]\n _ \u2264 (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T :=\n mul_le_mul_of_nonneg_left (nearZerosSub_mult_sum_le hZC2 h10T) hB0nn\n -- the near-sum integral bound\n have hRHScont : Continuous fun \u03c3 : \u211d =>\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2)) := by\n exact continuous_finsetSum _ (fun \u03c1 h\u03c1 => htermcont \u03c1 h\u03c1)\n have hSbound : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n (2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T := by\n have h1 : \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016 \u2264\n \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n (\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u211d) *\n (1 / Real.sqrt ((\u03c3 - \u03c1.1.re) ^ 2 + (T - \u03c1.1.im) ^ 2))) :=\n intervalIntegral.integral_mono_on hlen hSnorm_int\n (hRHScont.intervalIntegrable _ _) (fun \u03c3 h\u03c3 => hpt \u03c3 h\u03c3)\n exact h1.trans (hswap.trans_le hsum)\n -- assembly\n unfold HIntegral\n calc \u2016\u222b x in (-5 / 2 : \u211d)..(3 : \u211d), Jlag n ((x : \u211d) + (T : \u211d) * Complex.I)\u2016\n \u2264 \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 :=\n intervalIntegral.norm_integral_le_integral_norm hlen\n _ \u2264 (Real.exp 4 + 1) * \u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I)\u2016 := hJint\n _ \u2264 (Real.exp 4 + 1) *\n ((\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d), \u2016\u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016) +\n (\u222b \u03c3 in (-5 / 2 : \u211d)..(3 : \u211d),\n \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) -\n \u2211 \u03c1 \u2208 nearZerosSub T, (zeroMult \u03c1.1 : \u2102) /\n (((\u03c3 : \u211d) + (T : \u211d) * Complex.I) - \u03c1.1)\u2016)) :=\n mul_le_mul_of_nonneg_left hsplit (by positivity)\n _ \u2264 (Real.exp 4 + 1) *\n ((2 * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2))) * Z2hat T +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) :=\n mul_le_mul_of_nonneg_left (add_le_add hSbound hRint) (by positivity)\n _ = (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by ring\n\n/-- **6-c-iv (the bottom side \u2212T)**: the conj trick (DL-5 pattern). -/\ntheorem hIntegral_Jlag_mid_neg_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) (-5 / 2) 3 (-T)\u2016 \u2264\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) := by\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hT0 : (0 : \u211d) < T := by\n have h1 : (0 : \u211d) < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr (by linarith)\n linarith\n have hconj : HIntegral (Jlag n) (-5 / 2) 3 (-T) =\n (starRingEnd \u2102) (HIntegral (Jlag n) (-5 / 2) 3 T) := by\n unfold HIntegral\n rw [\u2190 intervalIntegral.intervalIntegral_conj]\n apply intervalIntegral.integral_congr\n intro \u03c3 h\u03c3\n show Jlag n ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) (Jlag n ((\u03c3 : \u211d) + T * Complex.I))\n have hid2 : ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by simp\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((\u03c3 : \u211d) + T * Complex.I)).im = T := by simp\n rw [h] at him\n simp at him\n linarith [hT0])\n rw [hconj, Complex.norm_conj]\n exact hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n\n/-! ## 5. 6-c-v: the full horizontal assembly (mid + DL-5 tails) -/\n\n/-- **6-c-v (the +T full horizontal side)**: split at 3 \u2014 the 6-c-iv mid\nbound + the DL-5 dog-leg tail charge. -/\ntheorem hIntegral_Jlag_full_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T\u2016 \u2264\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : \u211d) := by\n classical\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have h10T : (10 : \u211d) \u2264 T := by\n have h1 : (10 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n linarith\n have hT0 : (0 : \u211d) < T := by linarith\n have hn1 : 1 \u2264 n := by omega\n have hn16 : 16 \u2264 n := by omega\n have h3le : (3 : \u211d) \u2264 2 * Real.sqrt (n : \u211d) := by\n have h1 : (10 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n nlinarith [h1]\n -- the mid-path continuity (zero-free via the wide pigeonhole)\n have hJcontP : \u2200 \u03c3 : \u211d, ContinuousAt (Jlag n) ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n intro \u03c3\n have hs1 : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) \u2260 1 := by\n intro h\n have him := congrArg Complex.im h\n simp at him\n linarith [hT0]\n have hA := (kFun_differentiableAt (n := n) hs1).continuousAt\n have hB := continuousAt_logDeriv_zeta hs1 (zeta_ne_zero_horizontal hTwide hn1 hTn hTn1)\n show ContinuousAt (fun s => kFun n s * (-logDeriv riemannZeta s)) _\n exact hA.mul hB.neg\n have hpath : Continuous fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I) := by\n fun_prop\n have hcontJP : Continuous fun \u03c3 : \u211d => Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) := by\n rw [continuous_iff_continuousAt]\n intro \u03c3\n have hf : ContinuousAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) \u03c3 :=\n hpath.continuousAt\n exact ContinuousAt.comp (g := Jlag n)\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3) (hJcontP \u03c3) hf\n have hInt1 : IntervalIntegrable (fun \u03c3 : \u211d => Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I))\n MeasureTheory.volume (-5 / 2) 3 := hcontJP.intervalIntegrable _ _\n -- the tail-path continuity (zero-free by re \u2265 3 > 1, DL-1)\n have hInt2 : IntervalIntegrable (fun \u03c3 : \u211d => Jlag n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I))\n MeasureTheory.volume 3 (2 * Real.sqrt (n : \u211d)) := by\n apply ContinuousOn.intervalIntegrable\n rw [Set.uIcc_of_le h3le]\n intro \u03c3 h\u03c3\n obtain \u27e8h\u03c31, h\u03c32\u27e9 := h\u03c3\n have hre : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).re = \u03c3 := by simp\n have him : ((\u03c3 : \u211d) + (T : \u211d) * Complex.I).im = T := by simp\n have hg : ContinuousWithinAt (Jlag n)\n (Set.range fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I))\n ((\u03c3 : \u211d) + (T : \u211d) * Complex.I) :=\n (Jlag_differentiableAt_dogleg (s := ((\u03c3 : \u211d) + (T : \u211d) * Complex.I))\n (by rw [hre]; exact h\u03c31) (by rw [him]; exact hT0)).continuousAt.continuousWithinAt\n have hfp : ContinuousWithinAt (fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I))\n (Set.Icc 3 (2 * Real.sqrt (n : \u211d))) \u03c3 := hpath.continuousWithinAt\n exact ContinuousWithinAt.comp (g := Jlag n)\n (f := fun u : \u211d => ((u : \u211d) + (T : \u211d) * Complex.I)) (x := \u03c3) hg hfp\n (Set.mapsTo_range _ _)\n -- split at 3 and assemble\n have hsplit : HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T =\n HIntegral (Jlag n) (-5 / 2) 3 T + HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T :=\n HIntegral_split hInt1 hInt2\n have hmid := hIntegral_Jlag_mid_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n have htail := hIntegral_Jlag_low_le_dogLegUpper hn16 hTn hTn1\n have hDLR : DogLegRight (n : \u211d) = ((Real.sqrt (n : \u211d) + 1) / 2) *\n (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) + IIMaj (n : \u211d) / 4 := rfl\n rw [hsplit, hDLR]\n calc \u2016HIntegral (Jlag n) (-5 / 2) 3 T +\n HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016\n \u2264 \u2016HIntegral (Jlag n) (-5 / 2) 3 T\u2016 +\n \u2016HIntegral (Jlag n) 3 (2 * Real.sqrt (n : \u211d)) T\u2016 := norm_add_le _ _\n _ \u2264 (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) +\n (((Real.sqrt (n : \u211d) + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + (8.38 : \u211d) +\n IIMaj (n : \u211d) / 4) :=\n add_le_add hmid htail\n\n/-- **6-c-v (the \u2212T full horizontal side)**: the conj trick at the full\nlevel (no split needed \u2014 intervalIntegral_conj is unconditional). -/\ntheorem hIntegral_Jlag_full_neg_norm_le (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : \u211d) := by\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hT0 : (0 : \u211d) < T := by\n have h1 : (0 : \u211d) < Real.sqrt (n : \u211d) := Real.sqrt_pos.mpr (by linarith)\n linarith\n have hconj : HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T) =\n (starRingEnd \u2102) (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T) := by\n unfold HIntegral\n rw [\u2190 intervalIntegral.intervalIntegral_conj]\n apply intervalIntegral.integral_congr\n intro \u03c3 h\u03c3\n show Jlag n ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) (Jlag n ((\u03c3 : \u211d) + T * Complex.I))\n have hid2 : ((\u03c3 : \u211d) + (((-T : \u211d)) : \u2102) * Complex.I) =\n (starRingEnd \u2102) ((\u03c3 : \u211d) + T * Complex.I) := by simp\n rw [hid2]\n exact Jlag_conj n (by\n intro h\n have him : (((\u03c3 : \u211d) + T * Complex.I)).im = T := by simp\n rw [h] at him\n simp at him\n linarith [hT0])\n rw [hconj, Complex.norm_conj]\n exact hIntegral_Jlag_full_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1\n\n/-- **6-c-v (the two horizontal sides)**: the horizontal assembly charge \u2014\n2\u00b7(mid bound) + 2\u00b7DogLegRight. -/\ntheorem hIntegral_Jlag_full_two_sides (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2)\n (hNLZ : NoLowZeros) {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTwide : \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 Real.sqrt (n : \u211d) - 1 < \u03c1.im \u2192\n \u03c1.im < Real.sqrt (n : \u211d) + 2 \u2192\n 1 / (9 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264 |\u03c1.im - T|)\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n \u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T\u2016 +\n \u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T)\u2016 \u2264\n 2 * ((Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : \u211d)) := by\n rw [show (2 : \u211d) * ((Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : \u211d)) =\n ((Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : \u211d)) +\n ((Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48)) + DogLegRight (n : \u211d)) by ring]\n exact add_le_add (hIntegral_Jlag_full_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1)\n (hIntegral_Jlag_full_neg_norm_le hZC hZC2 hNLZ hn hTwide hTn hTn1)\n\n/-! ## 6. 6-d: the fold \u2014 `sfBoundProp : SfBoundProp` -/\n\n/-- \u0108\u2080(t) \u2264 t for t \u2265 8 (via log x \u2264 x/e with 1/e \u2264 0.36789 certified\nfrom e > 2.7182818283, and loglog x \u2264 log x \u2212 1). -/\ntheorem C0hat_le_self {t : \u211d} (ht : 8 \u2264 t) : C0hat t \u2264 t := by\n have ht2 : (0 : \u211d) < t + 2 := by linarith\n have ht1 : (1 : \u211d) < t + 2 := by linarith\n have hinv : (1 : \u211d) / Real.exp 1 \u2264 0.36789 := by\n rw [div_le_iff\u2080 (Real.exp_pos 1)]\n nlinarith [Real.exp_one_gt_d9]\n have hL1 : Real.log (t + 2) \u2264 (t + 2) / Real.exp 1 := by\n have h1 := Real.log_le_sub_one_of_pos (div_pos ht2 (Real.exp_pos 1))\n have h2 : Real.log ((t + 2) / Real.exp 1) = Real.log (t + 2) - 1 := by\n rw [Real.log_div (ne_of_gt ht2) (Real.exp_pos 1).ne', Real.log_exp]\n rw [h2] at h1\n linarith [h1]\n have hL : Real.log (t + 2) \u2264 (t + 2) * 0.36789 := by\n have h3 : (t + 2) / Real.exp 1 \u2264 (t + 2) * 0.36789 := by\n rw [div_eq_mul_one_div]\n exact mul_le_mul_of_nonneg_left hinv ht2.le\n exact hL1.trans h3\n have hLL : Real.log (Real.log (t + 2)) \u2264 (t + 2) * 0.36789 := by\n have h1 := Real.log_le_sub_one_of_pos (Real.log_pos ht1)\n nlinarith [h1, hL]\n unfold C0hat\n nlinarith [hL, hLL, ht]\n\n/-- **The horizontal pinch** (the E-030 V3 \u2264 0.40 witness made analytic):\nthe near-sum integral + the R-part \u2264 7\u00b7H\u0302(T). Chain (all elementary, no\ncertified log numerics): \u0108\u2080(\u221an+2) \u2264 \u221an+2 (\u0108\u2080(t) \u2264 t, t \u2265 318), so\n148.5\u00b7\u0108\u2080(\u221an+2) \u2264 (\u221an+2)\u00b2 and its log \u2264 2\u00b7log(T+2); Z\u2082(T) \u2264 2\u00b7\u0108\u2080(T);\n\u0108\u2080(T) \u2265 0.433\u00b7log(T+2) with 8 \u2264 21\u00b70.433 = 9.093; 5.5 \u2264 7 on the R-part. -/\ntheorem pinch_horizontal {n : \u2115} (hn : 100000 \u2264 n) {T : \u211d}\n (hTn : Real.sqrt (n : \u211d) \u2264 T) (_hTn1 : T \u2264 Real.sqrt (n : \u211d) + 1) :\n 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48) \u2264 7 * Hhat T := by\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hsqrt316 : (316 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have hT1 : (1 : \u211d) \u2264 T := by nlinarith [hsqrt316, hTn]\n have hT0 : (0 : \u211d) < T := by nlinarith\n -- (a) log(148.5\u00b7\u0108\u2080(\u221an+2)) \u2264 2\u00b7log(T+2)\n have hC0le : C0hat (Real.sqrt (n : \u211d) + 2) \u2264 Real.sqrt (n : \u211d) + 2 :=\n C0hat_le_self (by nlinarith [hsqrt316])\n have h148 : (148.5 : \u211d) \u2264 Real.sqrt (n : \u211d) + 2 := by nlinarith [hsqrt316]\n have hC0pos : (0 : \u211d) < C0hat (Real.sqrt (n : \u211d) + 2) := by\n have h2 := two_le_C0hat (by nlinarith [Real.sqrt_nonneg (n : \u211d)] :\n (1 : \u211d) \u2264 Real.sqrt (n : \u211d) + 2)\n linarith\n have hsq1 : 148.5 * C0hat (Real.sqrt (n : \u211d) + 2) \u2264 (Real.sqrt (n : \u211d) + 2) ^ 2 := by\n have h1 := mul_le_mul hC0le h148 (by norm_num : (0 : \u211d) \u2264 (148.5 : \u211d))\n (by positivity : (0 : \u211d) \u2264 Real.sqrt (n : \u211d) + 2)\n nlinarith [h1, hC0pos.le]\n have hlogarg : Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264\n 2 * Real.log (T + 2) := by\n have h2 := Real.log_le_log (by positivity) hsq1\n have h3 : Real.log ((Real.sqrt (n : \u211d) + 2) ^ 2) = 2 * Real.log (Real.sqrt (n : \u211d) + 2) := by\n rw [Real.log_pow]\n ring\n have h4 : Real.log (Real.sqrt (n : \u211d) + 2) \u2264 Real.log (T + 2) :=\n Real.log_le_log (by positivity) (by linarith [hTn])\n linarith [h2, h3, h4]\n -- (b) Z\u2082(T) \u2264 2\u00b7\u0108\u2080(T)\n have hZ2le : Z2hat T \u2264 2 * C0hat T := by\n have hL1 : (1 : \u211d) \u2264 Real.log (T + 2) := by\n have ht2 : (0 : \u211d) < T + 2 := by linarith\n rw [Real.le_log_iff_exp_le ht2]\n have he := Real.exp_one_lt_d9.le\n linarith\n have hLL0 : (0 : \u211d) \u2264 Real.log (Real.log (T + 2)) := Real.log_nonneg hL1\n unfold Z2hat C0hat\n nlinarith [hL1, hLL0]\n -- (c) \u0108\u2080(T) \u2265 0.433\u00b7log(T+2)\n have hC0L : 0.433 * Real.log (T + 2) \u2264 C0hat T := by\n have hL1 : (1 : \u211d) \u2264 Real.log (T + 2) := by\n have ht2 : (0 : \u211d) < T + 2 := by linarith\n rw [Real.le_log_iff_exp_le ht2]\n have he := Real.exp_one_lt_d9.le\n linarith\n have hLL0 : (0 : \u211d) \u2264 Real.log (Real.log (T + 2)) := Real.log_nonneg hL1\n unfold C0hat\n nlinarith [hL1, hLL0]\n -- (d) the near part \u2264 21\u00b7\u0108\u2080(T)\u00b2\n have hlogT0 : (0 : \u211d) \u2264 Real.log (T + 2) := Real.log_nonneg (by linarith)\n have hC0T0 : (0 : \u211d) < C0hat T := by\n have h2 := two_le_C0hat hT1\n linarith\n have hnear : 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264\n 21 * C0hat T * C0hat T := by\n have h1 : 2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) \u2264\n 2 * Z2hat T * (2 * Real.log (T + 2)) := by\n have hnn : (0 : \u211d) \u2264 2 * Z2hat T := by\n have h := Z2hat_nonneg hT1\n positivity\n exact mul_le_mul_of_nonneg_left hlogarg hnn\n have hZ2L : Z2hat T * Real.log (T + 2) \u2264 2 * C0hat T * Real.log (T + 2) :=\n mul_le_mul_of_nonneg_right hZ2le hlogT0\n have h8 : 8 * Real.log (T + 2) \u2264 21 * C0hat T := by\n have h1 : (8 : \u211d) \u2264 21 * (0.433 : \u211d) := by norm_num\n nlinarith [hC0L, h1, hlogT0]\n have h3 : (8 * Real.log (T + 2)) * C0hat T \u2264 (21 * C0hat T) * C0hat T :=\n mul_le_mul h8 le_rfl hC0T0.le (by positivity : (0 : \u211d) \u2264 21 * C0hat T)\n nlinarith [h1, hZ2L, h3, hlogT0]\n -- (e) the 5.5 \u2264 7 part\n have hR0 : (0 : \u211d) \u2264 10.5 * Real.log (T + 2) + 48 := by\n have h1 := Real.log_nonneg (by linarith : (1 : \u211d) \u2264 T + 2)\n nlinarith\n have hR : (3 - -5 / 2 : \u211d) * (10.5 * Real.log (T + 2) + 48) \u2264\n 7 * (10.5 * Real.log (T + 2) + 48) := by\n have h55 : (3 - -5 / 2 : \u211d) = 5.5 := by norm_num\n rw [h55]\n nlinarith [hR0]\n -- final: 21\u00b7\u0108\u2080\u00b2 + 7\u00b7R = 7\u00b7H\u0302\n unfold Hhat\n nlinarith [hnear, hR]\n\n/-- **THE FOLD (ii\u2032-6-d)**: `SfBoundProp` from the six declared perimeter\nhypotheses \u2014 the 6-b sides identity + the bridge (both-signs 4F + triv \u2264 1),\nthe rectangle side decomposition, the four side bounds of ii\u2032-6-c, the\nhorizontal pinch, and the F-E absorption e^{1/3} \u2264 1.4 \u2264 2\u03c0. -/\ntheorem sfBoundProp (hRH : RHUpTo (3 * 10 ^ 12)) (hZC : ZeroCountProp)\n (hZC2 : ZeroCountProp2) (hZCG : ZeroCountGlobalProp) (hNLZ : NoLowZeros)\n (hMZ : MZeroProp) : SfBoundProp := by\n intro n hn hN1\n classical\n have hnR : (100000 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have hn1 : 1 \u2264 n := by omega\n have hn16 : 16 \u2264 n := by omega\n have hsqrt316 : (316 : \u211d) \u2264 Real.sqrt (n : \u211d) := by\n rw [Real.le_sqrt (by norm_num) (by positivity)]\n nlinarith [hnR]\n have ha : (3 : \u211d) \u2264 Real.sqrt (n : \u211d) := by nlinarith [hsqrt316]\n obtain \u27e8T, hTn, hTn1, hTwide\u27e9 := exists_zero_avoiding_T_wide hZC ha\n have hT1 : (1 : \u211d) \u2264 T := by nlinarith [hTn]\n have hT2 : (2 : \u211d) \u2264 T := by nlinarith\n have hT0 : (0 : \u211d) < T := by nlinarith\n -- T \u2264 3\u00b710\u00b9\u00b2 (from n \u2264 N\u2081; the bridge's internal RHUpTo range)\n have hTle : T \u2264 3 * 10 ^ 12 := by\n have h1 : Real.sqrt (n : \u211d) \u2264 3 * 10 ^ 12 - 1 := by\n have h2 := Real.sqrt_le_sqrt hN1\n rwa [Real.sqrt_sq (by norm_num : (0 : \u211d) \u2264 3 * 10 ^ 12 - 1)] at h2\n linarith [hTn1]\n -- the sides identity\n have hsf := sf_abs_le_rectInt_add_zeroSum hZC hn1 hT1 hTn hTn1 hTwide\n -- the bridge (variant with T \u2264 3\u00b710\u00b9\u00b2 \u2014 the internal range actually used)\n have hbridge : \u2016\u2211 \u03c1 \u2208 ((zeroBothWindow_finite T).toFinset \u222a {(-2 : \u2102)}),\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 \u2264 4 * FAlt T + 1 := by\n have h2not : (-2 : \u2102) \u2209 (zeroBothWindow_finite T).toFinset := by\n intro h\n have hnt := (zeroBothWindow_finite T).mem_toFinset.mp h |>.1\n have h21 : (0 : \u211d) < (-2 : \u2102).re := hnt.2.1\n norm_num at h21\n have hdisj2 : Disjoint (zeroBothWindow_finite T).toFinset {(-2 : \u2102)} := by\n rw [Finset.disjoint_left]\n intro \u03c1 h\u03c1 h\u03c12\n rw [Finset.mem_singleton] at h\u03c12\n exact h2not (h\u03c12 \u25b8 h\u03c1)\n rw [Finset.sum_union hdisj2, Finset.sum_singleton]\n have htriv := trivTerm_norm_le_one n\n have hbr := zeroSum_nontriv_norm_le hRH (n := n) (T := T) hTle\n have hcount := zeroBothWindow_sum_eq_two_mul hNLZ T\n have hZ := hZCG T hT2\n calc \u2016\u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset,\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n) +\n (zeroMult (-2 : \u2102) : \u2102) * (1 - ((-2 : \u2102) / (-2 - 1)) ^ n)\u2016\n \u2264 \u2016\u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset,\n (zeroMult \u03c1 : \u2102) * (1 - (\u03c1 / (\u03c1 - 1)) ^ n)\u2016 +\n \u2016(zeroMult (-2 : \u2102) : \u2102) * (1 - ((-2 : \u2102) / (-2 - 1)) ^ n)\u2016 := norm_add_le _ _\n _ \u2264 (2 * \u2211 \u03c1 \u2208 (zeroBothWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d)) + 1 := by\n linarith [hbr, htriv]\n _ = 2 * (2 * \u2211 \u03c1 \u2208 (zeroGlobalWindow_finite T).toFinset, (zeroMult \u03c1 : \u211d)) + 1 := by\n rw [hcount]\n _ \u2264 4 * FAlt T + 1 := by linarith [hZ]\n -- the four side bounds\n have hVl := vIntegral_Jlag_left_norm_le hZC hZC2 hNLZ hMZ hn hTn hTn1\n have hVr := vIntegral_Jlag_right_le_exp_third_IIMaj hn hTn hTn1\n have hH := hIntegral_Jlag_full_two_sides hZC hZC2 hNLZ hn hTwide hTn hTn1\n -- \u2016RectInt'\u2016 = (1/2\u03c0)\u00b7\u2016RectInt\u2016\n have hnorm : \u2016RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)\u2016 =\n (1 / (2 * Real.pi)) * \u2016RectangleIntegral (Jlag n) (rectZ T) (rectW n T)\u2016 := by\n unfold RectangleIntegral'\n rw [norm_smul]\n congr 1\n have h1 : \u2016(2 : \u2102) * (Real.pi : \u2102) * Complex.I\u2016 = 2 * Real.pi := by\n rw [norm_mul, Complex.norm_I, mul_one, norm_mul]\n have h3 : \u2016(2 : \u2102)\u2016 = (2 : \u211d) := by\n rw [show (2 : \u2102) = ((2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real]\n exact abs_of_nonneg (by norm_num)\n have h4 : \u2016(Real.pi : \u2102)\u2016 = Real.pi := by\n rw [Complex.norm_real]\n exact abs_of_nonneg Real.pi_nonneg\n rw [h3, h4]\n rw [norm_div, norm_one, h1]\n -- the rectangle norm triangle\n have htri : \u2016RectangleIntegral (Jlag n) (rectZ T) (rectW n T)\u2016 \u2264\n \u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T)\u2016 +\n \u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T\u2016 +\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T\u2016 +\n \u2016VIntegral (Jlag n) (-5 / 2) (-T) T\u2016 := by\n rw [rectangleIntegral_Jlag_eq n T]\n have h1 := norm_sub_le (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T) -\n HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T +\n VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T)\n (VIntegral (Jlag n) (-5 / 2) (-T) T)\n have h2 := norm_add_le (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T) -\n HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T)\n (VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T)\n have h3 := norm_sub_le (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T))\n (HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T)\n linarith [h1, h2, h3]\n -- the horizontal pinch\n have hpinch := pinch_horizontal hn hTn hTn1\n -- the F-E absorption: e^{1/3} \u2264 1.4 \u2264 2\u03c0\n have he13 : Real.exp (1 / 3 : \u211d) \u2264 2 * Real.pi := by\n have h1 : Real.exp (1 / 3 : \u211d) \u2264 1.4 := by\n have h2 : (Real.exp (1 / 3 : \u211d)) ^ 3 \u2264 (1.4 : \u211d) ^ 3 := by\n have h3 : (Real.exp (1 / 3 : \u211d)) ^ 3 = Real.exp 1 := by\n rw [\u2190 Real.exp_nat_mul (1 / 3 : \u211d) 3]\n congr 1\n norm_num\n rw [h3]\n have h4 : Real.exp 1 \u2264 2.7182818286 := Real.exp_one_lt_d9.le\n norm_num1 at \u22a2\n linarith only [h4]\n exact le_of_pow_le_pow_left\u2080 (by norm_num : (3 : \u2115) \u2260 0) (by norm_num : (0 : \u211d) \u2264 1.4) h2\n have h5 : (3 : \u211d) \u2264 Real.pi := Real.pi_gt_three.le\n nlinarith only [h1, h5]\n -- the 1/(2\u03c0) comparisons\n have h2\u03c0pos : (0 : \u211d) < 2 * Real.pi := by positivity\n have h2\u03c0le : (1 / (2 * Real.pi)) \u2264 1 := by\n rw [div_le_iff\u2080 h2\u03c0pos, one_mul]\n have h := Real.pi_gt_three.le\n linarith\n have he13' : Real.exp (1 / 3 : \u211d) / (2 * Real.pi) \u2264 1 := by\n rw [div_le_iff\u2080 h2\u03c0pos, one_mul]\n exact he13\n -- nonneg facts\n have hIIMaj0 : (0 : \u211d) \u2264 IIMaj (n : \u211d) := by unfold IIMaj; positivity\n have hDLR0 : (0 : \u211d) \u2264 DogLegRight (n : \u211d) := by unfold DogLegRight IIMaj; positivity\n have hC0T0 : (0 : \u211d) < C0hat T := by\n have h2 := two_le_C0hat hT1\n linarith\n have hHhat0 : (0 : \u211d) \u2264 Hhat T := by\n unfold Hhat\n have hL1 : (1 : \u211d) \u2264 Real.log (T + 2) := by\n have ht2 : (0 : \u211d) < T + 2 := by linarith\n rw [Real.le_log_iff_exp_le ht2]\n have he := Real.exp_one_lt_d9.le\n linarith\n nlinarith [hC0T0.le, hL1]\n have hX0 : (0 : \u211d) \u2264 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 := by\n have h1 := Z2hat_nonneg hT1\n have h2 := Real.log_nonneg (by linarith : (1 : \u211d) \u2264 T + 2)\n nlinarith [hT0.le]\n -- the T \u2264 \u221an+1 monotonicity comparisons\n have hsqrt0 : (0 : \u211d) \u2264 Real.sqrt (n : \u211d) := Real.sqrt_nonneg _\n have hlogT1 : (1 : \u211d) \u2264 Real.log (T + 2) := by\n have ht2 : (0 : \u211d) < T + 2 := by linarith\n rw [Real.le_log_iff_exp_le ht2]\n have he := Real.exp_one_lt_d9.le\n linarith\n have hFAlt : FAlt T \u2264 FAlt (Real.sqrt (n : \u211d) + 1) := by\n unfold FAlt\n have hT0' : (0 : \u211d) < T := hT0\n have hlog1 : (1 : \u211d) \u2264 Real.log T := by\n have ht2 : (0 : \u211d) < T := hT0\n rw [Real.le_log_iff_exp_le hT0]\n have he := Real.exp_one_lt_d9.le\n nlinarith [hTn, hsqrt316, he]\n have hA : T * Real.log T \u2264 (Real.sqrt (n : \u211d) + 1) * Real.log (Real.sqrt (n : \u211d) + 1) := by\n have h1 := Real.log_le_log hT0 (by linarith [hTn1] : T \u2264 Real.sqrt (n : \u211d) + 1)\n exact mul_le_mul hTn1 h1 (Real.log_nonneg hlog1) (by linarith [hsqrt0])\n have hB : Real.log T \u2264 Real.log (Real.sqrt (n : \u211d) + 1) :=\n Real.log_le_log hT0 (by linarith [hTn1])\n have hC : Real.log (Real.log T) \u2264 Real.log (Real.log (Real.sqrt (n : \u211d) + 1)) := by\n apply Real.log_le_log (by linarith [hlog1] : (0 : \u211d) < Real.log T)\n have h1 : (1 : \u211d) \u2264 Real.log (Real.sqrt (n : \u211d) + 1) := by\n have ht2 : (0 : \u211d) < Real.sqrt (n : \u211d) + 1 := by positivity\n rw [Real.le_log_iff_exp_le ht2]\n have he := Real.exp_one_lt_d9.le\n nlinarith [hsqrt316, he]\n have h2 : Real.log T \u2264 Real.log (Real.sqrt (n : \u211d) + 1) := hB\n linarith [h2, hlog1]\n have hconst : (0 : \u211d) \u2264 1 / (2 * Real.pi) := by positivity\n have hA' := mul_le_mul_of_nonneg_left hA hconst\n nlinarith [hA', hB, hC]\n have hX : 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) \u2264\n 4 * (Real.sqrt (n : \u211d) + 1) *\n ((2 / 3) * Z2hat (Real.sqrt (n : \u211d) + 1) + 10.5 * Real.log (Real.sqrt (n : \u211d) + 1 + 2) + 48) := by\n have hZ := Z2hat_mono hT1 hTn1\n have hlog := Real.log_le_log (by linarith : (0 : \u211d) < T + 2)\n (by linarith [hTn1] : T + 2 \u2264 Real.sqrt (n : \u211d) + 1 + 2)\n have hXle : (2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 \u2264\n (2 / 3) * Z2hat (Real.sqrt (n : \u211d) + 1) + 10.5 * Real.log (Real.sqrt (n : \u211d) + 1 + 2) + 48 := by\n nlinarith [hZ, hlog]\n have hX0' : (0 : \u211d) \u2264 (2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48 := by\n have h1 := Z2hat_nonneg hT1\n nlinarith [hlogT1]\n have h4 : T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) \u2264\n (Real.sqrt (n : \u211d) + 1) *\n ((2 / 3) * Z2hat (Real.sqrt (n : \u211d) + 1) + 10.5 * Real.log (Real.sqrt (n : \u211d) + 1 + 2) + 48) :=\n mul_le_mul hTn1 hXle hX0' (by linarith [hsqrt0])\n nlinarith [h4]\n have hHhat : Hhat T \u2264 Hhat (Real.sqrt (n : \u211d) + 1) := by\n unfold Hhat\n have hC := C0hat_mono hT1 hTn1\n have hC2 : C0hat T ^ 2 \u2264 C0hat (Real.sqrt (n : \u211d) + 1) ^ 2 :=\n pow_le_pow_left\u2080 hC0T0.le hC 2\n have hlog := Real.log_le_log (by linarith : (0 : \u211d) < T + 2)\n (by linarith [hTn1] : T + 2 \u2264 Real.sqrt (n : \u211d) + 1 + 2)\n nlinarith [hC2, hlog]\n -- the Bn unfold\n have hBn : Bn FAlt (n : \u211d) = 4 * FAlt (Real.sqrt (n : \u211d) + 1) +\n 4 * (Real.sqrt (n : \u211d) + 1) *\n ((2 / 3) * Z2hat (Real.sqrt (n : \u211d) + 1) + 10.5 * Real.log (Real.sqrt (n : \u211d) + 1 + 2) + 48) +\n 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat (Real.sqrt (n : \u211d) + 1)) +\n 2 * DogLegRight (n : \u211d) + IIMaj (n : \u211d) + 1 := by\n unfold Bn\n rfl\n rw [hBn]\n -- the IIMaj absorption: (1/2\u03c0)\u00b7e^{1/3}\u00b7IIMaj \u2264 IIMaj\n have hIIMajAbs : (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d)) \u2264\n IIMaj (n : \u211d) := by\n have h1 := mul_le_mul_of_nonneg_right he13' hIIMaj0\n calc (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d))\n = ((1 / (2 * Real.pi)) * Real.exp (1 / 3 : \u211d)) * IIMaj (n : \u211d) := by ring\n _ \u2264 1 * IIMaj (n : \u211d) := h1\n _ = IIMaj (n : \u211d) := by ring\n -- the Hhat absorption: (1/2\u03c0)\u00b7Y \u2264 Y for Y \u2265 0\n have hHhatAbs : (1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1) * (7 * Hhat T)) \u2264\n 2 * (Real.exp 4 + 1) * (7 * Hhat T) := by\n have hY : (0 : \u211d) \u2264 2 * (Real.exp 4 + 1) * (7 * Hhat T) := by\n have h1 : (0 : \u211d) \u2264 7 * Hhat T := by nlinarith [hHhat0]\n positivity\n have h1 := mul_le_mul_of_nonneg_right h2\u03c0le hY\n rwa [one_mul] at h1\n have hDLRAbs : (1 / (2 * Real.pi)) * (2 * DogLegRight (n : \u211d)) \u2264 2 * DogLegRight (n : \u211d) := by\n have h1 := mul_le_mul_of_nonneg_right h2\u03c0le hDLR0\n rwa [one_mul] at h1\n have hXAbs : (1 / (2 * Real.pi)) * (4 * T *\n ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352) \u2264\n 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) + 40 * 1.3352 := by\n have h1 := mul_le_mul_of_nonneg_right h2\u03c0le hX0\n rwa [one_mul] at h1\n -- the mid-bound pinch absorption: (1/2\u03c0)\u00b72(e\u2074+1)(NI+5.5R) \u2264 (1/2\u03c0)\u00b72(e\u2074+1)\u00b77\u00b7H\u0302\n have hPinchAbs : (1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1) *\n (2 * Z2hat T * Real.log (148.5 * C0hat (Real.sqrt (n : \u211d) + 2)) +\n (3 - -5 / 2) * (10.5 * Real.log (T + 2) + 48))) \u2264\n (1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1) * (7 * Hhat T)) := by\n have h1 := mul_le_mul_of_nonneg_left hpinch (by positivity :\n (0 : \u211d) \u2264 (1 / (2 * Real.pi)) * (2 * (Real.exp 4 + 1)))\n convert h1 using 1\n \u00b7 ring\n \u00b7 ring\n -- the giant assembly\n have hnormRect : \u2016RectangleIntegral' (Jlag n) (rectZ T) (rectW n T)\u2016 \u2264\n (1 / (2 * Real.pi)) *\n (\u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) (-T)\u2016 +\n \u2016HIntegral (Jlag n) (-5 / 2) (2 * Real.sqrt (n : \u211d)) T\u2016 +\n \u2016VIntegral (Jlag n) (2 * Real.sqrt (n : \u211d)) (-T) T\u2016 +\n \u2016VIntegral (Jlag n) (-5 / 2) (-T) T\u2016) := by\n rw [hnorm]\n have h1 := mul_le_mul_of_nonneg_left htri (by positivity : (0 : \u211d) \u2264 1 / (2 * Real.pi))\n exact h1\n -- the per-side (1/2\u03c0)-scaled bounds (atom-mults linarith can't do)\n have hVr' := mul_le_mul_of_nonneg_left hVr (by positivity : (0 : \u211d) \u2264 1 / (2 * Real.pi))\n have hVl' := mul_le_mul_of_nonneg_left hVl (by positivity : (0 : \u211d) \u2264 1 / (2 * Real.pi))\n have hH' := mul_le_mul_of_nonneg_left hH (by positivity : (0 : \u211d) \u2264 1 / (2 * Real.pi))\n -- |Sf n| \u2264 \u2016RectInt'\u2016 + \u2016\u03a3\u2016, now everything slots in\n nlinarith [hsf, hnormRect, hVl', hVr', hH', hbridge, hIIMajAbs, hHhatAbs,\n hDLRAbs, hXAbs, hPinchAbs, hFAlt, hX, hHhat, hIIMaj0, hDLR0, hHhat0, hX0]\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 1654,
"oldLines": 7,
"newStart": 1654,
"newLines": 7,
"lines": [
" IIMaj (n : \u211d) := by",
" have h1 := mul_le_mul_of_nonneg_right he13' hIIMaj0",
" calc (1 / (2 * Real.pi)) * (Real.exp (1 / 3 : \u211d) * IIMaj (n : \u211d))",
"- = ((1 / (2 * Real.pi)) * Real.exp (1 / 3 : \u211d)) * IIMaj (n : \u211d) := by ring",
"+ = (Real.exp (1 / 3 : \u211d) / (2 * Real.pi)) * IIMaj (n : \u211d) := by ring",
" _ \u2264 1 * IIMaj (n : \u211d) := h1",
" _ = IIMaj (n : \u211d) := by ring",
" -- the Hhat absorption: (1/2\u03c0)\u00b7Y \u2264 Y for Y \u2265 0"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"Still inf for log log T, L2², L2 — the print only shows rel_dev; those have |v_hand| ≤ 1e-15 somewhere? No wait — psi_max is −7e-5 for log log T, so |v_hand| ≥ 7e-5 everywhere... then rel should be computable. The inf must come from the lambdified sympy form producing nan/inf at some T (overflow warnings: T**(1−2T) at T=3.1e12 → T**huge → inf → log(inf) = inf → rel inf). The v_sym values may contain inf at large T — but psi_max negative everywhere passed?? If v_sym had +inf, max would be inf > 0 → negative_everywhere False → but v2 check... let me check the JSON all-checks and exit code. The printed psi_max for log log T = −7.456e-05 (finite) — so v_sym is finite-negative; then rel_dev inf means diff/|v_hand| had an inf — i.e., v_sym = inf somewhere?? but then psi_max would be inf. Contradiction unless nan: max with nan — np.max propagates nan... hmm psi_max is finite so no nan in v_sym. Then rel inf requires |v_hand| tiny with finite diff — but we masked |v_hand| ≤ 1e-15 to 0.0 via np.where — EXCEPT np.where evaluates BOTH branches: diff/|v_hand| computed everywhere first → inf warning but masked... np.where mask sets those entries 0. But rel printed inf — so some |v_hand| > 1e-15 has diff/|v_hand| = inf → v_sym = ±inf there — but then psi_max ≥ ... psi_max is the max — if v_sym = −inf at some point, max unaffected; diff = |−inf − v_hand| = inf → rel = inf. So v_sym hits −inf at some large T (log(T**(1−2T)) overflow → log(0)?? T**(1−2T) = T^{−6e12} → underflows to 0 → log(0) = −inf). So v_sym has −inf at the largest T values, while v_hand is fine (−1e-25). ψ negative everywhere still true (−inf < 0 ✓). The rel_dev inf is cosmetic; the abs dev check: diff inf → max_abs_dev = inf → v1 fails! Exit code? The script printed no failure... let me check JSON.\n\nBetter fix: restrict symbolic evaluation to T ≤ 1e6 (where no overflow; the hand sign arguments cover the asymptotics anyway) and evaluate v_hand on the full grid. Or evaluate psi_sym via mpmath (subs) at sample points — slow but only 11×50. Simplest: tpts for the match check = geomspace(T0, 1e6, 200); negativity grid separate (full range, using hand forms which are stable). Edit: in build_table, use tpts_match = geomspace(T0, 1e6, 200) for v_sym/v_hand comparison, and check negativity of v_sym on that plus v_hand on the full grid.","signature":""},{"type":"text","text":"The `inf` is sympy's lambdified form underflowing at huge T (e.g., `T**(1−2T)` → log(0) = −inf) — cosmetic but it fails the metric. Restricting the symbolic-match grid to T ≤ 10⁶ and checking negativity on the full grid via the stable hand forms."},{"type":"tool_use","id":"Edit_178","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\numerics\\scripts\\E-029-convexity.py","new_string":" rows = []\n tpts = np.geomspace(T0, 1e6, 300) # symbolic-match grid\n tpts_full = np.geomspace(T0, 3.1e12, 400) # negativity grid\n for name, phi, psi_hand in phis:\n psi_sym = sp.lambdify(\n T, sp.simplify(sp.diff(phi, T, 2)\n - sp.diff(phi, T) / (T - 1)), \"numpy\")\n v_sym = psi_sym(tpts)\n v_hand = psi_hand(tpts)\n diff = np.abs(v_sym - v_hand)\n rel = float(np.max(np.where(np.abs(v_hand) > 1e-15,\n diff / np.abs(v_hand), 0.0)))\n absd = float(np.max(diff))\n rows.append({\"block\": name, \"max_rel_dev\": rel,\n \"max_abs_dev\": absd,\n \"psi_max_on_grid\":\n float(max(np.max(v_sym),\n np.max(psi_hand(tpts_full)))),\n \"negative_everywhere\":\n bool(np.max(v_sym) < 0\n and np.max(psi_hand(tpts_full)) < 0)})\n return rows","old_string":" rows = []\n tpts = np.geomspace(T0, 3.1e12, 400)\n for name, phi, psi_hand in phis:\n psi_sym = sp.lambdify(\n T, sp.simplify(sp.diff(phi, T, 2)\n - sp.diff(phi, T) / (T - 1)), \"numpy\")\n v_sym = psi_sym(tpts)\n v_hand = psi_hand(tpts)\n diff = np.abs(v_sym - v_hand)\n rel = float(np.max(np.where(np.abs(v_hand) > 1e-15,\n diff / np.abs(v_hand), 0.0)))\n absd = float(np.max(diff))\n rows.append({\"block\": name, \"max_rel_dev\": rel,\n \"max_abs_dev\": absd,\n \"psi_max_on_grid\": float(np.max(v_sym)),\n \"negative_everywhere\": bool(np.max(v_sym) < 0)})\n return rows","replace_all":false},"extra_content":null}]