← Session 3 — Project kickoff: RH blueprint, staged workflow + archive design
thinking (214 chars)
User asks "what happen?" — they saw activity but no summary. I wrote D-011 but didn't finish the closeout (index updates, commit) or report. Give a brief plain-language update and complete the bookkeeping + commit.
Sorry — I dove deep into the analysis and didn't report. Here's where we are:
**Task 1.3 analysis is done** (written to `D-011`, not yet committed). Three findings:
1. **The wall is precisely located.** The third moment tr G̃³ becomes unconditionally available only when the bandwidth parameter λ ≤ 2/3 (Rudnick–Sarnak range) — but at reduced bandwidth λ, the matrix has dimension λ·N, so any certificate is capped at λ. The moment becomes available *exactly* where it stops helping: λ = 2/3. That's the sharpest form of why "higher moments add nothing."
2. **But I found a hole in that wall.** The dimension cap assumes the grid is at "critical density." I verified from Lemma 2.1's proof that an *oversampled* grid (denser by factor q) keeps the key identity exact — moving the cap from 2/3 to q·(2/3) > 1. Whether the extra dimensions carry real spectral information or are just padding is **decidable numerically** on the sine-process model.
3. **E-005 designed** to settle it: compute the moments of the oversampled, reduced-bandwidth Gram matrix on simulated GUE spectra and run the 3-moment bound. Positive result → a genuine theorem path past 2/3. Negative → another clean, citable obstruction (G-002).
Let me finish the bookkeeping and commit, then I'll ask before running E-005.
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\derivations\\index.md",
"old_string": "| D-010 | Thread T1: sine moments m_k(1) + Christoffel \u039b\u2082(0) reproduced | 1.3 warm-up | complete | 2026-08-17 |",
"new_string": "| D-010 | Thread T1: sine moments m_k(1) + Christoffel \u039b\u2082(0) reproduced | 1.3 warm-up | complete | 2026-08-17 |\n| D-011 | Task 1.3: third-moment analysis; RS wall at \u03bb=2/3 + oversampling hatch | 1.3 | analysis complete | 2026-08-17 |"
}
result 2026-08-17 21:10:00Z → 2026-08-29 00:12:29Z
{
"filePath": "D:\\Python\\quantum-deploy\\docroot\\app.cgi",
"oldString": "from rhweb.wsgi import application\n\n\nfrom urllib.parse import unquote_to_bytes",
"newString": "from rhweb.wsgi import application\n\n_dbg(\"AFTER-IMPORT PATH_INFO=\" + repr(os.environ.get(\"PATH_INFO\")))\n\nfrom urllib.parse import unquote_to_bytes",
"originalFile": "#!/opt/alt/python311/bin/python3.11\n\"\"\"WSGI->CGI adapter \u2014 runs the RH-WEBSITE Django app on Apache shared hosting.\n\nApache rewrites every non-file request to /app.cgi/<path> (see .htaccess).\nwsgiref's CGIHandler bridges the CGI environment onto Django's WSGI app.\n\"\"\"\nimport os\nimport sys\n\nDOCROOT = os.path.dirname(os.path.abspath(__file__))\nAPP = os.path.join(DOCROOT, \"app\")\n\n\ndef _dbg(msg):\n if \"resources\" in (os.environ.get(\"PATH_INFO\") or \"\"):\n with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",\n encoding=\"utf-8\") as fh:\n fh.write(msg + \"\\n\")\n\n\n_dbg(\"TOP fsenc=\" + sys.getfilesystemencoding()\n + \" PATH_INFO=\" + repr(os.environ.get(\"PATH_INFO\")))\n\n# Vendored pure-Python deps (Django 5.2, markdown) + the project package.\nsys.path.insert(0, os.path.join(APP, \"vendor\"))\nsys.path.insert(0, os.path.join(APP, \"web\"))\n\nos.environ.setdefault(\"DJANGO_SETTINGS_MODULE\", \"rhweb.settings\")\n# Apache mounts us at /app.cgi/<path>; present clean root URLs to Django.\nos.environ[\"SCRIPT_NAME\"] = \"\"\n\nfrom wsgiref.handlers import CGIHandler\n\nfrom rhweb.wsgi import application\n\n\nfrom urllib.parse import unquote_to_bytes\n\n\ndef _pep3333_paths(environ, start_response):\n \"\"\"Normalize Apache's path vars to the PEP 3333 form Django needs.\n\n Apache hands these vars either percent-encoded (mod_rewrite path)\n or UTF-8-decoded (direct CGI path). Django (a) crashes with\n UnicodeEncodeError on any non-latin-1 char (500) and (b) needs the\n decoded path for URL resolution (else the resolver sees %XX and 404s).\n So: bytes -> unquote -> re-mangle as latin-1. SCRIPT_URL/REDIRECT_URL\n (set by mod_rewrite) are consulted by get_script_name BEFORE\n PATH_INFO \u2014 all three must be normalized.\"\"\"\n for key in (\"PATH_INFO\", \"SCRIPT_URL\", \"REDIRECT_URL\"):\n v = environ.get(key)\n if v:\n raw = unquote_to_bytes(v) # %XX-decodes; utf-8-encodes str first\n environ[key] = raw.decode(\"latin-1\")\n if \"resources\" in (environ.get(\"PATH_INFO\") or \"\"):\n with open(os.path.join(APP, \"debug-environ.txt\"), \"a\",\n encoding=\"utf-8\") as fh:\n fh.write(repr({k: environ.get(k) for k in\n (\"PATH_INFO\", \"SCRIPT_NAME\", \"SCRIPT_URL\",\n \"REDIRECT_URL\", \"REQUEST_METHOD\", \"HTTP_HOST\")})\n + \"\\n\")\n try:\n from django.core.handlers.wsgi import WSGIRequest\n req = WSGIRequest(dict(environ))\n fh.write(\"path_info=\" + repr(req.path_info) + \"\\n\")\n from django.urls import resolve\n m = resolve(req.path_info)\n fh.write(\"match=\" + repr(m.kwargs) + \"\\n\")\n except Exception as e: # noqa: BLE001\n fh.write(\"ERR \" + repr(e) + \"\\n\")\n try:\n raw = open(\"/proc/self/environ\", \"rb\").read()\n for entry in raw.split(b\"\\x00\"):\n if entry.startswith((b\"PATH_INFO=\", b\"SCRIPT_URL=\")):\n fh.write(\"ENVBYTES \" + repr(entry) + \"\\n\")\n except Exception as e: # noqa: BLE001\n fh.write(\"ENVBYTES ERR \" + repr(e) + \"\\n\")\n return application(environ, start_response)\n\n\nCGIHandler().run(_pep3333_paths)\n",
"structuredPatch": [
{
"oldStart": 33,
"oldLines": 6,
"newStart": 33,
"newLines": 7,
"lines": [
" ",
" from rhweb.wsgi import application",
" ",
"+_dbg(\"AFTER-IMPORT PATH_INFO=\" + repr(os.environ.get(\"PATH_INFO\")))",
" ",
" from urllib.parse import unquote_to_bytes",
" "
]
}
],
"userModified": false,
"replaceAll": false
}
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\STATE.md",
"old_string": "## NEXT ACTION\nTask 1.3 proper: quantify exactly what the diagonal method gives for\ntr G\u0303\u00b3 at X \u224d T and where it fails (D-010 \u00a76 sets the question; D-004 \u00a75\nhas the k=2 machinery). Then 1.4 and 1.2 (SDP tooling).\nDONE Phase 1: 1.1 \u2192 D-009 (T3 closed); T1 warm-up \u2192 D-010 + E-004\n(moments 1,4/3,2,13/4 confirmed by Monte Carlo; \u039b\u2082(0)=5/36 verified by\nhand; limiting density = near-uniform perturbation on [0,2]; paper\n\"+O(L)\" erratum noted).\nGRAVEYARD: G-001 (Idea C, s\u2082/p substitution symmetry).",
"new_string": "## NEXT ACTION\nRun E-005 (designed in D-011 \u00a74): sine-process moments m\u2081,m\u2082,m\u2083(\u03bb,q) for\n\u03bb-bandwidth q-oversampled sinc-Gram matrices; 3-moment Markov bound;\nscan \u03bb \u2208 [1/2,1], q \u2208 {1,2}. DECIDES: any configuration beating 2/3 with\nan unconditional third moment (\u03bb \u2264 2/3)? Yes \u2192 theorem path (make tr G\u0303\u00b3\nrigorous at that \u03bb). No \u2192 G-002 with exact obstruction.\nDONE Phase 1: 1.1 \u2192 D-009 (T3 closed); T1 \u2192 D-010+E-004; 1.3 analysis \u2192\nD-011 (RS wall located exactly: \u03bb_availability = 2/3 = certificate cap;\noversampling hatch found, needs E-005).\nGRAVEYARD: G-001 (Idea C, s\u2082/p substitution symmetry)."
}
result 2026-08-17 21:10:00Z → 2026-08-25 05:05:33Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
"oldString": " simp only [marginTilde, marginExpanded, mFblock, mTL1b, mTL2b, mIdb, mL1sqb,\n mL1L2b, mL2sqb, mL1b, mL2b, mIIM, mK, Hhat, C0hat]\n ring",
"newString": " simp only [marginTilde, marginExpanded, mFblock, mTL1b, mTL2b, mIdb, mL1sqb,\n mL1L2b, mL2sqb, mL1b, mL2b, mIIM, mK, Hhat, C0hat, Z2hat]\n ring",
"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] The B\u0303\u2084 bracket bound (D-057 \u00a73): for s \u2265 \u221a20,\n\u03c8\u0303\u2033(s) \u2212 \u03c8\u0303\u2032(s)/s < 2. 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.316 < 2. -/\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 < 2 := 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 _ < 2 := 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]\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 (-2))).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\n/-- [PROVED session 011] IIMaj\u2033(n) < 1/(2n) for n \u2265 20 (the analytic\nversion of D-057 \u00a73's \"max 2n\u00b7|B\u0303\u2084\u2033| = 0.189 < 1\"). -/\ntheorem IIMaj_deriv2_lt {n : \u211d} (hn : 20 \u2264 n) :\n deriv (deriv IIMaj) n < 1 / (2 * 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) / (2 * n) = 2 / (4 * n) := by\n field_simp [hn0.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 (show 20 \u2264 n by linarith)\n linarith [hIIM, 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": 1843,
"oldLines": 7,
"newStart": 1843,
"newLines": 7,
"lines": [
" marginTilde F = marginExpanded F := by",
" funext n",
" simp only [marginTilde, marginExpanded, mFblock, mTL1b, mTL2b, mIdb, mL1sqb,",
"- mL1L2b, mL2sqb, mL1b, mL2b, mIIM, mK, Hhat, C0hat]",
"+ mL1L2b, mL2sqb, mL1b, mL2b, mIIM, mK, Hhat, C0hat, Z2hat]",
" ring",
" ",
" /-- [PROVED session 011] The pieces are C\u00b2 on (20, \u221e). -/"
]
}
],
"userModified": false,
"replaceAll": false
}
tool: Edit ok
input
{
"replace_all": false,
"file_path": "D:\\Python\\Quantum\\research\\journal\\session-001.md",
"old_string": "**Outcome:** T1 closed. Ready for task 1.3 proper (third-moment diagonal\nmethod failure analysis).",
"new_string": "**Outcome:** T1 closed. Ready for task 1.3 proper (third-moment diagonal\nmethod failure analysis).\n\n---\n\n## Addendum 13 \u2014 Task 1.3 analysis completed (same day)\n\n**Task:** What fragment of the third moment survives unconditionally? \u2192 D-011.\n\n**Derivation chain:**\n1. tr G\u0303\u00b3 reduces (via Lemma 2.1) to a triple zero-correlation with\n band-limited kernel \u03a6(\u03b3\u2081\u2212\u03b3\u2082)\u03a6(\u03b3\u2082\u2212\u03b3\u2083)\u03a6(\u03b3\u2083\u2212\u03b3\u2081). [VERIFIED algebra]\n2. Prime side: diagonal method needs shift-correlations of THREE P_X's;\n off-diagonal control via MV costs ~X\u00b2/T \u27f9 Rudnick\u2013Sarnak X\u00b3 \u2264 T^{2\u2212\u03b5}\n \u27fa \u03bb \u2264 2/3. (k=2 works at \u03bb=1 only because of the 1/(2\u03c0)\u00b2 margin.)\n3. THE WALL, precisely: at bandwidth \u03bb the grid has d = \u03bbN rows \u27f9\n certificate \u2264 \u03bb; third moment available only at \u03bb \u2264 2/3. Availability\n and usefulness thresholds coincide EXACTLY at 2/3.\n4. THE HATCH (open): Lemma 2.1's no-aliasing needs only\n supp(\u03d5\u2217\u03d5) \u2282 (\u22122\u03c0/h, 2\u03c0/h) \u2014 an oversampled grid h = 2\u03c0/(qL\u2032), q \u2265 1,\n keeps Poisson\u2013Gabor EXACT (verified against the proof's H-support\n argument). At q=2, \u03bb=2/3: d = 4N/3 \u2014 the dimension cap evaporates.\n Whether the extra rank is spectrally real or empty padding is\n numerically decidable on the sine-process model \u2192 E-005 designed\n (scan \u03bb \u2208 [1/2,1], q \u2208 {1,2}, 3-moment Markov bound).\n\n**Outcome:** 1.3 analysis complete. E-005 is the decider: positive \u2192\ntheorem path past 2/3 (unconditional!); negative \u2192 G-002 with exact\nobstruction. Awaiting user go-ahead for E-005."
}
result 2026-08-17 21:10:00Z → 2026-08-26 05:33:16Z
{
"filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
"oldString": " rw [norm_div, hnormA, hnormB, \u2190 Real.sqrt_div hQpos]",
"newString": " rw [norm_div, hnormA, hnormB,\n \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]",
"originalFile": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n DifferentiableAt \u2102 (Jlag n) s := by\n apply Jlag_differentiableAt\n \u00b7 rintro rfl\n simp at him\n \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n intro s hs\n rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n HIntegral (Jlag n) 3 XR T =\n HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n VIntegral (Jlag n) 3 T U := by\n have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR\n unfold RectangleIntegral at h0\n rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n unfold kFun\n simp [map_sub, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n (starRingEnd \u2102) (deriv riemannZeta s) := by\n have h := iteratedDeriv_riemannZeta_conj 1 hs\n rwa [iteratedDeriv_one] at h\n unfold Jlag\n rw [kFun_conj, _root_.riemannZeta_conj, h1]\n simp only [map_mul, map_neg, map_div\u2080]\n\n/-! ## 3. The left-lift bound (DL-2, D-074 \u00a73.3 V_left) -/\n\n/-- **Kernel on the lift**: \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2\n(D-074 \u00a76: |(3+it)/(2+it)|\u00b2 = (9+t\u00b2)/(4+t\u00b2) = 1 + 5/(4+t\u00b2), whose n-th\npower is \u2264 e^{5n/(2(4+t\u00b2))} \u2264 e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : \u2115} {t : \u211d}\n (hT : (n : \u211d) \u2264 t ^ 2) :\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp (5 / 2) + 1 := by\n rcases Nat.eq_zero_or_pos n with hn | hn\n \u00b7 subst hn\n simp only [kFun, pow_zero, sub_self, norm_zero]\n positivity\n \u00b7 have hnR : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n have ht2 : (0 : \u211d) < 4 + t ^ 2 := by positivity\n have hn4t2 : (n : \u211d) \u2264 4 + t ^ 2 := by linarith [hT]\n have hQpos : (0 : \u211d) \u2264 (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n have hQle : (9 + t ^ 2) / (4 + t ^ 2) \u2264 Real.exp (5 / (n : \u211d)) := by\n have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n field_simp [ht2.ne']\n ring\n rw [h1]\n have h2 : 5 / (4 + t ^ 2) \u2264 5 / (n : \u211d) :=\n (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n have h3 := Real.add_one_le_exp (5 / (n : \u211d))\n linarith\n have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 Real.exp 5 := by\n calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 (Real.exp (5 / (n : \u211d))) ^ n :=\n pow_le_pow_left\u2080 hQpos hQle n\n _ = Real.exp 5 := by\n rw [\u2190 Real.exp_nat_mul]\n congr 1\n have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n field_simp [hn0]\n have hns3 : Complex.normSq ((3 : \u211d) + t * Complex.I) = 9 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hns2 : Complex.normSq ((2 : \u211d) + t * Complex.I) = 4 + t ^ 2 := by\n simp [Complex.normSq_apply]\n ring\n have hnormA : \u2016((3 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (9 + t ^ 2) := by\n have h1 : \u2016((3 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((3 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns3]\n have hnormB : \u2016((2 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (4 + t ^ 2) := by\n have h1 : \u2016((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt (Complex.normSq ((2 : \u211d) + t * Complex.I)) := by\n rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n rw [h1, hns2]\n have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =\n Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n rw [norm_div, hnormA, hnormB, \u2190 Real.sqrt_div hQpos]\n have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by\n push_cast\n ring\n unfold kFun\n rw [hs1]\n calc \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n - 1\u2016\n \u2264 \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n norm_sub_le _ _\n _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n rw [norm_pow, hnorm, norm_one]\n _ \u2264 Real.exp (5 / 2) + 1 := by\n have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n \u2264 Real.exp (5 / 2) := by\n have hx0 : (0 : \u211d) \u2264 Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=\n Real.sqrt_nonneg _\n have hx : (0 : \u211d) \u2264 (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=\n pow_nonneg hx0 n\n have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 \u2264 Real.exp 5 := by\n have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =\n ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by\n rw [\u2190 pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]\n rw [e]\n exact hQn\n have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =\n Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by\n rw [Real.sqrt_sq hx]\n rw [h8]\n calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)\n \u2264 Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5\n _ = Real.exp (5 / 2) := by rw [Real.sqrt_exp]\n linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : \u211d :=\n \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016\n\n/-- Termwise 3-vs-2 comparison for the \u039b L-series: \u039b(n)/n\u00b3 \u2264 (1/2)\u00b7\u039b(n)/n\u00b2. -/\nlemma norm_term_vonMangoldt_three_le_half (n : \u2115) :\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 \u2264\n (1 / 2) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 := by\n have h3re : ((3 : \u2102).re) = 3 := rfl\n have h2re : ((2 : \u2102).re) = 2 := rfl\n simp only [LSeries.norm_term_eq, h3re, h2re]\n split\n \u00b7 norm_num\n \u00b7 next hn =>\n rcases eq_or_ne n 1 with rfl | hn1\n \u00b7 simp [ArithmeticFunction.vonMangoldt_one]\n \u00b7 have hn2 : 2 \u2264 n := by omega\n have h\u039b : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016 =\n ArithmeticFunction.vonMangoldt n := by\n rw [Complex.norm_eq_abs, \u2190 Real.norm_eq_abs,\n Real.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg]\n rw [h\u039b]\n have e : ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ 3 =\n (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ 2) := by\n field_simp [show (n : \u211d) \u2260 0 by positivity]\n ring\n rw [e]\n apply mul_le_mul_of_nonneg_right _ (by positivity)\n rw [div_le_div_iff_of_pos_left (by norm_num : (0 : \u211d) < 1)\n (by norm_num : (0 : \u211d) < 2) (by positivity : (0 : \u211d) < (n : \u211d))]\n exact_mod_cast hn2\n\n/-- dirichletC3 \u2264 1/2 (the termwise comparison + dirichletC2 \u2264 1) \u2014\nthe certified C_zeta3 = 0.5 of D-074 \u00a74. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 \u2264 1 / 2 := by\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsum2 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n calc dirichletC3\n = \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 := rfl\n _ \u2264 \u2211' n : \u2115, (1 / 2) *\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n (hsum2.mul_left (1 / 2))\n _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n _ \u2264 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 dirichletC3 for re s \u2265 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC3 := by\n have hs1 : (1 : \u211d) < s.re := by linarith\n have h1 : -logDeriv riemannZeta s\n = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n rw [logDeriv, Pi.div_apply, h2]\n ring\n have hsum3 : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n have hsumS : Summable (fun n : \u2115 =>\n \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n rw [summable_norm_iff]\n exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n \u2264 dirichletC3 := by\n show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n norm_tsum_le_tsum_norm hsumS\n _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 :=\n Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n simp\n exact hs) n) hsumS hsum3\n _ = dirichletC3 := rfl\n calc \u2016logDeriv riemannZeta s\u2016\n = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n rw [\u2190 h1, norm_neg]\n _ \u2264 dirichletC3 := hle\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : \u2102} (hs : 3 \u2264 s.re) :\n \u2016logDeriv riemannZeta s\u2016 \u2264 1 / 2 :=\n (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 \u00a73.3 V_left): for 0 < T \u2264 U and\nn \u2264 T\u00b2, \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U \u2212 T)\u00b7(e^{5/2}+1)/2. The kernel\n\u2264 e^{5/2}+1 (the 1+5/(4+t\u00b2) computation), the zeta factor \u2264 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : \u2115} {T U : \u211d}\n (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n have hnorm : \u2016VIntegral (Jlag n) 3 T U\u2016 =\n \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 := by\n unfold VIntegral\n rw [norm_smul, Complex.norm_I, one_mul]\n rw [hnorm]\n have hbound : \u2200 t \u2208 Set.Ioc T U,\n \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 (Real.exp (5 / 2) + 1) * (1 / 2) := by\n intro t ht\n have htT : T < t := ht.1\n have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n have hre : (3 : \u211d) \u2264 ((3 : \u211d) + t * Complex.I).re := by simp\n have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n have h2 := norm_logDeriv_zeta_le_half (s := (3 : \u211d) + t * Complex.I) hre\n have hnorm3 : \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 =\n \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 *\n \u2016logDeriv riemannZeta ((3 : \u211d) + t * Complex.I)\u2016 := by\n show \u2016kFun n ((3 : \u211d) + t * Complex.I) *\n (-logDeriv riemannZeta ((3 : \u211d) + t * Complex.I))\u2016 = _\n rw [norm_mul, norm_neg]\n rw [hnorm3]\n exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n have hint : \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264\n ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n apply intervalIntegral.norm_integral_le_of_norm_le_const\n intro t ht\n rw [Set.uIoc_of_le hTU] at ht\n exact hbound t ht\n have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n rw [habs] at hint\n calc \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016\n \u2264 ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\nend NguyenRH1\n\nend\n",
"structuredPatch": [
{
"oldStart": 162,
"oldLines": 7,
"newStart": 162,
"newLines": 8,
"lines": [
" rw [h1, hns2]",
" have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =",
" Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by",
"- rw [norm_div, hnormA, hnormB, \u2190 Real.sqrt_div hQpos]",
"+ rw [norm_div, hnormA, hnormB,",
"+ \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]",
" have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by",
" push_cast",
" ring"
]
}
],
"userModified": false,
"replaceAll": false
}
raw content_json (database row)
[{"type":"thinking","thinking":"User asks \"what happen?\" — they saw activity but no summary. I wrote D-011 but didn't finish the closeout (index updates, commit) or report. Give a brief plain-language update and complete the bookkeeping + commit.","signature":""},{"type":"text","text":"Sorry — I dove deep into the analysis and didn't report. Here's where we are:\n\n**Task 1.3 analysis is done** (written to `D-011`, not yet committed). Three findings:\n\n1. **The wall is precisely located.** The third moment tr G̃³ becomes unconditionally available only when the bandwidth parameter λ ≤ 2/3 (Rudnick–Sarnak range) — but at reduced bandwidth λ, the matrix has dimension λ·N, so any certificate is capped at λ. The moment becomes available *exactly* where it stops helping: λ = 2/3. That's the sharpest form of why \"higher moments add nothing.\"\n\n2. **But I found a hole in that wall.** The dimension cap assumes the grid is at \"critical density.\" I verified from Lemma 2.1's proof that an *oversampled* grid (denser by factor q) keeps the key identity exact — moving the cap from 2/3 to q·(2/3) > 1. Whether the extra dimensions carry real spectral information or are just padding is **decidable numerically** on the sine-process model.\n\n3. **E-005 designed** to settle it: compute the moments of the oversampled, reduced-bandwidth Gram matrix on simulated GUE spectra and run the 3-moment bound. Positive result → a genuine theorem path past 2/3. Negative → another clean, citable obstruction (G-002).\n\nLet me finish the bookkeeping and commit, then I'll ask before running E-005."},{"type":"tool_use","id":"Edit_209","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\derivations\\index.md","old_string":"| D-010 | Thread T1: sine moments m_k(1) + Christoffel Λ₂(0) reproduced | 1.3 warm-up | complete | 2026-08-17 |","new_string":"| D-010 | Thread T1: sine moments m_k(1) + Christoffel Λ₂(0) reproduced | 1.3 warm-up | complete | 2026-08-17 |\n| D-011 | Task 1.3: third-moment analysis; RS wall at λ=2/3 + oversampling hatch | 1.3 | analysis complete | 2026-08-17 |"},"extra_content":null},{"type":"tool_use","id":"Edit_210","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\STATE.md","old_string":"## NEXT ACTION\nTask 1.3 proper: quantify exactly what the diagonal method gives for\ntr G̃³ at X ≍ T and where it fails (D-010 §6 sets the question; D-004 §5\nhas the k=2 machinery). Then 1.4 and 1.2 (SDP tooling).\nDONE Phase 1: 1.1 → D-009 (T3 closed); T1 warm-up → D-010 + E-004\n(moments 1,4/3,2,13/4 confirmed by Monte Carlo; Λ₂(0)=5/36 verified by\nhand; limiting density = near-uniform perturbation on [0,2]; paper\n\"+O(L)\" erratum noted).\nGRAVEYARD: G-001 (Idea C, s₂/p substitution symmetry).","new_string":"## NEXT ACTION\nRun E-005 (designed in D-011 §4): sine-process moments m₁,m₂,m₃(λ,q) for\nλ-bandwidth q-oversampled sinc-Gram matrices; 3-moment Markov bound;\nscan λ ∈ [1/2,1], q ∈ {1,2}. DECIDES: any configuration beating 2/3 with\nan unconditional third moment (λ ≤ 2/3)? Yes → theorem path (make tr G̃³\nrigorous at that λ). No → G-002 with exact obstruction.\nDONE Phase 1: 1.1 → D-009 (T3 closed); T1 → D-010+E-004; 1.3 analysis →\nD-011 (RS wall located exactly: λ_availability = 2/3 = certificate cap;\noversampling hatch found, needs E-005).\nGRAVEYARD: G-001 (Idea C, s₂/p substitution symmetry)."},"extra_content":null},{"type":"tool_use","id":"Edit_211","name":"Edit","input":{"replace_all":false,"file_path":"D:\\Python\\Quantum\\research\\journal\\session-001.md","old_string":"**Outcome:** T1 closed. Ready for task 1.3 proper (third-moment diagonal\nmethod failure analysis).","new_string":"**Outcome:** T1 closed. Ready for task 1.3 proper (third-moment diagonal\nmethod failure analysis).\n\n---\n\n## Addendum 13 — Task 1.3 analysis completed (same day)\n\n**Task:** What fragment of the third moment survives unconditionally? → D-011.\n\n**Derivation chain:**\n1. tr G̃³ reduces (via Lemma 2.1) to a triple zero-correlation with\n band-limited kernel Φ(γ₁−γ₂)Φ(γ₂−γ₃)Φ(γ₃−γ₁). [VERIFIED algebra]\n2. Prime side: diagonal method needs shift-correlations of THREE P_X's;\n off-diagonal control via MV costs ~X²/T ⟹ Rudnick–Sarnak X³ ≤ T^{2−ε}\n ⟺ λ ≤ 2/3. (k=2 works at λ=1 only because of the 1/(2π)² margin.)\n3. THE WALL, precisely: at bandwidth λ the grid has d = λN rows ⟹\n certificate ≤ λ; third moment available only at λ ≤ 2/3. Availability\n and usefulness thresholds coincide EXACTLY at 2/3.\n4. THE HATCH (open): Lemma 2.1's no-aliasing needs only\n supp(ϕ∗ϕ) ⊂ (−2π/h, 2π/h) — an oversampled grid h = 2π/(qL′), q ≥ 1,\n keeps Poisson–Gabor EXACT (verified against the proof's H-support\n argument). At q=2, λ=2/3: d = 4N/3 — the dimension cap evaporates.\n Whether the extra rank is spectrally real or empty padding is\n numerically decidable on the sine-process model → E-005 designed\n (scan λ ∈ [1/2,1], q ∈ {1,2}, 3-moment Markov bound).\n\n**Outcome:** 1.3 analysis complete. E-005 is the decider: positive →\ntheorem path past 2/3 (unconditional!); negative → G-002 with exact\nobstruction. Awaiting user go-ahead for E-005."},"extra_content":null}]