{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-037.md",
  "content": "# Session 037 (2026-08-24) \u2014 ii\u2032-3b STARTED: capstone dependency audit + LiMoments \u00a71\u2013\u00a74 COMPLETE (k=1 moment PROVED)\n\n## What happened\n\n1. **User-requested dependency audit of the ii\u2032-5f capstone** (pre-ii\u2032-3b).\n   New file `AuditSession037.lean` + output `audit-session037-axioms.txt`:\n   - `#print axioms logDeriv_riemannZeta_sub_nearZeros_le_tight` \u2192\n     **[propext, Classical.choice, Quot.sound] only** (no sorryAx, nothing else).\n   - The exact perimeter recorded verbatim from the elaborator:\n     `ZeroCountProp` (unit window, mult-weighted, \u2264 C0hat(t+1), t \u2265 2;\n     C0hat t = 0.433\u00b7log(t+2) + 0.886\u00b7log log(t+2) + 2.9),\n     `ZeroCountProp2` (two-unit window, \u2264 0.6\u00b7L + 0.886\u00b7LL + 2.7, t \u2265 10),\n     `NoLowZeros` (\u2200 \u03c1 nontrivial, 14 \u2264 |Im \u03c1|); plus the statement-level\n     constructs `nearZerosSub`, `Zeta23.zeroMult` (= analyticOrderAt.toNat),\n     `zeroAbsWindow`. One fix during the audit: `zeroMult` is `Zeta23.zeroMult`\n     (not NguyenRH1) \u2014 the first script run caught it.\n\n2. **ii\u2032-3b LAUNCHED with a route revision (D-070).** D-066 \u00a73's plan was\n   rectangle contours (zero-avoiding T, horizontal decay from the R-bound,\n   vertical push-off). But 5e's `partialFraction_identity (hZC)` IS the\n   contour work done once: with gFun := logDeriv xiL, xiL := (s(s\u22121)/2)\u00b7\u039b,\n   the identity **(G) gFun s = B + seriesFun s** at every good point is pure\n   logDeriv algebra, and the moments (M) sigmaP k = \u2212gFun^{(k\u22121)}(0)/(k\u22121)!\n   follow by termwise series calculus. Perimeter carried: ZeroCountProp ONLY\n   (the 5f tight bound's hZC2/hNLZ are NOT needed for the moments). D-070\n   filed with the full argument + sanity gate (\u03c3\u2081 = \u2212gFun(0) = \u2212B =\n   1 + \u03b3/2 \u2212 \u00bdlog 4\u03c0 \u2248 0.0230957, the Davenport value; B = log 2\u03c0 \u2212 1 \u2212\n   (log \u03c0)/2 \u2212 \u03b3/2 \u2248 \u22120.0230957 numerically).\n\n3. **LiMoments.lean \u00a71\u2013\u00a74 COMPLETE, build GREEN** (~730 lines, new file,\n   not yet root-imported; imports NguyenRH1.LiTightR + LiSwaps + LiResidue +\n   LiDigamma + LiReflect):\n   - \u00a71: `xiL` entire via the CLOSED FORM xiL s := (s(s\u22121)/2)\u00b7\u039b\u2080(s) \u2212 (s\u22121)/2\n     + s/2 (Mathlib `completedRiemannZeta_eq`: \u039b = \u039b\u2080 \u2212 1/s \u2212 1/(1\u2212s), \u039b\u2080\n     entire \u2014 sidesteps removable-singularity proofs; D-066's \"\u039b\u2080 wrong\n     object\" warning is about \u039b\u2080's ZEROS, never used). `xiL_eq_mul` (off\n     {0,1}), `xiL_zero`/`xiL_one` (= 1/2), `xiL_one_sub` (FE, by cases),\n     `xiL_ne_zero` (via RvM.completedRiemannZeta_eq_zero_iff),\n     `isNontrivialZero_one_sub` (conj then Zeta23 zeta_reflect_zero),\n     `conjZeroEquiv`/`oneSubZeroEquiv` (the two subtype involutions).\n   - \u00a72: `momentB` (Classical.choose of partialFraction_identity) +\n     **`gFun_eq_momentB`** \u2014 (G) at good points: logDeriv_mul chains\n     (xiL = (s(s\u22121)/2)\u00b7\u039b eventuallyEq; \u039b = \u0393R\u00b7\u03b6 eventuallyEq;\n     logDeriv \u0393R via logDeriv_Gamma\u211d_eq_of_not_neg_nat; the good-set\n     half-shift `good_half_ne_neg_nat`); final collapse by `ring`.\n   - \u00a73: `eq_of_eventuallyEq_nhd_ne` (punctured-continuity bridge,\n     tendsto_nhds_unique), `gFun_continuousAt`, the good-eventually sets at\n     0 (\u03b6(0) = \u22121/2 continuity) and 1 (zetaA factor), `seriesFun_zero` (= 0\n     termwise), `seriesFun_one` (= \u03a3 mult/(\u03c1(1\u2212\u03c1))), **`gFun_zero`**\n     (gFun 0 = B), **`gFun_one`** (gFun 1 = B + seriesFun 1),\n     **`gFun_one_eq_neg`** (FE sign: xiL(1\u2212s) = xiL(s) + deriv_comp chain\n     rule + EventuallEq.of_eq.deriv_eq).\n   - \u00a74: the summability budget + the k=1 rearrangement:\n     `summable_mult_div_norm_sq` (master, the ii\u2032-2 (9/4)-comparison\n     skeleton cloned), `exists_norm_lower_bound` (\u03b4-ball at 0),\n     `summable_mult_inv_pow` (k \u2265 2), `tsum_mult_inv_pow_conj` +\n     `summable_mult_inv_pow_conj` (conjEquiv reindex, zeroMult_conj),\n     **`sigmaP_eq_unpaired`** (k \u2265 2: sigmaP k = \u00bd(S+S) = S),\n     `summable_mult_div_norm_sq_one_sub` (oneSubEquiv transfer),\n     `mult_div_norm_mul_norm_le` (AM-GM: 1/(\u2016\u03c1\u2016\u20161\u2212\u03c1\u2016) \u2264 \u00bd(\u2016\u03c1\u2016\u207b\u00b2+\u20161\u2212\u03c1\u2016\u207b\u00b2),\n     via (1/a\u22121/b)\u00b2 \u2265 0 \u2014 NO im-lower-bound needed),\n     `summable_mult_one_div_mul_one_sub`, `summable_mult_vTerm` (the\n     1/\u03c1\u0304\u22121/(1\u2212\u03c1) = (1\u22122re)/(\u03c1\u0304(1\u2212\u03c1)) identity; |1\u22122re| \u2264 1),\n     **`vTerm_tsum_eq_zero`** (V = W by conj reindex, W = \u2212V by reflect\n     reindex, so 2V = 0), `summable_mult_fst/snd`, **`two_mul_sigmaP_one`**\n     (2\u03c3\u2081 = \u03a3 mult/(\u03c1(1\u2212\u03c1)) = seriesFun 1), and the k=1 capstone\n     **`sigmaP_one_eq_neg_gFun_zero`** (2\u03c3\u2081 = seriesFun 1 = gFun 1 \u2212 B =\n     \u22122\u00b7gFun 0 by the FE sign; linear_combination combo (h2 \u2212 hg1 + hg0 +\n     hfe)/2). NO re/conj-of-tsum bridges anywhere \u2014 all reality arguments\n     are subtype-equiv reindexes.\n\n## REMAINING for ii\u2032-3b (\u00a75/\u00a76) \u2014 full skeleton (design verified against Mathlib)\n\n**\u00a75 (termwise iterated derivation at 0, k \u2265 2):**\n- `iteratedDeriv_zpow_neg_one (k c) (hs : s+c \u2260 0)`: iteratedDeriv k\n  (fun s => (s+c)^(\u22121:\u2124)) s = (\u22121)^k\u00b7k!\u00b7(s+c)^(\u2212k\u22121) \u2014 from LiDigamma's\n  `iteratedDeriv_neg_zpow_neg_one_add` via e : f = \u2212(\u2212f) + **iteratedDeriv_neg\n  (EXISTS, explicit args (n f a), probed)**. (iteratedDeriv_const_mul (c)\n  (hf : ContDiffAt) also exists, Lemmas.lean:368.)\n- `iteratedDeriv_seriesTerm (j \u2265 1) \u03c1 (hs : s\u2212\u03c1 \u2260 0)`: seriesTerm s \u03c1 =\n  mult\u00b7((s+(\u2212\u03c1))^(\u22121:\u2124) + 1/\u03c1); rw [e, iteratedDeriv_const_mul,\n  iteratedDeriv_add hF1 hF2, iteratedDeriv_const, if_neg j\u22600, add_zero,\n  zpow lemma]. ContDiffAt proofs via AnalyticAt \u2192 **AnalyticAt.contDiffAt\n  (EXISTS, probed)**; constant via contDiff_const.contDiffAt.\n- `seriesTerm_deriv_summableLocallyUniformlyOn (j \u2265 1) h\u03b4 hball`: on\n  u := ball 0 (\u03b4/2) via **SummableLocallyUniformlyOn_of_locally_bounded\n  (probed: (IsOpen s) \u2192 (\u2200 K \u2286 s, IsCompact K \u2192 \u2203 u, Summable u \u2227 \u2200 n k \u2208 K,\n  \u2016f n k\u2016 \u2264 u n))**. Bound: \u2016s\u2212\u03c1\u2016 \u2265 \u2016\u03c1\u2016/2 (\u2016s\u2016 < \u03b4/2 \u2264 \u2016\u03c1\u2016/2), term \u2264\n  mult\u00b7j!\u00b72^{j+1}\u00b7(1/\u03b4)^{j\u22121}\u00b7\u2016\u03c1\u2016\u207b\u00b2 =: C_j\u00b7(mult/\u2016\u03c1\u2016\u00b2) (master lemma\n  mul_left). Norm chain: 3\u00d7 norm_mul + RCLike.norm_natCast \u00d72 + hsign\n  (\u2016(\u22121)^j\u2016=1) + norm_zpow + exponent rewrite (\u2212(j:\u2124)\u22121 = \u2212((j+1:\u2115):\u2124),\n  zpow_neg, zpow_natCast) \u2014 the LiDigamma:735\u2013746 pattern EXACTLY.\n  one_div_le_one_div_of_le (probed: 0<a \u2192 a\u2264b \u2192 1/b \u2264 1/a).\n- `iteratedDeriv_seriesFun_zero (j \u2265 1)`: obtain \u03b4 from\n  exists_ball_avoid_nontrivialZeros 0; **iteratedDerivWithin_tsum (probed\n  signature: (m) (IsOpen s) (x\u2208s) (\u2200 t\u2208s, Summable) (\u2200 k, 1\u2264k\u2192k\u2264m \u2192\n  SummableLocallyUniformlyOn ...) (\u2200 n k r, k\u2264m\u2192r\u2208s \u2192 DifferentiableAt\n  (iteratedDerivWithin k (f n) s) r))** \u2014 the LiDigamma:749\u2013785 call pattern\n  verbatim (side condition: j'=0 \u2192 seriesTerm differentiable (s\u2212\u03c1\u22600 on the\n  ball); j'\u22651 \u2192 eventuallyEq with the closed form, zpow differentiability\n  via hasDerivAt_zpow + rfl-bridge on \u2218). Then iteratedDerivWithin_of_isOpen\n  conversions + per-term iteratedDeriv_seriesTerm at 0.\n\n**\u00a76 (capstone):**\n- `gFun_eventuallyEq_zero (hZC)`: gFun =\u1da0[\ud835\udcdd 0] (B + seriesFun) \u2014 upgrade\n  the punctured version via **eventually_nhdsWithin_iff (probed \u2713)** +\n  gFun_zero/seriesFun_zero at the point.\n- `sigmaP_eq_neg_iteratedDeriv_gFun_div (hZC) (hk : 1 \u2264 k)`:\n  k=1: show (1\u22121)\u22610 defeq; sigmaP_one_eq_neg_gFun_zero.\n  k\u22652: iteratedDeriv_congr_of_eventuallyEq (LiDigamma:568) \u2192\n  (fun _ => B) + seriesFun via funext/Pi.add bridge \u2192 iteratedDeriv_add\n  hcf hcg (ContDiffAt: const + seriesFun analytic) \u2192 iteratedDeriv_const\n  if_neg (k\u22121\u22600) \u2192 iteratedDeriv_seriesFun_zero (k\u22121) \u2192 per-term at 0:\n  (0\u2212\u03c1)^(\u2212k:\u2124) = (\u22121)^k\u00b7(1/\u03c1)^k (zero_sub, zpow_neg, zpow_natCast, neg_pow,\n  mul_inv, ((\u22121)^k)\u207b\u00b9 = (\u22121)^k via inv_eq_of_mul_eq_one_right +\n  (\u22121)^{2k}=1, one_div/inv_pow) \u2192 sign (\u22121)^{k\u22121}\u00b7(\u22121)^k = \u22121 (pow_add,\n  2k\u22121 = 2(k\u22121)+1, pow_mul, (\u22121)\u00b2=1) \u2192 tsum = \u2212(k\u22121)!\u00b7sigmaP k\n  (tsum_congr, tsum_mul_left, sigmaP_eq_unpaired) \u2192 field_simp with\n  (k\u22121)! \u2260 0 (Nat.cast_eq_zero, Nat.factorial_ne_zero).\n- Then: root-import LiTightR + LiMoments in NguyenRH1.lean (STATE.md plan),\n  full build, axiom audit (expect 3 standard axioms; hZC-only dependency),\n  journal/db/STATE/NGUYEN updates, commit. **ii\u2032-3b \u2192 done; next is ii\u2032-3c**\n  ((4.10-a) assembly, D-066 \u00a72: needs also the FE derivative relation\n  gFun^{(k\u22121)}(0) = (\u22121)^k\u00b7gFun^{(k\u22121)}(1) \u2014 new but small from xiL_one_sub\n  + iteratedDeriv comp machinery).\n\n## Banked gotchas (this session)\n\n- **SummationFilter refactor**: tsum lemmas are SummationFilter-parameterized\n  in this Mathlib; `tsum_add`/`tsum_sub` exist ONLY as method forms\n  `Summable.tsum_add hf hg` / `Summable.tsum_sub` (plain `tsum_add` is\n  UNKNOWN); `tsum_neg`, `tsum_zero`, `tsum_congr`, `tsum_mul_left` are plain.\n- `eq_zero_of_neg_eq` needs LinearOrder \u2014 N/A for \u2102; use 2V = 0 via\n  linear_combination + mul_eq_zero.resolve_left.\n- `Complex.norm_conj : \u2016(starRingEnd \u2102) z\u2016 = \u2016z\u2016` \u2014 takes the starRingEnd\n  form DIRECTLY (don't rw [starRingEnd_apply] first; the star form breaks\n  rw matching).\n- `iteratedDeriv_neg (n) (f) (a)` EXISTS (explicit args);\n  `iteratedDeriv_const_mul (c) (hf : ContDiffAt \ud835\udd5c n f x)`;\n  `AnalyticAt.contDiffAt` exists (CompleteSpace needed).\n- `Equiv.tsum_eq e f : \u2211' a, f (e a) = \u2211' b, f b`;\n  `Equiv.summable_iff e : Summable (f \u2218 e) \u2194 Summable f` (f implicit \u2014 NO\n  second argument; state the family equation with `\u2218` and funext).\n- Beta-redex goals (families applied to equiv images): **show-before-rw**\n  (state the beta-reduced form with `show`, then rw) \u2014 plain rw can't find\n  the cast patterns inside redexes. (Recurred 5\u00d7.)\n- **Ascribe every tsum binder**: `\u2211' \u03c1, ... (zeroMult \u03c1 : \u2102) ...` elaborates\n  \u03c1 : \u2102 (zeroMult expects \u2102) \u2014 silently produces a tsum over the WRONG\n  domain. Always `\u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, ...`.\n- field_simp closes goals outright (trailing `ring` then errors \"no goals\" \u2014\n  3\u00d7 this session); but field_simp given \u2016x\u2016 \u2260 0 instead of x \u2260 0 normalizes\n  without clearing \u2014 pass the COMPLEX nonzeros (x \u2260 0, 1\u2212x \u2260 0, conj x \u2260 0).\n- `convert h using 1; ring` on HasDerivAt values: convert can produce\n  non-equality goals (\"ring_nf made no progress\") \u2014 instead ASCRIBE the\n  derivative value in the HasDerivAt statement and `rw [h.deriv]; ring`.\n- `deriv.comp` / `deriv_comp`: point arg x is EXPLICIT first\n  (`deriv_comp 0 h1 h2`); numeral-as-function error otherwise.\n- `ContinuousAt.add` on `continuousAt_const`: produces Pi.add functions \u2014\n  the defeq assignment `have hG : ContinuousAt (fun s => c + f s) x := hG0`\n  works (simpa [Pi.add_apply] does NOT).\n- `linear_combination` works over \u2102 (use it for \u2102 equalities; linarith does\n  NOT).\n- Housekeeping: `Scratch.lean` (previously the session-029 audit script) was\n  overwritten with this session's lemma probe \u2014 the session-029 audit RESULTS\n  are preserved in audit-session029-axioms.txt (script re-derivable from the\n  AuditSession03X pattern).\n\n## Files\n\n- research/lean/NguyenRH1/NguyenRH1/LiMoments.lean (NEW, ~730 lines, GREEN)\n- research/lean/NguyenRH1/AuditSession037.lean + audit-session037-axioms.txt\n- research/lean/NguyenRH1/Scratch.lean (lemma probe; see housekeeping)\n- research/derivations/D-070-ii-prime-3b-route-revision.md (NEW)\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\web\\dashboard\\templates\\dashboard\\lean_detail.html",
  "content": "{% extends \"dashboard/base.html\" %}\n{% block title %}{{ item.file }}{% endblock %}\n{% block nav_lean %}active{% endblock %}\n{% block content %}\n<p><a href=\"{% url 'lean' %}\">\u2190 Lean Proofs</a></p>\n<h1>{{ item.file }}</h1>\n<p class=\"muted\">{{ item.lines }} lines \u00b7 {{ item.decls|length }} declarations \u00b7\n  {{ item.sorries }} {{ item.sorries|pluralize:\"sorry,sorries\" }} \u00b7\n  updated {{ item.mtime|slice:\":10\" }}</p>\n\n{% if item.decls %}\n<section class=\"card\">\n  <h2>Declarations</h2>\n  <table class=\"tbl\">\n    <thead><tr><th>Kind</th><th>Name</th><th>Line</th></tr></thead>\n    <tbody>\n    {% for d in item.decls %}\n      <tr><td>{{ d.kind }}</td><td><code>{{ d.name }}</code></td><td>{{ d.line }}</td></tr>\n    {% endfor %}\n    </tbody>\n  </table>\n</section>\n{% endif %}\n\n<section class=\"card\">\n  <h2>Source</h2>\n  <pre class=\"json-box code-box\">{{ item.source }}</pre>\n</section>\n{% endblock %}\n",
  "structuredPatch": [],
  "originalFile": null
}