LiSkeleton.lean
2828 lines · 115 declarations · 0 sorries · updated 08-26-2026
Declarations
| Kind | Name | Line |
|---|---|---|
| def | liSummand | 46 |
| lemma | summand_conj | 50 |
| lemma | liSummand_eq | 54 |
| def | liCoeff | 63 |
| lemma | pow_one_add_inv_two_mul_le | 68 |
| lemma | re_li_summand_le | 89 |
| lemma | normSq_gammaOf_le_mul_norm_sq | 226 |
| lemma | liSummand_norm | 249 |
| lemma | liSummand_norm_le | 256 |
| theorem | liSummable | 290 |
| def | RHUpTo | 354 |
| def | LiVerifiedUpTo | 361 |
| def | lagariasA1 | 375 |
| def | SInfty | 380 |
| def | lagariasC1 | 386 |
| def | sInftyLower | 391 |
| theorem | bern_term_nonneg | 396 |
| theorem | bern_term_upper | 414 |
| theorem | sInf_series_summable | 477 |
| theorem | harmonic_lower | 495 |
| theorem | harmonic_upper | 503 |
| theorem | bern_term_lower | 511 |
| theorem | sInf_partial_lower | 530 |
| theorem | oddHarm_eq | 582 |
| theorem | oddHarm_lower | 610 |
| theorem | sInfty_lower_bound | 627 |
| def | C0hat | 736 |
| def | Z2hat | 745 |
| def | Hhat | 749 |
| def | IIMaj | 754 |
| def | DogLegRight | 762 |
| def | marginTilde | 773 |
| theorem | deriv2_of_hasDerivAt_nhds | 785 |
| def | psiOf | 792 |
| theorem | psiOf_id | 795 |
| theorem | psiOf_log_shift | 808 |
| theorem | psiOf_log_shift_neg | 830 |
| theorem | hasDerivAt_log_shift | 842 |
| theorem | hasDerivAt_log_log | 849 |
| theorem | block_range_bounds | 859 |
| theorem | psiOf_log_log_shift | 886 |
| theorem | psiOf_log_log_shift_neg | 936 |
| theorem | psiOf_log_sq_shift | 952 |
| theorem | psiOf_log_sq_shift_neg | 987 |
| theorem | psiOf_log_mul_log_shift | 998 |
| theorem | psiOf_log_mul_log_shift_neg | 1047 |
| theorem | psiOf_log_log_sq_shift | 1063 |
| theorem | psiOf_log_log_sq_shift_neg | 1120 |
| theorem | psiOf_T_mul_log_shift | 1138 |
| theorem | psiOf_T_mul_log_shift_neg | 1180 |
| theorem | psiOf_T_mul_log_log_shift | 1199 |
| theorem | psiOf_T_mul_log_log_shift_neg | 1262 |
| theorem | IIMaj_eq_psiTilde_sqrt | 1310 |
| theorem | IIMaj_le_two_mul | 1347 |
| theorem | IIMaj_nonneg | 1371 |
| theorem | psiTilde_contDiff | 1382 |
| theorem | hasDerivAt_psiTilde | 1389 |
| theorem | deriv_psiTilde | 1408 |
| theorem | deriv2_psiTilde | 1415 |
| theorem | iim_u2_antitone | 1452 |
| theorem | iimaj_bracket_bound | 1511 |
| theorem | contDiffOn_L1 | 1693 |
| theorem | contDiffOn_L2 | 1698 |
| theorem | contDiffOn_L1sq | 1704 |
| theorem | contDiffOn_L1L2 | 1708 |
| theorem | contDiffOn_L2sq | 1712 |
| theorem | contDiffOn_TL1 | 1716 |
| theorem | contDiffOn_TL2 | 1720 |
| theorem | contDiffOn_sqrt_shift | 1726 |
| theorem | mapsTo_sqrt_shift | 1732 |
| theorem | mapsTo_sqrt_shift_Ioi1 | 1741 |
| theorem | mapsTo_sqrt_shift_Ici_Ioi1 | 1749 |
| theorem | psiOf_sqrt_rel | 1758 |
| theorem | deriv2_add | 1766 |
| theorem | deriv2_const_mul | 1779 |
| theorem | deriv2_const_val | 1791 |
| theorem | hasDerivAt_marginS | 1798 |
| theorem | marginS_deriv2 | 1808 |
| theorem | marginTilde_eq_expanded | 1854 |
| theorem | contDiffOn_mS | 1862 |
| theorem | contDiffOn_mFblock | 1869 |
| theorem | contDiffOn_mTL1b | 1874 |
| theorem | contDiffOn_mTL2b | 1877 |
| theorem | contDiffOn_mIdb | 1880 |
| theorem | contDiffOn_mL1sqb | 1883 |
| theorem | contDiffOn_mL1L2b | 1886 |
| theorem | contDiffOn_mL2sqb | 1889 |
| theorem | contDiffOn_mL1b | 1892 |
| theorem | contDiffOn_mL2b | 1895 |
| theorem | contDiffOn_mIIM | 1898 |
| theorem | continuousOn_marginExpanded | 1913 |
| theorem | contDiffOn_marginExpanded | 1952 |
| theorem | chain_rule_sqrt_shift_on | 1968 |
| theorem | chain_rule_sqrt | 2042 |
| theorem | chain_rule_sqrt_shift | 2094 |
| theorem | IIMaj_deriv2_lt_three | 2159 |
| theorem | marginTilde_convex | 2187 |
| def | FAlt | 2444 |
| def | Bn | 2464 |
| theorem | marginTilde_eq_sub | 2472 |
| def | Sf | 2481 |
| def | SfBoundProp | 2490 |
| theorem | hasDerivAt_T_mul_log | 2497 |
| theorem | psiOf_T_mul_log | 2503 |
| theorem | psiOf_T_mul_log_neg | 2519 |
| theorem | psiOf_log | 2531 |
| theorem | psiOf_log_neg | 2549 |
| theorem | hasDerivAt_log_log_unshifted | 2560 |
| theorem | psiOf_log_log | 2569 |
| theorem | psiOf_log_log_neg | 2606 |
| theorem | contDiffOn_FAlt | 2623 |
| theorem | FAlt_psi_neg | 2641 |
| theorem | pos_of_convex_of_base | 2729 |
| theorem | pos_of_convex_of_two_points | 2768 |
| theorem | lambda_pos_finite_height | 2800 |
Source
/-
NguyenRH1/LiSkeleton.lean — formalization of paper draft.tex §3.1
(R-004 finite-height Li theorem + archimedean lower bound + margin
convexity mechanism).
Conventions follow zeta-23-lean's hypothesis-driven style (cf. Zeta23.Final):
the computational inputs (Platt–Trudgian RH-to-height; finite Li
verification) are named Prop hypotheses, exactly as Zeta23 treats hEF/hRvM.
Status (session 012): TIER (i) COMPLETE (session 011: sInfty_lower_bound,
marginTilde_convex, chain_rule_sqrt_shift). TIER (ii) STEP 1 COMPLETE
(session 012): `lambda_pos_finite_height` is PROVED modulo its named
hypotheses — the assembly is conditional only on `SfBoundProp` (the
isolated analytic obligation, triaged in D-062), the computational
perimeter (`RHUpTo`, `LiVerifiedUpTo`), and two elementary margin
evaluations (hbase/hbase2, E-028/E-029 values; their interval-bound
discharge is tier (ii) step 2). No `sorry` remains in this file;
`#print axioms` shows only the three standard axioms for every
declaration here.
Archive references: R-004, D-037, D-056, D-057, D-062, E-023, E-028, E-029.
-/
import Mathlib
import Zeta23.Statement
import Zeta23.WeilEF.ZeroSummability
import Zeta23.Statement.SeamClosed
open Zeta23 Complex Filter Topology
noncomputable section
namespace NguyenRH1
/-! ## 1. The Keiper–Li coefficients -/
/-- The paired (symmetrized) Li summand: ½·mult·(f ρ + f ρ̄),
f ρ = 1 − (1−1/ρ)ⁿ. Manifestly real-valued (`liSummand_eq`), absolutely
summable (`liSummable`) — the correct Keiper–Li summand.
(Session-015 ii′-1a, D-064 §1: the plain unordered sum of f over the
zeros is NOT absolutely summable for any n ≥ 1 — the summand is
~ n/|γ| for large |γ| and Σ mult/|ρ| = ∞ — so the previous direct
definition evaluated to the junk value 0 and `LiVerifiedUpTo`/
`SfBoundProp` were FALSE as encoded. The pairing is the classical
Bombieri–Lagarias symmetric convention and restores the intended
meaning; summability is proved below.) -/
def liSummand (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) : ℂ :=
(zeroMult ρ : ℂ) / 2 *
((1 - (1 - 1 / (ρ : ℂ)) ^ n) + (1 - (1 - 1 / ((starRingEnd ℂ) (ρ : ℂ))) ^ n))
lemma summand_conj (n : ℕ) (z : ℂ) :
(1 : ℂ) - (1 - 1 / ((starRingEnd ℂ) z)) ^ n = (starRingEnd ℂ) ((1 - (1 - 1 / z) ^ n)) := by
rw [map_sub, map_one, map_pow, map_sub, map_one, map_div₀, map_one]
lemma liSummand_eq (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :
liSummand n ρ = (zeroMult ρ : ℂ) * (((1 - (1 - 1 / (ρ : ℂ)) ^ n).re) : ℂ) := by
rw [liSummand, summand_conj, Complex.add_conj]
push_cast
ring
/-- The Keiper–Li coefficient λ_n as the paired zero-side sum with
multiplicity (draft §3.1; Zeta23's IsNontrivialZero/zeroMult
conventions; D-064 §1). Summability: `liSummable`. -/
def liCoeff (n : ℕ) : ℂ := ∑' ρ : {ρ : ℂ // IsNontrivialZero ρ}, liSummand n ρ
/-! ### 1a. The geometric-sum estimate: |Re(1 − wⁿ)| ≤ 2n²/‖z‖² (w = 1−1/z) -/
/-- (1 + 1/(2n))ⁿ ≤ 2 for n ≥ 1. Via (1+x)ⁿ ≤ exp(nx) and exp(1/2) ≤ 2. -/
lemma pow_one_add_inv_two_mul_le (n : ℕ) (hn : 1 ≤ n) :
((1 : ℝ) + 1 / (2 * n)) ^ n ≤ 2 := by
have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
have hbase : (1 : ℝ) + 1 / (2 * n) ≤ Real.exp (1 / (2 * n)) := by
have h := Real.add_one_le_exp (1 / (2 * (n : ℝ)))
linarith
have h1 : ((1 : ℝ) + 1 / (2 * n)) ^ n ≤ Real.exp (1 / 2) := by
calc ((1 : ℝ) + 1 / (2 * n)) ^ n
≤ (Real.exp (1 / (2 * n))) ^ n := pow_le_pow_left₀ (by positivity) hbase n
_ = Real.exp (↑n * (1 / (2 * n))) := by rw [Real.exp_nat_mul]
_ = Real.exp (1 / 2) := by congr 1; field_simp
have h2 : Real.exp (1 / 2 : ℝ) ≤ 2 := by
have h3 : (1 : ℝ) / 2 ≤ Real.log 2 := by
have h := Real.log_two_gt_d9
linarith
calc Real.exp (1 / 2 : ℝ) ≤ Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3
_ = 2 := Real.exp_log (by norm_num)
exact h1.trans h2
/-- Key estimate: for n ≥ 1, z with re z ∈ [0,1], 2n ≤ ‖z‖:
|Re(1 − (1−1/z)ⁿ)| ≤ 2n²/‖z‖². -/
lemma re_li_summand_le {n : ℕ} (hn : 1 ≤ n) {z : ℂ}
(hzre0 : 0 ≤ z.re) (hzre1 : z.re ≤ 1) (hz : 2 * n ≤ ‖z‖) :
|(1 - (1 - 1 / z) ^ n).re| ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by
have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
have hz0 : z ≠ 0 := by
intro h; rw [h, norm_zero] at hz; linarith
have hzn : (0 : ℝ) < ‖z‖ := norm_pos_iff.mpr hz0
have hnsq : Complex.normSq z = ‖z‖ ^ 2 := Complex.normSq_eq_norm_sq z
set M : ℝ := 1 + 1 / (2 * (n : ℝ)) with hM
have hM0 : (0 : ℝ) ≤ 1 / (2 * (n : ℝ)) := by positivity
have hM1 : (1 : ℝ) ≤ M := le_add_of_nonneg_right hM0
set w : ℂ := 1 - 1 / z with hw
have hgeom : (w - 1) * ∑ j ∈ Finset.range n, w ^ j = w ^ n - 1 := mul_geom_sum w n
have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring
have hf : (1 : ℂ) - w ^ n = (1 / z) * ∑ j ∈ Finset.range n, w ^ j := by
have e : (1 : ℂ) - w ^ n = -(w ^ n - 1) := by ring
rw [e, ← hgeom, hw1]; ring
set S : ℂ := ∑ j ∈ Finset.range n, w ^ j
have hwnorm : ‖w‖ ≤ 1 + 1 / ‖z‖ := by
have e : w = 1 - z⁻¹ := by rw [hw, div_eq_mul_inv, one_mul]
rw [e]
calc ‖(1 : ℂ) - z⁻¹‖ ≤ ‖(1 : ℂ)‖ + ‖z⁻¹‖ := norm_sub_le _ _
_ = 1 + 1 / ‖z‖ := by rw [norm_one, norm_inv, inv_eq_one_div]
have h1z : 1 / ‖z‖ ≤ 1 / (2 * n) :=
one_div_le_one_div_of_le (by positivity) (by exact_mod_cast hz)
have hwmax : max 1 ‖w‖ ≤ M := by
apply max_le hM1
exact hwnorm.trans (by rw [hM]; linarith)
have hSn : ‖S - n‖ ≤ n ^ 2 / ‖z‖ := by
have hSn1 : S - n = ∑ j ∈ Finset.range n, (w ^ j - 1) := by
have e : (n : ℂ) = ∑ j ∈ Finset.range n, (1 : ℂ) := by
simp [Finset.sum_const, Finset.card_range]
rw [e, ← Finset.sum_sub_distrib]
rw [hSn1]
have hbound : ∀ j ∈ Finset.range n,
‖w ^ j - 1‖ ≤ (1 / ‖z‖) * (j * M ^ (n - 1)) := by
intro j hj
have hgeomj : (w - 1) * ∑ i ∈ Finset.range j, w ^ i = w ^ j - 1 := mul_geom_sum w j
have h2 : w ^ j - 1 = -(1 / z) * ∑ i ∈ Finset.range j, w ^ i := by
rw [← hgeomj, hw1]
rw [h2, norm_mul, norm_neg, norm_div, norm_one]
have hsum : ‖∑ i ∈ Finset.range j, w ^ i‖ ≤ j * M ^ (n - 1) := by
calc ‖∑ i ∈ Finset.range j, w ^ i‖
≤ ∑ i ∈ Finset.range j, ‖w ^ i‖ := norm_sum_le _ _
_ ≤ ∑ i ∈ Finset.range j, M ^ (n - 1) := by
apply Finset.sum_le_sum
intro i hi
rw [norm_pow]
have hij : i < j := Finset.mem_range.mp hi
have hjn : j ≤ n := le_of_lt (Finset.mem_range.mp hj)
have h1 : ‖w‖ ^ i ≤ M ^ i :=
pow_le_pow_left₀ (norm_nonneg _)
(le_trans (le_max_right 1 ‖w‖) hwmax) i
have h2 : M ^ i ≤ M ^ (n - 1) := pow_le_pow_right₀ hM1 (by omega)
exact h1.trans h2
_ = j * M ^ (n - 1) := by
rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
exact mul_le_mul_of_nonneg_left hsum (by positivity)
calc ‖∑ j ∈ Finset.range n, (w ^ j - 1)‖
≤ ∑ j ∈ Finset.range n, ‖w ^ j - 1‖ := norm_sum_le _ _
_ ≤ ∑ j ∈ Finset.range n, (1 / ‖z‖) * (j * M ^ (n - 1)) :=
Finset.sum_le_sum hbound
_ = ((1 / ‖z‖) * M ^ (n - 1)) * ∑ j ∈ Finset.range n, (j : ℝ) := by
symm
rw [Finset.mul_sum]
apply Finset.sum_congr rfl
intro j _; ring
_ ≤ n ^ 2 / ‖z‖ := by
have hsumj : (∑ j ∈ Finset.range n, (j : ℝ)) = (n : ℝ) * ((n : ℝ) - 1) / 2 := by
have h6 := congrArg (Nat.cast : ℕ → ℝ) (Finset.sum_range_id_mul_two n)
simp only [Nat.cast_mul, Nat.cast_sub hn, Nat.cast_ofNat, Nat.cast_one] at h6
have h7 : (∑ j ∈ Finset.range n, (j : ℝ)) =
((∑ j ∈ Finset.range n, j : ℕ) : ℝ) := (Nat.cast_sum _ _).symm
rw [h7]
linarith
rw [hsumj]
have hpow : M ^ (n - 1) ≤ 2 :=
le_trans (pow_le_pow_right₀ hM1 (Nat.sub_le n 1))
(pow_one_add_inv_two_mul_le n hn)
have hb1 : (n : ℝ) * (n - 1) / 2 ≤ n ^ 2 / 2 := by nlinarith [hn0]
have hb2 : M ^ (n - 1) * (n * (n - 1) / 2) ≤ 2 * (n ^ 2 / 2) :=
mul_le_mul_of_nonneg hpow hb1 (by positivity) (by positivity)
have hb3 : ((1 : ℝ) / ‖z‖) * (M ^ (n - 1) * (n * (n - 1) / 2))
≤ (1 / ‖z‖) * (2 * (n ^ 2 / 2)) :=
mul_le_mul_of_nonneg_left hb2 (by positivity)
calc (1 / ‖z‖) * M ^ (n - 1) * (↑n * (↑n - 1) / 2)
= (1 / ‖z‖) * (M ^ (n - 1) * (↑n * (↑n - 1) / 2)) := by ring
_ ≤ (1 / ‖z‖) * (2 * (↑n ^ 2 / 2)) := hb3
_ = ↑n ^ 2 / ‖z‖ := by ring
have hre1 : ((n : ℂ) * (1 / z)).re = n * z.re / ‖z‖ ^ 2 := by
have hinv : ((1 : ℂ) / z).re = z.re / ‖z‖ ^ 2 := by
rw [one_div, Complex.inv_re, hnsq]
have e : ((n : ℂ) * (1 / z)).re = n * ((1 : ℂ) / z).re := by
rw [Complex.mul_re]
simp
rw [e, hinv]
ring
have hfre : (1 - w ^ n).re = n * z.re / ‖z‖ ^ 2 + ((S - n) / z).re := by
have hd : (1 / z) * ((n : ℂ) + (S - n)) = (n : ℂ) * (1 / z) + (S - n) / z := by
ring
rw [hf]
nth_rewrite 1 [show S = (n : ℂ) + (S - n) from by ring]
rw [hd, Complex.add_re, hre1]
rw [hfre]
have hA : |n * z.re / ‖z‖ ^ 2| ≤ n / ‖z‖ ^ 2 := by
have e : |n * z.re / ‖z‖ ^ 2| = n * |z.re| / ‖z‖ ^ 2 := by
rw [abs_div, abs_mul, abs_of_nonneg hn0.le,
abs_of_nonneg (sq_nonneg ‖z‖)]
rw [e, div_le_iff₀ (by positivity)]
have e2 : (n / ‖z‖ ^ 2) * ‖z‖ ^ 2 = n := by field_simp
rw [e2]
calc n * |z.re| ≤ n * 1 :=
mul_le_mul_of_nonneg_left (abs_le.mpr ⟨by linarith, hzre1⟩) hn0.le
_ = n := mul_one _
have hB : |((S - n) / z).re| ≤ n ^ 2 / ‖z‖ ^ 2 := by
have h1 : |((S - n) / z).re| ≤ ‖(S - n) / z‖ := Complex.abs_re_le_norm _
have h2 : ‖(S - n) / z‖ ≤ (n ^ 2 / ‖z‖) / ‖z‖ := by
rw [norm_div, div_le_iff₀ hzn]
have e : ((n ^ 2 / ‖z‖) / ‖z‖) * ‖z‖ = n ^ 2 / ‖z‖ := by field_simp
rw [e]
exact hSn
exact h1.trans (h2.trans (by rw [div_div, ← pow_two]))
have hnn : (n : ℝ) ≤ n ^ 2 := by
have h : (1 : ℝ) ≤ n := by exact_mod_cast hn
nlinarith
calc |n * z.re / ‖z‖ ^ 2 + ((S - n) / z).re|
≤ n / ‖z‖ ^ 2 + n ^ 2 / ‖z‖ ^ 2 := (abs_add_le _ _).trans (add_le_add hA hB)
_ = (n + n ^ 2) / ‖z‖ ^ 2 := by ring
_ ≤ 2 * n ^ 2 / ‖z‖ ^ 2 := by
rw [div_le_iff₀ (by positivity)]
have e : (2 * n ^ 2 / ‖z‖ ^ 2) * ‖z‖ ^ 2 = 2 * n ^ 2 := by field_simp
rw [e]
linarith
/-! ### 1b. The comparison 1 + ‖γ_ρ‖² ≤ (9/4)‖ρ‖² and summability -/
/-- For re z ∈ [0,1] and 2n ≤ ‖z‖ (n ≥ 1): 1 + ‖γ_z‖² ≤ (9/4)·‖z‖². -/
lemma normSq_gammaOf_le_mul_norm_sq {n : ℕ} (hn : 1 ≤ n) {z : ℂ}
(hzre0 : 0 ≤ z.re) (hzre1 : z.re ≤ 1) (hz : 2 * n ≤ ‖z‖) :
1 + Complex.normSq (gammaOf z) ≤ 9 / 4 * ‖z‖ ^ 2 := by
have hn0 : (0 : ℝ) < n := by exact_mod_cast hn
have hz2 : ‖z‖ ^ 2 = z.re ^ 2 + z.im ^ 2 := by
rw [← Complex.normSq_eq_norm_sq, Complex.normSq_apply]
ring
have hz4 : 4 * n ^ 2 ≤ ‖z‖ ^ 2 := by
have h := pow_le_pow_left₀ (by positivity : (0:ℝ) ≤ 2 * n) hz 2
nlinarith [h]
have hre2 : z.re ^ 2 ≤ 1 := by nlinarith [hzre0, hzre1]
have hn1 : (1 : ℝ) ≤ n := by exact_mod_cast hn
have hn4 : (4 : ℝ) ≤ 4 * (n : ℝ) ^ 2 := by
have h := pow_le_pow_left₀ (show (0 : ℝ) ≤ 1 by norm_num) hn1 2
nlinarith [h]
have him : 1 ≤ z.im ^ 2 := by nlinarith [hz2, hz4, hre2, hn4]
have hgam : Complex.normSq (gammaOf z) = z.im ^ 2 + (1 / 2 - z.re) ^ 2 := by
rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]
ring
rw [hgam, hz2]
nlinarith [hzre0, hzre1, him, sq_nonneg (1 / 2 - z.re), sq_nonneg z.re]
/-- Norm of the paired summand: mult·|Re f(ρ)|. -/
lemma liSummand_norm (n : ℕ) (ρ : {ρ : ℂ // IsNontrivialZero ρ}) :
‖liSummand n ρ‖ = (zeroMult ρ : ℝ) * |(1 - (1 - 1 / (ρ : ℂ)) ^ n).re| := by
rw [liSummand_eq n ρ, norm_mul, RCLike.norm_natCast]
congr 1
exact RCLike.norm_ofReal _
/-- The main bound: for 2n ≤ ‖ρ‖, ‖liSummand n ρ‖ ≤ (9/2)n²·mult/(1+‖γ_ρ‖²). -/
lemma liSummand_norm_le {n : ℕ} (hn : 1 ≤ n) (ρ : {ρ : ℂ // IsNontrivialZero ρ})
(hρ : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖) :
‖liSummand n ρ‖ ≤
(9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
have hz := ρ.2
have hre0 : 0 ≤ (ρ : ℂ).re := hz.2.1.le
have hre1 : (ρ : ℂ).re ≤ 1 := hz.2.2.le
have hcore := re_li_summand_le hn hre0 hre1 hρ
have hcomp := normSq_gammaOf_le_mul_norm_sq hn hre0 hre1 hρ
have hnpos : (0 : ℝ) < n := by exact_mod_cast hn
have hz0 : (0 : ℝ) < ‖(ρ : ℂ)‖ := lt_of_lt_of_le (by positivity) hρ
have hz0' : ‖(ρ : ℂ)‖ ≠ 0 := ne_of_gt hz0
have hg0 : (0 : ℝ) < 1 + Complex.normSq (gammaOf (ρ : ℂ)) := by
have h := Complex.normSq_nonneg (gammaOf (ρ : ℂ))
linarith
have key : (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2)
≤ (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf (ρ : ℂ))) := by
rw [le_div_iff₀ hg0]
have hbound : (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) *
(1 + Complex.normSq (gammaOf (ρ : ℂ)))
≤ (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) * ((9 / 4) * ‖(ρ : ℂ)‖ ^ 2) :=
mul_le_mul_of_nonneg_left hcomp (by positivity)
have heq : (zeroMult ρ : ℝ) * (2 * n ^ 2 / ‖(ρ : ℂ)‖ ^ 2) * ((9 / 4) * ‖(ρ : ℂ)‖ ^ 2)
= (9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) := by
field_simp
ring
exact hbound.trans (le_of_eq heq)
rw [liSummand_norm]
exact (mul_le_mul_of_nonneg_left hcore (Nat.cast_nonneg _)).trans key
/-- The paired Li summand is absolutely summable over the nontrivial zeros.
Uses Zeta23's `WeilEF.zero_sum_inv_sq` (Σ mult/(1+‖γ_ρ‖²) < ∞, proved) via
the tail bound of `liSummand_norm_le`; the ball {‖ρ‖ < 2n} contributes a
finite set (Mathlib `IsCompact.inter_riemannZetaZeros_finite`). -/
theorem liSummable (n : ℕ) : Summable (liSummand n) := by
rcases Nat.eq_zero_or_pos n with h0 | hn
· subst h0
have h : liSummand 0 = fun _ => (0 : ℂ) := by
funext ρ
simp [liSummand]
rw [h]
exact summable_zero
· have hbase : Summable (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
(9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ)))) := by
have h := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9 / 2) * (n : ℝ) ^ 2)
exact h
set D : {ρ : ℂ // IsNontrivialZero ρ} → ℝ := fun ρ =>
if (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖ then
(9 / 2) * n ^ 2 * (zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))
else ‖liSummand n ρ‖ with hDdef
have hfin : {ρ : {ρ // IsNontrivialZero ρ} | ¬ ((2 : ℝ) * n ≤ ‖(ρ : ℂ)‖)}.Finite := by
have hcomp : IsCompact (Metric.closedBall (0 : ℂ) (2 * n)) :=
isCompact_closedBall _ _
have hzeros : (Metric.closedBall (0 : ℂ) (2 * n)) ∩ {ρ : ℂ | IsNontrivialZero ρ}
⊆ (Metric.closedBall (0 : ℂ) (2 * n)) ∩ riemannZetaZeros := by
intro z hz
exact ⟨hz.1, hz.2.1⟩
have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros
have himg : (Subtype.val '' {ρ : {ρ // IsNontrivialZero ρ} |
¬ ((2 : ℝ) * n ≤ ‖(ρ : ℂ)‖)}).Finite := by
apply hfin2.subset
rintro z ⟨ρ, hρ, rfl⟩
refine ⟨?_, ρ.2⟩
simp only [Metric.mem_closedBall, dist_zero_right]
exact le_of_lt (lt_of_not_ge hρ)
exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)
have hE : Summable (fun ρ : {ρ // IsNontrivialZero ρ} =>
D ρ - (9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) /
(1 + Complex.normSq (gammaOf ρ)))) := by
apply summable_of_hasFiniteSupport
apply hfin.subset
intro ρ hρ
simp only [Function.mem_support, ne_eq] at hρ
by_contra hball
apply hρ
have hball' : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖ := not_not.mp hball
simp only [D, if_pos hball']
ring
have hD : Summable D := by
have hsum := hbase.add hE
have heq : (fun ρ : {ρ : ℂ // IsNontrivialZero ρ} =>
(9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) / (1 + Complex.normSq (gammaOf ρ))) +
(D ρ - (9 / 2) * (n : ℝ) ^ 2 * ((zeroMult ρ : ℝ) /
(1 + Complex.normSq (gammaOf ρ))))) = D := by
funext ρ
ring
rw [heq] at hsum
exact hsum
refine Summable.of_norm_bounded hD (fun ρ => ?_)
by_cases hρ : (2 : ℝ) * n ≤ ‖(ρ : ℂ)‖
· simp only [D, if_pos hρ]
exact liSummand_norm_le hn ρ hρ
· simp only [D, if_neg hρ, le_refl]
/-- "RH verified to height T₀": every nontrivial zero with |Im ρ| ≤ T₀ is
on the critical line. Platt–Trudgian 2021 (interval arithmetic) is the
T₀ = 3×10¹² instance; treated here as a hypothesis, mirroring Zeta23's
literature-hypothesis style. -/
def RHUpTo (T₀ : ℝ) : Prop :=
∀ ρ : ℂ, IsNontrivialZero ρ → |ρ.im| ≤ T₀ → ρ.re = 1 / 2
/-- "Li coefficients verified positive up to N" (computational input:
this project to N = 3000 (E-011/E-015, two independent methods);
Johansson 2015 § 4.2 to N = 10⁵ — rigorous interval-arithmetic computation of the ordinary Keiper–Li coefficients, all positive). λ_n is real (conjugate symmetry of the
zero set); the skeleton states positivity of the real part. -/
def LiVerifiedUpTo (N : ℕ) : Prop :=
∀ n : ℕ, 1 ≤ n → n ≤ N → 0 < (liCoeff n).re
/- [PROVED session 012, tier (ii) step 1 — assembly modulo the named
analytic hypothesis] R-004, the finite-height Li theorem (draft Thm 3.1).
The full statement and proof are at the END of this file (§4), after the
margin machinery they depend on: `lambda_pos_finite_height` there is
proved from `SfBoundProp` (the single named analytic hypothesis, D-062
triage) + the computational perimeter (Platt–Trudgian `RHUpTo`,
`LiVerifiedUpTo`) + two elementary margin evaluations. -/
/-! ## 2. The archimedean lower bound (D-037 Step 1) -/
/-- a₁ = (log 4π + γ)/2, the j = 1 Lagarias coefficient. -/
def lagariasA1 : ℝ := (Real.log (4 * Real.pi) + Real.eulerMascheroniConstant) / 2
/-- S_∞(n) in the exact odd-m identity form (D-037):
S_∞(n) = (1−a₁)n − 1 + Σ_{m ≥ 3, odd} [(1−1/m)ⁿ − 1 + n/m].
(Same tsum-summability honesty note as liCoeff.) -/
def SInfty (n : ℕ) : ℝ :=
(1 - lagariasA1) * n - 1 +
tsum fun m : {m : ℕ // Odd m ∧ 3 ≤ m} =>
((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ))
/-- C₁ = (γ − 1 − log 2π)/2 (D-037). -/
def lagariasC1 : ℝ :=
(Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2
/-- The explicit archimedean lower bound S(n) = ½n log n + (C₁−γ/2)n − 4
(D-037 (3.1)); named so the assembly can refer to it. -/
def sInftyLower (n : ℝ) : ℝ :=
(1 / 2) * n * Real.log n + (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4
/-- [PROVED session 011] h⁺(m) ≥ 0 for m ≥ 1: first-order Bernoulli,
(1−1/m)ⁿ ≥ 1 − n/m. (D-037 §3, "h⁺ ≥ max(0, n/m − 1)".) -/
theorem bern_term_nonneg (n : ℕ) (m : ℕ) (hm : 1 ≤ m) :
0 ≤ (1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / m := by
have hm0 : (m : ℝ) ≠ 0 := by positivity
have h1 : (1 : ℝ) + n * (-1 / m) ≤ (1 + -1 / (m : ℝ)) ^ n := by
apply one_add_mul_le_pow
have h3 : (0 : ℝ) ≤ 1 / (m : ℝ) := by positivity
have h4 : (1 : ℝ) / m ≤ 1 := by
rw [div_le_one (by positivity)]; exact_mod_cast hm
rw [neg_div]
linarith
have h2 : (1 : ℝ) - n / m ≤ (1 - 1 / m) ^ n := by
have : (1 : ℝ) + n * (-1 / m) = 1 - n / m := by field_simp; ring
rwa [this, show (1 : ℝ) + -1 / m = 1 - 1 / m by ring] at h1
linarith
/-- [PROVED session 011] h⁺(m) ≤ n(n−1)/(2m²) for m ≥ 1: geometric
factorization 1 − (1−x)ⁿ = x·Σ_{j<n} (1−x)ʲ plus Bernoulli per term.
(D-037 §3's "terms ~ C(n,2)/m²"; the summability input.) -/
theorem bern_term_upper (n : ℕ) (m : ℕ) (hm : 1 ≤ m) :
(1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / m ≤ (n : ℝ) * (n - 1) / (2 * m ^ 2) := by
have hm0 : (m : ℝ) ≠ 0 := by positivity
set x := (1 : ℝ) / m with hxdef
have hx1 : x ≤ 1 := by
rw [hxdef, div_le_one (by positivity)]; exact_mod_cast hm
have hx0 : 0 ≤ x := by positivity
have hterm : ∀ j : ℕ, 1 - j * x ≤ (1 - x) ^ j := by
intro j
have := one_add_mul_le_pow (a := -x) (by linarith : (-2 : ℝ) ≤ -x) j
rwa [show (1 : ℝ) + j * (-x) = 1 - j * x by ring,
show (1 : ℝ) + -x = 1 - x by ring] at this
have hsum : ∑ j ∈ Finset.range n, (j : ℝ) = (n : ℝ) * (n - 1) / 2 := by
have h := Finset.sum_range_id_mul_two n
have hcast : (((∑ i ∈ Finset.range n, i) * 2 : ℕ) : ℝ) = ((n * (n - 1) : ℕ) : ℝ) := by
exact_mod_cast h
rcases Nat.eq_zero_or_pos n with rfl | hnpos
· simp
· push_cast at hcast
rw [Nat.cast_sub hnpos] at hcast
push_cast at hcast
linarith
have hgeom : (1 - (1 - x) ^ n) = x * ∑ j ∈ Finset.range n, (1 - x) ^ j := by
have h := geom_sum_mul (1 - x) n
have hx1' : (1 - x) - 1 = -x := by ring
rw [hx1'] at h
linarith
have hmain : (1 - x) ^ n - 1 + (n : ℝ) * x ≤ (n : ℝ) * (n - 1) / 2 * x ^ 2 := by
have h4 : (n : ℝ) * x - (n * (n - 1) / 2) * x ^ 2 ≤ 1 - (1 - x) ^ n := by
rw [hgeom]
have h5 : (n : ℝ) - x * ((n : ℝ) * (n - 1) / 2) ≤
∑ j ∈ Finset.range n, (1 - x) ^ j := by
have h6 : ∑ j ∈ Finset.range n, (1 - (j : ℝ) * x) =
(n : ℝ) - x * ∑ j ∈ Finset.range n, (j : ℝ) := by
have e1 : ∑ j ∈ Finset.range n, (1 - (j : ℝ) * x) =
(∑ j ∈ Finset.range n, (1 : ℝ)) - ∑ j ∈ Finset.range n, (j : ℝ) * x :=
Finset.sum_sub_distrib (f := fun j : ℕ => (1 : ℝ)) (g := fun j : ℕ => (j : ℝ) * x)
have e2 : ∑ j ∈ Finset.range n, (1 : ℝ) = (n : ℝ) := by simp
have e3 : ∑ j ∈ Finset.range n, (j : ℝ) * x =
x * ∑ j ∈ Finset.range n, (j : ℝ) := by
rw [Finset.mul_sum]
refine Finset.sum_congr rfl fun j _ => ?_
ring
rw [e1, e2, e3]
rw [hsum] at h6
rw [← h6]
exact Finset.sum_le_sum fun j _ => hterm j
calc (n : ℝ) * x - (n * (n - 1) / 2) * x ^ 2
= x * ((n : ℝ) - x * (n * (n - 1) / 2)) := by ring
_ ≤ x * ∑ j ∈ Finset.range n, (1 - x) ^ j :=
mul_le_mul_of_nonneg_left h5 hx0
linarith
have hx2 : x ^ 2 = 1 / m ^ 2 := by rw [hxdef]; ring
have hdiv : (n : ℝ) / m = n * x := by rw [hxdef]; ring
rw [hdiv]
have h7 : (1 - 1 / (m : ℝ)) ^ n = (1 - x) ^ n := by rw [hxdef]
rw [h7]
calc (1 - x) ^ n - 1 + (n : ℝ) * x
≤ (n : ℝ) * (n - 1) / 2 * x ^ 2 := hmain
_ = (n : ℝ) * (n - 1) / (2 * m ^ 2) := by rw [hx2]; ring
/-- [PROVED session 011] Summability of the odd-m S_∞ series (the honesty
note on `SInfty`'s `tsum` discharged): terms are nonneg and O(n²/m²). -/
theorem sInf_series_summable (n : ℕ) :
Summable fun m : {m : ℕ // Odd m ∧ 3 ≤ m} =>
((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)) := by
refine Summable.of_nonneg_of_le
(g := fun m : {m : ℕ // Odd m ∧ 3 ≤ m} =>
(1 - 1 / ((m : ℕ) : ℝ)) ^ n - 1 + (n : ℝ) / ((m : ℕ) : ℝ))
(f := fun m : {m : ℕ // Odd m ∧ 3 ≤ m} =>
((n : ℝ) * ((n : ℝ) - 1) / 2) * (1 / ((m : ℕ) : ℝ) ^ 2)) ?_ ?_ ?_
· intro m
exact bern_term_nonneg n m.1 (Nat.le_trans (by norm_num) m.2.2)
· intro m
refine le_trans (bern_term_upper n m.1 (Nat.le_trans (by norm_num) m.2.2)) (le_of_eq ?_)
ring
· exact ((Real.summable_one_div_nat_pow.mpr (by norm_num : 1 < 2)).mul_left
((n : ℝ) * ((n : ℝ) - 1) / 2)).comp_injective Subtype.coe_injective
/-- [PROVED session 011] H1: `log M + γ ≤ H_M` (from Mathlib's strictly
decreasing `eulerMascheroniSeq'`). -/
theorem harmonic_lower (M : ℕ) (hM : 1 ≤ M) :
Real.log M + Real.eulerMascheroniConstant ≤ (harmonic M : ℝ) := by
have h := Real.eulerMascheroniConstant_lt_eulerMascheroniSeq' M
rw [Real.eulerMascheroniSeq', if_neg (by omega : M ≠ 0)] at h
linarith
/-- [PROVED session 011] H2: `H_M ≤ log (M+1) + γ` (from Mathlib's strictly
increasing `eulerMascheroniSeq`). -/
theorem harmonic_upper (M : ℕ) :
(harmonic M : ℝ) ≤ Real.log ((M : ℝ) + 1) + Real.eulerMascheroniConstant := by
have h := Real.eulerMascheroniSeq_lt_eulerMascheroniConstant M
rw [Real.eulerMascheroniSeq] at h
linarith
/-- [PROVED session 011] h⁺(m) ≥ n/m − 1 for m ≥ 1 (the power term is
nonneg). -/
theorem bern_term_lower (n : ℕ) (m : ℕ) (hm : 1 ≤ m) :
(n : ℝ) / m - 1 ≤ (1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / m := by
have hm1 : (1 : ℝ) ≤ m := by exact_mod_cast hm
have h4 : (1 : ℝ) / m ≤ 1 := by rw [div_le_one (by positivity)]; exact hm1
have hpos : (0 : ℝ) ≤ 1 - 1 / (m : ℝ) := by linarith
have h3 : (0 : ℝ) ≤ (1 - 1 / (m : ℝ)) ^ n := pow_nonneg hpos n
linarith
/-- The odd reciprocals sum `Σ_{k=1}^{K} 1/(2k+1)`. -/
private def oddHarm (K : ℕ) : ℝ := ∑ k ∈ Finset.Icc 1 K, (1 : ℝ) / (2 * k + 1)
/-- Embedding `k ↦ 2k+1` into the odd-≥-3 subtype (junk value at k = 0,
never used: only applied on `Icc 1 K`). -/
private def oddEmb : ℕ → {m : ℕ // Odd m ∧ 3 ≤ m} := fun k =>
if hk : 1 ≤ k then ⟨2 * k + 1, ⟨k, rfl⟩, by omega⟩ else ⟨3, ⟨1, rfl⟩, le_refl 3⟩
/-- [PROVED session 011] Partial-sum comparison (D-037 §3 truncation):
`n·oddHarm K − K ≤ Σ'_{m odd ≥ 3} h⁺(m)` for every K — Bernoulli
termwise, nonneg tail dropped. -/
theorem sInf_partial_lower (n K : ℕ) :
(n : ℝ) * oddHarm K - (K : ℝ) ≤
∑' m : {m : ℕ // Odd m ∧ 3 ≤ m},
((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)) := by
calc (n : ℝ) * oddHarm K - (K : ℝ)
= ∑ k ∈ Finset.Icc 1 K, ((n : ℝ) / (2 * k + 1) - 1) := by
unfold oddHarm
rw [Finset.mul_sum, Finset.sum_sub_distrib]
congr 1
· exact Finset.sum_congr rfl (fun k _ => mul_one_div _ _)
· simp [Finset.sum_const, Nat.card_Icc, nsmul_eq_mul]
_ ≤ ∑ k ∈ Finset.Icc 1 K,
((1 - 1 / (2 * (k : ℝ) + 1)) ^ n - 1 + (n : ℝ) / (2 * (k : ℝ) + 1)) := by
apply Finset.sum_le_sum
intro k hk
have h := bern_term_lower n (2 * k + 1) (by omega)
have hc : ((2 * k + 1 : ℕ) : ℝ) = 2 * (k : ℝ) + 1 := by push_cast; ring
rwa [hc] at h
_ ≤ ∑' m : {m : ℕ // Odd m ∧ 3 ≤ m},
((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)) := by
have hinj : ∀ x ∈ Finset.Icc 1 K, ∀ y ∈ Finset.Icc 1 K,
oddEmb x = oddEmb y → x = y := by
intro x hx y hy h
have hx1 : 1 ≤ x := (Finset.mem_Icc.mp hx).1
have hy1 : 1 ≤ y := (Finset.mem_Icc.mp hy).1
simp only [oddEmb, dif_pos hx1, dif_pos hy1, Subtype.mk.injEq] at h
omega
have hconv : ∑ k ∈ Finset.Icc 1 K,
((1 - 1 / (2 * (k : ℝ) + 1)) ^ n - 1 + (n : ℝ) / (2 * (k : ℝ) + 1)) =
∑ k ∈ Finset.Icc 1 K,
((1 - 1 / ((oddEmb k : ℕ) : ℝ)) ^ n - 1 +
(n : ℝ) / ((oddEmb k : ℕ) : ℝ)) := by
apply Finset.sum_congr rfl
intro k hk
have hk1 : 1 ≤ k := (Finset.mem_Icc.mp hk).1
have hc : ((2 * k + 1 : ℕ) : ℝ) = 2 * (k : ℝ) + 1 := by push_cast; ring
simp only [oddEmb, dif_pos hk1]
show ((1 - 1 / (2 * (k : ℝ) + 1)) ^ n - 1 + (n : ℝ) / (2 * (k : ℝ) + 1)) =
(1 - 1 / ((2 * k + 1 : ℕ) : ℝ)) ^ n - 1 + (n : ℝ) / ((2 * k + 1 : ℕ) : ℝ)
rw [hc]
rw [hconv]
have hsi := Finset.sum_image (s := Finset.Icc 1 K) (g := oddEmb)
(f := fun m : {m : ℕ // Odd m ∧ 3 ≤ m} =>
(1 - 1 / ((m : ℕ) : ℝ)) ^ n - 1 + (n : ℝ) / ((m : ℕ) : ℝ))
(show Set.InjOn oddEmb ↑(Finset.Icc 1 K) from hinj)
rw [← hsi]
exact Summable.sum_le_tsum _
(fun i _ => bern_term_nonneg n i.1 (Nat.le_trans (by norm_num) i.2.2))
(sInf_series_summable n)
/-- [PROVED session 011] Odd-harmonic identity (D-037 §3):
`Σ_{k=1}^{K} 1/(2k+1) = H_{2K+1} − ½H_K − 1`, by induction. -/
theorem oddHarm_eq (K : ℕ) :
oddHarm K = (harmonic (2 * K + 1) : ℝ) - (harmonic K : ℝ) / 2 - 1 := by
induction K with
| zero => simp [oddHarm, harmonic_succ]
| succ K ih =>
have h1 : (harmonic (2 * (K + 1) + 1) : ℝ) =
(harmonic (2 * K + 1) : ℝ) + 1 / (2 * (K : ℝ) + 2) + 1 / (2 * (K : ℝ) + 3) := by
have hs : 2 * (K + 1) + 1 = (2 * K + 1) + 1 + 1 := by ring
rw [hs, harmonic_succ, harmonic_succ]
push_cast
ring
have h2 : (harmonic (K + 1) : ℝ) = (harmonic K : ℝ) + 1 / ((K : ℝ) + 1) := by
rw [harmonic_succ]
push_cast
ring
have e3 : (1 : ℝ) / (2 * (K : ℝ) + 2) = (1 / ((K : ℝ) + 1)) / 2 := by
have h4 : (2 : ℝ) * (K : ℝ) + 2 = 2 * ((K : ℝ) + 1) := by ring
rw [h4, one_div, mul_inv, one_div, div_eq_mul_inv]
ring
show (∑ k ∈ Finset.Icc 1 (K + 1), (1 : ℝ) / (2 * k + 1)) = _
rw [Finset.sum_Icc_succ_top (by omega : 1 ≤ K + 1) (fun k => (1 : ℝ) / (2 * k + 1)),
show (∑ k ∈ Finset.Icc 1 K, (1 : ℝ) / (2 * k + 1)) = oddHarm K from rfl, ih, h1, h2]
push_cast
rw [e3]
ring
/-- [PROVED session 011] oddHarm lower bound (D-037 §3): from H1/H2,
`oddHarm K ≥ log(2K+1) − ½log(K+1) + γ/2 − 1`. -/
theorem oddHarm_lower (K : ℕ) :
Real.log (2 * (K : ℝ) + 1) - Real.log ((K : ℝ) + 1) / 2 +
Real.eulerMascheroniConstant / 2 - 1 ≤ oddHarm K := by
rw [oddHarm_eq K]
have hbl := harmonic_lower (2 * K + 1) (by omega)
have hbu := harmonic_upper K
have hc : ((2 * K + 1 : ℕ) : ℝ) = 2 * (K : ℝ) + 1 := by push_cast; ring
rw [hc] at hbl
linarith
/-- [PROVED session 011] Archimedean lower bound (draft §3.1 Step 1,
D-037 §3): S_∞(n) ≥ ½ n log n + (C₁ − γ/2) n − 4 for n ≥ 20.
Proof: Bernoulli truncation at K ≈ n/2 + the two γ-shifted harmonic
bounds; the γ/log 2/log π pieces cancel EXACTLY (parity algebra), and
the residual logarithmic defect is ≤ n/(n−1) (even) resp. ≤ 1/2 (odd),
absorbed by the −4 constant. Machine-validated against exact values for
20 ≤ n ≤ 5000 (E-021/E-023 V1, min slack 9.52). -/
theorem sInfty_lower_bound (n : ℕ) (hn : 20 ≤ n) :
sInftyLower n ≤ SInfty n := by
show (1 / 2) * (n : ℝ) * Real.log n +
(lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 ≤
SInfty n
-- reduction to a K-specialized real inequality
have hmain : ∀ K : ℕ,
(1 / 2) * (n : ℝ) * Real.log n +
(lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 ≤
(1 - lagariasA1) * (n : ℝ) - 1 +
((n : ℝ) * (Real.log (2 * (K : ℝ) + 1) - Real.log ((K : ℝ) + 1) / 2 +
Real.eulerMascheroniConstant / 2 - 1) - (K : ℝ)) →
(1 / 2) * (n : ℝ) * Real.log n +
(lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 ≤
SInfty n := by
intro K hK
have h1 := sInf_partial_lower n K
have h2 := oddHarm_lower K
have h3 : (n : ℝ) * (Real.log (2 * (K : ℝ) + 1) - Real.log ((K : ℝ) + 1) / 2 +
Real.eulerMascheroniConstant / 2 - 1) ≤ (n : ℝ) * oddHarm K :=
mul_le_mul_of_nonneg_left h2 (by positivity)
have h4 : SInfty n = (1 - lagariasA1) * (n : ℝ) - 1 +
∑' m : {m : ℕ // Odd m ∧ 3 ≤ m},
((1 - 1 / (m : ℝ)) ^ n - 1 + (n : ℝ) / (m : ℝ)) := rfl
rw [h4]
linarith [h1, h3]
-- logarithm identities for the π-factors
have h4pi : Real.log (4 * Real.pi) = 2 * Real.log 2 + Real.log Real.pi := by
rw [Real.log_mul (by norm_num : (4 : ℝ) ≠ 0) Real.pi_ne_zero]
have e : Real.log (4 : ℝ) = 2 * Real.log 2 := by
rw [show (4 : ℝ) = 2 ^ 2 by norm_num, Real.log_pow]
norm_num
rw [e]
have h2pi : Real.log (2 * Real.pi) = Real.log 2 + Real.log Real.pi := by
rw [Real.log_mul (by norm_num : (2 : ℝ) ≠ 0) Real.pi_ne_zero]
rcases Nat.even_or_odd n with ⟨q, rfl⟩ | ⟨q, rfl⟩
· -- n = q + q, K = q − 1: defect ≤ n/(n−1) ≤ 2 < 4
have hq10 : 10 ≤ q := by omega
have hQ : (10 : ℝ) ≤ (q : ℝ) := by exact_mod_cast hq10
refine hmain (q - 1) ?_
have hN : ((q + q : ℕ) : ℝ) = 2 * (q : ℝ) := by push_cast; ring
have hK1 : 2 * ((q - 1 : ℕ) : ℝ) + 1 = 2 * (q : ℝ) - 1 := by
rw [Nat.cast_sub (by omega : 1 ≤ q), Nat.cast_one]; ring
have hK2 : ((q - 1 : ℕ) : ℝ) + 1 = (q : ℝ) := by
rw [Nat.cast_sub (by omega : 1 ≤ q), Nat.cast_one]; ring
have hK3 : ((q - 1 : ℕ) : ℝ) = (q : ℝ) - 1 := by
rw [Nat.cast_sub (by omega : 1 ≤ q), Nat.cast_one]
have hlogq : Real.log (q : ℝ) = Real.log (2 * (q : ℝ)) - Real.log 2 := by
have h := Real.log_mul (by norm_num : (2 : ℝ) ≠ 0)
(ne_of_gt (by linarith : (0 : ℝ) < (q : ℝ)))
linarith [h]
rw [hN, hK1, hK2, hK3, hlogq]
unfold lagariasA1 lagariasC1
rw [h4pi, h2pi]
have hpos : (0 : ℝ) < 2 * (q : ℝ) - 1 := by linarith
have hlogb1 : Real.log (2 * (q : ℝ)) - Real.log (2 * (q : ℝ) - 1) ≤
1 / (2 * (q : ℝ) - 1) := by
have h1 := Real.log_le_sub_one_of_pos
(x := (2 * (q : ℝ)) / (2 * (q : ℝ) - 1)) (div_pos (by linarith) hpos)
rw [Real.log_div (by linarith : (2 : ℝ) * (q : ℝ) ≠ 0) hpos.ne'] at h1
have e : (2 * (q : ℝ)) / (2 * (q : ℝ) - 1) - 1 = 1 / (2 * (q : ℝ) - 1) := by
field_simp [hpos.ne']
ring
linarith [h1, e]
have hlogb2 : (2 * (q : ℝ)) * (Real.log (2 * (q : ℝ)) - Real.log (2 * (q : ℝ) - 1)) ≤
2 := by
have h2 := mul_le_mul_of_nonneg_left hlogb1 (by linarith : (0 : ℝ) ≤ 2 * (q : ℝ))
have e : (2 * (q : ℝ)) * (1 / (2 * (q : ℝ) - 1)) ≤ 2 := by
rw [mul_one_div, div_le_iff₀ hpos]
linarith
linarith [h2, e]
linarith [hlogb2]
· -- n = 2q + 1, K = q: defect ≤ 1/2 < 7/2
have hq10 : 10 ≤ q := by omega
have hQ : (10 : ℝ) ≤ (q : ℝ) := by exact_mod_cast hq10
refine hmain q ?_
have hN : ((2 * q + 1 : ℕ) : ℝ) = 2 * (q : ℝ) + 1 := by push_cast; ring
have hlogq1 : Real.log ((q : ℝ) + 1) = Real.log (2 * (q : ℝ) + 2) - Real.log 2 := by
have h1 : (2 * (q : ℝ) + 2) = 2 * ((q : ℝ) + 1) := by ring
have h2 := Real.log_mul (by norm_num : (2 : ℝ) ≠ 0)
(by positivity : ((q : ℝ) + 1) ≠ 0)
rw [← h1] at h2
linarith [h2]
rw [hN, hlogq1]
unfold lagariasA1 lagariasC1
rw [h4pi, h2pi]
have hpos : (0 : ℝ) < 2 * (q : ℝ) + 1 := by linarith
have hlogb1 : Real.log (2 * (q : ℝ) + 2) - Real.log (2 * (q : ℝ) + 1) ≤
1 / (2 * (q : ℝ) + 1) := by
have h1 := Real.log_le_sub_one_of_pos
(x := (2 * (q : ℝ) + 2) / (2 * (q : ℝ) + 1)) (div_pos (by linarith) hpos)
rw [Real.log_div (by linarith : (2 : ℝ) * (q : ℝ) + 2 ≠ 0) hpos.ne'] at h1
have e : (2 * (q : ℝ) + 2) / (2 * (q : ℝ) + 1) - 1 = 1 / (2 * (q : ℝ) + 1) := by
field_simp [hpos.ne']
ring
linarith [h1, e]
have hlogb2 : ((2 * (q : ℝ) + 1) / 2) *
(Real.log (2 * (q : ℝ) + 2) - Real.log (2 * (q : ℝ) + 1)) ≤ 1 / 2 := by
have h2 := mul_le_mul_of_nonneg_left hlogb1
(by positivity : (0 : ℝ) ≤ (2 * (q : ℝ) + 1) / 2)
have e : ((2 * (q : ℝ) + 1) / 2) * (1 / (2 * (q : ℝ) + 1)) = 1 / 2 := by
field_simp [hpos.ne']
linarith [h2, e]
linarith [hlogb2]
/-! ## 3. The margin and its convexity (D-057) -/
/-- The honest closed-form unit-interval zero-count majorant (D-056 §2):
Ĉ₀(t) = 0.433 log(t+2) + 0.886 log log(t+2) + 2.9. -/
def C0hat (t : ℝ) : ℝ :=
0.433 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.9
/-- The two-unit-window zero-count majorant Z₂(t) = 0.6 log(t+2) +
0.886 log log(t+2) + 2.7 (the `ZeroCountProp2` bound form, D-069 §2).
Named for use in the corrected `Bn` (D-071 F-B): the I_III near-sum's
window |γ−t| < 1 is a two-unit window, honestly counted by Z₂, not Ĉ₀.
Definitionally the `ZeroCountProp2` closed form (that Prop's statement
is untouched). -/
def Z2hat (t : ℝ) : ℝ :=
0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7
/-- H majorant with A = 10.5, B₀ = 48 (D-056). -/
def Hhat (T : ℝ) : ℝ :=
3 * C0hat T ^ 2 + 10.5 * Real.log (T + 2) + 48
/-- The I_I boundary-integral majorant (D-057 §3):
B̃₄(n) = 2(√n+1)·(e^{√n/2}+1)·0.57·2^{−(2√n−2)}. -/
def IIMaj (n : ℝ) : ℝ :=
2 * (Real.sqrt n + 1) * (Real.exp (Real.sqrt n / 2) + 1) * 0.57 *
2 ^ (-(2 * Real.sqrt n - 2))
/-- The dog-leg right-tail bound per side (D-074, DL-5 quarter-charge
form): V_left + 8.38 + IIMaj/4, replacing the F-D-broken "3.3" right-tail
charge (D-072). This is the bound `hIntegral_Jlag_low_le_dogLegUpper`
proves for each horizontal right tail. -/
def DogLegRight (n : ℝ) : ℝ :=
((Real.sqrt n + 1) / 2) * (Real.exp (5 / 2) + 1) / 2 + 8.38 + IIMaj n / 4
/-- The margin majorant chain (D-057, corrected per D-071): margiñ(n) =
S(n) − B̃(n) + 1 with the counting function majorized by a smooth
function F. M₀ = 1.3352 (E-023, grid-verified — see D-060 §4).
CORRECTION (D-071, user-approved session 038): the bridge is 4F (the
residue sum λ_n(T) runs over BOTH signs of γ — D-036/D-037's 2N(T)
was a factor-2 accounting slip, R-004 unaffected) and the I_III
near-sum uses the two-unit count (2/3)·Z2hat (D-069 Finding 2 made
exact). See D-071 + E-030. -/
def marginTilde (F : ℝ → ℝ) (n : ℝ) : ℝ :=
let T := Real.sqrt n + 1
((1 / 2) * n * Real.log n +
(lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4) -
(4 * F T + 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +
40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T) +
2 * DogLegRight n + IIMaj n + 1) + 1
/-! ### Block machinery for the `marginTilde_convex` proof (D-057 §2) -/
/-- Second-derivative computation package: if φ has derivative D1 on a
neighborhood of T and D1 has derivative D2 at T, then φ″(T) = D2. -/
theorem deriv2_of_hasDerivAt_nhds {φ D1 : ℝ → ℝ} {T D2 : ℝ}
(h1 : ∀ᶠ x in 𝓝 T, HasDerivAt φ (D1 x) x) (h2 : HasDerivAt D1 D2 T) :
deriv (deriv φ) T = D2 :=
(h2.congr_of_eventuallyEq (by
filter_upwards [h1] with x hx using hx.deriv)).deriv
/-- The ψ-functional of D-057: ψ[φ](T) = φ″(T) − φ′(T)/(T−1). -/
def psiOf (φ : ℝ → ℝ) (T : ℝ) : ℝ := deriv (deriv φ) T - deriv φ T / (T - 1)
/-- [PROVED session 011] Block #2 (identity): ψ[id](T) = −1/(T−1) < 0. -/
theorem psiOf_id (T : ℝ) (hT : 1 < T) : psiOf id T = -1 / (T - 1) ∧ psiOf id T < 0 := by
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt id 1 x := by
filter_upwards [] with x
exact hasDerivAt_id' x
have hd2 : deriv (deriv id) T = 0 :=
deriv2_of_hasDerivAt_nhds h1 (hasDerivAt_const T 1)
have hd1 : deriv id T = 1 := h1.self_of_nhds.deriv
have h3 : (0 : ℝ) < T - 1 := by linarith
refine ⟨?_, ?_⟩
· unfold psiOf; rw [hd2, hd1]; ring
· unfold psiOf; rw [hd2, hd1]; linarith [one_div_pos.mpr h3]
/-- [PROVED session 011] Block #10 (L1 = log(T+2)): ψ-formula. -/
theorem psiOf_log_shift (T : ℝ) (hT : 1 < T) :
psiOf (fun t => Real.log (t + 2)) T =
-1 / (T + 2) ^ 2 - 1 / ((T + 2) * (T - 1)) := by
have hT2 : (0 : ℝ) < T + 2 := by linarith
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => Real.log (t + 2)) ((x + 2)⁻¹) x := by
filter_upwards [eventually_gt_nhds (by linarith : (-2 : ℝ) < T)] with x hx
have h := (Real.hasDerivAt_log (show x + 2 ≠ 0 by linarith)).comp x
((hasDerivAt_id' x).add_const 2)
rwa [mul_one] at h
have h2 : HasDerivAt (fun t => (t + 2)⁻¹) (-1 / (T + 2) ^ 2) T := by
have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) ≠ 0)
have e : (-(1 : ℝ)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => Real.log (t + 2)) T = (T + 2)⁻¹ := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT2' : (T + 2) ≠ 0 := by linarith
field_simp [hT1, hT2']
/-- [PROVED session 011] Block #10 sign: ψ < 0 for T > 1. -/
theorem psiOf_log_shift_neg {T : ℝ} (hT : 1 < T) :
psiOf (fun t => Real.log (t + 2)) T < 0 := by
rw [psiOf_log_shift T hT]
have h1 : (0 : ℝ) < 1 / (T + 2) ^ 2 := one_div_pos.mpr (pow_pos (by linarith) 2)
have h2 : (0 : ℝ) < 1 / ((T + 2) * (T - 1)) :=
one_div_pos.mpr (mul_pos (by linarith) (by linarith))
have e : -1 / (T + 2) ^ 2 - 1 / ((T + 2) * (T - 1)) =
-(1 / (T + 2) ^ 2 + 1 / ((T + 2) * (T - 1))) := by ring
rw [e]
linarith [add_pos h1 h2]
/-- [PROVED session 011] Reusable per-point derivative of log(t+2). -/
theorem hasDerivAt_log_shift (x : ℝ) (hx : -2 < x) :
HasDerivAt (fun t => Real.log (t + 2)) (x + 2)⁻¹ x := by
have h := (Real.hasDerivAt_log (show x + 2 ≠ 0 by linarith)).comp x
((hasDerivAt_id' x).add_const 2)
rwa [mul_one] at h
/-- [PROVED session 011] Reusable per-point derivative of log log(t+2). -/
theorem hasDerivAt_log_log (x : ℝ) (hx : -1 < x) :
HasDerivAt (fun t => Real.log (Real.log (t + 2)))
((Real.log (x + 2))⁻¹ * (x + 2)⁻¹) x := by
have hin := hasDerivAt_log_shift x (by linarith)
have hout : HasDerivAt Real.log (Real.log (x + 2))⁻¹ (Real.log (x + 2)) :=
Real.hasDerivAt_log (ne_of_gt (Real.log_pos (by linarith)))
exact hout.comp x hin
/-- [PROVED session 011] Numerical bounds on the block-table range
T ≥ √20 + 1: T ≥ 5.4721, L1 ≥ 2 (via e² ≤ 7.4721), L2 ≥ 0.6931. -/
theorem block_range_bounds {T : ℝ} (hT : Real.sqrt 20 + 1 ≤ T) :
(5.4721 : ℝ) ≤ T ∧ 2 ≤ Real.log (T + 2) ∧
(0.6931 : ℝ) ≤ Real.log (Real.log (T + 2)) := by
have hs : (4.4721 : ℝ) ≤ Real.sqrt 20 := by
rw [Real.le_sqrt (by norm_num) (by norm_num)]
norm_num
have hT5 : (5.4721 : ℝ) ≤ T := by linarith
have hT2 : (7.4721 : ℝ) ≤ T + 2 := by linarith
have hL1 : (2 : ℝ) ≤ Real.log (T + 2) := by
have he2 : Real.exp 2 ≤ T + 2 := by
have hd := Real.exp_one_lt_d9
have e : Real.exp 2 = Real.exp 1 * Real.exp 1 := by
rw [← Real.exp_add]; norm_num
calc Real.exp 2 = Real.exp 1 * Real.exp 1 := e
_ ≤ 2.7182818286 * 2.7182818286 :=
mul_le_mul (le_of_lt hd) (le_of_lt hd) (Real.exp_pos 1).le (by positivity)
_ ≤ 7.4721 := by norm_num
_ ≤ T + 2 := hT2
have h2 := Real.log_le_log (Real.exp_pos 2) he2
rwa [Real.log_exp] at h2
have hL2 : (0.6931 : ℝ) ≤ Real.log (Real.log (T + 2)) := by
have h2 := Real.log_le_log (by norm_num : (0 : ℝ) < 2) hL1
have h3 := Real.log_two_gt_d9
linarith
exact ⟨hT5, hL1, hL2⟩
/-- [PROVED session 011] Block #11 (L2 = log log(T+2)): ψ-formula. -/
theorem psiOf_log_log_shift (T : ℝ) (hT : 1 < T) :
psiOf (fun t => Real.log (Real.log (t + 2))) T =
-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 -
1 / ((T + 2) * Real.log (T + 2) * (T - 1)) := by
have hT2 : (0 : ℝ) < T + 2 := by linarith
have hL1 : (0 : ℝ) < Real.log (T + 2) := Real.log_pos (by linarith)
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => Real.log (Real.log (t + 2)))
((Real.log (x + 2))⁻¹ * (x + 2)⁻¹) x := by
filter_upwards [eventually_gt_nhds (by linarith : (-2 : ℝ) < T),
eventually_gt_nhds (by linarith : (-1 : ℝ) < T)] with x hx2 hx1
have hin : HasDerivAt (fun t => Real.log (t + 2)) (x + 2)⁻¹ x := by
have h := (Real.hasDerivAt_log (show x + 2 ≠ 0 by linarith)).comp x
((hasDerivAt_id' x).add_const 2)
rwa [mul_one] at h
have hout : HasDerivAt Real.log (Real.log (x + 2))⁻¹ (Real.log (x + 2)) :=
Real.hasDerivAt_log (ne_of_gt (Real.log_pos (by linarith)))
exact hout.comp x hin
have h2 : HasDerivAt (fun t => (Real.log (t + 2))⁻¹ * (t + 2)⁻¹)
(-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) T := by
have hu : HasDerivAt (fun t => (Real.log (t + 2))⁻¹)
(-(T + 2)⁻¹ / Real.log (T + 2) ^ 2) T := by
have hin : HasDerivAt (fun t => Real.log (t + 2)) (T + 2)⁻¹ T := by
have h := (Real.hasDerivAt_log (show T + 2 ≠ 0 by linarith)).comp T
((hasDerivAt_id' T).add_const 2)
rwa [mul_one] at h
exact hin.inv (ne_of_gt hL1)
have hv : HasDerivAt (fun t => (t + 2)⁻¹) (-1 / (T + 2) ^ 2) T := by
have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) ≠ 0)
have e : (-(1 : ℝ)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring
rwa [e] at h
have h := hu.mul hv
have hT2' : (T + 2) ≠ 0 := ne_of_gt hT2
have hL1' : Real.log (T + 2) ≠ 0 := ne_of_gt hL1
have e : (-(T + 2)⁻¹ / Real.log (T + 2) ^ 2) * (T + 2)⁻¹ +
(Real.log (T + 2))⁻¹ * (-1 / (T + 2) ^ 2) =
-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 := by
field_simp [hT2', hL1']
ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => Real.log (Real.log (t + 2))) T =
(Real.log (T + 2))⁻¹ * (T + 2)⁻¹ := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT2' : (T + 2) ≠ 0 := ne_of_gt hT2
have hL1' : Real.log (T + 2) ≠ 0 := ne_of_gt hL1
field_simp [hT1, hT2', hL1']
/-- [PROVED session 011] Block #11 sign: ψ < 0 for T > 1. -/
theorem psiOf_log_log_shift_neg {T : ℝ} (hT : 1 < T) :
psiOf (fun t => Real.log (Real.log (t + 2))) T < 0 := by
rw [psiOf_log_log_shift T hT]
have hL1 : (0 : ℝ) < Real.log (T + 2) := Real.log_pos (by linarith)
have hp1 : (0 : ℝ) < (Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 :=
div_pos (by linarith) (pow_pos (mul_pos (by linarith) hL1) 2)
have hp2 : (0 : ℝ) < 1 / ((T + 2) * Real.log (T + 2) * (T - 1)) :=
one_div_pos.mpr (mul_pos (mul_pos (by linarith) hL1) (by linarith))
have e : -(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 -
1 / ((T + 2) * Real.log (T + 2) * (T - 1)) =
-((Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 +
1 / ((T + 2) * Real.log (T + 2) * (T - 1))) := by ring
rw [e]
linarith [add_pos hp1 hp2]
/-- [PROVED session 011] Block #7 (L1²): ψ-formula. -/
theorem psiOf_log_sq_shift (T : ℝ) (hT : 1 < T) :
psiOf (fun t => Real.log (t + 2) ^ 2) T =
2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2 -
2 * Real.log (T + 2) / ((T + 2) * (T - 1)) := by
have hT2 : (0 : ℝ) < T + 2 := by linarith
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => Real.log (t + 2) ^ 2)
(2 * Real.log (x + 2) * (x + 2)⁻¹) x := by
filter_upwards [eventually_gt_nhds (by linarith : (-2 : ℝ) < T)] with x hx
have h := (hasDerivAt_log_shift x (by linarith)).pow 2
rwa [pow_one, Nat.cast_ofNat] at h
have h2 : HasDerivAt (fun t => 2 * Real.log (t + 2) * (t + 2)⁻¹)
(2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2) T := by
have hu : HasDerivAt (fun t => 2 * Real.log (t + 2)) (2 * (T + 2)⁻¹) T :=
(hasDerivAt_log_shift T (by linarith : (-2 : ℝ) < T)).const_mul 2
have hv : HasDerivAt (fun t => (t + 2)⁻¹) (-1 / (T + 2) ^ 2) T := by
have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) ≠ 0)
have e : (-(1 : ℝ)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring
rwa [e] at h
have h := hu.mul hv
have hT2' : (T + 2) ≠ 0 := by linarith
have e : 2 * (T + 2)⁻¹ * (T + 2)⁻¹ + 2 * Real.log (T + 2) * (-1 / (T + 2) ^ 2) =
2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2 := by
field_simp [hT2']
ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => Real.log (t + 2) ^ 2) T =
2 * Real.log (T + 2) * (T + 2)⁻¹ := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT2' : (T + 2) ≠ 0 := by linarith
field_simp [hT1, hT2']
/-- [PROVED session 011] Block #7 sign: ψ < 0 on the table range (L1 ≥ 2). -/
theorem psiOf_log_sq_shift_neg {T : ℝ} (hT : Real.sqrt 20 + 1 ≤ T) :
psiOf (fun t => Real.log (t + 2) ^ 2) T < 0 := by
obtain ⟨hT5, hL1, _⟩ := block_range_bounds hT
rw [psiOf_log_sq_shift T (by linarith)]
have h1 : 2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2 < 0 :=
div_neg_of_neg_of_pos (by linarith) (pow_pos (by linarith) 2)
have h2 : (0 : ℝ) < 2 * Real.log (T + 2) / ((T + 2) * (T - 1)) :=
div_pos (by linarith) (mul_pos (by linarith) (by linarith))
linarith
/-- [PROVED session 011] Block #8 (L1·L2): ψ-formula. -/
theorem psiOf_log_mul_log_shift (T : ℝ) (hT : 1 < T) :
psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) T =
((Real.log (T + 2))⁻¹ - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2 -
(Real.log (Real.log (T + 2)) + 1) / ((T + 2) * (T - 1)) := by
have hT2 : (0 : ℝ) < T + 2 := by linarith
have hL1 : (0 : ℝ) < Real.log (T + 2) := Real.log_pos (by linarith)
have h1 : ∀ᶠ x in 𝓝 T,
HasDerivAt (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))
((Real.log (Real.log (x + 2)) + 1) * (x + 2)⁻¹) x := by
filter_upwards [eventually_gt_nhds (by linarith : (-1 : ℝ) < T)] with x hx
have hu := hasDerivAt_log_shift x (by linarith)
have hv := hasDerivAt_log_log x hx
have h := hu.mul hv
have hx2 : (x + 2) ≠ 0 := by linarith
have hxL : Real.log (x + 2) ≠ 0 := ne_of_gt (Real.log_pos (by linarith))
have e : (x + 2)⁻¹ * Real.log (Real.log (x + 2)) +
Real.log (x + 2) * ((Real.log (x + 2))⁻¹ * (x + 2)⁻¹) =
(Real.log (Real.log (x + 2)) + 1) * (x + 2)⁻¹ := by
field_simp [hx2, hxL]
rwa [e] at h
have h2 : HasDerivAt (fun t => (Real.log (Real.log (t + 2)) + 1) * (t + 2)⁻¹)
(((Real.log (T + 2))⁻¹ - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2) T := by
have hw : HasDerivAt (fun t => Real.log (Real.log (t + 2)) + 1)
((Real.log (T + 2))⁻¹ * (T + 2)⁻¹) T :=
(hasDerivAt_log_log T (by linarith)).add_const 1
have hz : HasDerivAt (fun t => (t + 2)⁻¹) (-1 / (T + 2) ^ 2) T := by
have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) ≠ 0)
have e : (-(1 : ℝ)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring
rwa [e] at h
have h := hw.mul hz
have hT2' : (T + 2) ≠ 0 := by linarith
have hL1' : Real.log (T + 2) ≠ 0 := ne_of_gt hL1
have e : (Real.log (T + 2))⁻¹ * (T + 2)⁻¹ * (T + 2)⁻¹ +
(Real.log (Real.log (T + 2)) + 1) * (-1 / (T + 2) ^ 2) =
((Real.log (T + 2))⁻¹ - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2 := by
field_simp [hT2', hL1']
ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) T =
(Real.log (Real.log (T + 2)) + 1) * (T + 2)⁻¹ := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT2' : (T + 2) ≠ 0 := by linarith
field_simp [hT1, hT2']
/-- [PROVED session 011] Block #8 sign: ψ < 0 on the table range
(1/L1 ≤ 1/2 < 1 + L2). -/
theorem psiOf_log_mul_log_shift_neg {T : ℝ} (hT : Real.sqrt 20 + 1 ≤ T) :
psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) T < 0 := by
obtain ⟨hT5, hL1, hL2⟩ := block_range_bounds hT
rw [psiOf_log_mul_log_shift T (by linarith)]
have hinv : (Real.log (T + 2))⁻¹ ≤ 1 / 2 := by
have h := one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 2) hL1
rwa [one_div] at h
have hbr : (Real.log (T + 2))⁻¹ - Real.log (Real.log (T + 2)) - 1 < 0 := by
linarith
have h1 : ((Real.log (T + 2))⁻¹ - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2 < 0 :=
div_neg_of_neg_of_pos hbr (pow_pos (by linarith) 2)
have h2 : (0 : ℝ) < (Real.log (Real.log (T + 2)) + 1) / ((T + 2) * (T - 1)) :=
div_pos (by linarith) (mul_pos (by linarith) (by linarith))
linarith
/-- [PROVED session 011] Block #9 (L2²): ψ-formula. -/
theorem psiOf_log_log_sq_shift (T : ℝ) (hT : 1 < T) :
psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) T =
2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /
((T + 2) * Real.log (T + 2)) ^ 2 -
2 * Real.log (Real.log (T + 2)) / ((T + 2) * Real.log (T + 2) * (T - 1)) := by
have hT2 : (0 : ℝ) < T + 2 := by linarith
have hL1 : (0 : ℝ) < Real.log (T + 2) := Real.log_pos (by linarith)
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => Real.log (Real.log (t + 2)) ^ 2)
(2 * Real.log (Real.log (x + 2)) * ((x + 2) * Real.log (x + 2))⁻¹) x := by
filter_upwards [eventually_gt_nhds (by linarith : (-1 : ℝ) < T)] with x hx
have h := (hasDerivAt_log_log x hx).pow 2
have e : (2 : ℝ) * Real.log (Real.log (x + 2)) ^ 1 *
((Real.log (x + 2))⁻¹ * (x + 2)⁻¹) =
2 * Real.log (Real.log (x + 2)) * ((x + 2) * Real.log (x + 2))⁻¹ := by
rw [pow_one, mul_inv]; ring
rwa [Nat.cast_ofNat, e] at h
have h2 : HasDerivAt
(fun t => 2 * Real.log (Real.log (t + 2)) * ((t + 2) * Real.log (t + 2))⁻¹)
(2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /
((T + 2) * Real.log (T + 2)) ^ 2) T := by
have hz_inner : HasDerivAt (fun t => (t + 2) * Real.log (t + 2))
(Real.log (T + 2) + 1) T := by
have h := ((hasDerivAt_id' T).add_const 2).mul
(hasDerivAt_log_shift T (by linarith))
have e : (1 : ℝ) * Real.log (T + 2) + (T + 2) * (T + 2)⁻¹ =
Real.log (T + 2) + 1 := by
rw [mul_inv_cancel₀ (by linarith : (T + 2) ≠ 0)]; ring
rwa [e] at h
have hz : HasDerivAt (fun t => ((t + 2) * Real.log (t + 2))⁻¹)
(-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) T :=
hz_inner.inv (mul_ne_zero (by linarith) (ne_of_gt hL1))
have hw := (hasDerivAt_log_log T (by linarith)).const_mul 2
have h := hw.mul hz
have hT2' : (T + 2) ≠ 0 := by linarith
have hL1' : Real.log (T + 2) ≠ 0 := ne_of_gt hL1
have e : 2 * ((Real.log (T + 2))⁻¹ * (T + 2)⁻¹) *
((T + 2) * Real.log (T + 2))⁻¹ +
2 * Real.log (Real.log (T + 2)) *
(-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) =
2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /
((T + 2) * Real.log (T + 2)) ^ 2 := by
field_simp [hT2', hL1']
ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => Real.log (Real.log (t + 2)) ^ 2) T =
2 * Real.log (Real.log (T + 2)) * ((T + 2) * Real.log (T + 2))⁻¹ :=
h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT2' : (T + 2) ≠ 0 := by linarith
have hL1' : Real.log (T + 2) ≠ 0 := ne_of_gt hL1
field_simp [hT1, hT2', hL1']
/-- [PROVED session 011] Block #9 sign: ψ < 0 on the table range
(L2(L1+1) ≥ 0.6931·3 > 1). -/
theorem psiOf_log_log_sq_shift_neg {T : ℝ} (hT : Real.sqrt 20 + 1 ≤ T) :
psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) T < 0 := by
obtain ⟨hT5, hL1, hL2⟩ := block_range_bounds hT
rw [psiOf_log_log_sq_shift T (by linarith)]
have hprod : (1 : ℝ) < Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1) := by
calc (1 : ℝ) < 0.6931 * (2 + 1) := by norm_num
_ ≤ Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1) :=
mul_le_mul hL2 (by linarith) (by linarith) (by linarith)
have h1 : 2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /
((T + 2) * Real.log (T + 2)) ^ 2 < 0 :=
div_neg_of_neg_of_pos (by linarith)
(pow_pos (mul_pos (by linarith) (by linarith)) 2)
have h2 : (0 : ℝ) < 2 * Real.log (Real.log (T + 2)) /
((T + 2) * Real.log (T + 2) * (T - 1)) :=
div_pos (by linarith) (mul_pos (mul_pos (by linarith) (by linarith)) (by linarith))
linarith
/-- [PROVED session 011] Block #5 (T·L1): ψ-formula. -/
theorem psiOf_T_mul_log_shift (T : ℝ) (hT : 1 < T) :
psiOf (fun t => t * Real.log (t + 2)) T =
(T + 4) / (T + 2) ^ 2 - Real.log (T + 2) / (T - 1) -
T / ((T + 2) * (T - 1)) := by
have hT2 : (0 : ℝ) < T + 2 := by linarith
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => t * Real.log (t + 2))
(Real.log (x + 2) + x * (x + 2)⁻¹) x := by
filter_upwards [eventually_gt_nhds (by linarith : (-2 : ℝ) < T)] with x hx
have h := (hasDerivAt_id' x).mul (hasDerivAt_log_shift x (by linarith))
rwa [one_mul] at h
have h2 : HasDerivAt (fun t => Real.log (t + 2) + t * (t + 2)⁻¹)
((T + 4) / (T + 2) ^ 2) T := by
have hu := hasDerivAt_log_shift T (by linarith : (-2 : ℝ) < T)
have hv : HasDerivAt (fun t => t * (t + 2)⁻¹) (2 / (T + 2) ^ 2) T := by
have hz : HasDerivAt (fun t => (t + 2)⁻¹) (-1 / (T + 2) ^ 2) T := by
have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) ≠ 0)
have e : (-(1 : ℝ)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring
rwa [e] at h
have h := (hasDerivAt_id' T).mul hz
have hT2' : (T + 2) ≠ 0 := by linarith
have e : (1 : ℝ) * (T + 2)⁻¹ + T * (-1 / (T + 2) ^ 2) = 2 / (T + 2) ^ 2 := by
field_simp [hT2']
ring
rwa [e] at h
have h := hu.add hv
have hT2' : (T + 2) ≠ 0 := by linarith
have e : (T + 2)⁻¹ + 2 / (T + 2) ^ 2 = (T + 4) / (T + 2) ^ 2 := by
field_simp [hT2']
ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => t * Real.log (t + 2)) T =
Real.log (T + 2) + T * (T + 2)⁻¹ := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT2' : (T + 2) ≠ 0 := by linarith
field_simp [hT1, hT2']
ring
/-- [PROVED session 011] Block #5 sign: ψ < 0 on the table range
(L1 ≥ 2; numerator −2T² − 7T − 12). -/
theorem psiOf_T_mul_log_shift_neg {T : ℝ} (hT : Real.sqrt 20 + 1 ≤ T) :
psiOf (fun t => t * Real.log (t + 2)) T < 0 := by
obtain ⟨hT5, hL1, _⟩ := block_range_bounds hT
have h1T : 1 < T := by linarith
rw [psiOf_T_mul_log_shift T h1T]
have hT1 : (0 : ℝ) < T - 1 := by linarith
have hT2 : (0 : ℝ) < T + 2 := by linarith
have hle : (2 : ℝ) / (T - 1) ≤ Real.log (T + 2) / (T - 1) := by gcongr
have hneg : (T + 4) / (T + 2) ^ 2 - 2 / (T - 1) - T / ((T + 2) * (T - 1)) < 0 := by
have hnum : (T + 4) / (T + 2) ^ 2 - 2 / (T - 1) - T / ((T + 2) * (T - 1)) =
(-(2 * T ^ 2 + 7 * T + 12)) / ((T + 2) ^ 2 * (T - 1)) := by
field_simp [hT1.ne', hT2.ne']
ring
rw [hnum]
exact div_neg_of_neg_of_pos (by linarith [sq_nonneg T])
(mul_pos (pow_pos hT2 2) hT1)
linarith
/-- [PROVED session 011] Block #6 (T·L2): ψ-formula. -/
theorem psiOf_T_mul_log_log_shift (T : ℝ) (hT : 1 < T) :
psiOf (fun t => t * Real.log (Real.log (t + 2))) T =
(T * (Real.log (T + 2) - 1) + 4 * Real.log (T + 2)) /
((T + 2) * Real.log (T + 2)) ^ 2 -
Real.log (Real.log (T + 2)) / (T - 1) -
T / ((T + 2) * Real.log (T + 2) * (T - 1)) := by
have hT2 : (0 : ℝ) < T + 2 := by linarith
have hL1 : (0 : ℝ) < Real.log (T + 2) := Real.log_pos (by linarith)
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => t * Real.log (Real.log (t + 2)))
(Real.log (Real.log (x + 2)) + x * ((x + 2) * Real.log (x + 2))⁻¹) x := by
filter_upwards [eventually_gt_nhds (by linarith : (-1 : ℝ) < T)] with x hx
have h := (hasDerivAt_id' x).mul (hasDerivAt_log_log x hx)
have hx2 : (x + 2) ≠ 0 := by linarith
have hxL : Real.log (x + 2) ≠ 0 := ne_of_gt (Real.log_pos (by linarith))
have e : (1 : ℝ) * Real.log (Real.log (x + 2)) +
x * ((Real.log (x + 2))⁻¹ * (x + 2)⁻¹) =
Real.log (Real.log (x + 2)) + x * ((x + 2) * Real.log (x + 2))⁻¹ := by
rw [one_mul, mul_inv]
ring
rwa [e] at h
have h2 : HasDerivAt
(fun t => Real.log (Real.log (t + 2)) + t * ((t + 2) * Real.log (t + 2))⁻¹)
((T * (Real.log (T + 2) - 1) + 4 * Real.log (T + 2)) /
((T + 2) * Real.log (T + 2)) ^ 2) T := by
have hu := hasDerivAt_log_log T (by linarith : (-1 : ℝ) < T)
have hz_inner : HasDerivAt (fun t => (t + 2) * Real.log (t + 2))
(Real.log (T + 2) + 1) T := by
have h := ((hasDerivAt_id' T).add_const 2).mul
(hasDerivAt_log_shift T (by linarith))
have e : (1 : ℝ) * Real.log (T + 2) + (T + 2) * (T + 2)⁻¹ =
Real.log (T + 2) + 1 := by
rw [mul_inv_cancel₀ (by linarith : (T + 2) ≠ 0)]; ring
rwa [e] at h
have hz : HasDerivAt (fun t => ((t + 2) * Real.log (t + 2))⁻¹)
(-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) T :=
hz_inner.inv (mul_ne_zero (by linarith) (ne_of_gt hL1))
have hv := (hasDerivAt_id' T).mul hz
have h := hu.add hv
have hT2' : (T + 2) ≠ 0 := by linarith
have hL1' : Real.log (T + 2) ≠ 0 := ne_of_gt hL1
have e : (Real.log (T + 2))⁻¹ * (T + 2)⁻¹ +
((1 : ℝ) * ((T + 2) * Real.log (T + 2))⁻¹ +
T * (-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2)) =
(T * (Real.log (T + 2) - 1) + 4 * Real.log (T + 2)) /
((T + 2) * Real.log (T + 2)) ^ 2 := by
field_simp [hT2', hL1']
ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => t * Real.log (Real.log (t + 2))) T =
Real.log (Real.log (T + 2)) + T * ((T + 2) * Real.log (T + 2))⁻¹ :=
h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT2' : (T + 2) ≠ 0 := by linarith
have hL1' : Real.log (T + 2) ≠ 0 := ne_of_gt hL1
field_simp [hT1, hT2', hL1']
ring
/-- [PROVED session 011] Block #6 sign: ψ < 0 on the table range.
Reduction (D-057 #6): ψ < 0 ⟸ A(T−1) ≤ T(T+2)L1 ⟸ L1(T−4) ≤ T(T−1)
⟸ L1 ≤ T+1 ≤ T(T−1)/(T−4). -/
theorem psiOf_T_mul_log_log_shift_neg {T : ℝ} (hT : Real.sqrt 20 + 1 ≤ T) :
psiOf (fun t => t * Real.log (Real.log (t + 2))) T < 0 := by
obtain ⟨hT5, hL1b, hL2b⟩ := block_range_bounds hT
have h1T : 1 < T := by linarith
rw [psiOf_T_mul_log_log_shift T h1T]
have hT1 : (0 : ℝ) < T - 1 := by linarith
have hT2 : (0 : ℝ) < T + 2 := by linarith
have hL1 : (0 : ℝ) < Real.log (T + 2) := Real.log_pos (by linarith)
have hL2 : (0 : ℝ) < Real.log (Real.log (T + 2)) := by linarith
set L1 := Real.log (T + 2) with hL1def
set L2 := Real.log (Real.log (T + 2)) with hL2def
set D := (T + 2) * L1 with hDdef
have hD : (0 : ℝ) < D := mul_pos hT2 hL1
have hlog_le : L1 ≤ T + 1 := by
have h := Real.log_le_sub_one_of_pos (x := T + 2) (by linarith)
linarith
have hstep : L1 * (T - 4) ≤ T * (T - 1) := by
have h1 : L1 * (T - 4) ≤ (T + 1) * (T - 4) :=
mul_le_mul_of_nonneg_right hlog_le (by linarith)
nlinarith
have hA : (T * (L1 - 1) + 4 * L1) * (T - 1) ≤ T * D := by
have h2 : (T * (L1 - 1) + 4 * L1) * (T - 1) = T * (T + 2) * L1 - (T * (T - 1) -
L1 * (T - 4)) := by ring
rw [h2, hDdef]
nlinarith [hstep]
have hkey : (T * (L1 - 1) + 4 * L1) * (T - 1) - L2 * D ^ 2 - T * D < 0 := by
have h3 : (0 : ℝ) < L2 * D ^ 2 := mul_pos hL2 (pow_pos hD 2)
linarith [hA]
have hpsi : (T * (L1 - 1) + 4 * L1) / D ^ 2 - L2 / (T - 1) - T / (D * (T - 1)) =
((T * (L1 - 1) + 4 * L1) * (T - 1) - L2 * D ^ 2 - T * D) /
(D ^ 2 * (T - 1)) := by
field_simp [hT1.ne', ne_of_gt hD]
rw [hpsi]
exact div_neg_of_neg_of_pos hkey (mul_pos (pow_pos hD 2) hT1)
/-! ### The IIMaj (B̃₄) term (D-057 §3) -/
/-- Decay rate a = 2 log 2 − 1/2 ≈ 0.8863. -/
private def iimA : ℝ := 2 * Real.log 2 - 1 / 2
/-- Decay rate b = 2 log 2 ≈ 1.3863. -/
private def iimB : ℝ := 2 * Real.log 2
/-- The IIMaj term as a function of s = √n: 4.56·(s+1)·(e^{−as} + e^{−bs}). -/
private def psiTilde (s : ℝ) : ℝ :=
4.56 * ((s + 1) * (Real.exp (-iimA * s) + Real.exp (-iimB * s)))
/-- [PROVED session 011] IIMaj n = ψ̃(√n): the rpow/exp bookkeeping. -/
theorem IIMaj_eq_psiTilde_sqrt (n : ℝ) :
IIMaj n = psiTilde (Real.sqrt n) := by
have hrw : (2 : ℝ) ^ (-(2 * Real.sqrt n - 2)) =
4 * Real.exp (-(2 * Real.log 2) * Real.sqrt n) := by
rw [show (-(2 * Real.sqrt n - 2) : ℝ) = 2 + -(2 * Real.sqrt n) by ring,
Real.rpow_add (by norm_num : (0 : ℝ) < 2)]
have e2 : (2 : ℝ) ^ (-(2 * Real.sqrt n)) =
Real.exp (-(2 * Real.log 2) * Real.sqrt n) := by
rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2)]
congr 1
ring
have e1 : (2 : ℝ) ^ (2 : ℝ) = 4 := by
rw [Real.rpow_def_of_pos (by norm_num : (0 : ℝ) < 2),
show Real.log 2 * 2 = Real.log (2 ^ 2) by rw [Real.log_pow]; ring,
Real.exp_log (by norm_num : (0 : ℝ) < 2 ^ 2)]
norm_num
rw [e2, e1]
have hEA : Real.exp (Real.sqrt n / 2) * Real.exp (-(2 * Real.log 2) * Real.sqrt n) =
Real.exp (-(2 * Real.log 2 - 1 / 2) * Real.sqrt n) := by
rw [← Real.exp_add]
congr 1
ring
unfold IIMaj psiTilde iimA iimB
rw [hrw,
show 2 * (Real.sqrt n + 1) * (Real.exp (Real.sqrt n / 2) + 1) * 0.57 *
(4 * Real.exp (-(2 * Real.log 2) * Real.sqrt n)) =
4.56 * ((Real.sqrt n + 1) *
((Real.exp (Real.sqrt n / 2) + 1) * Real.exp (-(2 * Real.log 2) * Real.sqrt n))) by ring,
show (Real.exp (Real.sqrt n / 2) + 1) * Real.exp (-(2 * Real.log 2) * Real.sqrt n) =
Real.exp (Real.sqrt n / 2) * Real.exp (-(2 * Real.log 2) * Real.sqrt n) +
Real.exp (-(2 * Real.log 2) * Real.sqrt n) by ring,
hEA]
/-- [PROVED session 012] Crude global upper bound on the I_I majorant:
IIMaj n ≤ 4.56·(√n+1)·2 for n ≥ 0 (both exponentials ≤ 1). Consumed by
the base-point numerics (LiBasePoints); the slack is absorbed by the
margin. -/
theorem IIMaj_le_two_mul (n : ℝ) (_hn : 0 ≤ n) :
IIMaj n ≤ 4.56 * (Real.sqrt n + 1) * 2 := by
rw [IIMaj_eq_psiTilde_sqrt]
unfold psiTilde
have hlog2 := Real.log_two_gt_d9
have ha : (0 : ℝ) < iimA := by unfold iimA; linarith
have hb : (0 : ℝ) < iimB := by unfold iimB; linarith
have hs : (0 : ℝ) ≤ Real.sqrt n := Real.sqrt_nonneg n
have heA : Real.exp (-iimA * Real.sqrt n) ≤ 1 := by
rw [Real.exp_le_one_iff]
exact mul_nonpos_of_nonpos_of_nonneg (by linarith) hs
have heB : Real.exp (-iimB * Real.sqrt n) ≤ 1 := by
rw [Real.exp_le_one_iff]
exact mul_nonpos_of_nonpos_of_nonneg (by linarith) hs
have hpos : (0 : ℝ) ≤ Real.sqrt n + 1 := by linarith
calc 4.56 * ((Real.sqrt n + 1) *
(Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)))
≤ 4.56 * ((Real.sqrt n + 1) * (1 + 1)) := by
apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : ℝ) ≤ 4.56)
apply mul_le_mul_of_nonneg_left _ hpos
linarith [heA, heB]
_ = 4.56 * (Real.sqrt n + 1) * 2 := by ring
/-- [PROVED session 012] IIMaj is nonnegative. -/
theorem IIMaj_nonneg (n : ℝ) : 0 ≤ IIMaj n := by
unfold IIMaj
apply mul_nonneg; apply mul_nonneg; apply mul_nonneg; apply mul_nonneg
· norm_num
· linarith [Real.sqrt_nonneg n]
· have h := Real.exp_pos (Real.sqrt n / 2)
linarith
· norm_num
· exact Real.rpow_nonneg (by norm_num) _
/-- [PROVED session 011] ψ̃ is globally C² (polynomial × exponentials). -/
theorem psiTilde_contDiff : ContDiff ℝ 2 psiTilde := by
unfold psiTilde iimA iimB
exact contDiff_const.mul
((contDiff_id.add contDiff_const).mul
((contDiff_const.mul contDiff_id).exp.add (contDiff_const.mul contDiff_id).exp))
/-- [PROVED session 011] ψ̃′ in closed form (per-point, global). -/
theorem hasDerivAt_psiTilde (x : ℝ) :
HasDerivAt psiTilde
(4.56 * ((Real.exp (-iimA * x) + Real.exp (-iimB * x)) +
(x + 1) * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)))) x := by
unfold psiTilde iimA iimB
have hu : HasDerivAt (fun t => t + 1) 1 x := (hasDerivAt_id' x).add_const 1
have hva : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2 - 1 / 2) * t))
(Real.exp (-(2 * Real.log 2 - 1 / 2) * x) * (-(2 * Real.log 2 - 1 / 2))) x := by
have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2 - 1 / 2))).exp
rwa [mul_one] at h
have hvb : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2) * t))
(Real.exp (-(2 * Real.log 2) * x) * (-(2 * Real.log 2))) x := by
have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2))).exp
rwa [mul_one] at h
have h := (hu.mul (hva.add hvb)).const_mul 4.56
simp only [Pi.add_apply, Pi.mul_apply] at h
convert h using 2 <;> first | rfl | ring
/-- [PROVED session 011] deriv ψ̃ = the closed D1 form. -/
theorem deriv_psiTilde (x : ℝ) :
deriv psiTilde x =
4.56 * ((Real.exp (-iimA * x) + Real.exp (-iimB * x)) +
(x + 1) * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x))) :=
(hasDerivAt_psiTilde x).deriv
/-- [PROVED session 011] ψ̃″ in closed form. -/
theorem deriv2_psiTilde (x : ℝ) :
deriv (deriv psiTilde) x =
4.56 * (2 * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)) +
(x + 1) * (iimA ^ 2 * Real.exp (-iimA * x) +
iimB ^ 2 * Real.exp (-iimB * x))) := by
have h1 : ∀ᶠ y in 𝓝 x, HasDerivAt psiTilde
(4.56 * ((Real.exp (-iimA * y) + Real.exp (-iimB * y)) +
(y + 1) * (-iimA * Real.exp (-iimA * y) - iimB * Real.exp (-iimB * y)))) y := by
filter_upwards [] with y
exact hasDerivAt_psiTilde y
have h2 : HasDerivAt
(fun t => 4.56 * ((Real.exp (-iimA * t) + Real.exp (-iimB * t)) +
(t + 1) * (-iimA * Real.exp (-iimA * t) - iimB * Real.exp (-iimB * t))))
(4.56 * (2 * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)) +
(x + 1) * (iimA ^ 2 * Real.exp (-iimA * x) +
iimB ^ 2 * Real.exp (-iimB * x)))) x := by
unfold iimA iimB
have hu : HasDerivAt (fun t => t + 1) 1 x := (hasDerivAt_id' x).add_const 1
have hva : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2 - 1 / 2) * t))
(Real.exp (-(2 * Real.log 2 - 1 / 2) * x) * (-(2 * Real.log 2 - 1 / 2))) x := by
have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2 - 1 / 2))).exp
rwa [mul_one] at h
have hvb : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2) * t))
(Real.exp (-(2 * Real.log 2) * x) * (-(2 * Real.log 2))) x := by
have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2))).exp
rwa [mul_one] at h
have hw := hva.add hvb
have hg := (hva.const_mul (-(2 * Real.log 2 - 1 / 2))).sub
(hvb.const_mul (2 * Real.log 2))
have hz := hu.mul hg
have h := (hw.add hz).const_mul 4.56
simp only [Pi.add_apply, Pi.mul_apply, Pi.sub_apply] at h
convert h using 2 <;> first | rfl | ring
exact deriv2_of_hasDerivAt_nhds h1 h2
/-- [PROVED session 011] u₂(t) = (b²t+b)·e^{−at} is antitone on [√20, ∞):
its derivative is e^{−at}·(b² − a(b²t+b)) and a(b²t+b) ≥ 8.846 > b² there. -/
theorem iim_u2_antitone :
AntitoneOn (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))
(Set.Ici (Real.sqrt 20)) := by
have hCD : ContDiff ℝ 2 (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t)) := by
unfold iimA iimB
exact ((contDiff_const.mul contDiff_id).add contDiff_const).mul
((contDiff_const.mul contDiff_id).exp)
have hder : ∀ x : ℝ,
HasDerivAt (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))
(Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB))) x := by
intro x
have hp : HasDerivAt (fun t => iimB ^ 2 * t + iimB) (iimB ^ 2 * 1) x :=
((hasDerivAt_id' x).const_mul (iimB ^ 2)).add_const iimB
have he : HasDerivAt (fun t => Real.exp (-iimA * t))
(Real.exp (-iimA * x) * (-iimA * 1)) x :=
((hasDerivAt_id' x).const_mul (-iimA)).exp
have h := hp.mul he
have e : iimB ^ 2 * 1 * Real.exp (-iimA * x) + (iimB ^ 2 * x + iimB) *
(Real.exp (-iimA * x) * (-iimA * 1)) =
Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB)) := by ring
rw [e] at h
exact h
apply antitoneOn_of_deriv_nonpos (convex_Ici _)
· exact hCD.continuous.continuousOn
· exact (hCD.differentiable (by norm_num)).differentiableOn.mono interior_subset
· intro x hx
rw [interior_Ici] at hx
have hxs : Real.sqrt 20 < x := Set.mem_Ioi.mp hx
have hlog2lo := Real.log_two_gt_d9
have hlog2hi := Real.log_two_lt_d9
have ha : (0.8862943606 : ℝ) ≤ iimA := by unfold iimA; linarith
have hblo : (1.3862943606 : ℝ) ≤ iimB := by unfold iimB; linarith
have hb : iimB ≤ (1.3862943616 : ℝ) := by unfold iimB; linarith
have hbpos : (0 : ℝ) < iimB := by linarith
have hapos : (0 : ℝ) < iimA := by linarith
have hb2lo : (1.9218 : ℝ) ≤ iimB ^ 2 := by nlinarith [hblo]
have hb2up : iimB ^ 2 ≤ (1.92182 : ℝ) := by nlinarith [hb, hbpos]
have hx4 : (4.4721 : ℝ) ≤ x := by
have h : (4.4721 : ℝ) ≤ Real.sqrt 20 := by
rw [Real.le_sqrt (by norm_num) (by norm_num)]; norm_num
linarith
have hbig : (8.8458 : ℝ) ≤ iimA * (iimB ^ 2 * x + iimB) := by
have hb2x : (9.9807 : ℝ) ≤ iimB ^ 2 * x + iimB := by
have h1 : (1.9218 : ℝ) * 4.4721 ≤ iimB ^ 2 * x :=
mul_le_mul hb2lo hx4 (by norm_num) (sq_nonneg iimB)
nlinarith [hblo]
calc (8.8458 : ℝ) ≤ 0.8862943606 * 9.9807 := by norm_num
_ ≤ iimA * (iimB ^ 2 * x + iimB) := mul_le_mul ha hb2x (by norm_num) hapos.le
rw [(hder x).deriv]
have h : iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB) ≤ 0 := by linarith
exact mul_nonpos_of_nonneg_of_nonpos (Real.exp_pos _).le h
set_option maxHeartbeats 800000 in
/-- [PROVED session 011; strengthened to 4/3 session 040 for the
D-074 dog-leg's 1.5·IIMaj charge] The B̃₄ bracket bound (D-057 §3):
for s ≥ √20,
ψ̃″(s) − ψ̃′(s)/s < 4/3. Factor-monotone argument: the bound splits as
4.56·[(s+1)/s]·[(b²s+b)e^{−as}]·[1+e^{−s/2}], three positive decreasing
factors; at s = √20 the product is ≤ 1.3155 < 4/3. -/
theorem iimaj_bracket_bound {s : ℝ} (hs : Real.sqrt 20 ≤ s) :
4.56 * (2 * (-iimA * Real.exp (-iimA * s) - iimB * Real.exp (-iimB * s)) +
(s + 1) * (iimA ^ 2 * Real.exp (-iimA * s) +
iimB ^ 2 * Real.exp (-iimB * s))) -
(4.56 * ((Real.exp (-iimA * s) + Real.exp (-iimB * s)) +
(s + 1) * (-iimA * Real.exp (-iimA * s) -
iimB * Real.exp (-iimB * s)))) / s < 4 / 3 := by
unfold iimA iimB
set L := Real.log 2 with hLdef
set a : ℝ := 2 * L - 1 / 2 with hadef
set b : ℝ := 2 * L with hbdef
set eA := Real.exp (-a * s) with heAdef
set eB := Real.exp (-b * s) with heBdef
have hlog2lo := Real.log_two_gt_d9
have hlog2hi := Real.log_two_lt_d9
rw [← hLdef] at hlog2lo hlog2hi
have ha : (0.8862943606 : ℝ) ≤ a := by rw [hadef]; linarith
have haup : a ≤ (0.8862943616 : ℝ) := by rw [hadef]; linarith
have hblo : (1.3862943606 : ℝ) ≤ b := by rw [hbdef]; linarith
have hb : b ≤ (1.3862943616 : ℝ) := by rw [hbdef]; linarith
have hab : a ≤ b := by rw [hadef, hbdef]; linarith
have hapos : (0 : ℝ) < a := by linarith
have hbpos : (0 : ℝ) < b := by linarith
have hsqrtlo : (4.4721 : ℝ) ≤ Real.sqrt 20 := by
rw [Real.le_sqrt (by norm_num) (by norm_num)]; norm_num
have hsqrthi : Real.sqrt 20 ≤ (4.4722 : ℝ) := by
have h : Real.sqrt 20 ≤ Real.sqrt (4.4722 ^ 2) :=
Real.sqrt_le_sqrt (by norm_num)
rwa [Real.sqrt_sq (by norm_num)] at h
have hs0 : (0 : ℝ) < s := by linarith [Real.sqrt_nonneg 20]
have hs4 : (4.4721 : ℝ) ≤ s := by linarith
have hs4' : s ≤ s := le_refl s
have heA : (0 : ℝ) < eA := Real.exp_pos _
have heB : (0 : ℝ) < eB := Real.exp_pos _
-- step 1: drop the two negative terms
have hstep1 :
4.56 * (2 * (-a * eA - b * eB) + (s + 1) * (a ^ 2 * eA + b ^ 2 * eB)) -
(4.56 * ((eA + eB) + (s + 1) * (-a * eA - b * eB))) / s ≤
4.56 * ((s + 1) * (a ^ 2 * eA + b ^ 2 * eB) +
(s + 1) * (a * eA + b * eB) / s) := by
have hd1 : 2 * (-a * eA - b * eB) ≤ 0 := by
nlinarith [mul_nonneg hapos.le heA.le, mul_nonneg hbpos.le heB.le]
have hd2 : -((eA + eB) / s) ≤ 0 := by
have h : (0 : ℝ) ≤ (eA + eB) / s :=
div_nonneg (add_nonneg heA.le heB.le) hs0.le
linarith
have hsf : (4.56 * ((eA + eB) + (s + 1) * (-a * eA - b * eB))) / s =
4.56 * ((eA + eB) / s + (s + 1) * (-a * eA - b * eB) / s) := by
field_simp [hs0.ne']
rw [hsf]
have hsf2 : (s + 1) * (-a * eA - b * eB) / s = -((s + 1) * (a * eA + b * eB) / s) := by
field_simp [hs0.ne']
ring
rw [hsf2]
linarith
-- step 2: factor out b² and b/s termwise
have hstep2 :
4.56 * ((s + 1) * (a ^ 2 * eA + b ^ 2 * eB) +
(s + 1) * (a * eA + b * eB) / s) ≤
4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) := by
have hsq : a ^ 2 ≤ b ^ 2 := by nlinarith [hab, hapos]
have h1 : a ^ 2 * eA + b ^ 2 * eB ≤ b ^ 2 * (eA + eB) := by
nlinarith [mul_le_mul_of_nonneg_right hsq heA.le]
have h2 : (a * eA + b * eB) / s ≤ b * (eA + eB) / s := by
have h := add_le_add (mul_le_mul_of_nonneg_right hab heA.le) (le_refl (b * eB))
have h' : a * eA + b * eB ≤ b * (eA + eB) := by nlinarith [h]
gcongr
have m1 : (s + 1) * (a ^ 2 * eA + b ^ 2 * eB) ≤ (s + 1) * (b ^ 2 * (eA + eB)) :=
mul_le_mul_of_nonneg_left h1 (by linarith)
have m2 : (s + 1) * (a * eA + b * eB) / s ≤ (s + 1) * (b * (eA + eB)) / s := by
have h3 := mul_le_mul_of_nonneg_left h2 (show (0 : ℝ) ≤ s + 1 by linarith)
rwa [← mul_div_assoc, ← mul_div_assoc] at h3
have e3 : 4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) =
4.56 * ((s + 1) * (b ^ 2 * (eA + eB)) + (s + 1) * (b * (eA + eB)) / s) := by
field_simp [hs0.ne']
rw [e3]
exact mul_le_mul_of_nonneg_left (add_le_add m1 m2) (by norm_num)
-- step 3: the three-factor split
have hstep3 :
4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) =
4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) := by
have heB' : eB = eA * Real.exp (-s / 2) := by
rw [heBdef, heAdef, ← Real.exp_add]
congr 1
rw [hadef, hbdef]
ring
rw [heB']
field_simp [hs0.ne']
-- step 4: the three monotone factors at s = √20
have hu1 : (s + 1) / s ≤ (1.2237 : ℝ) := by
have h1 : (1 : ℝ) / s ≤ 1 / 4.4721 := one_div_le_one_div_of_le (by norm_num) hs4
have h2 : (1 : ℝ) / 4.4721 ≤ 0.2237 := by
rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 4.4721)]
norm_num
have h3 : (s + 1) / s = 1 + 1 / s := by field_simp [hs0.ne']
rw [h3]
linarith
have hu2fac : (b ^ 2 * s + b) * eA ≤ (0.2124 : ℝ) := by
have hAid : iimA = a := by unfold iimA; rw [← hLdef, ← hadef]
have hBid : iimB = b := by unfold iimB; rw [← hLdef, ← hbdef]
have hanti := iim_u2_antitone
rw [hAid, hBid] at hanti
have hu2le : (b ^ 2 * s + b) * Real.exp (-a * s) ≤
(b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) :=
hanti (Set.mem_Ici.mpr (le_refl _)) (Set.mem_Ici.mpr hs) hs
have hu2val : (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) ≤
(0.2124 : ℝ) := by
have hb2up : b ^ 2 ≤ (1.92182 : ℝ) := by nlinarith [hb, hbpos]
have hexp : Real.exp (-a * Real.sqrt 20) ≤ (0.0212766 : ℝ) := by
have ht : (3.9635 : ℝ) ≤ a * Real.sqrt 20 := by
calc (3.9635 : ℝ) ≤ 0.8862943606 * 4.4721 := by norm_num
_ ≤ a * Real.sqrt 20 :=
mul_le_mul ha hsqrtlo (by norm_num) hapos.le
have hsum : (47 : ℝ) ≤ Real.exp (a * Real.sqrt 20) := by
have h1 := Real.sum_le_exp_of_nonneg (x := (3.9635 : ℝ)) (by norm_num) 7
have h2 : Real.exp (3.9635 : ℝ) ≤ Real.exp (a * Real.sqrt 20) :=
Real.exp_le_exp.mpr ht
have h3 : (47 : ℝ) ≤ ∑ i ∈ Finset.range 7,
(3.9635 : ℝ) ^ i / (Nat.factorial i : ℝ) := by
norm_num [Finset.sum_range_succ]
linarith
rw [show -a * Real.sqrt 20 = -(a * Real.sqrt 20) by ring, Real.exp_neg]
calc (Real.exp (a * Real.sqrt 20))⁻¹ ≤ 1 / 47 := by
rw [← one_div]
exact one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 47) hsum
_ ≤ 0.0212766 := by
rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 47)]; norm_num
have hpoly : b ^ 2 * Real.sqrt 20 + b ≤ (9.9811 : ℝ) := by
have h1 : b ^ 2 * Real.sqrt 20 ≤ 1.92182 * 4.4722 :=
mul_le_mul hb2up hsqrthi (Real.sqrt_nonneg 20) (by norm_num)
linarith
exact le_trans (mul_le_mul hpoly hexp (Real.exp_pos _).le (by norm_num))
(by norm_num)
calc (b ^ 2 * s + b) * eA = (b ^ 2 * s + b) * Real.exp (-a * s) := rfl
_ ≤ (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) := hu2le
_ ≤ 0.2124 := hu2val
have hu3 : 1 + Real.exp (-s / 2) ≤ (1.1099 : ℝ) := by
have hexp : Real.exp (-s / 2) ≤ (0.10982 : ℝ) := by
have ht : (2.23605 : ℝ) ≤ s / 2 := by linarith
have hsum : (9.1064 : ℝ) ≤ Real.exp (s / 2) := by
have h1 := Real.sum_le_exp_of_nonneg (x := (2.23605 : ℝ)) (by norm_num) 6
have h2 : Real.exp (2.23605 : ℝ) ≤ Real.exp (s / 2) := Real.exp_le_exp.mpr ht
have h3 : (9.1064 : ℝ) ≤ ∑ i ∈ Finset.range 6,
(2.23605 : ℝ) ^ i / (Nat.factorial i : ℝ) := by
norm_num [Finset.sum_range_succ]
linarith
rw [show -s / 2 = -(s / 2) by ring, Real.exp_neg]
calc (Real.exp (s / 2))⁻¹ ≤ 1 / 9.1064 := by
rw [← one_div]
exact one_div_le_one_div_of_le (by norm_num : (0 : ℝ) < 9.1064) hsum
_ ≤ 0.10982 := by
rw [div_le_iff₀ (by norm_num : (0 : ℝ) < 9.1064)]; norm_num
linarith
-- final assembly
have hpos1 : (0 : ℝ) ≤ (b ^ 2 * s + b) * eA :=
mul_nonneg (by nlinarith [hbpos, hs0, sq_nonneg b]) heA.le
have hpos2 : (0 : ℝ) ≤ 1 + Real.exp (-s / 2) := by positivity
have hpos3 : (0 : ℝ) ≤ (s + 1) / s := by positivity
have hchain : 4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) ≤
4.56 * 1.2237 * 0.2124 * 1.1099 := by
have h1 : ((s + 1) / s) * ((b ^ 2 * s + b) * eA) ≤ 1.2237 * 0.2124 :=
mul_le_mul hu1 hu2fac hpos1 (by norm_num)
have h2 : ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) ≤
1.2237 * 0.2124 * 1.1099 :=
mul_le_mul h1 hu3 hpos2 (by positivity)
have h3 := mul_le_mul_of_nonneg_left h2 (by norm_num : (0 : ℝ) ≤ 4.56)
have e : (4.56 : ℝ) * (((s + 1) / s) * ((b ^ 2 * s + b) * eA) *
(1 + Real.exp (-s / 2))) =
4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) := by ring
have e' : (4.56 : ℝ) * (1.2237 * 0.2124 * 1.1099) = 4.56 * 1.2237 * 0.2124 * 1.1099 := by ring
rwa [e, e'] at h3
calc 4.56 * (2 * (-a * eA - b * eB) + (s + 1) * (a ^ 2 * eA + b ^ 2 * eB)) -
(4.56 * ((eA + eB) + (s + 1) * (-a * eA - b * eB))) / s
≤ 4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) := le_trans hstep1 hstep2
_ = 4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) := hstep3
_ ≤ 4.56 * 1.2237 * 0.2124 * 1.1099 := hchain
_ < 4 / 3 := by norm_num
/-! ### Assembly: regularity bundles -/
/-- [PROVED session 011] The blocks are C² on (−1, ∞) (all
L1/L2-singularities lie at T ≤ −1). -/
theorem contDiffOn_L1 : ContDiffOn ℝ 2 (fun t => Real.log (t + 2)) (Set.Ioi (-1)) :=
(contDiffOn_id.add contDiffOn_const).log (fun x hx => by
have h : -1 < x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x + 2))
theorem contDiffOn_L2 :
ContDiffOn ℝ 2 (fun t => Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=
contDiffOn_L1.log (fun x hx => by
have h : -1 < x := hx
exact ne_of_gt (Real.log_pos (by linarith : (1 : ℝ) < x + 2)))
theorem contDiffOn_L1sq :
ContDiffOn ℝ 2 (fun t => Real.log (t + 2) ^ 2) (Set.Ioi (-1)) :=
contDiffOn_L1.pow 2
theorem contDiffOn_L1L2 : ContDiffOn ℝ 2
(fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=
contDiffOn_L1.mul contDiffOn_L2
theorem contDiffOn_L2sq :
ContDiffOn ℝ 2 (fun t => Real.log (Real.log (t + 2)) ^ 2) (Set.Ioi (-1)) :=
contDiffOn_L2.pow 2
theorem contDiffOn_TL1 :
ContDiffOn ℝ 2 (fun t => t * Real.log (t + 2)) (Set.Ioi (-1)) :=
contDiffOn_id.mul contDiffOn_L1
theorem contDiffOn_TL2 :
ContDiffOn ℝ 2 (fun t => t * Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=
contDiffOn_id.mul contDiffOn_L2
/-- [PROVED session 011] T(m) = √m + 1 is C² on (20, ∞) and maps it
into (−1, ∞). -/
theorem contDiffOn_sqrt_shift :
ContDiffOn ℝ 2 (fun m => Real.sqrt m + 1) (Set.Ioi 20) :=
(contDiffOn_id.sqrt (fun x hx => by
have h : 20 < x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x))).add contDiffOn_const
theorem mapsTo_sqrt_shift :
Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) := by
intro x hx
have h : 20 < x := hx
have hnn := Real.sqrt_nonneg x
exact Set.mem_Ioi.mpr (by linarith)
/-- [PROVED session 012] √m + 1 maps (20, ∞) into (1, ∞) (the FAlt
domain). -/
theorem mapsTo_sqrt_shift_Ioi1 :
Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi 1) := by
intro x hx
have h : 20 < x := hx
have hpos := Real.sqrt_pos.mpr (by linarith : (0 : ℝ) < x)
exact Set.mem_Ioi.mpr (by linarith)
/-- [PROVED session 012] √m + 1 maps [20, ∞) into (1, ∞). -/
theorem mapsTo_sqrt_shift_Ici_Ioi1 :
Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi 1) := by
intro x hx
have h : 20 ≤ x := hx
have hpos := Real.sqrt_pos.mpr (by linarith : (0 : ℝ) < x)
exact Set.mem_Ioi.mpr (by linarith)
/-- [PROVED session 011] psiOf at T = √n + 1 in the chain-rule form
(with T − 1 = √n). -/
theorem psiOf_sqrt_rel (φ : ℝ → ℝ) (n : ℝ) :
psiOf φ (Real.sqrt n + 1) =
deriv (deriv φ) (Real.sqrt n + 1) - deriv φ (Real.sqrt n + 1) / Real.sqrt n := by
unfold psiOf
rw [show Real.sqrt n + 1 - 1 = Real.sqrt n by ring]
/-- [PROVED session 011] Second derivative of a sum (needs first-deriv
differentiability at n and eventual differentiability near n). -/
theorem deriv2_add {f g : ℝ → ℝ} {n : ℝ}
(hf1 : DifferentiableAt ℝ (deriv f) n) (hg1 : DifferentiableAt ℝ (deriv g) n)
(hf2 : ∀ᶠ m in 𝓝 n, DifferentiableAt ℝ f m)
(hg2 : ∀ᶠ m in 𝓝 n, DifferentiableAt ℝ g m) :
deriv (deriv fun x => f x + g x) n = deriv (deriv f) n + deriv (deriv g) n := by
have he : deriv (fun x => f x + g x) =ᶠ[𝓝 n] (fun m => deriv f m + deriv g m) := by
filter_upwards [hf2, hg2] with m hfm hgm
exact deriv_add hfm hgm
have h2 := (hf1.add hg1).hasDerivAt
rw [deriv_add hf1 hg1] at h2
exact (h2.congr_of_eventuallyEq he).deriv
/-- [PROVED session 011] Second derivative of a constant multiple. -/
theorem deriv2_const_mul {f : ℝ → ℝ} {n : ℝ} (c : ℝ)
(hf1 : DifferentiableAt ℝ (deriv f) n)
(hf2 : ∀ᶠ m in 𝓝 n, DifferentiableAt ℝ f m) :
deriv (deriv (fun m => c * f m)) n = c * deriv (deriv f) n := by
have he : deriv (fun m => c * f m) =ᶠ[𝓝 n] (fun m => c * deriv f m) := by
filter_upwards [hf2] with m hfm
exact deriv_const_mul c hfm
have h2 := (hf1.const_mul c).hasDerivAt
rw [deriv_const_mul c hf1] at h2
exact (h2.congr_of_eventuallyEq he).deriv
/-- [PROVED session 011] Second derivative of a constant function. -/
theorem deriv2_const_val (K n : ℝ) : deriv (deriv fun _ => K) n = 0 := by
have h1 : ∀ᶠ m in 𝓝 n, HasDerivAt (fun _ => K) 0 m := by
filter_upwards [] with m
exact hasDerivAt_const m K
exact deriv2_of_hasDerivAt_nhds h1 (hasDerivAt_const n 0)
/-- [PROVED session 011] Per-point first derivative of the S-function. -/
theorem hasDerivAt_marginS (c : ℝ) {m : ℝ} (hm : 0 < m) :
HasDerivAt (fun m => (1 / 2) * m * Real.log m + c * m - 4)
((1 / 2) * (Real.log m + 1) + c) m := by
have hlog : HasDerivAt Real.log m⁻¹ m := Real.hasDerivAt_log (ne_of_gt hm)
have hml := ((hasDerivAt_id' m).const_mul (1 / 2)).mul hlog
have h := (hml.add ((hasDerivAt_id' m).const_mul c)).sub_const 4
have hm0 : m ≠ 0 := ne_of_gt hm
convert h using 2 <;> first | rfl | field_simp [hm0]
/-- [PROVED session 011] Second derivative of the S-function: S″ = 1/(2n). -/
theorem marginS_deriv2 (c : ℝ) {n : ℝ} (hn : 0 < n) :
deriv (deriv fun m => (1 / 2) * m * Real.log m + c * m - 4) n =
1 / (2 * n) := by
have h1 : ∀ᶠ m in 𝓝 n, HasDerivAt (fun m => (1 / 2) * m * Real.log m + c * m - 4)
((1 / 2) * (Real.log m + 1) + c) m := by
filter_upwards [eventually_gt_nhds hn] with m hm
exact hasDerivAt_marginS c hm
have h2 : HasDerivAt (fun m => (1 / 2) * (Real.log m + 1) + c) (1 / (2 * n)) n := by
have h := ((Real.hasDerivAt_log (ne_of_gt hn)).add_const 1).const_mul (1 / 2)
convert h.add_const c using 2 <;> first | rfl | ring
exact deriv2_of_hasDerivAt_nhds h1 h2
/-! ### The expanded margin (D-057 §4 assembly) -/
/-- The margin pieces as block compositions (for chain-rule application).
Constants updated for the D-071 correction (4F bridge; (2/3)Z2 I_III)
and the D-074 dog-leg repair (the √n-linear dog-leg charge merges into
mIdb's coefficient +(e^{5/2}+1)/2; the I_I/dog-leg IIMaj total is 1.5;
mK loses the broken 3.3 and gains the dog-leg 16.76). -/
private def mFblock (F : ℝ → ℝ) : ℝ → ℝ := fun m => (-4) * F (Real.sqrt m + 1)
private def mTL1b : ℝ → ℝ := fun m => (-((8/3)*0.6 + 42)) *
((fun t => t * Real.log (t + 2)) (Real.sqrt m + 1))
private def mTL2b : ℝ → ℝ := fun m => (-((8/3)*0.886)) *
((fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))
private def mIdb : ℝ → ℝ := fun m => (-(((8/3)*2.7 + 192) + (Real.exp (5/2) + 1) / 2)) * (Real.sqrt m + 1)
private def mL1sqb : ℝ → ℝ := fun m => (-(42*0.433^2*(Real.exp 4 + 1))) *
((fun t => Real.log (t + 2) ^ 2) (Real.sqrt m + 1))
private def mL1L2b : ℝ → ℝ := fun m => (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *
((fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))
private def mL2sqb : ℝ → ℝ := fun m => (-(42*0.886^2*(Real.exp 4 + 1))) *
((fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt m + 1))
private def mL1b : ℝ → ℝ := fun m => (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *
((fun t => Real.log (t + 2)) (Real.sqrt m + 1))
private def mL2b : ℝ → ℝ := fun m => (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *
((fun t => Real.log (Real.log (t + 2))) (Real.sqrt m + 1))
private def mIIM : ℝ → ℝ := fun m => (-1.5) * IIMaj m
private def mK : ℝ := -40*1.3352 - 2*(Real.exp 4 + 1)*(7*(3*2.9^2 + 48)) - 16.76 - 1 + 1
/-- The margin as an explicit left-nested sum of pieces. -/
private def marginExpanded (F : ℝ → ℝ) : ℝ → ℝ := fun n =>
(((((((((((fun m => (1/2)*m*Real.log m + (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n +
mFblock F n) + mTL1b n) + mTL2b n) + mIdb n) + mL1sqb n) + mL1L2b n) +
mL2sqb n) + mL1b n) + mL2b n) + mIIM n) + mK
/-- [PROVED session 011] marginTilde = marginExpanded (the D-056/D-057
constant bookkeeping, checked by `ring`). -/
theorem marginTilde_eq_expanded (F : ℝ → ℝ) :
marginTilde F = marginExpanded F := by
funext n
simp only [marginTilde, marginExpanded, mFblock, mTL1b, mTL2b, mIdb, mL1sqb,
mL1L2b, mL2sqb, mL1b, mL2b, mIIM, mK, Hhat, C0hat, Z2hat, DogLegRight]
ring
/-- [PROVED session 011] The pieces are C² on (20, ∞). -/
theorem contDiffOn_mS (c : ℝ) :
ContDiffOn ℝ 2 (fun m => (1/2)*m*Real.log m + c*m - 4) (Set.Ioi 20) :=
(((contDiffOn_const.mul contDiffOn_id).mul (contDiffOn_id.log (fun x hx => by
have h : 20 < x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x)))).add
(contDiffOn_const.mul contDiffOn_id)).sub contDiffOn_const
theorem contDiffOn_mFblock (F : ℝ → ℝ) (hF : ContDiffOn ℝ 2 F (Set.Ioi 1)) :
ContDiffOn ℝ 2 (mFblock F) (Set.Ioi 20) :=
contDiffOn_const.mul
(hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1)
theorem contDiffOn_mTL1b : ContDiffOn ℝ 2 mTL1b (Set.Ioi 20) :=
contDiffOn_const.mul (contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)
theorem contDiffOn_mTL2b : ContDiffOn ℝ 2 mTL2b (Set.Ioi 20) :=
contDiffOn_const.mul (contDiffOn_TL2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)
theorem contDiffOn_mIdb : ContDiffOn ℝ 2 mIdb (Set.Ioi 20) :=
contDiffOn_const.mul contDiffOn_sqrt_shift
theorem contDiffOn_mL1sqb : ContDiffOn ℝ 2 mL1sqb (Set.Ioi 20) :=
contDiffOn_const.mul (contDiffOn_L1sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)
theorem contDiffOn_mL1L2b : ContDiffOn ℝ 2 mL1L2b (Set.Ioi 20) :=
contDiffOn_const.mul (contDiffOn_L1L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)
theorem contDiffOn_mL2sqb : ContDiffOn ℝ 2 mL2sqb (Set.Ioi 20) :=
contDiffOn_const.mul (contDiffOn_L2sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)
theorem contDiffOn_mL1b : ContDiffOn ℝ 2 mL1b (Set.Ioi 20) :=
contDiffOn_const.mul (contDiffOn_L1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)
theorem contDiffOn_mL2b : ContDiffOn ℝ 2 mL2b (Set.Ioi 20) :=
contDiffOn_const.mul (contDiffOn_L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)
theorem contDiffOn_mIIM : ContDiffOn ℝ 2 mIIM (Set.Ioi 20) := by
have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=
funext fun m => IIMaj_eq_psiTilde_sqrt m
have hsqrt : ContDiffOn ℝ 2 (fun m => Real.sqrt m) (Set.Ioi 20) :=
contDiffOn_id.sqrt (fun x hx => by
have h : 20 < x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x))
have hcomp : ContDiffOn ℝ 2 (psiTilde ∘ Real.sqrt) (Set.Ioi 20) :=
(psiTilde_contDiff.contDiffOn).comp hsqrt (Set.mapsTo_univ _ _)
unfold mIIM
rw [hId]
exact contDiffOn_const.mul hcomp
/-- [PROVED session 011] The margin is continuous on [20, ∞) (endpoint
included — the C² regularity on (20, ∞) does not give the endpoint). -/
theorem continuousOn_marginExpanded (F : ℝ → ℝ) (hF : ContDiffOn ℝ 2 F (Set.Ioi 1)) :
ContinuousOn (marginExpanded F) (Set.Ici 20) := by
have hsqrt : ContinuousOn Real.sqrt (Set.Ici 20) := Real.continuous_sqrt.continuousOn
have hT : ContinuousOn (fun m => Real.sqrt m + 1) (Set.Ici 20) :=
hsqrt.add continuousOn_const
have hmaps : Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi (-1)) := by
intro x hx
have h : 20 ≤ x := hx
have hnn := Real.sqrt_nonneg x
exact Set.mem_Ioi.mpr (by linarith)
have hlog : ContinuousOn Real.log (Set.Ici 20) :=
Real.continuousOn_log.mono (fun x hx => by
have h : 20 ≤ x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x))
have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=
funext fun m => IIMaj_eq_psiTilde_sqrt m
have hIIMc : ContinuousOn IIMaj (Set.Ici 20) := by
rw [hId]
exact (psiTilde_contDiff.continuous.continuousOn).comp hsqrt (Set.mapsTo_univ _ _)
have hSc : ContinuousOn
(fun m => (1/2)*m*Real.log m + (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4)
(Set.Ici 20) :=
(((continuousOn_const.mul continuousOn_id).mul hlog).add
(continuousOn_const.mul continuousOn_id)).sub continuousOn_const
unfold marginExpanded mFblock mTL1b mTL2b mIdb mL1sqb mL1L2b mL2sqb mL1b mL2b mIIM
refine (((((((((((hSc.add
((hF.continuousOn.comp hT mapsTo_sqrt_shift_Ici_Ioi1).const_mul (-4))).add
((contDiffOn_TL1.continuousOn.comp hT hmaps).const_mul _)).add
((contDiffOn_TL2.continuousOn.comp hT hmaps).const_mul _)).add
(hT.const_mul _)).add
((contDiffOn_L1sq.continuousOn.comp hT hmaps).const_mul _)).add
((contDiffOn_L1L2.continuousOn.comp hT hmaps).const_mul _)).add
((contDiffOn_L2sq.continuousOn.comp hT hmaps).const_mul _)).add
((contDiffOn_L1.continuousOn.comp hT hmaps).const_mul _)).add
((contDiffOn_L2.continuousOn.comp hT hmaps).const_mul _)).add
(hIIMc.const_mul (-1.5)))).add
continuousOn_const
/-- [PROVED session 011] The full margin is C² on (20, ∞). -/
theorem contDiffOn_marginExpanded (F : ℝ → ℝ) (hF : ContDiffOn ℝ 2 F (Set.Ioi 1)) :
ContDiffOn ℝ 2 (marginExpanded F) (Set.Ioi 20) := by
unfold marginExpanded
refine (((((((((((contDiffOn_mS _).add (contDiffOn_mFblock F hF)).add
contDiffOn_mTL1b).add contDiffOn_mTL2b).add contDiffOn_mIdb).add
contDiffOn_mL1sqb).add contDiffOn_mL1L2b).add contDiffOn_mL2sqb).add
contDiffOn_mL1b).add contDiffOn_mL2b).add contDiffOn_mIIM).add
contDiffOn_const
/-- [PROVED session 011; generalized session 012 to any c ≤ 1]
Localized variant of `chain_rule_sqrt_shift`: φ only needs to be C² on
(c, ∞) with c ≤ 1 (all D-057 blocks: L1-singularities at T = −2,
L2-singularities at T = −1, so c = −1 suffices for them; the explicit
Trudgian majorant FAlt of session 012 has log-singularities at 0 and 1,
so it uses c = 1). -/
theorem chain_rule_sqrt_shift_on (φ : ℝ → ℝ) {c : ℝ} (hc : c ≤ 1)
(hφ : ContDiffOn ℝ 2 φ (Set.Ioi c)) (n : ℝ) (hn : 0 < n) :
deriv (deriv fun n => φ (Real.sqrt n + 1)) n =
(deriv (deriv φ) (Real.sqrt n + 1) -
deriv φ (Real.sqrt n + 1) / Real.sqrt n) / (4 * n) := by
have hφd : DifferentiableOn ℝ φ (Set.Ioi c) :=
hφ.differentiableOn (by norm_num)
have hφdd : DifferentiableOn ℝ (deriv φ) (Set.Ioi c) :=
(hφ.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn
one_ne_zero
have hmem : ∀ m : ℝ, 0 < m → Set.Ioi c ∈ 𝓝 (Real.sqrt m + 1) := by
intro m hm
have h1 : (1 : ℝ) < Real.sqrt m + 1 := by
have h := Real.sqrt_pos.mpr hm
linarith
exact Ioi_mem_nhds (lt_of_le_of_lt hc h1)
have hφ1 : ∀ m : ℝ, 0 < m → DifferentiableAt ℝ φ (Real.sqrt m + 1) :=
fun m hm => hφd.differentiableAt (hmem m hm)
have hφ2 : DifferentiableAt ℝ (deriv φ) (Real.sqrt n + 1) :=
hφdd.differentiableAt (hmem n hn)
have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=
Real.hasDerivAt_sqrt hn.ne'
have hdiff_sqrt : DifferentiableAt ℝ Real.sqrt n := hsqrt.differentiableAt
have hdiff_h : DifferentiableAt ℝ (fun n => Real.sqrt n + 1) n :=
hdiff_sqrt.add (differentiableAt_const 1)
have hpos : Set.Ioi (0 : ℝ) ∈ 𝓝 n := Ioi_mem_nhds hn
have hg1 : deriv (fun n => φ (Real.sqrt n + 1)) =ᶠ[𝓝 n]
fun n => deriv φ (Real.sqrt n + 1) * (2 * Real.sqrt n)⁻¹ := by
filter_upwards [hpos] with m hm
have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=
Real.hasDerivAt_sqrt (ne_of_gt hm)
have hhm : DifferentiableAt ℝ (fun x => Real.sqrt x + 1) m :=
hsm.differentiableAt.add (differentiableAt_const 1)
have h1 : deriv (fun x => Real.sqrt x + 1) m = 1 / (2 * Real.sqrt m) := by
rw [deriv_add_const]
exact hsm.deriv
rw [show (fun x => φ (Real.sqrt x + 1)) = φ ∘ (fun x => Real.sqrt x + 1)
from rfl,
deriv_comp m (hφ1 m hm) hhm, h1]
ring
have hA : HasDerivAt (fun n => deriv φ (Real.sqrt n + 1))
(deriv (deriv φ) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n))) n := by
have h1 : HasDerivAt (fun x => Real.sqrt x + 1) (1 / (2 * Real.sqrt n)) n :=
hsqrt.add_const 1
have h2 : HasDerivAt (deriv φ) (deriv (deriv φ) (Real.sqrt n + 1))
(Real.sqrt n + 1) :=
hφ2.hasDerivAt
have h3 := h2.comp n h1
rwa [show (fun n => deriv φ (Real.sqrt n + 1)) =
deriv φ ∘ (fun n => Real.sqrt n + 1) from rfl]
have hB : HasDerivAt (fun n => (2 * Real.sqrt n)⁻¹)
(-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2) n := by
have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=
hsqrt.const_mul 2
have h2 : (2 * Real.sqrt n) ≠ 0 :=
mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)
exact h1.inv h2
have hmul : HasDerivAt (fun n => deriv φ (Real.sqrt n + 1) * (2 * Real.sqrt n)⁻¹)
(deriv (deriv φ) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n)) * (2 * Real.sqrt n)⁻¹ +
deriv φ (Real.sqrt n + 1) *
(-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n :=
hA.mul hB
have hder := (hmul.congr_of_eventuallyEq hg1).deriv
rw [hder]
set s := Real.sqrt n with hsdef
have hs0 : s ≠ 0 := Real.sqrt_ne_zero'.2 hn
have hn_eq : n = s ^ 2 := by
rw [hsdef]; exact (Real.sq_sqrt hn.le).symm
rw [hn_eq]
field_simp [hs0]
ring
/-- [PROVED session 011] Chain-rule identity with T(n) = √n (no shift),
for the IIMaj term: d²/dn² ψ(√n) = [ψ″(√n) − ψ′(√n)/√n] / (4n). -/
theorem chain_rule_sqrt (ψ : ℝ → ℝ) (hψ : ContDiff ℝ 2 ψ)
(n : ℝ) (hn : 0 < n) :
deriv (deriv fun n => ψ (Real.sqrt n)) n =
(deriv (deriv ψ) (Real.sqrt n) -
deriv ψ (Real.sqrt n) / Real.sqrt n) / (4 * n) := by
have hψ1 : Differentiable ℝ ψ := hψ.differentiable (by norm_num)
have hψ2 : Differentiable ℝ (deriv ψ) :=
(hψ.deriv' (n := 1)).differentiable one_ne_zero
have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=
Real.hasDerivAt_sqrt hn.ne'
have hpos : Set.Ioi (0 : ℝ) ∈ 𝓝 n := Ioi_mem_nhds hn
have hg1 : deriv (fun n => ψ (Real.sqrt n)) =ᶠ[𝓝 n]
fun n => deriv ψ (Real.sqrt n) * (2 * Real.sqrt n)⁻¹ := by
filter_upwards [hpos] with m hm
have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=
Real.hasDerivAt_sqrt (ne_of_gt hm)
rw [show (fun x => ψ (Real.sqrt x)) = ψ ∘ Real.sqrt from rfl,
deriv_comp m (hψ1 (Real.sqrt m)) hsm.differentiableAt, hsm.deriv]
ring
have hA : HasDerivAt (fun n => deriv ψ (Real.sqrt n))
(deriv (deriv ψ) (Real.sqrt n) * (1 / (2 * Real.sqrt n))) n := by
have h2 : HasDerivAt (deriv ψ) (deriv (deriv ψ) (Real.sqrt n))
(Real.sqrt n) :=
(hψ2 (Real.sqrt n)).hasDerivAt
have h3 := h2.comp n hsqrt
rwa [show (fun n => deriv ψ (Real.sqrt n)) = deriv ψ ∘ Real.sqrt from rfl]
have hB : HasDerivAt (fun n => (2 * Real.sqrt n)⁻¹)
(-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2) n := by
have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=
hsqrt.const_mul 2
have h2 : (2 * Real.sqrt n) ≠ 0 :=
mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)
exact h1.inv h2
have hmul : HasDerivAt (fun n => deriv ψ (Real.sqrt n) * (2 * Real.sqrt n)⁻¹)
(deriv (deriv ψ) (Real.sqrt n) * (1 / (2 * Real.sqrt n)) * (2 * Real.sqrt n)⁻¹ +
deriv ψ (Real.sqrt n) *
(-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n :=
hA.mul hB
have hder := (hmul.congr_of_eventuallyEq hg1).deriv
rw [hder]
set s := Real.sqrt n with hsdef
have hs0 : s ≠ 0 := Real.sqrt_ne_zero'.2 hn
have hn_eq : n = s ^ 2 := by
rw [hsdef]; exact (Real.sq_sqrt hn.le).symm
rw [hn_eq]
field_simp [hs0]
ring
/-- [PROVED session 011] The D-057 chain-rule identity behind the
11-block reduction: with T(n) = √n + 1,
d²/dn² φ(T(n)) = [φ″(T) − φ′(T)/(T−1)] / (4n), written with
√n = T−1. (Warm-up proof; first sorry eliminated from the library.) -/
theorem chain_rule_sqrt_shift (φ : ℝ → ℝ) (hφ : ContDiff ℝ 2 φ)
(n : ℝ) (hn : 0 < n) :
deriv (deriv fun n => φ (Real.sqrt n + 1)) n =
(deriv (deriv φ) (Real.sqrt n + 1) -
deriv φ (Real.sqrt n + 1) / Real.sqrt n) / (4 * n) := by
have hφ1 : Differentiable ℝ φ := hφ.differentiable (by norm_num)
have hφ2 : Differentiable ℝ (deriv φ) :=
(hφ.deriv' (n := 1)).differentiable one_ne_zero
have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=
Real.hasDerivAt_sqrt hn.ne'
have hdiff_sqrt : DifferentiableAt ℝ Real.sqrt n := hsqrt.differentiableAt
have hdiff_h : DifferentiableAt ℝ (fun n => Real.sqrt n + 1) n :=
hdiff_sqrt.add (differentiableAt_const 1)
have hpos : Set.Ioi (0 : ℝ) ∈ 𝓝 n := Ioi_mem_nhds hn
have hg1 : deriv (fun n => φ (Real.sqrt n + 1)) =ᶠ[𝓝 n]
fun n => deriv φ (Real.sqrt n + 1) * (2 * Real.sqrt n)⁻¹ := by
filter_upwards [hpos] with m hm
have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=
Real.hasDerivAt_sqrt (ne_of_gt hm)
have hhm : DifferentiableAt ℝ (fun x => Real.sqrt x + 1) m :=
hsm.differentiableAt.add (differentiableAt_const 1)
have h1 : deriv (fun x => Real.sqrt x + 1) m = 1 / (2 * Real.sqrt m) := by
rw [deriv_add_const]
exact hsm.deriv
rw [show (fun x => φ (Real.sqrt x + 1)) = φ ∘ (fun x => Real.sqrt x + 1)
from rfl,
deriv_comp m (hφ1 (Real.sqrt m + 1)) hhm, h1]
ring
have hA : HasDerivAt (fun n => deriv φ (Real.sqrt n + 1))
(deriv (deriv φ) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n))) n := by
have h1 : HasDerivAt (fun x => Real.sqrt x + 1) (1 / (2 * Real.sqrt n)) n :=
hsqrt.add_const 1
have h2 : HasDerivAt (deriv φ) (deriv (deriv φ) (Real.sqrt n + 1))
(Real.sqrt n + 1) :=
(hφ2 (Real.sqrt n + 1)).hasDerivAt
have h3 := h2.comp n h1
rwa [show (fun n => deriv φ (Real.sqrt n + 1)) =
deriv φ ∘ (fun n => Real.sqrt n + 1) from rfl]
have hB : HasDerivAt (fun n => (2 * Real.sqrt n)⁻¹)
(-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2) n := by
have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=
hsqrt.const_mul 2
have h2 : (2 * Real.sqrt n) ≠ 0 :=
mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)
exact h1.inv h2
have hmul : HasDerivAt (fun n => deriv φ (Real.sqrt n + 1) * (2 * Real.sqrt n)⁻¹)
(deriv (deriv φ) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n)) * (2 * Real.sqrt n)⁻¹ +
deriv φ (Real.sqrt n + 1) *
(-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n :=
hA.mul hB
have hder := (hmul.congr_of_eventuallyEq hg1).deriv
rw [hder]
set s := Real.sqrt n with hsdef
have hs0 : s ≠ 0 := Real.sqrt_ne_zero'.2 hn
have hn_eq : n = s ^ 2 := by
rw [hsdef]; exact (Real.sq_sqrt hn.le).symm
rw [hn_eq]
field_simp [hs0]
ring
set_option maxHeartbeats 1600000 in
/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the
4/3 bracket — the D-074 dog-leg charges 1.5·IIMaj, and 1.5/(3n) =
1/(2n) preserves the convexity slack] IIMaj″(n) < 1/(3n) for n ≥ 20
(the analytic version of D-057 §3's "max 2n·|B̃₄″| = 0.189 < 1"). -/
theorem IIMaj_deriv2_lt_three {n : ℝ} (hn : 20 ≤ n) :
deriv (deriv IIMaj) n < 1 / (3 * n) := by
have hn0 : (0 : ℝ) < n := by linarith
have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=
funext fun m => IIMaj_eq_psiTilde_sqrt m
rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,
deriv2_psiTilde]
have hb := iimaj_bracket_bound (Real.sqrt_le_sqrt hn)
have h4n : (0 : ℝ) < 4 * n := by linarith
have e : (1 : ℝ) / (3 * n) = (4 / 3) / (4 * n) := by
have h1 : (0 : ℝ) < 3 * n := by linarith [hn0]
have h2 : (0 : ℝ) < 4 * n := by linarith [hn0]
rw [div_eq_div_iff h1.ne' h2.ne']
ring
rw [e]
exact div_lt_div_of_pos_right hb h4n
set_option maxHeartbeats 800000 in
/-- [PROVED session 011] Margin convexity (D-057, draft §3.1 Step 4):
for any twice-differentiable majorant F of the zero count N(0,T] whose
ψ-block ψ[F](T) = F″(T) − F′(T)/(T−1) is negative for T ≥ √20 + 1
(the D-057 11-block table discharges this for the explicit Trudgian
majorant), the margin majorant margiñ is convex on [20, ∞).
Proof: margiñ″(n) = 1/(2n) − 2ψ_F/(4n) − Σwᵢψᵢ/(4n) − IIMaj″(n)
≥ 1/(2n) − IIMaj″(n) > 0 (every ψ < 0 by the block table;
IIMaj″ < 1/(2n) by IIMaj_deriv2_lt).
Together with margiñ(8×10⁴) = 16 020 > 0 and margiñ′(8×10⁴) > 0
(E-028/E-029) this gives margin > 0 on [8×10⁴, N₁]. -/
theorem marginTilde_convex (F : ℝ → ℝ) (hF : ContDiffOn ℝ 2 F (Set.Ioi 1))
(hψ : ∀ T : ℝ, Real.sqrt 20 + 1 ≤ T →
deriv (deriv F) T - deriv F T / (T - 1) < 0) :
ConvexOn ℝ (Set.Ici 20) (marginTilde F) := by
have hCDfull : ContDiffOn ℝ 2 (marginTilde F) (Set.Ioi 20) := by
rw [marginTilde_eq_expanded F]
exact contDiffOn_marginExpanded F hF
apply convexOn_of_deriv2_nonneg (convex_Ici 20)
· rw [marginTilde_eq_expanded F]
exact continuousOn_marginExpanded F hF
· rw [interior_Ici]
exact hCDfull.differentiableOn (by norm_num)
· rw [interior_Ici]
exact ((hCDfull.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num))).differentiableOn
one_ne_zero
· intro n hn
rw [interior_Ici] at hn
have hn20 : 20 < n := hn
have hn0 : (0 : ℝ) < n := by linarith
have hn4 : (0 : ℝ) < 4 * n := by linarith
have hTn : Real.sqrt 20 + 1 ≤ Real.sqrt n + 1 := by
have h := Real.sqrt_le_sqrt (show (20 : ℝ) ≤ n by linarith)
linarith
-- diff-fact helpers
have hdd : ∀ {P : ℝ → ℝ}, ContDiffOn ℝ 2 P (Set.Ioi 20) →
DifferentiableAt ℝ (deriv P) n := fun hCD =>
((hCD.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn
one_ne_zero).differentiableAt (Ioi_mem_nhds hn20)
have hev : ∀ {P : ℝ → ℝ}, ContDiffOn ℝ 2 P (Set.Ioi 20) →
(∀ᶠ m in 𝓝 n, DifferentiableAt ℝ P m) := fun hCD => by
filter_upwards [Ioi_mem_nhds hn20] with m hm
exact (hCD.differentiableOn (by norm_num)).differentiableAt (Ioi_mem_nhds hm)
-- unweighted composition bundles
have hCDFc : ContDiffOn ℝ 2 (fun m => F (Real.sqrt m + 1)) (Set.Ioi 20) :=
hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1
have hCDTL1c : ContDiffOn ℝ 2
(fun m => (fun t => t * Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=
contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
have hCDTL2c : ContDiffOn ℝ 2
(fun m => (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))
(Set.Ioi 20) :=
contDiffOn_TL2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
have hCDL1sqc : ContDiffOn ℝ 2
(fun m => (fun t => Real.log (t + 2) ^ 2) (Real.sqrt m + 1)) (Set.Ioi 20) :=
contDiffOn_L1sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
have hCDL1L2c : ContDiffOn ℝ 2
(fun m => (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))
(Real.sqrt m + 1)) (Set.Ioi 20) :=
contDiffOn_L1L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
have hCDL2sqc : ContDiffOn ℝ 2
(fun m => (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt m + 1))
(Set.Ioi 20) :=
contDiffOn_L2sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
have hCDL1c : ContDiffOn ℝ 2
(fun m => (fun t => Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=
contDiffOn_L1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
have hCDL2c : ContDiffOn ℝ 2
(fun m => (fun t => Real.log (Real.log (t + 2))) (Real.sqrt m + 1))
(Set.Ioi 20) :=
contDiffOn_L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift
have hCDIIM : ContDiffOn ℝ 2 IIMaj (Set.Ioi 20) := by
have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=
funext fun m => IIMaj_eq_psiTilde_sqrt m
rw [hId]
exact (psiTilde_contDiff.contDiffOn).comp
(contDiffOn_id.sqrt (fun x hx => by
have h : 20 < x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x))) (Set.mapsTo_univ _ _)
-- piece values
have vS : deriv (deriv fun m => (1/2)*m*Real.log m +
(lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n = 1/(2*n) :=
marginS_deriv2 _ hn0
have vF : deriv (deriv (mFblock F)) n =
(-4) * (psiOf F (Real.sqrt n + 1) / (4 * n)) := by
unfold mFblock
rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),
chain_rule_sqrt_shift_on F (le_refl 1) hF n hn0, ← psiOf_sqrt_rel]
have vTL1 : deriv (deriv mTL1b) n = (-((8/3)*0.6 + 42)) *
(psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by
unfold mTL1b
rw [deriv2_const_mul _ (hdd hCDTL1c) (hev hCDTL1c),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_TL1 n hn0, ← psiOf_sqrt_rel]
have vTL2 : deriv (deriv mTL2b) n = (-((8/3)*0.886)) *
(psiOf (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by
unfold mTL2b
rw [deriv2_const_mul _ (hdd hCDTL2c) (hev hCDTL2c),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_TL2 n hn0, ← psiOf_sqrt_rel]
have vId : deriv (deriv mIdb) n = (-(((8/3)*2.7 + 192) + (Real.exp (5/2) + 1) / 2)) *
(psiOf id (Real.sqrt n + 1) / (4 * n)) := by
unfold mIdb
have hCDidc : ContDiffOn ℝ 2 (fun m => id (Real.sqrt m + 1)) (Set.Ioi 20) :=
contDiffOn_id.comp contDiffOn_sqrt_shift (Set.mapsTo_univ _ _)
rw [show (fun m => -(((8/3)*2.7 + 192) + (Real.exp (5/2) + 1) / 2) * (Real.sqrt m + 1)) =
(fun m => -(((8/3)*2.7 + 192) + (Real.exp (5/2) + 1) / 2) * id (Real.sqrt m + 1)) from rfl,
deriv2_const_mul _ (hdd hCDidc) (hev hCDidc),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_id n hn0, ← psiOf_sqrt_rel]
have vL1sq : deriv (deriv mL1sqb) n = (-(42*0.433^2*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (t + 2) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by
unfold mL1sqb
rw [deriv2_const_mul _ (hdd hCDL1sqc) (hev hCDL1sqc),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1sq n hn0, ← psiOf_sqrt_rel]
have vL1L2 : deriv (deriv mL1L2b) n = (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))
(Real.sqrt n + 1) / (4 * n)) := by
unfold mL1L2b
rw [deriv2_const_mul _ (hdd hCDL1L2c) (hev hCDL1L2c),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1L2 n hn0, ← psiOf_sqrt_rel]
have vL2sq : deriv (deriv mL2sqb) n = (-(42*0.886^2*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by
unfold mL2sqb
rw [deriv2_const_mul _ (hdd hCDL2sqc) (hev hCDL2sqc),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L2sq n hn0, ← psiOf_sqrt_rel]
have vL1 : deriv (deriv mL1b) n = (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by
unfold mL1b
rw [deriv2_const_mul _ (hdd hCDL1c) (hev hCDL1c),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L1 n hn0, ← psiOf_sqrt_rel]
have vL2 : deriv (deriv mL2b) n = (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by
unfold mL2b
rw [deriv2_const_mul _ (hdd hCDL2c) (hev hCDL2c),
chain_rule_sqrt_shift_on _ (by norm_num : (-1 : ℝ) ≤ 1) contDiffOn_L2 n hn0, ← psiOf_sqrt_rel]
have vIIM : deriv (deriv mIIM) n = (-1.5) * deriv (deriv IIMaj) n := by
unfold mIIM
rw [deriv2_const_mul (-1.5) (hdd hCDIIM) (hev hCDIIM)]
-- prefix ContDiffOn chain
have hCD1 := (contDiffOn_mS (lagariasC1 - Real.eulerMascheroniConstant/2)).add
(contDiffOn_mFblock F hF)
have hCD2 := hCD1.add contDiffOn_mTL1b
have hCD3 := hCD2.add contDiffOn_mTL2b
have hCD4 := hCD3.add contDiffOn_mIdb
have hCD5 := hCD4.add contDiffOn_mL1sqb
have hCD6 := hCD5.add contDiffOn_mL1L2b
have hCD7 := hCD6.add contDiffOn_mL2sqb
have hCD8 := hCD7.add contDiffOn_mL1b
have hCD9 := hCD8.add contDiffOn_mL2b
have hCD10 := hCD9.add contDiffOn_mIIM
-- split the sum
rw [marginTilde_eq_expanded F]
show (0 : ℝ) ≤ deriv (deriv (marginExpanded F)) n
unfold marginExpanded
dsimp only
rw [deriv2_add (hdd hCD10) (hdd contDiffOn_const) (hev hCD10) (hev contDiffOn_const),
deriv2_const_val,
deriv2_add (hdd hCD9) (hdd contDiffOn_mIIM) (hev hCD9) (hev contDiffOn_mIIM), vIIM,
deriv2_add (hdd hCD8) (hdd contDiffOn_mL2b) (hev hCD8) (hev contDiffOn_mL2b), vL2,
deriv2_add (hdd hCD7) (hdd contDiffOn_mL1b) (hev hCD7) (hev contDiffOn_mL1b), vL1,
deriv2_add (hdd hCD6) (hdd contDiffOn_mL2sqb) (hev hCD6) (hev contDiffOn_mL2sqb),
vL2sq,
deriv2_add (hdd hCD5) (hdd contDiffOn_mL1L2b) (hev hCD5) (hev contDiffOn_mL1L2b),
vL1L2,
deriv2_add (hdd hCD4) (hdd contDiffOn_mL1sqb) (hev hCD4) (hev contDiffOn_mL1sqb),
vL1sq,
deriv2_add (hdd hCD3) (hdd contDiffOn_mIdb) (hev hCD3) (hev contDiffOn_mIdb), vId,
deriv2_add (hdd hCD2) (hdd contDiffOn_mTL2b) (hev hCD2) (hev contDiffOn_mTL2b), vTL2,
deriv2_add (hdd hCD1) (hdd contDiffOn_mTL1b) (hev hCD1) (hev contDiffOn_mTL1b), vTL1,
deriv2_add (hdd (contDiffOn_mS _)) (hdd (contDiffOn_mFblock F hF))
(hev (contDiffOn_mS _)) (hev (contDiffOn_mFblock F hF)), vS, vF]
-- sign assembly: every ψ-term is nonneg
have hψn : psiOf F (Real.sqrt n + 1) < 0 := hψ _ hTn
have hnn1 : (0 : ℝ) ≤ -4 * (psiOf F (Real.sqrt n + 1) / (4 * n)) :=
mul_nonneg_of_nonpos_of_nonpos (by norm_num)
(div_neg_of_neg_of_pos hψn hn4).le
have hnn2 : (0 : ℝ) ≤ (-((8/3)*0.6 + 42)) *
(psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) :=
mul_nonneg_of_nonpos_of_nonpos (by norm_num)
(div_neg_of_neg_of_pos (psiOf_T_mul_log_shift_neg hTn) hn4).le
have hnn3 : (0 : ℝ) ≤ (-((8/3)*0.886)) *
(psiOf (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) :=
mul_nonneg_of_nonpos_of_nonpos (by norm_num)
(div_neg_of_neg_of_pos (psiOf_T_mul_log_log_shift_neg hTn) hn4).le
have hnn4 : (0 : ℝ) ≤ (-(((8/3)*2.7 + 192) + (Real.exp (5/2) + 1) / 2)) *
(psiOf id (Real.sqrt n + 1) / (4 * n)) := by
have hp : psiOf id (Real.sqrt n + 1) < 0 :=
(psiOf_id (Real.sqrt n + 1) (by
have h := Real.sqrt_pos.mpr hn0
linarith)).2
have hw : (-(((8/3)*2.7 + 192) + (Real.exp (5/2) + 1) / 2) : ℝ) ≤ 0 := by
have hE := Real.exp_pos (5 / 2)
nlinarith [hE]
exact mul_nonneg_of_nonpos_of_nonpos hw
(div_neg_of_neg_of_pos hp hn4).le
have hnn5 : (0 : ℝ) ≤ (-(42*0.433^2*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (t + 2) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by
have hw : (-(42*0.433^2*(Real.exp 4 + 1)) : ℝ) ≤ 0 := by
have hE := Real.exp_pos 4
nlinarith [hE]
exact mul_nonneg_of_nonpos_of_nonpos hw
(div_neg_of_neg_of_pos (psiOf_log_sq_shift_neg hTn) hn4).le
have hnn6 : (0 : ℝ) ≤ (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))
(Real.sqrt n + 1) / (4 * n)) := by
have hw : (-(42*(2*0.433*0.886)*(Real.exp 4 + 1)) : ℝ) ≤ 0 := by
have hE := Real.exp_pos 4
nlinarith [hE]
exact mul_nonneg_of_nonpos_of_nonpos hw
(div_neg_of_neg_of_pos (psiOf_log_mul_log_shift_neg hTn) hn4).le
have hnn7 : (0 : ℝ) ≤ (-(42*0.886^2*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by
have hw : (-(42*0.886^2*(Real.exp 4 + 1)) : ℝ) ≤ 0 := by
have hE := Real.exp_pos 4
nlinarith [hE]
exact mul_nonneg_of_nonpos_of_nonpos hw
(div_neg_of_neg_of_pos (psiOf_log_log_sq_shift_neg hTn) hn4).le
have hnn8 : (0 : ℝ) ≤ (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by
have hw : (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1)) : ℝ) ≤ 0 := by
have hE := Real.exp_pos 4
nlinarith [hE]
exact mul_nonneg_of_nonpos_of_nonpos hw
(div_neg_of_neg_of_pos (psiOf_log_shift_neg (by
have h := Real.sqrt_pos.mpr hn0
linarith)) hn4).le
have hnn9 : (0 : ℝ) ≤ (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *
(psiOf (fun t => Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by
have hw : (-(42*(2*0.886*2.9)*(Real.exp 4 + 1)) : ℝ) ≤ 0 := by
have hE := Real.exp_pos 4
nlinarith [hE]
exact mul_nonneg_of_nonpos_of_nonpos hw
(div_neg_of_neg_of_pos (psiOf_log_log_shift_neg (by
have h := Real.sqrt_pos.mpr hn0
linarith)) hn4).le
have hIIM := IIMaj_deriv2_lt_three (show 20 ≤ n by linarith)
have hbridge : (1.5 : ℝ) * (1 / (3 * n)) = 1 / (2 * n) := by
have h1 : (0 : ℝ) < 3 * n := by linarith [hn0]
have h2 : (0 : ℝ) < 2 * n := by linarith [hn0]
rw [mul_one_div, div_eq_div_iff h1.ne' h2.ne']
ring
linarith [hIIM, hbridge, hnn1, hnn2, hnn3, hnn4, hnn5, hnn6, hnn7, hnn8, hnn9]
/-! ## 4. Tier (ii) step 1 (session 012): the finite-height Li theorem,
assembled modulo the single named analytic hypothesis `SfBoundProp`.
Design (session-012-notes.txt, D-062 triage): the theorem is proved from
(i) `SfBoundProp` — the remaining analytic obligation, isolated;
(ii) the computational perimeter: `RHUpTo` (Platt–Trudgian 2021) and
`LiVerifiedUpTo` (E-011/E-015 to 3000 + Johansson 2015 § 4.2 to
10⁵ — rigorous ordinary-λ_n interval computation);
(iii) two elementary evaluations of the explicit margin function
(E-028/E-029 values, dischargeable by rational interval
bounds — tier (ii) step 2).
The D-036/D-056 contour estimate, the Trudgian N(T)/S(T) input, and the
RH-to-height bridge all live INSIDE `SfBoundProp`'s eventual proof, not
in the assembly below. -/
/-- The explicit zero-count majorant used in the assembly (session 012):
FAlt(T) = (1/2π)·T·log T + 0.137·log T + 0.443·log log T + (7/8 + 1.588).
This is Trudgian 2014's F(T) + S_b(T) (F(T) = (T/2π)log(T/2πe) + 7/8,
S_b(T) = 0.137 log T + 0.443 log log T + 1.588) with the negative-weight
term −(log 2πe/2π)·T DROPPED, so FAlt ≥ F + S_b pointwise for T ≥ 0 and
any literature bound N(T) ≤ F(T) + S_b(T) upgrades to N(T) ≤ FAlt(T).
The swap is needed because ψ[F + S_b] crosses POSITIVE on [5.47, ~16]
(the dropped term has negative weight against a negative-ψ block), while
every FAlt block has provably negative ψ (D-057 rows #1/#3/#4). Margin
cost: 2·(log 2πe/2π)·T ≈ 0.9√n, negligible vs margiñ(8×10⁴) ≈ 1.6×10⁴
(E-028). Domain note: smooth only on (1, ∞) (log log needs T > 1); the
margin composition hits only T = √n + 1 ≥ √20 + 1 > 1. -/
def FAlt (T : ℝ) : ℝ :=
(1 / (2 * Real.pi)) * (T * Real.log T) + 0.137 * Real.log T +
0.443 * Real.log (Real.log T) + (7 / 8 + 1.588)
/-- The explicit finite-part bound B(n) (D-037 (4.1) CORRECTED per D-071,
user-approved session 038; REPAIRED per D-074, session 040; constants
A = 10.5, B₀ = 48 from D-056; Ĉ₀/Ĥ/Z₂ closed forms; M₀ = 1.3352 from
E-023; IIMaj the I_I majorant), with the zero-count majorant F as a
parameter:
B(n) = 4F(T) + 4T[(2/3)Z₂(T) + 10.5·log(T+2) + 48] + 40·1.3352
+ 2(e⁴+1)·7Ĥ(T) + 2·DogLegRight(n) + IIMaj(n) + 1, T = √n + 1.
The corrections: (D-071 F-A/F-B) the bridge is 4F (both-signs slip,
R-004 unaffected) and the I_III near-sum uses (2/3)Z₂ (D-069 Finding 2
made exact). (D-074, the F-D REPAIR) the horizontal right tail
[3, 2√n] is bounded by the zero-free dog-leg deformation (T_cut = √n
KEPT, the tail lifted to U = (3/2)√n through the unconditionally
zero-free region Re ≥ 3 — DL-1..DL-6, E-034-validated): the broken
"3.3" charge (D-072) is replaced by 2·DogLegRight(n) =
(√n+1)(e^{5/2}+1)/2 + 16.76 + IIMaj(n)/2 — the ORIGINAL endpoint
N₁ = (T₀−1)² ≈ 9×10²⁴ is PRESERVED. -/
def Bn (F : ℝ → ℝ) (n : ℝ) : ℝ :=
let T := Real.sqrt n + 1
4 * F T + 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +
40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T) +
2 * DogLegRight n + IIMaj n + 1
/-- [PROVED session 012] The margin IS sInftyLower − Bn + 1 (pure
bookkeeping; same constants as `marginTilde_eq_expanded`). -/
theorem marginTilde_eq_sub (F : ℝ → ℝ) (n : ℝ) :
marginTilde F n = sInftyLower n - Bn F n + 1 := by
simp only [marginTilde, Bn, sInftyLower]
/-- The finite part S_f(n) of the Bombieri–Lagarias decomposition
λ_n = S_∞(n) − S_f(n) + 1 (BL 1999 Thm 2, D-037 P1), here DEFINED by the
identity rearranged (λ_n is real by conjugate symmetry, so taking the
real part is no loss — see `LiVerifiedUpTo`). The analytic content — that
this quantity is bounded by B(n) — is isolated in `SfBoundProp`. -/
def Sf (n : ℕ) : ℝ := SInfty n + 1 - (liCoeff n).re
/-- ⭐ THE named analytic hypothesis of tier (ii): the finite part is
bounded by the explicit traced B(n) on the whole margin range
10⁵ ≤ n ≤ N₁ = (T₀−1)², T₀ = 3×10¹².
Proof content (triage D-062): the D-036/D-056 contour estimate — kernel
bounds + reference-point R-bound (Mathlib-tractable complex analysis),
Trudgian 2014 N(T)/S(T) (trusted-perimeter literature candidate), the
bridge via `RHUpTo` (perimeter), M₀ (E-023 grid; E-023b acb optional). -/
def SfBoundProp : Prop :=
∀ n : ℕ, 100000 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →
|Sf n| ≤ Bn FAlt (n : ℝ)
/-! ### The ψ-blocks of FAlt (D-057 table rows #1/#3/#4) -/
/-- [PROVED session 012] Per-point derivative of T·log T. -/
theorem hasDerivAt_T_mul_log (x : ℝ) (hx : 0 < x) :
HasDerivAt (fun t => t * Real.log t) (Real.log x + 1) x := by
have h := (hasDerivAt_id' x).mul (Real.hasDerivAt_log (ne_of_gt hx))
rwa [one_mul, mul_inv_cancel₀ (ne_of_gt hx)] at h
/-- [PROVED session 012] Block #1 (T·log T): ψ-formula. -/
theorem psiOf_T_mul_log (T : ℝ) (hT : 1 < T) :
psiOf (fun t => t * Real.log t) T =
1 / T - (Real.log T + 1) / (T - 1) := by
have hT0 : (0 : ℝ) < T := by linarith
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => t * Real.log t) (Real.log x + 1) x := by
filter_upwards [eventually_gt_nhds hT0] with x hx
exact hasDerivAt_T_mul_log x hx
have h2 : HasDerivAt (fun t => Real.log t + 1) T⁻¹ T :=
(Real.hasDerivAt_log (ne_of_gt hT0)).add_const 1
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => t * Real.log t) T = Real.log T + 1 := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1, one_div]
/-- [PROVED session 012] Block #1 sign: ψ < 0 for T > 1
(⟺ −1 < T·log T, D-057 row #1). -/
theorem psiOf_T_mul_log_neg {T : ℝ} (hT : 1 < T) :
psiOf (fun t => t * Real.log t) T < 0 := by
rw [psiOf_T_mul_log T hT]
have hT0 : (0 : ℝ) < T := by linarith
have hT1 : (0 : ℝ) < T - 1 := by linarith
have hlog : (0 : ℝ) < Real.log T := Real.log_pos hT
have key : (1 : ℝ) / T < (Real.log T + 1) / (T - 1) := by
rw [div_lt_div_iff₀ hT0 hT1]
nlinarith [mul_pos hT0 hlog]
linarith
/-- [PROVED session 012] Block #3 (log T): ψ-formula. -/
theorem psiOf_log (T : ℝ) (hT : 1 < T) :
psiOf Real.log T = -1 / T ^ 2 - 1 / (T * (T - 1)) := by
have hT0 : (0 : ℝ) < T := by linarith
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt Real.log x⁻¹ x := by
filter_upwards [eventually_gt_nhds hT0] with x hx
exact Real.hasDerivAt_log (ne_of_gt hx)
have h2 : HasDerivAt (fun t : ℝ => t⁻¹) (-1 / T ^ 2) T := by
have h := (hasDerivAt_id' T).inv (ne_of_gt hT0)
have e : (-(1 : ℝ)) / T ^ 2 = -1 / T ^ 2 := by ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv Real.log T = T⁻¹ := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
field_simp [ne_of_gt hT0, hT1]
/-- [PROVED session 012] Block #3 sign: ψ < 0 for T > 1. -/
theorem psiOf_log_neg {T : ℝ} (hT : 1 < T) :
psiOf Real.log T < 0 := by
rw [psiOf_log T hT]
have h1 : (0 : ℝ) < 1 / T ^ 2 := one_div_pos.mpr (pow_pos (by linarith) 2)
have h2 : (0 : ℝ) < 1 / (T * (T - 1)) :=
one_div_pos.mpr (mul_pos (by linarith) (by linarith))
have e : -1 / T ^ 2 - 1 / (T * (T - 1)) = -(1 / T ^ 2 + 1 / (T * (T - 1))) := by ring
rw [e]
linarith [add_pos h1 h2]
/-- [PROVED session 012] Per-point derivative of log log T. -/
theorem hasDerivAt_log_log_unshifted (x : ℝ) (hx : 1 < x) :
HasDerivAt (fun t => Real.log (Real.log t)) ((Real.log x)⁻¹ * x⁻¹) x := by
have hin : HasDerivAt Real.log x⁻¹ x :=
Real.hasDerivAt_log (ne_of_gt (by linarith : (0 : ℝ) < x))
have hout : HasDerivAt Real.log (Real.log x)⁻¹ (Real.log x) :=
Real.hasDerivAt_log (ne_of_gt (Real.log_pos hx))
exact hout.comp x hin
/-- [PROVED session 012] Block #4 (log log T): ψ-formula. -/
theorem psiOf_log_log (T : ℝ) (hT : 1 < T) :
psiOf (fun t => Real.log (Real.log t)) T =
-(Real.log T + 1) / ((T * Real.log T) ^ 2) -
1 / (T * Real.log T * (T - 1)) := by
have hT0 : (0 : ℝ) < T := by linarith
have hL1 : (0 : ℝ) < Real.log T := Real.log_pos hT
have h1 : ∀ᶠ x in 𝓝 T, HasDerivAt (fun t => Real.log (Real.log t))
((Real.log x)⁻¹ * x⁻¹) x := by
filter_upwards [eventually_gt_nhds hT] with x hx
exact hasDerivAt_log_log_unshifted x hx
have h2 : HasDerivAt (fun t => (Real.log t)⁻¹ * t⁻¹)
(-(Real.log T + 1) / ((T * Real.log T) ^ 2)) T := by
have hu : HasDerivAt (fun t => (Real.log t)⁻¹) (-T⁻¹ / (Real.log T) ^ 2) T :=
(Real.hasDerivAt_log (ne_of_gt hT0)).inv (ne_of_gt hL1)
have hv : HasDerivAt (fun t : ℝ => t⁻¹) (-1 / T ^ 2) T := by
have h := (hasDerivAt_id' T).inv (ne_of_gt hT0)
have e : (-(1 : ℝ)) / T ^ 2 = -1 / T ^ 2 := by ring
rwa [e] at h
have h := hu.mul hv
have hT0' : T ≠ 0 := ne_of_gt hT0
have hL1' : Real.log T ≠ 0 := ne_of_gt hL1
have e : (-T⁻¹ / (Real.log T) ^ 2) * T⁻¹ + (Real.log T)⁻¹ * (-1 / T ^ 2) =
-(Real.log T + 1) / ((T * Real.log T) ^ 2) := by
field_simp [hT0', hL1']
ring
rwa [e] at h
have hd2 := deriv2_of_hasDerivAt_nhds h1 h2
have hd1 : deriv (fun t => Real.log (Real.log t)) T =
(Real.log T)⁻¹ * T⁻¹ := h1.self_of_nhds.deriv
unfold psiOf
rw [hd2, hd1]
have hT1 : (T - 1) ≠ 0 := by linarith
have hT0' : T ≠ 0 := ne_of_gt hT0
have hL1' : Real.log T ≠ 0 := ne_of_gt hL1
field_simp [hT0', hL1', hT1]
/-- [PROVED session 012] Block #4 sign: ψ < 0 for T > 1. -/
theorem psiOf_log_log_neg {T : ℝ} (hT : 1 < T) :
psiOf (fun t => Real.log (Real.log t)) T < 0 := by
rw [psiOf_log_log T hT]
have hT0 : (0 : ℝ) < T := by linarith
have hL1 : (0 : ℝ) < Real.log T := Real.log_pos hT
have hp1 : (0 : ℝ) < (Real.log T + 1) / ((T * Real.log T) ^ 2) :=
div_pos (by linarith) (pow_pos (mul_pos hT0 hL1) 2)
have hp2 : (0 : ℝ) < 1 / (T * Real.log T * (T - 1)) :=
one_div_pos.mpr (mul_pos (mul_pos hT0 hL1) (by linarith))
have e : -(Real.log T + 1) / ((T * Real.log T) ^ 2) -
1 / (T * Real.log T * (T - 1)) =
-((Real.log T + 1) / ((T * Real.log T) ^ 2) +
1 / (T * Real.log T * (T - 1))) := by ring
rw [e]
linarith [add_pos hp1 hp2]
/-- [PROVED session 012] FAlt is C² on (1, ∞). -/
theorem contDiffOn_FAlt : ContDiffOn ℝ 2 FAlt (Set.Ioi 1) := by
have hA : ContDiffOn ℝ 2 (fun t : ℝ => t * Real.log t) (Set.Ioi 1) :=
contDiffOn_id.mul (contDiffOn_id.log (fun x hx => by
have h : 1 < x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x)))
have hB : ContDiffOn ℝ 2 Real.log (Set.Ioi 1) :=
contDiffOn_id.log (fun x hx => by
have h : 1 < x := hx
exact ne_of_gt (by linarith : (0 : ℝ) < x))
have hC : ContDiffOn ℝ 2 (fun t : ℝ => Real.log (Real.log t)) (Set.Ioi 1) :=
hB.log (fun x hx => ne_of_gt (Real.log_pos hx))
unfold FAlt
exact (((contDiffOn_const.mul hA).add (contDiffOn_const.mul hB)).add
(contDiffOn_const.mul hC)).add contDiffOn_const
/-- [PROVED session 012] ψ-condition for FAlt (the D-057 rows #1/#3/#4
assembly): deriv(deriv FAlt) T − deriv FAlt T/(T−1) < 0 for
T ≥ √20 + 1. All three weights positive, all three brackets negative. -/
theorem FAlt_psi_neg (T : ℝ) (hT : Real.sqrt 20 + 1 ≤ T) :
deriv (deriv FAlt) T - deriv FAlt T / (T - 1) < 0 := by
have hs : (4.4721 : ℝ) ≤ Real.sqrt 20 := by
rw [Real.le_sqrt (by norm_num) (by norm_num)]
norm_num
have h1T : 1 < T := by linarith
have hT0 : (0 : ℝ) < T := by linarith
have hT1 : (0 : ℝ) < T - 1 := by linarith
have hL1 : (0 : ℝ) < Real.log T := Real.log_pos h1T
-- first derivative of FAlt, valid in a neighborhood of T
have hD1 : ∀ᶠ x in 𝓝 T, HasDerivAt FAlt
((1 / (2 * Real.pi)) * (Real.log x + 1) + 0.137 * x⁻¹ +
0.443 * ((Real.log x)⁻¹ * x⁻¹)) x := by
filter_upwards [eventually_gt_nhds h1T] with x hx
have hx0 : (0 : ℝ) < x := by linarith
have hA := (hasDerivAt_T_mul_log x hx0).const_mul (1 / (2 * Real.pi))
have hB := (Real.hasDerivAt_log (ne_of_gt hx0)).const_mul (0.137 : ℝ)
have hC := (hasDerivAt_log_log_unshifted x hx).const_mul (0.443 : ℝ)
have hK : HasDerivAt (fun _ : ℝ => (7 / 8 + 1.588 : ℝ)) 0 x :=
hasDerivAt_const x _
have h := ((hA.add hB).add hC).add hK
have e : (1 / (2 * Real.pi)) * (Real.log x + 1) + 0.137 * x⁻¹ +
0.443 * ((Real.log x)⁻¹ * x⁻¹) + 0 =
(1 / (2 * Real.pi)) * (Real.log x + 1) + 0.137 * x⁻¹ +
0.443 * ((Real.log x)⁻¹ * x⁻¹) := by ring
rwa [← e]
-- second derivative at T
have hD2 : HasDerivAt
(fun t => (1 / (2 * Real.pi)) * (Real.log t + 1) + 0.137 * t⁻¹ +
0.443 * ((Real.log t)⁻¹ * t⁻¹))
((1 / (2 * Real.pi)) * T⁻¹ + 0.137 * (-1 / T ^ 2) +
0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2))) T := by
have hA := ((Real.hasDerivAt_log (ne_of_gt hT0)).add_const 1).const_mul
(1 / (2 * Real.pi))
have hv : HasDerivAt (fun t : ℝ => t⁻¹) (-1 / T ^ 2) T := by
have h := (hasDerivAt_id' T).inv (ne_of_gt hT0)
have e : (-(1 : ℝ)) / T ^ 2 = -1 / T ^ 2 := by ring
rwa [e] at h
have hB := hv.const_mul (0.137 : ℝ)
have hu : HasDerivAt (fun t => (Real.log t)⁻¹) (-T⁻¹ / (Real.log T) ^ 2) T :=
(Real.hasDerivAt_log (ne_of_gt hT0)).inv (ne_of_gt hL1)
have hC := (hu.mul hv).const_mul (0.443 : ℝ)
have h := (hA.add hB).add hC
have hT0' : T ≠ 0 := ne_of_gt hT0
have hL1' : Real.log T ≠ 0 := ne_of_gt hL1
have e : (1 / (2 * Real.pi)) * T⁻¹ + 0.137 * (-1 / T ^ 2) +
0.443 * ((-T⁻¹ / (Real.log T) ^ 2) * T⁻¹ + (Real.log T)⁻¹ * (-1 / T ^ 2)) =
(1 / (2 * Real.pi)) * T⁻¹ + 0.137 * (-1 / T ^ 2) +
0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2)) := by
field_simp [hT0', hL1']
ring
rwa [e] at h
have hd1 : deriv FAlt T = (1 / (2 * Real.pi)) * (Real.log T + 1) + 0.137 * T⁻¹ +
0.443 * ((Real.log T)⁻¹ * T⁻¹) := hD1.self_of_nhds.deriv
have hd2 : deriv (deriv FAlt) T = (1 / (2 * Real.pi)) * T⁻¹ +
0.137 * (-1 / T ^ 2) + 0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2)) :=
deriv2_of_hasDerivAt_nhds hD1 hD2
-- the three negative brackets (reused block signs)
have hbrA := psiOf_T_mul_log_neg h1T
rw [psiOf_T_mul_log T h1T] at hbrA
have hbrB := psiOf_log_neg h1T
rw [psiOf_log T h1T] at hbrB
have hbrC := psiOf_log_log_neg h1T
rw [psiOf_log_log T h1T] at hbrC
have hc1 : (0 : ℝ) < 1 / (2 * Real.pi) := by positivity
-- assemble: ψ = c₁·brA + c₂·brB + c₃·brC < 0
have hT0' : T ≠ 0 := ne_of_gt hT0
have hL1' : Real.log T ≠ 0 := ne_of_gt hL1
have hsum : deriv (deriv FAlt) T - deriv FAlt T / (T - 1) =
(1 / (2 * Real.pi)) * (1 / T - (Real.log T + 1) / (T - 1)) +
0.137 * (-1 / T ^ 2 - 1 / (T * (T - 1))) +
0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2) -
1 / (T * Real.log T * (T - 1))) := by
rw [hd1, hd2]
field_simp [hT0', hL1', hT1.ne']
ring
rw [hsum]
have h1 : (1 / (2 * Real.pi)) * (1 / T - (Real.log T + 1) / (T - 1)) < 0 :=
mul_neg_of_pos_of_neg hc1 hbrA
have h2' : 0.137 * (-1 / T ^ 2 - 1 / (T * (T - 1))) < 0 :=
mul_neg_of_pos_of_neg (by norm_num) hbrB
have h3' : 0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2) -
1 / (T * Real.log T * (T - 1))) < 0 :=
mul_neg_of_pos_of_neg (by norm_num) hbrC
linarith [h1, h2', h3']
/-- [PROVED session 012] Convexity + positive base point + positive base
derivative ⟹ positivity on the whole tail (MVT + monotone derivative). -/
theorem pos_of_convex_of_base {f : ℝ → ℝ} {a N₀ x : ℝ}
(hconv : ConvexOn ℝ (Set.Ici a) f)
(hdiff : ∀ y : ℝ, y ∈ Set.Ioi a → DifferentiableAt ℝ f y)
(hN : a < N₀) (hx : N₀ ≤ x) (h0 : 0 < f N₀) (h0' : 0 < deriv f N₀) :
0 < f x := by
rcases eq_or_lt_of_le hx with heq | hlt
· rw [← heq]
exact h0
· have hfc : ContinuousOn f (Set.Icc N₀ x) :=
DifferentiableOn.continuousOn (s := Set.Icc N₀ x) (f := f) fun y hy =>
(hdiff y (Set.mem_Ioi.mpr (by
have h1 : N₀ ≤ y := hy.1
linarith))).differentiableWithinAt
have hfd : DifferentiableOn ℝ f (Set.Ioo N₀ x) := fun y hy =>
(hdiff y (Set.mem_Ioi.mpr (by
have h1 : N₀ < y := hy.1
linarith))).differentiableWithinAt
obtain ⟨ξ, hξ, hξeq⟩ := exists_deriv_eq_slope f hlt hfc hfd
have hconv' : ConvexOn ℝ (Set.Ici N₀) f :=
hconv.subset (Set.Ici_subset_Ici.mpr (le_of_lt hN)) (convex_Ici N₀)
have hfd' : ∀ y : ℝ, y ∈ Set.Ici N₀ → DifferentiableAt ℝ f y := by
intro y hy
have : a < y := by
have : N₀ ≤ y := hy
linarith
exact hdiff y this
have hmono : deriv f N₀ ≤ deriv f ξ :=
(hconv'.monotoneOn_deriv hfd') (Set.mem_Ici.mpr (le_refl N₀))
(Set.mem_Ici.mpr (le_of_lt hξ.1)) (le_of_lt hξ.1)
have hpos : (0 : ℝ) < x - N₀ := sub_pos.mpr hlt
have hkey : (0 : ℝ) < (f x - f N₀) / (x - N₀) :=
hξeq ▸ lt_of_lt_of_le h0' hmono
have hfx : (0 : ℝ) < f x - f N₀ := (div_pos_iff_of_pos_right hpos).mp hkey
linarith
/-- [PROVED session 012] Convexity + f(N₀) > 0 + f(N₁) > f(N₀) ⟹
positivity on [N₁, ∞) (three-chord secant monotonicity; the increasing
secant slope is positive, so f keeps climbing). Cheaper to discharge than
the derivative base point: two plain evaluations, no deriv machinery. -/
theorem pos_of_convex_of_two_points {f : ℝ → ℝ} {a N₀ N₁ x : ℝ}
(hconv : ConvexOn ℝ (Set.Ici a) f)
(hN : a < N₀) (hN01 : N₀ < N₁) (hx : N₁ ≤ x)
(h0 : 0 < f N₀) (h01 : f N₀ < f N₁) :
0 < f x := by
rcases eq_or_lt_of_le hx with heq | hlt
· rw [← heq]
linarith
· have hslope := hconv.slope_mono_adjacent
(Set.mem_Ici.mpr (le_of_lt hN)) (Set.mem_Ici.mpr (by linarith)) hN01 hlt
have hp1 : (0 : ℝ) < N₁ - N₀ := by linarith
have hp2 : (0 : ℝ) < x - N₁ := by linarith
have hs : (0 : ℝ) < (f N₁ - f N₀) / (N₁ - N₀) := div_pos (by linarith) hp1
have hs2 : (0 : ℝ) < (f x - f N₁) / (x - N₁) := lt_of_lt_of_le hs hslope
have hfx : (0 : ℝ) < f x - f N₁ := (div_pos_iff_of_pos_right hp2).mp hs2
linarith
/-- [PROVED session 012 — TIER (ii) STEP 1, assembly modulo `SfBoundProp`]
R-004, the finite-height Li theorem (draft Thm 3.1): assuming the named
analytic hypothesis `SfBoundProp`, the computational perimeter
(Platt–Trudgian RH-to-T₀, finite Li verification to 5×10⁵), and two
elementary evaluations of the explicit margin function (E-028/E-029
values: margiñ(8×10⁴) ≈ 1.58×10⁴ > 0 and margiñ(10⁵) ≈ 9.3×10⁴
> margiñ(8×10⁴); interval-bound discharge = tier (ii) step 2),
λ_n > 0 for all n ≤ (T₀−1)².
Proof: for n < 10⁵ use the perimeter finite verification; for
n ≥ 10⁵, λ_n = S_∞(n) − S_f(n) + 1 ≥ sInftyLower(n) − B(n) + 1
= margiñ(n) > 0 by convexity (`marginTilde_convex` + `FAlt_psi_neg`)
and the two base points (`pos_of_convex_of_two_points`).
`_hRH` documents the bridge input: it is consumed by `SfBoundProp`'s
eventual proof (D-037 §6), not by the assembly itself. -/
theorem lambda_pos_finite_height
(_hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (10 ^ 5))
(hbase : 0 < marginTilde FAlt 80000)
(hbase2 : marginTilde FAlt 80000 < marginTilde FAlt 100000)
(hSf : SfBoundProp) :
∀ n : ℕ, 1 ≤ n → (n : ℝ) ≤ (3 * 10 ^ 12 - 1 : ℝ) ^ 2 →
0 < (liCoeff n).re := by
intro n hn1 hnN
rcases lt_or_ge n 100000 with hlt | hge
· exact hfinite n hn1 (by omega)
· have hn20 : 20 ≤ n := by omega
have h1 := sInfty_lower_bound n hn20
have h2 := hSf n hge hnN
have h3 : (liCoeff n).re = SInfty n - Sf n + 1 := by
unfold Sf
ring
have h4 : marginTilde FAlt (n : ℝ) = sInftyLower (n : ℝ) - Bn FAlt (n : ℝ) + 1 :=
marginTilde_eq_sub FAlt n
have h5 : 0 < marginTilde FAlt (n : ℝ) :=
pos_of_convex_of_two_points
(marginTilde_convex FAlt contDiffOn_FAlt FAlt_psi_neg)
(by norm_num) (by norm_num) (by exact_mod_cast hge) hbase hbase2
have habs : Sf n ≤ |Sf n| := le_abs_self _
rw [h3]
linarith [h1, h2, h4, h5, habs]
end NguyenRH1
end