{
  "content": "\"\"\"E-009b \u2014 Task 3.4c (D-018 plan step 2): Galerkin spectrum of Suzuki's A_a.\n\nOperator (Suzuki arXiv:2606.09096v1, Thm 1.1): A_a = Friedrichs extension\nof B_a = D* G_a D on L^2_0(-a,a) (mean-zero), D = i d/dx Dirichlet, G =\nconvolution with the screw function g (E-009a). Quadratic form (eq. 2.9):\n\n  Q(u,v) = int int g(x-y) u'(x) v'(y) dx dy      (u,v in H^1_0(-a,a))\n\n(the mean projection P_a drops out since int v' = 0 for H^1_0 functions).\n\nGalerkin: P1 hat functions on a uniform mesh of [-a,a], N elements,\nh = 2a/N. Convolution kernel + uniform mesh => Toeplitz stiffness:\n\n  Q_{i,i+k} = (1/h^2) (2 S_k - S_{k+1} - S_{|k-1|}),\n  S(k) = int_{-h}^{h} (h-|s|) g(kh+s) ds.\n\nS(k) is computed by DIRECT piecewise Gauss-Legendre quadrature of g\n(split at the prime-sum kinks log n; 12-pt GL per sub-interval; mpmath\nlerchphi only for arguments t <= 0.35). An earlier version integrated the\nregular part from the E-009a 1e-3 table; interpolation error ~1e-8 in g\nwas amplified by the 1/h^2 = 4e4 factor into ~1e-6 eigenvalue noise that\nmasked the true (tiny, positive) bottom of the spectrum. Direct quadrature\npushes S(k) errors below 1e-13.\n\nEigenproblem: Q c = lambda M c on the mean-zero subspace (QR projection),\nM = hat mass matrix. Under RH (zeros on the line), Weil positivity makes\nQ_W^a PSD, so all eigenvalues must be >= 0 (up to solver noise); the\nbottom eigenvalue is Suzuki's lambda_a (Thm 1.4: lambda_a = log(1/a)+O(1)\nfor small a).\n\nAbsolute validation: for v = sin(pi(x+a)/a) (H^1_0, mean-zero), the\nzero-side of the explicit formula gives Q(v,v) = 2 sum_{gamma>0}\n|vhat(gamma)|^2 = 2.437e-4 at a=3 (E-002 zeros; tail ~1e-11); checked\nagainst v^T Q v (validated conventions: Gaussian explicit-formula test\nclosed to 9e-16, session-003 diagnostic).\n\nRuns:\n  * h-convergence at a = 3: h = 0.01, 0.005, 0.002\n  * a-sweep at h = 0.005: a = 1, 2, 3, 4, 5\nInternal check: Q entries vs brute-force 2D integration of the E-009a\ntable (relative tolerance 1e-3, table-noise limited).\n\nOutputs: research/numerics/data/E-009b-suzuki-galerkin.csv (+ .json)\n\"\"\"\nimport json\nimport sys\nimport time\nfrom datetime import datetime, timezone\nfrom pathlib import Path\n\nimport numpy as np\nimport scipy.linalg\nimport mpmath as mp\nfrom numpy.polynomial.legendre import leggauss\n\nREPO = Path(__file__).resolve().parents[3]\nDATA = REPO / \"research\" / \"numerics\" / \"data\"\nG_CSV = DATA / \"E-009-suzuki-screw-function.csv\"\nZEROS_CSV = DATA / \"E-002-zeros-first-10000.csv\"\nCSV = DATA / \"E-009b-suzuki-galerkin.csv\"\nJSON = DATA / \"E-009b-suzuki-galerkin.json\"\n\nA_CONST = 0.5 * (np.log(2 * np.pi) + np.euler_gamma - 1.0)\nN_EIG = 12\nA_SWEEP = [1.0, 2.0, 3.0, 4.0, 5.0]\nH_SWEEP = 0.005\nH_CONV = [0.01, 0.005, 0.002]\nA_CONV = 3.0\nT_MAXG = 10.0                      # g needed on [0, 2a], a <= 5\nGL_N = 12                          # Gauss-Legendre points per sub-interval\nT_LERCH = 0.35                     # below this, Lerch via mpmath\n\n\n# ---------------------------------------------------------- g construction\ndef mangoldt_sieve(n_max: int) -> np.ndarray:\n    lam_log = np.zeros(n_max + 1)\n    is_comp = np.zeros(n_max + 1, dtype=bool)\n    for p in range(2, n_max + 1):\n        if not is_comp[p]:\n            if p * p <= n_max:\n                is_comp[p * p :: p] = True\n            pk = p\n            while pk <= n_max:\n                lam_log[pk] = np.log(p)\n                pk *= p\n    return lam_log\n\n\nN_MAXG = int(np.exp(T_MAXG)) + 2\nLAM_LOG = mangoldt_sieve(N_MAXG)\nNS = np.arange(2, N_MAXG + 1)\nLOGS = np.log(NS)\nLAM = LAM_LOG[2:] / np.sqrt(NS)\nC1 = np.cumsum(LAM)\nC0 = np.cumsum(LAM * LOGS)\n\nmp.dps = 30\nDIG_COEFF = float(-(mp.digamma(mp.mpf(1) / 4) - mp.log(mp.pi)) / 2)\nPHI1 = float(mp.lerchphi(1, 2, mp.mpf(1) / 4))\nKK = np.arange(0, 80)\nDENOM = (KK + 0.25) ** 2\n\n\ndef prime_sum_vec(t: np.ndarray) -> np.ndarray:\n    m = np.searchsorted(LOGS, t, side=\"right\")\n    out = np.zeros_like(t)\n    pos = m > 0\n    idx = m[pos] - 1\n    out[pos] = C1[idx] * t[pos] - C0[idx]\n    return out\n\n\ndef lerch_comb(t: np.ndarray) -> np.ndarray:\n    \"\"\"-1/4 [Phi(1,2,1/4) - e^{-t/2} Phi(e^{-2t},2,1/4)], t >= 0.\"\"\"\n    out = np.empty_like(t)\n    fast = t > T_LERCH\n    if fast.any():\n        z = np.exp(-2.0 * t[fast])\n        phi = (np.power.outer(z, KK) / DENOM).sum(axis=1)\n        out[fast] = -0.25 * (PHI1 - np.exp(-t[fast] / 2) * phi)\n    if (~fast).any():\n        mp.dps = 25\n        for i in np.flatnonzero(~fast):\n            ti = mp.mpf(float(t[i]))\n            out[i] = float(-0.25 * (mp.lerchphi(1, 2, mp.mpf(1) / 4)\n                                    - mp.exp(-ti / 2)\n                                    * mp.lerchphi(mp.exp(-2 * ti), 2,\n                                                  mp.mpf(1) / 4)))\n    return out\n\n\ndef g_float(t: np.ndarray) -> np.ndarray:\n    \"\"\"Suzuki's g(t) for t >= 0 (g even), float64 with mpmath Lerch tail.\"\"\"\n    t = np.asarray(t, dtype=float)\n    g = -4.0 * (np.exp(t / 2) + np.exp(-t / 2) - 2.0)\n    g += prime_sum_vec(t)\n    g += DIG_COEFF * t\n    g += lerch_comb(t)\n    g[t == 0.0] = 0.0\n    return g\n\n\n# --------------------------------------------------------------- S(k) exact\nXN, XW = leggauss(GL_N)\n\n\ndef S(k: int, h: float) -> float:\n    \"\"\"int_{-h}^{h} (h-|s|) g(kh+s) ds, split at prime-sum kinks log n.\"\"\"\n    if k == 0:\n        lo, hi, peak = 0.0, h, 0.0\n        # kinks in (0, h): none for h < log 2, but handle generally\n        n_lo = int(np.ceil(np.exp(lo)))\n        n_hi = int(np.floor(np.exp(hi)))\n        pts = [lo] + [float(np.log(n)) for n in range(max(n_lo, 2), n_hi + 1)\n                      if lo < np.log(n) < hi] + [hi]\n        tot = 0.0\n        for p0, p1 in zip(pts, pts[1:]):\n            mid, half = 0.5 * (p0 + p1), 0.5 * (p1 - p0)\n            xs = mid + half * XN\n            tot += half * float(np.dot(XW, (h - xs) * g_float(xs)))\n        return 2.0 * tot\n    lo, hi = (k - 1) * h, (k + 1) * h\n    n_lo = int(np.ceil(np.exp(lo)))\n    n_hi = int(np.floor(np.exp(hi)))\n    pts = [lo] + [float(np.log(n)) for n in range(max(n_lo, 2), n_hi + 1)\n                  if lo < np.log(n) < hi] + [hi]\n    tot = 0.0\n    for p0, p1 in zip(pts, pts[1:]):\n        mid, half = 0.5 * (p0 + p1), 0.5 * (p1 - p0)\n        xs = mid + half * XN\n        tot += half * float(np.dot(XW, (h - np.abs(xs - k * h))\n                                    * g_float(xs)))\n    return tot\n\n\ndef stiffness_first_col(n_elem: int, h: float) -> np.ndarray:\n    n_q = n_elem - 1\n    s = np.array([S(k, h) for k in range(n_elem)])\n    q = np.empty(n_q)\n    q[0] = (2.0 * s[0] - 2.0 * s[1]) / h**2\n    for k in range(1, n_q):\n        q[k] = (2.0 * s[k] - s[k + 1] - s[k - 1]) / h**2\n    return q\n\n\n# ------------------------------------------------- brute-force entry check\ndef brute_force_entry(i: int, k: int, h: float) -> float:\n    \"\"\"Q_{i,i+k} by 2D midpoint integration of g_float directly.\"\"\"\n    n_q = 24\n    x0 = -A_CONV + i * h\n    elems_i = [(x0 - h, x0, +1.0), (x0, x0 + h, -1.0)]\n    xj = x0 + k * h\n    elems_j = [(xj - h, xj, +1.0), (xj, xj + h, -1.0)]\n    tot = 0.0\n    for (a1, b1, s1) in elems_i:\n        xm = a1 + (np.arange(n_q) + 0.5) * (h / n_q)\n        for (a2, b2, s2) in elems_j:\n            ym = a2 + (np.arange(n_q) + 0.5) * (h / n_q)\n            d = np.abs(xm[:, None] - ym[None, :])\n            tot += s1 * s2 * g_float(d.ravel()).sum() * (h / n_q) ** 2\n    return tot / h**2\n\n\ndef spectrum(a: float, h: float) -> np.ndarray:\n    n_elem = int(round(2 * a / h))\n    n = n_elem - 1\n    q = stiffness_first_col(n_elem, h)\n    Q = scipy.linalg.toeplitz(q)\n    M = scipy.linalg.toeplitz(np.r_[2 * h / 3, h / 6,\n                                    np.zeros(max(n - 2, 0))])\n    Z = np.linalg.qr(np.ones((n, 1)), mode=\"complete\")[0][:, 1:]\n    Qz = Z.T @ Q @ Z\n    Mz = Z.T @ M @ Z\n    return scipy.linalg.eigvalsh(Qz, Mz, subset_by_index=[0, N_EIG - 1])\n\n\ndef main() -> int:\n    if CSV.exists() and \"--force\" not in sys.argv:\n        print(f\"cached: {CSV} exists (use --force to recompute)\"); return 0\n    t0 = time.time()\n    gam = np.loadtxt(ZEROS_CSV, delimiter=\",\", skiprows=1, usecols=1)\n    gam10 = gam[:N_EIG]\n\n    # ---- internal checks\n    h_chk = 0.005\n    q_chk = stiffness_first_col(int(round(2 * A_CONV / h_chk)), h_chk)\n    bf = {k: brute_force_entry(5, k, h_chk) for k in (0, 3)}\n    rel = {k: abs(q_chk[k] - bf[k]) / abs(bf[k]) for k in bf}\n    check_entries = bool(max(rel.values()) < 1e-3)\n    print(f\"entry check: rel err { {k: f'{v:.2e}' for k, v in rel.items()} }\")\n\n    # absolute validation: v = sin(pi(x+a)/a) at a=3 vs zero-side value\n    ne = int(round(2 * A_CONV / h_chk))\n    ii = np.arange(1, ne)\n    xs = -A_CONV + ii * h_chk\n    v = np.sin(np.pi * (xs + A_CONV) / A_CONV)\n    Qfull = scipy.linalg.toeplitz(q_chk)\n    vQv = float(v @ Qfull @ v)\n    beta = gam * A_CONV / np.pi\n    zero_side = 2.0 * ((A_CONV / np.pi) ** 2 * 4 * np.sin(gam * A_CONV) ** 2\n                       / (beta**2 - 1) ** 2).sum()\n    check_weil = bool(abs(vQv - zero_side) / zero_side < 2e-3)\n    print(f\"Weil validation: v^TQv={vQv:.6e} vs zero-side={zero_side:.6e} \"\n          f\"(rel {abs(vQv - zero_side) / zero_side:.2e})\")\n\n    rows = []\n    conv = {}\n    for h in H_CONV:\n        t1 = time.time()\n        w = spectrum(A_CONV, h)\n        conv[h] = w\n        print(f\"a={A_CONV} h={h}: N={int(round(2*A_CONV/h))} \"\n              f\"lambda_1={w[0]:.6e} ({time.time()-t1:.0f}s)\")\n        for j, lam in enumerate(w, start=1):\n            rows.append((A_CONV, h, int(round(2 * A_CONV / h)), j, lam))\n    gaps = [abs(conv[H_CONV[i + 1]][0] - conv[H_CONV[i]][0])\n            for i in range(len(H_CONV) - 1)]\n    check_hconv = bool(gaps[-1] <= gaps[0])\n\n    sweep = {}\n    for a in A_SWEEP:\n        t1 = time.time()\n        w = spectrum(a, H_SWEEP)\n        sweep[a] = w\n        print(f\"a={a}: lambda_1={w[0]:.6e} lambda_2={w[1]:.6e} \"\n              f\"({time.time()-t1:.0f}s)\")\n        for j, lam in enumerate(w, start=1):\n            rows.append((a, H_SWEEP, int(round(2 * a / H_SWEEP)), j, lam))\n\n    all_lam = np.array([r[4] for r in rows])\n    min_lam = float(all_lam.min())\n    check_pos = bool(min_lam > -1e-7)      # documented noise floor\n    check_mono = bool(all(sweep[a1][0] >= sweep[a2][0] - 1e-9\n                          for a1, a2 in zip(A_SWEEP, A_SWEEP[1:])))\n\n    checks = {\n        \"entries_vs_brute_force\": check_entries,\n        \"weil_form_value_matches_zero_side\": check_weil,\n        \"eigenvalues_ge_minus_noise_floor\": check_pos,\n        \"h_convergence_gaps_shrink\": check_hconv,\n        \"lambda1_nonincreasing_in_a\": check_mono,\n    }\n\n    DATA.mkdir(parents=True, exist_ok=True)\n    with CSV.open(\"w\", encoding=\"utf-8\", newline=\"\") as f:\n        f.write(\"a,h,N,j,lambda_j,gamma_j,lambda_over_gamma2\\n\")\n        for (a, h, n, j, lam) in rows:\n            g = gam10[j - 1]\n            f.write(f\"{a},{h},{n},{j},{lam:.10e},{g:.10f},\"\n                    f\"{lam / g**2:.6e}\\n\")\n\n    meta = {\n        \"experiment\": \"E-009b\",\n        \"task\": \"3.4c (D-018 step 2): Galerkin spectrum of Suzuki A_a\",\n        \"description\": \"P1-hat Galerkin discretization of the Weil-form \"\n                       \"operator A_a (Friedrichs ext of D*G_aD, mean-zero \"\n                       \"constraint); Toeplitz stiffness via exact piecewise \"\n                       \"Gauss-Legendre quadrature of g; bottom 12 \"\n                       \"eigenvalues; absolute validation vs zero-side \"\n                       \"explicit formula\",\n        \"script\": \"research/numerics/scripts/E-009-suzuki-galerkin.py\",\n        \"parameters\": {\"a_sweep\": A_SWEEP, \"h_sweep\": H_SWEEP,\n                       \"h_convergence_at_a\": A_CONV, \"h_conv\": H_CONV,\n                       \"n_eig\": N_EIG, \"gl_points\": GL_N},\n        \"checks\": checks,\n        \"key_values\": {\n            \"min_eigenvalue\": min_lam,\n            \"weil_validation\": {\"vTQv\": vQv, \"zero_side\": float(zero_side)},\n            \"h_conv_lambda1\": {str(h): float(conv[h][0]) for h in H_CONV},\n            \"lambda1_vs_a\": {str(a): float(sweep[a][0]) for a in A_SWEEP},\n            \"lambda2_vs_a\": {str(a): float(sweep[a][1]) for a in A_SWEEP},\n        },\n        \"caveats\": [\n            \"bottom eigenvalue lambda_a is POSITIVE but very small \"\n            \"(~1e-6 scale at a<=5) \u2014 earlier table-quadrature version \"\n            \"showed spurious -1e-4 values from 1e-3-mesh interpolation \"\n            \"noise amplified by 1/h^2; fixed by exact quadrature\",\n            \"eigenvalues of A_a are NOT the zero ordinates: the \"\n            \"zeta-aligned operator is Dbar_{a,theta} (first-order, in the \"\n            \"T_a-inner-product space) \u2014 its spectrum = zeros of \"\n            \"W(a,theta;z) (eq 1.11), a separate computation (E-010 candidate)\",\n            \"mean-zero constraint enforced (theorem's operator is on L^2_0)\",\n        ],\n        \"elapsed_seconds\": round(time.time() - t0, 1),\n        \"timestamp_utc\": datetime.now(timezone.utc).isoformat(),\n        \"row_count\": len(rows),\n    }\n    JSON.write_text(json.dumps(meta, indent=2), encoding=\"utf-8\")\n    ok = all(checks.values())\n    print(f\"wrote {CSV.name}, {JSON.name} \u2014 \"\n          f\"{'ALL CHECKS PASS' if ok else 'CHECK FAILURE: ' + str(checks)}\")\n    return 0 if ok else 1\n\n\nif __name__ == \"__main__\":\n    raise SystemExit(main())\n",
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-009-suzuki-galerkin.py"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiMoments.lean",
  "content": "/-\nLiMoments.lean \u2014 tier ii\u2032-3b: the contour moments (M) via the 5e\npartial-fraction identity (D-070 route revision; D-066 \u00a73's rectangle\nplan superseded).\n\nTarget (D-066 \u00a72 piece (M)): for all k \u2265 1,\n  sigmaP k = \u2212(iteratedDeriv (k\u22121) gFun 0)/(k\u22121)!,\nwhere gFun = logDeriv xiL and xiL = (s(s\u22121)/2)\u00b7completedRiemannZeta is\nthe entire \u03be. The whole argument is the identity\n\n  (G)  gFun s = B + seriesFun s\n\nat every good point (\u03b6 s \u2260 0, s \u2260 0, s \u2260 1, s \u2260 \u22122n for n \u2265 1) \u2014 pure\nlogDeriv algebra from 5e's `partialFraction_identity` \u2014 plus termwise\nseries calculus: k \u2265 2 by iterated derivation of the absolutely\nsummable zero series at 0 (the LiDigamma \u00a77\u20138 `iteratedDerivWithin_tsum`\npattern), k = 1 by the conj/reflect reindex V = \u03a3 mult\u00b7(1/\u03c1\u0304 \u2212 1/(1\u2212\u03c1))\n= \u2212V = 0 (zeroMult_conj + zeroMult_one_sub).\n\n\u00a71: xiL (entire closed form via completedRiemannZeta\u2080) + basic facts +\n    the two zero-subtype equivs.\n\u00a72: the good-set lemmas + (G) (`gFun_eq_momentB`).\n\u00a73: evaluation at 0 and 1 (punctured-continuity bridges) + the FE sign\n    (`gFun_one_eq_neg`).\n\u00a74: summability budget + the k = 1 rearrangement (`two_mul_sigmaP_one`).\n\u00a75: the per-term derivative machine + termwise iterated derivation at 0\n    (`iteratedDeriv_seriesFun_zero`).\n\u00a76: the capstone `sigmaP_eq_neg_iteratedDeriv_gFun_div`.\n\nPerimeter: `ZeroCountProp` only (inherited from 5e's gap circles).\nArchive references: D-066 \u00a72, D-068 \u00a75, D-070.\n-/\nimport Mathlib\nimport NguyenRH1.LiTightR\nimport NguyenRH1.LiSwaps\nimport NguyenRH1.LiResidue\nimport NguyenRH1.LiDigamma\nimport NguyenRH1.LiReflect\n\nopen Zeta23 Complex Filter Topology\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. The entire \u03be and the zero-subtype equivs -/\n\n/-- The entire \u03be in closed form: (s(s\u22121)/2)\u00b7\u039b\u2080(s) \u2212 (s\u22121)/2 + s/2 with\n\u039b\u2080 = `completedRiemannZeta\u2080` entire (Mathlib `differentiable_completedZeta\u2080`).\nEquals (s(s\u22121)/2)\u00b7\u039b(s) off {0, 1} (`xiL_eq_mul`); xiL(0) = xiL(1) = 1/2. -/\ndef xiL (s : \u2102) : \u2102 :=\n  (s * (s - 1) / 2) * completedRiemannZeta\u2080 s - (s - 1) / 2 + s / 2\n\nlemma differentiable_xiL : Differentiable \u2102 xiL := by\n  have h1 : Differentiable \u2102 (fun s : \u2102 => s * (s - 1) / 2) :=\n    (differentiable_id.mul (differentiable_id.sub_const 1)).div_const 2\n  have h2 : Differentiable \u2102 (fun s : \u2102 => (s - 1) / 2) :=\n    (differentiable_id.sub_const 1).div_const 2\n  have h3 : Differentiable \u2102 (fun s : \u2102 => s / 2) := differentiable_id.div_const 2\n  exact ((h1.mul differentiable_completedZeta\u2080).sub h2).add h3\n\nlemma analyticAt_xiL (s : \u2102) : AnalyticAt \u2102 xiL s :=\n  (differentiable_xiL.differentiableOn.analyticOnNhd isOpen_univ) s (Set.mem_univ s)\n\n/-- The defining equation off {0, 1}: xiL s = (s(s\u22121)/2)\u00b7\u039b(s). -/\nlemma xiL_eq_mul {s : \u2102} (h0 : s \u2260 0) (h1 : s \u2260 1) :\n    xiL s = (s * (s - 1) / 2) * completedRiemannZeta s := by\n  rw [xiL, completedRiemannZeta_eq]\n  have h1s : (1 : \u2102) - s \u2260 0 := sub_ne_zero.mpr (Ne.symm h1)\n  field_simp\n  ring\n\nlemma xiL_zero : xiL 0 = 1 / 2 := by simp [xiL]\n\nlemma xiL_one : xiL 1 = 1 / 2 := by simp [xiL]\n\n/-- The functional equation xiL(1\u2212s) = xiL(s), all s. -/\nlemma xiL_one_sub (s : \u2102) : xiL (1 - s) = xiL s := by\n  by_cases h0 : s = 0\n  \u00b7 subst h0\n    show xiL (1 - 0) = xiL 0\n    rw [sub_zero, xiL_one, xiL_zero]\n  by_cases h1 : s = 1\n  \u00b7 subst h1\n    show xiL (1 - 1) = xiL 1\n    rw [sub_self, xiL_zero, xiL_one]\n  \u00b7 have h10 : (1 : \u2102) - s \u2260 0 := sub_ne_zero.mpr (Ne.symm h0)\n    have h11 : (1 : \u2102) - s \u2260 1 := by\n      intro h\n      apply h0\n      have h2 := congrArg (fun t : \u2102 => (1 : \u2102) - t) h\n      simp at h2\n      exact h2\n    rw [xiL_eq_mul h10 h11, xiL_eq_mul h0 h1, completedRiemannZeta_one_sub]\n    congr 1\n    ring\n\n/-- xiL vanishes nowhere off {0, 1} where \u03b6 \u2260 0. -/\nlemma xiL_ne_zero {s : \u2102} (h0 : s \u2260 0) (h1 : s \u2260 1) (h\u03b6 : riemannZeta s \u2260 0) :\n    xiL s \u2260 0 := by\n  rw [xiL_eq_mul h0 h1]\n  apply mul_ne_zero\n  \u00b7 exact div_ne_zero (mul_ne_zero h0 (sub_ne_zero.mpr h1)) two_ne_zero\n  \u00b7 intro h\u039b\n    rw [completedRiemannZeta_eq_zero_iff] at h\u039b\n    exact h\u03b6 h\u039b.1\n\nlemma not_isNontrivialZero_zero : \u00ac IsNontrivialZero (0 : \u2102) := by\n  intro h\n  have h2 := h.2.1\n  rw [Complex.zero_re] at h2\n  exact lt_irrefl 0 h2\n\nlemma not_isNontrivialZero_one : \u00ac IsNontrivialZero (1 : \u2102) := by\n  intro h\n  have h2 := h.2.2\n  rw [Complex.one_re] at h2\n  exact lt_irrefl 1 h2\n\n/-- Reflection of a nontrivial zero: 1 \u2212 \u03c1 is a nontrivial zero\n(conj then Zeta23 reflect). -/\nlemma isNontrivialZero_one_sub {\u03c1 : \u2102} (h\u03c1 : IsNontrivialZero \u03c1) :\n    IsNontrivialZero (1 - \u03c1) := by\n  have h := zeta_reflect_zero \u03c1 (isNontrivialZero_conj h\u03c1)\n  have e : Zeta23.reflect ((starRingEnd \u2102) \u03c1) = 1 - \u03c1 := by\n    simp [Zeta23.reflect]\n  rwa [e] at h\n\n/-- The conjugation involution on the nontrivial-zero subtype. -/\ndef conjZeroEquiv : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} \u2243 {\u03c1 : \u2102 // IsNontrivialZero \u03c1} where\n  toFun \u03c1 := \u27e8(starRingEnd \u2102) \u03c1, isNontrivialZero_conj \u03c1.2\u27e9\n  invFun \u03c1 := \u27e8(starRingEnd \u2102) \u03c1, isNontrivialZero_conj \u03c1.2\u27e9\n  left_inv \u03c1 := Subtype.ext (by simp)\n  right_inv \u03c1 := Subtype.ext (by simp)\n\n/-- The reflection involution \u03c1 \u21a6 1 \u2212 \u03c1 on the nontrivial-zero subtype. -/\ndef oneSubZeroEquiv : {\u03c1 : \u2102 // IsNontrivialZero \u03c1} \u2243 {\u03c1 : \u2102 // IsNontrivialZero \u03c1} where\n  toFun \u03c1 := \u27e81 - \u03c1, isNontrivialZero_one_sub \u03c1.2\u27e9\n  invFun \u03c1 := \u27e81 - \u03c1, isNontrivialZero_one_sub \u03c1.2\u27e9\n  left_inv \u03c1 := Subtype.ext (by simp)\n  right_inv \u03c1 := Subtype.ext (by simp)\n\n/-! ## 2. The good set and the identity (G) -/\n\n/-- The chosen constant from the 5e partial-fraction identity. -/\nnoncomputable def momentB (hZC : ZeroCountProp) : \u2102 :=\n  Classical.choose (partialFraction_identity hZC)\n\nlemma momentB_spec (hZC : ZeroCountProp) (s : \u2102) (h\u03b6 : riemannZeta s \u2260 0)\n    (h0 : s \u2260 0) (h1 : s \u2260 1) (hn : \u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102)) :\n    logDeriv riemannZeta s = momentB hZC + seriesFun s - 1 / s - 1 / (s - 1) +\n      (Real.log Real.pi : \u2102) / 2 - Complex.digamma (s / 2) / 2 :=\n  Classical.choose_spec (partialFraction_identity hZC) s h\u03b6 h0 h1 hn\n\n/-- The log-derivative of \u03be. -/\nnoncomputable def gFun (s : \u2102) : \u2102 := logDeriv xiL s\n\n/-- The good-set half-shift condition for the \u0393R identity: s/2 \u2209 \u2212\u2115. -/\nlemma good_half_ne_neg_nat {s : \u2102} (h0 : s \u2260 0)\n    (hn : \u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102)) :\n    \u2200 m : \u2115, s / 2 \u2260 -(m : \u2102) := by\n  intro m hm\n  rcases Nat.eq_zero_or_pos m with hm0 | hm0\n  \u00b7 subst hm0\n    simp only [Nat.cast_zero, neg_zero] at hm\n    exact h0 (by linarith [hm])\n  \u00b7 apply hn m hm0\n    have h2 : s = -2 * (s / 2) := by ring\n    rw [h2, hm]\n    ring\n\n/-- **The identity (G)**: off the excluded set, gFun = B + seriesFun.\nPure logDeriv algebra: logDeriv of xiL = (s(s\u22121)/2)\u00b7\u039b splits as\n1/s + 1/(s\u22121) + [\u2212(log \u03c0)/2 + \u03c8(s/2)/2] + \u03b6\u2032/\u03b6, and 5e's\npartial-fraction identity collapses everything to B + seriesFun. -/\ntheorem gFun_eq_momentB (hZC : ZeroCountProp) {s : \u2102} (h\u03b6 : riemannZeta s \u2260 0)\n    (h0 : s \u2260 0) (h1 : s \u2260 1) (hn : \u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102)) :\n    gFun s = momentB hZC + seriesFun s := by\n  have hhalf : \u2200 m : \u2115, s / 2 \u2260 -(m : \u2102) := good_half_ne_neg_nat h0 hn\n  have h\u03930 : Complex.Gamma\u211d s \u2260 0 := by\n    rw [Ne, Complex.Gamma\u211d_eq_zero_iff]\n    push_neg\n    intro m\n    rcases Nat.eq_zero_or_pos m with hm | hm\n    \u00b7 subst hm\n      simp only [Nat.cast_zero, mul_zero, neg_zero]\n      exact h0\n    \u00b7 exact hn m hm\n  have h\u0393diff : DifferentiableAt \u2102 Complex.Gamma\u211d s :=\n    differentiableAt_Gamma\u211d_of_not_neg_nat hhalf\n  -- xiL agrees with the product form on a neighbourhood of s\n  have hopen : IsOpen ({0}\u1d9c \u2229 {1}\u1d9c : Set \u2102) :=\n    isOpen_compl_singleton.inter isOpen_compl_singleton\n  have hexp : \u2200\u1da0 t in \ud835\udcdd s, xiL t = (t * (t - 1) / 2) * completedRiemannZeta t := by\n    filter_upwards [hopen.mem_nhds \u27e8h0, h1\u27e9] with t ht\n    exact xiL_eq_mul ht.1 ht.2\n  -- \u039b agrees with \u0393R\u00b7\u03b6 on a neighbourhood of s\n  have h\u039beq : \u2200\u1da0 t in \ud835\udcdd s, completedRiemannZeta t = Complex.Gamma\u211d t * riemannZeta t := by\n    filter_upwards [h\u0393diff.continuousAt.eventually_ne h\u03930, eventually_ne_nhds h0]\n      with t ht\u0393 ht0\n    rw [riemannZeta_def_of_ne_zero ht0]\n    field_simp [ht\u0393]\n  have hlog : logDeriv xiL s =\n      logDeriv (fun t => (t * (t - 1) / 2) * completedRiemannZeta t) s := by\n    rw [logDeriv_apply, logDeriv_apply, hexp.deriv_eq, hexp.eq_of_nhds]\n  rw [gFun, hlog]\n  have hP : DifferentiableAt \u2102 (fun t : \u2102 => t * (t - 1) / 2) s :=\n    (differentiableAt_id.mul (differentiableAt_id.sub_const 1)).div_const 2\n  have h\u039b : DifferentiableAt \u2102 completedRiemannZeta s := differentiableAt_completedZeta h0 h1\n  have hP0 : s * (s - 1) / 2 \u2260 0 :=\n    div_ne_zero (mul_ne_zero h0 (sub_ne_zero.mpr h1)) two_ne_zero\n  have h\u039b0 : completedRiemannZeta s \u2260 0 := by\n    rw [Ne, completedRiemannZeta_eq_zero_iff]\n    rintro h\n    exact h\u03b6 h.1\n  rw [logDeriv_mul (f := fun t : \u2102 => t * (t - 1) / 2) (g := completedRiemannZeta) _\n    hP0 h\u039b0 hP h\u039b]\n  have hPlog : logDeriv (fun t : \u2102 => t * (t - 1) / 2) s = 1 / s + 1 / (s - 1) := by\n    rw [logDeriv_apply]\n    have hderiv : deriv (fun t : \u2102 => t * (t - 1) / 2) s = s - 1 / 2 := by\n      have hh : HasDerivAt (fun t : \u2102 => t * (t - 1) / 2) (s - 1 / 2) s := by\n        have h1' := (hasDerivAt_id' s).mul ((hasDerivAt_id' s).sub_const 1)\n        have h2' := h1'.div_const 2\n        convert h2' using 1\n        ring\n      exact hh.deriv\n    rw [hderiv]\n    have hs1 : s - 1 \u2260 0 := sub_ne_zero.mpr h1\n    field_simp\n    ring\n  rw [hPlog]\n  have hlog\u039b : logDeriv completedRiemannZeta s =\n      logDeriv Complex.Gamma\u211d s + logDeriv riemannZeta s := by\n    have heq : logDeriv completedRiemannZeta s =\n        logDeriv (fun t => Complex.Gamma\u211d t * riemannZeta t) s := by\n      rw [logDeriv_apply, logDeriv_apply, h\u039beq.deriv_eq, h\u039beq.eq_of_nhds]\n    rw [heq, logDeriv_mul (f := Complex.Gamma\u211d) (g := riemannZeta) _ h\u03930 h\u03b6\n      (differentiableAt_Gamma\u211d_of_not_neg_nat hhalf) (differentiableAt_riemannZeta h1)]\n  rw [hlog\u039b, logDeriv_Gamma\u211d_eq_of_not_neg_nat hhalf, momentB_spec hZC s h\u03b6 h0 h1 hn]\n  ring\n\n/-! ## 3. Evaluation at 0 and 1 -/\n\n/-- Functions continuous at s\u2080 that agree on the punctured neighbourhood\nagree at s\u2080. -/\nlemma eq_of_eventuallyEq_nhd_ne {F G : \u2102 \u2192 \u2102} {s\u2080 : \u2102} (hF : ContinuousAt F s\u2080)\n    (hG : ContinuousAt G s\u2080) (h : F =\u1da0[\ud835\udcdd[\u2260] s\u2080] G) : F s\u2080 = G s\u2080 :=\n  tendsto_nhds_unique (hF.tendsto.mono_left nhdsWithin_le_nhds)\n    ((hG.tendsto.mono_left nhdsWithin_le_nhds).congr' h.symm)\n\n/-- gFun is continuous wherever xiL \u2260 0. -/\nlemma gFun_continuousAt (s : \u2102) (hs : xiL s \u2260 0) : ContinuousAt gFun s :=\n  (((analyticAt_xiL s).deriv).div (analyticAt_xiL s) hs).continuousAt\n\n/-- The good conditions hold eventually in the punctured neighbourhood of 0. -/\nlemma good_eventually_zero :\n    \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102), riemannZeta s \u2260 0 \u2227 s \u2260 1 \u2227\n      (\u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102)) := by\n  have h\u03b6 : \u2200\u1da0 s in \ud835\udcdd (0 : \u2102), riemannZeta s \u2260 0 :=\n    (analyticAt_riemannZeta (by norm_num : (0 : \u2102) \u2260 1)).continuousAt.eventually_ne\n      (by rw [riemannZeta_zero]; norm_num)\n  have h1 : \u2200\u1da0 s in \ud835\udcdd (0 : \u2102), s \u2260 1 := eventually_ne_nhds (by norm_num : (0 : \u2102) \u2260 1)\n  have hnorm : \u2200\u1da0 s in \ud835\udcdd (0 : \u2102), \u2016s\u2016 < 2 := by\n    have h : Metric.ball (0 : \u2102) 2 \u2208 \ud835\udcdd (0 : \u2102) := Metric.ball_mem_nhds _ (by norm_num)\n    filter_upwards [h] with s hs\n    rw [Metric.mem_ball, dist_zero_right] at hs\n    exact hs\n  filter_upwards [h\u03b6.filter_mono nhdsWithin_le_nhds, h1.filter_mono nhdsWithin_le_nhds,\n    hnorm.filter_mono nhdsWithin_le_nhds] with s h\u03b6s h1s hsn\n  refine \u27e8h\u03b6s, h1s, fun n hn1 habs => ?_\u27e9\n  rw [habs] at hsn\n  have h2 : \u2016(-2 : \u2102)\u2016 = 2 := by\n    rw [show (-2 : \u2102) = ((-2 : \u211d) : \u2102) by push_cast; ring, Complex.norm_real,\n      Real.norm_eq_abs, abs_neg]\n    norm_num\n  have hbig : (2 : \u211d) \u2264 \u2016(-2 : \u2102) * (n : \u2102)\u2016 := by\n    rw [norm_mul, h2, RCLike.norm_natCast]\n    have hn1' : (1 : \u211d) \u2264 (n : \u211d) := Nat.one_le_cast.mpr hn1\n    linarith\n  linarith\n\n/-- The good conditions hold eventually in the punctured neighbourhood of 1. -/\nlemma good_eventually_one :\n    \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102), riemannZeta s \u2260 0 \u2227 s \u2260 0 \u2227\n      (\u2200 n : \u2115, 1 \u2264 n \u2192 s \u2260 -2 * (n : \u2102)) := by\n  have hA : \u2200\u1da0 s in \ud835\udcdd (1 : \u2102), zetaA s \u2260 0 := zetaA_ne_zero_near_one\n  have h0 : \u2200\u1da0 s in \ud835\udcdd (1 : \u2102), s \u2260 0 := eventually_ne_nhds (by norm_num : (1 : \u2102) \u2260 0)\n  have hnorm : \u2200\u1da0 s in \ud835\udcdd (1 : \u2102), \u2016s - 1\u2016 < 1 := by\n    have h : Metric.ball (1 : \u2102) 1 \u2208 \ud835\udcdd (1 : \u2102) := Metric.ball_mem_nhds _ (by norm_num)\n    filter_upwards [h] with s hs\n    rw [Metric.mem_ball, dist_eq_norm] at hs\n    exact hs\n  filter_upwards [hA.filter_mono nhdsWithin_le_nhds, self_mem_nhdsWithin,\n    h0.filter_mono nhdsWithin_le_nhds, hnorm.filter_mono nhdsWithin_le_nhds]\n    with s hAs hs1 h0s hsn\n  refine \u27e8?_, h0s, fun n hn1 habs => ?_\u27e9\n  \u00b7 intro h\u03b6\n    rw [zetaA_apply hs1, h\u03b6, mul_zero] at hAs\n    exact hAs rfl\n  \u00b7 rw [habs] at hsn\n    have hnorm2 : \u2016(-2 : \u2102) * (n : \u2102) - 1\u2016 = 2 * (n : \u211d) + 1 := by\n      have e : (-2 : \u2102) * (n : \u2102) - 1 = ((- (2 * (n : \u211d) + 1) : \u211d) : \u2102) := by\n        push_cast\n        ring\n      rw [e, Complex.norm_real, Real.norm_eq_abs, abs_neg, abs_of_nonneg (by\n        have hn0 : (0 : \u211d) \u2264 (n : \u211d) := Nat.cast_nonneg _\n        linarith)]\n      ring\n    rw [hnorm2] at hsn\n    have hn1' : (1 : \u211d) \u2264 (n : \u211d) := Nat.one_le_cast.mpr hn1\n    linarith\n\n/-- gFun(0) = B (punctured continuity; seriesFun(0) = 0). -/\nlemma gFun_zero (hZC : ZeroCountProp) : gFun 0 = momentB hZC := by\n  have hgood : \u2200\u1da0 s in \ud835\udcdd[\u2260] (0 : \u2102), gFun s = momentB hZC + seriesFun s := by\n    filter_upwards [good_eventually_zero, self_mem_nhdsWithin] with s \u27e8h\u03b6, h1, hn\u27e9 h0\n    exact gFun_eq_momentB hZC h\u03b6 h0 h1 hn\n  have hF : ContinuousAt gFun 0 := gFun_continuousAt 0 (by rw [xiL_zero]; norm_num)\n  have hG : ContinuousAt (fun s => momentB hZC + seriesFun s) 0 :=\n    continuousAt_const.add (seriesFun_analyticAt not_isNontrivialZero_zero).continuousAt\n  have h := eq_of_eventuallyEq_nhd_ne hF hG hgood\n  rwa [seriesFun_zero, add_zero] at h\n\n/-- gFun(1) = B + seriesFun(1) (punctured continuity). -/\nlemma gFun_one (hZC : ZeroCountProp) : gFun 1 = momentB hZC + seriesFun 1 := by\n  have hgood : \u2200\u1da0 s in \ud835\udcdd[\u2260] (1 : \u2102), gFun s = momentB hZC + seriesFun s := by\n    filter_upwards [good_eventually_one, self_mem_nhdsWithin] with s \u27e8h\u03b6, h0, hn\u27e9 h1\n    exact gFun_eq_momentB hZC h\u03b6 h0 h1 hn\n  have hF : ContinuousAt gFun 1 := gFun_continuousAt 1 (by rw [xiL_one]; norm_num)\n  have hG : ContinuousAt (fun s => momentB hZC + seriesFun s) 1 :=\n    continuousAt_const.add (seriesFun_analyticAt not_isNontrivialZero_one).continuousAt\n  exact eq_of_eventuallyEq_nhd_ne hF hG hgood\n\n/-- The FE sign: gFun(1) = \u2212gFun(0) (xiL(1\u2212s) = xiL(s), chain rule). -/\nlemma gFun_one_eq_neg : gFun 1 = -gFun 0 := by\n  have hfun : (fun s : \u2102 => xiL (1 - s)) = xiL := funext xiL_one_sub\n  have hderiv : deriv (fun s : \u2102 => xiL (1 - s)) 0 = -deriv xiL 1 := by\n    have h1 : DifferentiableAt \u2102 xiL ((fun s : \u2102 => 1 - s) 0) := by\n      simpa using differentiable_xiL 1\n    have h2 : DifferentiableAt \u2102 (fun s : \u2102 => 1 - s) 0 :=\n      (differentiableAt_const (1 : \u2102)).sub differentiableAt_id\n    have hcomp : deriv (xiL \u2218 fun s : \u2102 => 1 - s) 0 =\n        deriv (fun s : \u2102 => 1 - s) 0 * deriv xiL ((fun s : \u2102 => 1 - s) 0) :=\n      deriv.comp 0 h1 h2\n    have heq : (xiL \u2218 fun s : \u2102 => 1 - s) = fun s : \u2102 => xiL (1 - s) := rfl\n    rw [heq] at hcomp\n    have hinner : deriv (fun s : \u2102 => 1 - s) 0 = -1 := by\n      rw [deriv_const_sub differentiableAt_id]\n      simp\n    rw [hinner] at hcomp\n    simp at hcomp\n    exact hcomp\n  have h0 : deriv xiL 0 = -deriv xiL 1 := by\n    rw [\u2190 hfun]\n    exact hderiv\n  rw [gFun, gFun, logDeriv_apply, logDeriv_apply, xiL_zero, xiL_one, h0]\n  field_simp\n  ring\n\nend NguyenRH1\n",
  "structuredPatch": [],
  "originalFile": null
}