← Session 35 — ii′-6-R: Lagarias 6.1 right-tail re-proof (E-032/D-073)
thinking (5540 chars)
The diff is clean — exactly my intended changes. The timeouts are in the lt_three's `rw [e]; exact div_lt_div_of_pos_right hb h4n` and marginTilde_convex's final linarith. Since the ORIGINAL proof worked with the same structure (only the e form changed from field_simp to div_eq_div_iff), let me test whether the lt_three's `exact div_lt_div_of_pos_right hb h4n` is the actual loop by reverting JUST that proof to the original e form but keeping the lt_three statement:
Actually — hold on. Let me look at the original e more carefully:
Original: `have e : (1 : ℝ) / (2 * n) = 2 / (4 * n) := by field_simp [hn0.ne']; ring` then `rw [e]; exact div_lt_div_of_pos_right hb h4n`.
The original's `rw [e]` rewrites `1/(2n)` → `2/(4n)` in the GOAL (whose RHS is 1/(2n)) ✓ then exact div_lt_div_of_pos_right hb h4n : HUGE/(4n) < 2/(4n) ✓ — with hb : HUGE < 2 (original) ✓.
Mine: e : `1/(3n) = (4/3)/(4n)`; `rw [e]` rewrites `1/(3n)` → `(4/3)/(4n)`; exact div_lt_div_of_pos_right hb h4n : HUGE/(4n) < (4/3)/(4n) — with hb : HUGE < 4/3 ✓.
The structures are IDENTICAL. The whnf timeout at 800000 suggests the unification of HUGE with the goal's LHS is looping — but the original did the same unification fine?! Unless the iimaj_bracket_bound's PROOF is now broken (the statement change to < 4/3 + the proof's final norm_num — the bracket bound ITSELF is failing to elaborate, leaving hb in a weird state?).
Wait — maybe iimaj_bracket_bound ITSELF fails to compile now (statement < 4/3, proof unchanged except the last norm_num) — let me check if iimaj_bracket_bound alone compiles by testing it in isolation... — the whnf timeout at 2166:0 is at the lt_three theorem — if iimaj_bracket_bound failed to elaborate (its own proof), hb would be ill-formed and everything downstream loops. Let me check the build output more carefully for iimaj_bracket_bound's own errors — the error list showed NO error at iimaj_bracket_bound's lines (1498-1678) — only 2166/2191/2399/2777. Hmm — but the earlier error list DID show `1510:52: error: unsolved goals` (the calc.step at the < 4/3 final line) BEFORE I fixed the statement — and I fixed the statement to < 4/3 ✓ — so iimaj_bracket_bound should compile now... unless its norm_num at `< 4/3` leaves an unsolved goal because norm_num evaluates `4.56·1.2237·0.2124·1.1099 < 4/3` as... — my scratch probe PROVED that norm_num handles both comparisons instantly ✓. So iimaj_bracket_bound compiles ✓.
Hmm. Let me test the lt_three in isolation in a scratch with a stub iimaj_bracket_bound... — too heavy. Alternative: let me check if the whnf timeout is at `rw [e]` (2162) rather than the exact (2163). The `rw [e]` rewrites `1/(3n)` in the goal `closed-forms < 1/(3n)` — rewriting the RHS to `(4/3)/(4n)` ✓ should be instant.
Let me try a completely different final for lt_three that avoids div_lt_div_of_pos_right's huge unification: prove the chain via mul/div algebra:
```
rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,
deriv2_psiTilde]
have hbig := iimaj_bracket_bound (Real.sqrt_le_sqrt hn)
have h4n : (0 : ℝ) < 4 * n := by linarith
have hdiv := div_lt_div_of_pos_right hbig h4n
have heq : (1 : ℝ) / (3 * n) = (4 / 3) / (4 * n) := by
rw [div_eq_div_iff (by linarith [hn0] : (0 : ℝ) < 3 * n).ne'
(by linarith [hn0] : (0 : ℝ) < 4 * n).ne']
ring
rw [heq]
exact hdiv
```
That's the same thing. The loop must be in `exact hdiv` (or `exact div_lt_div_of_pos_right hb h4n`) unifying `HUGE/(4n)` with the goal's LHS — since the goal's LHS after the rewrites IS HUGE/(4n) syntactically... — hmm wait — is it? chain_rule_sqrt gives `deriv (deriv fun n => ψ (√n)) n = (ψ″(√n) − ψ′(√n)/√n)/(4n)` — with ψ := psiTilde — and then deriv_psiTilde/deriv2_psiTilde rewrite `deriv psiTilde (√n)` and `deriv (deriv psiTilde) (√n)` to the closed forms — but the goal's LHS is `deriv (deriv IIMaj) n` — the first rw [hId] turns IIMaj into `fun m => psiTilde (√m)` — then `chain_rule_sqrt psiTilde psiTilde_contDiff n hn0` rewrites `deriv (deriv fun n => psiTilde (√n)) n` to the chain-rule form ✓ then deriv_psiTilde/deriv2_psiTilde close the derivs ✓ — the final LHS = (deriv2_psiTilde-form(√n) − (deriv_psiTilde-form(√n))/√n)/(4n) — and hbig's HUGE = `4.56·(2·(−iimA·e^{−iimA·√n} − iimB·e^{−iimB·√n}) + (√n+1)·(iimA²·e^{−iimA·√n}+iimB²·e^{−iimB·√n})) − (4.56·((e^{−iimA·√n}+e^{−iimB·√n}) + (√n+1)·(−iimA·e^{−iimA·√n} − iimB·e^{−iimB·√n})))/√n` — the closed deriv forms from deriv_psiTilde/deriv2_psiTilde are EXACTLY these (from lines 1401–1411) ✓ SAME ✓.
So the exact unification SHOULD be syntactic and instant. The timeout must be environmental or from something else in the elaboration. Let me try compiling the ORIGINAL IIMaj_deriv2_lt (revert just the lt_three to its original form) to see if it compiles — if the ORIGINAL now ALSO times out, something environmental changed (maybe the div_eq_div_iff/div_lt_div_iff₀ fixes aren't the issue but the elaborator state from the many edits).
Actually — wait. Let me look at the error at 2191:2 («tactic execution») and 2399:6 more carefully. 2191:2 in the CURRENT file is marginTilde_convex's `intro n hn` — an intro timing out is bizarre. Unless... the elaborator is spending heartbeats from an EARLIER heavy error and each subsequent tactic fails on the residual state. The FIRST error is at 2166:0 — the lt_three. If I fix that, the rest likely clears.
Let me try compiling lt_three's proof with `set_option maxHeartbeats 1600000` (2x the bracket's budget) — if it passes, it's just expensive, not a loop.
Trying 1.6M heartbeats on the lt_three to distinguish expensive-vs-looping.
tool: Edit ok
input
{
"file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"old_string": "set_option maxHeartbeats 800000 in\n/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the\n4/3 bracket \u2014 the D-074 dog-leg charges 1.5\u00b7IIMaj, and 1.5/(3n) =\n1/(2n) preserves the convexity slack] IIMaj\u2033(n) < 1/(3n) for n \u2265 20\n(the analytic version of D-057 \u00a73's \"max 2n\u00b7|B\u0303\u2084\u2033| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt_three {n : \u211d} (hn : 20 \u2264 n) :\n deriv (deriv IIMaj) n < 1 / (3 * n) := by",
"new_string": "set_option maxHeartbeats 1600000 in\n/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the\n4/3 bracket \u2014 the D-074 dog-leg charges 1.5\u00b7IIMaj, and 1.5/(3n) =\n1/(2n) preserves the convexity slack] IIMaj\u2033(n) < 1/(3n) for n \u2265 20\n(the analytic version of D-057 \u00a73's \"max 2n\u00b7|B\u0303\u2084\u2033| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt_three {n : \u211d} (hn : 20 \u2264 n) :\n deriv (deriv IIMaj) n < 1 / (3 * n) := by"
}
result 2026-08-26 11:33:41Z → 2026-08-26 11:33:41Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"oldString": "set_option maxHeartbeats 800000 in\n/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the\n4/3 bracket \u2014 the D-074 dog-leg charges 1.5\u00b7IIMaj, and 1.5/(3n) =\n1/(2n) preserves the convexity slack] IIMaj\u2033(n) < 1/(3n) for n \u2265 20\n(the analytic version of D-057 \u00a73's \"max 2n\u00b7|B\u0303\u2084\u2033| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt_three {n : \u211d} (hn : 20 \u2264 n) :\n deriv (deriv IIMaj) n < 1 / (3 * n) := by",
"newString": "set_option maxHeartbeats 1600000 in\n/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the\n4/3 bracket \u2014 the D-074 dog-leg charges 1.5\u00b7IIMaj, and 1.5/(3n) =\n1/(2n) preserves the convexity slack] IIMaj\u2033(n) < 1/(3n) for n \u2265 20\n(the analytic version of D-057 \u00a73's \"max 2n\u00b7|B\u0303\u2084\u2033| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt_three {n : \u211d} (hn : 20 \u2264 n) :\n deriv (deriv IIMaj) n < 1 / (3 * n) := by",
"originalFile": "/-\nNguyenRH1/LiSkeleton.lean \u2014 formalization of paper draft.tex \u00a73.1\n(R-004 finite-height Li theorem + archimedean lower bound + margin\nconvexity mechanism).\n\nConventions follow zeta-23-lean's hypothesis-driven style (cf. Zeta23.Final):\nthe computational inputs (Platt\u2013Trudgian RH-to-height; finite Li\nverification) are named Prop hypotheses, exactly as Zeta23 treats hEF/hRvM.\n\nStatus (session 012): TIER (i) COMPLETE (session 011: sInfty_lower_bound,\nmarginTilde_convex, chain_rule_sqrt_shift). TIER (ii) STEP 1 COMPLETE\n(session 012): `lambda_pos_finite_height` is PROVED modulo its named\nhypotheses \u2014 the assembly is conditional only on `SfBoundProp` (the\nisolated analytic obligation, triaged in D-062), the computational\nperimeter (`RHUpTo`, `LiVerifiedUpTo`), and two elementary margin\nevaluations (hbase/hbase2, E-028/E-029 values; their interval-bound\ndischarge is tier (ii) step 2). No `sorry` remains in this file;\n`#print axioms` shows only the three standard axioms for every\ndeclaration here.\n\nArchive references: R-004, D-037, D-056, D-057, D-062, E-023, E-028, E-029.\n-/\nimport Mathlib\nimport Zeta23.Statement\nimport Zeta23.WeilEF.ZeroSummability\nimport Zeta23.Statement.SeamClosed\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Keiper\u2013Li coefficients -/\n\n/-- The paired (symmetrized) Li summand: \u00bd\u00b7mult\u00b7(f \u03c1 + f \u03c1\u0304),\nf \u03c1 = 1 \u2212 (1\u22121/\u03c1)\u207f. Manifestly real-valued (`liSummand_eq`), absolutely\nsummable (`liSummable`) \u2014 the correct Keiper\u2013Li summand.\n(Session-015 ii\u2032-1a, D-064 \u00a71: the plain unordered sum of f over the\nzeros is NOT absolutely summable for any n \u2265 1 \u2014 the summand is\n~ n/|\u03b3| for large |\u03b3| and \u03a3 mult/|\u03c1| = \u221e \u2014 so the previous direct\ndefinition evaluated to the junk value 0 and `LiVerifiedUpTo`/\n`SfBoundProp` were FALSE as encoded. The pairing is the classical\nBombieri\u2013Lagarias symmetric convention and restores the intended\nmeaning; summability is proved below.) -/\ndef liSummand (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n (zeroMult \u03c1 : \u2102) / 2 *\n ((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n) + (1 - (1 - 1 / ((starRingEnd \u2102) (\u03c1 : \u2102))) ^ n))\n\nlemma summand_conj (n : \u2115) (z : \u2102) :\n (1 : \u2102) - (1 - 1 / ((starRingEnd \u2102) z)) ^ n = (starRingEnd \u2102) ((1 - (1 - 1 / z) ^ n)) := by\n rw [map_sub, map_one, map_pow, map_sub, map_one, map_div\u2080, map_one]\n\nlemma liSummand_eq (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n liSummand n \u03c1 = (zeroMult \u03c1 : \u2102) * (((1 - (1 - 1 / (\u03c1 : \u2102)) ^ n).re) : \u2102) := by\n rw [liSummand, summand_conj, Complex.add_conj]\n push_cast\n ring\n\n/-- The Keiper\u2013Li coefficient \u03bb_n as the paired zero-side sum with\nmultiplicity (draft \u00a73.1; Zeta23's IsNontrivialZero/zeroMult\nconventions; D-064 \u00a71). Summability: `liSummable`. -/\ndef liCoeff (n : \u2115) : \u2102 := \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, liSummand n \u03c1\n\n/-! ### 1a. The geometric-sum estimate: |Re(1 \u2212 w\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2 (w = 1\u22121/z) -/\n\n/-- (1 + 1/(2n))\u207f \u2264 2 for n \u2265 1. Via (1+x)\u207f \u2264 exp(nx) and exp(1/2) \u2264 2. -/\nlemma pow_one_add_inv_two_mul_le (n : \u2115) (hn : 1 \u2264 n) :\n ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hbase : (1 : \u211d) + 1 / (2 * n) \u2264 Real.exp (1 / (2 * n)) := by\n have h := Real.add_one_le_exp (1 / (2 * (n : \u211d)))\n linarith\n have h1 : ((1 : \u211d) + 1 / (2 * n)) ^ n \u2264 Real.exp (1 / 2) := by\n calc ((1 : \u211d) + 1 / (2 * n)) ^ n\n \u2264 (Real.exp (1 / (2 * n))) ^ n := pow_le_pow_left\u2080 (by positivity) hbase n\n _ = Real.exp (\u2191n * (1 / (2 * n))) := by rw [Real.exp_nat_mul]\n _ = Real.exp (1 / 2) := by congr 1; field_simp\n have h2 : Real.exp (1 / 2 : \u211d) \u2264 2 := by\n have h3 : (1 : \u211d) / 2 \u2264 Real.log 2 := by\n have h := Real.log_two_gt_d9\n linarith\n calc Real.exp (1 / 2 : \u211d) \u2264 Real.exp (Real.log 2) := Real.exp_le_exp.mpr h3\n _ = 2 := Real.exp_log (by norm_num)\n exact h1.trans h2\n\n/-- Key estimate: for n \u2265 1, z with re z \u2208 [0,1], 2n \u2264 \u2016z\u2016:\n|Re(1 \u2212 (1\u22121/z)\u207f)| \u2264 2n\u00b2/\u2016z\u2016\u00b2. -/\nlemma re_li_summand_le {n : \u2115} (hn : 1 \u2264 n) {z : \u2102}\n (hzre0 : 0 \u2264 z.re) (hzre1 : z.re \u2264 1) (hz : 2 * n \u2264 \u2016z\u2016) :\n |(1 - (1 - 1 / z) ^ n).re| \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hz0 : z \u2260 0 := by\n intro h; rw [h, norm_zero] at hz; linarith\n have hzn : (0 : \u211d) < \u2016z\u2016 := norm_pos_iff.mpr hz0\n have hnsq : Complex.normSq z = \u2016z\u2016 ^ 2 := Complex.normSq_eq_norm_sq z\n set M : \u211d := 1 + 1 / (2 * (n : \u211d)) with hM\n have hM0 : (0 : \u211d) \u2264 1 / (2 * (n : \u211d)) := by positivity\n have hM1 : (1 : \u211d) \u2264 M := le_add_of_nonneg_right hM0\n set w : \u2102 := 1 - 1 / z with hw\n have hgeom : (w - 1) * \u2211 j \u2208 Finset.range n, w ^ j = w ^ n - 1 := mul_geom_sum w n\n have hw1 : w - 1 = -(1 / z) := by rw [hw]; ring\n have hf : (1 : \u2102) - w ^ n = (1 / z) * \u2211 j \u2208 Finset.range n, w ^ j := by\n have e : (1 : \u2102) - w ^ n = -(w ^ n - 1) := by ring\n rw [e, \u2190 hgeom, hw1]; ring\n set S : \u2102 := \u2211 j \u2208 Finset.range n, w ^ j\n have hwnorm : \u2016w\u2016 \u2264 1 + 1 / \u2016z\u2016 := by\n have e : w = 1 - z\u207b\u00b9 := by rw [hw, div_eq_mul_inv, one_mul]\n rw [e]\n calc \u2016(1 : \u2102) - z\u207b\u00b9\u2016 \u2264 \u2016(1 : \u2102)\u2016 + \u2016z\u207b\u00b9\u2016 := norm_sub_le _ _\n _ = 1 + 1 / \u2016z\u2016 := by rw [norm_one, norm_inv, inv_eq_one_div]\n have h1z : 1 / \u2016z\u2016 \u2264 1 / (2 * n) :=\n one_div_le_one_div_of_le (by positivity) (by exact_mod_cast hz)\n have hwmax : max 1 \u2016w\u2016 \u2264 M := by\n apply max_le hM1\n exact hwnorm.trans (by rw [hM]; linarith)\n have hSn : \u2016S - n\u2016 \u2264 n ^ 2 / \u2016z\u2016 := by\n have hSn1 : S - n = \u2211 j \u2208 Finset.range n, (w ^ j - 1) := by\n have e : (n : \u2102) = \u2211 j \u2208 Finset.range n, (1 : \u2102) := by\n simp [Finset.sum_const, Finset.card_range]\n rw [e, \u2190 Finset.sum_sub_distrib]\n rw [hSn1]\n have hbound : \u2200 j \u2208 Finset.range n,\n \u2016w ^ j - 1\u2016 \u2264 (1 / \u2016z\u2016) * (j * M ^ (n - 1)) := by\n intro j hj\n have hgeomj : (w - 1) * \u2211 i \u2208 Finset.range j, w ^ i = w ^ j - 1 := mul_geom_sum w j\n have h2 : w ^ j - 1 = -(1 / z) * \u2211 i \u2208 Finset.range j, w ^ i := by\n rw [\u2190 hgeomj, hw1]\n rw [h2, norm_mul, norm_neg, norm_div, norm_one]\n have hsum : \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016 \u2264 j * M ^ (n - 1) := by\n calc \u2016\u2211 i \u2208 Finset.range j, w ^ i\u2016\n \u2264 \u2211 i \u2208 Finset.range j, \u2016w ^ i\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 i \u2208 Finset.range j, M ^ (n - 1) := by\n apply Finset.sum_le_sum\n intro i hi\n rw [norm_pow]\n have hij : i < j := Finset.mem_range.mp hi\n have hjn : j \u2264 n := le_of_lt (Finset.mem_range.mp hj)\n have h1 : \u2016w\u2016 ^ i \u2264 M ^ i :=\n pow_le_pow_left\u2080 (norm_nonneg _)\n (le_trans (le_max_right 1 \u2016w\u2016) hwmax) i\n have h2 : M ^ i \u2264 M ^ (n - 1) := pow_le_pow_right\u2080 hM1 (by omega)\n exact h1.trans h2\n _ = j * M ^ (n - 1) := by\n rw [Finset.sum_const, Finset.card_range, nsmul_eq_mul]\n exact mul_le_mul_of_nonneg_left hsum (by positivity)\n calc \u2016\u2211 j \u2208 Finset.range n, (w ^ j - 1)\u2016\n \u2264 \u2211 j \u2208 Finset.range n, \u2016w ^ j - 1\u2016 := norm_sum_le _ _\n _ \u2264 \u2211 j \u2208 Finset.range n, (1 / \u2016z\u2016) * (j * M ^ (n - 1)) :=\n Finset.sum_le_sum hbound\n _ = ((1 / \u2016z\u2016) * M ^ (n - 1)) * \u2211 j \u2208 Finset.range n, (j : \u211d) := by\n symm\n rw [Finset.mul_sum]\n apply Finset.sum_congr rfl\n intro j _; ring\n _ \u2264 n ^ 2 / \u2016z\u2016 := by\n have hsumj : (\u2211 j \u2208 Finset.range n, (j : \u211d)) = (n : \u211d) * ((n : \u211d) - 1) / 2 := by\n have h6 := congrArg (Nat.cast : \u2115 \u2192 \u211d) (Finset.sum_range_id_mul_two n)\n simp only [Nat.cast_mul, Nat.cast_sub hn, Nat.cast_ofNat, Nat.cast_one] at h6\n have h7 : (\u2211 j \u2208 Finset.range n, (j : \u211d)) =\n ((\u2211 j \u2208 Finset.range n, j : \u2115) : \u211d) := (Nat.cast_sum _ _).symm\n rw [h7]\n linarith\n rw [hsumj]\n have hpow : M ^ (n - 1) \u2264 2 :=\n le_trans (pow_le_pow_right\u2080 hM1 (Nat.sub_le n 1))\n (pow_one_add_inv_two_mul_le n hn)\n have hb1 : (n : \u211d) * (n - 1) / 2 \u2264 n ^ 2 / 2 := by nlinarith [hn0]\n have hb2 : M ^ (n - 1) * (n * (n - 1) / 2) \u2264 2 * (n ^ 2 / 2) :=\n mul_le_mul_of_nonneg hpow hb1 (by positivity) (by positivity)\n have hb3 : ((1 : \u211d) / \u2016z\u2016) * (M ^ (n - 1) * (n * (n - 1) / 2))\n \u2264 (1 / \u2016z\u2016) * (2 * (n ^ 2 / 2)) :=\n mul_le_mul_of_nonneg_left hb2 (by positivity)\n calc (1 / \u2016z\u2016) * M ^ (n - 1) * (\u2191n * (\u2191n - 1) / 2)\n = (1 / \u2016z\u2016) * (M ^ (n - 1) * (\u2191n * (\u2191n - 1) / 2)) := by ring\n _ \u2264 (1 / \u2016z\u2016) * (2 * (\u2191n ^ 2 / 2)) := hb3\n _ = \u2191n ^ 2 / \u2016z\u2016 := by ring\n have hre1 : ((n : \u2102) * (1 / z)).re = n * z.re / \u2016z\u2016 ^ 2 := by\n have hinv : ((1 : \u2102) / z).re = z.re / \u2016z\u2016 ^ 2 := by\n rw [one_div, Complex.inv_re, hnsq]\n have e : ((n : \u2102) * (1 / z)).re = n * ((1 : \u2102) / z).re := by\n rw [Complex.mul_re]\n simp\n rw [e, hinv]\n ring\n have hfre : (1 - w ^ n).re = n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re := by\n have hd : (1 / z) * ((n : \u2102) + (S - n)) = (n : \u2102) * (1 / z) + (S - n) / z := by\n ring\n rw [hf]\n nth_rewrite 1 [show S = (n : \u2102) + (S - n) from by ring]\n rw [hd, Complex.add_re, hre1]\n rw [hfre]\n have hA : |n * z.re / \u2016z\u2016 ^ 2| \u2264 n / \u2016z\u2016 ^ 2 := by\n have e : |n * z.re / \u2016z\u2016 ^ 2| = n * |z.re| / \u2016z\u2016 ^ 2 := by\n rw [abs_div, abs_mul, abs_of_nonneg hn0.le,\n abs_of_nonneg (sq_nonneg \u2016z\u2016)]\n rw [e, div_le_iff\u2080 (by positivity)]\n have e2 : (n / \u2016z\u2016 ^ 2) * \u2016z\u2016 ^ 2 = n := by field_simp\n rw [e2]\n calc n * |z.re| \u2264 n * 1 :=\n mul_le_mul_of_nonneg_left (abs_le.mpr \u27e8by linarith, hzre1\u27e9) hn0.le\n _ = n := mul_one _\n have hB : |((S - n) / z).re| \u2264 n ^ 2 / \u2016z\u2016 ^ 2 := by\n have h1 : |((S - n) / z).re| \u2264 \u2016(S - n) / z\u2016 := Complex.abs_re_le_norm _\n have h2 : \u2016(S - n) / z\u2016 \u2264 (n ^ 2 / \u2016z\u2016) / \u2016z\u2016 := by\n rw [norm_div, div_le_iff\u2080 hzn]\n have e : ((n ^ 2 / \u2016z\u2016) / \u2016z\u2016) * \u2016z\u2016 = n ^ 2 / \u2016z\u2016 := by field_simp\n rw [e]\n exact hSn\n exact h1.trans (h2.trans (by rw [div_div, \u2190 pow_two]))\n have hnn : (n : \u211d) \u2264 n ^ 2 := by\n have h : (1 : \u211d) \u2264 n := by exact_mod_cast hn\n nlinarith\n calc |n * z.re / \u2016z\u2016 ^ 2 + ((S - n) / z).re|\n \u2264 n / \u2016z\u2016 ^ 2 + n ^ 2 / \u2016z\u2016 ^ 2 := (abs_add_le _ _).trans (add_le_add hA hB)\n _ = (n + n ^ 2) / \u2016z\u2016 ^ 2 := by ring\n _ \u2264 2 * n ^ 2 / \u2016z\u2016 ^ 2 := by\n rw [div_le_iff\u2080 (by positivity)]\n have e : (2 * n ^ 2 / \u2016z\u2016 ^ 2) * \u2016z\u2016 ^ 2 = 2 * n ^ 2 := by field_simp\n rw [e]\n linarith\n\n/-! ### 1b. The comparison 1 + \u2016\u03b3_\u03c1\u2016\u00b2 \u2264 (9/4)\u2016\u03c1\u2016\u00b2 and summability -/\n\n/-- For re z \u2208 [0,1] and 2n \u2264 \u2016z\u2016 (n \u2265 1): 1 + \u2016\u03b3_z\u2016\u00b2 \u2264 (9/4)\u00b7\u2016z\u2016\u00b2. -/\nlemma normSq_gammaOf_le_mul_norm_sq {n : \u2115} (hn : 1 \u2264 n) {z : \u2102}\n (hzre0 : 0 \u2264 z.re) (hzre1 : z.re \u2264 1) (hz : 2 * n \u2264 \u2016z\u2016) :\n 1 + Complex.normSq (gammaOf z) \u2264 9 / 4 * \u2016z\u2016 ^ 2 := by\n have hn0 : (0 : \u211d) < n := by exact_mod_cast hn\n have hz2 : \u2016z\u2016 ^ 2 = z.re ^ 2 + z.im ^ 2 := by\n rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n ring\n have hz4 : 4 * n ^ 2 \u2264 \u2016z\u2016 ^ 2 := by\n have h := pow_le_pow_left\u2080 (by positivity : (0:\u211d) \u2264 2 * n) hz 2\n nlinarith [h]\n have hre2 : z.re ^ 2 \u2264 1 := by nlinarith [hzre0, hzre1]\n have hn1 : (1 : \u211d) \u2264 n := by exact_mod_cast hn\n have hn4 : (4 : \u211d) \u2264 4 * (n : \u211d) ^ 2 := by\n have h := pow_le_pow_left\u2080 (show (0 : \u211d) \u2264 1 by norm_num) hn1 2\n nlinarith [h]\n have him : 1 \u2264 z.im ^ 2 := by nlinarith [hz2, hz4, hre2, hn4]\n have hgam : Complex.normSq (gammaOf z) = z.im ^ 2 + (1 / 2 - z.re) ^ 2 := by\n rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n ring\n rw [hgam, hz2]\n nlinarith [hzre0, hzre1, him, sq_nonneg (1 / 2 - z.re), sq_nonneg z.re]\n\n/-- Norm of the paired summand: mult\u00b7|Re f(\u03c1)|. -/\nlemma liSummand_norm (n : \u2115) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) :\n \u2016liSummand n \u03c1\u2016 = (zeroMult \u03c1 : \u211d) * |(1 - (1 - 1 / (\u03c1 : \u2102)) ^ n).re| := by\n rw [liSummand_eq n \u03c1, norm_mul, RCLike.norm_natCast]\n congr 1\n exact RCLike.norm_ofReal _\n\n/-- The main bound: for 2n \u2264 \u2016\u03c1\u2016, \u2016liSummand n \u03c1\u2016 \u2264 (9/2)n\u00b2\u00b7mult/(1+\u2016\u03b3_\u03c1\u2016\u00b2). -/\nlemma liSummand_norm_le {n : \u2115} (hn : 1 \u2264 n) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1})\n (h\u03c1 : (2 : \u211d) * n \u2264 \u2016(\u03c1 : \u2102)\u2016) :\n \u2016liSummand n \u03c1\u2016 \u2264\n (9 / 2) * n ^ 2 * (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n have hz := \u03c1.2\n have hre0 : 0 \u2264 (\u03c1 : \u2102).re := hz.2.1.le\n have hre1 : (\u03c1 : \u2102).re \u2264 1 := hz.2.2.le\n have hcore := re_li_summand_le hn hre0 hre1 h\u03c1\n have hcomp := normSq_gammaOf_le_mul_norm_sq hn hre0 hre1 h\u03c1\n have hnpos : (0 : \u211d) < n := by exact_mod_cast hn\n have hz0 : (0 : \u211d) < \u2016(\u03c1 : \u2102)\u2016 := lt_of_lt_of_le (by positivity) h\u03c1\n have hz0' : \u2016(\u03c1 : \u2102)\u2016 \u2260 0 := ne_of_gt hz0\n have hg0 : (0 : \u211d) < 1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) := by\n have h := Complex.normSq_nonneg (gammaOf (\u03c1 : \u2102))\n linarith\n have key : (zeroMult \u03c1 : \u211d) * (2 * n ^ 2 / \u2016(\u03c1 : \u2102)\u2016 ^ 2)\n \u2264 (9 / 2) * n ^ 2 * (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf (\u03c1 : \u2102))) := by\n rw [le_div_iff\u2080 hg0]\n have hbound : (zeroMult \u03c1 : \u211d) * (2 * n ^ 2 / \u2016(\u03c1 : \u2102)\u2016 ^ 2) *\n (1 + Complex.normSq (gammaOf (\u03c1 : \u2102)))\n \u2264 (zeroMult \u03c1 : \u211d) * (2 * n ^ 2 / \u2016(\u03c1 : \u2102)\u2016 ^ 2) * ((9 / 4) * \u2016(\u03c1 : \u2102)\u2016 ^ 2) :=\n mul_le_mul_of_nonneg_left hcomp (by positivity)\n have heq : (zeroMult \u03c1 : \u211d) * (2 * n ^ 2 / \u2016(\u03c1 : \u2102)\u2016 ^ 2) * ((9 / 4) * \u2016(\u03c1 : \u2102)\u2016 ^ 2)\n = (9 / 2) * n ^ 2 * (zeroMult \u03c1 : \u211d) := by\n field_simp\n ring\n exact hbound.trans (le_of_eq heq)\n rw [liSummand_norm]\n exact (mul_le_mul_of_nonneg_left hcore (Nat.cast_nonneg _)).trans key\n\n/-- The paired Li summand is absolutely summable over the nontrivial zeros.\nUses Zeta23's `WeilEF.zero_sum_inv_sq` (\u03a3 mult/(1+\u2016\u03b3_\u03c1\u2016\u00b2) < \u221e, proved) via\nthe tail bound of `liSummand_norm_le`; the ball {\u2016\u03c1\u2016 < 2n} contributes a\nfinite set (Mathlib `IsCompact.inter_riemannZetaZeros_finite`). -/\ntheorem liSummable (n : \u2115) : Summable (liSummand n) := by\n rcases Nat.eq_zero_or_pos n with h0 | hn\n \u00b7 subst h0\n have h : liSummand 0 = fun _ => (0 : \u2102) := by\n funext \u03c1\n simp [liSummand]\n rw [h]\n exact summable_zero\n \u00b7 have hbase : Summable (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n (9 / 2) * (n : \u211d) ^ 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf \u03c1)))) := by\n have h := (WeilEF.zero_sum_inv_sq zetaSeam).mul_left ((9 / 2) * (n : \u211d) ^ 2)\n exact h\n set D : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} \u2192 \u211d := fun \u03c1 =>\n if (2 : \u211d) * n \u2264 \u2016(\u03c1 : \u2102)\u2016 then\n (9 / 2) * n ^ 2 * (zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf \u03c1))\n else \u2016liSummand n \u03c1\u2016 with hDdef\n have hfin : {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} | \u00ac ((2 : \u211d) * n \u2264 \u2016(\u03c1 : \u2102)\u2016)}.Finite := by\n have hcomp : IsCompact (Metric.closedBall (0 : \u2102) (2 * n)) :=\n isCompact_closedBall _ _\n have hzeros : (Metric.closedBall (0 : \u2102) (2 * n)) \u2229 {\u03c1 : \u2102 | IsNontrivialZero \u03c1}\n \u2286 (Metric.closedBall (0 : \u2102) (2 * n)) \u2229 riemannZetaZeros := by\n intro z hz\n exact \u27e8hz.1, hz.2.1\u27e9\n have hfin2 := (hcomp.inter_riemannZetaZeros_finite).subset hzeros\n have himg : (Subtype.val '' {\u03c1 : {\u03c1 // IsNontrivialZero \u03c1} |\n \u00ac ((2 : \u211d) * n \u2264 \u2016(\u03c1 : \u2102)\u2016)}).Finite := by\n apply hfin2.subset\n rintro z \u27e8\u03c1, h\u03c1, rfl\u27e9\n refine \u27e8?_, \u03c1.2\u27e9\n simp only [Metric.mem_closedBall, dist_zero_right]\n exact le_of_lt (lt_of_not_ge h\u03c1)\n exact Set.Finite.of_finite_image himg (Subtype.val_injective.injOn)\n have hE : Summable (fun \u03c1 : {\u03c1 // IsNontrivialZero \u03c1} =>\n D \u03c1 - (9 / 2) * (n : \u211d) ^ 2 * ((zeroMult \u03c1 : \u211d) /\n (1 + Complex.normSq (gammaOf \u03c1)))) := by\n apply summable_of_hasFiniteSupport\n apply hfin.subset\n intro \u03c1 h\u03c1\n simp only [Function.mem_support, ne_eq] at h\u03c1\n by_contra hball\n apply h\u03c1\n have hball' : (2 : \u211d) * n \u2264 \u2016(\u03c1 : \u2102)\u2016 := not_not.mp hball\n simp only [D, if_pos hball']\n ring\n have hD : Summable D := by\n have hsum := hbase.add hE\n have heq : (fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n (9 / 2) * (n : \u211d) ^ 2 * ((zeroMult \u03c1 : \u211d) / (1 + Complex.normSq (gammaOf \u03c1))) +\n (D \u03c1 - (9 / 2) * (n : \u211d) ^ 2 * ((zeroMult \u03c1 : \u211d) /\n (1 + Complex.normSq (gammaOf \u03c1))))) = D := by\n funext \u03c1\n ring\n rw [heq] at hsum\n exact hsum\n refine Summable.of_norm_bounded hD (fun \u03c1 => ?_)\n by_cases h\u03c1 : (2 : \u211d) * n \u2264 \u2016(\u03c1 : \u2102)\u2016\n \u00b7 simp only [D, if_pos h\u03c1]\n exact liSummand_norm_le hn \u03c1 h\u03c1\n \u00b7 simp only [D, if_neg h\u03c1, le_refl]\n\n/-- \"RH verified to height T\u2080\": every nontrivial zero with |Im \u03c1| \u2264 T\u2080 is\non the critical line. Platt\u2013Trudgian 2021 (interval arithmetic) is the\nT\u2080 = 3\u00d710\u00b9\u00b2 instance; treated here as a hypothesis, mirroring Zeta23's\nliterature-hypothesis style. -/\ndef RHUpTo (T\u2080 : \u211d) : Prop :=\n \u2200 \u03c1 : \u2102, IsNontrivialZero \u03c1 \u2192 |\u03c1.im| \u2264 T\u2080 \u2192 \u03c1.re = 1 / 2\n\n/-- \"Li coefficients verified positive up to N\" (computational input:\nthis project to N = 3000 (E-011/E-015, two independent methods);\nMisguich\u2013Voros to N = 5\u00d710\u2075). \u03bb_n is real (conjugate symmetry of the\nzero set); the skeleton states positivity of the real part. -/\ndef LiVerifiedUpTo (N : \u2115) : Prop :=\n \u2200 n : \u2115, 1 \u2264 n \u2192 n \u2264 N \u2192 0 < (liCoeff n).re\n\n/- [PROVED session 012, tier (ii) step 1 \u2014 assembly modulo the named\nanalytic hypothesis] R-004, the finite-height Li theorem (draft Thm 3.1).\nThe full statement and proof are at the END of this file (\u00a74), after the\nmargin machinery they depend on: `lambda_pos_finite_height` there is\nproved from `SfBoundProp` (the single named analytic hypothesis, D-062\ntriage) + the computational perimeter (Platt\u2013Trudgian `RHUpTo`,\n`LiVerifiedUpTo`) + two elementary margin evaluations. -/\n\n/-! ## 2. The archimedean lower bound (D-037 Step 1) -/\n\n/-- a\u2081 = (log 4\u03c0 + \u03b3)/2, the j = 1 Lagarias coefficient. -/\ndef lagariasA1 : \u211d := (Real.log (4 * Real.pi) + Real.eulerMascheroniConstant) / 2\n\n/-- S_\u221e(n) in the exact odd-m identity form (D-037):\nS_\u221e(n) = (1\u2212a\u2081)n \u2212 1 + \u03a3_{m \u2265 3, odd} [(1\u22121/m)\u207f \u2212 1 + n/m].\n(Same tsum-summability honesty note as liCoeff.) -/\ndef SInfty (n : \u2115) : \u211d :=\n (1 - lagariasA1) * n - 1 +\n tsum fun m : {m : \u2115 // Odd m \u2227 3 \u2264 m} =>\n ((1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d))\n\n/-- C\u2081 = (\u03b3 \u2212 1 \u2212 log 2\u03c0)/2 (D-037). -/\ndef lagariasC1 : \u211d :=\n (Real.eulerMascheroniConstant - 1 - Real.log (2 * Real.pi)) / 2\n\n/-- The explicit archimedean lower bound S(n) = \u00bdn log n + (C\u2081\u2212\u03b3/2)n \u2212 4\n(D-037 (3.1)); named so the assembly can refer to it. -/\ndef sInftyLower (n : \u211d) : \u211d :=\n (1 / 2) * n * Real.log n + (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4\n\n/-- [PROVED session 011] h\u207a(m) \u2265 0 for m \u2265 1: first-order Bernoulli,\n(1\u22121/m)\u207f \u2265 1 \u2212 n/m. (D-037 \u00a73, \"h\u207a \u2265 max(0, n/m \u2212 1)\".) -/\ntheorem bern_term_nonneg (n : \u2115) (m : \u2115) (hm : 1 \u2264 m) :\n 0 \u2264 (1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / m := by\n have hm0 : (m : \u211d) \u2260 0 := by positivity\n have h1 : (1 : \u211d) + n * (-1 / m) \u2264 (1 + -1 / (m : \u211d)) ^ n := by\n apply one_add_mul_le_pow\n have h3 : (0 : \u211d) \u2264 1 / (m : \u211d) := by positivity\n have h4 : (1 : \u211d) / m \u2264 1 := by\n rw [div_le_one (by positivity)]; exact_mod_cast hm\n rw [neg_div]\n linarith\n have h2 : (1 : \u211d) - n / m \u2264 (1 - 1 / m) ^ n := by\n have : (1 : \u211d) + n * (-1 / m) = 1 - n / m := by field_simp; ring\n rwa [this, show (1 : \u211d) + -1 / m = 1 - 1 / m by ring] at h1\n linarith\n\n/-- [PROVED session 011] h\u207a(m) \u2264 n(n\u22121)/(2m\u00b2) for m \u2265 1: geometric\nfactorization 1 \u2212 (1\u2212x)\u207f = x\u00b7\u03a3_{j<n} (1\u2212x)\u02b2 plus Bernoulli per term.\n(D-037 \u00a73's \"terms ~ C(n,2)/m\u00b2\"; the summability input.) -/\ntheorem bern_term_upper (n : \u2115) (m : \u2115) (hm : 1 \u2264 m) :\n (1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / m \u2264 (n : \u211d) * (n - 1) / (2 * m ^ 2) := by\n have hm0 : (m : \u211d) \u2260 0 := by positivity\n set x := (1 : \u211d) / m with hxdef\n have hx1 : x \u2264 1 := by\n rw [hxdef, div_le_one (by positivity)]; exact_mod_cast hm\n have hx0 : 0 \u2264 x := by positivity\n have hterm : \u2200 j : \u2115, 1 - j * x \u2264 (1 - x) ^ j := by\n intro j\n have := one_add_mul_le_pow (a := -x) (by linarith : (-2 : \u211d) \u2264 -x) j\n rwa [show (1 : \u211d) + j * (-x) = 1 - j * x by ring,\n show (1 : \u211d) + -x = 1 - x by ring] at this\n have hsum : \u2211 j \u2208 Finset.range n, (j : \u211d) = (n : \u211d) * (n - 1) / 2 := by\n have h := Finset.sum_range_id_mul_two n\n have hcast : (((\u2211 i \u2208 Finset.range n, i) * 2 : \u2115) : \u211d) = ((n * (n - 1) : \u2115) : \u211d) := by\n exact_mod_cast h\n rcases Nat.eq_zero_or_pos n with rfl | hnpos\n \u00b7 simp\n \u00b7 push_cast at hcast\n rw [Nat.cast_sub hnpos] at hcast\n push_cast at hcast\n linarith\n have hgeom : (1 - (1 - x) ^ n) = x * \u2211 j \u2208 Finset.range n, (1 - x) ^ j := by\n have h := geom_sum_mul (1 - x) n\n have hx1' : (1 - x) - 1 = -x := by ring\n rw [hx1'] at h\n linarith\n have hmain : (1 - x) ^ n - 1 + (n : \u211d) * x \u2264 (n : \u211d) * (n - 1) / 2 * x ^ 2 := by\n have h4 : (n : \u211d) * x - (n * (n - 1) / 2) * x ^ 2 \u2264 1 - (1 - x) ^ n := by\n rw [hgeom]\n have h5 : (n : \u211d) - x * ((n : \u211d) * (n - 1) / 2) \u2264\n \u2211 j \u2208 Finset.range n, (1 - x) ^ j := by\n have h6 : \u2211 j \u2208 Finset.range n, (1 - (j : \u211d) * x) =\n (n : \u211d) - x * \u2211 j \u2208 Finset.range n, (j : \u211d) := by\n have e1 : \u2211 j \u2208 Finset.range n, (1 - (j : \u211d) * x) =\n (\u2211 j \u2208 Finset.range n, (1 : \u211d)) - \u2211 j \u2208 Finset.range n, (j : \u211d) * x :=\n Finset.sum_sub_distrib (f := fun j : \u2115 => (1 : \u211d)) (g := fun j : \u2115 => (j : \u211d) * x)\n have e2 : \u2211 j \u2208 Finset.range n, (1 : \u211d) = (n : \u211d) := by simp\n have e3 : \u2211 j \u2208 Finset.range n, (j : \u211d) * x =\n x * \u2211 j \u2208 Finset.range n, (j : \u211d) := by\n rw [Finset.mul_sum]\n refine Finset.sum_congr rfl fun j _ => ?_\n ring\n rw [e1, e2, e3]\n rw [hsum] at h6\n rw [\u2190 h6]\n exact Finset.sum_le_sum fun j _ => hterm j\n calc (n : \u211d) * x - (n * (n - 1) / 2) * x ^ 2\n = x * ((n : \u211d) - x * (n * (n - 1) / 2)) := by ring\n _ \u2264 x * \u2211 j \u2208 Finset.range n, (1 - x) ^ j :=\n mul_le_mul_of_nonneg_left h5 hx0\n linarith\n have hx2 : x ^ 2 = 1 / m ^ 2 := by rw [hxdef]; ring\n have hdiv : (n : \u211d) / m = n * x := by rw [hxdef]; ring\n rw [hdiv]\n have h7 : (1 - 1 / (m : \u211d)) ^ n = (1 - x) ^ n := by rw [hxdef]\n rw [h7]\n calc (1 - x) ^ n - 1 + (n : \u211d) * x\n \u2264 (n : \u211d) * (n - 1) / 2 * x ^ 2 := hmain\n _ = (n : \u211d) * (n - 1) / (2 * m ^ 2) := by rw [hx2]; ring\n\n/-- [PROVED session 011] Summability of the odd-m S_\u221e series (the honesty\nnote on `SInfty`'s `tsum` discharged): terms are nonneg and O(n\u00b2/m\u00b2). -/\ntheorem sInf_series_summable (n : \u2115) :\n Summable fun m : {m : \u2115 // Odd m \u2227 3 \u2264 m} =>\n ((1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d)) := by\n refine Summable.of_nonneg_of_le\n (g := fun m : {m : \u2115 // Odd m \u2227 3 \u2264 m} =>\n (1 - 1 / ((m : \u2115) : \u211d)) ^ n - 1 + (n : \u211d) / ((m : \u2115) : \u211d))\n (f := fun m : {m : \u2115 // Odd m \u2227 3 \u2264 m} =>\n ((n : \u211d) * ((n : \u211d) - 1) / 2) * (1 / ((m : \u2115) : \u211d) ^ 2)) ?_ ?_ ?_\n \u00b7 intro m\n exact bern_term_nonneg n m.1 (Nat.le_trans (by norm_num) m.2.2)\n \u00b7 intro m\n refine le_trans (bern_term_upper n m.1 (Nat.le_trans (by norm_num) m.2.2)) (le_of_eq ?_)\n ring\n \u00b7 exact ((Real.summable_one_div_nat_pow.mpr (by norm_num : 1 < 2)).mul_left\n ((n : \u211d) * ((n : \u211d) - 1) / 2)).comp_injective Subtype.coe_injective\n\n/-- [PROVED session 011] H1: `log M + \u03b3 \u2264 H_M` (from Mathlib's strictly\ndecreasing `eulerMascheroniSeq'`). -/\ntheorem harmonic_lower (M : \u2115) (hM : 1 \u2264 M) :\n Real.log M + Real.eulerMascheroniConstant \u2264 (harmonic M : \u211d) := by\n have h := Real.eulerMascheroniConstant_lt_eulerMascheroniSeq' M\n rw [Real.eulerMascheroniSeq', if_neg (by omega : M \u2260 0)] at h\n linarith\n\n/-- [PROVED session 011] H2: `H_M \u2264 log (M+1) + \u03b3` (from Mathlib's strictly\nincreasing `eulerMascheroniSeq`). -/\ntheorem harmonic_upper (M : \u2115) :\n (harmonic M : \u211d) \u2264 Real.log ((M : \u211d) + 1) + Real.eulerMascheroniConstant := by\n have h := Real.eulerMascheroniSeq_lt_eulerMascheroniConstant M\n rw [Real.eulerMascheroniSeq] at h\n linarith\n\n/-- [PROVED session 011] h\u207a(m) \u2265 n/m \u2212 1 for m \u2265 1 (the power term is\nnonneg). -/\ntheorem bern_term_lower (n : \u2115) (m : \u2115) (hm : 1 \u2264 m) :\n (n : \u211d) / m - 1 \u2264 (1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / m := by\n have hm1 : (1 : \u211d) \u2264 m := by exact_mod_cast hm\n have h4 : (1 : \u211d) / m \u2264 1 := by rw [div_le_one (by positivity)]; exact hm1\n have hpos : (0 : \u211d) \u2264 1 - 1 / (m : \u211d) := by linarith\n have h3 : (0 : \u211d) \u2264 (1 - 1 / (m : \u211d)) ^ n := pow_nonneg hpos n\n linarith\n\n/-- The odd reciprocals sum `\u03a3_{k=1}^{K} 1/(2k+1)`. -/\nprivate def oddHarm (K : \u2115) : \u211d := \u2211 k \u2208 Finset.Icc 1 K, (1 : \u211d) / (2 * k + 1)\n\n/-- Embedding `k \u21a6 2k+1` into the odd-\u2265-3 subtype (junk value at k = 0,\nnever used: only applied on `Icc 1 K`). -/\nprivate def oddEmb : \u2115 \u2192 {m : \u2115 // Odd m \u2227 3 \u2264 m} := fun k =>\n if hk : 1 \u2264 k then \u27e82 * k + 1, \u27e8k, rfl\u27e9, by omega\u27e9 else \u27e83, \u27e81, rfl\u27e9, le_refl 3\u27e9\n\n/-- [PROVED session 011] Partial-sum comparison (D-037 \u00a73 truncation):\n`n\u00b7oddHarm K \u2212 K \u2264 \u03a3'_{m odd \u2265 3} h\u207a(m)` for every K \u2014 Bernoulli\ntermwise, nonneg tail dropped. -/\ntheorem sInf_partial_lower (n K : \u2115) :\n (n : \u211d) * oddHarm K - (K : \u211d) \u2264\n \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m},\n ((1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d)) := by\n calc (n : \u211d) * oddHarm K - (K : \u211d)\n = \u2211 k \u2208 Finset.Icc 1 K, ((n : \u211d) / (2 * k + 1) - 1) := by\n unfold oddHarm\n rw [Finset.mul_sum, Finset.sum_sub_distrib]\n congr 1\n \u00b7 exact Finset.sum_congr rfl (fun k _ => mul_one_div _ _)\n \u00b7 simp [Finset.sum_const, Nat.card_Icc, nsmul_eq_mul]\n _ \u2264 \u2211 k \u2208 Finset.Icc 1 K,\n ((1 - 1 / (2 * (k : \u211d) + 1)) ^ n - 1 + (n : \u211d) / (2 * (k : \u211d) + 1)) := by\n apply Finset.sum_le_sum\n intro k hk\n have h := bern_term_lower n (2 * k + 1) (by omega)\n have hc : ((2 * k + 1 : \u2115) : \u211d) = 2 * (k : \u211d) + 1 := by push_cast; ring\n rwa [hc] at h\n _ \u2264 \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m},\n ((1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d)) := by\n have hinj : \u2200 x \u2208 Finset.Icc 1 K, \u2200 y \u2208 Finset.Icc 1 K,\n oddEmb x = oddEmb y \u2192 x = y := by\n intro x hx y hy h\n have hx1 : 1 \u2264 x := (Finset.mem_Icc.mp hx).1\n have hy1 : 1 \u2264 y := (Finset.mem_Icc.mp hy).1\n simp only [oddEmb, dif_pos hx1, dif_pos hy1, Subtype.mk.injEq] at h\n omega\n have hconv : \u2211 k \u2208 Finset.Icc 1 K,\n ((1 - 1 / (2 * (k : \u211d) + 1)) ^ n - 1 + (n : \u211d) / (2 * (k : \u211d) + 1)) =\n \u2211 k \u2208 Finset.Icc 1 K,\n ((1 - 1 / ((oddEmb k : \u2115) : \u211d)) ^ n - 1 +\n (n : \u211d) / ((oddEmb k : \u2115) : \u211d)) := by\n apply Finset.sum_congr rfl\n intro k hk\n have hk1 : 1 \u2264 k := (Finset.mem_Icc.mp hk).1\n have hc : ((2 * k + 1 : \u2115) : \u211d) = 2 * (k : \u211d) + 1 := by push_cast; ring\n simp only [oddEmb, dif_pos hk1]\n show ((1 - 1 / (2 * (k : \u211d) + 1)) ^ n - 1 + (n : \u211d) / (2 * (k : \u211d) + 1)) =\n (1 - 1 / ((2 * k + 1 : \u2115) : \u211d)) ^ n - 1 + (n : \u211d) / ((2 * k + 1 : \u2115) : \u211d)\n rw [hc]\n rw [hconv]\n have hsi := Finset.sum_image (s := Finset.Icc 1 K) (g := oddEmb)\n (f := fun m : {m : \u2115 // Odd m \u2227 3 \u2264 m} =>\n (1 - 1 / ((m : \u2115) : \u211d)) ^ n - 1 + (n : \u211d) / ((m : \u2115) : \u211d))\n (show Set.InjOn oddEmb \u2191(Finset.Icc 1 K) from hinj)\n rw [\u2190 hsi]\n exact Summable.sum_le_tsum _\n (fun i _ => bern_term_nonneg n i.1 (Nat.le_trans (by norm_num) i.2.2))\n (sInf_series_summable n)\n\n/-- [PROVED session 011] Odd-harmonic identity (D-037 \u00a73):\n`\u03a3_{k=1}^{K} 1/(2k+1) = H_{2K+1} \u2212 \u00bdH_K \u2212 1`, by induction. -/\ntheorem oddHarm_eq (K : \u2115) :\n oddHarm K = (harmonic (2 * K + 1) : \u211d) - (harmonic K : \u211d) / 2 - 1 := by\n induction K with\n | zero => simp [oddHarm, harmonic_succ]\n | succ K ih =>\n have h1 : (harmonic (2 * (K + 1) + 1) : \u211d) =\n (harmonic (2 * K + 1) : \u211d) + 1 / (2 * (K : \u211d) + 2) + 1 / (2 * (K : \u211d) + 3) := by\n have hs : 2 * (K + 1) + 1 = (2 * K + 1) + 1 + 1 := by ring\n rw [hs, harmonic_succ, harmonic_succ]\n push_cast\n ring\n have h2 : (harmonic (K + 1) : \u211d) = (harmonic K : \u211d) + 1 / ((K : \u211d) + 1) := by\n rw [harmonic_succ]\n push_cast\n ring\n have e3 : (1 : \u211d) / (2 * (K : \u211d) + 2) = (1 / ((K : \u211d) + 1)) / 2 := by\n have h4 : (2 : \u211d) * (K : \u211d) + 2 = 2 * ((K : \u211d) + 1) := by ring\n rw [h4, one_div, mul_inv, one_div, div_eq_mul_inv]\n ring\n show (\u2211 k \u2208 Finset.Icc 1 (K + 1), (1 : \u211d) / (2 * k + 1)) = _\n rw [Finset.sum_Icc_succ_top (by omega : 1 \u2264 K + 1) (fun k => (1 : \u211d) / (2 * k + 1)),\n show (\u2211 k \u2208 Finset.Icc 1 K, (1 : \u211d) / (2 * k + 1)) = oddHarm K from rfl, ih, h1, h2]\n push_cast\n rw [e3]\n ring\n\n/-- [PROVED session 011] oddHarm lower bound (D-037 \u00a73): from H1/H2,\n`oddHarm K \u2265 log(2K+1) \u2212 \u00bdlog(K+1) + \u03b3/2 \u2212 1`. -/\ntheorem oddHarm_lower (K : \u2115) :\n Real.log (2 * (K : \u211d) + 1) - Real.log ((K : \u211d) + 1) / 2 +\n Real.eulerMascheroniConstant / 2 - 1 \u2264 oddHarm K := by\n rw [oddHarm_eq K]\n have hbl := harmonic_lower (2 * K + 1) (by omega)\n have hbu := harmonic_upper K\n have hc : ((2 * K + 1 : \u2115) : \u211d) = 2 * (K : \u211d) + 1 := by push_cast; ring\n rw [hc] at hbl\n linarith\n\n/-- [PROVED session 011] Archimedean lower bound (draft \u00a73.1 Step 1,\nD-037 \u00a73): S_\u221e(n) \u2265 \u00bd n log n + (C\u2081 \u2212 \u03b3/2) n \u2212 4 for n \u2265 20.\nProof: Bernoulli truncation at K \u2248 n/2 + the two \u03b3-shifted harmonic\nbounds; the \u03b3/log 2/log \u03c0 pieces cancel EXACTLY (parity algebra), and\nthe residual logarithmic defect is \u2264 n/(n\u22121) (even) resp. \u2264 1/2 (odd),\nabsorbed by the \u22124 constant. Machine-validated against exact values for\n20 \u2264 n \u2264 5000 (E-021/E-023 V1, min slack 9.52). -/\ntheorem sInfty_lower_bound (n : \u2115) (hn : 20 \u2264 n) :\n sInftyLower n \u2264 SInfty n := by\n show (1 / 2) * (n : \u211d) * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n SInfty n\n -- reduction to a K-specialized real inequality\n have hmain : \u2200 K : \u2115,\n (1 / 2) * (n : \u211d) * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n (1 - lagariasA1) * (n : \u211d) - 1 +\n ((n : \u211d) * (Real.log (2 * (K : \u211d) + 1) - Real.log ((K : \u211d) + 1) / 2 +\n Real.eulerMascheroniConstant / 2 - 1) - (K : \u211d)) \u2192\n (1 / 2) * (n : \u211d) * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n SInfty n := by\n intro K hK\n have h1 := sInf_partial_lower n K\n have h2 := oddHarm_lower K\n have h3 : (n : \u211d) * (Real.log (2 * (K : \u211d) + 1) - Real.log ((K : \u211d) + 1) / 2 +\n Real.eulerMascheroniConstant / 2 - 1) \u2264 (n : \u211d) * oddHarm K :=\n mul_le_mul_of_nonneg_left h2 (by positivity)\n have h4 : SInfty n = (1 - lagariasA1) * (n : \u211d) - 1 +\n \u2211' m : {m : \u2115 // Odd m \u2227 3 \u2264 m},\n ((1 - 1 / (m : \u211d)) ^ n - 1 + (n : \u211d) / (m : \u211d)) := rfl\n rw [h4]\n linarith [h1, h3]\n -- logarithm identities for the \u03c0-factors\n have h4pi : Real.log (4 * Real.pi) = 2 * Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num : (4 : \u211d) \u2260 0) Real.pi_ne_zero]\n have e : Real.log (4 : \u211d) = 2 * Real.log 2 := by\n rw [show (4 : \u211d) = 2 ^ 2 by norm_num, Real.log_pow]\n norm_num\n rw [e]\n have h2pi : Real.log (2 * Real.pi) = Real.log 2 + Real.log Real.pi := by\n rw [Real.log_mul (by norm_num : (2 : \u211d) \u2260 0) Real.pi_ne_zero]\n rcases Nat.even_or_odd n with \u27e8q, rfl\u27e9 | \u27e8q, rfl\u27e9\n \u00b7 -- n = q + q, K = q \u2212 1: defect \u2264 n/(n\u22121) \u2264 2 < 4\n have hq10 : 10 \u2264 q := by omega\n have hQ : (10 : \u211d) \u2264 (q : \u211d) := by exact_mod_cast hq10\n refine hmain (q - 1) ?_\n have hN : ((q + q : \u2115) : \u211d) = 2 * (q : \u211d) := by push_cast; ring\n have hK1 : 2 * ((q - 1 : \u2115) : \u211d) + 1 = 2 * (q : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 q), Nat.cast_one]; ring\n have hK2 : ((q - 1 : \u2115) : \u211d) + 1 = (q : \u211d) := by\n rw [Nat.cast_sub (by omega : 1 \u2264 q), Nat.cast_one]; ring\n have hK3 : ((q - 1 : \u2115) : \u211d) = (q : \u211d) - 1 := by\n rw [Nat.cast_sub (by omega : 1 \u2264 q), Nat.cast_one]\n have hlogq : Real.log (q : \u211d) = Real.log (2 * (q : \u211d)) - Real.log 2 := by\n have h := Real.log_mul (by norm_num : (2 : \u211d) \u2260 0)\n (ne_of_gt (by linarith : (0 : \u211d) < (q : \u211d)))\n linarith [h]\n rw [hN, hK1, hK2, hK3, hlogq]\n unfold lagariasA1 lagariasC1\n rw [h4pi, h2pi]\n have hpos : (0 : \u211d) < 2 * (q : \u211d) - 1 := by linarith\n have hlogb1 : Real.log (2 * (q : \u211d)) - Real.log (2 * (q : \u211d) - 1) \u2264\n 1 / (2 * (q : \u211d) - 1) := by\n have h1 := Real.log_le_sub_one_of_pos\n (x := (2 * (q : \u211d)) / (2 * (q : \u211d) - 1)) (div_pos (by linarith) hpos)\n rw [Real.log_div (by linarith : (2 : \u211d) * (q : \u211d) \u2260 0) hpos.ne'] at h1\n have e : (2 * (q : \u211d)) / (2 * (q : \u211d) - 1) - 1 = 1 / (2 * (q : \u211d) - 1) := by\n field_simp [hpos.ne']\n ring\n linarith [h1, e]\n have hlogb2 : (2 * (q : \u211d)) * (Real.log (2 * (q : \u211d)) - Real.log (2 * (q : \u211d) - 1)) \u2264\n 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogb1 (by linarith : (0 : \u211d) \u2264 2 * (q : \u211d))\n have e : (2 * (q : \u211d)) * (1 / (2 * (q : \u211d) - 1)) \u2264 2 := by\n rw [mul_one_div, div_le_iff\u2080 hpos]\n linarith\n linarith [h2, e]\n linarith [hlogb2]\n \u00b7 -- n = 2q + 1, K = q: defect \u2264 1/2 < 7/2\n have hq10 : 10 \u2264 q := by omega\n have hQ : (10 : \u211d) \u2264 (q : \u211d) := by exact_mod_cast hq10\n refine hmain q ?_\n have hN : ((2 * q + 1 : \u2115) : \u211d) = 2 * (q : \u211d) + 1 := by push_cast; ring\n have hlogq1 : Real.log ((q : \u211d) + 1) = Real.log (2 * (q : \u211d) + 2) - Real.log 2 := by\n have h1 : (2 * (q : \u211d) + 2) = 2 * ((q : \u211d) + 1) := by ring\n have h2 := Real.log_mul (by norm_num : (2 : \u211d) \u2260 0)\n (by positivity : ((q : \u211d) + 1) \u2260 0)\n rw [\u2190 h1] at h2\n linarith [h2]\n rw [hN, hlogq1]\n unfold lagariasA1 lagariasC1\n rw [h4pi, h2pi]\n have hpos : (0 : \u211d) < 2 * (q : \u211d) + 1 := by linarith\n have hlogb1 : Real.log (2 * (q : \u211d) + 2) - Real.log (2 * (q : \u211d) + 1) \u2264\n 1 / (2 * (q : \u211d) + 1) := by\n have h1 := Real.log_le_sub_one_of_pos\n (x := (2 * (q : \u211d) + 2) / (2 * (q : \u211d) + 1)) (div_pos (by linarith) hpos)\n rw [Real.log_div (by linarith : (2 : \u211d) * (q : \u211d) + 2 \u2260 0) hpos.ne'] at h1\n have e : (2 * (q : \u211d) + 2) / (2 * (q : \u211d) + 1) - 1 = 1 / (2 * (q : \u211d) + 1) := by\n field_simp [hpos.ne']\n ring\n linarith [h1, e]\n have hlogb2 : ((2 * (q : \u211d) + 1) / 2) *\n (Real.log (2 * (q : \u211d) + 2) - Real.log (2 * (q : \u211d) + 1)) \u2264 1 / 2 := by\n have h2 := mul_le_mul_of_nonneg_left hlogb1\n (by positivity : (0 : \u211d) \u2264 (2 * (q : \u211d) + 1) / 2)\n have e : ((2 * (q : \u211d) + 1) / 2) * (1 / (2 * (q : \u211d) + 1)) = 1 / 2 := by\n field_simp [hpos.ne']\n linarith [h2, e]\n linarith [hlogb2]\n\n/-! ## 3. The margin and its convexity (D-057) -/\n\n/-- The honest closed-form unit-interval zero-count majorant (D-056 \u00a72):\n\u0108\u2080(t) = 0.433 log(t+2) + 0.886 log log(t+2) + 2.9. -/\ndef C0hat (t : \u211d) : \u211d :=\n 0.433 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.9\n\n/-- The two-unit-window zero-count majorant Z\u2082(t) = 0.6 log(t+2) +\n0.886 log log(t+2) + 2.7 (the `ZeroCountProp2` bound form, D-069 \u00a72).\nNamed for use in the corrected `Bn` (D-071 F-B): the I_III near-sum's\nwindow |\u03b3\u2212t| < 1 is a two-unit window, honestly counted by Z\u2082, not \u0108\u2080.\nDefinitionally the `ZeroCountProp2` closed form (that Prop's statement\nis untouched). -/\ndef Z2hat (t : \u211d) : \u211d :=\n 0.6 * Real.log (t + 2) + 0.886 * Real.log (Real.log (t + 2)) + 2.7\n\n/-- H majorant with A = 10.5, B\u2080 = 48 (D-056). -/\ndef Hhat (T : \u211d) : \u211d :=\n 3 * C0hat T ^ 2 + 10.5 * Real.log (T + 2) + 48\n\n/-- The I_I boundary-integral majorant (D-057 \u00a73):\nB\u0303\u2084(n) = 2(\u221an+1)\u00b7(e^{\u221an/2}+1)\u00b70.57\u00b72^{\u2212(2\u221an\u22122)}. -/\ndef IIMaj (n : \u211d) : \u211d :=\n 2 * (Real.sqrt n + 1) * (Real.exp (Real.sqrt n / 2) + 1) * 0.57 *\n 2 ^ (-(2 * Real.sqrt n - 2))\n\n/-- The margin majorant chain (D-057, corrected per D-071): margin\u0303(n) =\nS(n) \u2212 B\u0303(n) + 1 with the counting function majorized by a smooth\nfunction F. M\u2080 = 1.3352 (E-023, grid-verified \u2014 see D-060 \u00a74).\nCORRECTION (D-071, user-approved session 038): the bridge is 4F (the\nresidue sum \u03bb_n(T) runs over BOTH signs of \u03b3 \u2014 D-036/D-037's 2N(T)\nwas a factor-2 accounting slip, R-004 unaffected) and the I_III\nnear-sum uses the two-unit count (2/3)\u00b7Z2hat (D-069 Finding 2 made\nexact). See D-071 + E-030. -/\ndef marginTilde (F : \u211d \u2192 \u211d) (n : \u211d) : \u211d :=\n let T := Real.sqrt n + 1\n ((1 / 2) * n * Real.log n +\n (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4) -\n (4 * F T + 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3) +\n IIMaj n + 1) + 1\n\n/-! ### Block machinery for the `marginTilde_convex` proof (D-057 \u00a72) -/\n\n/-- Second-derivative computation package: if \u03c6 has derivative D1 on a\nneighborhood of T and D1 has derivative D2 at T, then \u03c6\u2033(T) = D2. -/\ntheorem deriv2_of_hasDerivAt_nhds {\u03c6 D1 : \u211d \u2192 \u211d} {T D2 : \u211d}\n (h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt \u03c6 (D1 x) x) (h2 : HasDerivAt D1 D2 T) :\n deriv (deriv \u03c6) T = D2 :=\n (h2.congr_of_eventuallyEq (by\n filter_upwards [h1] with x hx using hx.deriv)).deriv\n\n/-- The \u03c8-functional of D-057: \u03c8[\u03c6](T) = \u03c6\u2033(T) \u2212 \u03c6\u2032(T)/(T\u22121). -/\ndef psiOf (\u03c6 : \u211d \u2192 \u211d) (T : \u211d) : \u211d := deriv (deriv \u03c6) T - deriv \u03c6 T / (T - 1)\n\n/-- [PROVED session 011] Block #2 (identity): \u03c8[id](T) = \u22121/(T\u22121) < 0. -/\ntheorem psiOf_id (T : \u211d) (hT : 1 < T) : psiOf id T = -1 / (T - 1) \u2227 psiOf id T < 0 := by\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt id 1 x := by\n filter_upwards [] with x\n exact hasDerivAt_id' x\n have hd2 : deriv (deriv id) T = 0 :=\n deriv2_of_hasDerivAt_nhds h1 (hasDerivAt_const T 1)\n have hd1 : deriv id T = 1 := h1.self_of_nhds.deriv\n have h3 : (0 : \u211d) < T - 1 := by linarith\n refine \u27e8?_, ?_\u27e9\n \u00b7 unfold psiOf; rw [hd2, hd1]; ring\n \u00b7 unfold psiOf; rw [hd2, hd1]; linarith [one_div_pos.mpr h3]\n\n/-- [PROVED session 011] Block #10 (L1 = log(T+2)): \u03c8-formula. -/\ntheorem psiOf_log_shift (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => Real.log (t + 2)) T =\n -1 / (T + 2) ^ 2 - 1 / ((T + 2) * (T - 1)) := by\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => Real.log (t + 2)) ((x + 2)\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds (by linarith : (-2 : \u211d) < T)] with x hx\n have h := (Real.hasDerivAt_log (show x + 2 \u2260 0 by linarith)).comp x\n ((hasDerivAt_id' x).add_const 2)\n rwa [mul_one] at h\n have h2 : HasDerivAt (fun t => (t + 2)\u207b\u00b9) (-1 / (T + 2) ^ 2) T := by\n have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) \u2260 0)\n have e : (-(1 : \u211d)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => Real.log (t + 2)) T = (T + 2)\u207b\u00b9 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT2' : (T + 2) \u2260 0 := by linarith\n field_simp [hT1, hT2']\n\n/-- [PROVED session 011] Block #10 sign: \u03c8 < 0 for T > 1. -/\ntheorem psiOf_log_shift_neg {T : \u211d} (hT : 1 < T) :\n psiOf (fun t => Real.log (t + 2)) T < 0 := by\n rw [psiOf_log_shift T hT]\n have h1 : (0 : \u211d) < 1 / (T + 2) ^ 2 := one_div_pos.mpr (pow_pos (by linarith) 2)\n have h2 : (0 : \u211d) < 1 / ((T + 2) * (T - 1)) :=\n one_div_pos.mpr (mul_pos (by linarith) (by linarith))\n have e : -1 / (T + 2) ^ 2 - 1 / ((T + 2) * (T - 1)) =\n -(1 / (T + 2) ^ 2 + 1 / ((T + 2) * (T - 1))) := by ring\n rw [e]\n linarith [add_pos h1 h2]\n\n/-- [PROVED session 011] Reusable per-point derivative of log(t+2). -/\ntheorem hasDerivAt_log_shift (x : \u211d) (hx : -2 < x) :\n HasDerivAt (fun t => Real.log (t + 2)) (x + 2)\u207b\u00b9 x := by\n have h := (Real.hasDerivAt_log (show x + 2 \u2260 0 by linarith)).comp x\n ((hasDerivAt_id' x).add_const 2)\n rwa [mul_one] at h\n\n/-- [PROVED session 011] Reusable per-point derivative of log log(t+2). -/\ntheorem hasDerivAt_log_log (x : \u211d) (hx : -1 < x) :\n HasDerivAt (fun t => Real.log (Real.log (t + 2)))\n ((Real.log (x + 2))\u207b\u00b9 * (x + 2)\u207b\u00b9) x := by\n have hin := hasDerivAt_log_shift x (by linarith)\n have hout : HasDerivAt Real.log (Real.log (x + 2))\u207b\u00b9 (Real.log (x + 2)) :=\n Real.hasDerivAt_log (ne_of_gt (Real.log_pos (by linarith)))\n exact hout.comp x hin\n\n/-- [PROVED session 011] Numerical bounds on the block-table range\nT \u2265 \u221a20 + 1: T \u2265 5.4721, L1 \u2265 2 (via e\u00b2 \u2264 7.4721), L2 \u2265 0.6931. -/\ntheorem block_range_bounds {T : \u211d} (hT : Real.sqrt 20 + 1 \u2264 T) :\n (5.4721 : \u211d) \u2264 T \u2227 2 \u2264 Real.log (T + 2) \u2227\n (0.6931 : \u211d) \u2264 Real.log (Real.log (T + 2)) := by\n have hs : (4.4721 : \u211d) \u2264 Real.sqrt 20 := by\n rw [Real.le_sqrt (by norm_num) (by norm_num)]\n norm_num\n have hT5 : (5.4721 : \u211d) \u2264 T := by linarith\n have hT2 : (7.4721 : \u211d) \u2264 T + 2 := by linarith\n have hL1 : (2 : \u211d) \u2264 Real.log (T + 2) := by\n have he2 : Real.exp 2 \u2264 T + 2 := by\n have hd := Real.exp_one_lt_d9\n have e : Real.exp 2 = Real.exp 1 * Real.exp 1 := by\n rw [\u2190 Real.exp_add]; norm_num\n calc Real.exp 2 = Real.exp 1 * Real.exp 1 := e\n _ \u2264 2.7182818286 * 2.7182818286 :=\n mul_le_mul (le_of_lt hd) (le_of_lt hd) (Real.exp_pos 1).le (by positivity)\n _ \u2264 7.4721 := by norm_num\n _ \u2264 T + 2 := hT2\n have h2 := Real.log_le_log (Real.exp_pos 2) he2\n rwa [Real.log_exp] at h2\n have hL2 : (0.6931 : \u211d) \u2264 Real.log (Real.log (T + 2)) := by\n have h2 := Real.log_le_log (by norm_num : (0 : \u211d) < 2) hL1\n have h3 := Real.log_two_gt_d9\n linarith\n exact \u27e8hT5, hL1, hL2\u27e9\n\n/-- [PROVED session 011] Block #11 (L2 = log log(T+2)): \u03c8-formula. -/\ntheorem psiOf_log_log_shift (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => Real.log (Real.log (t + 2))) T =\n -(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 -\n 1 / ((T + 2) * Real.log (T + 2) * (T - 1)) := by\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have hL1 : (0 : \u211d) < Real.log (T + 2) := Real.log_pos (by linarith)\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => Real.log (Real.log (t + 2)))\n ((Real.log (x + 2))\u207b\u00b9 * (x + 2)\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds (by linarith : (-2 : \u211d) < T),\n eventually_gt_nhds (by linarith : (-1 : \u211d) < T)] with x hx2 hx1\n have hin : HasDerivAt (fun t => Real.log (t + 2)) (x + 2)\u207b\u00b9 x := by\n have h := (Real.hasDerivAt_log (show x + 2 \u2260 0 by linarith)).comp x\n ((hasDerivAt_id' x).add_const 2)\n rwa [mul_one] at h\n have hout : HasDerivAt Real.log (Real.log (x + 2))\u207b\u00b9 (Real.log (x + 2)) :=\n Real.hasDerivAt_log (ne_of_gt (Real.log_pos (by linarith)))\n exact hout.comp x hin\n have h2 : HasDerivAt (fun t => (Real.log (t + 2))\u207b\u00b9 * (t + 2)\u207b\u00b9)\n (-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) T := by\n have hu : HasDerivAt (fun t => (Real.log (t + 2))\u207b\u00b9)\n (-(T + 2)\u207b\u00b9 / Real.log (T + 2) ^ 2) T := by\n have hin : HasDerivAt (fun t => Real.log (t + 2)) (T + 2)\u207b\u00b9 T := by\n have h := (Real.hasDerivAt_log (show T + 2 \u2260 0 by linarith)).comp T\n ((hasDerivAt_id' T).add_const 2)\n rwa [mul_one] at h\n exact hin.inv (ne_of_gt hL1)\n have hv : HasDerivAt (fun t => (t + 2)\u207b\u00b9) (-1 / (T + 2) ^ 2) T := by\n have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) \u2260 0)\n have e : (-(1 : \u211d)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring\n rwa [e] at h\n have h := hu.mul hv\n have hT2' : (T + 2) \u2260 0 := ne_of_gt hT2\n have hL1' : Real.log (T + 2) \u2260 0 := ne_of_gt hL1\n have e : (-(T + 2)\u207b\u00b9 / Real.log (T + 2) ^ 2) * (T + 2)\u207b\u00b9 +\n (Real.log (T + 2))\u207b\u00b9 * (-1 / (T + 2) ^ 2) =\n -(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 := by\n field_simp [hT2', hL1']\n ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => Real.log (Real.log (t + 2))) T =\n (Real.log (T + 2))\u207b\u00b9 * (T + 2)\u207b\u00b9 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT2' : (T + 2) \u2260 0 := ne_of_gt hT2\n have hL1' : Real.log (T + 2) \u2260 0 := ne_of_gt hL1\n field_simp [hT1, hT2', hL1']\n\n/-- [PROVED session 011] Block #11 sign: \u03c8 < 0 for T > 1. -/\ntheorem psiOf_log_log_shift_neg {T : \u211d} (hT : 1 < T) :\n psiOf (fun t => Real.log (Real.log (t + 2))) T < 0 := by\n rw [psiOf_log_log_shift T hT]\n have hL1 : (0 : \u211d) < Real.log (T + 2) := Real.log_pos (by linarith)\n have hp1 : (0 : \u211d) < (Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 :=\n div_pos (by linarith) (pow_pos (mul_pos (by linarith) hL1) 2)\n have hp2 : (0 : \u211d) < 1 / ((T + 2) * Real.log (T + 2) * (T - 1)) :=\n one_div_pos.mpr (mul_pos (mul_pos (by linarith) hL1) (by linarith))\n have e : -(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 -\n 1 / ((T + 2) * Real.log (T + 2) * (T - 1)) =\n -((Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2 +\n 1 / ((T + 2) * Real.log (T + 2) * (T - 1))) := by ring\n rw [e]\n linarith [add_pos hp1 hp2]\n\n/-- [PROVED session 011] Block #7 (L1\u00b2): \u03c8-formula. -/\ntheorem psiOf_log_sq_shift (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => Real.log (t + 2) ^ 2) T =\n 2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2 -\n 2 * Real.log (T + 2) / ((T + 2) * (T - 1)) := by\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => Real.log (t + 2) ^ 2)\n (2 * Real.log (x + 2) * (x + 2)\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds (by linarith : (-2 : \u211d) < T)] with x hx\n have h := (hasDerivAt_log_shift x (by linarith)).pow 2\n rwa [pow_one, Nat.cast_ofNat] at h\n have h2 : HasDerivAt (fun t => 2 * Real.log (t + 2) * (t + 2)\u207b\u00b9)\n (2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2) T := by\n have hu : HasDerivAt (fun t => 2 * Real.log (t + 2)) (2 * (T + 2)\u207b\u00b9) T :=\n (hasDerivAt_log_shift T (by linarith : (-2 : \u211d) < T)).const_mul 2\n have hv : HasDerivAt (fun t => (t + 2)\u207b\u00b9) (-1 / (T + 2) ^ 2) T := by\n have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) \u2260 0)\n have e : (-(1 : \u211d)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring\n rwa [e] at h\n have h := hu.mul hv\n have hT2' : (T + 2) \u2260 0 := by linarith\n have e : 2 * (T + 2)\u207b\u00b9 * (T + 2)\u207b\u00b9 + 2 * Real.log (T + 2) * (-1 / (T + 2) ^ 2) =\n 2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2 := by\n field_simp [hT2']\n ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => Real.log (t + 2) ^ 2) T =\n 2 * Real.log (T + 2) * (T + 2)\u207b\u00b9 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT2' : (T + 2) \u2260 0 := by linarith\n field_simp [hT1, hT2']\n\n/-- [PROVED session 011] Block #7 sign: \u03c8 < 0 on the table range (L1 \u2265 2). -/\ntheorem psiOf_log_sq_shift_neg {T : \u211d} (hT : Real.sqrt 20 + 1 \u2264 T) :\n psiOf (fun t => Real.log (t + 2) ^ 2) T < 0 := by\n obtain \u27e8hT5, hL1, _\u27e9 := block_range_bounds hT\n rw [psiOf_log_sq_shift T (by linarith)]\n have h1 : 2 * (1 - Real.log (T + 2)) / (T + 2) ^ 2 < 0 :=\n div_neg_of_neg_of_pos (by linarith) (pow_pos (by linarith) 2)\n have h2 : (0 : \u211d) < 2 * Real.log (T + 2) / ((T + 2) * (T - 1)) :=\n div_pos (by linarith) (mul_pos (by linarith) (by linarith))\n linarith\n\n/-- [PROVED session 011] Block #8 (L1\u00b7L2): \u03c8-formula. -/\ntheorem psiOf_log_mul_log_shift (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) T =\n ((Real.log (T + 2))\u207b\u00b9 - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2 -\n (Real.log (Real.log (T + 2)) + 1) / ((T + 2) * (T - 1)) := by\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have hL1 : (0 : \u211d) < Real.log (T + 2) := Real.log_pos (by linarith)\n have h1 : \u2200\u1da0 x in \ud835\udcdd T,\n HasDerivAt (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n ((Real.log (Real.log (x + 2)) + 1) * (x + 2)\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds (by linarith : (-1 : \u211d) < T)] with x hx\n have hu := hasDerivAt_log_shift x (by linarith)\n have hv := hasDerivAt_log_log x hx\n have h := hu.mul hv\n have hx2 : (x + 2) \u2260 0 := by linarith\n have hxL : Real.log (x + 2) \u2260 0 := ne_of_gt (Real.log_pos (by linarith))\n have e : (x + 2)\u207b\u00b9 * Real.log (Real.log (x + 2)) +\n Real.log (x + 2) * ((Real.log (x + 2))\u207b\u00b9 * (x + 2)\u207b\u00b9) =\n (Real.log (Real.log (x + 2)) + 1) * (x + 2)\u207b\u00b9 := by\n field_simp [hx2, hxL]\n rwa [e] at h\n have h2 : HasDerivAt (fun t => (Real.log (Real.log (t + 2)) + 1) * (t + 2)\u207b\u00b9)\n (((Real.log (T + 2))\u207b\u00b9 - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2) T := by\n have hw : HasDerivAt (fun t => Real.log (Real.log (t + 2)) + 1)\n ((Real.log (T + 2))\u207b\u00b9 * (T + 2)\u207b\u00b9) T :=\n (hasDerivAt_log_log T (by linarith)).add_const 1\n have hz : HasDerivAt (fun t => (t + 2)\u207b\u00b9) (-1 / (T + 2) ^ 2) T := by\n have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) \u2260 0)\n have e : (-(1 : \u211d)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring\n rwa [e] at h\n have h := hw.mul hz\n have hT2' : (T + 2) \u2260 0 := by linarith\n have hL1' : Real.log (T + 2) \u2260 0 := ne_of_gt hL1\n have e : (Real.log (T + 2))\u207b\u00b9 * (T + 2)\u207b\u00b9 * (T + 2)\u207b\u00b9 +\n (Real.log (Real.log (T + 2)) + 1) * (-1 / (T + 2) ^ 2) =\n ((Real.log (T + 2))\u207b\u00b9 - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2 := by\n field_simp [hT2', hL1']\n ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) T =\n (Real.log (Real.log (T + 2)) + 1) * (T + 2)\u207b\u00b9 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT2' : (T + 2) \u2260 0 := by linarith\n field_simp [hT1, hT2']\n\n/-- [PROVED session 011] Block #8 sign: \u03c8 < 0 on the table range\n(1/L1 \u2264 1/2 < 1 + L2). -/\ntheorem psiOf_log_mul_log_shift_neg {T : \u211d} (hT : Real.sqrt 20 + 1 \u2264 T) :\n psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) T < 0 := by\n obtain \u27e8hT5, hL1, hL2\u27e9 := block_range_bounds hT\n rw [psiOf_log_mul_log_shift T (by linarith)]\n have hinv : (Real.log (T + 2))\u207b\u00b9 \u2264 1 / 2 := by\n have h := one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 2) hL1\n rwa [one_div] at h\n have hbr : (Real.log (T + 2))\u207b\u00b9 - Real.log (Real.log (T + 2)) - 1 < 0 := by\n linarith\n have h1 : ((Real.log (T + 2))\u207b\u00b9 - Real.log (Real.log (T + 2)) - 1) / (T + 2) ^ 2 < 0 :=\n div_neg_of_neg_of_pos hbr (pow_pos (by linarith) 2)\n have h2 : (0 : \u211d) < (Real.log (Real.log (T + 2)) + 1) / ((T + 2) * (T - 1)) :=\n div_pos (by linarith) (mul_pos (by linarith) (by linarith))\n linarith\n\n/-- [PROVED session 011] Block #9 (L2\u00b2): \u03c8-formula. -/\ntheorem psiOf_log_log_sq_shift (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) T =\n 2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /\n ((T + 2) * Real.log (T + 2)) ^ 2 -\n 2 * Real.log (Real.log (T + 2)) / ((T + 2) * Real.log (T + 2) * (T - 1)) := by\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have hL1 : (0 : \u211d) < Real.log (T + 2) := Real.log_pos (by linarith)\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => Real.log (Real.log (t + 2)) ^ 2)\n (2 * Real.log (Real.log (x + 2)) * ((x + 2) * Real.log (x + 2))\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds (by linarith : (-1 : \u211d) < T)] with x hx\n have h := (hasDerivAt_log_log x hx).pow 2\n have e : (2 : \u211d) * Real.log (Real.log (x + 2)) ^ 1 *\n ((Real.log (x + 2))\u207b\u00b9 * (x + 2)\u207b\u00b9) =\n 2 * Real.log (Real.log (x + 2)) * ((x + 2) * Real.log (x + 2))\u207b\u00b9 := by\n rw [pow_one, mul_inv]; ring\n rwa [Nat.cast_ofNat, e] at h\n have h2 : HasDerivAt\n (fun t => 2 * Real.log (Real.log (t + 2)) * ((t + 2) * Real.log (t + 2))\u207b\u00b9)\n (2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /\n ((T + 2) * Real.log (T + 2)) ^ 2) T := by\n have hz_inner : HasDerivAt (fun t => (t + 2) * Real.log (t + 2))\n (Real.log (T + 2) + 1) T := by\n have h := ((hasDerivAt_id' T).add_const 2).mul\n (hasDerivAt_log_shift T (by linarith))\n have e : (1 : \u211d) * Real.log (T + 2) + (T + 2) * (T + 2)\u207b\u00b9 =\n Real.log (T + 2) + 1 := by\n rw [mul_inv_cancel\u2080 (by linarith : (T + 2) \u2260 0)]; ring\n rwa [e] at h\n have hz : HasDerivAt (fun t => ((t + 2) * Real.log (t + 2))\u207b\u00b9)\n (-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) T :=\n hz_inner.inv (mul_ne_zero (by linarith) (ne_of_gt hL1))\n have hw := (hasDerivAt_log_log T (by linarith)).const_mul 2\n have h := hw.mul hz\n have hT2' : (T + 2) \u2260 0 := by linarith\n have hL1' : Real.log (T + 2) \u2260 0 := ne_of_gt hL1\n have e : 2 * ((Real.log (T + 2))\u207b\u00b9 * (T + 2)\u207b\u00b9) *\n ((T + 2) * Real.log (T + 2))\u207b\u00b9 +\n 2 * Real.log (Real.log (T + 2)) *\n (-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) =\n 2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /\n ((T + 2) * Real.log (T + 2)) ^ 2 := by\n field_simp [hT2', hL1']\n ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => Real.log (Real.log (t + 2)) ^ 2) T =\n 2 * Real.log (Real.log (T + 2)) * ((T + 2) * Real.log (T + 2))\u207b\u00b9 :=\n h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT2' : (T + 2) \u2260 0 := by linarith\n have hL1' : Real.log (T + 2) \u2260 0 := ne_of_gt hL1\n field_simp [hT1, hT2', hL1']\n\n/-- [PROVED session 011] Block #9 sign: \u03c8 < 0 on the table range\n(L2(L1+1) \u2265 0.6931\u00b73 > 1). -/\ntheorem psiOf_log_log_sq_shift_neg {T : \u211d} (hT : Real.sqrt 20 + 1 \u2264 T) :\n psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) T < 0 := by\n obtain \u27e8hT5, hL1, hL2\u27e9 := block_range_bounds hT\n rw [psiOf_log_log_sq_shift T (by linarith)]\n have hprod : (1 : \u211d) < Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1) := by\n calc (1 : \u211d) < 0.6931 * (2 + 1) := by norm_num\n _ \u2264 Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1) :=\n mul_le_mul hL2 (by linarith) (by linarith) (by linarith)\n have h1 : 2 * (1 - Real.log (Real.log (T + 2)) * (Real.log (T + 2) + 1)) /\n ((T + 2) * Real.log (T + 2)) ^ 2 < 0 :=\n div_neg_of_neg_of_pos (by linarith)\n (pow_pos (mul_pos (by linarith) (by linarith)) 2)\n have h2 : (0 : \u211d) < 2 * Real.log (Real.log (T + 2)) /\n ((T + 2) * Real.log (T + 2) * (T - 1)) :=\n div_pos (by linarith) (mul_pos (mul_pos (by linarith) (by linarith)) (by linarith))\n linarith\n\n/-- [PROVED session 011] Block #5 (T\u00b7L1): \u03c8-formula. -/\ntheorem psiOf_T_mul_log_shift (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => t * Real.log (t + 2)) T =\n (T + 4) / (T + 2) ^ 2 - Real.log (T + 2) / (T - 1) -\n T / ((T + 2) * (T - 1)) := by\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => t * Real.log (t + 2))\n (Real.log (x + 2) + x * (x + 2)\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds (by linarith : (-2 : \u211d) < T)] with x hx\n have h := (hasDerivAt_id' x).mul (hasDerivAt_log_shift x (by linarith))\n rwa [one_mul] at h\n have h2 : HasDerivAt (fun t => Real.log (t + 2) + t * (t + 2)\u207b\u00b9)\n ((T + 4) / (T + 2) ^ 2) T := by\n have hu := hasDerivAt_log_shift T (by linarith : (-2 : \u211d) < T)\n have hv : HasDerivAt (fun t => t * (t + 2)\u207b\u00b9) (2 / (T + 2) ^ 2) T := by\n have hz : HasDerivAt (fun t => (t + 2)\u207b\u00b9) (-1 / (T + 2) ^ 2) T := by\n have h := ((hasDerivAt_id' T).add_const 2).inv (by linarith : (T + 2) \u2260 0)\n have e : (-(1 : \u211d)) / (T + 2) ^ 2 = -1 / (T + 2) ^ 2 := by ring\n rwa [e] at h\n have h := (hasDerivAt_id' T).mul hz\n have hT2' : (T + 2) \u2260 0 := by linarith\n have e : (1 : \u211d) * (T + 2)\u207b\u00b9 + T * (-1 / (T + 2) ^ 2) = 2 / (T + 2) ^ 2 := by\n field_simp [hT2']\n ring\n rwa [e] at h\n have h := hu.add hv\n have hT2' : (T + 2) \u2260 0 := by linarith\n have e : (T + 2)\u207b\u00b9 + 2 / (T + 2) ^ 2 = (T + 4) / (T + 2) ^ 2 := by\n field_simp [hT2']\n ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => t * Real.log (t + 2)) T =\n Real.log (T + 2) + T * (T + 2)\u207b\u00b9 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT2' : (T + 2) \u2260 0 := by linarith\n field_simp [hT1, hT2']\n ring\n\n/-- [PROVED session 011] Block #5 sign: \u03c8 < 0 on the table range\n(L1 \u2265 2; numerator \u22122T\u00b2 \u2212 7T \u2212 12). -/\ntheorem psiOf_T_mul_log_shift_neg {T : \u211d} (hT : Real.sqrt 20 + 1 \u2264 T) :\n psiOf (fun t => t * Real.log (t + 2)) T < 0 := by\n obtain \u27e8hT5, hL1, _\u27e9 := block_range_bounds hT\n have h1T : 1 < T := by linarith\n rw [psiOf_T_mul_log_shift T h1T]\n have hT1 : (0 : \u211d) < T - 1 := by linarith\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have hle : (2 : \u211d) / (T - 1) \u2264 Real.log (T + 2) / (T - 1) := by gcongr\n have hneg : (T + 4) / (T + 2) ^ 2 - 2 / (T - 1) - T / ((T + 2) * (T - 1)) < 0 := by\n have hnum : (T + 4) / (T + 2) ^ 2 - 2 / (T - 1) - T / ((T + 2) * (T - 1)) =\n (-(2 * T ^ 2 + 7 * T + 12)) / ((T + 2) ^ 2 * (T - 1)) := by\n field_simp [hT1.ne', hT2.ne']\n ring\n rw [hnum]\n exact div_neg_of_neg_of_pos (by linarith [sq_nonneg T])\n (mul_pos (pow_pos hT2 2) hT1)\n linarith\n\n/-- [PROVED session 011] Block #6 (T\u00b7L2): \u03c8-formula. -/\ntheorem psiOf_T_mul_log_log_shift (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => t * Real.log (Real.log (t + 2))) T =\n (T * (Real.log (T + 2) - 1) + 4 * Real.log (T + 2)) /\n ((T + 2) * Real.log (T + 2)) ^ 2 -\n Real.log (Real.log (T + 2)) / (T - 1) -\n T / ((T + 2) * Real.log (T + 2) * (T - 1)) := by\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have hL1 : (0 : \u211d) < Real.log (T + 2) := Real.log_pos (by linarith)\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => t * Real.log (Real.log (t + 2)))\n (Real.log (Real.log (x + 2)) + x * ((x + 2) * Real.log (x + 2))\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds (by linarith : (-1 : \u211d) < T)] with x hx\n have h := (hasDerivAt_id' x).mul (hasDerivAt_log_log x hx)\n have hx2 : (x + 2) \u2260 0 := by linarith\n have hxL : Real.log (x + 2) \u2260 0 := ne_of_gt (Real.log_pos (by linarith))\n have e : (1 : \u211d) * Real.log (Real.log (x + 2)) +\n x * ((Real.log (x + 2))\u207b\u00b9 * (x + 2)\u207b\u00b9) =\n Real.log (Real.log (x + 2)) + x * ((x + 2) * Real.log (x + 2))\u207b\u00b9 := by\n rw [one_mul, mul_inv]\n ring\n rwa [e] at h\n have h2 : HasDerivAt\n (fun t => Real.log (Real.log (t + 2)) + t * ((t + 2) * Real.log (t + 2))\u207b\u00b9)\n ((T * (Real.log (T + 2) - 1) + 4 * Real.log (T + 2)) /\n ((T + 2) * Real.log (T + 2)) ^ 2) T := by\n have hu := hasDerivAt_log_log T (by linarith : (-1 : \u211d) < T)\n have hz_inner : HasDerivAt (fun t => (t + 2) * Real.log (t + 2))\n (Real.log (T + 2) + 1) T := by\n have h := ((hasDerivAt_id' T).add_const 2).mul\n (hasDerivAt_log_shift T (by linarith))\n have e : (1 : \u211d) * Real.log (T + 2) + (T + 2) * (T + 2)\u207b\u00b9 =\n Real.log (T + 2) + 1 := by\n rw [mul_inv_cancel\u2080 (by linarith : (T + 2) \u2260 0)]; ring\n rwa [e] at h\n have hz : HasDerivAt (fun t => ((t + 2) * Real.log (t + 2))\u207b\u00b9)\n (-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2) T :=\n hz_inner.inv (mul_ne_zero (by linarith) (ne_of_gt hL1))\n have hv := (hasDerivAt_id' T).mul hz\n have h := hu.add hv\n have hT2' : (T + 2) \u2260 0 := by linarith\n have hL1' : Real.log (T + 2) \u2260 0 := ne_of_gt hL1\n have e : (Real.log (T + 2))\u207b\u00b9 * (T + 2)\u207b\u00b9 +\n ((1 : \u211d) * ((T + 2) * Real.log (T + 2))\u207b\u00b9 +\n T * (-(Real.log (T + 2) + 1) / ((T + 2) * Real.log (T + 2)) ^ 2)) =\n (T * (Real.log (T + 2) - 1) + 4 * Real.log (T + 2)) /\n ((T + 2) * Real.log (T + 2)) ^ 2 := by\n field_simp [hT2', hL1']\n ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => t * Real.log (Real.log (t + 2))) T =\n Real.log (Real.log (T + 2)) + T * ((T + 2) * Real.log (T + 2))\u207b\u00b9 :=\n h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT2' : (T + 2) \u2260 0 := by linarith\n have hL1' : Real.log (T + 2) \u2260 0 := ne_of_gt hL1\n field_simp [hT1, hT2', hL1']\n ring\n\n/-- [PROVED session 011] Block #6 sign: \u03c8 < 0 on the table range.\nReduction (D-057 #6): \u03c8 < 0 \u27f8 A(T\u22121) \u2264 T(T+2)L1 \u27f8 L1(T\u22124) \u2264 T(T\u22121)\n\u27f8 L1 \u2264 T+1 \u2264 T(T\u22121)/(T\u22124). -/\ntheorem psiOf_T_mul_log_log_shift_neg {T : \u211d} (hT : Real.sqrt 20 + 1 \u2264 T) :\n psiOf (fun t => t * Real.log (Real.log (t + 2))) T < 0 := by\n obtain \u27e8hT5, hL1b, hL2b\u27e9 := block_range_bounds hT\n have h1T : 1 < T := by linarith\n rw [psiOf_T_mul_log_log_shift T h1T]\n have hT1 : (0 : \u211d) < T - 1 := by linarith\n have hT2 : (0 : \u211d) < T + 2 := by linarith\n have hL1 : (0 : \u211d) < Real.log (T + 2) := Real.log_pos (by linarith)\n have hL2 : (0 : \u211d) < Real.log (Real.log (T + 2)) := by linarith\n set L1 := Real.log (T + 2) with hL1def\n set L2 := Real.log (Real.log (T + 2)) with hL2def\n set D := (T + 2) * L1 with hDdef\n have hD : (0 : \u211d) < D := mul_pos hT2 hL1\n have hlog_le : L1 \u2264 T + 1 := by\n have h := Real.log_le_sub_one_of_pos (x := T + 2) (by linarith)\n linarith\n have hstep : L1 * (T - 4) \u2264 T * (T - 1) := by\n have h1 : L1 * (T - 4) \u2264 (T + 1) * (T - 4) :=\n mul_le_mul_of_nonneg_right hlog_le (by linarith)\n nlinarith\n have hA : (T * (L1 - 1) + 4 * L1) * (T - 1) \u2264 T * D := by\n have h2 : (T * (L1 - 1) + 4 * L1) * (T - 1) = T * (T + 2) * L1 - (T * (T - 1) -\n L1 * (T - 4)) := by ring\n rw [h2, hDdef]\n nlinarith [hstep]\n have hkey : (T * (L1 - 1) + 4 * L1) * (T - 1) - L2 * D ^ 2 - T * D < 0 := by\n have h3 : (0 : \u211d) < L2 * D ^ 2 := mul_pos hL2 (pow_pos hD 2)\n linarith [hA]\n have hpsi : (T * (L1 - 1) + 4 * L1) / D ^ 2 - L2 / (T - 1) - T / (D * (T - 1)) =\n ((T * (L1 - 1) + 4 * L1) * (T - 1) - L2 * D ^ 2 - T * D) /\n (D ^ 2 * (T - 1)) := by\n field_simp [hT1.ne', ne_of_gt hD]\n rw [hpsi]\n exact div_neg_of_neg_of_pos hkey (mul_pos (pow_pos hD 2) hT1)\n\n/-! ### The IIMaj (B\u0303\u2084) term (D-057 \u00a73) -/\n\n/-- Decay rate a = 2 log 2 \u2212 1/2 \u2248 0.8863. -/\nprivate def iimA : \u211d := 2 * Real.log 2 - 1 / 2\n\n/-- Decay rate b = 2 log 2 \u2248 1.3863. -/\nprivate def iimB : \u211d := 2 * Real.log 2\n\n/-- The IIMaj term as a function of s = \u221an: 4.56\u00b7(s+1)\u00b7(e^{\u2212as} + e^{\u2212bs}). -/\nprivate def psiTilde (s : \u211d) : \u211d :=\n 4.56 * ((s + 1) * (Real.exp (-iimA * s) + Real.exp (-iimB * s)))\n\n/-- [PROVED session 011] IIMaj n = \u03c8\u0303(\u221an): the rpow/exp bookkeeping. -/\ntheorem IIMaj_eq_psiTilde_sqrt (n : \u211d) :\n IIMaj n = psiTilde (Real.sqrt n) := by\n have hrw : (2 : \u211d) ^ (-(2 * Real.sqrt n - 2)) =\n 4 * Real.exp (-(2 * Real.log 2) * Real.sqrt n) := by\n rw [show (-(2 * Real.sqrt n - 2) : \u211d) = 2 + -(2 * Real.sqrt n) by ring,\n Real.rpow_add (by norm_num : (0 : \u211d) < 2)]\n have e2 : (2 : \u211d) ^ (-(2 * Real.sqrt n)) =\n Real.exp (-(2 * Real.log 2) * Real.sqrt n) := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2)]\n congr 1\n ring\n have e1 : (2 : \u211d) ^ (2 : \u211d) = 4 := by\n rw [Real.rpow_def_of_pos (by norm_num : (0 : \u211d) < 2),\n show Real.log 2 * 2 = Real.log (2 ^ 2) by rw [Real.log_pow]; ring,\n Real.exp_log (by norm_num : (0 : \u211d) < 2 ^ 2)]\n norm_num\n rw [e2, e1]\n have hEA : Real.exp (Real.sqrt n / 2) * Real.exp (-(2 * Real.log 2) * Real.sqrt n) =\n Real.exp (-(2 * Real.log 2 - 1 / 2) * Real.sqrt n) := by\n rw [\u2190 Real.exp_add]\n congr 1\n ring\n unfold IIMaj psiTilde iimA iimB\n rw [hrw,\n show 2 * (Real.sqrt n + 1) * (Real.exp (Real.sqrt n / 2) + 1) * 0.57 *\n (4 * Real.exp (-(2 * Real.log 2) * Real.sqrt n)) =\n 4.56 * ((Real.sqrt n + 1) *\n ((Real.exp (Real.sqrt n / 2) + 1) * Real.exp (-(2 * Real.log 2) * Real.sqrt n))) by ring,\n show (Real.exp (Real.sqrt n / 2) + 1) * Real.exp (-(2 * Real.log 2) * Real.sqrt n) =\n Real.exp (Real.sqrt n / 2) * Real.exp (-(2 * Real.log 2) * Real.sqrt n) +\n Real.exp (-(2 * Real.log 2) * Real.sqrt n) by ring,\n hEA]\n\n/-- [PROVED session 012] Crude global upper bound on the I_I majorant:\nIIMaj n \u2264 4.56\u00b7(\u221an+1)\u00b72 for n \u2265 0 (both exponentials \u2264 1). Consumed by\nthe base-point numerics (LiBasePoints); the slack is absorbed by the\nmargin. -/\ntheorem IIMaj_le_two_mul (n : \u211d) (_hn : 0 \u2264 n) :\n IIMaj n \u2264 4.56 * (Real.sqrt n + 1) * 2 := by\n rw [IIMaj_eq_psiTilde_sqrt]\n unfold psiTilde\n have hlog2 := Real.log_two_gt_d9\n have ha : (0 : \u211d) < iimA := by unfold iimA; linarith\n have hb : (0 : \u211d) < iimB := by unfold iimB; linarith\n have hs : (0 : \u211d) \u2264 Real.sqrt n := Real.sqrt_nonneg n\n have heA : Real.exp (-iimA * Real.sqrt n) \u2264 1 := by\n rw [Real.exp_le_one_iff]\n exact mul_nonpos_of_nonpos_of_nonneg (by linarith) hs\n have heB : Real.exp (-iimB * Real.sqrt n) \u2264 1 := by\n rw [Real.exp_le_one_iff]\n exact mul_nonpos_of_nonpos_of_nonneg (by linarith) hs\n have hpos : (0 : \u211d) \u2264 Real.sqrt n + 1 := by linarith\n calc 4.56 * ((Real.sqrt n + 1) *\n (Real.exp (-iimA * Real.sqrt n) + Real.exp (-iimB * Real.sqrt n)))\n \u2264 4.56 * ((Real.sqrt n + 1) * (1 + 1)) := by\n apply mul_le_mul_of_nonneg_left _ (by norm_num : (0 : \u211d) \u2264 4.56)\n apply mul_le_mul_of_nonneg_left _ hpos\n linarith [heA, heB]\n _ = 4.56 * (Real.sqrt n + 1) * 2 := by ring\n\n/-- [PROVED session 012] IIMaj is nonnegative. -/\ntheorem IIMaj_nonneg (n : \u211d) : 0 \u2264 IIMaj n := by\n unfold IIMaj\n apply mul_nonneg; apply mul_nonneg; apply mul_nonneg; apply mul_nonneg\n \u00b7 norm_num\n \u00b7 linarith [Real.sqrt_nonneg n]\n \u00b7 have h := Real.exp_pos (Real.sqrt n / 2)\n linarith\n \u00b7 norm_num\n \u00b7 exact Real.rpow_nonneg (by norm_num) _\n\n/-- [PROVED session 011] \u03c8\u0303 is globally C\u00b2 (polynomial \u00d7 exponentials). -/\ntheorem psiTilde_contDiff : ContDiff \u211d 2 psiTilde := by\n unfold psiTilde iimA iimB\n exact contDiff_const.mul\n ((contDiff_id.add contDiff_const).mul\n ((contDiff_const.mul contDiff_id).exp.add (contDiff_const.mul contDiff_id).exp))\n\n/-- [PROVED session 011] \u03c8\u0303\u2032 in closed form (per-point, global). -/\ntheorem hasDerivAt_psiTilde (x : \u211d) :\n HasDerivAt psiTilde\n (4.56 * ((Real.exp (-iimA * x) + Real.exp (-iimB * x)) +\n (x + 1) * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)))) x := by\n unfold psiTilde iimA iimB\n have hu : HasDerivAt (fun t => t + 1) 1 x := (hasDerivAt_id' x).add_const 1\n have hva : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2 - 1 / 2) * t))\n (Real.exp (-(2 * Real.log 2 - 1 / 2) * x) * (-(2 * Real.log 2 - 1 / 2))) x := by\n have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2 - 1 / 2))).exp\n rwa [mul_one] at h\n have hvb : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2) * t))\n (Real.exp (-(2 * Real.log 2) * x) * (-(2 * Real.log 2))) x := by\n have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2))).exp\n rwa [mul_one] at h\n have h := (hu.mul (hva.add hvb)).const_mul 4.56\n simp only [Pi.add_apply, Pi.mul_apply] at h\n convert h using 2 <;> first | rfl | ring\n\n/-- [PROVED session 011] deriv \u03c8\u0303 = the closed D1 form. -/\ntheorem deriv_psiTilde (x : \u211d) :\n deriv psiTilde x =\n 4.56 * ((Real.exp (-iimA * x) + Real.exp (-iimB * x)) +\n (x + 1) * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x))) :=\n (hasDerivAt_psiTilde x).deriv\n\n/-- [PROVED session 011] \u03c8\u0303\u2033 in closed form. -/\ntheorem deriv2_psiTilde (x : \u211d) :\n deriv (deriv psiTilde) x =\n 4.56 * (2 * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)) +\n (x + 1) * (iimA ^ 2 * Real.exp (-iimA * x) +\n iimB ^ 2 * Real.exp (-iimB * x))) := by\n have h1 : \u2200\u1da0 y in \ud835\udcdd x, HasDerivAt psiTilde\n (4.56 * ((Real.exp (-iimA * y) + Real.exp (-iimB * y)) +\n (y + 1) * (-iimA * Real.exp (-iimA * y) - iimB * Real.exp (-iimB * y)))) y := by\n filter_upwards [] with y\n exact hasDerivAt_psiTilde y\n have h2 : HasDerivAt\n (fun t => 4.56 * ((Real.exp (-iimA * t) + Real.exp (-iimB * t)) +\n (t + 1) * (-iimA * Real.exp (-iimA * t) - iimB * Real.exp (-iimB * t))))\n (4.56 * (2 * (-iimA * Real.exp (-iimA * x) - iimB * Real.exp (-iimB * x)) +\n (x + 1) * (iimA ^ 2 * Real.exp (-iimA * x) +\n iimB ^ 2 * Real.exp (-iimB * x)))) x := by\n unfold iimA iimB\n have hu : HasDerivAt (fun t => t + 1) 1 x := (hasDerivAt_id' x).add_const 1\n have hva : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2 - 1 / 2) * t))\n (Real.exp (-(2 * Real.log 2 - 1 / 2) * x) * (-(2 * Real.log 2 - 1 / 2))) x := by\n have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2 - 1 / 2))).exp\n rwa [mul_one] at h\n have hvb : HasDerivAt (fun t => Real.exp (-(2 * Real.log 2) * t))\n (Real.exp (-(2 * Real.log 2) * x) * (-(2 * Real.log 2))) x := by\n have h := ((hasDerivAt_id' x).const_mul (-(2 * Real.log 2))).exp\n rwa [mul_one] at h\n have hw := hva.add hvb\n have hg := (hva.const_mul (-(2 * Real.log 2 - 1 / 2))).sub\n (hvb.const_mul (2 * Real.log 2))\n have hz := hu.mul hg\n have h := (hw.add hz).const_mul 4.56\n simp only [Pi.add_apply, Pi.mul_apply, Pi.sub_apply] at h\n convert h using 2 <;> first | rfl | ring\n exact deriv2_of_hasDerivAt_nhds h1 h2\n\n/-- [PROVED session 011] u\u2082(t) = (b\u00b2t+b)\u00b7e^{\u2212at} is antitone on [\u221a20, \u221e):\nits derivative is e^{\u2212at}\u00b7(b\u00b2 \u2212 a(b\u00b2t+b)) and a(b\u00b2t+b) \u2265 8.846 > b\u00b2 there. -/\ntheorem iim_u2_antitone :\n AntitoneOn (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))\n (Set.Ici (Real.sqrt 20)) := by\n have hCD : ContDiff \u211d 2 (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t)) := by\n unfold iimA iimB\n exact ((contDiff_const.mul contDiff_id).add contDiff_const).mul\n ((contDiff_const.mul contDiff_id).exp)\n have hder : \u2200 x : \u211d,\n HasDerivAt (fun t => (iimB ^ 2 * t + iimB) * Real.exp (-iimA * t))\n (Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB))) x := by\n intro x\n have hp : HasDerivAt (fun t => iimB ^ 2 * t + iimB) (iimB ^ 2 * 1) x :=\n ((hasDerivAt_id' x).const_mul (iimB ^ 2)).add_const iimB\n have he : HasDerivAt (fun t => Real.exp (-iimA * t))\n (Real.exp (-iimA * x) * (-iimA * 1)) x :=\n ((hasDerivAt_id' x).const_mul (-iimA)).exp\n have h := hp.mul he\n have e : iimB ^ 2 * 1 * Real.exp (-iimA * x) + (iimB ^ 2 * x + iimB) *\n (Real.exp (-iimA * x) * (-iimA * 1)) =\n Real.exp (-iimA * x) * (iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB)) := by ring\n rw [e] at h\n exact h\n apply antitoneOn_of_deriv_nonpos (convex_Ici _)\n \u00b7 exact hCD.continuous.continuousOn\n \u00b7 exact (hCD.differentiable (by norm_num)).differentiableOn.mono interior_subset\n \u00b7 intro x hx\n rw [interior_Ici] at hx\n have hxs : Real.sqrt 20 < x := Set.mem_Ioi.mp hx\n have hlog2lo := Real.log_two_gt_d9\n have hlog2hi := Real.log_two_lt_d9\n have ha : (0.8862943606 : \u211d) \u2264 iimA := by unfold iimA; linarith\n have hblo : (1.3862943606 : \u211d) \u2264 iimB := by unfold iimB; linarith\n have hb : iimB \u2264 (1.3862943616 : \u211d) := by unfold iimB; linarith\n have hbpos : (0 : \u211d) < iimB := by linarith\n have hapos : (0 : \u211d) < iimA := by linarith\n have hb2lo : (1.9218 : \u211d) \u2264 iimB ^ 2 := by nlinarith [hblo]\n have hb2up : iimB ^ 2 \u2264 (1.92182 : \u211d) := by nlinarith [hb, hbpos]\n have hx4 : (4.4721 : \u211d) \u2264 x := by\n have h : (4.4721 : \u211d) \u2264 Real.sqrt 20 := by\n rw [Real.le_sqrt (by norm_num) (by norm_num)]; norm_num\n linarith\n have hbig : (8.8458 : \u211d) \u2264 iimA * (iimB ^ 2 * x + iimB) := by\n have hb2x : (9.9807 : \u211d) \u2264 iimB ^ 2 * x + iimB := by\n have h1 : (1.9218 : \u211d) * 4.4721 \u2264 iimB ^ 2 * x :=\n mul_le_mul hb2lo hx4 (by norm_num) (sq_nonneg iimB)\n nlinarith [hblo]\n calc (8.8458 : \u211d) \u2264 0.8862943606 * 9.9807 := by norm_num\n _ \u2264 iimA * (iimB ^ 2 * x + iimB) := mul_le_mul ha hb2x (by norm_num) hapos.le\n rw [(hder x).deriv]\n have h : iimB ^ 2 - iimA * (iimB ^ 2 * x + iimB) \u2264 0 := by linarith\n exact mul_nonpos_of_nonneg_of_nonpos (Real.exp_pos _).le h\n\nset_option maxHeartbeats 800000 in\n/-- [PROVED session 011; strengthened to 4/3 session 040 for the\nD-074 dog-leg's 1.5\u00b7IIMaj charge] The B\u0303\u2084 bracket bound (D-057 \u00a73):\nfor s \u2265 \u221a20,\n\u03c8\u0303\u2033(s) \u2212 \u03c8\u0303\u2032(s)/s < 4/3. Factor-monotone argument: the bound splits as\n4.56\u00b7[(s+1)/s]\u00b7[(b\u00b2s+b)e^{\u2212as}]\u00b7[1+e^{\u2212s/2}], three positive decreasing\nfactors; at s = \u221a20 the product is \u2264 1.3155 < 4/3. -/\ntheorem iimaj_bracket_bound {s : \u211d} (hs : Real.sqrt 20 \u2264 s) :\n 4.56 * (2 * (-iimA * Real.exp (-iimA * s) - iimB * Real.exp (-iimB * s)) +\n (s + 1) * (iimA ^ 2 * Real.exp (-iimA * s) +\n iimB ^ 2 * Real.exp (-iimB * s))) -\n (4.56 * ((Real.exp (-iimA * s) + Real.exp (-iimB * s)) +\n (s + 1) * (-iimA * Real.exp (-iimA * s) -\n iimB * Real.exp (-iimB * s)))) / s < 4 / 3 := by\n unfold iimA iimB\n set L := Real.log 2 with hLdef\n set a : \u211d := 2 * L - 1 / 2 with hadef\n set b : \u211d := 2 * L with hbdef\n set eA := Real.exp (-a * s) with heAdef\n set eB := Real.exp (-b * s) with heBdef\n have hlog2lo := Real.log_two_gt_d9\n have hlog2hi := Real.log_two_lt_d9\n rw [\u2190 hLdef] at hlog2lo hlog2hi\n have ha : (0.8862943606 : \u211d) \u2264 a := by rw [hadef]; linarith\n have haup : a \u2264 (0.8862943616 : \u211d) := by rw [hadef]; linarith\n have hblo : (1.3862943606 : \u211d) \u2264 b := by rw [hbdef]; linarith\n have hb : b \u2264 (1.3862943616 : \u211d) := by rw [hbdef]; linarith\n have hab : a \u2264 b := by rw [hadef, hbdef]; linarith\n have hapos : (0 : \u211d) < a := by linarith\n have hbpos : (0 : \u211d) < b := by linarith\n have hsqrtlo : (4.4721 : \u211d) \u2264 Real.sqrt 20 := by\n rw [Real.le_sqrt (by norm_num) (by norm_num)]; norm_num\n have hsqrthi : Real.sqrt 20 \u2264 (4.4722 : \u211d) := by\n have h : Real.sqrt 20 \u2264 Real.sqrt (4.4722 ^ 2) :=\n Real.sqrt_le_sqrt (by norm_num)\n rwa [Real.sqrt_sq (by norm_num)] at h\n have hs0 : (0 : \u211d) < s := by linarith [Real.sqrt_nonneg 20]\n have hs4 : (4.4721 : \u211d) \u2264 s := by linarith\n have hs4' : s \u2264 s := le_refl s\n have heA : (0 : \u211d) < eA := Real.exp_pos _\n have heB : (0 : \u211d) < eB := Real.exp_pos _\n -- step 1: drop the two negative terms\n have hstep1 :\n 4.56 * (2 * (-a * eA - b * eB) + (s + 1) * (a ^ 2 * eA + b ^ 2 * eB)) -\n (4.56 * ((eA + eB) + (s + 1) * (-a * eA - b * eB))) / s \u2264\n 4.56 * ((s + 1) * (a ^ 2 * eA + b ^ 2 * eB) +\n (s + 1) * (a * eA + b * eB) / s) := by\n have hd1 : 2 * (-a * eA - b * eB) \u2264 0 := by\n nlinarith [mul_nonneg hapos.le heA.le, mul_nonneg hbpos.le heB.le]\n have hd2 : -((eA + eB) / s) \u2264 0 := by\n have h : (0 : \u211d) \u2264 (eA + eB) / s :=\n div_nonneg (add_nonneg heA.le heB.le) hs0.le\n linarith\n have hsf : (4.56 * ((eA + eB) + (s + 1) * (-a * eA - b * eB))) / s =\n 4.56 * ((eA + eB) / s + (s + 1) * (-a * eA - b * eB) / s) := by\n field_simp [hs0.ne']\n rw [hsf]\n have hsf2 : (s + 1) * (-a * eA - b * eB) / s = -((s + 1) * (a * eA + b * eB) / s) := by\n field_simp [hs0.ne']\n ring\n rw [hsf2]\n linarith\n -- step 2: factor out b\u00b2 and b/s termwise\n have hstep2 :\n 4.56 * ((s + 1) * (a ^ 2 * eA + b ^ 2 * eB) +\n (s + 1) * (a * eA + b * eB) / s) \u2264\n 4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) := by\n have hsq : a ^ 2 \u2264 b ^ 2 := by nlinarith [hab, hapos]\n have h1 : a ^ 2 * eA + b ^ 2 * eB \u2264 b ^ 2 * (eA + eB) := by\n nlinarith [mul_le_mul_of_nonneg_right hsq heA.le]\n have h2 : (a * eA + b * eB) / s \u2264 b * (eA + eB) / s := by\n have h := add_le_add (mul_le_mul_of_nonneg_right hab heA.le) (le_refl (b * eB))\n have h' : a * eA + b * eB \u2264 b * (eA + eB) := by nlinarith [h]\n gcongr\n have m1 : (s + 1) * (a ^ 2 * eA + b ^ 2 * eB) \u2264 (s + 1) * (b ^ 2 * (eA + eB)) :=\n mul_le_mul_of_nonneg_left h1 (by linarith)\n have m2 : (s + 1) * (a * eA + b * eB) / s \u2264 (s + 1) * (b * (eA + eB)) / s := by\n have h3 := mul_le_mul_of_nonneg_left h2 (show (0 : \u211d) \u2264 s + 1 by linarith)\n rwa [\u2190 mul_div_assoc, \u2190 mul_div_assoc] at h3\n have e3 : 4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) =\n 4.56 * ((s + 1) * (b ^ 2 * (eA + eB)) + (s + 1) * (b * (eA + eB)) / s) := by\n field_simp [hs0.ne']\n rw [e3]\n exact mul_le_mul_of_nonneg_left (add_le_add m1 m2) (by norm_num)\n -- step 3: the three-factor split\n have hstep3 :\n 4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) =\n 4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) := by\n have heB' : eB = eA * Real.exp (-s / 2) := by\n rw [heBdef, heAdef, \u2190 Real.exp_add]\n congr 1\n rw [hadef, hbdef]\n ring\n rw [heB']\n field_simp [hs0.ne']\n -- step 4: the three monotone factors at s = \u221a20\n have hu1 : (s + 1) / s \u2264 (1.2237 : \u211d) := by\n have h1 : (1 : \u211d) / s \u2264 1 / 4.4721 := one_div_le_one_div_of_le (by norm_num) hs4\n have h2 : (1 : \u211d) / 4.4721 \u2264 0.2237 := by\n rw [div_le_iff\u2080 (by norm_num : (0 : \u211d) < 4.4721)]\n norm_num\n have h3 : (s + 1) / s = 1 + 1 / s := by field_simp [hs0.ne']\n rw [h3]\n linarith\n have hu2fac : (b ^ 2 * s + b) * eA \u2264 (0.2124 : \u211d) := by\n have hAid : iimA = a := by unfold iimA; rw [\u2190 hLdef, \u2190 hadef]\n have hBid : iimB = b := by unfold iimB; rw [\u2190 hLdef, \u2190 hbdef]\n have hanti := iim_u2_antitone\n rw [hAid, hBid] at hanti\n have hu2le : (b ^ 2 * s + b) * Real.exp (-a * s) \u2264\n (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) :=\n hanti (Set.mem_Ici.mpr (le_refl _)) (Set.mem_Ici.mpr hs) hs\n have hu2val : (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) \u2264\n (0.2124 : \u211d) := by\n have hb2up : b ^ 2 \u2264 (1.92182 : \u211d) := by nlinarith [hb, hbpos]\n have hexp : Real.exp (-a * Real.sqrt 20) \u2264 (0.0212766 : \u211d) := by\n have ht : (3.9635 : \u211d) \u2264 a * Real.sqrt 20 := by\n calc (3.9635 : \u211d) \u2264 0.8862943606 * 4.4721 := by norm_num\n _ \u2264 a * Real.sqrt 20 :=\n mul_le_mul ha hsqrtlo (by norm_num) hapos.le\n have hsum : (47 : \u211d) \u2264 Real.exp (a * Real.sqrt 20) := by\n have h1 := Real.sum_le_exp_of_nonneg (x := (3.9635 : \u211d)) (by norm_num) 7\n have h2 : Real.exp (3.9635 : \u211d) \u2264 Real.exp (a * Real.sqrt 20) :=\n Real.exp_le_exp.mpr ht\n have h3 : (47 : \u211d) \u2264 \u2211 i \u2208 Finset.range 7,\n (3.9635 : \u211d) ^ i / (Nat.factorial i : \u211d) := by\n norm_num [Finset.sum_range_succ]\n linarith\n rw [show -a * Real.sqrt 20 = -(a * Real.sqrt 20) by ring, Real.exp_neg]\n calc (Real.exp (a * Real.sqrt 20))\u207b\u00b9 \u2264 1 / 47 := by\n rw [\u2190 one_div]\n exact one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 47) hsum\n _ \u2264 0.0212766 := by\n rw [div_le_iff\u2080 (by norm_num : (0 : \u211d) < 47)]; norm_num\n have hpoly : b ^ 2 * Real.sqrt 20 + b \u2264 (9.9811 : \u211d) := by\n have h1 : b ^ 2 * Real.sqrt 20 \u2264 1.92182 * 4.4722 :=\n mul_le_mul hb2up hsqrthi (Real.sqrt_nonneg 20) (by norm_num)\n linarith\n exact le_trans (mul_le_mul hpoly hexp (Real.exp_pos _).le (by norm_num))\n (by norm_num)\n calc (b ^ 2 * s + b) * eA = (b ^ 2 * s + b) * Real.exp (-a * s) := rfl\n _ \u2264 (b ^ 2 * Real.sqrt 20 + b) * Real.exp (-a * Real.sqrt 20) := hu2le\n _ \u2264 0.2124 := hu2val\n have hu3 : 1 + Real.exp (-s / 2) \u2264 (1.1099 : \u211d) := by\n have hexp : Real.exp (-s / 2) \u2264 (0.10982 : \u211d) := by\n have ht : (2.23605 : \u211d) \u2264 s / 2 := by linarith\n have hsum : (9.1064 : \u211d) \u2264 Real.exp (s / 2) := by\n have h1 := Real.sum_le_exp_of_nonneg (x := (2.23605 : \u211d)) (by norm_num) 6\n have h2 : Real.exp (2.23605 : \u211d) \u2264 Real.exp (s / 2) := Real.exp_le_exp.mpr ht\n have h3 : (9.1064 : \u211d) \u2264 \u2211 i \u2208 Finset.range 6,\n (2.23605 : \u211d) ^ i / (Nat.factorial i : \u211d) := by\n norm_num [Finset.sum_range_succ]\n linarith\n rw [show -s / 2 = -(s / 2) by ring, Real.exp_neg]\n calc (Real.exp (s / 2))\u207b\u00b9 \u2264 1 / 9.1064 := by\n rw [\u2190 one_div]\n exact one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 9.1064) hsum\n _ \u2264 0.10982 := by\n rw [div_le_iff\u2080 (by norm_num : (0 : \u211d) < 9.1064)]; norm_num\n linarith\n -- final assembly\n have hpos1 : (0 : \u211d) \u2264 (b ^ 2 * s + b) * eA :=\n mul_nonneg (by nlinarith [hbpos, hs0, sq_nonneg b]) heA.le\n have hpos2 : (0 : \u211d) \u2264 1 + Real.exp (-s / 2) := by positivity\n have hpos3 : (0 : \u211d) \u2264 (s + 1) / s := by positivity\n have hchain : 4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) \u2264\n 4.56 * 1.2237 * 0.2124 * 1.1099 := by\n have h1 : ((s + 1) / s) * ((b ^ 2 * s + b) * eA) \u2264 1.2237 * 0.2124 :=\n mul_le_mul hu1 hu2fac hpos1 (by norm_num)\n have h2 : ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) \u2264\n 1.2237 * 0.2124 * 1.1099 :=\n mul_le_mul h1 hu3 hpos2 (by positivity)\n have h3 := mul_le_mul_of_nonneg_left h2 (by norm_num : (0 : \u211d) \u2264 4.56)\n have e : (4.56 : \u211d) * (((s + 1) / s) * ((b ^ 2 * s + b) * eA) *\n (1 + Real.exp (-s / 2))) =\n 4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) := by ring\n have e' : (4.56 : \u211d) * (1.2237 * 0.2124 * 1.1099) = 4.56 * 1.2237 * 0.2124 * 1.1099 := by ring\n rwa [e, e'] at h3\n calc 4.56 * (2 * (-a * eA - b * eB) + (s + 1) * (a ^ 2 * eA + b ^ 2 * eB)) -\n (4.56 * ((eA + eB) + (s + 1) * (-a * eA - b * eB))) / s\n \u2264 4.56 * (s + 1) * (b ^ 2 + b / s) * (eA + eB) := le_trans hstep1 hstep2\n _ = 4.56 * ((s + 1) / s) * ((b ^ 2 * s + b) * eA) * (1 + Real.exp (-s / 2)) := hstep3\n _ \u2264 4.56 * 1.2237 * 0.2124 * 1.1099 := hchain\n _ < 4 / 3 := by norm_num\n\n/-! ### Assembly: regularity bundles -/\n\n/-- [PROVED session 011] The blocks are C\u00b2 on (\u22121, \u221e) (all\nL1/L2-singularities lie at T \u2264 \u22121). -/\ntheorem contDiffOn_L1 : ContDiffOn \u211d 2 (fun t => Real.log (t + 2)) (Set.Ioi (-1)) :=\n (contDiffOn_id.add contDiffOn_const).log (fun x hx => by\n have h : -1 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x + 2))\n\ntheorem contDiffOn_L2 :\n ContDiffOn \u211d 2 (fun t => Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=\n contDiffOn_L1.log (fun x hx => by\n have h : -1 < x := hx\n exact ne_of_gt (Real.log_pos (by linarith : (1 : \u211d) < x + 2)))\n\ntheorem contDiffOn_L1sq :\n ContDiffOn \u211d 2 (fun t => Real.log (t + 2) ^ 2) (Set.Ioi (-1)) :=\n contDiffOn_L1.pow 2\n\ntheorem contDiffOn_L1L2 : ContDiffOn \u211d 2\n (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=\n contDiffOn_L1.mul contDiffOn_L2\n\ntheorem contDiffOn_L2sq :\n ContDiffOn \u211d 2 (fun t => Real.log (Real.log (t + 2)) ^ 2) (Set.Ioi (-1)) :=\n contDiffOn_L2.pow 2\n\ntheorem contDiffOn_TL1 :\n ContDiffOn \u211d 2 (fun t => t * Real.log (t + 2)) (Set.Ioi (-1)) :=\n contDiffOn_id.mul contDiffOn_L1\n\ntheorem contDiffOn_TL2 :\n ContDiffOn \u211d 2 (fun t => t * Real.log (Real.log (t + 2))) (Set.Ioi (-1)) :=\n contDiffOn_id.mul contDiffOn_L2\n\n/-- [PROVED session 011] T(m) = \u221am + 1 is C\u00b2 on (20, \u221e) and maps it\ninto (\u22121, \u221e). -/\ntheorem contDiffOn_sqrt_shift :\n ContDiffOn \u211d 2 (fun m => Real.sqrt m + 1) (Set.Ioi 20) :=\n (contDiffOn_id.sqrt (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x))).add contDiffOn_const\n\ntheorem mapsTo_sqrt_shift :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi (-1)) := by\n intro x hx\n have h : 20 < x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)\n\n/-- [PROVED session 012] \u221am + 1 maps (20, \u221e) into (1, \u221e) (the FAlt\ndomain). -/\ntheorem mapsTo_sqrt_shift_Ioi1 :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ioi 20) (Set.Ioi 1) := by\n intro x hx\n have h : 20 < x := hx\n have hpos := Real.sqrt_pos.mpr (by linarith : (0 : \u211d) < x)\n exact Set.mem_Ioi.mpr (by linarith)\n\n/-- [PROVED session 012] \u221am + 1 maps [20, \u221e) into (1, \u221e). -/\ntheorem mapsTo_sqrt_shift_Ici_Ioi1 :\n Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi 1) := by\n intro x hx\n have h : 20 \u2264 x := hx\n have hpos := Real.sqrt_pos.mpr (by linarith : (0 : \u211d) < x)\n exact Set.mem_Ioi.mpr (by linarith)\n\n/-- [PROVED session 011] psiOf at T = \u221an + 1 in the chain-rule form\n(with T \u2212 1 = \u221an). -/\ntheorem psiOf_sqrt_rel (\u03c6 : \u211d \u2192 \u211d) (n : \u211d) :\n psiOf \u03c6 (Real.sqrt n + 1) =\n deriv (deriv \u03c6) (Real.sqrt n + 1) - deriv \u03c6 (Real.sqrt n + 1) / Real.sqrt n := by\n unfold psiOf\n rw [show Real.sqrt n + 1 - 1 = Real.sqrt n by ring]\n\n/-- [PROVED session 011] Second derivative of a sum (needs first-deriv\ndifferentiability at n and eventual differentiability near n). -/\ntheorem deriv2_add {f g : \u211d \u2192 \u211d} {n : \u211d}\n (hf1 : DifferentiableAt \u211d (deriv f) n) (hg1 : DifferentiableAt \u211d (deriv g) n)\n (hf2 : \u2200\u1da0 m in \ud835\udcdd n, DifferentiableAt \u211d f m)\n (hg2 : \u2200\u1da0 m in \ud835\udcdd n, DifferentiableAt \u211d g m) :\n deriv (deriv fun x => f x + g x) n = deriv (deriv f) n + deriv (deriv g) n := by\n have he : deriv (fun x => f x + g x) =\u1da0[\ud835\udcdd n] (fun m => deriv f m + deriv g m) := by\n filter_upwards [hf2, hg2] with m hfm hgm\n exact deriv_add hfm hgm\n have h2 := (hf1.add hg1).hasDerivAt\n rw [deriv_add hf1 hg1] at h2\n exact (h2.congr_of_eventuallyEq he).deriv\n\n/-- [PROVED session 011] Second derivative of a constant multiple. -/\ntheorem deriv2_const_mul {f : \u211d \u2192 \u211d} {n : \u211d} (c : \u211d)\n (hf1 : DifferentiableAt \u211d (deriv f) n)\n (hf2 : \u2200\u1da0 m in \ud835\udcdd n, DifferentiableAt \u211d f m) :\n deriv (deriv (fun m => c * f m)) n = c * deriv (deriv f) n := by\n have he : deriv (fun m => c * f m) =\u1da0[\ud835\udcdd n] (fun m => c * deriv f m) := by\n filter_upwards [hf2] with m hfm\n exact deriv_const_mul c hfm\n have h2 := (hf1.const_mul c).hasDerivAt\n rw [deriv_const_mul c hf1] at h2\n exact (h2.congr_of_eventuallyEq he).deriv\n\n/-- [PROVED session 011] Second derivative of a constant function. -/\ntheorem deriv2_const_val (K n : \u211d) : deriv (deriv fun _ => K) n = 0 := by\n have h1 : \u2200\u1da0 m in \ud835\udcdd n, HasDerivAt (fun _ => K) 0 m := by\n filter_upwards [] with m\n exact hasDerivAt_const m K\n exact deriv2_of_hasDerivAt_nhds h1 (hasDerivAt_const n 0)\n\n/-- [PROVED session 011] Per-point first derivative of the S-function. -/\ntheorem hasDerivAt_marginS (c : \u211d) {m : \u211d} (hm : 0 < m) :\n HasDerivAt (fun m => (1 / 2) * m * Real.log m + c * m - 4)\n ((1 / 2) * (Real.log m + 1) + c) m := by\n have hlog : HasDerivAt Real.log m\u207b\u00b9 m := Real.hasDerivAt_log (ne_of_gt hm)\n have hml := ((hasDerivAt_id' m).const_mul (1 / 2)).mul hlog\n have h := (hml.add ((hasDerivAt_id' m).const_mul c)).sub_const 4\n have hm0 : m \u2260 0 := ne_of_gt hm\n convert h using 2 <;> first | rfl | field_simp [hm0]\n\n/-- [PROVED session 011] Second derivative of the S-function: S\u2033 = 1/(2n). -/\ntheorem marginS_deriv2 (c : \u211d) {n : \u211d} (hn : 0 < n) :\n deriv (deriv fun m => (1 / 2) * m * Real.log m + c * m - 4) n =\n 1 / (2 * n) := by\n have h1 : \u2200\u1da0 m in \ud835\udcdd n, HasDerivAt (fun m => (1 / 2) * m * Real.log m + c * m - 4)\n ((1 / 2) * (Real.log m + 1) + c) m := by\n filter_upwards [eventually_gt_nhds hn] with m hm\n exact hasDerivAt_marginS c hm\n have h2 : HasDerivAt (fun m => (1 / 2) * (Real.log m + 1) + c) (1 / (2 * n)) n := by\n have h := ((Real.hasDerivAt_log (ne_of_gt hn)).add_const 1).const_mul (1 / 2)\n convert h.add_const c using 2 <;> first | rfl | ring\n exact deriv2_of_hasDerivAt_nhds h1 h2\n\n/-! ### The expanded margin (D-057 \u00a74 assembly) -/\n\n/-- The margin pieces as block compositions (for chain-rule application).\nConstants updated for the D-071 correction (4F bridge; (2/3)Z2 I_III). -/\nprivate def mFblock (F : \u211d \u2192 \u211d) : \u211d \u2192 \u211d := fun m => (-4) * F (Real.sqrt m + 1)\nprivate def mTL1b : \u211d \u2192 \u211d := fun m => (-((8/3)*0.6 + 42)) *\n ((fun t => t * Real.log (t + 2)) (Real.sqrt m + 1))\nprivate def mTL2b : \u211d \u2192 \u211d := fun m => (-((8/3)*0.886)) *\n ((fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\nprivate def mIdb : \u211d \u2192 \u211d := fun m => (-((8/3)*2.7 + 192)) * (Real.sqrt m + 1)\nprivate def mL1sqb : \u211d \u2192 \u211d := fun m => (-(42*0.433^2*(Real.exp 4 + 1))) *\n ((fun t => Real.log (t + 2) ^ 2) (Real.sqrt m + 1))\nprivate def mL1L2b : \u211d \u2192 \u211d := fun m => (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *\n ((fun t => Real.log (t + 2) * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\nprivate def mL2sqb : \u211d \u2192 \u211d := fun m => (-(42*0.886^2*(Real.exp 4 + 1))) *\n ((fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt m + 1))\nprivate def mL1b : \u211d \u2192 \u211d := fun m => (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *\n ((fun t => Real.log (t + 2)) (Real.sqrt m + 1))\nprivate def mL2b : \u211d \u2192 \u211d := fun m => (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *\n ((fun t => Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\nprivate def mIIM : \u211d \u2192 \u211d := fun m => (-1) * IIMaj m\nprivate def mK : \u211d := -40*1.3352 - 2*(Real.exp 4 + 1)*(7*(3*2.9^2 + 48) + 3.3) - 1 + 1\n\n/-- The margin as an explicit left-nested sum of pieces. -/\nprivate def marginExpanded (F : \u211d \u2192 \u211d) : \u211d \u2192 \u211d := fun n =>\n (((((((((((fun m => (1/2)*m*Real.log m + (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n +\n mFblock F n) + mTL1b n) + mTL2b n) + mIdb n) + mL1sqb n) + mL1L2b n) +\n mL2sqb n) + mL1b n) + mL2b n) + mIIM n) + mK\n\n/-- [PROVED session 011] marginTilde = marginExpanded (the D-056/D-057\nconstant bookkeeping, checked by `ring`). -/\ntheorem marginTilde_eq_expanded (F : \u211d \u2192 \u211d) :\n marginTilde F = marginExpanded F := by\n funext n\n simp only [marginTilde, marginExpanded, mFblock, mTL1b, mTL2b, mIdb, mL1sqb,\n mL1L2b, mL2sqb, mL1b, mL2b, mIIM, mK, Hhat, C0hat, Z2hat]\n ring\n\n/-- [PROVED session 011] The pieces are C\u00b2 on (20, \u221e). -/\ntheorem contDiffOn_mS (c : \u211d) :\n ContDiffOn \u211d 2 (fun m => (1/2)*m*Real.log m + c*m - 4) (Set.Ioi 20) :=\n (((contDiffOn_const.mul contDiffOn_id).mul (contDiffOn_id.log (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x)))).add\n (contDiffOn_const.mul contDiffOn_id)).sub contDiffOn_const\n\ntheorem contDiffOn_mFblock (F : \u211d \u2192 \u211d) (hF : ContDiffOn \u211d 2 F (Set.Ioi 1)) :\n ContDiffOn \u211d 2 (mFblock F) (Set.Ioi 20) :=\n contDiffOn_const.mul\n (hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1)\n\ntheorem contDiffOn_mTL1b : ContDiffOn \u211d 2 mTL1b (Set.Ioi 20) :=\n contDiffOn_const.mul (contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)\n\ntheorem contDiffOn_mTL2b : ContDiffOn \u211d 2 mTL2b (Set.Ioi 20) :=\n contDiffOn_const.mul (contDiffOn_TL2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)\n\ntheorem contDiffOn_mIdb : ContDiffOn \u211d 2 mIdb (Set.Ioi 20) :=\n contDiffOn_const.mul contDiffOn_sqrt_shift\n\ntheorem contDiffOn_mL1sqb : ContDiffOn \u211d 2 mL1sqb (Set.Ioi 20) :=\n contDiffOn_const.mul (contDiffOn_L1sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)\n\ntheorem contDiffOn_mL1L2b : ContDiffOn \u211d 2 mL1L2b (Set.Ioi 20) :=\n contDiffOn_const.mul (contDiffOn_L1L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)\n\ntheorem contDiffOn_mL2sqb : ContDiffOn \u211d 2 mL2sqb (Set.Ioi 20) :=\n contDiffOn_const.mul (contDiffOn_L2sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)\n\ntheorem contDiffOn_mL1b : ContDiffOn \u211d 2 mL1b (Set.Ioi 20) :=\n contDiffOn_const.mul (contDiffOn_L1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)\n\ntheorem contDiffOn_mL2b : ContDiffOn \u211d 2 mL2b (Set.Ioi 20) :=\n contDiffOn_const.mul (contDiffOn_L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift)\n\ntheorem contDiffOn_mIIM : ContDiffOn \u211d 2 mIIM (Set.Ioi 20) := by\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n have hsqrt : ContDiffOn \u211d 2 (fun m => Real.sqrt m) (Set.Ioi 20) :=\n contDiffOn_id.sqrt (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x))\n have hcomp : ContDiffOn \u211d 2 (psiTilde \u2218 Real.sqrt) (Set.Ioi 20) :=\n (psiTilde_contDiff.contDiffOn).comp hsqrt (Set.mapsTo_univ _ _)\n unfold mIIM\n rw [hId]\n exact contDiffOn_const.mul hcomp\n\n/-- [PROVED session 011] The margin is continuous on [20, \u221e) (endpoint\nincluded \u2014 the C\u00b2 regularity on (20, \u221e) does not give the endpoint). -/\ntheorem continuousOn_marginExpanded (F : \u211d \u2192 \u211d) (hF : ContDiffOn \u211d 2 F (Set.Ioi 1)) :\n ContinuousOn (marginExpanded F) (Set.Ici 20) := by\n have hsqrt : ContinuousOn Real.sqrt (Set.Ici 20) := Real.continuous_sqrt.continuousOn\n have hT : ContinuousOn (fun m => Real.sqrt m + 1) (Set.Ici 20) :=\n hsqrt.add continuousOn_const\n have hmaps : Set.MapsTo (fun m => Real.sqrt m + 1) (Set.Ici 20) (Set.Ioi (-1)) := by\n intro x hx\n have h : 20 \u2264 x := hx\n have hnn := Real.sqrt_nonneg x\n exact Set.mem_Ioi.mpr (by linarith)\n have hlog : ContinuousOn Real.log (Set.Ici 20) :=\n Real.continuousOn_log.mono (fun x hx => by\n have h : 20 \u2264 x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x))\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n have hIIMc : ContinuousOn IIMaj (Set.Ici 20) := by\n rw [hId]\n exact (psiTilde_contDiff.continuous.continuousOn).comp hsqrt (Set.mapsTo_univ _ _)\n have hSc : ContinuousOn\n (fun m => (1/2)*m*Real.log m + (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4)\n (Set.Ici 20) :=\n (((continuousOn_const.mul continuousOn_id).mul hlog).add\n (continuousOn_const.mul continuousOn_id)).sub continuousOn_const\n unfold marginExpanded mFblock mTL1b mTL2b mIdb mL1sqb mL1L2b mL2sqb mL1b mL2b mIIM\n refine (((((((((((hSc.add\n ((hF.continuousOn.comp hT mapsTo_sqrt_shift_Ici_Ioi1).const_mul (-4))).add\n ((contDiffOn_TL1.continuousOn.comp hT hmaps).const_mul _)).add\n ((contDiffOn_TL2.continuousOn.comp hT hmaps).const_mul _)).add\n (hT.const_mul _)).add\n ((contDiffOn_L1sq.continuousOn.comp hT hmaps).const_mul _)).add\n ((contDiffOn_L1L2.continuousOn.comp hT hmaps).const_mul _)).add\n ((contDiffOn_L2sq.continuousOn.comp hT hmaps).const_mul _)).add\n ((contDiffOn_L1.continuousOn.comp hT hmaps).const_mul _)).add\n ((contDiffOn_L2.continuousOn.comp hT hmaps).const_mul _)).add\n (hIIMc.const_mul (-1)))).add\n continuousOn_const\n\n/-- [PROVED session 011] The full margin is C\u00b2 on (20, \u221e). -/\ntheorem contDiffOn_marginExpanded (F : \u211d \u2192 \u211d) (hF : ContDiffOn \u211d 2 F (Set.Ioi 1)) :\n ContDiffOn \u211d 2 (marginExpanded F) (Set.Ioi 20) := by\n unfold marginExpanded\n refine (((((((((((contDiffOn_mS _).add (contDiffOn_mFblock F hF)).add\n contDiffOn_mTL1b).add contDiffOn_mTL2b).add contDiffOn_mIdb).add\n contDiffOn_mL1sqb).add contDiffOn_mL1L2b).add contDiffOn_mL2sqb).add\n contDiffOn_mL1b).add contDiffOn_mL2b).add contDiffOn_mIIM).add\n contDiffOn_const\n\n\n/-- [PROVED session 011; generalized session 012 to any c \u2264 1]\nLocalized variant of `chain_rule_sqrt_shift`: \u03c6 only needs to be C\u00b2 on\n(c, \u221e) with c \u2264 1 (all D-057 blocks: L1-singularities at T = \u22122,\nL2-singularities at T = \u22121, so c = \u22121 suffices for them; the explicit\nTrudgian majorant FAlt of session 012 has log-singularities at 0 and 1,\nso it uses c = 1). -/\ntheorem chain_rule_sqrt_shift_on (\u03c6 : \u211d \u2192 \u211d) {c : \u211d} (hc : c \u2264 1)\n (h\u03c6 : ContDiffOn \u211d 2 \u03c6 (Set.Ioi c)) (n : \u211d) (hn : 0 < n) :\n deriv (deriv fun n => \u03c6 (Real.sqrt n + 1)) n =\n (deriv (deriv \u03c6) (Real.sqrt n + 1) -\n deriv \u03c6 (Real.sqrt n + 1) / Real.sqrt n) / (4 * n) := by\n have h\u03c6d : DifferentiableOn \u211d \u03c6 (Set.Ioi c) :=\n h\u03c6.differentiableOn (by norm_num)\n have h\u03c6dd : DifferentiableOn \u211d (deriv \u03c6) (Set.Ioi c) :=\n (h\u03c6.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero\n have hmem : \u2200 m : \u211d, 0 < m \u2192 Set.Ioi c \u2208 \ud835\udcdd (Real.sqrt m + 1) := by\n intro m hm\n have h1 : (1 : \u211d) < Real.sqrt m + 1 := by\n have h := Real.sqrt_pos.mpr hm\n linarith\n exact Ioi_mem_nhds (lt_of_le_of_lt hc h1)\n have h\u03c61 : \u2200 m : \u211d, 0 < m \u2192 DifferentiableAt \u211d \u03c6 (Real.sqrt m + 1) :=\n fun m hm => h\u03c6d.differentiableAt (hmem m hm)\n have h\u03c62 : DifferentiableAt \u211d (deriv \u03c6) (Real.sqrt n + 1) :=\n h\u03c6dd.differentiableAt (hmem n hn)\n have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=\n Real.hasDerivAt_sqrt hn.ne'\n have hdiff_sqrt : DifferentiableAt \u211d Real.sqrt n := hsqrt.differentiableAt\n have hdiff_h : DifferentiableAt \u211d (fun n => Real.sqrt n + 1) n :=\n hdiff_sqrt.add (differentiableAt_const 1)\n have hpos : Set.Ioi (0 : \u211d) \u2208 \ud835\udcdd n := Ioi_mem_nhds hn\n have hg1 : deriv (fun n => \u03c6 (Real.sqrt n + 1)) =\u1da0[\ud835\udcdd n]\n fun n => deriv \u03c6 (Real.sqrt n + 1) * (2 * Real.sqrt n)\u207b\u00b9 := by\n filter_upwards [hpos] with m hm\n have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=\n Real.hasDerivAt_sqrt (ne_of_gt hm)\n have hhm : DifferentiableAt \u211d (fun x => Real.sqrt x + 1) m :=\n hsm.differentiableAt.add (differentiableAt_const 1)\n have h1 : deriv (fun x => Real.sqrt x + 1) m = 1 / (2 * Real.sqrt m) := by\n rw [deriv_add_const]\n exact hsm.deriv\n rw [show (fun x => \u03c6 (Real.sqrt x + 1)) = \u03c6 \u2218 (fun x => Real.sqrt x + 1)\n from rfl,\n deriv_comp m (h\u03c61 m hm) hhm, h1]\n ring\n have hA : HasDerivAt (fun n => deriv \u03c6 (Real.sqrt n + 1))\n (deriv (deriv \u03c6) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n))) n := by\n have h1 : HasDerivAt (fun x => Real.sqrt x + 1) (1 / (2 * Real.sqrt n)) n :=\n hsqrt.add_const 1\n have h2 : HasDerivAt (deriv \u03c6) (deriv (deriv \u03c6) (Real.sqrt n + 1))\n (Real.sqrt n + 1) :=\n h\u03c62.hasDerivAt\n have h3 := h2.comp n h1\n rwa [show (fun n => deriv \u03c6 (Real.sqrt n + 1)) =\n deriv \u03c6 \u2218 (fun n => Real.sqrt n + 1) from rfl]\n have hB : HasDerivAt (fun n => (2 * Real.sqrt n)\u207b\u00b9)\n (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2) n := by\n have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=\n hsqrt.const_mul 2\n have h2 : (2 * Real.sqrt n) \u2260 0 :=\n mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)\n exact h1.inv h2\n have hmul : HasDerivAt (fun n => deriv \u03c6 (Real.sqrt n + 1) * (2 * Real.sqrt n)\u207b\u00b9)\n (deriv (deriv \u03c6) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n)) * (2 * Real.sqrt n)\u207b\u00b9 +\n deriv \u03c6 (Real.sqrt n + 1) *\n (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n :=\n hA.mul hB\n have hder := (hmul.congr_of_eventuallyEq hg1).deriv\n rw [hder]\n set s := Real.sqrt n with hsdef\n have hs0 : s \u2260 0 := Real.sqrt_ne_zero'.2 hn\n have hn_eq : n = s ^ 2 := by\n rw [hsdef]; exact (Real.sq_sqrt hn.le).symm\n rw [hn_eq]\n field_simp [hs0]\n ring\n\n/-- [PROVED session 011] Chain-rule identity with T(n) = \u221an (no shift),\nfor the IIMaj term: d\u00b2/dn\u00b2 \u03c8(\u221an) = [\u03c8\u2033(\u221an) \u2212 \u03c8\u2032(\u221an)/\u221an] / (4n). -/\ntheorem chain_rule_sqrt (\u03c8 : \u211d \u2192 \u211d) (h\u03c8 : ContDiff \u211d 2 \u03c8)\n (n : \u211d) (hn : 0 < n) :\n deriv (deriv fun n => \u03c8 (Real.sqrt n)) n =\n (deriv (deriv \u03c8) (Real.sqrt n) -\n deriv \u03c8 (Real.sqrt n) / Real.sqrt n) / (4 * n) := by\n have h\u03c81 : Differentiable \u211d \u03c8 := h\u03c8.differentiable (by norm_num)\n have h\u03c82 : Differentiable \u211d (deriv \u03c8) :=\n (h\u03c8.deriv' (n := 1)).differentiable one_ne_zero\n have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=\n Real.hasDerivAt_sqrt hn.ne'\n have hpos : Set.Ioi (0 : \u211d) \u2208 \ud835\udcdd n := Ioi_mem_nhds hn\n have hg1 : deriv (fun n => \u03c8 (Real.sqrt n)) =\u1da0[\ud835\udcdd n]\n fun n => deriv \u03c8 (Real.sqrt n) * (2 * Real.sqrt n)\u207b\u00b9 := by\n filter_upwards [hpos] with m hm\n have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=\n Real.hasDerivAt_sqrt (ne_of_gt hm)\n rw [show (fun x => \u03c8 (Real.sqrt x)) = \u03c8 \u2218 Real.sqrt from rfl,\n deriv_comp m (h\u03c81 (Real.sqrt m)) hsm.differentiableAt, hsm.deriv]\n ring\n have hA : HasDerivAt (fun n => deriv \u03c8 (Real.sqrt n))\n (deriv (deriv \u03c8) (Real.sqrt n) * (1 / (2 * Real.sqrt n))) n := by\n have h2 : HasDerivAt (deriv \u03c8) (deriv (deriv \u03c8) (Real.sqrt n))\n (Real.sqrt n) :=\n (h\u03c82 (Real.sqrt n)).hasDerivAt\n have h3 := h2.comp n hsqrt\n rwa [show (fun n => deriv \u03c8 (Real.sqrt n)) = deriv \u03c8 \u2218 Real.sqrt from rfl]\n have hB : HasDerivAt (fun n => (2 * Real.sqrt n)\u207b\u00b9)\n (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2) n := by\n have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=\n hsqrt.const_mul 2\n have h2 : (2 * Real.sqrt n) \u2260 0 :=\n mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)\n exact h1.inv h2\n have hmul : HasDerivAt (fun n => deriv \u03c8 (Real.sqrt n) * (2 * Real.sqrt n)\u207b\u00b9)\n (deriv (deriv \u03c8) (Real.sqrt n) * (1 / (2 * Real.sqrt n)) * (2 * Real.sqrt n)\u207b\u00b9 +\n deriv \u03c8 (Real.sqrt n) *\n (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n :=\n hA.mul hB\n have hder := (hmul.congr_of_eventuallyEq hg1).deriv\n rw [hder]\n set s := Real.sqrt n with hsdef\n have hs0 : s \u2260 0 := Real.sqrt_ne_zero'.2 hn\n have hn_eq : n = s ^ 2 := by\n rw [hsdef]; exact (Real.sq_sqrt hn.le).symm\n rw [hn_eq]\n field_simp [hs0]\n ring\n\n/-- [PROVED session 011] The D-057 chain-rule identity behind the\n11-block reduction: with T(n) = \u221an + 1,\nd\u00b2/dn\u00b2 \u03c6(T(n)) = [\u03c6\u2033(T) \u2212 \u03c6\u2032(T)/(T\u22121)] / (4n), written with\n\u221an = T\u22121. (Warm-up proof; first sorry eliminated from the library.) -/\ntheorem chain_rule_sqrt_shift (\u03c6 : \u211d \u2192 \u211d) (h\u03c6 : ContDiff \u211d 2 \u03c6)\n (n : \u211d) (hn : 0 < n) :\n deriv (deriv fun n => \u03c6 (Real.sqrt n + 1)) n =\n (deriv (deriv \u03c6) (Real.sqrt n + 1) -\n deriv \u03c6 (Real.sqrt n + 1) / Real.sqrt n) / (4 * n) := by\n have h\u03c61 : Differentiable \u211d \u03c6 := h\u03c6.differentiable (by norm_num)\n have h\u03c62 : Differentiable \u211d (deriv \u03c6) :=\n (h\u03c6.deriv' (n := 1)).differentiable one_ne_zero\n have hsqrt : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt n)) n :=\n Real.hasDerivAt_sqrt hn.ne'\n have hdiff_sqrt : DifferentiableAt \u211d Real.sqrt n := hsqrt.differentiableAt\n have hdiff_h : DifferentiableAt \u211d (fun n => Real.sqrt n + 1) n :=\n hdiff_sqrt.add (differentiableAt_const 1)\n have hpos : Set.Ioi (0 : \u211d) \u2208 \ud835\udcdd n := Ioi_mem_nhds hn\n have hg1 : deriv (fun n => \u03c6 (Real.sqrt n + 1)) =\u1da0[\ud835\udcdd n]\n fun n => deriv \u03c6 (Real.sqrt n + 1) * (2 * Real.sqrt n)\u207b\u00b9 := by\n filter_upwards [hpos] with m hm\n have hsm : HasDerivAt Real.sqrt (1 / (2 * Real.sqrt m)) m :=\n Real.hasDerivAt_sqrt (ne_of_gt hm)\n have hhm : DifferentiableAt \u211d (fun x => Real.sqrt x + 1) m :=\n hsm.differentiableAt.add (differentiableAt_const 1)\n have h1 : deriv (fun x => Real.sqrt x + 1) m = 1 / (2 * Real.sqrt m) := by\n rw [deriv_add_const]\n exact hsm.deriv\n rw [show (fun x => \u03c6 (Real.sqrt x + 1)) = \u03c6 \u2218 (fun x => Real.sqrt x + 1)\n from rfl,\n deriv_comp m (h\u03c61 (Real.sqrt m + 1)) hhm, h1]\n ring\n have hA : HasDerivAt (fun n => deriv \u03c6 (Real.sqrt n + 1))\n (deriv (deriv \u03c6) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n))) n := by\n have h1 : HasDerivAt (fun x => Real.sqrt x + 1) (1 / (2 * Real.sqrt n)) n :=\n hsqrt.add_const 1\n have h2 : HasDerivAt (deriv \u03c6) (deriv (deriv \u03c6) (Real.sqrt n + 1))\n (Real.sqrt n + 1) :=\n (h\u03c62 (Real.sqrt n + 1)).hasDerivAt\n have h3 := h2.comp n h1\n rwa [show (fun n => deriv \u03c6 (Real.sqrt n + 1)) =\n deriv \u03c6 \u2218 (fun n => Real.sqrt n + 1) from rfl]\n have hB : HasDerivAt (fun n => (2 * Real.sqrt n)\u207b\u00b9)\n (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2) n := by\n have h1 : HasDerivAt (fun n => 2 * Real.sqrt n) (2 * (1 / (2 * Real.sqrt n))) n :=\n hsqrt.const_mul 2\n have h2 : (2 * Real.sqrt n) \u2260 0 :=\n mul_ne_zero two_ne_zero (Real.sqrt_ne_zero'.2 hn)\n exact h1.inv h2\n have hmul : HasDerivAt (fun n => deriv \u03c6 (Real.sqrt n + 1) * (2 * Real.sqrt n)\u207b\u00b9)\n (deriv (deriv \u03c6) (Real.sqrt n + 1) * (1 / (2 * Real.sqrt n)) * (2 * Real.sqrt n)\u207b\u00b9 +\n deriv \u03c6 (Real.sqrt n + 1) *\n (-(2 * (1 / (2 * Real.sqrt n))) / (2 * Real.sqrt n) ^ 2)) n :=\n hA.mul hB\n have hder := (hmul.congr_of_eventuallyEq hg1).deriv\n rw [hder]\n set s := Real.sqrt n with hsdef\n have hs0 : s \u2260 0 := Real.sqrt_ne_zero'.2 hn\n have hn_eq : n = s ^ 2 := by\n rw [hsdef]; exact (Real.sq_sqrt hn.le).symm\n rw [hn_eq]\n field_simp [hs0]\n ring\n\nset_option maxHeartbeats 800000 in\n/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the\n4/3 bracket \u2014 the D-074 dog-leg charges 1.5\u00b7IIMaj, and 1.5/(3n) =\n1/(2n) preserves the convexity slack] IIMaj\u2033(n) < 1/(3n) for n \u2265 20\n(the analytic version of D-057 \u00a73's \"max 2n\u00b7|B\u0303\u2084\u2033| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt_three {n : \u211d} (hn : 20 \u2264 n) :\n deriv (deriv IIMaj) n < 1 / (3 * n) := by\n have hn0 : (0 : \u211d) < n := by linarith\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,\n deriv2_psiTilde]\n have hb := iimaj_bracket_bound (Real.sqrt_le_sqrt hn)\n have h4n : (0 : \u211d) < 4 * n := by linarith\n have e : (1 : \u211d) / (3 * n) = (4 / 3) / (4 * n) := by\n have h1 : (0 : \u211d) < 3 * n := by linarith [hn0]\n have h2 : (0 : \u211d) < 4 * n := by linarith [hn0]\n rw [div_eq_div_iff h1.ne' h2.ne']\n ring\n rw [e]\n exact div_lt_div_of_pos_right hb h4n\n\n/-- [PROVED session 011] Margin convexity (D-057, draft \u00a73.1 Step 4):\nfor any twice-differentiable majorant F of the zero count N(0,T] whose\n\u03c8-block \u03c8[F](T) = F\u2033(T) \u2212 F\u2032(T)/(T\u22121) is negative for T \u2265 \u221a20 + 1\n(the D-057 11-block table discharges this for the explicit Trudgian\nmajorant), the margin majorant margin\u0303 is convex on [20, \u221e).\nProof: margin\u0303\u2033(n) = 1/(2n) \u2212 2\u03c8_F/(4n) \u2212 \u03a3w\u1d62\u03c8\u1d62/(4n) \u2212 IIMaj\u2033(n)\n\u2265 1/(2n) \u2212 IIMaj\u2033(n) > 0 (every \u03c8 < 0 by the block table;\nIIMaj\u2033 < 1/(2n) by IIMaj_deriv2_lt).\nTogether with margin\u0303(8\u00d710\u2074) = 16 020 > 0 and margin\u0303\u2032(8\u00d710\u2074) > 0\n(E-028/E-029) this gives margin > 0 on [8\u00d710\u2074, N\u2081]. -/\ntheorem marginTilde_convex (F : \u211d \u2192 \u211d) (hF : ContDiffOn \u211d 2 F (Set.Ioi 1))\n (h\u03c8 : \u2200 T : \u211d, Real.sqrt 20 + 1 \u2264 T \u2192\n deriv (deriv F) T - deriv F T / (T - 1) < 0) :\n ConvexOn \u211d (Set.Ici 20) (marginTilde F) := by\n have hCDfull : ContDiffOn \u211d 2 (marginTilde F) (Set.Ioi 20) := by\n rw [marginTilde_eq_expanded F]\n exact contDiffOn_marginExpanded F hF\n apply convexOn_of_deriv2_nonneg (convex_Ici 20)\n \u00b7 rw [marginTilde_eq_expanded F]\n exact continuousOn_marginExpanded F hF\n \u00b7 rw [interior_Ici]\n exact hCDfull.differentiableOn (by norm_num)\n \u00b7 rw [interior_Ici]\n exact ((hCDfull.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num))).differentiableOn\n one_ne_zero\n \u00b7 intro n hn\n rw [interior_Ici] at hn\n have hn20 : 20 < n := hn\n have hn0 : (0 : \u211d) < n := by linarith\n have hn4 : (0 : \u211d) < 4 * n := by linarith\n have hTn : Real.sqrt 20 + 1 \u2264 Real.sqrt n + 1 := by\n have h := Real.sqrt_le_sqrt (show (20 : \u211d) \u2264 n by linarith)\n linarith\n -- diff-fact helpers\n have hdd : \u2200 {P : \u211d \u2192 \u211d}, ContDiffOn \u211d 2 P (Set.Ioi 20) \u2192\n DifferentiableAt \u211d (deriv P) n := fun hCD =>\n ((hCD.deriv_of_isOpen (m := 1) isOpen_Ioi (by norm_num)).differentiableOn\n one_ne_zero).differentiableAt (Ioi_mem_nhds hn20)\n have hev : \u2200 {P : \u211d \u2192 \u211d}, ContDiffOn \u211d 2 P (Set.Ioi 20) \u2192\n (\u2200\u1da0 m in \ud835\udcdd n, DifferentiableAt \u211d P m) := fun hCD => by\n filter_upwards [Ioi_mem_nhds hn20] with m hm\n exact (hCD.differentiableOn (by norm_num)).differentiableAt (Ioi_mem_nhds hm)\n -- unweighted composition bundles\n have hCDFc : ContDiffOn \u211d 2 (fun m => F (Real.sqrt m + 1)) (Set.Ioi 20) :=\n hF.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift_Ioi1\n have hCDTL1c : ContDiffOn \u211d 2\n (fun m => (fun t => t * Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_TL1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDTL2c : ContDiffOn \u211d 2\n (fun m => (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_TL2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1sqc : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2) ^ 2) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1L2c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL2sqc : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2sq.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL1c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (t + 2)) (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_L1.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDL2c : ContDiffOn \u211d 2\n (fun m => (fun t => Real.log (Real.log (t + 2))) (Real.sqrt m + 1))\n (Set.Ioi 20) :=\n contDiffOn_L2.comp contDiffOn_sqrt_shift mapsTo_sqrt_shift\n have hCDIIM : ContDiffOn \u211d 2 IIMaj (Set.Ioi 20) := by\n have hId : IIMaj = fun m => psiTilde (Real.sqrt m) :=\n funext fun m => IIMaj_eq_psiTilde_sqrt m\n rw [hId]\n exact (psiTilde_contDiff.contDiffOn).comp\n (contDiffOn_id.sqrt (fun x hx => by\n have h : 20 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x))) (Set.mapsTo_univ _ _)\n -- piece values\n have vS : deriv (deriv fun m => (1/2)*m*Real.log m +\n (lagariasC1 - Real.eulerMascheroniConstant/2)*m - 4) n = 1/(2*n) :=\n marginS_deriv2 _ hn0\n have vF : deriv (deriv (mFblock F)) n =\n (-4) * (psiOf F (Real.sqrt n + 1) / (4 * n)) := by\n unfold mFblock\n rw [deriv2_const_mul (-4) (hdd hCDFc) (hev hCDFc),\n chain_rule_sqrt_shift_on F (le_refl 1) hF n hn0, \u2190 psiOf_sqrt_rel]\n have vTL1 : deriv (deriv mTL1b) n = (-((8/3)*0.6 + 42)) *\n (psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL1b\n rw [deriv2_const_mul _ (hdd hCDTL1c) (hev hCDTL1c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_TL1 n hn0, \u2190 psiOf_sqrt_rel]\n have vTL2 : deriv (deriv mTL2b) n = (-((8/3)*0.886)) *\n (psiOf (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mTL2b\n rw [deriv2_const_mul _ (hdd hCDTL2c) (hev hCDTL2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_TL2 n hn0, \u2190 psiOf_sqrt_rel]\n have vId : deriv (deriv mIdb) n = (-((8/3)*2.7 + 192)) *\n (psiOf id (Real.sqrt n + 1) / (4 * n)) := by\n unfold mIdb\n have hCDidc : ContDiffOn \u211d 2 (fun m => id (Real.sqrt m + 1)) (Set.Ioi 20) :=\n contDiffOn_id.comp contDiffOn_sqrt_shift (Set.mapsTo_univ _ _)\n rw [show (fun m => -(8/3*2.7 + 192) * (Real.sqrt m + 1)) =\n (fun m => -(8/3*2.7 + 192) * id (Real.sqrt m + 1)) from rfl,\n deriv2_const_mul _ (hdd hCDidc) (hev hCDidc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_id n hn0, \u2190 psiOf_sqrt_rel]\n have vL1sq : deriv (deriv mL1sqb) n = (-(42*0.433^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1sqb\n rw [deriv2_const_mul _ (hdd hCDL1sqc) (hev hCDL1sqc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1sq n hn0, \u2190 psiOf_sqrt_rel]\n have vL1L2 : deriv (deriv mL1L2b) n = (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1L2b\n rw [deriv2_const_mul _ (hdd hCDL1L2c) (hev hCDL1L2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1L2 n hn0, \u2190 psiOf_sqrt_rel]\n have vL2sq : deriv (deriv mL2sqb) n = (-(42*0.886^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL2sqb\n rw [deriv2_const_mul _ (hdd hCDL2sqc) (hev hCDL2sqc),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L2sq n hn0, \u2190 psiOf_sqrt_rel]\n have vL1 : deriv (deriv mL1b) n = (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL1b\n rw [deriv2_const_mul _ (hdd hCDL1c) (hev hCDL1c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L1 n hn0, \u2190 psiOf_sqrt_rel]\n have vL2 : deriv (deriv mL2b) n = (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by\n unfold mL2b\n rw [deriv2_const_mul _ (hdd hCDL2c) (hev hCDL2c),\n chain_rule_sqrt_shift_on _ (by norm_num : (-1 : \u211d) \u2264 1) contDiffOn_L2 n hn0, \u2190 psiOf_sqrt_rel]\n have vIIM : deriv (deriv mIIM) n = (-1) * deriv (deriv IIMaj) n := by\n unfold mIIM\n rw [deriv2_const_mul (-1) (hdd hCDIIM) (hev hCDIIM)]\n -- prefix ContDiffOn chain\n have hCD1 := (contDiffOn_mS (lagariasC1 - Real.eulerMascheroniConstant/2)).add\n (contDiffOn_mFblock F hF)\n have hCD2 := hCD1.add contDiffOn_mTL1b\n have hCD3 := hCD2.add contDiffOn_mTL2b\n have hCD4 := hCD3.add contDiffOn_mIdb\n have hCD5 := hCD4.add contDiffOn_mL1sqb\n have hCD6 := hCD5.add contDiffOn_mL1L2b\n have hCD7 := hCD6.add contDiffOn_mL2sqb\n have hCD8 := hCD7.add contDiffOn_mL1b\n have hCD9 := hCD8.add contDiffOn_mL2b\n have hCD10 := hCD9.add contDiffOn_mIIM\n -- split the sum\n rw [marginTilde_eq_expanded F]\n show (0 : \u211d) \u2264 deriv (deriv (marginExpanded F)) n\n unfold marginExpanded\n dsimp only\n rw [deriv2_add (hdd hCD10) (hdd contDiffOn_const) (hev hCD10) (hev contDiffOn_const),\n deriv2_const_val,\n deriv2_add (hdd hCD9) (hdd contDiffOn_mIIM) (hev hCD9) (hev contDiffOn_mIIM), vIIM,\n deriv2_add (hdd hCD8) (hdd contDiffOn_mL2b) (hev hCD8) (hev contDiffOn_mL2b), vL2,\n deriv2_add (hdd hCD7) (hdd contDiffOn_mL1b) (hev hCD7) (hev contDiffOn_mL1b), vL1,\n deriv2_add (hdd hCD6) (hdd contDiffOn_mL2sqb) (hev hCD6) (hev contDiffOn_mL2sqb),\n vL2sq,\n deriv2_add (hdd hCD5) (hdd contDiffOn_mL1L2b) (hev hCD5) (hev contDiffOn_mL1L2b),\n vL1L2,\n deriv2_add (hdd hCD4) (hdd contDiffOn_mL1sqb) (hev hCD4) (hev contDiffOn_mL1sqb),\n vL1sq,\n deriv2_add (hdd hCD3) (hdd contDiffOn_mIdb) (hev hCD3) (hev contDiffOn_mIdb), vId,\n deriv2_add (hdd hCD2) (hdd contDiffOn_mTL2b) (hev hCD2) (hev contDiffOn_mTL2b), vTL2,\n deriv2_add (hdd hCD1) (hdd contDiffOn_mTL1b) (hev hCD1) (hev contDiffOn_mTL1b), vTL1,\n deriv2_add (hdd (contDiffOn_mS _)) (hdd (contDiffOn_mFblock F hF))\n (hev (contDiffOn_mS _)) (hev (contDiffOn_mFblock F hF)), vS, vF]\n -- sign assembly: every \u03c8-term is nonneg\n have h\u03c8n : psiOf F (Real.sqrt n + 1) < 0 := h\u03c8 _ hTn\n have hnn1 : (0 : \u211d) \u2264 -4 * (psiOf F (Real.sqrt n + 1) / (4 * n)) :=\n mul_nonneg_of_nonpos_of_nonpos (by norm_num)\n (div_neg_of_neg_of_pos h\u03c8n hn4).le\n have hnn2 : (0 : \u211d) \u2264 (-((8/3)*0.6 + 42)) *\n (psiOf (fun t => t * Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) :=\n mul_nonneg_of_nonpos_of_nonpos (by norm_num)\n (div_neg_of_neg_of_pos (psiOf_T_mul_log_shift_neg hTn) hn4).le\n have hnn3 : (0 : \u211d) \u2264 (-((8/3)*0.886)) *\n (psiOf (fun t => t * Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) :=\n mul_nonneg_of_nonpos_of_nonpos (by norm_num)\n (div_neg_of_neg_of_pos (psiOf_T_mul_log_log_shift_neg hTn) hn4).le\n have hnn4 : (0 : \u211d) \u2264 (-((8/3)*2.7 + 192)) *\n (psiOf id (Real.sqrt n + 1) / (4 * n)) := by\n have hp : psiOf id (Real.sqrt n + 1) < 0 :=\n (psiOf_id (Real.sqrt n + 1) (by\n have h := Real.sqrt_pos.mpr hn0\n linarith)).2\n exact mul_nonneg_of_nonpos_of_nonpos (by norm_num)\n (div_neg_of_neg_of_pos hp hn4).le\n have hnn5 : (0 : \u211d) \u2264 (-(42*0.433^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n have hw : (-(42*0.433^2*(Real.exp 4 + 1)) : \u211d) \u2264 0 := by\n have hE := Real.exp_pos 4\n nlinarith [hE]\n exact mul_nonneg_of_nonpos_of_nonpos hw\n (div_neg_of_neg_of_pos (psiOf_log_sq_shift_neg hTn) hn4).le\n have hnn6 : (0 : \u211d) \u2264 (-(42*(2*0.433*0.886)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2) * Real.log (Real.log (t + 2)))\n (Real.sqrt n + 1) / (4 * n)) := by\n have hw : (-(42*(2*0.433*0.886)*(Real.exp 4 + 1)) : \u211d) \u2264 0 := by\n have hE := Real.exp_pos 4\n nlinarith [hE]\n exact mul_nonneg_of_nonpos_of_nonpos hw\n (div_neg_of_neg_of_pos (psiOf_log_mul_log_shift_neg hTn) hn4).le\n have hnn7 : (0 : \u211d) \u2264 (-(42*0.886^2*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2)) ^ 2) (Real.sqrt n + 1) / (4 * n)) := by\n have hw : (-(42*0.886^2*(Real.exp 4 + 1)) : \u211d) \u2264 0 := by\n have hE := Real.exp_pos 4\n nlinarith [hE]\n exact mul_nonneg_of_nonpos_of_nonpos hw\n (div_neg_of_neg_of_pos (psiOf_log_log_sq_shift_neg hTn) hn4).le\n have hnn8 : (0 : \u211d) \u2264 (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (t + 2)) (Real.sqrt n + 1) / (4 * n)) := by\n have hw : (-((42*(2*0.433*2.9) + 147)*(Real.exp 4 + 1)) : \u211d) \u2264 0 := by\n have hE := Real.exp_pos 4\n nlinarith [hE]\n exact mul_nonneg_of_nonpos_of_nonpos hw\n (div_neg_of_neg_of_pos (psiOf_log_shift_neg (by\n have h := Real.sqrt_pos.mpr hn0\n linarith)) hn4).le\n have hnn9 : (0 : \u211d) \u2264 (-(42*(2*0.886*2.9)*(Real.exp 4 + 1))) *\n (psiOf (fun t => Real.log (Real.log (t + 2))) (Real.sqrt n + 1) / (4 * n)) := by\n have hw : (-(42*(2*0.886*2.9)*(Real.exp 4 + 1)) : \u211d) \u2264 0 := by\n have hE := Real.exp_pos 4\n nlinarith [hE]\n exact mul_nonneg_of_nonpos_of_nonpos hw\n (div_neg_of_neg_of_pos (psiOf_log_log_shift_neg (by\n have h := Real.sqrt_pos.mpr hn0\n linarith)) hn4).le\n have hIIM := IIMaj_deriv2_lt_three (show 20 \u2264 n by linarith)\n have hbridge : (1 : \u211d) / (3 * n) < 1 / (2 * n) := by\n rw [div_lt_div_iff\u2080 (by linarith [hn0] : (0 : \u211d) < 3 * n)\n (by linarith [hn0] : (0 : \u211d) < 2 * n), one_mul, one_mul]\n linarith [hn0]\n linarith [hIIM, hbridge, hnn1, hnn2, hnn3, hnn4, hnn5, hnn6, hnn7, hnn8, hnn9]\n\n/-! ## 4. Tier (ii) step 1 (session 012): the finite-height Li theorem,\n assembled modulo the single named analytic hypothesis `SfBoundProp`.\n\nDesign (session-012-notes.txt, D-062 triage): the theorem is proved from\n (i) `SfBoundProp` \u2014 the remaining analytic obligation, isolated;\n (ii) the computational perimeter: `RHUpTo` (Platt\u2013Trudgian 2021) and\n `LiVerifiedUpTo` (E-011/E-015 + Misguich\u2013Voros);\n (iii) two elementary evaluations of the explicit margin function\n (E-028/E-029 values, dischargeable by rational interval\n bounds \u2014 tier (ii) step 2).\nThe D-036/D-056 contour estimate, the Trudgian N(T)/S(T) input, and the\nRH-to-height bridge all live INSIDE `SfBoundProp`'s eventual proof, not\nin the assembly below. -/\n\n/-- The explicit zero-count majorant used in the assembly (session 012):\nFAlt(T) = (1/2\u03c0)\u00b7T\u00b7log T + 0.137\u00b7log T + 0.443\u00b7log log T + (7/8 + 1.588).\nThis is Trudgian 2014's F(T) + S_b(T) (F(T) = (T/2\u03c0)log(T/2\u03c0e) + 7/8,\nS_b(T) = 0.137 log T + 0.443 log log T + 1.588) with the negative-weight\nterm \u2212(log 2\u03c0e/2\u03c0)\u00b7T DROPPED, so FAlt \u2265 F + S_b pointwise for T \u2265 0 and\nany literature bound N(T) \u2264 F(T) + S_b(T) upgrades to N(T) \u2264 FAlt(T).\nThe swap is needed because \u03c8[F + S_b] crosses POSITIVE on [5.47, ~16]\n(the dropped term has negative weight against a negative-\u03c8 block), while\nevery FAlt block has provably negative \u03c8 (D-057 rows #1/#3/#4). Margin\ncost: 2\u00b7(log 2\u03c0e/2\u03c0)\u00b7T \u2248 0.9\u221an, negligible vs margin\u0303(8\u00d710\u2074) \u2248 1.6\u00d710\u2074\n(E-028). Domain note: smooth only on (1, \u221e) (log log needs T > 1); the\nmargin composition hits only T = \u221an + 1 \u2265 \u221a20 + 1 > 1. -/\ndef FAlt (T : \u211d) : \u211d :=\n (1 / (2 * Real.pi)) * (T * Real.log T) + 0.137 * Real.log T +\n 0.443 * Real.log (Real.log T) + (7 / 8 + 1.588)\n\n/-- The explicit finite-part bound B(n) (D-037 (4.1) CORRECTED per D-071,\nuser-approved session 038; constants A = 10.5, B\u2080 = 48 from D-056;\n\u0108\u2080/H\u0302/Z\u2082 closed forms; M\u2080 = 1.3352 from E-023; IIMaj the I_I majorant),\nwith the zero-count majorant F as a parameter:\nB(n) = 4F(T) + 4T[(2/3)Z\u2082(T) + 10.5\u00b7log(T+2) + 48] + 40\u00b71.3352\n + 2(e\u2074+1)\u00b7[7H\u0302(T) + 3.3] + IIMaj(n) + 1, T = \u221an + 1.\nThe correction (D-071 F-A/F-B): the bridge is 4F \u2014 the residue sum\n\u03bb_n(T) runs over BOTH signs of \u03b3 (D-036/D-037's 2N(T) was a factor-2\naccounting slip; R-004's theorem is unaffected, see E-030); the I_III\nnear-sum uses the two-unit count (2/3)Z\u2082 (D-069 Finding 2 made exact). -/\ndef Bn (F : \u211d \u2192 \u211d) (n : \u211d) : \u211d :=\n let T := Real.sqrt n + 1\n 4 * F T + 4 * T * ((2 / 3) * Z2hat T + 10.5 * Real.log (T + 2) + 48) +\n 40 * 1.3352 + 2 * (Real.exp 4 + 1) * (7 * Hhat T + 3.3) + IIMaj n + 1\n\n/-- [PROVED session 012] The margin IS sInftyLower \u2212 Bn + 1 (pure\nbookkeeping; same constants as `marginTilde_eq_expanded`). -/\ntheorem marginTilde_eq_sub (F : \u211d \u2192 \u211d) (n : \u211d) :\n marginTilde F n = sInftyLower n - Bn F n + 1 := by\n simp only [marginTilde, Bn, sInftyLower]\n\n/-- The finite part S_f(n) of the Bombieri\u2013Lagarias decomposition\n\u03bb_n = S_\u221e(n) \u2212 S_f(n) + 1 (BL 1999 Thm 2, D-037 P1), here DEFINED by the\nidentity rearranged (\u03bb_n is real by conjugate symmetry, so taking the\nreal part is no loss \u2014 see `LiVerifiedUpTo`). The analytic content \u2014 that\nthis quantity is bounded by B(n) \u2014 is isolated in `SfBoundProp`. -/\ndef Sf (n : \u2115) : \u211d := SInfty n + 1 - (liCoeff n).re\n\n/-- \u2b50 THE named analytic hypothesis of tier (ii): the finite part is\nbounded by the explicit traced B(n) on the whole margin range\n10\u2075 \u2264 n \u2264 N\u2081 = (T\u2080\u22121)\u00b2, T\u2080 = 3\u00d710\u00b9\u00b2.\nProof content (triage D-062): the D-036/D-056 contour estimate \u2014 kernel\nbounds + reference-point R-bound (Mathlib-tractable complex analysis),\nTrudgian 2014 N(T)/S(T) (trusted-perimeter literature candidate), the\nbridge via `RHUpTo` (perimeter), M\u2080 (E-023 grid; E-023b acb optional). -/\ndef SfBoundProp : Prop :=\n \u2200 n : \u2115, 100000 \u2264 n \u2192 (n : \u211d) \u2264 (3 * 10 ^ 12 - 1 : \u211d) ^ 2 \u2192\n |Sf n| \u2264 Bn FAlt (n : \u211d)\n\n/-! ### The \u03c8-blocks of FAlt (D-057 table rows #1/#3/#4) -/\n\n/-- [PROVED session 012] Per-point derivative of T\u00b7log T. -/\ntheorem hasDerivAt_T_mul_log (x : \u211d) (hx : 0 < x) :\n HasDerivAt (fun t => t * Real.log t) (Real.log x + 1) x := by\n have h := (hasDerivAt_id' x).mul (Real.hasDerivAt_log (ne_of_gt hx))\n rwa [one_mul, mul_inv_cancel\u2080 (ne_of_gt hx)] at h\n\n/-- [PROVED session 012] Block #1 (T\u00b7log T): \u03c8-formula. -/\ntheorem psiOf_T_mul_log (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => t * Real.log t) T =\n 1 / T - (Real.log T + 1) / (T - 1) := by\n have hT0 : (0 : \u211d) < T := by linarith\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => t * Real.log t) (Real.log x + 1) x := by\n filter_upwards [eventually_gt_nhds hT0] with x hx\n exact hasDerivAt_T_mul_log x hx\n have h2 : HasDerivAt (fun t => Real.log t + 1) T\u207b\u00b9 T :=\n (Real.hasDerivAt_log (ne_of_gt hT0)).add_const 1\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => t * Real.log t) T = Real.log T + 1 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1, one_div]\n\n/-- [PROVED session 012] Block #1 sign: \u03c8 < 0 for T > 1\n(\u27fa \u22121 < T\u00b7log T, D-057 row #1). -/\ntheorem psiOf_T_mul_log_neg {T : \u211d} (hT : 1 < T) :\n psiOf (fun t => t * Real.log t) T < 0 := by\n rw [psiOf_T_mul_log T hT]\n have hT0 : (0 : \u211d) < T := by linarith\n have hT1 : (0 : \u211d) < T - 1 := by linarith\n have hlog : (0 : \u211d) < Real.log T := Real.log_pos hT\n have key : (1 : \u211d) / T < (Real.log T + 1) / (T - 1) := by\n rw [div_lt_div_iff\u2080 hT0 hT1]\n nlinarith [mul_pos hT0 hlog]\n linarith\n\n/-- [PROVED session 012] Block #3 (log T): \u03c8-formula. -/\ntheorem psiOf_log (T : \u211d) (hT : 1 < T) :\n psiOf Real.log T = -1 / T ^ 2 - 1 / (T * (T - 1)) := by\n have hT0 : (0 : \u211d) < T := by linarith\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt Real.log x\u207b\u00b9 x := by\n filter_upwards [eventually_gt_nhds hT0] with x hx\n exact Real.hasDerivAt_log (ne_of_gt hx)\n have h2 : HasDerivAt (fun t : \u211d => t\u207b\u00b9) (-1 / T ^ 2) T := by\n have h := (hasDerivAt_id' T).inv (ne_of_gt hT0)\n have e : (-(1 : \u211d)) / T ^ 2 = -1 / T ^ 2 := by ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv Real.log T = T\u207b\u00b9 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n field_simp [ne_of_gt hT0, hT1]\n\n/-- [PROVED session 012] Block #3 sign: \u03c8 < 0 for T > 1. -/\ntheorem psiOf_log_neg {T : \u211d} (hT : 1 < T) :\n psiOf Real.log T < 0 := by\n rw [psiOf_log T hT]\n have h1 : (0 : \u211d) < 1 / T ^ 2 := one_div_pos.mpr (pow_pos (by linarith) 2)\n have h2 : (0 : \u211d) < 1 / (T * (T - 1)) :=\n one_div_pos.mpr (mul_pos (by linarith) (by linarith))\n have e : -1 / T ^ 2 - 1 / (T * (T - 1)) = -(1 / T ^ 2 + 1 / (T * (T - 1))) := by ring\n rw [e]\n linarith [add_pos h1 h2]\n\n/-- [PROVED session 012] Per-point derivative of log log T. -/\ntheorem hasDerivAt_log_log_unshifted (x : \u211d) (hx : 1 < x) :\n HasDerivAt (fun t => Real.log (Real.log t)) ((Real.log x)\u207b\u00b9 * x\u207b\u00b9) x := by\n have hin : HasDerivAt Real.log x\u207b\u00b9 x :=\n Real.hasDerivAt_log (ne_of_gt (by linarith : (0 : \u211d) < x))\n have hout : HasDerivAt Real.log (Real.log x)\u207b\u00b9 (Real.log x) :=\n Real.hasDerivAt_log (ne_of_gt (Real.log_pos hx))\n exact hout.comp x hin\n\n/-- [PROVED session 012] Block #4 (log log T): \u03c8-formula. -/\ntheorem psiOf_log_log (T : \u211d) (hT : 1 < T) :\n psiOf (fun t => Real.log (Real.log t)) T =\n -(Real.log T + 1) / ((T * Real.log T) ^ 2) -\n 1 / (T * Real.log T * (T - 1)) := by\n have hT0 : (0 : \u211d) < T := by linarith\n have hL1 : (0 : \u211d) < Real.log T := Real.log_pos hT\n have h1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt (fun t => Real.log (Real.log t))\n ((Real.log x)\u207b\u00b9 * x\u207b\u00b9) x := by\n filter_upwards [eventually_gt_nhds hT] with x hx\n exact hasDerivAt_log_log_unshifted x hx\n have h2 : HasDerivAt (fun t => (Real.log t)\u207b\u00b9 * t\u207b\u00b9)\n (-(Real.log T + 1) / ((T * Real.log T) ^ 2)) T := by\n have hu : HasDerivAt (fun t => (Real.log t)\u207b\u00b9) (-T\u207b\u00b9 / (Real.log T) ^ 2) T :=\n (Real.hasDerivAt_log (ne_of_gt hT0)).inv (ne_of_gt hL1)\n have hv : HasDerivAt (fun t : \u211d => t\u207b\u00b9) (-1 / T ^ 2) T := by\n have h := (hasDerivAt_id' T).inv (ne_of_gt hT0)\n have e : (-(1 : \u211d)) / T ^ 2 = -1 / T ^ 2 := by ring\n rwa [e] at h\n have h := hu.mul hv\n have hT0' : T \u2260 0 := ne_of_gt hT0\n have hL1' : Real.log T \u2260 0 := ne_of_gt hL1\n have e : (-T\u207b\u00b9 / (Real.log T) ^ 2) * T\u207b\u00b9 + (Real.log T)\u207b\u00b9 * (-1 / T ^ 2) =\n -(Real.log T + 1) / ((T * Real.log T) ^ 2) := by\n field_simp [hT0', hL1']\n ring\n rwa [e] at h\n have hd2 := deriv2_of_hasDerivAt_nhds h1 h2\n have hd1 : deriv (fun t => Real.log (Real.log t)) T =\n (Real.log T)\u207b\u00b9 * T\u207b\u00b9 := h1.self_of_nhds.deriv\n unfold psiOf\n rw [hd2, hd1]\n have hT1 : (T - 1) \u2260 0 := by linarith\n have hT0' : T \u2260 0 := ne_of_gt hT0\n have hL1' : Real.log T \u2260 0 := ne_of_gt hL1\n field_simp [hT0', hL1', hT1]\n\n/-- [PROVED session 012] Block #4 sign: \u03c8 < 0 for T > 1. -/\ntheorem psiOf_log_log_neg {T : \u211d} (hT : 1 < T) :\n psiOf (fun t => Real.log (Real.log t)) T < 0 := by\n rw [psiOf_log_log T hT]\n have hT0 : (0 : \u211d) < T := by linarith\n have hL1 : (0 : \u211d) < Real.log T := Real.log_pos hT\n have hp1 : (0 : \u211d) < (Real.log T + 1) / ((T * Real.log T) ^ 2) :=\n div_pos (by linarith) (pow_pos (mul_pos hT0 hL1) 2)\n have hp2 : (0 : \u211d) < 1 / (T * Real.log T * (T - 1)) :=\n one_div_pos.mpr (mul_pos (mul_pos hT0 hL1) (by linarith))\n have e : -(Real.log T + 1) / ((T * Real.log T) ^ 2) -\n 1 / (T * Real.log T * (T - 1)) =\n -((Real.log T + 1) / ((T * Real.log T) ^ 2) +\n 1 / (T * Real.log T * (T - 1))) := by ring\n rw [e]\n linarith [add_pos hp1 hp2]\n\n/-- [PROVED session 012] FAlt is C\u00b2 on (1, \u221e). -/\ntheorem contDiffOn_FAlt : ContDiffOn \u211d 2 FAlt (Set.Ioi 1) := by\n have hA : ContDiffOn \u211d 2 (fun t : \u211d => t * Real.log t) (Set.Ioi 1) :=\n contDiffOn_id.mul (contDiffOn_id.log (fun x hx => by\n have h : 1 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x)))\n have hB : ContDiffOn \u211d 2 Real.log (Set.Ioi 1) :=\n contDiffOn_id.log (fun x hx => by\n have h : 1 < x := hx\n exact ne_of_gt (by linarith : (0 : \u211d) < x))\n have hC : ContDiffOn \u211d 2 (fun t : \u211d => Real.log (Real.log t)) (Set.Ioi 1) :=\n hB.log (fun x hx => ne_of_gt (Real.log_pos hx))\n unfold FAlt\n exact (((contDiffOn_const.mul hA).add (contDiffOn_const.mul hB)).add\n (contDiffOn_const.mul hC)).add contDiffOn_const\n\n/-- [PROVED session 012] \u03c8-condition for FAlt (the D-057 rows #1/#3/#4\nassembly): deriv(deriv FAlt) T \u2212 deriv FAlt T/(T\u22121) < 0 for\nT \u2265 \u221a20 + 1. All three weights positive, all three brackets negative. -/\ntheorem FAlt_psi_neg (T : \u211d) (hT : Real.sqrt 20 + 1 \u2264 T) :\n deriv (deriv FAlt) T - deriv FAlt T / (T - 1) < 0 := by\n have hs : (4.4721 : \u211d) \u2264 Real.sqrt 20 := by\n rw [Real.le_sqrt (by norm_num) (by norm_num)]\n norm_num\n have h1T : 1 < T := by linarith\n have hT0 : (0 : \u211d) < T := by linarith\n have hT1 : (0 : \u211d) < T - 1 := by linarith\n have hL1 : (0 : \u211d) < Real.log T := Real.log_pos h1T\n -- first derivative of FAlt, valid in a neighborhood of T\n have hD1 : \u2200\u1da0 x in \ud835\udcdd T, HasDerivAt FAlt\n ((1 / (2 * Real.pi)) * (Real.log x + 1) + 0.137 * x\u207b\u00b9 +\n 0.443 * ((Real.log x)\u207b\u00b9 * x\u207b\u00b9)) x := by\n filter_upwards [eventually_gt_nhds h1T] with x hx\n have hx0 : (0 : \u211d) < x := by linarith\n have hA := (hasDerivAt_T_mul_log x hx0).const_mul (1 / (2 * Real.pi))\n have hB := (Real.hasDerivAt_log (ne_of_gt hx0)).const_mul (0.137 : \u211d)\n have hC := (hasDerivAt_log_log_unshifted x hx).const_mul (0.443 : \u211d)\n have hK : HasDerivAt (fun _ : \u211d => (7 / 8 + 1.588 : \u211d)) 0 x :=\n hasDerivAt_const x _\n have h := ((hA.add hB).add hC).add hK\n have e : (1 / (2 * Real.pi)) * (Real.log x + 1) + 0.137 * x\u207b\u00b9 +\n 0.443 * ((Real.log x)\u207b\u00b9 * x\u207b\u00b9) + 0 =\n (1 / (2 * Real.pi)) * (Real.log x + 1) + 0.137 * x\u207b\u00b9 +\n 0.443 * ((Real.log x)\u207b\u00b9 * x\u207b\u00b9) := by ring\n rwa [\u2190 e]\n -- second derivative at T\n have hD2 : HasDerivAt\n (fun t => (1 / (2 * Real.pi)) * (Real.log t + 1) + 0.137 * t\u207b\u00b9 +\n 0.443 * ((Real.log t)\u207b\u00b9 * t\u207b\u00b9))\n ((1 / (2 * Real.pi)) * T\u207b\u00b9 + 0.137 * (-1 / T ^ 2) +\n 0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2))) T := by\n have hA := ((Real.hasDerivAt_log (ne_of_gt hT0)).add_const 1).const_mul\n (1 / (2 * Real.pi))\n have hv : HasDerivAt (fun t : \u211d => t\u207b\u00b9) (-1 / T ^ 2) T := by\n have h := (hasDerivAt_id' T).inv (ne_of_gt hT0)\n have e : (-(1 : \u211d)) / T ^ 2 = -1 / T ^ 2 := by ring\n rwa [e] at h\n have hB := hv.const_mul (0.137 : \u211d)\n have hu : HasDerivAt (fun t => (Real.log t)\u207b\u00b9) (-T\u207b\u00b9 / (Real.log T) ^ 2) T :=\n (Real.hasDerivAt_log (ne_of_gt hT0)).inv (ne_of_gt hL1)\n have hC := (hu.mul hv).const_mul (0.443 : \u211d)\n have h := (hA.add hB).add hC\n have hT0' : T \u2260 0 := ne_of_gt hT0\n have hL1' : Real.log T \u2260 0 := ne_of_gt hL1\n have e : (1 / (2 * Real.pi)) * T\u207b\u00b9 + 0.137 * (-1 / T ^ 2) +\n 0.443 * ((-T\u207b\u00b9 / (Real.log T) ^ 2) * T\u207b\u00b9 + (Real.log T)\u207b\u00b9 * (-1 / T ^ 2)) =\n (1 / (2 * Real.pi)) * T\u207b\u00b9 + 0.137 * (-1 / T ^ 2) +\n 0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2)) := by\n field_simp [hT0', hL1']\n ring\n rwa [e] at h\n have hd1 : deriv FAlt T = (1 / (2 * Real.pi)) * (Real.log T + 1) + 0.137 * T\u207b\u00b9 +\n 0.443 * ((Real.log T)\u207b\u00b9 * T\u207b\u00b9) := hD1.self_of_nhds.deriv\n have hd2 : deriv (deriv FAlt) T = (1 / (2 * Real.pi)) * T\u207b\u00b9 +\n 0.137 * (-1 / T ^ 2) + 0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2)) :=\n deriv2_of_hasDerivAt_nhds hD1 hD2\n -- the three negative brackets (reused block signs)\n have hbrA := psiOf_T_mul_log_neg h1T\n rw [psiOf_T_mul_log T h1T] at hbrA\n have hbrB := psiOf_log_neg h1T\n rw [psiOf_log T h1T] at hbrB\n have hbrC := psiOf_log_log_neg h1T\n rw [psiOf_log_log T h1T] at hbrC\n have hc1 : (0 : \u211d) < 1 / (2 * Real.pi) := by positivity\n -- assemble: \u03c8 = c\u2081\u00b7brA + c\u2082\u00b7brB + c\u2083\u00b7brC < 0\n have hT0' : T \u2260 0 := ne_of_gt hT0\n have hL1' : Real.log T \u2260 0 := ne_of_gt hL1\n have hsum : deriv (deriv FAlt) T - deriv FAlt T / (T - 1) =\n (1 / (2 * Real.pi)) * (1 / T - (Real.log T + 1) / (T - 1)) +\n 0.137 * (-1 / T ^ 2 - 1 / (T * (T - 1))) +\n 0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2) -\n 1 / (T * Real.log T * (T - 1))) := by\n rw [hd1, hd2]\n field_simp [hT0', hL1', hT1.ne']\n ring\n rw [hsum]\n have h1 : (1 / (2 * Real.pi)) * (1 / T - (Real.log T + 1) / (T - 1)) < 0 :=\n mul_neg_of_pos_of_neg hc1 hbrA\n have h2' : 0.137 * (-1 / T ^ 2 - 1 / (T * (T - 1))) < 0 :=\n mul_neg_of_pos_of_neg (by norm_num) hbrB\n have h3' : 0.443 * (-(Real.log T + 1) / ((T * Real.log T) ^ 2) -\n 1 / (T * Real.log T * (T - 1))) < 0 :=\n mul_neg_of_pos_of_neg (by norm_num) hbrC\n linarith [h1, h2', h3']\n\n/-- [PROVED session 012] Convexity + positive base point + positive base\nderivative \u27f9 positivity on the whole tail (MVT + monotone derivative). -/\ntheorem pos_of_convex_of_base {f : \u211d \u2192 \u211d} {a N\u2080 x : \u211d}\n (hconv : ConvexOn \u211d (Set.Ici a) f)\n (hdiff : \u2200 y : \u211d, y \u2208 Set.Ioi a \u2192 DifferentiableAt \u211d f y)\n (hN : a < N\u2080) (hx : N\u2080 \u2264 x) (h0 : 0 < f N\u2080) (h0' : 0 < deriv f N\u2080) :\n 0 < f x := by\n rcases eq_or_lt_of_le hx with heq | hlt\n \u00b7 rw [\u2190 heq]\n exact h0\n \u00b7 have hfc : ContinuousOn f (Set.Icc N\u2080 x) :=\n DifferentiableOn.continuousOn (s := Set.Icc N\u2080 x) (f := f) fun y hy =>\n (hdiff y (Set.mem_Ioi.mpr (by\n have h1 : N\u2080 \u2264 y := hy.1\n linarith))).differentiableWithinAt\n have hfd : DifferentiableOn \u211d f (Set.Ioo N\u2080 x) := fun y hy =>\n (hdiff y (Set.mem_Ioi.mpr (by\n have h1 : N\u2080 < y := hy.1\n linarith))).differentiableWithinAt\n obtain \u27e8\u03be, h\u03be, h\u03beeq\u27e9 := exists_deriv_eq_slope f hlt hfc hfd\n have hconv' : ConvexOn \u211d (Set.Ici N\u2080) f :=\n hconv.subset (Set.Ici_subset_Ici.mpr (le_of_lt hN)) (convex_Ici N\u2080)\n have hfd' : \u2200 y : \u211d, y \u2208 Set.Ici N\u2080 \u2192 DifferentiableAt \u211d f y := by\n intro y hy\n have : a < y := by\n have : N\u2080 \u2264 y := hy\n linarith\n exact hdiff y this\n have hmono : deriv f N\u2080 \u2264 deriv f \u03be :=\n (hconv'.monotoneOn_deriv hfd') (Set.mem_Ici.mpr (le_refl N\u2080))\n (Set.mem_Ici.mpr (le_of_lt h\u03be.1)) (le_of_lt h\u03be.1)\n have hpos : (0 : \u211d) < x - N\u2080 := sub_pos.mpr hlt\n have hkey : (0 : \u211d) < (f x - f N\u2080) / (x - N\u2080) :=\n h\u03beeq \u25b8 lt_of_lt_of_le h0' hmono\n have hfx : (0 : \u211d) < f x - f N\u2080 := (div_pos_iff_of_pos_right hpos).mp hkey\n linarith\n\n/-- [PROVED session 012] Convexity + f(N\u2080) > 0 + f(N\u2081) > f(N\u2080) \u27f9\npositivity on [N\u2081, \u221e) (three-chord secant monotonicity; the increasing\nsecant slope is positive, so f keeps climbing). Cheaper to discharge than\nthe derivative base point: two plain evaluations, no deriv machinery. -/\ntheorem pos_of_convex_of_two_points {f : \u211d \u2192 \u211d} {a N\u2080 N\u2081 x : \u211d}\n (hconv : ConvexOn \u211d (Set.Ici a) f)\n (hN : a < N\u2080) (hN01 : N\u2080 < N\u2081) (hx : N\u2081 \u2264 x)\n (h0 : 0 < f N\u2080) (h01 : f N\u2080 < f N\u2081) :\n 0 < f x := by\n rcases eq_or_lt_of_le hx with heq | hlt\n \u00b7 rw [\u2190 heq]\n linarith\n \u00b7 have hslope := hconv.slope_mono_adjacent\n (Set.mem_Ici.mpr (le_of_lt hN)) (Set.mem_Ici.mpr (by linarith)) hN01 hlt\n have hp1 : (0 : \u211d) < N\u2081 - N\u2080 := by linarith\n have hp2 : (0 : \u211d) < x - N\u2081 := by linarith\n have hs : (0 : \u211d) < (f N\u2081 - f N\u2080) / (N\u2081 - N\u2080) := div_pos (by linarith) hp1\n have hs2 : (0 : \u211d) < (f x - f N\u2081) / (x - N\u2081) := lt_of_lt_of_le hs hslope\n have hfx : (0 : \u211d) < f x - f N\u2081 := (div_pos_iff_of_pos_right hp2).mp hs2\n linarith\n\n/-- [PROVED session 012 \u2014 TIER (ii) STEP 1, assembly modulo `SfBoundProp`]\nR-004, the finite-height Li theorem (draft Thm 3.1): assuming the named\nanalytic hypothesis `SfBoundProp`, the computational perimeter\n(Platt\u2013Trudgian RH-to-T\u2080, finite Li verification to 5\u00d710\u2075), and two\nelementary evaluations of the explicit margin function (E-028/E-029\nvalues: margin\u0303(8\u00d710\u2074) \u2248 1.58\u00d710\u2074 > 0 and margin\u0303(10\u2075) \u2248 9.3\u00d710\u2074\n> margin\u0303(8\u00d710\u2074); interval-bound discharge = tier (ii) step 2),\n\u03bb_n > 0 for all n \u2264 (T\u2080\u22121)\u00b2.\n\nProof: for n < 10\u2075 use the perimeter finite verification; for\nn \u2265 10\u2075, \u03bb_n = S_\u221e(n) \u2212 S_f(n) + 1 \u2265 sInftyLower(n) \u2212 B(n) + 1\n= margin\u0303(n) > 0 by convexity (`marginTilde_convex` + `FAlt_psi_neg`)\nand the two base points (`pos_of_convex_of_two_points`).\n`_hRH` documents the bridge input: it is consumed by `SfBoundProp`'s\neventual proof (D-037 \u00a76), not by the assembly itself. -/\ntheorem lambda_pos_finite_height\n (_hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5))\n (hbase : 0 < marginTilde FAlt 80000)\n (hbase2 : marginTilde FAlt 80000 < marginTilde FAlt 100000)\n (hSf : SfBoundProp) :\n \u2200 n : \u2115, 1 \u2264 n \u2192 (n : \u211d) \u2264 (3 * 10 ^ 12 - 1 : \u211d) ^ 2 \u2192\n 0 < (liCoeff n).re := by\n intro n hn1 hnN\n rcases lt_or_ge n 100000 with hlt | hge\n \u00b7 exact hfinite n hn1 (by omega)\n \u00b7 have hn20 : 20 \u2264 n := by omega\n have h1 := sInfty_lower_bound n hn20\n have h2 := hSf n hge hnN\n have h3 : (liCoeff n).re = SInfty n - Sf n + 1 := by\n unfold Sf\n ring\n have h4 : marginTilde FAlt (n : \u211d) = sInftyLower (n : \u211d) - Bn FAlt (n : \u211d) + 1 :=\n marginTilde_eq_sub FAlt n\n have h5 : 0 < marginTilde FAlt (n : \u211d) :=\n pos_of_convex_of_two_points\n (marginTilde_convex FAlt contDiffOn_FAlt FAlt_psi_neg)\n (by norm_num) (by norm_num) (by exact_mod_cast hge) hbase hbase2\n have habs : Sf n \u2264 |Sf n| := le_abs_self _\n rw [h3]\n linarith [h1, h2, h4, h5, habs]\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 2141,
"oldLines": 7,
"newStart": 2141,
"newLines": 7,
"lines": [
" field_simp [hs0]",
" ring",
" ",
"-set_option maxHeartbeats 800000 in",
"+set_option maxHeartbeats 1600000 in",
" /-- [PROVED session 011; strengthened session 040 to 1/(3n) via the",
" 4/3 bracket \u2014 the D-074 dog-leg charges 1.5\u00b7IIMaj, and 1.5/(3n) =",
" 1/(2n) preserves the convexity slack] IIMaj\u2033(n) < 1/(3n) for n \u2265 20"
]
}
],
"userModified": false,
"replaceAll": false
}
tool: Bash
input
{
"command": "cd D:/Python/Quantum/research/lean/NguyenRH1 && export PATH=\"$HOME/.elan/bin:$PATH\" && lake env lean NguyenRH1/LiSkeleton.lean 2>&1 | grep -cE \"error|warning\"; echo \"EXIT: $?\"",
"description": "Rebuild with 1.6M heartbeats",
"timeout": 600000
}
raw content_json (database row)
[{"type":"thinking","thinking":"The diff is clean — exactly my intended changes. The timeouts are in the lt_three's `rw [e]; exact div_lt_div_of_pos_right hb h4n` and marginTilde_convex's final linarith. Since the ORIGINAL proof worked with the same structure (only the e form changed from field_simp to div_eq_div_iff), let me test whether the lt_three's `exact div_lt_div_of_pos_right hb h4n` is the actual loop by reverting JUST that proof to the original e form but keeping the lt_three statement:\n\nActually — hold on. Let me look at the original e more carefully:\nOriginal: `have e : (1 : ℝ) / (2 * n) = 2 / (4 * n) := by field_simp [hn0.ne']; ring` then `rw [e]; exact div_lt_div_of_pos_right hb h4n`.\n\nThe original's `rw [e]` rewrites `1/(2n)` → `2/(4n)` in the GOAL (whose RHS is 1/(2n)) ✓ then exact div_lt_div_of_pos_right hb h4n : HUGE/(4n) < 2/(4n) ✓ — with hb : HUGE < 2 (original) ✓.\n\nMine: e : `1/(3n) = (4/3)/(4n)`; `rw [e]` rewrites `1/(3n)` → `(4/3)/(4n)`; exact div_lt_div_of_pos_right hb h4n : HUGE/(4n) < (4/3)/(4n) — with hb : HUGE < 4/3 ✓.\n\nThe structures are IDENTICAL. The whnf timeout at 800000 suggests the unification of HUGE with the goal's LHS is looping — but the original did the same unification fine?! Unless the iimaj_bracket_bound's PROOF is now broken (the statement change to < 4/3 + the proof's final norm_num — the bracket bound ITSELF is failing to elaborate, leaving hb in a weird state?).\n\nWait — maybe iimaj_bracket_bound ITSELF fails to compile now (statement < 4/3, proof unchanged except the last norm_num) — let me check if iimaj_bracket_bound alone compiles by testing it in isolation... — the whnf timeout at 2166:0 is at the lt_three theorem — if iimaj_bracket_bound failed to elaborate (its own proof), hb would be ill-formed and everything downstream loops. Let me check the build output more carefully for iimaj_bracket_bound's own errors — the error list showed NO error at iimaj_bracket_bound's lines (1498-1678) — only 2166/2191/2399/2777. Hmm — but the earlier error list DID show `1510:52: error: unsolved goals` (the calc.step at the < 4/3 final line) BEFORE I fixed the statement — and I fixed the statement to < 4/3 ✓ — so iimaj_bracket_bound should compile now... unless its norm_num at `< 4/3` leaves an unsolved goal because norm_num evaluates `4.56·1.2237·0.2124·1.1099 < 4/3` as... — my scratch probe PROVED that norm_num handles both comparisons instantly ✓. So iimaj_bracket_bound compiles ✓.\n\nHmm. Let me test the lt_three in isolation in a scratch with a stub iimaj_bracket_bound... — too heavy. Alternative: let me check if the whnf timeout is at `rw [e]` (2162) rather than the exact (2163). The `rw [e]` rewrites `1/(3n)` in the goal `closed-forms < 1/(3n)` — rewriting the RHS to `(4/3)/(4n)` ✓ should be instant.\n\nLet me try a completely different final for lt_three that avoids div_lt_div_of_pos_right's huge unification: prove the chain via mul/div algebra:\n\n```\n rw [hId, chain_rule_sqrt psiTilde psiTilde_contDiff n hn0, deriv_psiTilde,\n deriv2_psiTilde]\n have hbig := iimaj_bracket_bound (Real.sqrt_le_sqrt hn)\n have h4n : (0 : ℝ) < 4 * n := by linarith\n have hdiv := div_lt_div_of_pos_right hbig h4n\n have heq : (1 : ℝ) / (3 * n) = (4 / 3) / (4 * n) := by\n rw [div_eq_div_iff (by linarith [hn0] : (0 : ℝ) < 3 * n).ne'\n (by linarith [hn0] : (0 : ℝ) < 4 * n).ne']\n ring\n rw [heq]\n exact hdiv\n```\nThat's the same thing. The loop must be in `exact hdiv` (or `exact div_lt_div_of_pos_right hb h4n`) unifying `HUGE/(4n)` with the goal's LHS — since the goal's LHS after the rewrites IS HUGE/(4n) syntactically... — hmm wait — is it? chain_rule_sqrt gives `deriv (deriv fun n => ψ (√n)) n = (ψ″(√n) − ψ′(√n)/√n)/(4n)` — with ψ := psiTilde — and then deriv_psiTilde/deriv2_psiTilde rewrite `deriv psiTilde (√n)` and `deriv (deriv psiTilde) (√n)` to the closed forms — but the goal's LHS is `deriv (deriv IIMaj) n` — the first rw [hId] turns IIMaj into `fun m => psiTilde (√m)` — then `chain_rule_sqrt psiTilde psiTilde_contDiff n hn0` rewrites `deriv (deriv fun n => psiTilde (√n)) n` to the chain-rule form ✓ then deriv_psiTilde/deriv2_psiTilde close the derivs ✓ — the final LHS = (deriv2_psiTilde-form(√n) − (deriv_psiTilde-form(√n))/√n)/(4n) — and hbig's HUGE = `4.56·(2·(−iimA·e^{−iimA·√n} − iimB·e^{−iimB·√n}) + (√n+1)·(iimA²·e^{−iimA·√n}+iimB²·e^{−iimB·√n})) − (4.56·((e^{−iimA·√n}+e^{−iimB·√n}) + (√n+1)·(−iimA·e^{−iimA·√n} − iimB·e^{−iimB·√n})))/√n` — the closed deriv forms from deriv_psiTilde/deriv2_psiTilde are EXACTLY these (from lines 1401–1411) ✓ SAME ✓.\n\nSo the exact unification SHOULD be syntactic and instant. The timeout must be environmental or from something else in the elaboration. Let me try compiling the ORIGINAL IIMaj_deriv2_lt (revert just the lt_three to its original form) to see if it compiles — if the ORIGINAL now ALSO times out, something environmental changed (maybe the div_eq_div_iff/div_lt_div_iff₀ fixes aren't the issue but the elaborator state from the many edits).\n\nActually — wait. Let me look at the error at 2191:2 («tactic execution») and 2399:6 more carefully. 2191:2 in the CURRENT file is marginTilde_convex's `intro n hn` — an intro timing out is bizarre. Unless... the elaborator is spending heartbeats from an EARLIER heavy error and each subsequent tactic fails on the residual state. The FIRST error is at 2166:0 — the lt_three. If I fix that, the rest likely clears.\n\nLet me try compiling lt_three's proof with `set_option maxHeartbeats 1600000` (2x the bracket's budget) — if it passes, it's just expensive, not a loop.","signature":""},{"type":"text","text":"Trying 1.6M heartbeats on the lt_three to distinguish expensive-vs-looping."},{"type":"tool_use","id":"Edit_579","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"set_option maxHeartbeats 800000 in\n/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the\n4/3 bracket — the D-074 dog-leg charges 1.5·IIMaj, and 1.5/(3n) =\n1/(2n) preserves the convexity slack] IIMaj″(n) < 1/(3n) for n ≥ 20\n(the analytic version of D-057 §3's \"max 2n·|B̃₄″| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt_three {n : ℝ} (hn : 20 ≤ n) :\n deriv (deriv IIMaj) n < 1 / (3 * n) := by","new_string":"set_option maxHeartbeats 1600000 in\n/-- [PROVED session 011; strengthened session 040 to 1/(3n) via the\n4/3 bracket — the D-074 dog-leg charges 1.5·IIMaj, and 1.5/(3n) =\n1/(2n) preserves the convexity slack] IIMaj″(n) < 1/(3n) for n ≥ 20\n(the analytic version of D-057 §3's \"max 2n·|B̃₄″| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt_three {n : ℝ} (hn : 20 ≤ n) :\n deriv (deriv IIMaj) n < 1 / (3 * n) := by"},"extra_content":null},{"type":"tool_use","id":"Bash_580","name":"Bash","input":{"command":"cd D:/Python/Quantum/research/lean/NguyenRH1 && export PATH=\"$HOME/.elan/bin:$PATH\" && lake env lean NguyenRH1/LiSkeleton.lean 2>&1 | grep -cE \"error|warning\"; echo \"EXIT: $?\"","description":"Rebuild with 1.6M heartbeats","timeout":600000},"extra_content":null}]