{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1.lean",
  "old_string": "  NguyenRH1.LiArchimedean  \u2014 tier ii\u2032-3a piece (A): the archimedean\n                             coefficients (logDeriv_Gamma\u211d split; \u03c4\u2080)",
  "new_string": "  NguyenRH1.LiDigamma      \u2014 tier ii\u2032-3a piece (A) core: the digamma\n                             series + polygamma values at 1/2\n  NguyenRH1.LiArchimedean  \u2014 tier ii\u2032-3a piece (A): the archimedean\n                             coefficients (iteratedDeriv_logDeriv_Gamma\u211d)"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1.lean",
  "oldString": "  NguyenRH1.LiArchimedean  \u2014 tier ii\u2032-3a piece (A): the archimedean\n                             coefficients (logDeriv_Gamma\u211d split; \u03c4\u2080)",
  "newString": "  NguyenRH1.LiDigamma      \u2014 tier ii\u2032-3a piece (A) core: the digamma\n                             series + polygamma values at 1/2\n  NguyenRH1.LiArchimedean  \u2014 tier ii\u2032-3a piece (A): the archimedean\n                             coefficients (iteratedDeriv_logDeriv_Gamma\u211d)",
  "originalFile": "/-\nNguyenRH1.lean \u2014 root of the NGUYEN-RH-1 Phase-5 skeleton library.\n\nStatement-level Lean 4 skeletons for the project's new results\n(paper draft.tex \u00a73), built on zeta-23-lean (tag v1.0) conventions.\nEvery proof is `sorry` at this stage BY DESIGN: this is task 5.1's\nfirst pass \u2014 get the *statements* machine-checked against Mathlib +\nZeta23 types. `#print axioms` on any declaration here shows `sorryAx`\nuntil the corresponding proof is formalized; that marker is the\nhonesty tag, mirrored by the [SKELETON] comments.\n\nContents:\n  NguyenRH1.LiSkeleton     \u2014 R-004 finite-height Li theorem + the\n                             archimedean lower bound (draft \u00a73.1);\n                             assembly proved modulo SfBoundProp\n  NguyenRH1.LiBasePoints   \u2014 tier (ii) step 2: certified interval-bound\n                             discharge of the two margin evaluations;\n                             lambda_pos_finite_height_verified (perimeter\n                             + SfBoundProp only)\n  NguyenRH1.LiResidue      \u2014 tier ii\u2032-1b(i): the w = 1 residue of the\n                             Lagarias-kernel integrand (ResW1_eq_sum)\n  NguyenRH1.LiPrincipal    \u2014 tier ii\u2032-1b(ii): the principal-part integral\n                             (rectInt'_ppart)\n  NguyenRH1.LiSides        \u2014 tier ii\u2032-1b(iii): rectangle residue theorem\n                             for the integrand (rectInt'_Jlag)\n  NguyenRH1.LiSwaps        \u2014 tier ii\u2032-2: the elementary swaps\n                             (liCoeff_eq_sum_sigma, sInfty_eq_sum)\n  NguyenRH1.LiZetaCoeff    \u2014 tier ii\u2032-3a piece (B): the \u03b6-piece Taylor\n                             coefficients (iteratedDeriv_hLiExt)\n  NguyenRH1.LiArchimedean  \u2014 tier ii\u2032-3a piece (A): the archimedean\n                             coefficients (logDeriv_Gamma\u211d split; \u03c4\u2080)\n  NguyenRH1.SuzukiSkeleton \u2014 R-003 exact factorization (draft \u00a73.2)\n  NguyenRH1.ValleySkeleton \u2014 valley law statements (draft \u00a73.3)\n-/\nimport NguyenRH1.LiSkeleton\nimport NguyenRH1.LiBasePoints\nimport NguyenRH1.LiResidue\nimport NguyenRH1.LiPrincipal\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiSwaps\nimport NguyenRH1.LiZetaCoeff\nimport NguyenRH1.LiArchimedean\nimport NguyenRH1.SuzukiSkeleton\nimport NguyenRH1.ValleySkeleton\n",
  "structuredPatch": [
    {
      "oldStart": 27,
      "oldLines": 8,
      "newStart": 27,
      "newLines": 10,
      "lines": [
        "                              (liCoeff_eq_sum_sigma, sInfty_eq_sum)",
        "   NguyenRH1.LiZetaCoeff    \u2014 tier ii\u2032-3a piece (B): the \u03b6-piece Taylor",
        "                              coefficients (iteratedDeriv_hLiExt)",
        "+  NguyenRH1.LiDigamma      \u2014 tier ii\u2032-3a piece (A) core: the digamma",
        "+                             series + polygamma values at 1/2",
        "   NguyenRH1.LiArchimedean  \u2014 tier ii\u2032-3a piece (A): the archimedean",
        "-                             coefficients (logDeriv_Gamma\u211d split; \u03c4\u2080)",
        "+                             coefficients (iteratedDeriv_logDeriv_Gamma\u211d)",
        "   NguyenRH1.SuzukiSkeleton \u2014 R-003 exact factorization (draft \u00a73.2)",
        "   NguyenRH1.ValleySkeleton \u2014 valley law statements (draft \u00a73.3)",
        " -/"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1.lean",
  "old_string": "import NguyenRH1.LiSides\nimport NguyenRH1.LiSwaps\nimport NguyenRH1.LiZetaCoeff\nimport NguyenRH1.LiArchimedean",
  "new_string": "import NguyenRH1.LiSides\nimport NguyenRH1.LiSwaps\nimport NguyenRH1.LiZetaCoeff\nimport NguyenRH1.LiDigamma\nimport NguyenRH1.LiArchimedean"
}

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

{
  "file_path": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\PrintAxioms.lean",
  "content": "/- Session 020 axiom audit: ii\u2032-3a pieces (A)+(B) \u2014 all key declarations. -/\nimport Mathlib\nimport NguyenRH1.LiArchimedean\n\nopen NguyenRH1\n\n#print axioms iteratedDeriv_logDeriv_Gamma\u211d\n#print axioms logDeriv_Gamma\u211d_one\n#print axioms logDeriv_Gamma\u211d_one_add\n#print axioms iteratedDeriv_digamma_half_value\n#print axioms iteratedDeriv_digamma_half\n#print axioms iteratedDeriv_DinfC_half\n#print axioms psiReal_eq_DinfR\n#print axioms deriv_log_Gamma_real\n#print axioms dpsiSeqR_tendstoLocallyUniformlyOn\n#print axioms digamma_eq_DinfC_on\n#print axioms DinfC_analyticOn\n#print axioms tsum_two_mul_add_one_inv_pow\n#print axioms tsum_half_add_nat_zpow\n#print axioms iteratedDeriv_one_add_div_two\n#print axioms iteratedDerivWithin_dpsiTermC\n#print axioms iteratedDerivWithin_tsum_dpsiTermC\n#print axioms dpsiTermC_summable\n#print axioms dpsiTermR_summable\n"
}

{
  "type": "update",
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\PrintAxioms.lean",
  "content": "/- Session 020 axiom audit: ii\u2032-3a pieces (A)+(B) \u2014 all key declarations. -/\nimport Mathlib\nimport NguyenRH1.LiArchimedean\n\nopen NguyenRH1\n\n#print axioms iteratedDeriv_logDeriv_Gamma\u211d\n#print axioms logDeriv_Gamma\u211d_one\n#print axioms logDeriv_Gamma\u211d_one_add\n#print axioms iteratedDeriv_digamma_half_value\n#print axioms iteratedDeriv_digamma_half\n#print axioms iteratedDeriv_DinfC_half\n#print axioms psiReal_eq_DinfR\n#print axioms deriv_log_Gamma_real\n#print axioms dpsiSeqR_tendstoLocallyUniformlyOn\n#print axioms digamma_eq_DinfC_on\n#print axioms DinfC_analyticOn\n#print axioms tsum_two_mul_add_one_inv_pow\n#print axioms tsum_half_add_nat_zpow\n#print axioms iteratedDeriv_one_add_div_two\n#print axioms iteratedDerivWithin_dpsiTermC\n#print axioms iteratedDerivWithin_tsum_dpsiTermC\n#print axioms dpsiTermC_summable\n#print axioms dpsiTermR_summable\n",
  "structuredPatch": [
    {
      "oldStart": 1,
      "oldLines": 11,
      "newStart": 1,
      "newLines": 25,
      "lines": [
        "-/- Session 020 axiom audit: ii\u2032-3a piece (A) part 1 new declarations. -/",
        "+/- Session 020 axiom audit: ii\u2032-3a pieces (A)+(B) \u2014 all key declarations. -/",
        " import Mathlib",
        " import NguyenRH1.LiArchimedean",
        " ",
        " open NguyenRH1",
        " ",
        "+#print axioms iteratedDeriv_logDeriv_Gamma\u211d",
        " #print axioms logDeriv_Gamma\u211d_one",
        " #print axioms logDeriv_Gamma\u211d_one_add",
        "-#print axioms pi_cpow_neg_half_eq_exp",
        "-#print axioms log_four_pi",
        "+#print axioms iteratedDeriv_digamma_half_value",
        "+#print axioms iteratedDeriv_digamma_half",
        "+#print axioms iteratedDeriv_DinfC_half",
        "+#print axioms psiReal_eq_DinfR",
        "+#print axioms deriv_log_Gamma_real",
        "+#print axioms dpsiSeqR_tendstoLocallyUniformlyOn",
        "+#print axioms digamma_eq_DinfC_on",
        "+#print axioms DinfC_analyticOn",
        "+#print axioms tsum_two_mul_add_one_inv_pow",
        "+#print axioms tsum_half_add_nat_zpow",
        "+#print axioms iteratedDeriv_one_add_div_two",
        "+#print axioms iteratedDerivWithin_dpsiTermC",
        "+#print axioms iteratedDerivWithin_tsum_dpsiTermC",
        "+#print axioms dpsiTermC_summable",
        "+#print axioms dpsiTermR_summable",
        " "
      ]
    }
  ],
  "originalFile": "/- Session 020 axiom audit: ii\u2032-3a piece (A) part 1 new declarations. -/\nimport Mathlib\nimport NguyenRH1.LiArchimedean\n\nopen NguyenRH1\n\n#print axioms logDeriv_Gamma\u211d_one\n#print axioms logDeriv_Gamma\u211d_one_add\n#print axioms pi_cpow_neg_half_eq_exp\n#print axioms log_four_pi\n",
  "autoRead": false
}