Message #687 · Riemann Hypothesis Research

← Session 17 — Lean tier (i): elementary proofs (after crash)

#687 assistant 2026-08-20 07:24:21.556 UTC · 1310→835 tok open ⤢

thinking (1475 chars)

Line 1518: `exact (((((((((((contDiffOn_mS _)` — count opens: 12! `((((((((((((` = 12 (my edit inserted 12). The adds are 11 → need 11 outer closes + the mFblock-arg close... wait no: the argument `(contDiffOn_mFblock F hF)` has its own parens, separate. The structure: 12 opens, closes: mFblock-arg is its own; then `)` after = 1; mTL1b) 2; mTL2b) 3; mIdb) 4; mL1sqb) 5; mL1L2b) 6; mL2sqb) 7; mL1b) 8; mL2b) 9; mIIM) 10; const) 11. 12 opens − 11 closes = 1 unclosed?? But error says unexpected ')' (too many closes)... at 1521:83 — end of line 1521 — the last `)`. If 12 opens and 11 closes, parser waits for more → would say "expected term" not "unexpected )". Hmm — unless the FIRST `(` pairs differently: `exact (` ... `)` — the `exact (term)` — so it's 11 opens for the nesting + ... let me count the exact string: `exact (((((((((((contDiffOn_mS _)` — e-x-a-c-t space then parens: I count from the read: "((((((((((((" — precisely 12 `(` before `contDiffOn_mS`. With 11 closes → the 12th open is the exact-grouping paren needing a final close — parser hit `)` at col 83 and... col 83 IS the last char `)` after contDiffOn_const — that's close #11 — the 12th open remains → parser expects more content, hits newline/`/--` — the error "unexpected token ')'" at 1521:83 doesn't fit... unless there were actually 12 closes and 11 opens before my fix and the first error was the opposite. Simplest: rewrite the exact with a structured refine to kill paren-counting entirely.

Paren counting is error-prone — restructuring with `refine`.

tool: Edit ok

input

{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
  "old_string": "  unfold marginExpanded\n  exact (((((((((((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 contDiffOn_const)",
  "new_string": "  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"
}

result 2026-08-20 07:24:21Z → 2026-08-20 07:24:21Z

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean",
  "oldString": "  unfold marginExpanded\n  exact (((((((((((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 contDiffOn_const)",
  "newString": "  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",
  "originalFile": "/-\nNguyenRH1/LiSkeleton.lean \u2014 [SKELETON] statement-level formalization of\npaper draft.tex \u00a73.1 (R-004 finite-height Li theorem + archimedean lower\nbound + margin convexity 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\nAll proofs are `sorry` at this stage BY DESIGN (task 5.1 first pass:\nmachine-checked statements). `#print axioms` shows `sorryAx` until the\nproofs are filled in; no new axioms are introduced anywhere.\n\nArchive references: R-004, D-037, D-056, D-057, E-023, E-028, E-029.\n-/\nimport Mathlib\nimport Zeta23.Statement\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The Keiper\u2013Li coefficients -/\n\n/-- The Keiper\u2013Li coefficient \u03bb_n as the zero-side sum with multiplicity\n(draft \u00a73.1; Zeta23's IsNontrivialZero/zeroMult conventions).\nNOTE (honesty): `tsum` of a non-summable family is 0 in Lean, so the\nSUMMABILITY of this family is part of the mathematical content to be\nformalized (it follows from \u03a3 |\u03c1|\u207b\u00b2 < \u221e and |1\u2212(1\u22121/\u03c1)\u207f| = O(n/|\u03c1|)). -/\ndef liCoeff (n : \u2115) : \u2102 :=\n  tsum fun \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} =>\n    (zeroMult \u03c1 : \u2102) * (1 - (1 - 1 / (\u03c1 : \u2102)) ^ n)\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/-- [SKELETON] R-004, the finite-height Li theorem (draft Thm 3.1):\nassuming RH verified to T\u2080 = 3\u00d710\u00b9\u00b2 and finite Li verification to\n5\u00d710\u2075, \u03bb_n > 0 for all n \u2264 (T\u2080\u22121)\u00b2 \u2248 9.0\u00d710\u00b2\u2074.\nProof content to formalize: D-037 assembly (archimedean lower bound +\ntraced contour bound + bridge + margin argument). -/\ntheorem lambda_pos_finite_height\n    (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (5 * 10 ^ 5)) :\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  sorry\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/-- [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    (1 / 2) * n * Real.log n +\n        (lagariasC1 - Real.eulerMascheroniConstant / 2) * n - 4 \u2264\n      SInfty n := by\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/-- 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): margin\u0303(n) = S(n) \u2212 B\u0303(n) + 1 with\nthe counting function majorized by a smooth function F (the explicit\nTrudgian N(T) majorant is part of the formalization content and enters\nhere as a parameter with its majorant property as a hypothesis).\nM\u2080 = 1.3352 (E-023, grid-verified \u2014 see D-060 \u00a74 for its status). -/\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    (2 * F T + 4 * T * ((2 / 3) * C0hat 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 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 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 (f + g)) n = deriv (deriv f) n + deriv (deriv g) n := by\n  have he : deriv (f + g) =\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). -/\nprivate def mFblock (F : \u211d \u2192 \u211d) : \u211d \u2192 \u211d := fun m => (-2) * F (Real.sqrt m + 1)\nprivate def mTL1b : \u211d \u2192 \u211d := fun m => (-((8/3)*0.433 + 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.9 + 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 : ContDiff \u211d 2 F) :\n    ContDiffOn \u211d 2 (mFblock F) (Set.Ioi 20) :=\n  contDiffOn_const.mul\n    (hF.contDiffOn.comp contDiffOn_sqrt_shift (Set.mapsTo_univ _ _))\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 full margin is C\u00b2 on (20, \u221e). -/\ntheorem contDiffOn_marginExpanded (F : \u211d \u2192 \u211d) (hF : ContDiff \u211d 2 F) :\n    ContDiffOn \u211d 2 (marginExpanded F) (Set.Ioi 20) := by\n  unfold marginExpanded\n  exact (((((((((((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 contDiffOn_const)\n\n/-- [SKELETON] Margin convexity (D-057, draft \u00a73.1 Step 4): for any\ntwice-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).\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 : ContDiff \u211d 2 F)\n    (hmaj : \u2200 T : \u211d, (Ncount 0 T : \u211d) \u2264 F T)\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  sorry\n\n/-- [PROVED session 011] Localized variant of `chain_rule_sqrt_shift`:\n\u03c6 only needs to be C\u00b2 on (\u22121, \u221e) (all D-057 blocks: L1-singularities at\nT = \u22122, L2-singularities at T = \u22121). -/\ntheorem chain_rule_sqrt_shift_on (\u03c6 : \u211d \u2192 \u211d)\n    (h\u03c6 : ContDiffOn \u211d 2 \u03c6 (Set.Ioi (-1))) (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 (-1)) :=\n    h\u03c6.differentiableOn (by norm_num)\n  have h\u03c6dd : DifferentiableOn \u211d (deriv \u03c6) (Set.Ioi (-1)) :=\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 (-1) \u2208 \ud835\udcdd (Real.sqrt m + 1) := by\n    intro m hm\n    exact Ioi_mem_nhds (by linarith [Real.sqrt_nonneg m])\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\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 1515,
      "oldLines": 10,
      "newStart": 1515,
      "newLines": 11,
      "lines": [
        " theorem contDiffOn_marginExpanded (F : \u211d \u2192 \u211d) (hF : ContDiff \u211d 2 F) :",
        "     ContDiffOn \u211d 2 (marginExpanded F) (Set.Ioi 20) := by",
        "   unfold marginExpanded",
        "-  exact (((((((((((contDiffOn_mS _).add (contDiffOn_mFblock F hF)).add",
        "+  refine (((((((((((contDiffOn_mS _).add (contDiffOn_mFblock F hF)).add",
        "     contDiffOn_mTL1b).add contDiffOn_mTL2b).add contDiffOn_mIdb).add",
        "     contDiffOn_mL1sqb).add contDiffOn_mL1L2b).add contDiffOn_mL2sqb).add",
        "-    contDiffOn_mL1b).add contDiffOn_mL2b).add contDiffOn_mIIM).add contDiffOn_const)",
        "+    contDiffOn_mL1b).add contDiffOn_mL2b).add contDiffOn_mIIM).add",
        "+    contDiffOn_const",
        " ",
        " /-- [SKELETON] Margin convexity (D-057, draft \u00a73.1 Step 4): for any",
        " twice-differentiable majorant F of the zero count N(0,T] whose"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

raw content_json (database row)

[{"type":"thinking","thinking":"Line 1518: `exact (((((((((((contDiffOn_mS _)` — count opens: 12! `((((((((((((` = 12 (my edit inserted 12). The adds are 11 → need 11 outer closes + the mFblock-arg close... wait no: the argument `(contDiffOn_mFblock F hF)` has its own parens, separate. The structure: 12 opens, closes: mFblock-arg is its own; then `)` after = 1; mTL1b) 2; mTL2b) 3; mIdb) 4; mL1sqb) 5; mL1L2b) 6; mL2sqb) 7; mL1b) 8; mL2b) 9; mIIM) 10; const) 11. 12 opens − 11 closes = 1 unclosed?? But error says unexpected ')' (too many closes)... at 1521:83 — end of line 1521 — the last `)`. If 12 opens and 11 closes, parser waits for more → would say \"expected term\" not \"unexpected )\". Hmm — unless the FIRST `(` pairs differently: `exact (` ... `)` — the `exact (term)` — so it's 11 opens for the nesting + ... let me count the exact string: `exact (((((((((((contDiffOn_mS _)` — e-x-a-c-t space then parens: I count from the read: \"((((((((((((\" — precisely 12 `(` before `contDiffOn_mS`. With 11 closes → the 12th open is the exact-grouping paren needing a final close — parser hit `)` at col 83 and... col 83 IS the last char `)` after contDiffOn_const — that's close #11 — the 12th open remains → parser expects more content, hits newline/`/--` — the error \"unexpected token ')'\" at 1521:83 doesn't fit... unless there were actually 12 closes and 11 opens before my fix and the first error was the opposite. Simplest: rewrite the exact with a structured refine to kill paren-counting entirely.","signature":""},{"type":"text","text":"Paren counting is error-prone — restructuring with `refine`."},{"type":"tool_use","id":"Edit_300","name":"Edit","input":{"file_path":"D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSkeleton.lean","old_string":"  unfold marginExpanded\n  exact (((((((((((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 contDiffOn_const)","new_string":"  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"},"extra_content":null}]