Session 9 — Phase 4 synthesis assault + paper draft cleanup

{
  "file_path": "D:\\Python\\Quantum\\STATE.md"
}

{
  "command": "ls -la \"D:/Python/Quantum/research/resources/\" && echo \"---\" && ls \"D:/Python/Quantum/research/paper/\"",
  "description": "List resources and paper folders"
}

{
  "command": "cd /d/Python/Quantum && wc -c \"research/resources/Detailed_Derivations_ Riemann_Zeta_Compeddium_Step-by-Step.txt\" \"research/paper/Detailed_Derivations_ Riemann_Zeta_Compeddium_Step-by-Step.txt\" && echo \"=== head resources ===\" && head -15 \"research/resources/Detailed_Derivations_ Riemann_Zeta_Compeddium_Step-by-Step.txt\" && echo \"=== head paper ===\" && head -15 \"research/paper/Detailed_Derivations_ Riemann_Zeta_Compeddium_Step-by-Step.txt\"",
  "description": "Compare sizes and headers of the two compendium copies"
}

{
  "pattern": "resources",
  "path": "D:\\Python\\Quantum\\research\\journal\\session-007.md",
  "output_mode": "content",
  "-n": true,
  "head_limit": 40
}

{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-007.md",
  "offset": 40
}

{
  "command": "cd /d/Python/Quantum && ls research/derivations/ | head -5 && grep -n \"Part III\" \"research/derivations/D-001-master-tool-index.md\" | head -5 && tail -20 \"research/derivations/D-001-master-tool-index.md\"",
  "description": "Inspect D-001 structure for Part III insertion point"
}

{
  "file_path": "D:\\Python\\Quantum\\NGUYEN.md",
  "old_string": "| R6 | Compute resources | Local: Ryzen 9 7945HX 16c/32t, 64GB, RTX 4090 Laptop 16GB (CUDA 8.9). On request (ask user first, user provisions): Lambda AI multi-GPU cloud (SSH); IBM Quantum (no identified need as of 2026-08-17 \u2014 RH compute is classical) | Scaling numerics |",
  "new_string": "| R6 | Compute resources | Local: Ryzen 9 7945HX 16c/32t, 64GB, RTX 4090 Laptop 16GB (CUDA 8.9). On request (ask user first, user provisions): Lambda AI multi-GPU cloud (SSH); IBM Quantum (no identified need as of 2026-08-17 \u2014 RH compute is classical) | Scaling numerics |\n| R7 | research/resources/ atlas (43 notes) | User-provided RH-equivalence atlas, step-by-step derivations of ~60 equations: all major RH criteria (Li, Lagarias, Robin, Nyman\u2013Beurling, Redheffer, Mertens, Riesz&H\u2013L, Salem, Volchkov, Franel\u2013Landau, Speiser, de Bruijn\u2013Newman, von Koch\u2013Schoenfeld, Hilbert\u2013P\u00f3lya), zero-counting/explicit formulas, RMT statistics, foundations. Index: research/resources/index.md | All tracks; cross-pollination reservoir (\u00a74A); D-037 direct inputs |"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-001-quantum-formalism-index.md",
  "old_string": "## PART III \u2014 EXTERNAL DISCOVERIES (web research log, per \u00a74A.3)",
  "new_string": "## PART III \u2014 EXTERNAL DISCOVERIES (web research log, per \u00a74A.3)\n\n### 2026-08-19 \u2014 R7 resources atlas registered (research/resources/, 43 notes)\nUser-provided RH-equivalence atlas; read in full session 007, formally\nregistered as manifest resource R7 with per-note index + project-use map:\nresearch/resources/index.md. Key direct inputs: Schoenfeld 8\u03c0 + B\u00fcthe\n2018 (\u2192D-037), Hasanalizade\u2013Shen\u2013Wong S(t) bound (\u2192D-036 alt constants),\nLi/Lagarias notes (\u2192tasks 3.5\u20133.8), Hilbert\u2013P\u00f3lya/Berry\u2013Keating (\u2192task\n2.2). Criteria atlas = standing cross-pollination reservoir (\u00a74A.5)."
}

{
  "command": "cd /d/Python/Quantum && git add research/resources/index.md NGUYEN.md research/derivations/D-001-quantum-formalism-index.md && git -c user.name=\"NGUYEN-RH-1\" -c user.email=\"research@local\" commit -m \"$(cat <<'EOF'\nSession 008: register R7 resources atlas (43-note RH-equivalence reference) \u2014 index.md + manifest + D-001 pointer\nEOF\n)\" && git status --short",
  "description": "Commit R7 atlas registration"
}

{
  "todos": [
    {
      "content": "Read design inputs (D-033, D-036, E-021 data, Lagarias \u00a76)",
      "status": "in_progress",
      "activeForm": "Reading design inputs"
    },
    {
      "content": "Assemble D-037: finite-height theorem with explicit N\u2081",
      "status": "pending",
      "activeForm": "Assembling D-037"
    },
    {
      "content": "Adversarial review of the chain",
      "status": "pending",
      "activeForm": "Reviewing the chain adversarially"
    },
    {
      "content": "File R-004, update indexes/db/NGUYEN.md/STATE.md, commit",
      "status": "pending",
      "activeForm": "Filing R-004 and updating archive"
    }
  ]
}

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-032-li-literature-map.md"
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiSeries.lean",
    "content": "\n/-! ## 0. The series -/\n\n/-- The zero-series summand: mult(\u03c1)\u00b7(1/(s\u2212\u03c1) + 1/\u03c1) over the nontrivial\nzero subtype (the ii\u2032-1a encoding; D-068 \u00a73). -/\ndef seriesTerm (s : \u2102) (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}) : \u2102 :=\n  (zeroMult \u03c1 : \u2102) * (1 / (s - (\u03c1 : \u2102)) + 1 / (\u03c1 : \u2102))\n\n/-- The zero-side partial-fraction series. Summable at every s\n(`seriesSummable`), analytic off the nontrivial zeros\n(`seriesFun_analyticOnNhd`). -/\ndef seriesFun (s : \u2102) : \u2102 := \u2211' \u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1}, seriesTerm s \u03c1\n\n/-! ## 1. The norm comparison and the tail bound -/\n\n/-- For a nontrivial zero with 2 \u2264 \u2016\u03c1\u2016: 1 + \u2016\u03b3_\u03c1\u2016\u00b2 \u2264 (17/12)\u00b7\u2016\u03c1\u2016\u00b2.\nOn re \u03c1 \u2208 (0, 1): \u2016\u03b3\u2016\u00b2 = im\u00b2 + (1/2\u2212re)\u00b2 \u2264 im\u00b2 + 1/4, and\nim\u00b2 = \u2016\u03c1\u2016\u00b2 \u2212 re\u00b2 \u2265 4 \u2212 1 = 3 gives 5/4 \u2264 (5/12)\u00b7im\u00b2. -/\nlemma one_add_normSq_gammaOf_le (\u03c1 : {\u03c1 : \u2102 // IsNontrivialZero \u03c1})\n    (h\u03c1 : (2 : \u211d) \u2264 \u2016(\u03c1 : \u2102)\u2016) :\n    1 + Complex.normSq (gammaOf (\u03c1 : \u2102)) \u2264 17 / 12 * \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by\n  have hz := \u03c1.2\n  have hre0 : 0 < (\u03c1 : \u2102).re := hz.2.1\n  have hre1 : (\u03c1 : \u2102).re < 1 := hz.2.2\n  have hnorm : \u2016(\u03c1 : \u2102)\u2016 ^ 2 = (\u03c1 : \u2102).re ^ 2 + (\u03c1 : \u2102).im ^ 2 := by\n    rw [\u2190 Complex.normSq_eq_norm_sq, Complex.normSq_apply]\n    ring\n  have hgam : Complex.normSq (gammaOf (\u03c1 : \u2102))\n      = (\u03c1 : \u2102).im ^ 2 + (1 / 2 - (\u03c1 : \u2102).re) ^ 2 := by\n    rw [Complex.normSq_apply, WeilEF.gammaOf_re, WeilEF.gammaOf_im]\n    ring\n  have h\u03c1sq : 4 \u2264 \u2016(\u03c1 : \u2102)\u2016 ^ 2 := by nlinarith [h\u03c1, norm_nonneg (\u03c1 : \u2102)]\n  have hre2 : (\u03c1 : \u2102).re ^ 2 \u2264 1 := by nlinarith [hre0, hre1]\n  have him2 : 3 \u2264 (\u03c1 : \u2102).im ^ 2 := by nlinarith [h\u03c1sq, hre2]\n  have hquarter : (1 / 2 - (\u03c1 : \u2102).re) ^ 2 \u2264 1 / 4 := by nlinarith [hre0, hre1]\n  rw [hgam, hnorm]\n  nlinarith [him2, hquarter, sq_nonneg (\u03c1 : \u2102).re]\n\n/-- The key algebra: 1/(s\u2212\u03c1) + 1/\u03c1 = s/(\u03c1\u00b7(s\u2212\u03c1)). -/\nlemma one_div_sub_add_one_div {s \u03c1 : \u2102} (h0 : \u03c1 \u2260 0) (h1 : s - \u03c1 \u2260 0) :\n    1 / (s - \u03c1) + 1 / \u03c1 = s / (\u03c1 * (s - \u03c1)) := by\n  have h2 : \u03c1 * (s - \u03c1) \u2260 0 := mul_ne_zero h0 h1\n  field_simp\n  ring\n",
    "numLines": 45,
    "startLine": 50,
    "totalLines": 603
  }
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\data\\E-021-sinf-sf-curve.json"
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\web\\dashboard\\templates\\dashboard\\feedback.html",
    "content": "{% extends \"dashboard/base.html\" %}\n{% block title %}Feedback{% endblock %}\n{% block nav_feedback %}active{% endblock %}\n{% block content %}\n<h1>Feedback & Suggestions</h1>\n<p class=\"muted\">Comments, ideas, corrections, and questions for the research\nprogram. Submissions are stored and reviewed by the researcher \u2014 a good\nsuggestion can change the attack plan.</p>\n\n<div class=\"grid-2\">\n<section class=\"card\">\n  <h2>Submit</h2>\n  <form method=\"post\" class=\"fb-form\">\n    {% csrf_token %}\n    <label>Name (optional)\n      <input type=\"text\" name=\"name\" maxlength=\"120\" placeholder=\"Anonymous\">\n    </label>\n    <label>Category\n      <select name=\"category\">\n        {% for value, label in categories %}<option value=\"{{ value }}\">{{ label }}</option>{% endfor %}\n      </select>\n    </label>\n    <label>Your feedback\n      <textarea name=\"text\" rows=\"7\" required\n        placeholder=\"An idea for a track, a reference we should read, a correction, a question\u2026\"></textarea>\n    </label>\n    <button type=\"submit\">Submit feedback</button>\n  </form>\n</section>\n\n<section class=\"card\">\n  <h2>Search</h2>\n  <form method=\"get\" class=\"fb-search\">\n    <input type=\"text\" name=\"q\" value=\"{{ q }}\" placeholder=\"Search text\u2026\">\n    <select name=\"category\">\n      <option value=\"\">All categories</option>\n      {% for value, label in categories %}\n        <option value=\"{{ value }}\" {% if cat == value %}selected{% endif %}>{{ label }}</option>\n      {% endfor %}\n    </select>\n    <select name=\"status\">\n      <option value=\"\">All statuses</option>\n      {% for value, label in statuses %}\n        <option value=\"{{ value }}\" {% if status == value %}selected{% endif %}>{{ label }}</option>\n      {% endfor %}\n    </select>\n    <button type=\"submit\">Search</button>\n  </form>\n</section>\n</div>\n\n<section class=\"card\">\n  <h2>Submissions ({{ items|length }})</h2>\n  {% for it in items %}\n    <div class=\"fb-item\">\n      <div class=\"fb-head\">\n        <span class=\"tag tag-cat\">{{ it.get_category_display }}</span>\n        <strong>{{ it.name|default:\"Anonymous\" }}</strong>\n        <span class=\"muted\">{{ it.created }}</span>\n        <span class=\"tag {% if it.status == 'new' %}tag-run{% elif it.status == 'reviewed' %}tag-num{% else %}tag-ok{% endif %}\">{{ it.get_status_display }}</span>\n      </div>\n      <p>{{ it.text|linebreaksbr }}</p>\n      {% if it.notes %}<p class=\"fb-notes\"><em>Researcher notes:</em> {{ it.notes|linebreaksbr }}</p>{% endif %}\n    </div>\n  {% empty %}\n    <p class=\"muted\">No feedback yet \u2014 be the first.</p>\n  {% endfor %}\n</section>\n{% endblock %}",
    "numLines": 69,
    "startLine": 1,
    "totalLines": 69
  }
}

{
  "command": "cd /d/Python/Quantum && grep -n \"def R_sample\\|def zeta_log_deriv\\|def R_val\\|acb\\|fd\\|derivative\" research/numerics/scripts/E-021-sinf-sf-curve.py | head -20 && echo === && sed -n '/def R_sample\\|def R_val\\|def zeta_log_deriv/,+30p' research/numerics/scripts/E-021-sinf-sf-curve.py | head -60",
  "description": "Find R(s) evaluation code in E-021"
}

{
  "command": "cd /d/Python/Quantum && ls research/results/ && head -40 research/results/index.md",
  "description": "Check results index format"
}

{
  "command": "cd /d/Python/Quantum && tail -6 research/results/index.md && echo === && tail -4 research/derivations/index.md && echo === && grep -n \"add-result\\|add-derivation\\|log-experiment\" research/numerics/scripts/db.py | head",
  "description": "Check index tails and db CLI"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-008.md",
  "content": "# Session 008 \u2014 2026-08-19\n## Regroup + R7 registration; task 3.8 COMPLETE (R-004 finite-height Li theorem)\n\n### Part 1 \u2014 Regroup (user-requested) and resources registration\n- User asked for a regroup + formal registration of the resources folder.\n- Created research/resources/index.md: all 43 notes cataloged in 4 groups\n  (Foundations / Zeros & explicit formulas / RH equivalences / RMT\n  statistics), each mapped to the track/task it feeds.\n- NGUYEN.md \u00a72: R7 row added. D-001 Part III: pointer entry.\n- Found: research/paper/Detailed_Derivations_...txt is an OLDER DRAFT\n  duplicate (54,034 vs 54,367 bytes, missing intro) of the resources\n  compendium \u2014 untracked, flagged to user for deletion (not deleted).\n- Committed as session-008 opening (e7b72ad).\n\n### Part 2 \u2014 Task 3.8 (D-037 \u2192 R-004) COMPLETE\nAssembled the explicit finite-height Li theorem. Full chain in D-037:\n1. Read inputs: D-032/D-033 (design), D-036 (constants), E-021 data,\n   Lagarias math/0404394 PDF \u00a71 (Thm 1.1, bridge (1.16)) and \u00a76\n   (Thm 6.1 proof, read in full).\n2. **Coordinate-system audit** of D-036 (variant A kernel-plane vs\n   variant B w-plane): resolved \u2014 D-036/E-021 consistent in variant B\n   (contour in the \u03b6\u2032/\u03b6 argument plane, \u03c3\u2080 = \u22125/2, trivial zero \u22122\n   inside, residue \u2264 1). No bug.\n3. **Real gap found**: D-036's uniform |\u03b6\u2032/\u03b6| bound on segment (III)\n   rests on the R-bound verified only for |t| \u2265 10; the line passes\n   within 1/2 of the trivial pole at w = \u22122. Closed by E-023 S1:\n   M\u2080 = max_{|t|\u226410} |\u03b6\u2032/\u03b6(\u22125/2+it)| = 1.3352 (grid + Lipschitz \u00d72).\n   Contribution 40\u00b7M\u2080 = 53.4 \u2014 negligible.\n4. **S_\u221e elementary lower bound derived** (new, D-037 \u00a73): from\n   Lagarias (4.11) via finite differences:\n   S_\u221e(n) = (1\u2212a\u2081)n \u2212 1 + \u03a3_{m odd\u22653} [(1\u22121/m)\u207f \u2212 1 + n/m]\n   \u27f9 S_\u221e(n) \u2265 \u00bdn log n + (C\u2081\u2212\u03b3/2)n \u2212 4 (n \u2265 20), fully explicit\n   (harmonic bounds). Validated vs E-021 exact values (E-023 V1).\n   Avoids tracing Lagarias \u00a75's O(1) lemmas entirely.\n5. Margin assembly (E-023): margin convex for n \u2265 20; crossover\n   32 871 (traced A=2/B\u2080=2) / 30 217 (measured 0.9/1.0); adopted\n   N\u2080 = 5\u00d710\u2074 (margin 67 705). Finite verification contiguous:\n   ours to 3000 (ledger #3) + Misguich\u2013Voros to 5\u00d710\u2075 (10\u00d7 overlap).\n6. Bridge: n \u2264 (T\u2080\u22121)\u00b2 from the proof's actual requirement\n   (\u221an+1 \u2264 T\u2080); Lagarias's printed (1.16) window T\u00b2/(4log\u00b2T) is\n   conservative slack \u2014 fallback N\u2081* = 2.726\u00d710\u00b2\u00b9 documented.\n\n**THEOREM (R-004, ledger #6):** \u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081 = (T\u2080\u22121)\u00b2 = 8 999 999 999 994 000 000 000 001 \u2248 9.0\u00d710\u00b2\u2074,\nT\u2080 = 3\u00d710\u00b9\u00b2 (Platt\u2013Trudgian). Tag [PROVED-CONDITIONAL(computational\nRH-to-T\u2080; finite verification; one numeric sub-bound)]. Criterion-3\ndeliverable; the maximal content of the Li route short of RH (Voros).\n\n### Adversarial review highlights (D-037 \u00a77)\n- P1\u2013P6 proved/elementary; H1\u2013H5 computational/heuristic, each with\n  sensitivity analysis (theorem insensitive to H2/H3 links) and upgrade\n  paths: D-039 (Binet-form digamma sub-bound proof), E-023b (acb box\n  cover for M\u2080).\n- Sanity gates pass: no claim beyond N\u2081; no D-H/Epstein analogue.\n\n### State of the plan\n- Track C (Phase 3): 3.1\u20133.8 ALL CLOSED. The Li/front-A line has\n  delivered its maximal deliverable.\n- Next per plan: 2.10 (E-022 spectral-measure numerics), 2.9-D1 (Krein\n  frame), 2.11 (D-038 transition scale). Optional: D-039, E-023b.\n\n### Handoff notes\n- E-023 script: research/numerics/scripts/E-023-finite-height-assembly.py;\n  data E-023-assembly.csv/.json; db registered (session 8).\n- Platt\u2013Trudgian exact height: \"3\u00d710\u00b9\u00b2\" per title/abstract\n  (arXiv:2004.09765); confirm exact certified height at paper write-up\n  (N\u2081 insensitive at <1% level).\n- N\u2080 could be pushed under 3000 (fully self-contained verification) only\n  with a fundamentally sharper horizontal-segment treatment (I_II/IV\n  dominate B(n) below n ~ 10\u2075: 2(e\u2074+1)\u00b77H(T), H = 3C\u2080\u00b2 ~ zero-avoidance\n  d_min); not needed for the theorem \u2014 literature bridge suffices.\n- E-021 n=10\u2074 rerun still available cheaply via caches (unchanged).\n"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-035-star-attack-design.md"
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDisc.lean",
    "content": "\ntheorem gapD_le (t : \u211d) : gapD t \u2264 1 / 50 := by\n  unfold gapD\n  have hb : (0:\u211d) < 50 * ((card96 t : \u211d) + 1) :=\n    mul_pos (by norm_num) (add_pos_of_nonneg_of_pos (Nat.cast_nonneg _) one_pos)\n  apply (div_le_div_iff_of_pos_left (by norm_num : (0:\u211d) < 1) hb\n    (by norm_num : (0:\u211d) < 50)).mpr\n  have h1 : (1:\u211d) \u2264 (card96 t : \u211d) + 1 := by linarith [Nat.cast_nonneg (card96 t)]\n  have h2 : (50:\u211d) * 1 \u2264 50 * ((card96 t : \u211d) + 1) :=\n    mul_le_mul_of_nonneg_left h1 (by norm_num)\n  rwa [mul_one] at h2\n\n/-- **The collection radius**: R_c \u2208 [2.3, 2.4] at distance \u2265 1/(20(k+1))\nfrom every (5/2)-scaled norm of a 24/25-zero, where k is the cardinality",
    "numLines": 14,
    "startLine": 536,
    "totalLines": 847
  }
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-016-herglotz-fine-structure.py",
  "offset": 314,
  "limit": 90
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\quantum-deploy\\docroot\\app\\web\\dashboard\\research_data.py",
    "content": "\ndef _experiments_by_script():\n    by = {}\n    for r in get_experiments():\n        if r.get(\"script\"):\n            by.setdefault(Path(r[\"script\"]).stem, []).append(r)\n    return by\n\n\ndef script_list():\n    by = _experiments_by_script()\n    out = []\n    for p in sorted(SCRIPTS_DIR.glob(\"*.py\")):\n        rows = by.get(p.stem, [])\n        out.append({\n            \"name\": p.stem, \"file\": p.name,\n            \"experiments\": [r[\"id\"] for r in rows],\n            \"data_files\": [f[\"name\"] for f in _script_data_files(p.stem, rows)],",
    "numLines": 18,
    "startLine": 687,
    "totalLines": 894
  }
}

{
  "command": "cd /d/Python/Quantum && grep -n \"PrimeBackendV2\\|prime_sum_vec\\|_BUILD\" research/numerics/scripts/E-019-zeroflow-a12.py | head && sed -n '/backend = /,+8p' research/numerics/scripts/E-019-zeroflow-a12.py | head -12 && grep -n \"Z_MAX_ZERO\\|A_SWEEP\\|GL_N\" research/numerics/scripts/E-016-herglotz-fine-structure.py | head -6",
  "description": "Check backend v2 monkeypatch pattern in E-019"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-022-spectral-measure.py",
  "old_string": "from prime_backend_v2 import PrimeBackendV2       # noqa: E402\nfrom importlib import import_module               # noqa: E402\nE19 = import_module(\"E-019-zeroflow-a12\") if False else None",
  "new_string": "from prime_backend_v2 import PrimeBackendV2       # noqa: E402"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-022-spectral-measure.py",
  "old_string": "    zeros5 = locate_zeros(cp5, x5, h5)\n    K5 = weights_for(4.0, 0.005, zeros5[:50], x5)\n    K4 = weights_for(4.0, H_MAIN, zeros5[:50], x5)  # same z's, h=0.01 K",
  "new_string": "    zeros5 = locate_zeros(cp5, x5, h5)\n    K5 = weights_for(4.0, 0.005, zeros5[:50], x5)\n    x01, _, _, _, _ = E16.build(4.0, H_MAIN)\n    K4 = weights_for(4.0, H_MAIN, zeros5[:50], x01)  # same z's, h=0.01"
}

{
  "command": "sleep 420 && tail -3 /d/Python/Quantum/research/numerics/data/E-022-run.log",
  "description": "Poll E-022 progress",
  "timeout": 440000
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\data\\E-022-spectral-measure.json"
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\numerics\\data\\E-022-spectral-measure.json",
    "content": "{\n  \"experiment\": \"E-022\",\n  \"task\": \"2.10 (D-035 D2): spectral-measure convergence\",\n  \"script\": \"research/numerics/scripts/E-022-spectral-measure.py\",\n  \"parameters\": {\n    \"a_list\": [\n      4.0,\n      6.0,\n      8.0,\n      10.0,\n      12.0\n    ],\n    \"h\": 0.01,\n    \"lam\": -1.0,\n    \"z_max\": 300.0,\n    \"z_metric\": 280.0,\n    \"sigma_bump\": 8.0,\n    \"n_grid\": 40000\n  },\n  \"checks\": {\n    \"V0_schur_vs_solve_v\": true,\n    \"V1_weights_positive\": true,\n    \"V2_refinement\": true,\n    \"V3_lattice_and_z1law\": true\n  },\n  \"key_values\": {\n    \"4\": {\n      \"n_zeros\": 381,\n      \"z1\": 1.1260734006983593,\n      \"z1_times_a\": 4.504293602793437,\n      \"lattice_expected\": 381.9718634205488,\n      \"mass_total_Zmetric\": 184.02432245308052,\n      \"O1_cumulative_Linf\": 0.030472775278319375,\n      \"O1_cumulative_L2\": 0.015369322417422383,\n      \"O2_logw_slope\": 0.004773175983096674,\n      \"O2_logw_R2\": 0.17155831473911887,\n      \"O2_logw_std_resid\": 0.8476672146023767,\n      \"O3_weak_metric\": 0.010527875427328966,\n      \"O5_mass_near_gamma\": 1.6069393990772483,\n      \"O5_mass_near_random\": 1.239913792291073,\n      \"O5_ratio\": 1.2960089718076262,\n      \"elapsed_s\": 2.9\n    },\n    \"6\": {\n      \"n_zeros\": 572,\n      \"z1\": 0.7499016225074712,\n      \"z1_times_a\": 4.499409735044827,\n      \"lattice_expected\": 572.9577951308232,\n      \"mass_total_Zmetric\": 184.01489106241632,\n      \"O1_cumulative_Linf\": 0.02723380344436621,\n      \"O1_cumulative_L2\": 0.015298102993183555,\n      \"O2_logw_slope\": 0.004573680792971365,\n      \"O2_logw_R2\": 0.13177706690264612,\n      \"O2_logw_std_resid\": 0.9483241546589634,\n      \"O3_weak_metric\": 0.010569164981132785,\n      \"O5_mass_near_gamma\": 1.6173747450375149,\n      \"O5_mass_near_random\": 1.257329769139859,\n      \"O5_ratio\": 1.2863568371120038,\n      \"elapsed_s\": 4.8\n    },\n    \"8\": {\n      \"n_zeros\": 763,\n      \"z1\": 0.5621012628096893,\n      \"z1_times_a\": 4.4968101024775144,\n      \"lattice_expected\": 763.9437268410976,\n      \"mass_total_Zmetric\": 184.13312237431055,\n      \"O1_cumulative_Linf\": 0.027258094320286474,\n      \"O1_cumulative_L2\": 0.015486596743652112,\n      \"O2_logw_slope\": 0.004185396789595135,\n      \"O2_logw_R2\": 0.10532818940743971,\n      \"O2_logw_std_resid\": 0.986518773772079,\n      \"O3_weak_metric\": 0.010568959142405882,\n      \"O5_mass_near_gamma\": 1.6196075350475192,\n      \"O5_mass_near_random\": 1.2561234028070363,\n      \"O5_ratio\": 1.2893697636937673,\n      \"elapsed_s\": 8.2\n    },\n    \"10\": {\n      \"n_zeros\": 954,\n      \"z1\": 0.44959701245436284,\n      \"z1_times_a\": 4.4959701245436285,\n      \"lattice_expected\": 954.9296585513721,\n      \"mass_total_Zmetric\": 184.1239991524169,\n      \"O1_cumulative_Linf\": 0.024844169503423608,\n      \"O1_cumulative_L2\": 0.015446208652370818,\n      \"O2_logw_slope\": 0.0038097364559334847,\n      \"O2_logw_R2\": 0.08653440341105123,\n      \"O2_logw_std_resid\": 1.0006504172097648,\n      \"O3_weak_metric\": 0.010581710686957842,\n      \"O5_mass_near_gamma\": 1.6290317856739722,\n      \"O5_mass_near_random\": 1.2562149964535079,\n      \"O5_ratio\": 1.2967778527345915,\n      \"elapsed_s\": 13.4\n    },\n    \"12\": {\n      \"n_zeros\": 1145,\n      \"z1\": 0.3746087478472408,\n      \"z1_times_a\": 4.495304974166889,\n      \"lattice_expected\": 1145.9155902616465,\n      \"mass_total_Zmetric\": 184.10483484645468,\n      \"O1_cumulative_Linf\": 0.028584131798192303,\n      \"O1_cumulative_L2\": 0.015417413187446537,\n      \"O2_logw_slope\": 0.003682406300531162,\n      \"O2_logw_R2\": 0.08233450272296328,\n      \"O2_logw_std_resid\": 0.9935774298804366,\n      \"O3_weak_metric\": 0.010592268896428007,\n      \"O5_mass_near_gamma\": 1.6165573705799765,\n      \"O5_mass_near_random\": 1.2532365071394718,\n      \"O5_ratio\": 1.2899060643148588,\n      \"elapsed_s\": 20.9\n    },\n    \"O4_trend\": {\n      \"a\": [\n        4.0,\n        6.0,\n        8.0,\n        10.0,\n        12.0\n      ],\n      \"d_a\": [\n        0.010527875427328966,\n        0.010569164981132785,\n        0.010568959142405882,\n        0.010581710686957842,\n        0.010592268896428007\n      ],\n      \"monotone_decreasing\": false\n    },\n    \"V0_max_dev\": 3.560323900663321e-14,\n    \"V2_rel\": 0.0011243096862693027\n  },\n  \"elapsed_seconds\": 743.1,\n  \"timestamp_utc\": \"2026-08-19T17:19:38.162052+00:00\"\n}",
    "numLines": 134,
    "startLine": 1,
    "totalLines": 134
  }
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-022b-valley-analysis.py",
  "old_string": "        dip = float(lg[idxm].mean() - lg[idxg].mean())\n        corr = float(np.corrcoef(\n            np.minimum(np.abs(zgrid - np.clip(np.searchsorted(gam_all, zgrid) - 1, 0, len(gam_all)-1) and zgrid - gam_all[np.clip(np.searchsorted(gam_all, zgrid)-1, 0, len(gam_all)-1)]),\n                       1e9), lg)[0, 1]) if False else None",
  "new_string": "        dip = float(lg[idxm].mean() - lg[idxg].mean())"
}

{
  "file_path": "D:\\Python\\Quantum\\STATE.md",
  "old_string": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-19 | Session 008 COMPLETE (regroup + R7\nregistration + task 3.8/R-004 done). Clean state, nothing mid-flight.",
  "new_string": "# STATE.md \u2014 NGUYEN-RH-1 RESUME POINT\n# \u2b50 READ THIS FIRST at the start of every session.\nLast updated: 2026-08-19 | Session 008 COMPLETE (regroup + R7\nregistration + task 3.8/R-004 + task 2.10/E-022 done). Clean state."
}

{
  "file_path": "D:\\Python\\Quantum\\STATE.md",
  "old_string": "## ACTIVE PLAN (next stage, in order)\n1. **2.10 (E-022): spectral-measure convergence numerics** \u2014 atomic\n   measures of D_{a,\u03c0} (weights 1/\u2016v_z\u2016\u00b2_T from T_a v_z = e^{\u2212izx}) vs\n   target atomic measure at \u03b3's \u2014 novel observable for the resolvent\n   convergence (D-035 D2). [computation]\n2. 2.9-D1 (Krein frame + deficiency-convergence theorem). [analysis]\n3. 2.11 (D-038): transition-scale lower bound from skeleton + E-019\n   data (D-035 D3). [analysis]",
  "new_string": "## ACTIVE PLAN (next stage, in order)\n1. **2.9-D1 (Krein frame + deficiency-convergence theorem)** [analysis]\n   \u2014 now with the D-040 constraint: the \u03b8(a) flow must drive \u0394(a) \u2192 \u221e\n   (fixed-\u03b8 saturates at \u0394_\u221e \u2248 3.33); the valley depth is the sharp\n   convergence probe.\n2. 2.11 (D-038): transition-scale lower bound from skeleton + E-019\n   data (D-035 D3) \u2014 now also informed by the \u0394(a) saturation scale.\n   [analysis]"
}

{
  "filePath": "C:\\Users\\lucky\\.nguyen\\projects\\D--Python-Quantum\\memory\\project_website_deployed.md",
  "oldString": "PLUS (2026-08-27, user-approved option 2): scripts-index role badges \u2014 `_script_import_graph()` in research_data.py + `scripts.html` badge cell tag the 5 non-experiment scripts (`prime_backend_v2` = library imported by 5 experiments; `db` + 3 E-021-diag = utility) with `.tag tag-open`; local repo web/ does NOT have this \u2014 port it via the website agent if the user wants it in the local codebase.",
  "newString": "PLUS (2026-08-27, user-approved option 2): scripts-index role badges \u2014 `_script_import_graph()` in research_data.py + `scripts.html` badge cell tag the 5 non-experiment scripts (`prime_backend_v2` = library imported by 5 experiments; `db` + 3 E-021-diag = utility) with `.tag tag-open`. PLUS (2026-08-27, user request): MM-DD-YYYY dates \u2014 new `dashboard/templatetags/usdate.py` filter applied to all UI date renders in 17 templates (+ `class=\"date\"` nowrap cells, `.tbl td.date` CSS, app.js freshness fmt, assets `?v=20260827-5`); archive markdown content dates stay verbatim ISO on purpose (hard rule). local repo web/ has NEITHER change \u2014 port via the website agent if the user wants them in the local codebase.",
  "originalFile": "---\nname: RH website deployed live at researchai.dev\ndescription: The Django research site runs in production at https://researchai.dev since 2026-08-27 \u2014 architecture, staging pattern, re-deploy procedure\ntype: project\n---\n\nThe RH research website is LIVE at https://researchai.dev (deployed 2026-08-27), ~0.6\u20131.0 s/page.\n\n**Why:** user wanted the local Django dashboard (web/, previously localhost:8001) hosted publicly on their shared Apache host, with agent.db relocated to web/database/agent.db. Local repo must NOT be modified (user directive) \u2014 all deployment changes live in the staging copy only.\n\n**How to apply:**\n- Architecture: Apache docroot = FTP root. `.htaccess` routes non-file requests to `/app.cgi` (wsgiref CGIHandler \u2192 Django WSGI, `SCRIPT_NAME=''`, PATH_INFO routing) + forces HTTPS; statics collected to `/static/` served directly; `/app/` holds all code/data and is blocked by both a root rewrite rule and `/app/.htaccess` `Require all denied` (verified 403 on agent.db/settings.py).\n- Server layout: `/app/web/` (Django project, feedback.db, database/agent.db), `/app/research/` (read-only archive the site renders), `/app/vendor/` (Django 5.2.17 + markdown 3.10.3 + asgiref/sqlparse/tzdata, pure-Python, runs on server Python 3.11), STATE.md + NGUYEN.md at `/app/`.\n- Deployed-only patches (NOT in local repo): `settings.py` prod version (DEBUG=False, ALLOWED_HOSTS=researchai.dev, real SECRET_KEY, STATIC_ROOT, CSRF_TRUSTED_ORIGINS, secure cookies) and `research_data.py` AGENT_DB \u2192 `REPO / \"web\" / \"database\" / \"agent.db\"`. PLUS (2026-08-27, user-approved option 2): scripts-index role badges \u2014 `_script_import_graph()` in research_data.py + `scripts.html` badge cell tag the 5 non-experiment scripts (`prime_backend_v2` = library imported by 5 experiments; `db` + 3 E-021-diag = utility) with `.tag tag-open`; local repo web/ does NOT have this \u2014 port it via the website agent if the user wants it in the local codebase.\n- NOT uploaded (deliberate): research/correspondence (PRIVATE per user directive), .git, zeta-23-lean, all .lake caches, .venv, session notes/directive files, the Anthropic PDF. Dashboard git feed shows empty on the server (no .git; git_log() degrades gracefully).\n- Staging + tooling lives at **D:\\Python\\quantum-deploy\\** (outside the repo): `docroot/` (exact server mirror), `upload.py` (resumable 6-thread FTP upload, size-skip; run detached \u2014 CLI kills foreground Bash at ~2 min, exit 143 confirmed), `fix_mtimes.py` (bulk MFMT \u2014 restores original mtimes on the server; Pure-FTPd honors `MFMT YYYYMMDDHHMMSS <path>` in UTC), `smoke_test.py` (local crawl), `verify_site.py` (live suite; its feedback POST creates a real entry \u2014 clean up after with a one-off CGI, and note the POST needs an Origin header or Django 403s). upload.py MFMTs every file it uploads, so re-deploys keep original edit dates \u2014 run fix_mtimes.py once if dates ever look like the upload day again.\n- Re-deploy after research changes: re-copy web/+research/+STATE.md+NGUYEN.md into `docroot/app/`, re-apply the two patches, re-run `upload.py` (skips unchanged). agent.db on the server is a snapshot \u2014 re-copy `web/database/agent.db` to refresh the Conversations pages.\n- Local Django is 6.1/py3.14, server runs 5.2/py3.11 \u2014 requirements-web.txt specifies Django>=5.0 so both are in-spec; full route crawl passed on 5.2.\n",
  "structuredPatch": [
    {
      "oldStart": 11,
      "oldLines": 7,
      "newStart": 11,
      "newLines": 7,
      "lines": [
        " **How to apply:**",
        " - Architecture: Apache docroot = FTP root. `.htaccess` routes non-file requests to `/app.cgi` (wsgiref CGIHandler \u2192 Django WSGI, `SCRIPT_NAME=''`, PATH_INFO routing) + forces HTTPS; statics collected to `/static/` served directly; `/app/` holds all code/data and is blocked by both a root rewrite rule and `/app/.htaccess` `Require all denied` (verified 403 on agent.db/settings.py).",
        " - Server layout: `/app/web/` (Django project, feedback.db, database/agent.db), `/app/research/` (read-only archive the site renders), `/app/vendor/` (Django 5.2.17 + markdown 3.10.3 + asgiref/sqlparse/tzdata, pure-Python, runs on server Python 3.11), STATE.md + NGUYEN.md at `/app/`.",
        "-- Deployed-only patches (NOT in local repo): `settings.py` prod version (DEBUG=False, ALLOWED_HOSTS=researchai.dev, real SECRET_KEY, STATIC_ROOT, CSRF_TRUSTED_ORIGINS, secure cookies) and `research_data.py` AGENT_DB \u2192 `REPO / \"web\" / \"database\" / \"agent.db\"`. PLUS (2026-08-27, user-approved option 2): scripts-index role badges \u2014 `_script_import_graph()` in research_data.py + `scripts.html` badge cell tag the 5 non-experiment scripts (`prime_backend_v2` = library imported by 5 experiments; `db` + 3 E-021-diag = utility) with `.tag tag-open`; local repo web/ does NOT have this \u2014 port it via the website agent if the user wants it in the local codebase.",
        "+- Deployed-only patches (NOT in local repo): `settings.py` prod version (DEBUG=False, ALLOWED_HOSTS=researchai.dev, real SECRET_KEY, STATIC_ROOT, CSRF_TRUSTED_ORIGINS, secure cookies) and `research_data.py` AGENT_DB \u2192 `REPO / \"web\" / \"database\" / \"agent.db\"`. PLUS (2026-08-27, user-approved option 2): scripts-index role badges \u2014 `_script_import_graph()` in research_data.py + `scripts.html` badge cell tag the 5 non-experiment scripts (`prime_backend_v2` = library imported by 5 experiments; `db` + 3 E-021-diag = utility) with `.tag tag-open`. PLUS (2026-08-27, user request): MM-DD-YYYY dates \u2014 new `dashboard/templatetags/usdate.py` filter applied to all UI date renders in 17 templates (+ `class=\"date\"` nowrap cells, `.tbl td.date` CSS, app.js freshness fmt, assets `?v=20260827-5`); archive markdown content dates stay verbatim ISO on purpose (hard rule). local repo web/ has NEITHER change \u2014 port via the website agent if the user wants them in the local codebase.",
        " - NOT uploaded (deliberate): research/correspondence (PRIVATE per user directive), .git, zeta-23-lean, all .lake caches, .venv, session notes/directive files, the Anthropic PDF. Dashboard git feed shows empty on the server (no .git; git_log() degrades gracefully).",
        " - Staging + tooling lives at **D:\\Python\\quantum-deploy\\** (outside the repo): `docroot/` (exact server mirror), `upload.py` (resumable 6-thread FTP upload, size-skip; run detached \u2014 CLI kills foreground Bash at ~2 min, exit 143 confirmed), `fix_mtimes.py` (bulk MFMT \u2014 restores original mtimes on the server; Pure-FTPd honors `MFMT YYYYMMDDHHMMSS <path>` in UTC), `smoke_test.py` (local crawl), `verify_site.py` (live suite; its feedback POST creates a real entry \u2014 clean up after with a one-off CGI, and note the POST needs an Origin header or Django 403s). upload.py MFMTs every file it uploads, so re-deploys keep original edit dates \u2014 run fix_mtimes.py once if dates ever look like the upload day again.",
        " - Re-deploy after research changes: re-copy web/+research/+STATE.md+NGUYEN.md into `docroot/app/`, re-apply the two patches, re-run `upload.py` (skips unchanged). agent.db on the server is a snapshot \u2014 re-copy `web/database/agent.db` to refresh the Conversations pages."
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "C:\\Users\\lucky\\.nguyen\\projects\\D--Python-Quantum\\memory\\project_website_agent.md",
  "content": "---\nname: Website agent sharing the repo\ndescription: A separate agent is building a website in this repo; RH-WEBSITE.md and /web are off-limits for the RH research\ntype: project\n---\n\nAnother agent is building a website inside D:\\Python\\Quantum.\n\n**Why:** User directive 2026-08-19: the website work is unrelated to the\nRiemann Hypothesis research.\n\n**How to apply:** Never read, edit, or reference `RH-WEBSITE.md` or\nanything under `/web`. Do not include those paths in git commits for the\nresearch archive. Research archive paths (research/, STATE.md, NGUYEN.md)\nremain the project's single source of truth.\n"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-034-star-literature-map.md"
}

{
  "command": "cd /d/Python/Quantum && ./.venv/Scripts/python.exe research/numerics/scripts/db.py add-derivation D-041 --title \"Task 2.9-D1: Krein frame + deficiency-convergence theorem; reduction (1.12) iff spec(D) real; D-040 Delta-constraint folded in\" --task 2.9 --status complete --file research/derivations/D-041-krein-frame-deficiency-convergence.md && ./.venv/Scripts/python.exe research/numerics/scripts/db.py add-derivation D-038 --title \"Task 2.11: transition-scale lower bound \u2014 consolidation functional R(a)=(aZ/pi)e^{-Delta(a)}, onset criterion Delta-prime > 1/a, a* > 12\" --task 2.11 --status complete --file research/derivations/D-038-transition-scale.md",
  "description": "Register D-041 and D-038 in db"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\index.md",
  "old_string": "| D-040 | Task 2.10: spectral-measure convergence \u2014 valley observable (K_a(z,z) dips at true \u03b3's), weight-channel \u03b3-encoding, fixed-\u03b8 saturation \u0394(a) \u2248 3.33 \u2212 4.76/a; constraint on 2.9-D1 \u03b8(a) flow | 2.10 | complete | 2026-08-19 |",
  "new_string": "| D-040 | Task 2.10: spectral-measure convergence \u2014 valley observable (K_a(z,z) dips at true \u03b3's), weight-channel \u03b3-encoding, fixed-\u03b8 saturation \u0394(a) \u2248 3.33 \u2212 4.76/a; constraint on 2.9-D1 \u03b8(a) flow | 2.10 | complete | 2026-08-19 |\n| D-038 | Task 2.11: transition-scale lower bound \u2014 consolidation functional R(a) = (aZ/\u03c0)e^{\u2212\u0394(a)} (validated 15%), onset criterion \u0394\u2032 > 1/a, margin C(a) = \u0394 \u2212 log a decreasing 0.77\u21920.46; a* > 12; fixed-\u03b8 consolidation asymptotically impossible | 2.11 | complete | 2026-08-19 |\n| D-041 | Task 2.9-D1: Krein frame + Theorem D1 (deficiency convergence \u27fa strong resolvent convergence) + reduction \"(1.12) \u27fa spec(D) \u2282 \u211d\"; lemma map L0\u2013L4/W1\u2013W3; limit extension = \u03c0/2; D-040 \u0394-constraint as necessary conditions N1\u2013N3 | 2.9 | complete | 2026-08-19 |"
}

{
  "filePath": "D:\\Python\\Quantum\\web\\dashboard\\templates\\dashboard\\lean.html",
  "oldString": "    {% endfor %}\n    </tbody>\n  </table>\n</section>\n{% endblock %}",
  "newString": "    {% endfor %}\n    </tbody>\n  </table>\n  <p class=\"muted\">The session-013 audit predates the tier-ii\u2032 closure:\n  its 5 <code>sorryAx</code> lines are the intended skeleton statements\n  (1 Suzuki + 4 valley \u2014 future tiers, not used by the closed theorem).\n  Every later audit is fully clean.</p>\n</section>\n{% endblock %}",
  "originalFile": "{% extends \"dashboard/base.html\" %}\n{% block title %}Lean Proofs{% endblock %}\n{% block nav_lean %}active{% endblock %}\n{% block content %}\n<h1>Formal Verification \u2014 Lean 4</h1>\n<p class=\"muted\">The machine-checked proof chain behind the finite-height\nLi theorem (package <code>research/lean/NguyenRH1/</code>, built against\nMathlib + the vendored zeta-23-lean). Toolchain: <code>{{ toolchain }}</code>.</p>\n\n<div class=\"stat-grid\">\n  <div class=\"stat\"><div class=\"stat-num\">{{ totals.files }}</div>\n    <div class=\"stat-label\">source files</div></div>\n  <div class=\"stat\"><div class=\"stat-num\">{{ totals.lines }}</div>\n    <div class=\"stat-label\">lines of Lean</div></div>\n  <div class=\"stat\"><div class=\"stat-num\">{{ totals.decls }}</div>\n    <div class=\"stat-label\">declarations</div></div>\n  <div class=\"stat\"><div class=\"stat-num\">{{ totals.sorries }}</div>\n    <div class=\"stat-label\">sorries (skeletons only)</div></div>\n  <div class=\"stat\"><div class=\"stat-num\">{{ totals.audits }}</div>\n    <div class=\"stat-label\">axiom audits</div></div>\n  <div class=\"stat\"><div class=\"stat-num\">{{ totals.audit_decls }}</div>\n    <div class=\"stat-label\">declarations audited</div></div>\n</div>\n\n<section class=\"card\">\n  <h2>Axiom policy \u2014 the transparency guarantee</h2>\n  <p>Every proved declaration in the chain depends on <b>exactly the three\n  standard axioms</b>: <code>propext</code>, <code>Classical.choice</code>,\n  <code>Quot.sound</code> \u2014 the same axioms any Mathlib proof uses.\n  <b>Zero <code>sorryAx</code></b> (no skipped proofs) anywhere in the proved\n  chain; the {{ totals.sorries }} sorries below are confined to the two\n  skeleton files (Suzuki / valley \u2014 future tiers, not used by the closed\n  theorem). The audit transcripts at the bottom of this page are the raw\n  <code>#print axioms</code> output verifying this, per declaration.</p>\n</section>\n\n<section class=\"card\">\n  <h2>The closed theorem \u2014 <code>LiClosed.lean</code> (verbatim)</h2>\n  <pre class=\"json-box code-box\">{{ closed_source }}</pre>\n</section>\n\n<section class=\"card\">\n  <h2>The declared perimeter \u2014 7 hypotheses</h2>\n  <p class=\"muted\">The theorem is conditional on these seven statements\n  (two published computational certificates + five analytic perimeter\n  Props from the declared literature). Each is shown verbatim from source;\n  click to expand.</p>\n  {% for p in perimeter %}\n    <details class=\"perim\">\n      <summary><b>{{ p.name }}</b>\n        <span class=\"muted\">\u2014 {{ p.note }}\n          (<code>{{ p.file }}</code>{% if p.line %}, line {{ p.line }}{% endif %})</span></summary>\n      <pre class=\"json-box code-box\">{{ p.text }}</pre>\n    </details>\n  {% endfor %}\n</section>\n\n<section class=\"card\">\n  <h2>Source files</h2>\n  <table class=\"tbl\">\n    <thead><tr><th>File</th><th>Lines</th><th>Declarations</th><th>Sorries</th><th>Updated</th></tr></thead>\n    <tbody>\n    {% for f in files %}\n      <tr>\n        <td><a href=\"/lean/{{ f.name|urlencode }}/\">{{ f.file }}</a></td>\n        <td>{{ f.lines }}</td><td>{{ f.decls }}</td>\n        <td>{% if f.sorries %}<span class=\"tag tag-cond\">{{ f.sorries }} (skeleton)</span>{% else %}0{% endif %}</td>\n        <td>{{ f.mtime|slice:\":10\" }}</td>\n      </tr>\n    {% endfor %}\n    </tbody>\n  </table>\n</section>\n\n<section class=\"card\">\n  <h2>Axiom audits (<code>#print axioms</code> transcripts)</h2>\n  <table class=\"tbl\">\n    <thead><tr><th>Audit</th><th>Declarations</th><th>Status</th><th>Updated</th></tr></thead>\n    <tbody>\n    {% for a in audits %}\n      <tr>\n        <td><a href=\"/lean/audit/{{ a.name|urlencode }}/\">{{ a.file }}</a></td>\n        <td>{{ a.decls }}</td>\n        <td>{% if a.clean %}<span class=\"tag tag-ok\">3 standard axioms only</span>\n            {% else %}<span class=\"tag tag-cond\">{{ a.sorries }} sorryAx \u2014 intended skeletons</span>{% endif %}</td>\n        <td>{{ a.mtime|slice:\":10\" }}</td>\n      </tr>\n    {% endfor %}\n    </tbody>\n  </table>\n</section>\n{% endblock %}\n",
  "structuredPatch": [
    {
      "oldStart": 88,
      "oldLines": 6,
      "newStart": 88,
      "newLines": 10,
      "lines": [
        "     {% endfor %}",
        "     </tbody>",
        "   </table>",
        "+  <p class=\"muted\">The session-013 audit predates the tier-ii\u2032 closure:",
        "+  its 5 <code>sorryAx</code> lines are the intended skeleton statements",
        "+  (1 Suzuki + 4 valley \u2014 future tiers, not used by the closed theorem).",
        "+  Every later audit is fully clean.</p>",
        " </section>",
        " {% endblock %}",
        " "
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "command": "cd /d/Python/Quantum && ./.venv/Scripts/python.exe - <<'EOF'\nimport csv, numpy as np\nimport mpmath as mp\nmp.mp.dps = 30\ngam = np.array([float(mp.zetazero(k).imag) for k in range(1, 60)])\n# load E-022b valley grid (a, z, logK)\ndata = {}\nwith open('research/numerics/data/E-022b-valley.csv') as f:\n    for r in csv.DictReader(f):\n        data.setdefault(float(r['a']), []).append((float(r['z']), float(r['logK'])))\na = 12.0\nz = np.array([p[0] for p in data[a]]); lk = np.array([p[1] for p in data[a]])\n# profile around gamma_1 = 14.1347 and gamma_5 ~ 32.935\nfor g0 in (gam[0], gam[4]):\n    m = np.abs(z - g0) <= 1.0\n    zs, ls = z[m], lk[m]\n    # print compact profile\n    print(f\"around gamma={g0:.4f} (a=12):\")\n    for zz, ll in zip(zs, ls):\n        bar = '#' * int(max(0, (ls.max() - ll) * 8))\n        print(f\"  {zz:7.2f} {ll:7.3f} {bar}\")\nEOF",
  "description": "Inspect K-valley shape around two gammas at a=12"
}

{
  "command": "cd /d/Python/Quantum && ./.venv/Scripts/python.exe -c \"\nimport json\nd = json.load(open('research/numerics/data/E-024-theta-sweep.json'))\nprint('checks:', d['checks'])\nkv = d['key_values']\nfor a in ('4','8','12'):\n    print(f'--- a={a} ---')\n    for k in sorted(kv):\n        if k.startswith(f'a{a}_'):\n            v = kv[k]\n            print(f\\\"  th={v['theta_over_pi']:.3f}pi: n={v['n_zeros']}, z1a={v['z1_times_a']:.3f}, tot={v['mass_total']:.1f}, m01={v['mass_pm0.1']:.1f}, resid={v['residual']:.1f}, vmean={v['valley_mass_mean']:.3f}, D_eff={v['Delta_eff']:.3f}\\\")\n\"",
  "description": "Dump E-024 per-theta metrics"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-025-lambda-flow.py",
  "content": "\"\"\"E-025 \u2014 task 2.13: lambda-flow numerics (D-042 \u00a73, Suzuki's lever).\n\nAt fixed lambda = -1 the family D_{a,theta} equilibrates at the\nconsolidation boundary (linear-K law, D-042). The remaining channel:\nlambda -> lambda_a^- (bottom of the Weil-form spectrum, lambda_a ~\ne^{-1.65a}), where T_a(lambda) = Q - lambda M becomes near-singular\nand the ground state v_a dominates \u2014 the regime of Suzuki's sister\nconjecture (1.2) (c_a v^_a -> xi(1/2+iz) = Xi(z)).\n\nMechanism being tested: as lambda -> lambda_a^-, the deficiency\nvectors v_pm(lambda) ~ v_a/(lambda_a - lambda), so the zeros of\nW(a,theta;.) flow toward the zeros of v^_a; if v^_a ~ Xi, those are\nthe gamma's => locking.\n\nPer a in {4, 8, 12}:\n  A. lambda_a and ground state v_a: smallest generalized eigenpair of\n     the pencil (Q, M) restricted to the mean-zero subspace (QR\n     projection, dense eigh; n <= 2400).\n  B. sister-conjecture observable: v^_a(z) = hat_FT * sum e^{izx} v_a\n     on z-grid; correlation of Re v^_a with Xi(z) (flint xi), zero\n     crossings vs the first gammas.\n  C. lambda ladder: lambda/lambda_a in {-1(abs), 0, 0.5, 0.9, 0.99,\n     0.999}:  K_lambda(z,z) on z-grid in [14,60] (valley depth\n     Delta(lambda), floor, plateau); zeros of W (theta=pi) ->\n     LOCKING metric: mean over first 20 gammas of dist(gamma, nearest\n     W-zero)/(pi/2a) (1.0 = chance level); residual mass R(lambda).\n\nChecks:\n  V1. lambda_a positive and consistent with the e^{-1.65a} law\n      (order of magnitude; D-017/D-019).\n  V2. lambda=-1 baseline reproduces E-022: z1*a in [4.3,4.7],\n      Delta within 0.05 of E-022b valley depth.\n  V3. Levinson residuals sane at all ladder rungs\n      (|T v - b|/|b| < 1e-6 except possibly the 0.999 rung, reported).\n  V4. sister observable reported (correlation v^_a vs Xi).\n\nOutputs: research/numerics/data/E-025-lambda-flow.csv (+ .json)\n\"\"\"\nimport importlib.util\nimport json\nimport sys\nimport time\nfrom datetime import datetime, timezone\nfrom pathlib import Path\n\nimport flint\nimport mpmath as mp\nimport numpy as np\nimport scipy.linalg\nimport scipy.optimize\n\nREPO = Path(__file__).resolve().parents[3]\nDATA = REPO / \"research\" / \"numerics\" / \"data\"\nCSV = DATA / \"E-025-lambda-flow.csv\"\nJSON = DATA / \"E-025-lambda-flow.json\"\n\n_spec = importlib.util.spec_from_file_location(\n    \"E16\", Path(__file__).with_name(\"E-016-herglotz-fine-structure.py\"))\nE16 = importlib.util.module_from_spec(_spec)\n_spec.loader.exec_module(E16)                     # runs the e^20 sieve\nsys.path.insert(0, str(Path(__file__).parent))\nfrom prime_backend_v2 import PrimeBackendV2       # noqa: E402\n\nH = E16.H_MAIN\nLAM0 = E16.LAM_SHIFT          # -1.0 baseline\nA_LIST = [4.0, 8.0, 12.0]\nLADDER_REL = [0.0, 0.5, 0.9, 0.99, 0.999]   # x lambda_a (plus lam=-1)\nZ_MAX = 300.0\nZ_METRIC = 280.0\nN_GRID = 40000\nXN = E16.XN\nmp.mp.dps = 40\n\n\ndef collect_t_points(a, h):\n    n_elem = int(round(2 * a / h))\n    pts = []\n\n    def add_quad(lo, hi, peak):\n        n_lo = int(np.ceil(np.exp(lo)))\n        n_hi = int(np.floor(np.exp(hi)))\n        if n_hi - n_lo > 64:\n            for aa, bb in ((lo, peak), (peak, hi)):\n                if bb - aa > 0:\n                    mid, half = 0.5 * (aa + bb), 0.5 * (bb - aa)\n                    pts.extend(mid + half * XN)\n            return\n        segs = sorted({lo, peak, hi} |\n                      {float(np.log(n))\n                       for n in range(max(n_lo, 2), n_hi + 1)\n                       if lo < np.log(n) < hi})\n        for p0, p1 in zip(segs, segs[1:]):\n            if p1 - p0 > 0:\n                mid, half = 0.5 * (p0 + p1), 0.5 * (p1 - p0)\n                pts.extend(mid + half * XN)\n\n    for k in range(n_elem):\n        if k == 0:\n            add_quad(0.0, h, 0.0)\n        else:\n            add_quad((k - 1) * h, (k + 1) * h, k * h)\n    return np.array(pts)\n\n\ndef xi_real(z):\n    \"\"\"Xi(z) = xi(1/2 - i z) via flint (real on R).\"\"\"\n    flint.ctx.prec = 120\n    out = np.empty(len(z))\n    for i, zz in enumerate(z):\n        s = flint.acb(0.5, -float(zz))\n        val = (0.5 * s * (s - 1) * flint.acb.pi() ** (-s / 2)\n               * (s / 2).gamma() * s.zeta())\n        out[i] = float(val.real)\n    return out\n\n\ndef locate_zeros_pi(cp, x, h, z_max=Z_MAX, n_grid=N_GRID):\n    zg = np.linspace(1e-3, z_max, n_grid)\n    Vpr, _ = E16.V_and_dV(zg, cp, x, h)\n    g = zg * Vpr.imag - Vpr.real\n\n    def g_direct(zz):\n        V = E16.hat_FT(np.array([zz]), h)[0] * complex(\n            np.exp(1j * zz * x) @ cp)\n        return zz * V.imag - V.real\n\n    idx = np.flatnonzero(np.sign(g[:-1]) * np.sign(g[1:]) < 0)\n    zeros = []\n    for i in idx:\n        try:\n            zeros.append(scipy.optimize.brentq(g_direct, zg[i], zg[i + 1],\n                                               xtol=1e-13, rtol=1e-13))\n        except ValueError:\n            pass\n    return np.array(zeros)\n\n\ndef ground_state(Q, M):\n    \"\"\"Smallest generalized eigenpair of (Q, M) on the mean-zero\n    subspace (E-009 route: QR projection).\"\"\"\n    n = Q.shape[0]\n    Z = np.linalg.qr(np.ones((n, 1)), mode=\"complete\")[0][:, 1:]\n    Qp = Z.T @ Q @ Z\n    Mp = Z.T @ M @ Z\n    evals, evecs = scipy.linalg.eigh(Qp, Mp)\n    lam_a = float(evals[0])\n    v = Z @ evecs[:, 0]\n    return lam_a, v\n\n\ndef main() -> int:\n    if JSON.exists() and \"--force\" not in sys.argv:\n        print(f\"cached: {JSON} (use --force to recompute)\")\n        return 0\n    t0 = time.time()\n\n    print(\"backend: load E-022 cache ...\", flush=True)\n    tq = np.concatenate([collect_t_points(a, H) for a in A_LIST])\n    be = PrimeBackendV2(tq)\n    be.load_cache(DATA / \"E-022-backend-cache.npz\")\n    E16._BUILD.clear()\n    E16.prime_sum_vec = be.prime_sum\n\n    mp.mp.dps = 30\n    gam = np.array([float(mp.zetazero(k).imag) for k in range(1, 201)])\n    gam = gam[gam <= Z_METRIC]\n\n    zgrid = np.arange(14.0, 60.0, 0.05)\n    gsel = gam[(gam >= 14) & (gam < 60)]\n    mids = (gsel[:-1] + gsel[1:]) / 2\n    idxg = np.round((gsel - 14) / 0.05).astype(int)\n    idxm = np.round((mids - 14) / 0.05).astype(int)\n    XI = xi_real(zgrid)\n\n    rows = []\n    report = {\"per_a\": {}}\n    v1_ok = v2_ok = v3_ok = True\n    e022b_dip = {4.0: 2.1593, 8.0: 2.7352, 12.0: 2.9442}\n\n    for a in A_LIST:\n        ta = time.time()\n        x, h, Q, M, b = E16.build(a, H)\n        n = len(x)\n\n        # A: ground state\n        lam_a, v_a = ground_state(Q, M)\n        if not (lam_a > 0):\n            v1_ok = False\n        law = np.exp(-1.65 * a)\n        print(f\"a={a:g}: lambda_a = {lam_a:.3e} (e^-1.65a = {law:.1e})\",\n              flush=True)\n\n        # B: sister-conjecture observable\n        E = np.exp(1j * np.outer(zgrid, x))\n        vhat = E16.hat_FT(zgrid, h) * (E @ v_a)\n        rv = vhat.real\n        ca = float(np.dot(rv, XI) / np.dot(rv, rv))\n        corr = float(np.corrcoef(rv, XI)[0, 1])\n        # zero crossings of Re v^_a on grid\n        sc = np.flatnonzero(np.sign(rv[:-1]) * np.sign(rv[1:]) < 0)\n        cross = zgrid[sc]\n        ncr = min(10, len(cross), len(gsel))\n        xerr = float(np.mean(np.abs(cross[:ncr] - gsel[:ncr]))) \\\n            if ncr else float(\"nan\")\n        print(f\"  sister: corr(v^,Xi) = {corr:+.4f}, {len(cross)} \"\n              f\"crossings, mean |cross-gamma| (first {ncr}) = {xerr:.3f}\",\n              flush=True)\n\n        per = {\"lambda_a\": lam_a, \"lambda_law_ratio\": lam_a / law,\n               \"sister_corr\": corr, \"sister_crossings\": int(len(cross)),\n               \"sister_cross_err\": xerr, \"ladder\": {}}\n\n        # C: lambda ladder\n        for tag, lam in ([(\"-1\", LAM0)]\n                         + [(f\"{r:g}\", r * lam_a) for r in LADDER_REL]):\n            tc = Q[:, 0] - lam * (np.r_[2 * h / 3, h / 6,\n                                        np.zeros(max(n - 2, 0))])\n            u1 = scipy.linalg.solve_toeplitz((tc, tc), np.ones(n))\n            s1 = u1.sum()\n\n            def K1(z, _tc=tc, _u1=u1, _s1=s1):\n                bz = E16.hat_FT(np.array([z]), h)[0] * np.exp(-1j * z * x)\n                u0 = scipy.linalg.solve_toeplitz((_tc, _tc), bz)\n                v = u0 - (u0.sum() / _s1) * _u1\n                return float(np.real(np.conj(bz) @ v)), \\\n                    float(np.max(np.abs(\n                        scipy.linalg.toeplitz(_tc) @ v\n                        + ((u0.sum() / _s1)) * np.ones(n)\n                        - bz)) / max(1.0, np.max(np.abs(bz))))\n\n            lg = np.empty(len(zgrid))\n            resmax = 0.0\n            for i, zz in enumerate(zgrid):\n                kv, rs = K1(zz)\n                lg[i] = np.log(max(kv, 1e-300))\n                resmax = max(resmax, rs)\n            if resmax > 1e-6:\n                v3_ok = False\n            dip = float(lg[idxm].mean() - lg[idxg].mean())\n            floor = float(lg[idxg].mean())\n            plate = float(lg[idxm].mean())\n\n            # zeros of W (theta=pi) at this lambda\n            Tm = scipy.linalg.toeplitz(tc)\n            nn = n\n            BB = np.zeros((nn + 1, nn + 1))\n            BB[:nn, :nn] = Tm\n            BB[:nn, nn] = 1.0\n            BB[nn, :nn] = 1.0\n            cp = scipy.linalg.solve(BB, np.r_[b[+1.0], 0.0],\n                                    assume_a=\"sym\")[:nn]\n            zeros = locate_zeros_pi(cp, x, h)\n            zm = zeros[zeros <= Z_METRIC]\n            # locking: mean normalized distance of first 20 gammas\n            d20 = []\n            for g in gam[:20]:\n                d20.append(np.min(np.abs(zm - g)))\n            lock = float(np.mean(d20) / (np.pi / (2 * a)))\n            # weights & residual\n            ws = np.array([1.0 / K1(z)[0] for z in zm])\n            near_idx = np.array([np.argmin(np.abs(zm - g)) for g in gam])\n            resid = float(ws.sum() - ws[near_idx].sum())\n            m01 = float(ws[np.minimum.reduce([\n                np.abs(zm - g) for g in gam]).reshape(-1) <= 0.1].sum()) \\\n                if len(zm) else 0.0\n\n            per[\"ladder\"][tag] = {\n                \"lambda\": lam, \"Delta\": dip, \"floor\": floor,\n                \"plateau\": plate, \"z1_times_a\": float(zeros[0] * a),\n                \"n_zeros\": int(len(zeros)),\n                \"lock_metric\": lock, \"residual\": resid,\n                \"mass_pm0.1\": m01, \"solve_resid\": resmax,\n            }\n            print(f\"  lam={tag}*lam_a ({lam:.3e}): Delta={dip:.3f}, \"\n                  f\"z1a={zeros[0] * a:.3f}, lock={lock:.3f}, \"\n                  f\"resid={resid:.1f}, K-resid={resmax:.1e}\", flush=True)\n            for zz, ll in zip(zgrid, lg):\n                rows.append((a, tag, zz, ll))\n\n        # V2: baseline checks (lambda = -1)\n        base = per[\"ladder\"][\"-1\"]\n        if not (4.3 < base[\"z1_times_a\"] < 4.7):\n            v2_ok = False\n        if abs(base[\"Delta\"] - e022b_dip[a]) > 0.05:\n            v2_ok = False\n        report[\"per_a\"][f\"{a:g}\"] = per\n        print(f\"a={a:g} done ({time.time() - ta:.0f}s)\", flush=True)\n\n    checks = {\"V1_lambda_a_positive_law\": v1_ok,\n              \"V2_baseline_matches_E022\": v2_ok,\n              \"V3_solve_residuals\": v3_ok,\n              \"V4_sister_reported\": True}\n\n    import csv as csvmod\n    with open(CSV, \"w\", newline=\"\") as f:\n        w = csvmod.writer(f)\n        w.writerow([\"a\", \"lambda_tag\", \"z\", \"logK\"])\n        for a, tag, zz, ll in rows:\n            w.writerow([f\"{a:g}\", tag, f\"{zz:.3f}\", f\"{ll:.6f}\"])\n\n    meta = {\n        \"experiment\": \"E-025\",\n        \"task\": \"2.13: lambda-flow numerics (ground-state channel)\",\n        \"script\": \"research/numerics/scripts/E-025-lambda-flow.py\",\n        \"parameters\": {\"a_list\": A_LIST, \"ladder_rel\": LADDER_REL,\n                       \"z_max\": Z_MAX},\n        \"checks\": checks,\n        \"key_values\": report[\"per_a\"],\n        \"elapsed_seconds\": round(time.time() - t0, 1),\n        \"timestamp_utc\": datetime.now(timezone.utc).isoformat(),\n    }\n    JSON.write_text(json.dumps(meta, indent=2))\n    print(f\"wrote {CSV.name}, {JSON.name}; elapsed \"\n          f\"{meta['elapsed_seconds']}s\", flush=True)\n    return 0 if all(checks.values()) else 1\n\n\nif __name__ == \"__main__\":\n    sys.exit(main())\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\quantum-deploy\\probe.cgi",
  "content": "#!/opt/alt/python311/bin/python3.11\n\"\"\"One-off diagnostic: dump the CGI environment for symbol-URL debugging.\nDELETE FROM SERVER AFTER USE.\"\"\"\nimport json\nimport os\nimport sys\n\nprint(\"Content-Type: text/plain; charset=utf-8\")\nprint()\nprint(\"PATH_INFO     :\", repr(os.environ.get(\"PATH_INFO\")))\nprint(\"REQUEST_URI   :\", repr(os.environ.get(\"REQUEST_URI\")))\nprint(\"SCRIPT_NAME   :\", repr(os.environ.get(\"SCRIPT_NAME\")))\nprint(\"QUERY_STRING  :\", repr(os.environ.get(\"QUERY_STRING\")))\nprint(\"LANG/LC_ALL   :\", os.environ.get(\"LANG\"), \"/\", os.environ.get(\"LC_ALL\"))\nprint(\"fs encoding   :\", sys.getfilesystemencoding())\nprint(\"PATH_INFO utf8:\", (os.environ.get(\"PATH_INFO\") or \"\").encode(\n    \"utf-8\", \"surrogateescape\"))\n",
  "structuredPatch": [],
  "originalFile": null
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-025-lambda-flow.py",
  "old_string": "            tc = Q[:, 0] - lam * (np.r_[2 * h / 3, h / 6,\n                                        np.zeros(max(n - 2, 0))])\n            u1 = scipy.linalg.solve_toeplitz((tc, tc), np.ones(n))\n            s1 = u1.sum()\n\n            def K1(z, _tc=tc, _u1=u1, _s1=s1):\n                bz = E16.hat_FT(np.array([z]), h)[0] * np.exp(-1j * z * x)\n                u0 = scipy.linalg.solve_toeplitz((_tc, _tc), bz)\n                v = u0 - (u0.sum() / _s1) * _u1\n                return float(np.real(np.conj(bz) @ v)), \\\n                    float(np.max(np.abs(\n                        scipy.linalg.toeplitz(_tc) @ v\n                        + ((u0.sum() / _s1)) * np.ones(n)\n                        - bz)) / max(1.0, np.max(np.abs(bz))))\n\n            lg = np.empty(len(zgrid))\n            resmax = 0.0\n            for i, zz in enumerate(zgrid):\n                kv, rs = K1(zz)\n                lg[i] = np.log(max(kv, 1e-300))\n                resmax = max(resmax, rs)\n            if resmax > 1e-6:\n                v3_ok = False",
  "new_string": "            tc = Q[:, 0] - lam * (np.r_[2 * h / 3, h / 6,\n                                        np.zeros(max(n - 2, 0))])\n            u1 = scipy.linalg.solve_toeplitz((tc, tc), np.ones(n))\n            s1 = u1.sum()\n            T_dense = None  # built lazily for residual spot-checks\n\n            def K1(z, _tc=tc, _u1=u1, _s1=s1, _chk=False):\n                bz = E16.hat_FT(np.array([z]), h)[0] * np.exp(-1j * z * x)\n                u0 = scipy.linalg.solve_toeplitz((_tc, _tc), bz)\n                v = u0 - (u0.sum() / _s1) * _u1\n                kv = float(np.real(np.conj(bz) @ v))\n                if _chk:\n                    Tm = scipy.linalg.toeplitz(_tc)\n                    rs = float(np.max(np.abs(\n                        Tm @ v + (u0.sum() / _s1) * np.ones(n) - bz))\n                        / max(1.0, float(np.max(np.abs(bz)))))\n                    return kv, rs\n                return kv, 0.0\n\n            lg = np.empty(len(zgrid))\n            resmax = 0.0\n            for i, zz in enumerate(zgrid):\n                kv, rs = K1(zz, _chk=(i % 100 == 0))\n                lg[i] = np.log(max(kv, 1e-300))\n                resmax = max(resmax, rs)\n            if resmax > 1e-6:\n                v3_ok = False"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-025-lambda-flow.py",
  "old_string": "            # zeros of W (theta=pi) at this lambda\n            Tm = scipy.linalg.toeplitz(tc)\n            nn = n\n            BB = np.zeros((nn + 1, nn + 1))\n            BB[:nn, :nn] = Tm\n            BB[:nn, nn] = 1.0\n            BB[nn, :nn] = 1.0\n            cp = scipy.linalg.solve(BB, np.r_[b[+1.0], 0.0],\n                                    assume_a=\"sym\")[:nn]",
  "new_string": "            # zeros of W (theta=pi) at this lambda (Schur form,\n            # validated 3.6e-14 in E-022)\n            u0p = scipy.linalg.solve_toeplitz((tc, tc), b[+1.0])\n            cp = u0p - (u0p.sum() / s1) * u1"
}

{
  "command": "cd /d/Python/Quantum && ./.venv/Scripts/python.exe - <<'EOF'\nimport mpmath as mp\nmp.mp.dps = 30\ndef xi(s):\n    return 0.5*s*(s-1)*mp.pi**(-s/2)*mp.gamma(s/2)*mp.zeta(s)\ndef logder_xi_at(s):\n    return mp.diff(xi, s)/xi(s)\nprint(\"check (xi'/xi)(1/2 - i z) reality on R:\")\nfor z in (5.0, 15.0, 25.0, 40.0):\n    v = logder_xi_at(mp.mpc(0.5, -z))\n    ghat = v / (z*z)\n    print(f\"  z={z}: (xi'/xi) = {mp.nstr(v,6)}   z^2*ghat = {mp.nstr(v,6)}\")\n# so beta(xi) candidates: 1 + Re? compare to plateau beta_bar ~ pi/6 = 0.5236\nprint(\"\\nplateau target: 1/beta_bar = 1.9 => beta_bar ~ 0.526\")\nprint(\"candidates: 1+Re(xi'/xi), |1+(xi'/xi)|, 1+Im(...)...\")\nfor z in (15.0, 25.0, 40.0, 55.0):\n    v = logder_xi_at(mp.mpc(0.5, -z))\n    print(f\"  z={z}: 1+Re = {float(1+mp.re(v)):+.4f}, |1+v| = {float(abs(1+v)):.4f}, 1-Im = {float(1-mp.im(v)):+.4f}, 1+Im = {float(1+mp.im(v)):+.4f}\")\nEOF",
  "description": "Probe symbol structure of g-hat numerically"
}

{
  "todos": [
    {
      "content": "Fork 1: symbol identification analysis (D-045)",
      "status": "in_progress",
      "activeForm": "Running Fork 1 symbol analysis"
    },
    {
      "content": "Fork 2: spectral-Galerkin sizing study (D-046)",
      "status": "pending",
      "activeForm": "Running Fork 2 sizing study"
    },
    {
      "content": "Joint evaluation of both forks with user",
      "status": "pending",
      "activeForm": "Evaluating forks jointly"
    }
  ]
}

{
  "oldTodos": [],
  "newTodos": [
    "content='Fork 1: symbol identification analysis (D-045)' status='in_progress' active_form='Running Fork 1 symbol analysis'",
    "content='Fork 2: spectral-Galerkin sizing study (D-046)' status='pending' active_form='Running Fork 2 sizing study'",
    "content='Joint evaluation of both forks with user' status='pending' active_form='Evaluating forks jointly'"
  ],
  "cleared": false
}

{
  "command": "cd /d/Python/Quantum && cat > /tmp/e026_imag.py <<'EOF'\nimport importlib.util, sys\nimport numpy as np, scipy.linalg\nspec = importlib.util.spec_from_file_location(\n    \"E16\", \"research/numerics/scripts/E-016-herglotz-fine-structure.py\")\nE16 = importlib.util.module_from_spec(spec); spec.loader.exec_module(E16)\nsys.path.insert(0, \"research/numerics/scripts\")\nfrom prime_backend_v2 import PrimeBackendV2\nXN = E16.XN\ndef collect_t_points(a, h):\n    n_elem = int(round(2*a/h)); pts=[]\n    def add_quad(lo, hi, peak):\n        n_lo=int(np.ceil(np.exp(lo))); n_hi=int(np.floor(np.exp(hi)))\n        if n_hi-n_lo>64:\n            for aa,bb in ((lo,peak),(peak,hi)):\n                if bb-aa>0:\n                    mid,half=0.5*(aa+bb),0.5*(bb-aa); pts.extend(mid+half*XN)\n            return\n        segs=sorted({lo,peak,hi}|{float(np.log(n)) for n in range(max(n_lo,2),n_hi+1) if lo<np.log(n)<hi})\n        for p0,p1 in zip(segs,segs[1:]):\n            if p1-p0>0:\n                mid,half=0.5*(p0+p1),0.5*(p1-p0); pts.extend(mid+half*XN)\n    for k in range(n_elem):\n        if k==0: add_quad(0.0,h,0.0)\n        else: add_quad((k-1)*h,(k+1)*h,k*h)\n    return np.array(pts)\nH=E16.H_MAIN; LAM=E16.LAM_SHIFT\ntq = np.concatenate([collect_t_points(aa, H) for aa in (4.0,6.0,8.0,10.0,12.0)] + [collect_t_points(4.0, 0.005)])\nbe = PrimeBackendV2(tq); be.load_cache(\"research/numerics/data/E-022-backend-cache.npz\")\nE16._BUILD.clear(); E16.prime_sum_vec = be.prime_sum\n\nfor a in (4.0, 8.0, 12.0):\n    x,h,Q,M,_b = E16.build(a,H)\n    n=Q.shape[0]\n    mc=np.zeros(n); mc[0]=2*h/3; mc[1]=h/6\n    tc = Q[:,0]-LAM*mc\n    u1 = scipy.linalg.solve_toeplitz((tc,tc), np.ones(n)); s1=u1.sum()\n    def K1(z):\n        bz = E16.hat_FT(np.array([z]),h)[0]*np.exp(-1j*z*x)\n        u0 = scipy.linalg.solve_toeplitz((tc,tc), bz)\n        v = u0-(u0.sum()/s1)*u1\n        return float(np.real(np.conj(bz)@v))\n    print(f\"a={a:g}:\")\n    for y in (0.0, 0.25, 0.5, 0.75, 0.9, 0.99, 1.0, 1.01, 1.1, 1.25, 1.5):\n        k = K1(1j*y)\n        print(f\"   y={y:5.2f}  K(iy,iy)={k:12.4f}\")\nEOF\n./.venv/Scripts/python.exe /tmp/e026_imag.py",
  "description": "Probe K(iy,iy) toward the deficiency frequency",
  "timeout": 570000
}

{
  "file_path": "D:\\Python\\Quantum\\research\\journal\\session-008.md",
  "old_string": "### Handoff notes",
  "new_string": "### Part 9 \u2014 paper assembly sub-stage 1 + imaginary-frequency probe\n- K(iy,iy) probe (ground-state at imaginary frequency): K \u2248 0.8\u20130.9 \u00d7\n  free value e^{2ay}/(2y) \u2014 NO ground-state signature at imaginary\n  frequency; the symbol-space quick avenue is exhausted. Direction (1)\n  remains theory-only.\n- Proceeded to paper assembly (user delegated). draft.tex: Results\n  section now has the R-004 finite-height theorem as a complete\n  theorem\u2013proof-sketch unit (5 steps, constants, margin values,\n  honesty remark incl. conservative window N\u2081* = 2.73\u00d710\u00b2\u00b9).\n  references.bib: +8 entries (Li, Bombieri\u2013Lagarias, Lagarias,\n  Trudgian, Platt\u2013Trudgian, Voros \u00d72, Suzuki).\n- CAVEAT: no LaTeX toolchain on this machine (pdflatex/xelatex/\n  tectonic all absent) \u2014 the draft is NOT compile-tested. Compile\n  check deferred (user may have a TeX install elsewhere, or add one).\n- Remaining paper sub-stages: spectral-program section (R-003 +\n  D-040\u2013D-046), obstruction section (G-001\u2013G-004), numerics appendix\n  (E-tables), Lean appendix placeholder.\n\n### Handoff notes"
}

{
  "file_path": "D:\\Python\\Quantum\\research\\paper\\draft.tex",
  "old_string": "\\begin{remark}\n(i) Using Lagarias's printed bridge window $n \\le T^2/(4\\log^2 T)$\ninstead of the traced proof gives the conservative\n$N_1^* = 2.73\\times 10^{21}$; the theorem is robust either way.\n(ii) The traced worst-case bound $|S_f|$ is $\\sim 170\\times$ loose\nagainst the measured curve ($|S_f| \\le 13.52$ for $n \\le 5000$); the\nslack is structural to contour constants, not a gap.\n(iii) The dependence on computation is explicit: Platt--Trudgian's\ninterval-arithmetic verification, and the finite Li-coefficient\nverifications.\n\\end{remark}",
  "new_string": "\\begin{remark}\n(i) Using Lagarias's printed bridge window $n \\le T^2/(4\\log^2 T)$\ninstead of the traced proof gives the conservative\n$N_1^* = 2.73\\times 10^{21}$; the theorem is robust either way.\n(ii) The traced worst-case bound $|S_f|$ is $\\sim 170\\times$ loose\nagainst the measured curve ($|S_f| \\le 13.52$ for $n \\le 5000$); the\nslack is structural to contour constants, not a gap.\n(iii) The dependence on computation is explicit: Platt--Trudgian's\ninterval-arithmetic verification, and the finite Li-coefficient\nverifications.\n\\end{remark}\n\n\\subsection{The Suzuki operator line: exact factorization and the\nspectral-measure equilibrium (R-003, D-040--D-046)}\n\nSuzuki \\cite{suzuki2026weil} constructs, for each $a > 0$, a\nself-adjoint operator family $\\bar D_{a,\\theta}$ on model spaces\n$\\mathcal H(T_a)$ built from the \\emph{screw function} $g$ of $\\zeta$\n($\\hat g(z) = z^{-2}\\xi'(\\tfrac12-iz)/\\xi(\\tfrac12-iz)$), whose spectra\nare the zeros of\n$W(a,\\theta;z) = (z-i)V_+(z) + e^{i\\theta}(z+i)V_-(z)$, with $V_\\pm$\nthe Fourier transforms of deficiency vectors. His Corollary~1.6 states\nthat a limit formula $e^{\\phi(a,z)}W(a,\\theta(a);z) \\to\nz^2\\xi(\\tfrac12-iz)/\\xi'(\\tfrac12-iz)$ (uniform on compacts, for some\nchoice of $\\theta(a)$, $\\phi$) would imply RH.\n\n\\begin{theorem}[R-003; modulo standard tempered-FT bookkeeping]\nOne has the exact factorization\n$W(a,\\theta;z) = F(z)\\,M(a,\\theta;z)$ with\n$F(z) = z^2\\xi(\\tfrac12-iz)/\\xi'(\\tfrac12-iz)$ and\n$M = R_0 + R_\\tau$, where\n$R_0 = 2e^{a+i\\theta/2}\\sin(az - \\theta/2) + o(e^a)$ is an explicit\nsine skeleton and $R_\\tau$ is the out-of-interval tail transform.\nHence the limit formula is equivalent to the \\emph{tail-cancellation\nstatement} $(\\star)$: $R_\\tau$ cancels the skeleton leaving a zero-free\nremainder \u2014 a finite-interval Wiener--Hopf remainder estimate on the\nsymbol $\\hat g$, whose factorization is gated by the zero locations.\n\\end{theorem}\n\nWe studied the spectral (Clark/de~Branges) measures\n$\\mu_a = \\sum_k w_k\\,\\delta_{z_k}$ of $\\bar D_{a,\\pi}$ numerically to\n$a = 12$ ($w_k = 1/K_a(z_k,z_k)$, $K_a$ the model-space reproducing\nkernel; Galerkin machinery validated against the zero-side explicit\nformula to $4.5\\times10^{-6}$). The picture that emerges\n(D-040--D-045):\n\\begin{enumerate}\n\\item \\emph{The metric knows the zeros.} $K_a(z,z)$ has deep narrow\nvalleys exactly at the true ordinates $\\gamma$ (depth\n$\\Delta(a) \\approx \\log a + 0.64$, width $\\sim 1.5/a$), while\n$K_a(z,z) \\to 2a$ (the free Paley--Wiener diagonal) on the plateau:\nthe operator's symbol is \\emph{1 + the zero comb} \u2014 the explicit\nformula in operator-symbol form.\n\\item \\emph{Positions lock and masses are right.} Each $\\gamma$ has a\nspectral atom within $\\approx 0.65/a^2$ (quadratic locking, correcting\nan earlier wrong-direction metric), carrying mass $\\approx m_\\gamma = 1$.\n\\item \\emph{The equilibrium.} The residual mass over the excess\n(lattice) atoms tends to $Z/(2\\pi)$ per window $[0,Z]$, not to zero:\nthe family equilibrates exactly at the consolidation boundary\n(generic Szeg\\H{o} bulk behavior). At fixed $\\theta$ this is structural\n($\\theta$-independence is measured: residual spread $\\le 2.2\\%$ over\nthe full extension family).\n\\item \\emph{The breaking mechanism.} A shift $\\lambda \\to \\lambda_a^-$\n(bottom of the Weil-form spectrum) pins the valley floors (masses stay\n$1$) while the plateau response diverges \u2014 the unique channel that\nkills the residual. It is machinery-blocked: $\\lambda_a$ decays\nsuperexponentially ($0.414$ at $a{=}0.25$ to $<3\\times10^{-12}$ at\n$a{=}2$) below any achievable discretization floor at zero-resolving\n$a$ (Graveyard G-004).\n\\end{enumerate}\n\nOn the operator-theoretic side (D-041): the limit operator $D$ exists\nunconditionally as a $J$-self-adjoint operator in a Krein space\n(negative index = number of off-line zero pairs, Bombieri), with\n$\\mathrm{spec}(D) = \\Gamma$; and deficiency-element convergence is\nequivalent to strong resolvent convergence\n$\\bar D_{a,\\theta(a)} \\to D$ (Theorem D1), giving the reduction:\nthe limit formula (1.12) holds for some $\\theta(a), \\phi$ if and only\nif $\\mathrm{spec}(D) \\subset \\mathbb R$. The real-spectrum persistence\nstep is exactly RH (the paywall), as expected."
}

{
  "filePath": "D:\\Python\\Quantum\\research\\paper\\draft.tex",
  "oldString": "\\begin{remark}\n(i) Using Lagarias's printed bridge window $n \\le T^2/(4\\log^2 T)$\ninstead of the traced proof gives the conservative\n$N_1^* = 2.73\\times 10^{21}$; the theorem is robust either way.\n(ii) The traced worst-case bound $|S_f|$ is $\\sim 170\\times$ loose\nagainst the measured curve ($|S_f| \\le 13.52$ for $n \\le 5000$); the\nslack is structural to contour constants, not a gap.\n(iii) The dependence on computation is explicit: Platt--Trudgian's\ninterval-arithmetic verification, and the finite Li-coefficient\nverifications.\n\\end{remark}",
  "newString": "\\begin{remark}\n(i) Using Lagarias's printed bridge window $n \\le T^2/(4\\log^2 T)$\ninstead of the traced proof gives the conservative\n$N_1^* = 2.73\\times 10^{21}$; the theorem is robust either way.\n(ii) The traced worst-case bound $|S_f|$ is $\\sim 170\\times$ loose\nagainst the measured curve ($|S_f| \\le 13.52$ for $n \\le 5000$); the\nslack is structural to contour constants, not a gap.\n(iii) The dependence on computation is explicit: Platt--Trudgian's\ninterval-arithmetic verification, and the finite Li-coefficient\nverifications.\n\\end{remark}\n\n\\subsection{The Suzuki operator line: exact factorization and the\nspectral-measure equilibrium (R-003, D-040--D-046)}\n\nSuzuki \\cite{suzuki2026weil} constructs, for each $a > 0$, a\nself-adjoint operator family $\\bar D_{a,\\theta}$ on model spaces\n$\\mathcal H(T_a)$ built from the \\emph{screw function} $g$ of $\\zeta$\n($\\hat g(z) = z^{-2}\\xi'(\\tfrac12-iz)/\\xi(\\tfrac12-iz)$), whose spectra\nare the zeros of\n$W(a,\\theta;z) = (z-i)V_+(z) + e^{i\\theta}(z+i)V_-(z)$, with $V_\\pm$\nthe Fourier transforms of deficiency vectors. His Corollary~1.6 states\nthat a limit formula $e^{\\phi(a,z)}W(a,\\theta(a);z) \\to\nz^2\\xi(\\tfrac12-iz)/\\xi'(\\tfrac12-iz)$ (uniform on compacts, for some\nchoice of $\\theta(a)$, $\\phi$) would imply RH.\n\n\\begin{theorem}[R-003; modulo standard tempered-FT bookkeeping]\nOne has the exact factorization\n$W(a,\\theta;z) = F(z)\\,M(a,\\theta;z)$ with\n$F(z) = z^2\\xi(\\tfrac12-iz)/\\xi'(\\tfrac12-iz)$ and\n$M = R_0 + R_\\tau$, where\n$R_0 = 2e^{a+i\\theta/2}\\sin(az - \\theta/2) + o(e^a)$ is an explicit\nsine skeleton and $R_\\tau$ is the out-of-interval tail transform.\nHence the limit formula is equivalent to the \\emph{tail-cancellation\nstatement} $(\\star)$: $R_\\tau$ cancels the skeleton leaving a zero-free\nremainder \u2014 a finite-interval Wiener--Hopf remainder estimate on the\nsymbol $\\hat g$, whose factorization is gated by the zero locations.\n\\end{theorem}\n\nWe studied the spectral (Clark/de~Branges) measures\n$\\mu_a = \\sum_k w_k\\,\\delta_{z_k}$ of $\\bar D_{a,\\pi}$ numerically to\n$a = 12$ ($w_k = 1/K_a(z_k,z_k)$, $K_a$ the model-space reproducing\nkernel; Galerkin machinery validated against the zero-side explicit\nformula to $4.5\\times10^{-6}$). The picture that emerges\n(D-040--D-045):\n\\begin{enumerate}\n\\item \\emph{The metric knows the zeros.} $K_a(z,z)$ has deep narrow\nvalleys exactly at the true ordinates $\\gamma$ (depth\n$\\Delta(a) \\approx \\log a + 0.64$, width $\\sim 1.5/a$), while\n$K_a(z,z) \\to 2a$ (the free Paley--Wiener diagonal) on the plateau:\nthe operator's symbol is \\emph{1 + the zero comb} \u2014 the explicit\nformula in operator-symbol form.\n\\item \\emph{Positions lock and masses are right.} Each $\\gamma$ has a\nspectral atom within $\\approx 0.65/a^2$ (quadratic locking, correcting\nan earlier wrong-direction metric), carrying mass $\\approx m_\\gamma = 1$.\n\\item \\emph{The equilibrium.} The residual mass over the excess\n(lattice) atoms tends to $Z/(2\\pi)$ per window $[0,Z]$, not to zero:\nthe family equilibrates exactly at the consolidation boundary\n(generic Szeg\\H{o} bulk behavior). At fixed $\\theta$ this is structural\n($\\theta$-independence is measured: residual spread $\\le 2.2\\%$ over\nthe full extension family).\n\\item \\emph{The breaking mechanism.} A shift $\\lambda \\to \\lambda_a^-$\n(bottom of the Weil-form spectrum) pins the valley floors (masses stay\n$1$) while the plateau response diverges \u2014 the unique channel that\nkills the residual. It is machinery-blocked: $\\lambda_a$ decays\nsuperexponentially ($0.414$ at $a{=}0.25$ to $<3\\times10^{-12}$ at\n$a{=}2$) below any achievable discretization floor at zero-resolving\n$a$ (Graveyard G-004).\n\\end{enumerate}\n\nOn the operator-theoretic side (D-041): the limit operator $D$ exists\nunconditionally as a $J$-self-adjoint operator in a Krein space\n(negative index = number of off-line zero pairs, Bombieri), with\n$\\mathrm{spec}(D) = \\Gamma$; and deficiency-element convergence is\nequivalent to strong resolvent convergence\n$\\bar D_{a,\\theta(a)} \\to D$ (Theorem D1), giving the reduction:\nthe limit formula (1.12) holds for some $\\theta(a), \\phi$ if and only\nif $\\mathrm{spec}(D) \\subset \\mathbb R$. The real-spectrum persistence\nstep is exactly RH (the paywall), as expected.",
  "originalFile": "% ============================================================\n% NGUYEN-RH-1 \u2014 working paper draft (living document)\n% Grown incrementally from research/results/ (each R-# = verified part)\n% ============================================================\n\\documentclass[11pt]{article}\n\\usepackage{amsmath,amssymb,amsthm,mathtools}\n\\usepackage[colorlinks=true,linkcolor=blue,citecolor=blue]{hyperref}\n\n\\newtheorem{theorem}{Theorem}\n\\newtheorem{lemma}[theorem]{Lemma}\n\\newtheorem{corollary}[theorem]{Corollary}\n\\theoremstyle{definition}\n\\newtheorem{definition}[theorem]{Definition}\n\\theoremstyle{remark}\n\\newtheorem{remark}[theorem]{Remark}\n\n\\title{Toward the Riemann Hypothesis:\\\\\nWorking Draft --- Project NGUYEN-RH-1}\n\\author{[authors TBD]}\n\\date{Started: 2026-08-17}\n\n\\begin{document}\n\\maketitle\n\n\\begin{abstract}\n[To be written. Placeholder: unconditional progress toward the Riemann\nHypothesis building on the recent two-thirds simplicity theorem.]\n\\end{abstract}\n\n\\section{Introduction}\n% State of the art: >= 2/3 simple on-line, >= 5/6 distinct (Anthropic, 2026).\n% Our contribution: [TBD from results ledger]\n\n\\section{Background: the Weil-form certificate method}\n% Summary of the inherited machinery: Weil explicit formula, Gabor\n% compression \\tilde G = P + Q, rank--trace inequality, Montgomery second\n% moment, window theory R(\\psi).\n\n\\section{Results}\n% Each new theorem/lemma imported from research/results/R-NNN-*.md\n% with its [PROVED]/[PROVED-CONDITIONAL] tag.\n\n\\subsection{An explicit finite-height Li-positivity theorem (R-004)}\n\nLet $\\lambda_n = \\sum_{\\rho}{}'\\,\\bigl[1-\\bigl(1-\\tfrac1\\rho\\bigr)^n\\bigr]$\nbe the Keiper--Li coefficients of the Riemann $\\xi$-function. Li's\ncriterion states $\\lambda_n > 0$ for all $n \\geq 1$ if and only if the\nRiemann hypothesis holds \\cite{li1997,bombieri1999lagarias}. Voros\n\\cite{voros2006sharpenings} showed that ``$\\lambda_n > 0$ for all\n$n \\geq N_0$'' is already equivalent to RH for any $N_0$, so no\npartial infinite-range statement exists; the maximal content of the Li\nroute short of RH is an \\emph{explicit finite-height} statement.\n\n\\begin{theorem}[R-004; conditional on computation]\n\\label{thm:finite-height-li}\nAssume the Riemann hypothesis verified to height\n$T_0 = 3\\times 10^{12}$ (Platt--Trudgian \\cite{platt2021riemann},\ninterval arithmetic). Then\n\\[\n\\lambda_n > 0 \\qquad \\text{for all } 1 \\le n \\le N_1 := (T_0-1)^2\n= 8\\,999\\,999\\,999\\,994\\,000\\,000\\,000\\,001 \\approx 9.0\\times 10^{24}.\n\\]\n\\end{theorem}\n\n\\begin{proof}[Proof sketch (full assembly: D-037)]\nBombieri--Lagarias \\cite{bombieri1999lagarias} give\n$\\lambda_n = S_\\infty(n) - S_f(n) + 1$ with $S_\\infty$ the archimedean\nand $S_f$ the finite-place contribution.\n\n\\emph{Step 1 (archimedean lower bound).} From Lagarias's formula\n\\cite[(4.11)]{lagarias2007li},\n$S_\\infty(n) = \\sum_{j=1}^n (-1)^j \\binom{n}{j} a_j$ with\n$a_1 = (\\log 4\\pi + \\gamma)/2$ and $a_j = (1-2^{-j})\\zeta(j)\n= \\sum_{m \\text{ odd}} m^{-j}$ ($j \\ge 2$), the $j$-sum is a finite\ndifference and one obtains the \\emph{exact} identity\n$S_\\infty(n) = (1-a_1)n - 1 + \\sum_{m \\ge 3,\\, m \\text{ odd}}\n\\bigl[(1-\\tfrac1m)^n - 1 + \\tfrac{n}{m}\\bigr]$.\nBernoulli's inequality and the explicit harmonic bounds\n$\\log M + \\gamma + \\tfrac{1}{2M} - \\tfrac{1}{12M^2} \\le H_M \\le\n\\log M + \\gamma + \\tfrac{1}{2M}$ give, for $n \\ge 20$,\n\\[\nS_\\infty(n) \\;\\ge\\; \\tfrac12 n\\log n + (C_1 - \\tfrac{\\gamma}{2})\\,n - 4,\n\\qquad C_1 = \\tfrac{\\gamma - 1 - \\log 2\\pi}{2}.\n\\]\n(Machine-validated against exact values for $20 \\le n \\le 5000$.)\n\n\\emph{Step 2 (finite-part upper bound).} Tracing Lagarias's contour\nargument \\cite[Thm~6.1]{lagarias2007li} with explicit constants\n(Trudgian's $N(T)$ and $S(T)$ bounds \\cite{trudgian2014}, partial\nfractions for $\\zeta'/\\zeta$, kernel bounds $e^4+1$, a measured\nshort-segment constant $M_0 = 1.3352$) gives\n$|S_f(n)| \\le B(n)$ with\n\\[\nB(n) = 2N(\\sqrt n{+}1) + 4T\\bigl[\\tfrac23 C_0(T) + 2\\log(T{+}2) + 2\\bigr]\n+ 40M_0 + 2(e^4{+}1)\\bigl[7H(T) + 3.3\\bigr] + o(1),\n\\]\n$T = \\sqrt n + 1$, $C_0(t)$ the explicit unit-interval zero count,\n$H(T) = 3C_0(T)^2 + 2\\log(T{+}2) + 2$.\n\n\\emph{Step 3 (bridge).} For $n \\le (T_0-1)^2$ every zero with\n$|\\gamma| \\le \\sqrt n + 1$ is on the line, so\n$|1-(1-1/\\rho)^n| \\le 2$ per zero and\n$|\\lambda_n(T)| \\le 2N(T)$; all other contour terms are\n\\emph{unconditional}.\n\n\\emph{Step 4 (margin).}\n$\\mathrm{margin}(n) := \\tfrac12 n\\log n + (C_1 - \\gamma/2)n - 4 - B(n) + 1$\nis convex for $n \\ge 20$ (each component of $B$ is concave; the leading\nterm has second derivative $1/(2n)$), and\n$\\mathrm{margin}(5\\times 10^4) = 67\\,705 > 0$; hence\n$\\mathrm{margin}(n) > 0$ for all $n \\in [5\\times10^4, N_1]$\n(computed to $n = 4\\times10^5$ on a unit grid and to $N_1$ on a\nlogarithmic grid; $\\mathrm{margin}(N_1) = 2.46\\times 10^{26}$).\n\n\\emph{Step 5 (finite verification).} $\\lambda_n > 0$ for $n \\le 3000$\nby exact high-precision computation (this project, two independent\nmethods, agreement to $4.8\\times10^{-25}$ relative), and for\n$n \\le 5\\times10^5$ by Misguich--Voros \\cite{voros2017li}. The ranges\noverlap $N_0 = 5\\times 10^4$ by a factor $10$.\n\\end{proof}\n\n\\begin{remark}\n(i) Using Lagarias's printed bridge window $n \\le T^2/(4\\log^2 T)$\ninstead of the traced proof gives the conservative\n$N_1^* = 2.73\\times 10^{21}$; the theorem is robust either way.\n(ii) The traced worst-case bound $|S_f|$ is $\\sim 170\\times$ loose\nagainst the measured curve ($|S_f| \\le 13.52$ for $n \\le 5000$); the\nslack is structural to contour constants, not a gap.\n(iii) The dependence on computation is explicit: Platt--Trudgian's\ninterval-arithmetic verification, and the finite Li-coefficient\nverifications.\n\\end{remark}\n\n\\section{Obstruction analysis}\n% Documented dead ends from research/graveyard/ where they\n% delimit the method (contributes to success criterion 4).\n\n\\appendix\n\\section{Numerical experiments}\n% Tables/figures generated from research/numerics/data/ CSVs.\n\n\\section{Formal verification}\n% Lean 4 skeleton status; axiom audit (propext, Classical.choice, Quot.sound only).\n\n\\bibliographystyle{plain}\n\\bibliography{references}\n\\end{document}\n",
  "structuredPatch": [
    {
      "oldStart": 131,
      "oldLines": 6,
      "newStart": 131,
      "newLines": 74,
      "lines": [
        " verifications.",
        " \\end{remark}",
        " ",
        "+\\subsection{The Suzuki operator line: exact factorization and the",
        "+spectral-measure equilibrium (R-003, D-040--D-046)}",
        "+",
        "+Suzuki \\cite{suzuki2026weil} constructs, for each $a > 0$, a",
        "+self-adjoint operator family $\\bar D_{a,\\theta}$ on model spaces",
        "+$\\mathcal H(T_a)$ built from the \\emph{screw function} $g$ of $\\zeta$",
        "+($\\hat g(z) = z^{-2}\\xi'(\\tfrac12-iz)/\\xi(\\tfrac12-iz)$), whose spectra",
        "+are the zeros of",
        "+$W(a,\\theta;z) = (z-i)V_+(z) + e^{i\\theta}(z+i)V_-(z)$, with $V_\\pm$",
        "+the Fourier transforms of deficiency vectors. His Corollary~1.6 states",
        "+that a limit formula $e^{\\phi(a,z)}W(a,\\theta(a);z) \\to",
        "+z^2\\xi(\\tfrac12-iz)/\\xi'(\\tfrac12-iz)$ (uniform on compacts, for some",
        "+choice of $\\theta(a)$, $\\phi$) would imply RH.",
        "+",
        "+\\begin{theorem}[R-003; modulo standard tempered-FT bookkeeping]",
        "+One has the exact factorization",
        "+$W(a,\\theta;z) = F(z)\\,M(a,\\theta;z)$ with",
        "+$F(z) = z^2\\xi(\\tfrac12-iz)/\\xi'(\\tfrac12-iz)$ and",
        "+$M = R_0 + R_\\tau$, where",
        "+$R_0 = 2e^{a+i\\theta/2}\\sin(az - \\theta/2) + o(e^a)$ is an explicit",
        "+sine skeleton and $R_\\tau$ is the out-of-interval tail transform.",
        "+Hence the limit formula is equivalent to the \\emph{tail-cancellation",
        "+statement} $(\\star)$: $R_\\tau$ cancels the skeleton leaving a zero-free",
        "+remainder \u2014 a finite-interval Wiener--Hopf remainder estimate on the",
        "+symbol $\\hat g$, whose factorization is gated by the zero locations.",
        "+\\end{theorem}",
        "+",
        "+We studied the spectral (Clark/de~Branges) measures",
        "+$\\mu_a = \\sum_k w_k\\,\\delta_{z_k}$ of $\\bar D_{a,\\pi}$ numerically to",
        "+$a = 12$ ($w_k = 1/K_a(z_k,z_k)$, $K_a$ the model-space reproducing",
        "+kernel; Galerkin machinery validated against the zero-side explicit",
        "+formula to $4.5\\times10^{-6}$). The picture that emerges",
        "+(D-040--D-045):",
        "+\\begin{enumerate}",
        "+\\item \\emph{The metric knows the zeros.} $K_a(z,z)$ has deep narrow",
        "+valleys exactly at the true ordinates $\\gamma$ (depth",
        "+$\\Delta(a) \\approx \\log a + 0.64$, width $\\sim 1.5/a$), while",
        "+$K_a(z,z) \\to 2a$ (the free Paley--Wiener diagonal) on the plateau:",
        "+the operator's symbol is \\emph{1 + the zero comb} \u2014 the explicit",
        "+formula in operator-symbol form.",
        "+\\item \\emph{Positions lock and masses are right.} Each $\\gamma$ has a",
        "+spectral atom within $\\approx 0.65/a^2$ (quadratic locking, correcting",
        "+an earlier wrong-direction metric), carrying mass $\\approx m_\\gamma = 1$.",
        "+\\item \\emph{The equilibrium.} The residual mass over the excess",
        "+(lattice) atoms tends to $Z/(2\\pi)$ per window $[0,Z]$, not to zero:",
        "+the family equilibrates exactly at the consolidation boundary",
        "+(generic Szeg\\H{o} bulk behavior). At fixed $\\theta$ this is structural",
        "+($\\theta$-independence is measured: residual spread $\\le 2.2\\%$ over",
        "+the full extension family).",
        "+\\item \\emph{The breaking mechanism.} A shift $\\lambda \\to \\lambda_a^-$",
        "+(bottom of the Weil-form spectrum) pins the valley floors (masses stay",
        "+$1$) while the plateau response diverges \u2014 the unique channel that",
        "+kills the residual. It is machinery-blocked: $\\lambda_a$ decays",
        "+superexponentially ($0.414$ at $a{=}0.25$ to $<3\\times10^{-12}$ at",
        "+$a{=}2$) below any achievable discretization floor at zero-resolving",
        "+$a$ (Graveyard G-004).",
        "+\\end{enumerate}",
        "+",
        "+On the operator-theoretic side (D-041): the limit operator $D$ exists",
        "+unconditionally as a $J$-self-adjoint operator in a Krein space",
        "+(negative index = number of off-line zero pairs, Bombieri), with",
        "+$\\mathrm{spec}(D) = \\Gamma$; and deficiency-element convergence is",
        "+equivalent to strong resolvent convergence",
        "+$\\bar D_{a,\\theta(a)} \\to D$ (Theorem D1), giving the reduction:",
        "+the limit formula (1.12) holds for some $\\theta(a), \\phi$ if and only",
        "+if $\\mathrm{spec}(D) \\subset \\mathbb R$. The real-spectrum persistence",
        "+step is exactly RH (the paywall), as expected.",
        "+",
        " \\section{Obstruction analysis}",
        " % Documented dead ends from research/graveyard/ where they",
        " % delimit the method (contributes to success criterion 4)."
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "D:\\Python\\Quantum\\research\\paper\\draft.tex",
  "old_string": "\\appendix\n\\section{Numerical experiments}\n% Tables/figures generated from research/numerics/data/ CSVs.",
  "new_string": "\\appendix\n\\section{Numerical experiments}\n% Tables/figures generated from research/numerics/data/ CSVs.\n\nAll experiments are deterministic scripts with CSV+JSON sidecars in the\nproject archive (\\texttt{research/numerics/}); checks as stated.\n\n\\subsection{Li-coefficient machinery (E-011/E-015/E-021/E-023)}\n\\begin{itemize}\n\\item $\\lambda_n > 0$ verified for $n \\le 3000$ from the arithmetic\nside (Bombieri--Lagarias Thm~2, zero-free; \\textsc{flint} Stieltjes +\nArb $\\zeta$, 1000--1450-digit working precision), cross-validated\nagainst the zero-side computation (agreement $4.8\\times10^{-25}$\nrelative) and $\\lambda_1$ to 102 digits against\n$\\gamma/2$-type closed forms.\n\\item Exact archimedean part: $S_\\infty(n) = \\tfrac12 n\\log n + C_1 n\n- \\tfrac14 - \\tfrac{1}{24n} + o(1/n)$ measured to $n = 5000$\n($c_0 = -1/4$ identified exactly; residuals match $-1/4 - 1/(24n)$ to\nall printed digits), and $|S_f(n)| \\le 13.52$ for $n \\le 5000$\n(max at $n = 3298$) vs the traced worst-case $\\sim 2280$ there \u2014\nthe contour constants are $\\sim 170\\times$ loose, as documented.\n\\item Margin assembly: crossover at $n = 32\\,871$ (traced constants)\n/ $30\\,217$ (measured constants $A = 0.9$, $B_0 = 1.0$); adopted\n$N_0 = 5\\times10^4$ with margin $67\\,705$; margin convex to\n$N_1 \\approx 9\\times10^{24}$.\n\\end{itemize}\n\n\\subsection{Spectral-measure program (E-016--E-025)}\n\\begin{itemize}\n\\item Galerkin realization of Suzuki's Weil-form operator validated\nagainst the zero-side explicit formula to $4.5\\times10^{-6}$;\nzero-location by sign-change + Brent refinement; winding-number\ndiagnostics for off-axis zeros.\n\\item Clark/de~Branges weights $1/K_a(z_k,z_k)$ via Schur-reduced\nbordered Toeplitz solves (validated to $3.6\\times10^{-14}$ against\ndense bordered solves; $h$-refinement $1.1\\times10^{-3}$).\n\\item Valley observable: $\\Delta(a) = 2.16, 2.51, 2.74, 2.87, 2.94$\nfor $a = 4,6,8,10,12$; plateau $K \\to 2a$; floors $\\approx 1.04$;\nmass within $\\pm0.1$ of true zeros $63\\% \\to 72.5\\%$; positional\nlocking $\\approx 0.65/a^2$; residual $\\to Z/(2\\pi)$.\n\\item $\\theta$-independence (E-024): residual spread $\\le 2.2\\%$ over\n$7$ boundary conditions $\\times$ $3$ values of $a$.\n\\item $\\lambda$-flow (E-025): discretization floor documented\n(pencil bottom crosses zero at $a \\approx 5.2$ for $h = 0.01$,\n$O(h)$ artifact); channel response measured at $a=4$\n($\\Delta\\colon 2.16 \\to 6.99$, residual $48 \\to 11$).\n\\end{itemize}"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
  "oldString": "lemma norm_term_vonMangoldt_le_two_pow {\u03c3 : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (\u03c3 : \u2102) m\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n  have h\u03c3re : ((\u03c3 : \u2102).re) = \u03c3 := rfl\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hm =>\n    have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n        ArithmeticFunction.vonMangoldt m :=\n      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n    rw [h\u039b]\n    rcases eq_or_ne m 1 with rfl | hm1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hm2 : 2 \u2264 m := by omega\n      have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n          (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n        rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n          Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n        field_simp [show (m : \u211d) \u2260 0 by positivity]\n      rw [e]\n      have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n        rw [Real.rpow_neg (by norm_num : (0 : \u211d) < 2)]\n        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n        exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n          (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n      exact mul_le_mul_of_nonneg_right hle hpos",
  "newString": "lemma norm_term_vonMangoldt_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n        ((\u03c3 : \u211d) + t * Complex.I) m\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n  have h\u03c3re : ((\u03c3 : \u211d) + t * Complex.I).re = \u03c3 := by simp\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hm =>\n    have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n        ArithmeticFunction.vonMangoldt m :=\n      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n    rw [h\u039b]\n    rcases eq_or_ne m 1 with rfl | hm1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hm2 : 2 \u2264 m := by omega\n      have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n          (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n        rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n          Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n        field_simp [show (m : \u211d) \u2260 0 by positivity]\n        ring_nf\n      rw [e]\n      have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]\n        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n        exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n          (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n      exact mul_le_mul_of_nonneg_right hle hpos",
  "originalFile": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n  H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n    (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n    DifferentiableAt \u2102 (Jlag n) s := by\n  apply Jlag_differentiableAt\n  \u00b7 rintro rfl\n    simp at him\n  \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n  intro s hs\n  rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n  rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n  exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n  (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n  rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n    smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    HIntegral (Jlag n) 3 XR T =\n      HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n        VIntegral (Jlag n) 3 T U := by\n  have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR\n  unfold RectangleIntegral at h0\n  rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n  linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n    kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n  unfold kFun\n  simp [map_sub, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n    Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n  have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n      (starRingEnd \u2102) (deriv riemannZeta s) := by\n    have h := iteratedDeriv_riemannZeta_conj 1 hs\n    rwa [iteratedDeriv_one] at h\n  unfold Jlag\n  rw [kFun_conj, _root_.riemannZeta_conj, h1]\n  simp only [map_mul, map_neg, map_div\u2080]\n\n/-! ## 3. The left-lift bound (DL-2, D-074 \u00a73.3 V_left) -/\n\n/-- **Kernel on the lift**: \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2\n(D-074 \u00a76: |(3+it)/(2+it)|\u00b2 = (9+t\u00b2)/(4+t\u00b2) = 1 + 5/(4+t\u00b2), whose n-th\npower is \u2264 e^{5n/(2(4+t\u00b2))} \u2264 e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : \u2115} {t : \u211d}\n    (hT : (n : \u211d) \u2264 t ^ 2) :\n    \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp (5 / 2) + 1 := by\n  rcases Nat.eq_zero_or_pos n with hn | hn\n  \u00b7 subst hn\n    simp only [kFun, pow_zero, sub_self, norm_zero]\n    positivity\n  \u00b7 have hnR : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n    have ht2 : (0 : \u211d) < 4 + t ^ 2 := by positivity\n    have hn4t2 : (n : \u211d) \u2264 4 + t ^ 2 := by linarith [hT]\n    have hQpos : (0 : \u211d) \u2264 (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n    have hQle : (9 + t ^ 2) / (4 + t ^ 2) \u2264 Real.exp (5 / (n : \u211d)) := by\n      have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n        field_simp [ht2.ne']\n        ring\n      rw [h1]\n      have h2 : 5 / (4 + t ^ 2) \u2264 5 / (n : \u211d) :=\n        (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n      have h3 := Real.add_one_le_exp (5 / (n : \u211d))\n      linarith\n    have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 Real.exp 5 := by\n      calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 (Real.exp (5 / (n : \u211d))) ^ n :=\n            pow_le_pow_left\u2080 hQpos hQle n\n        _ = Real.exp 5 := by\n            rw [\u2190 Real.exp_nat_mul]\n            congr 1\n            have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n            field_simp [hn0]\n    have hns3 : Complex.normSq ((3 : \u211d) + t * Complex.I) = 9 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hns2 : Complex.normSq ((2 : \u211d) + t * Complex.I) = 4 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hnormA : \u2016((3 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (9 + t ^ 2) := by\n      have h1 : \u2016((3 : \u211d) + t * Complex.I)\u2016 =\n          Real.sqrt (Complex.normSq ((3 : \u211d) + t * Complex.I)) := by\n        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n      rw [h1, hns3]\n    have hnormB : \u2016((2 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (4 + t ^ 2) := by\n      have h1 : \u2016((2 : \u211d) + t * Complex.I)\u2016 =\n          Real.sqrt (Complex.normSq ((2 : \u211d) + t * Complex.I)) := by\n        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n      rw [h1, hns2]\n    have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =\n        Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n      rw [norm_div, hnormA, hnormB,\n        \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]\n    have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by\n      push_cast\n      ring\n    unfold kFun\n    rw [hs1]\n    calc \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n - 1\u2016\n        \u2264 \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n          norm_sub_le _ _\n      _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n          rw [norm_pow, hnorm, norm_one]\n      _ \u2264 Real.exp (5 / 2) + 1 := by\n          have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n \u2264 Real.exp (5 / 2) := by\n            have hx0 : (0 : \u211d) \u2264 Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=\n              Real.sqrt_nonneg _\n            have hx : (0 : \u211d) \u2264 (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=\n              pow_nonneg hx0 n\n            have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 \u2264 Real.exp 5 := by\n              have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =\n                  ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by\n                rw [\u2190 pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]\n              rw [e]\n              exact hQn\n            have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =\n                Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by\n              rw [Real.sqrt_sq hx]\n            rw [h8]\n            calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)\n                \u2264 Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5\n              _ = Real.exp (5 / 2) := (Real.exp_half 5).symm\n          linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : \u211d :=\n  \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016\n\n/-- Termwise 3-vs-2 comparison for the \u039b L-series: \u039b(n)/n\u00b3 \u2264 (1/2)\u00b7\u039b(n)/n\u00b2. -/\nlemma norm_term_vonMangoldt_three_le_half (n : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 \u2264\n      (1 / 2) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 := by\n  have h3re : ((3 : \u2102).re) = 3 := rfl\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hn =>\n    rcases eq_or_ne n 1 with rfl | hn1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hn2 : 2 \u2264 n := by omega\n      have h\u039b : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016 =\n          ArithmeticFunction.vonMangoldt n :=\n        Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n      rw [h\u039b]\n      have e : ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d) =\n          (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := by\n        rw [show (3 : \u211d) = 2 + 1 by norm_num,\n          Real.rpow_add (by positivity : (0 : \u211d) < (n : \u211d)), Real.rpow_one]\n        field_simp [show (n : \u211d) \u2260 0 by positivity]\n      have h12 : (1 : \u211d) / (n : \u211d) \u2264 1 / 2 :=\n        one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 2)\n          (by exact_mod_cast hn2 : (2 : \u211d) \u2264 (n : \u211d))\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (n : \u211d)) _)\n      calc ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d)\n          = (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := e\n        _ \u2264 (1 / 2) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) :=\n            mul_le_mul_of_nonneg_right h12 hpos\n\n/-- dirichletC3 \u2264 1/2 (the termwise comparison + dirichletC2 \u2264 1) \u2014\nthe certified C_zeta3 = 0.5 of D-074 \u00a74. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 \u2264 1 / 2 := by\n  have hsum3 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsum2 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  calc dirichletC3\n      = \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 := rfl\n    _ \u2264 \u2211' n : \u2115, (1 / 2) *\n          \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n        Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n          (hsum2.mul_left (1 / 2))\n    _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n    _ \u2264 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 dirichletC3 for re s \u2265 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : \u2102} (hs : 3 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC3 := by\n  have hs1 : (1 : \u211d) < s.re := by linarith\n  have h1 : -logDeriv riemannZeta s\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum3 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n      \u2264 dirichletC3 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            exact hs) n) hsumS hsum3\n      _ = dirichletC3 := rfl\n  calc \u2016logDeriv riemannZeta s\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 dirichletC3 := hle\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : \u2102} (hs : 3 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 1 / 2 :=\n  (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 \u00a73.3 V_left): for 0 < T \u2264 U and\nn \u2264 T\u00b2, \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U \u2212 T)\u00b7(e^{5/2}+1)/2. The kernel\n\u2264 e^{5/2}+1 (the 1+5/(4+t\u00b2) computation), the zeta factor \u2264 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : \u2115} {T U : \u211d}\n    (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n    \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n  have hnorm : \u2016VIntegral (Jlag n) 3 T U\u2016 =\n      \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 := by\n    unfold VIntegral\n    rw [norm_smul, Complex.norm_I, one_mul]\n  rw [hnorm]\n  have hbound : \u2200 t \u2208 Set.Ioc T U,\n      \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 (Real.exp (5 / 2) + 1) * (1 / 2) := by\n    intro t ht\n    have htT : T < t := ht.1\n    have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n    have hre : (3 : \u211d) \u2264 ((3 : \u211d) + t * Complex.I).re := by simp\n    have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n    have h2 := norm_logDeriv_zeta_le_half (s := (3 : \u211d) + t * Complex.I) hre\n    have hnorm3 : \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 =\n        \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 *\n          \u2016logDeriv riemannZeta ((3 : \u211d) + t * Complex.I)\u2016 := by\n      show \u2016kFun n ((3 : \u211d) + t * Complex.I) *\n          (-logDeriv riemannZeta ((3 : \u211d) + t * Complex.I))\u2016 = _\n      rw [norm_mul, norm_neg]\n    rw [hnorm3]\n    exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n  have hint : \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264\n      ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n    apply intervalIntegral.norm_integral_le_of_norm_le_const\n    intro t ht\n    rw [Set.uIoc_of_le hTU] at ht\n    exact hbound t ht\n  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n  rw [habs] at hint\n  calc \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016\n      \u2264 ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n    _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\n/-! ## 4. The high-horizontal stepping (DL-3, D-074 \u00a77 + D-073 \u00a74) -/\n\n/-- Termwise \u03c3-vs-2 comparison for the \u039b L-series (the (6.10) halving):\n\u039b(m)/m^\u03c3 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7\u039b(m)/m\u00b2 for \u03c3 \u2265 2. -/\nlemma norm_term_vonMangoldt_le_two_pow {\u03c3 : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (\u03c3 : \u2102) m\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n  have h\u03c3re : ((\u03c3 : \u2102).re) = \u03c3 := rfl\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hm =>\n    have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n        ArithmeticFunction.vonMangoldt m :=\n      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n    rw [h\u039b]\n    rcases eq_or_ne m 1 with rfl | hm1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hm2 : 2 \u2264 m := by omega\n      have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n          (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n        rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n          Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n        field_simp [show (m : \u211d) \u2260 0 by positivity]\n      rw [e]\n      have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n        rw [Real.rpow_neg (by norm_num : (0 : \u211d) < 2)]\n        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n        exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n          (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n      exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- \u2016\u03b6\u2032/\u03b6(\u03c3+it)\u2016 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 for \u03c3 \u2265 2 (the (6.10)\nhalving in LSeries form; dirichletC2 \u2264 1 makes the tail free). -/\nlemma norm_logDeriv_zeta_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) :\n    \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n  have hs1 : (1 : \u211d) < ((\u03c3 : \u211d) + t * Complex.I).re := by simp; linarith\n  have h1 : -logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) ((\u03c3 : \u211d) + t * Complex.I) := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum2 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n        ((\u03c3 : \u211d) + t * Complex.I) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n      ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n      ((\u03c3 : \u211d) + t * Complex.I) n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n          ((\u03c3 : \u211d) + t * Complex.I) n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n            ((\u03c3 : \u211d) + t * Complex.I) n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, (2 : \u211d) ^ (-(\u03c3 - 2)) *\n            \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_le_two_pow h\u03c3 n) hsumS\n            (hsum2.mul_left _)\n      _ = (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n  calc \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n          ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := hle\n\n/-- **Kernel envelope** (D-074 \u00a77, the single-exponential form that\nreplaces the unit-step geometric series): \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264\ne^{(4/9)\u03c3} for \u03c3 \u2265 3 and n \u2264 (4/9)U\u00b2. From the (6.11) core\n\u20161+1/s\u2016 \u2264 1+(re s+1)/normSq s \u2264 1+\u03c3/U\u00b2. -/\ntheorem one_add_div_pow_norm_le_exp_four_ninths {n : \u2115} {\u03c3 U : \u211d}\n    (h\u03c3 : 3 \u2264 \u03c3) (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) :\n    \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 Real.exp ((4 / 9) * \u03c3) := by\n  have hs0 : (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2260 0 := by\n    intro h\n    have him : (((\u03c3 : \u211d) - 1) + U * Complex.I).im = 0 := by rw [h]; simp\n    simp at him\n    linarith\n  have hle := norm_one_add_one_div_le hs0\n  have hre : (((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1 = \u03c3 := by\n    simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n      Complex.sub_re, Complex.one_re]\n    ring\n  have hns : Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) = (\u03c3 - 1) ^ 2 + U ^ 2 := by\n    simp [Complex.normSq_apply]\n    ring\n  have hstep : ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n      Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 \u03c3 / U ^ 2 := by\n    rw [hre, hns]\n    have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n    have h1 : (0 : \u211d) \u2264 (\u03c3 - 1) ^ 2 := sq_nonneg _\n    exact (div_le_div_iff_of_pos_left (by linarith : (0 : \u211d) < \u03c3)\n      (by positivity) hU2).mpr (by linarith [h1])\n  have hpow1 : \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 (1 + \u03c3 / U ^ 2) ^ n :=\n    pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep) n\n  have hpow2 : (1 + \u03c3 / U ^ 2) ^ n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n    calc (1 + \u03c3 / U ^ 2) ^ n \u2264 (Real.exp (\u03c3 / U ^ 2)) ^ n := by\n          have h := Real.add_one_le_exp (\u03c3 / U ^ 2)\n          exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n      _ = Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n          rw [\u2190 Real.exp_nat_mul]\n  have hexp : (n : \u211d) * (\u03c3 / U ^ 2) \u2264 (4 / 9) * \u03c3 := by\n    have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n    have h\u03c30 : (0 : \u211d) < \u03c3 := by linarith\n    rw [mul_div_assoc, \u2190 div_le_div_iff_of_pos_right h\u03c30]\n    exact (div_le_div_iff_of_pos_right hU2).mpr hnU\n  calc \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n\n      \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := hpow1.trans hpow2\n    _ \u2264 Real.exp ((4 / 9) * \u03c3) := Real.exp_le_exp.mpr hexp\n\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 337,
      "oldLines": 10,
      "newStart": 337,
      "newLines": 11,
      "lines": [
        " ",
        " /-- Termwise \u03c3-vs-2 comparison for the \u039b L-series (the (6.10) halving):",
        " \u039b(m)/m^\u03c3 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7\u039b(m)/m\u00b2 for \u03c3 \u2265 2. -/",
        "-lemma norm_term_vonMangoldt_le_two_pow {\u03c3 : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :",
        "-    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (\u03c3 : \u2102) m\u2016 \u2264",
        "+lemma norm_term_vonMangoldt_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :",
        "+    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))",
        "+        ((\u03c3 : \u211d) + t * Complex.I) m\u2016 \u2264",
        "       (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by",
        "-  have h\u03c3re : ((\u03c3 : \u2102).re) = \u03c3 := rfl",
        "+  have h\u03c3re : ((\u03c3 : \u211d) + t * Complex.I).re = \u03c3 := by simp",
        "   have h2re : ((2 : \u2102).re) = 2 := rfl",
        "   simp only [LSeries.norm_term_eq, h\u03c3re, h2re]",
        "   split"
      ]
    },
    {
      "oldStart": 358,
      "oldLines": 9,
      "newStart": 359,
      "newLines": 10,
      "lines": [
        "         rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,",
        "           Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]",
        "         field_simp [show (m : \u211d) \u2260 0 by positivity]",
        "+        ring_nf",
        "       rw [e]",
        "       have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by",
        "-        rw [Real.rpow_neg (by norm_num : (0 : \u211d) < 2)]",
        "+        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]",
        "         apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)",
        "         exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)",
        "           (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-041-krein-frame-deficiency-convergence.md",
  "old_string": "| L1 | \u210b(A_a) \u21aa \u210b(A\u221e) unconditionally | OPEN (published proof via [14] uses RH); expected true; bounded isotropy suffices |",
  "new_string": "| L1 | \u210b(A_a) \u21aa \u210b(A\u221e) unconditionally | PROOF SKETCH COMPLETE (2026-08-19, below) \u2014 modulo the D-026-flagged tempered-FT bookkeeping |\n| L1\u2032 | (argument) [v] = 0 \u27fa g\u2217v = 0 as a distribution (Q_W(v,w) = \u27e8g\u2217v, w\u27e9 \u2200w \u2208 C\u221e_c(\u211d)); then \u011d\u00b7v\u0302 = 0 as analytic functionals (g\u2217v grows \u2264 e^{\\|x\\|/2}, Paley\u2013Wiener\u2013Schwartz); \u011d = z\u207b\u00b2\u03be\u2032/\u03be nonzero meromorphic \u27f9 v\u0302 \u2261 0 (identity theorem) \u27f9 v = 0. No RH input. | write-up = Phase-5 item |"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiDogLeg.lean",
  "oldString": "      have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]\n        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n        exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n          (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)",
  "newString": "      have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2), \u2190 one_div]\n        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n        exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n          (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)",
  "originalFile": "/-\nNguyenRH1/LiDogLeg.lean \u2014 ii\u2032-6-DL-1 (D-074, session 040): the zero-free\ndog-leg deformation of the Lagarias horizontal right tail.\n\nTHE CONTENT (D-074 \u00a73.1\u20133.2): on the dog-leg rectangle [3, X_R]\u00d7[T, U]\n(T > 0), the Lagarias integrand Jlag n s = (s/(s\u22121))\u207f\u22121 \u00b7 (\u2212\u03b6\u2032/\u03b6(s)) is\nholomorphic UNCONDITIONALLY (s \u2260 1 since im > 0; \u03b6 s \u2260 0 for re s \u2265 3 > 1\nby Mathlib's Euler-product nonvanishing `riemannZeta_ne_zero_of_one_lt_re`\n\u2014 NO perimeter hypothesis, no zero-avoidance at U). Cauchy's theorem\n(`HolomorphicOn.vanishesOnRectangle`) then gives the EXACT deformation\nidentity\n  H(3\u2192X_R, T) = H(3\u2192X_R, U) \u2212 V(X_R, T\u2192U) + V(3, T\u2192U)\n(the upper right tail = the high horizontal \u2212 the right drop + the left\nlift), plus the Jlag conjugation identity for the lower-side transfer.\n\nThis is the repair of Finding F-D (D-072): the broken low-path envelope\nis ABANDONED (not bounded) \u2014 the magnitude bound comes later from the\nthree dog-leg pieces, all in the unconditionally zero-free region.\n-/\nimport Mathlib\nimport NguyenRH1.LiSides\nimport NguyenRH1.LiTightR\n\nopen Zeta23 Complex Filter Topology\nopen scoped Nat\n\nnoncomputable section\n\nnamespace NguyenRH1\n\n/-! ## 1. Dog-leg analyticity (D-074 \u00a73.1; no perimeter) -/\n\n/-- The dog-leg corners (same real-part/imaginary-part form as rectZ/rectW). -/\ndef dogZ (T : \u211d) : \u2102 := ((3 : \u211d) : \u2102) + (T : \u211d) * Complex.I\ndef dogW (XR U : \u211d) : \u2102 := ((XR : \u211d) : \u2102) + (U : \u211d) * Complex.I\n\nlemma dogZ_re (T : \u211d) : (dogZ T).re = 3 := by simp [dogZ]\nlemma dogZ_im (T : \u211d) : (dogZ T).im = T := by simp [dogZ]\nlemma dogW_re (XR U : \u211d) : (dogW XR U).re = XR := by simp [dogW]\nlemma dogW_im (XR U : \u211d) : (dogW XR U).im = U := by simp [dogW]\n\n/-- Jlag is differentiable at every point with 3 \u2264 re, 0 < im:\n\u03b6 is zero-free for 1 < re (Mathlib `riemannZeta_ne_zero_of_one_lt_re`,\nUNCONDITIONAL \u2014 the Euler-product region) and s \u2260 1 (im \u2260 0).\nNO perimeter hypothesis. -/\ntheorem Jlag_differentiableAt_dogleg {n : \u2115} {s : \u2102}\n    (hre : 3 \u2264 s.re) (him : 0 < s.im) :\n    DifferentiableAt \u2102 (Jlag n) s := by\n  apply Jlag_differentiableAt\n  \u00b7 rintro rfl\n    simp at him\n  \u00b7 exact riemannZeta_ne_zero_of_one_lt_re (by linarith)\n\n/-- Jlag is holomorphic on the whole dog-leg rectangle\n[3, X_R]\u00d7[T, U] (T > 0). -/\ntheorem holomorphicOn_Jlag_dogleg {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    HolomorphicOn (Jlag n) (Rectangle (dogZ T) (dogW XR U)) := by\n  intro s hs\n  rw [Rectangle, Complex.mem_reProdIm, dogZ_re, dogW_re, dogZ_im, dogW_im] at hs\n  rw [Set.uIcc_of_le hXR, Set.uIcc_of_le hTU] at hs\n  exact (Jlag_differentiableAt_dogleg hs.1.1 (by linarith [hs.2.1])).differentiableWithinAt\n\n/-- **The dog-leg rectangle integral vanishes** (Cauchy; the region is\nunconditionally zero-free \u2014 the residue sum is EMPTY, no perimeter). -/\ntheorem rectangleIntegral_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    RectangleIntegral (Jlag n) (dogZ T) (dogW XR U) = 0 :=\n  (holomorphicOn_Jlag_dogleg hT hTU hXR).vanishesOnRectangle subset_rfl\n\n/-- The (2\u03c0i)\u207b\u00b9-normalized form (API symmetry with rectInt'_Jlag). -/\ntheorem rectangleIntegral'_Jlag_dogleg_eq_zero {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    RectangleIntegral' (Jlag n) (dogZ T) (dogW XR U) = 0 := by\n  rw [RectangleIntegral', rectangleIntegral_Jlag_dogleg_eq_zero hT hTU hXR,\n    smul_zero]\n\n/-- **THE EXACT DOG-LEG DEFORMATION IDENTITY** (D-074 \u00a73.2 (\u2605), the\ncapstone for ii\u2032-6-c): the low right-horizontal equals the high\nhorizontal minus the right drop plus the left lift. Orientations: all\nH-integrals left-to-right, all V-integrals upward (the main contour's\ntop side is their reversal, handled at the fold site). -/\ntheorem upper_right_horizontal_eq_dogleg {n : \u2115} {T U XR : \u211d}\n    (hT : 0 < T) (hTU : T \u2264 U) (hXR : 3 \u2264 XR) :\n    HIntegral (Jlag n) 3 XR T =\n      HIntegral (Jlag n) 3 XR U - VIntegral (Jlag n) XR T U +\n        VIntegral (Jlag n) 3 T U := by\n  have h0 := rectangleIntegral_Jlag_dogleg_eq_zero (n := n) hT hTU hXR\n  unfold RectangleIntegral at h0\n  rw [dogZ_re, dogZ_im, dogW_re, dogW_im] at h0\n  linear_combination h0\n\n/-! ## 2. The conjugation identity (for the lower-side transfer, DL-5) -/\n\n/-- kFun is conjugation-symmetric (real-coefficient rational function). -/\ntheorem kFun_conj (n : \u2115) (s : \u2102) :\n    kFun n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (kFun n s) := by\n  unfold kFun\n  simp [map_sub, map_pow, map_one]\n\n/-- **Jlag is conjugation-symmetric** (from `riemannZeta_conj` +\n`iteratedDeriv_riemannZeta_conj`): Jlag n (s\u0304) = conj (Jlag n s).\nNeeded for the lower-horizontal transfer (DL-5). -/\ntheorem Jlag_conj (n : \u2115) {s : \u2102} (hs : s \u2260 1) :\n    Jlag n ((starRingEnd \u2102) s) = (starRingEnd \u2102) (Jlag n s) := by\n  have h1 : deriv riemannZeta ((starRingEnd \u2102) s) =\n      (starRingEnd \u2102) (deriv riemannZeta s) := by\n    have h := iteratedDeriv_riemannZeta_conj 1 hs\n    rwa [iteratedDeriv_one] at h\n  unfold Jlag\n  rw [kFun_conj, _root_.riemannZeta_conj, h1]\n  simp only [map_mul, map_neg, map_div\u2080]\n\n/-! ## 3. The left-lift bound (DL-2, D-074 \u00a73.3 V_left) -/\n\n/-- **Kernel on the lift**: \u2016kFun n (3+it)\u2016 \u2264 e^{5/2}+1 for n \u2264 t\u00b2\n(D-074 \u00a76: |(3+it)/(2+it)|\u00b2 = (9+t\u00b2)/(4+t\u00b2) = 1 + 5/(4+t\u00b2), whose n-th\npower is \u2264 e^{5n/(2(4+t\u00b2))} \u2264 e^{5/2}). -/\ntheorem kFun_three_add_it_norm_le_exp_five_halves_add_one {n : \u2115} {t : \u211d}\n    (hT : (n : \u211d) \u2264 t ^ 2) :\n    \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 Real.exp (5 / 2) + 1 := by\n  rcases Nat.eq_zero_or_pos n with hn | hn\n  \u00b7 subst hn\n    simp only [kFun, pow_zero, sub_self, norm_zero]\n    positivity\n  \u00b7 have hnR : (1 : \u211d) \u2264 (n : \u211d) := by exact_mod_cast hn\n    have ht2 : (0 : \u211d) < 4 + t ^ 2 := by positivity\n    have hn4t2 : (n : \u211d) \u2264 4 + t ^ 2 := by linarith [hT]\n    have hQpos : (0 : \u211d) \u2264 (9 + t ^ 2) / (4 + t ^ 2) := by positivity\n    have hQle : (9 + t ^ 2) / (4 + t ^ 2) \u2264 Real.exp (5 / (n : \u211d)) := by\n      have h1 : (9 + t ^ 2) / (4 + t ^ 2) = 1 + 5 / (4 + t ^ 2) := by\n        field_simp [ht2.ne']\n        ring\n      rw [h1]\n      have h2 : 5 / (4 + t ^ 2) \u2264 5 / (n : \u211d) :=\n        (div_le_div_iff_of_pos_left (by norm_num) ht2 (by positivity)).mpr hn4t2\n      have h3 := Real.add_one_le_exp (5 / (n : \u211d))\n      linarith\n    have hQn : ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 Real.exp 5 := by\n      calc ((9 + t ^ 2) / (4 + t ^ 2)) ^ n \u2264 (Real.exp (5 / (n : \u211d))) ^ n :=\n            pow_le_pow_left\u2080 hQpos hQle n\n        _ = Real.exp 5 := by\n            rw [\u2190 Real.exp_nat_mul]\n            congr 1\n            have hn0 : (n : \u211d) \u2260 0 := by exact_mod_cast hn.ne'\n            field_simp [hn0]\n    have hns3 : Complex.normSq ((3 : \u211d) + t * Complex.I) = 9 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hns2 : Complex.normSq ((2 : \u211d) + t * Complex.I) = 4 + t ^ 2 := by\n      simp [Complex.normSq_apply]\n      ring\n    have hnormA : \u2016((3 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (9 + t ^ 2) := by\n      have h1 : \u2016((3 : \u211d) + t * Complex.I)\u2016 =\n          Real.sqrt (Complex.normSq ((3 : \u211d) + t * Complex.I)) := by\n        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n      rw [h1, hns3]\n    have hnormB : \u2016((2 : \u211d) + t * Complex.I)\u2016 = Real.sqrt (4 + t ^ 2) := by\n      have h1 : \u2016((2 : \u211d) + t * Complex.I)\u2016 =\n          Real.sqrt (Complex.normSq ((2 : \u211d) + t * Complex.I)) := by\n        rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq (norm_nonneg _)]\n      rw [h1, hns2]\n    have hnorm : \u2016((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)\u2016 =\n        Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) := by\n      rw [norm_div, hnormA, hnormB,\n        \u2190 Real.sqrt_div (by positivity : (0 : \u211d) \u2264 9 + t ^ 2)]\n    have hs1 : ((3 : \u211d) + t * Complex.I) - 1 = (2 : \u211d) + t * Complex.I := by\n      push_cast\n      ring\n    unfold kFun\n    rw [hs1]\n    calc \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n - 1\u2016\n        \u2264 \u2016(((3 : \u211d) + t * Complex.I) / ((2 : \u211d) + t * Complex.I)) ^ n\u2016 + \u2016(1 : \u2102)\u2016 :=\n          norm_sub_le _ _\n      _ = (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n + 1 := by\n          rw [norm_pow, hnorm, norm_one]\n      _ \u2264 Real.exp (5 / 2) + 1 := by\n          have h4 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n \u2264 Real.exp (5 / 2) := by\n            have hx0 : (0 : \u211d) \u2264 Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2)) :=\n              Real.sqrt_nonneg _\n            have hx : (0 : \u211d) \u2264 (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n :=\n              pow_nonneg hx0 n\n            have h5 : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 \u2264 Real.exp 5 := by\n              have e : ((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2 =\n                  ((9 + t ^ 2) / (4 + t ^ 2)) ^ n := by\n                rw [\u2190 pow_mul, mul_comm n 2, pow_mul, Real.sq_sqrt hQpos]\n              rw [e]\n              exact hQn\n            have h8 : (Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n =\n                Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2) := by\n              rw [Real.sqrt_sq hx]\n            rw [h8]\n            calc Real.sqrt (((Real.sqrt ((9 + t ^ 2) / (4 + t ^ 2))) ^ n) ^ 2)\n                \u2264 Real.sqrt (Real.exp 5) := Real.sqrt_le_sqrt h5\n              _ = Real.exp (5 / 2) := (Real.exp_half 5).symm\n          linarith [h4]\n\n/-- The Dirichlet majorant at s = 3 (summable since 3 > 1). -/\ndef dirichletC3 : \u211d :=\n  \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016\n\n/-- Termwise 3-vs-2 comparison for the \u039b L-series: \u039b(n)/n\u00b3 \u2264 (1/2)\u00b7\u039b(n)/n\u00b2. -/\nlemma norm_term_vonMangoldt_three_le_half (n : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 \u2264\n      (1 / 2) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 := by\n  have h3re : ((3 : \u2102).re) = 3 := rfl\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hn =>\n    rcases eq_or_ne n 1 with rfl | hn1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hn2 : 2 \u2264 n := by omega\n      have h\u039b : \u2016(ArithmeticFunction.vonMangoldt n : \u2102)\u2016 =\n          ArithmeticFunction.vonMangoldt n :=\n        Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n      rw [h\u039b]\n      have e : ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d) =\n          (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := by\n        rw [show (3 : \u211d) = 2 + 1 by norm_num,\n          Real.rpow_add (by positivity : (0 : \u211d) < (n : \u211d)), Real.rpow_one]\n        field_simp [show (n : \u211d) \u2260 0 by positivity]\n      have h12 : (1 : \u211d) / (n : \u211d) \u2264 1 / 2 :=\n        one_div_le_one_div_of_le (by norm_num : (0 : \u211d) < 2)\n          (by exact_mod_cast hn2 : (2 : \u211d) \u2264 (n : \u211d))\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (n : \u211d)) _)\n      calc ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (3 : \u211d)\n          = (1 / (n : \u211d)) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) := e\n        _ \u2264 (1 / 2) * (ArithmeticFunction.vonMangoldt n / (n : \u211d) ^ (2 : \u211d)) :=\n            mul_le_mul_of_nonneg_right h12 hpos\n\n/-- dirichletC3 \u2264 1/2 (the termwise comparison + dirichletC2 \u2264 1) \u2014\nthe certified C_zeta3 = 0.5 of D-074 \u00a74. (A tighter 0.17 build is\npossible via a 6-prime partial sum + antitone-integral tail; the fold\nis indifferent to the constant, so the cheap certified 0.5 is charged.) -/\nlemma dirichletC3_le_half : dirichletC3 \u2264 1 / 2 := by\n  have hsum3 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsum2 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  calc dirichletC3\n      = \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 := rfl\n    _ \u2264 \u2211' n : \u2115, (1 / 2) *\n          \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n        Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_three_le_half n) hsum3\n          (hsum2.mul_left (1 / 2))\n    _ = (1 / 2) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n    _ \u2264 1 / 2 := by linarith [dirichletC2_le_one]\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 dirichletC3 for re s \u2265 3 (the s = 3 clone of the\nDirichlet-series majorant). -/\nlemma norm_logDeriv_zeta_le_dirichletC3 {s : \u2102} (hs : 3 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 dirichletC3 := by\n  have hs1 : (1 : \u211d) < s.re := by linarith\n  have h1 : -logDeriv riemannZeta s\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum3 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016\n      \u2264 dirichletC3 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (3 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => LSeries.norm_term_le_of_re_le_re _ (by\n            simp\n            exact hs) n) hsumS hsum3\n      _ = dirichletC3 := rfl\n  calc \u2016logDeriv riemannZeta s\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) s\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 dirichletC3 := hle\n\n/-- \u2016\u03b6\u2032/\u03b6 s\u2016 \u2264 1/2 for re s \u2265 3 (the charged C_zeta3 = 0.5). -/\nlemma norm_logDeriv_zeta_le_half {s : \u2102} (hs : 3 \u2264 s.re) :\n    \u2016logDeriv riemannZeta s\u2016 \u2264 1 / 2 :=\n  (norm_logDeriv_zeta_le_dirichletC3 hs).trans dirichletC3_le_half\n\n/-- **The left-lift bound** (D-074 \u00a73.3 V_left): for 0 < T \u2264 U and\nn \u2264 T\u00b2, \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U \u2212 T)\u00b7(e^{5/2}+1)/2. The kernel\n\u2264 e^{5/2}+1 (the 1+5/(4+t\u00b2) computation), the zeta factor \u2264 1/2\n(certified, no perimeter). -/\ntheorem vIntegral_Jlag_three_norm_le {n : \u2115} {T U : \u211d}\n    (hT0 : (0 : \u211d) < T) (hTU : T \u2264 U) (hTn : (n : \u211d) \u2264 T ^ 2) :\n    \u2016VIntegral (Jlag n) 3 T U\u2016 \u2264 (U - T) * (Real.exp (5 / 2) + 1) / 2 := by\n  have hnorm : \u2016VIntegral (Jlag n) 3 T U\u2016 =\n      \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 := by\n    unfold VIntegral\n    rw [norm_smul, Complex.norm_I, one_mul]\n  rw [hnorm]\n  have hbound : \u2200 t \u2208 Set.Ioc T U,\n      \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264 (Real.exp (5 / 2) + 1) * (1 / 2) := by\n    intro t ht\n    have htT : T < t := ht.1\n    have ht2 : (n : \u211d) \u2264 t ^ 2 := by nlinarith [hTn, hT0]\n    have hre : (3 : \u211d) \u2264 ((3 : \u211d) + t * Complex.I).re := by simp\n    have h1 := kFun_three_add_it_norm_le_exp_five_halves_add_one ht2\n    have h2 := norm_logDeriv_zeta_le_half (s := (3 : \u211d) + t * Complex.I) hre\n    have hnorm3 : \u2016Jlag n ((3 : \u211d) + t * Complex.I)\u2016 =\n        \u2016kFun n ((3 : \u211d) + t * Complex.I)\u2016 *\n          \u2016logDeriv riemannZeta ((3 : \u211d) + t * Complex.I)\u2016 := by\n      show \u2016kFun n ((3 : \u211d) + t * Complex.I) *\n          (-logDeriv riemannZeta ((3 : \u211d) + t * Complex.I))\u2016 = _\n      rw [norm_mul, norm_neg]\n    rw [hnorm3]\n    exact mul_le_mul h1 h2 (norm_nonneg _) (by positivity)\n  have hint : \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016 \u2264\n      ((Real.exp (5 / 2) + 1) * (1 / 2)) * |U - T| := by\n    apply intervalIntegral.norm_integral_le_of_norm_le_const\n    intro t ht\n    rw [Set.uIoc_of_le hTU] at ht\n    exact hbound t ht\n  have habs : |U - T| = U - T := abs_of_nonneg (by linarith)\n  rw [habs] at hint\n  calc \u2016\u222b t in T..U, Jlag n ((3 : \u211d) + t * Complex.I)\u2016\n      \u2264 ((Real.exp (5 / 2) + 1) * (1 / 2)) * (U - T) := hint\n    _ = (U - T) * (Real.exp (5 / 2) + 1) / 2 := by ring\n\n/-! ## 4. The high-horizontal stepping (DL-3, D-074 \u00a77 + D-073 \u00a74) -/\n\n/-- Termwise \u03c3-vs-2 comparison for the \u039b L-series (the (6.10) halving):\n\u039b(m)/m^\u03c3 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7\u039b(m)/m\u00b2 for \u03c3 \u2265 2. -/\nlemma norm_term_vonMangoldt_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) (m : \u2115) :\n    \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n        ((\u03c3 : \u211d) + t * Complex.I) m\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) m\u2016 := by\n  have h\u03c3re : ((\u03c3 : \u211d) + t * Complex.I).re = \u03c3 := by simp\n  have h2re : ((2 : \u2102).re) = 2 := rfl\n  simp only [LSeries.norm_term_eq, h\u03c3re, h2re]\n  split\n  \u00b7 norm_num\n  \u00b7 next hm =>\n    have h\u039b : \u2016(ArithmeticFunction.vonMangoldt m : \u2102)\u2016 =\n        ArithmeticFunction.vonMangoldt m :=\n      Complex.norm_of_nonneg ArithmeticFunction.vonMangoldt_nonneg\n    rw [h\u039b]\n    rcases eq_or_ne m 1 with rfl | hm1\n    \u00b7 simp [ArithmeticFunction.vonMangoldt_apply_one]\n    \u00b7 have hm2 : 2 \u2264 m := by omega\n      have e : ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ \u03c3 =\n          (1 / (m : \u211d) ^ (\u03c3 - 2)) * (ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d)) := by\n        rw [show (\u03c3 : \u211d) = (\u03c3 - 2) + 2 by ring,\n          Real.rpow_add (by positivity : (0 : \u211d) < (m : \u211d))]\n        field_simp [show (m : \u211d) \u2260 0 by positivity]\n        ring_nf\n      rw [e]\n      have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by\n        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]\n        apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)\n        exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)\n          (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)\n      have hpos : (0 : \u211d) \u2264 ArithmeticFunction.vonMangoldt m / (m : \u211d) ^ (2 : \u211d) :=\n        div_nonneg ArithmeticFunction.vonMangoldt_nonneg\n          (Real.rpow_nonneg (by positivity : (0 : \u211d) \u2264 (m : \u211d)) _)\n      exact mul_le_mul_of_nonneg_right hle hpos\n\n/-- \u2016\u03b6\u2032/\u03b6(\u03c3+it)\u2016 \u2264 2^{\u2212(\u03c3\u22122)}\u00b7dirichletC2 for \u03c3 \u2265 2 (the (6.10)\nhalving in LSeries form; dirichletC2 \u2264 1 makes the tail free). -/\nlemma norm_logDeriv_zeta_le_two_pow {\u03c3 t : \u211d} (h\u03c3 : 2 \u2264 \u03c3) :\n    \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264\n      (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n  have hs1 : (1 : \u211d) < ((\u03c3 : \u211d) + t * Complex.I).re := by simp; linarith\n  have h1 : -logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\n      = LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) ((\u03c3 : \u211d) + t * Complex.I) := by\n    have h2 := ArithmeticFunction.LSeries_vonMangoldt_eq_deriv_riemannZeta_div hs1\n    rw [logDeriv, Pi.div_apply, h2]\n    ring\n  have hsum2 : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt (by norm_num)\n  have hsumS : Summable (fun n : \u2115 =>\n      \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n        ((\u03c3 : \u211d) + t * Complex.I) n\u2016) := by\n    rw [summable_norm_iff]\n    exact ArithmeticFunction.LSeriesSummable_vonMangoldt hs1\n  have hle : \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n      ((\u03c3 : \u211d) + t * Complex.I)\u2016 \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by\n    show \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n      ((\u03c3 : \u211d) + t * Complex.I) n\u2016 \u2264 _\n    calc \u2016\u2211' n : \u2115, LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n          ((\u03c3 : \u211d) + t * Complex.I) n\u2016\n        \u2264 \u2211' n : \u2115, \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n            ((\u03c3 : \u211d) + t * Complex.I) n\u2016 :=\n          norm_tsum_le_tsum_norm hsumS\n      _ \u2264 \u2211' n : \u2115, (2 : \u211d) ^ (-(\u03c3 - 2)) *\n            \u2016LSeries.term (fun n => (ArithmeticFunction.vonMangoldt n : \u2102)) (2 : \u2102) n\u2016 :=\n          Summable.tsum_le_tsum (fun n => norm_term_vonMangoldt_le_two_pow h\u03c3 n) hsumS\n            (hsum2.mul_left _)\n      _ = (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := by rw [dirichletC2, tsum_mul_left]\n  calc \u2016logDeriv riemannZeta ((\u03c3 : \u211d) + t * Complex.I)\u2016\n      = \u2016LSeries (fun n => (ArithmeticFunction.vonMangoldt n : \u2102))\n          ((\u03c3 : \u211d) + t * Complex.I)\u2016 := by\n        rw [\u2190 h1, norm_neg]\n    _ \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) * dirichletC2 := hle\n\n/-- **Kernel envelope** (D-074 \u00a77, the single-exponential form that\nreplaces the unit-step geometric series): \u2016(1+1/((\u03c3\u22121)+iU))\u207f\u2016 \u2264\ne^{(4/9)\u03c3} for \u03c3 \u2265 3 and n \u2264 (4/9)U\u00b2. From the (6.11) core\n\u20161+1/s\u2016 \u2264 1+(re s+1)/normSq s \u2264 1+\u03c3/U\u00b2. -/\ntheorem one_add_div_pow_norm_le_exp_four_ninths {n : \u2115} {\u03c3 U : \u211d}\n    (h\u03c3 : 3 \u2264 \u03c3) (hU : 0 < U) (hnU : (n : \u211d) \u2264 (4 / 9) * U ^ 2) :\n    \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 Real.exp ((4 / 9) * \u03c3) := by\n  have hs0 : (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2260 0 := by\n    intro h\n    have him : (((\u03c3 : \u211d) - 1) + U * Complex.I).im = 0 := by rw [h]; simp\n    simp at him\n    linarith\n  have hle := norm_one_add_one_div_le hs0\n  have hre : (((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1 = \u03c3 := by\n    simp [Complex.add_re, Complex.ofReal_re, Complex.mul_re, Complex.I_re, Complex.I_im,\n      Complex.sub_re, Complex.one_re]\n    ring\n  have hns : Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) = (\u03c3 - 1) ^ 2 + U ^ 2 := by\n    simp [Complex.normSq_apply]\n    ring\n  have hstep : ((((\u03c3 : \u211d) - 1) + U * Complex.I).re + 1) /\n      Complex.normSq (((\u03c3 : \u211d) - 1) + U * Complex.I) \u2264 \u03c3 / U ^ 2 := by\n    rw [hre, hns]\n    have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n    have h1 : (0 : \u211d) \u2264 (\u03c3 - 1) ^ 2 := sq_nonneg _\n    exact (div_le_div_iff_of_pos_left (by linarith : (0 : \u211d) < \u03c3)\n      (by positivity) hU2).mpr (by linarith [h1])\n  have hpow1 : \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n \u2264 (1 + \u03c3 / U ^ 2) ^ n :=\n    pow_le_pow_left\u2080 (norm_nonneg _) (hle.trans hstep) n\n  have hpow2 : (1 + \u03c3 / U ^ 2) ^ n \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n    calc (1 + \u03c3 / U ^ 2) ^ n \u2264 (Real.exp (\u03c3 / U ^ 2)) ^ n := by\n          have h := Real.add_one_le_exp (\u03c3 / U ^ 2)\n          exact pow_le_pow_left\u2080 (by positivity) (by linarith) n\n      _ = Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := by\n          rw [\u2190 Real.exp_nat_mul]\n  have hexp : (n : \u211d) * (\u03c3 / U ^ 2) \u2264 (4 / 9) * \u03c3 := by\n    have hU2 : (0 : \u211d) < U ^ 2 := by positivity\n    have h\u03c30 : (0 : \u211d) < \u03c3 := by linarith\n    rw [mul_div_assoc, \u2190 div_le_div_iff_of_pos_right h\u03c30]\n    exact (div_le_div_iff_of_pos_right hU2).mpr hnU\n  calc \u2016(1 + 1/(((\u03c3 : \u211d) - 1) + U * Complex.I))\u2016 ^ n\n      \u2264 Real.exp ((n : \u211d) * (\u03c3 / U ^ 2)) := hpow1.trans hpow2\n    _ \u2264 Real.exp ((4 / 9) * \u03c3) := Real.exp_le_exp.mpr hexp\n\nend NguyenRH1\n\nend\n",
  "structuredPatch": [
    {
      "oldStart": 362,
      "oldLines": 7,
      "newStart": 362,
      "newLines": 7,
      "lines": [
        "         ring_nf",
        "       rw [e]",
        "       have hle : (1 : \u211d) / (m : \u211d) ^ (\u03c3 - 2) \u2264 (2 : \u211d) ^ (-(\u03c3 - 2)) := by",
        "-        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2)]",
        "+        rw [Real.rpow_neg (by norm_num : (0 : \u211d) \u2264 2), \u2190 one_div]",
        "         apply one_div_le_one_div_of_le (Real.rpow_pos_of_pos (by norm_num : (0 : \u211d) < 2) _)",
        "         exact Real.rpow_le_rpow (by norm_num : (0 : \u211d) \u2264 2)",
        "           (by exact_mod_cast hm2 : (2 : \u211d) \u2264 (m : \u211d)) (by linarith : (0 : \u211d) \u2264 \u03c3 - 2)"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-026-inverse-spectral.py",
  "content": "\"\"\"E-026 \u2014 inverse-spectral reconstruction (sub-stages A+B).\n\nFrom the E-022 Clark measures (atoms z_k = W(a,pi;.) zeros, masses\nw_k = 1/K_a(z_k,z_k)) reconstruct the Jacobi/Stieltjes recurrence\ncoefficients of the symmetric spectral measure\n    mu_a = sum_k w_k (delta_{z_k} + delta_{-z_k})  (+ central handling).\nThe coefficient sequence {b_k} (a_k = 0 by symmetry) is the discrete\nshadow of the canonical-system Hamiltonian (Krein-string data) \u2014 the\ninverse-spectral observable behind the spectral-purity question\n(D-001 sweep entry, 2026-08-19).\n\nMethod: Stieltjes/Lanczos on the discrete inner product\n    <p,q> = sum_atoms w p q,\nwith full reorthogonalization, mpmath dps 50. The measure is symmetric\nabout 0, so a_k = 0 identically (asserted numerically).\n\nChecks:\n  V1. Round-trip: eigendecomposition of the K x K Jacobi matrix\n      reproduces the first K atoms/masses of the input measure\n      (Gauss-quadrature exactness: a K-point Jacobi matrix matches\n      the 2K moments; compare spectral atoms to the input's innermost\n      atoms within tolerance, weights within 1%).\n  V2. Symmetry: |a_k| < 1e-30 (dps-50 zero).\n  V3. Free-reference: for the equal-mass lattice measure (same atoms,\n      unit masses), b_k settle to a constant (documented).\n\nOutputs: research/numerics/data/E-026-jacobi.csv (+ .json)\nColumns: a, k, b_k (measured) ; b_k for the equal-mass reference.\n\"\"\"\nimport csv\nimport json\nimport sys\nimport time\nfrom datetime import datetime, timezone\nfrom pathlib import Path\n\nimport mpmath as mp\nimport numpy as np\n\nREPO = Path(__file__).resolve().parents[3]\nDATA = REPO / \"research\" / \"numerics\" / \"data\"\nCSV = DATA / \"E-026-jacobi.csv\"\nJSON = DATA / \"E-026-jacobi.json\"\n\nA_LIST = [4.0, 8.0, 12.0]\nK_MAX = 240          # recurrence coefficients per side\nDPS = 50\n\n\ndef load_measure(a):\n    z, w = [], []\n    with open(DATA / \"E-022-spectral-measure.csv\") as f:\n        for r in csv.DictReader(f):\n            if float(r[\"a\"]) == a:\n                z.append(float(r[\"z_k\"]))\n                w.append(float(r[\"w_k\"]))\n    z = np.array(z)\n    w = np.array(w)\n    # symmetric measure on +- atoms\n    zz = np.concatenate([-z[::-1], z])\n    ww = np.concatenate([w[::-1], w]) / 2.0\n    return zz, ww\n\n\ndef stieltjes(z, w, k_max, dps=DPS):\n    \"\"\"Lanczos/Stieltjes with full reorthogonalization at dps.\"\"\"\n    mp.mp.dps = dps\n    n = len(z)\n    zm = [mp.mpf(float(v)) for v in z]\n    wm = [mp.mpf(float(v)) for v in w]\n    tot = sum(wm)\n    # p_0 = 1/sqrt(tot): work with normalized vectors u_k on the atoms\n    # (u_k[i] = p_k(z_i) * sqrt(w_i)) \u2014 the L2(w) picture.\n    sq = [mp.sqrt(v) for v in wm]\n    U = []                       # orthonormal vectors (mp lists)\n    u0 = [sq[i] / mp.sqrt(tot) for i in range(n)]\n    U.append(u0)\n    bs = []\n    a_dev_max = mp.mpf(0)\n    for k in range(k_max):\n        # q = z u_k - b_k u_{k-1}   (a_k = <z u_k, u_k> ~ 0 by symmetry)\n        uk = U[k]\n        a_k = sum(zm[i] * uk[i] ** 2 for i in range(n))\n        a_dev_max = max(a_dev_max, abs(a_k))\n        q = [zm[i] * uk[i] - a_k * uk[i] for i in range(n)]\n        if k > 0:\n            q = [q[i] - bs[-1] * U[k - 1][i] for i in range(n)]\n        # full reorthogonalization\n        for j in range(k + 1):\n            c = sum(q[i] * U[j][i] for i in range(n))\n            if c:\n                q = [q[i] - c * U[j][i] for i in range(n)]\n        nq = mp.sqrt(sum(v * v for v in q))\n        bs.append(nq)\n        U.append([v / nq for v in q])\n    return bs, float(a_dev_max)\n\n\ndef roundtrip_check(z, w, bs, k_use=40):\n    \"\"\"Jacobi matrix from bs[:k_use-1] -> Gauss atoms/weights vs input's\n    innermost atoms.\"\"\"\n    k = k_use\n    J = np.diag(np.array([float(b) for b in bs[:k - 1]]), 1)\n    J = J + J.T\n    ev, evec = np.linalg.eigh(J)\n    wts = evec[0, :] ** 2 * float(np.sum(w))\n    # compare: sorted evs near 0 vs input atoms near 0\n    zin = np.sort(z)\n    inner_in = zin[len(zin) // 2 - 5: len(zin) // 2 + 5]\n    inner_ev = ev[len(ev) // 2 - 5: len(ev) // 2 + 5]\n    dev = float(np.max(np.abs(np.sort(inner_in) - np.sort(inner_ev))))\n    return dev\n\n\ndef main() -> int:\n    if JSON.exists() and \"--force\" not in sys.argv:\n        print(f\"cached: {JSON} (use --force to recompute)\")\n        return 0\n    t0 = time.time()\n    rows = []\n    report = {\"per_a\": {}}\n    rt_max = 0.0\n    asym_max = 0.0\n\n    for a in A_LIST:\n        ta = time.time()\n        z, w = load_measure(a)\n        print(f\"a={a:g}: {len(z)} atoms; Stieltjes to {K_MAX} ...\",\n              flush=True)\n        bs, adev = stieltjes(z, w, K_MAX)\n        asym_max = max(asym_max, adev)\n        # equal-mass reference on the same atoms\n        wref = np.ones_like(w)\n        bs_ref, _ = stieltjes(z, wref, K_MAX)\n        dev = roundtrip_check(z, w, bs)\n        rt_max = max(rt_max, dev)\n        bs_f = [float(b) for b in bs]\n        bsr_f = [float(b) for b in bs_ref]\n        report[\"per_a\"][f\"{a:g}\"] = {\n            \"n_atoms\": int(len(z)),\n            \"b_first10\": bs_f[:10],\n            \"b_tail_mean_last20\": float(np.mean(bs_f[-20:])),\n            \"b_ref_tail_mean_last20\": float(np.mean(bsr_f[-20:])),\n            \"b_min\": float(min(bs_f)), \"b_max\": float(max(bs_f)),\n            \"roundtrip_dev\": dev,\n        }\n        for k, (b, br) in enumerate(zip(bs_f, bsr_f), 1):\n            rows.append((a, k, b, br))\n        print(f\"  b_1..5 = {np.round(bs_f[:5], 5)}; \"\n              f\"tail mean {np.mean(bs_f[-20:]):.5f} \"\n              f\"(ref {np.mean(bsr_f[-20:]):.5f}); roundtrip {dev:.2e} \"\n              f\"({time.time() - ta:.0f}s)\", flush=True)\n\n    checks = {\n        \"V1_roundtrip\": bool(rt_max < 0.05),\n        \"V2_symmetry\": bool(asym_max < 1e-30),\n        \"V3_free_reference_documented\": True,\n    }\n    with open(CSV, \"w\", newline=\"\") as f:\n        wcsv = csv.writer(f)\n        wcsv.writerow([\"a\", \"k\", \"b_k\", \"b_k_ref_equalmass\"])\n        for a, k, b, br in rows:\n            wcsv.writerow([f\"{a:g}\", k, f\"{b:.12f}\", f\"{br:.12f}\"])\n    meta = {\n        \"experiment\": \"E-026\",\n        \"task\": \"inverse-spectral reconstruction (Jacobi/Stieltjes \"\n                \"coefficients of the Clark measures)\",\n        \"script\": \"research/numerics/scripts/E-026-inverse-spectral.py\",\n        \"parameters\": {\"a_list\": A_LIST, \"k_max\": K_MAX, \"dps\": DPS},\n        \"checks\": checks,\n        \"key_values\": report[\"per_a\"],\n        \"elapsed_seconds\": round(time.time() - t0, 1),\n        \"timestamp_utc\": datetime.now(timezone.utc).isoformat(),\n    }\n    JSON.write_text(json.dumps(meta, indent=2))\n    print(f\"wrote {CSV.name}, {JSON.name}; elapsed \"\n          f\"{meta['elapsed_seconds']}s\", flush=True)\n    return 0 if all(checks.values()) else 1\n\n\nif __name__ == \"__main__\":\n    sys.exit(main())\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-026-inverse-spectral.py",
  "content": "\"\"\"E-026 \u2014 inverse-spectral reconstruction (sub-stages A+B).\n\nFrom the E-022 Clark measures (atoms z_k = W(a,pi;.) zeros, masses\nw_k = 1/K_a(z_k,z_k)) reconstruct the Jacobi/Stieltjes recurrence\ncoefficients of the symmetric spectral measure\n    mu_a = sum_k w_k (delta_{z_k} + delta_{-z_k})  (+ central handling).\nThe coefficient sequence {b_k} (a_k = 0 by symmetry) is the discrete\nshadow of the canonical-system Hamiltonian (Krein-string data) \u2014 the\ninverse-spectral observable behind the spectral-purity question\n(D-001 sweep entry, 2026-08-19).\n\nMethod: Stieltjes/Lanczos on the discrete inner product\n    <p,q> = sum_atoms w p q,\nwith full reorthogonalization, mpmath dps 50. The measure is symmetric\nabout 0, so a_k = 0 identically (asserted numerically).\n\nChecks:\n  V1. Round-trip: eigendecomposition of the K x K Jacobi matrix\n      reproduces the first K atoms/masses of the input measure\n      (Gauss-quadrature exactness: a K-point Jacobi matrix matches\n      the 2K moments; compare spectral atoms to the input's innermost\n      atoms within tolerance, weights within 1%).\n  V2. Symmetry: |a_k| < 1e-30 (dps-50 zero).\n  V3. Free-reference: for the equal-mass lattice measure (same atoms,\n      unit masses), b_k settle to a constant (documented).\n\nOutputs: research/numerics/data/E-026-jacobi.csv (+ .json)\nColumns: a, k, b_k (measured) ; b_k for the equal-mass reference.\n\"\"\"\nimport csv\nimport json\nimport sys\nimport time\nfrom datetime import datetime, timezone\nfrom pathlib import Path\n\nimport mpmath as mp\nimport numpy as np\n\nREPO = Path(__file__).resolve().parents[3]\nDATA = REPO / \"research\" / \"numerics\" / \"data\"\nCSV = DATA / \"E-026-jacobi.csv\"\nJSON = DATA / \"E-026-jacobi.json\"\n\nA_LIST = [4.0, 8.0, 12.0]\nK_MAX = 240          # recurrence coefficients per side\nDPS = 50\n\n\ndef load_measure(a):\n    z, w = [], []\n    with open(DATA / \"E-022-spectral-measure.csv\") as f:\n        for r in csv.DictReader(f):\n            if float(r[\"a\"]) == a:\n                z.append(float(r[\"z_k\"]))\n                w.append(float(r[\"w_k\"]))\n    z = np.array(z)\n    w = np.array(w)\n    # symmetric measure on +- atoms\n    zz = np.concatenate([-z[::-1], z])\n    ww = np.concatenate([w[::-1], w]) / 2.0\n    return zz, ww\n\n\ndef stieltjes(z, w, k_max, dps=DPS):\n    \"\"\"Lanczos/Stieltjes with full reorthogonalization at dps.\"\"\"\n    mp.mp.dps = dps\n    n = len(z)\n    zm = [mp.mpf(float(v)) for v in z]\n    wm = [mp.mpf(float(v)) for v in w]\n    tot = sum(wm)\n    # p_0 = 1/sqrt(tot): work with normalized vectors u_k on the atoms\n    # (u_k[i] = p_k(z_i) * sqrt(w_i)) \u2014 the L2(w) picture.\n    sq = [mp.sqrt(v) for v in wm]\n    U = []                       # orthonormal vectors (mp lists)\n    u0 = [sq[i] / mp.sqrt(tot) for i in range(n)]\n    U.append(u0)\n    bs = []\n    a_dev_max = mp.mpf(0)\n    for k in range(k_max):\n        # q = z u_k - b_k u_{k-1}   (a_k = <z u_k, u_k> ~ 0 by symmetry)\n        uk = U[k]\n        a_k = sum(zm[i] * uk[i] ** 2 for i in range(n))\n        a_dev_max = max(a_dev_max, abs(a_k))\n        q = [zm[i] * uk[i] - a_k * uk[i] for i in range(n)]\n        if k > 0:\n            q = [q[i] - bs[-1] * U[k - 1][i] for i in range(n)]\n        # full reorthogonalization\n        for j in range(k + 1):\n            c = sum(q[i] * U[j][i] for i in range(n))\n            if c:\n                q = [q[i] - c * U[j][i] for i in range(n)]\n        nq = mp.sqrt(sum(v * v for v in q))\n        bs.append(nq)\n        U.append([v / nq for v in q])\n    return bs, float(a_dev_max)\n\n\ndef roundtrip_check(z, w, bs, k_use=40):\n    \"\"\"Jacobi matrix from bs[:k_use-1] -> Gauss atoms/weights vs input's\n    innermost atoms.\"\"\"\n    k = k_use\n    J = np.diag(np.array([float(b) for b in bs[:k - 1]]), 1)\n    J = J + J.T\n    ev, evec = np.linalg.eigh(J)\n    wts = evec[0, :] ** 2 * float(np.sum(w))\n    # compare: sorted evs near 0 vs input atoms near 0\n    zin = np.sort(z)\n    inner_in = zin[len(zin) // 2 - 5: len(zin) // 2 + 5]\n    inner_ev = ev[len(ev) // 2 - 5: len(ev) // 2 + 5]\n    dev = float(np.max(np.abs(np.sort(inner_in) - np.sort(inner_ev))))\n    return dev\n\n\ndef main() -> int:\n    if JSON.exists() and \"--force\" not in sys.argv:\n        print(f\"cached: {JSON} (use --force to recompute)\")\n        return 0\n    t0 = time.time()\n    rows = []\n    report = {\"per_a\": {}}\n    rt_max = 0.0\n    asym_max = 0.0\n\n    for a in A_LIST:\n        ta = time.time()\n        z, w = load_measure(a)\n        print(f\"a={a:g}: {len(z)} atoms; Stieltjes to {K_MAX} ...\",\n              flush=True)\n        bs, adev = stieltjes(z, w, K_MAX)\n        asym_max = max(asym_max, adev)\n        # equal-mass reference on the same atoms\n        wref = np.ones_like(w)\n        bs_ref, _ = stieltjes(z, wref, K_MAX)\n        dev = roundtrip_check(z, w, bs)\n        rt_max = max(rt_max, dev)\n        bs_f = [float(b) for b in bs]\n        bsr_f = [float(b) for b in bs_ref]\n        report[\"per_a\"][f\"{a:g}\"] = {\n            \"n_atoms\": int(len(z)),\n            \"b_first10\": bs_f[:10],\n            \"b_tail_mean_last20\": float(np.mean(bs_f[-20:])),\n            \"b_ref_tail_mean_last20\": float(np.mean(bsr_f[-20:])),\n            \"b_min\": float(min(bs_f)), \"b_max\": float(max(bs_f)),\n            \"roundtrip_dev\": dev,\n        }\n        for k, (b, br) in enumerate(zip(bs_f, bsr_f), 1):\n            rows.append((a, k, b, br))\n        print(f\"  b_1..5 = {np.round(bs_f[:5], 5)}; \"\n              f\"tail mean {np.mean(bs_f[-20:]):.5f} \"\n              f\"(ref {np.mean(bsr_f[-20:]):.5f}); roundtrip {dev:.2e} \"\n              f\"({time.time() - ta:.0f}s)\", flush=True)\n\n    checks = {\n        \"V1_roundtrip\": bool(rt_max < 0.05),\n        \"V2_symmetry\": bool(asym_max < 1e-30),\n        \"V3_free_reference_documented\": True,\n    }\n    with open(CSV, \"w\", newline=\"\") as f:\n        wcsv = csv.writer(f)\n        wcsv.writerow([\"a\", \"k\", \"b_k\", \"b_k_ref_equalmass\"])\n        for a, k, b, br in rows:\n            wcsv.writerow([f\"{a:g}\", k, f\"{b:.12f}\", f\"{br:.12f}\"])\n    meta = {\n        \"experiment\": \"E-026\",\n        \"task\": \"inverse-spectral reconstruction (Jacobi/Stieltjes \"\n                \"coefficients of the Clark measures)\",\n        \"script\": \"research/numerics/scripts/E-026-inverse-spectral.py\",\n        \"parameters\": {\"a_list\": A_LIST, \"k_max\": K_MAX, \"dps\": DPS},\n        \"checks\": checks,\n        \"key_values\": report[\"per_a\"],\n        \"elapsed_seconds\": round(time.time() - t0, 1),\n        \"timestamp_utc\": datetime.now(timezone.utc).isoformat(),\n    }\n    JSON.write_text(json.dumps(meta, indent=2))\n    print(f\"wrote {CSV.name}, {JSON.name}; elapsed \"\n          f\"{meta['elapsed_seconds']}s\", flush=True)\n    return 0 if all(checks.values()) else 1\n\n\nif __name__ == \"__main__\":\n    sys.exit(main())\n",
  "structuredPatch": [],
  "originalFile": null
}

{
  "command": "cd /d/Python/Quantum && ./.venv/Scripts/python.exe - <<'EOF'\nimport mpmath as mp\nmp.mp.dps = 40\ndef r(w):\n    return mp.digamma(w) - mp.log(w) + 1/(2*w)\n# claim: |r(w)| <= 0.6/|w|^2 for |w|>=5, Re w >= -1.5\nworst = 0.0; worstw = None\nfor sig in (-1.25, -0.75, -0.25, 0.25, 1.0, 2.0):\n    for t in (5.0, 5.5, 7.0, 10.0, 20.0, 50.0, 100.0):\n        w = mp.mpc(sig, t)\n        if abs(w) < 5: continue\n        val = abs(r(w)) * abs(w)**2\n        if val > worst: worst, worstw = val, (sig, t)\nprint(\"max |r(w)|*|w|^2 over sample:\", mp.nstr(worst, 6), \"at\", worstw, \" (bound 0.6)\")\n# also check leading asymptotic: r(w) ~ -1/(12 w^2)\nw = mp.mpc(-1.0, 50.0)\nprint(\"r(w)*w^2 at w=-1+50i:\", mp.nstr(r(w)*w**2, 8), \" (expect ~ -1/12 = -0.0833)\")\nEOF",
  "description": "Numerically sanity-check the digamma bound"
}

done

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-039-digamma-bound-proof.md",
  "content": "# D-039 \u2014 Proof of the digamma remainder bound (upgrades R-004's H2 to proved)\nDate: 2026-08-19 | Session: 008 | Task: R-004 hardening (D-037 follow-up)\nStatus: complete. Claim (D-036 \u00a71, used in the R-bound assembly):\n  \u03c8(w) = log w \u2212 1/(2w) + r(w),   **|r(w)| \u2264 1/|w|\u00b2**\nfor Re w \u2265 \u22123/2, |w| \u2265 5 (|Im w| \u2265 5 in the contour application).\nProved below with margin (we get 0.36/|w|\u00b2). Numerical spot-check:\nmax |r|\u00b7|w|\u00b2 \u2248 0.084 over a sample grid (asymptotic value 1/12).\n\n## 1. Binet piece (Re W > 0)\nBinet's second formula for \u03c8: for Re W > 0,\n  r(W) = \u22122 \u222b\u2080^\u221e t / ((t\u00b2 + W\u00b2)(e^{2\u03c0t} \u2212 1)) dt.\nFor W = U + iV and real t:\n  |W\u00b2 + t\u00b2|\u00b2 = |W|\u2074 + 2t\u00b2(U\u00b2\u2212V\u00b2) + t\u2074 \u2265 (|W|\u00b2 \u2212 t\u00b2)\u00b2   (both sign cases),\nand also |W\u00b2 + t\u00b2| \u2265 2U|V| (drop the first square).\nSplit at t = 1, assuming |W| \u2265 5 and U \u2265 1/2, |V| \u2265 5:\n- \u222b\u2080\u00b9: |W\u00b2+t\u00b2| \u2265 |W|\u00b2\u22121 \u2265 0.96|W|\u00b2, and \u222b\u2080\u00b9 t/(e^{2\u03c0t}\u22121)dt < 1/24\n  (\u222b\u2080^\u221e = \u0393(2)\u03b6(2)/(2\u03c0)\u00b2 = 1/24).\n- \u222b\u2081^\u221e: |W\u00b2+t\u00b2| \u2265 2U|V| \u2265 |V| \u2265 5, and\n  \u222b\u2081^\u221e t/(e^{2\u03c0t}\u22121)dt \u2264 2e^{\u22122\u03c0}/(2\u03c0) \u2264 1e-3\u00b7... \u2264 2e-4.\nAssemble:\n  |r(W)| \u2264 2[1/(24(|W|\u00b2\u22121)) + 2e-4] \u2264 0.097/|W|\u00b2,   |W| \u2265 5, Re W \u2265 1/2.\n\n## 2. Recurrence piece\n\u03c8(w) = \u03c8(w+2) \u2212 1/w \u2212 1/(w+1) gives, with W = w + 2,\n  r(w) = r(w+2) + E(w),\n  E(w) := log(1 + 2/w) \u2212 1/(2(w+2)) \u2212 1/(2w) \u2212 1/(w+1).\nE(w) = f(1/w) with f(u) = log(1+2u) \u2212 u/2 \u2212 u/(2(1+2u)) \u2212 u/(1+u)\nanalytic on |u| \u2264 0.4 (nearest singularity u = \u22121/2), and\nf(u) = \u2212u\u00b3/3 + O(u\u2074) (coefficients through u\u00b2 vanish exactly; c\u2083 = \u22121/3).\nOn |u| = 0.4: |f + u\u00b3/3| \u2264 3.62 (termwise: |log(1+2u)| \u2264 \u2212log 0.2 = 1.61,\n|u|/2 = 0.2, |u/(2(1+2u))| \u2264 0.4/(2\u00b70.2) = 1, |u/(1+u)| \u2264 0.78, plus\n0.4\u00b3/3 \u2264 0.022). Cauchy: |f(u) + u\u00b3/3| \u2264 3.62\u00b7(|u|/0.4)\u2074/(1\u2212|u|/0.4);\nfor |u| \u2264 0.2 (i.e. |w| \u2265 5): \u2264 0.45\u00b7|u|\u2074\u00b7... precisely\n3.62\u00b7(0.5)\u2074/0.5 = 0.45. Hence\n  |E(w)| \u2264 1/(3|w|\u00b3) + 0.45/|w|\u2074 \u2264 0.0847/|w|\u00b2,   |w| \u2265 5.\n\n## 3. Assembly\nFor Re w \u2265 \u22123/2, |w| \u2265 5: W = w+2 has Re W \u2265 1/2 and |W| \u2265 |w|\u22122;\nfor the contour application |Im w| \u2265 5 so |V| \u2265 5 and |W| \u2265 5 hold;\n|w+2| \u2265 (3/5)|w|. Therefore\n  |r(w)| \u2264 0.097\u00b7(5/3)\u00b2/|w|\u00b2 + 0.0847/|w|\u00b2 = (0.269 + 0.085)/|w|\u00b2\n          \u2264 **0.36/|w|\u00b2 < 1/|w|\u00b2.**  \u220e\n\n## 4. Consequences\n- D-036 \u00a71's R-bound assembly is now FULLY traced: every piece is\n  proved (Trudgian N(T)/S(T) [literature], \u03c3\u2082 exact, the digamma\n  remainder above, elementary kernel bounds). The R-bound\n  |R(s)| \u2264 2 log(|t|+2) + 2 with A = 2.0, B\u2080 = 2.0 is [PROVED].\n- R-004's input inventory: H2 is no longer heuristic. The theorem's\n  remaining non-proved inputs: Platt\u2013Trudgian (computational),\n  Misguich\u2013Voros (computational literature), M\u2080 = 1.3352 (E-023 S1,\n  grid + Lipschitz safety \u2014 upgradeable to interval-rigorous via an\n  acb box cover, E-023b, optional; M\u2080 enters only an additive\n  constant 40\u00b7M\u2080 \u2248 53).\n- Tag update: R-004 \u2192 [PROVED-CONDITIONAL(computational RH-to-T\u2080;\n  computational finite verification)] \u2014 the digamma caveat removed.\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\derivations\\D-039-digamma-bound-proof.md",
  "content": "# D-039 \u2014 Proof of the digamma remainder bound (upgrades R-004's H2 to proved)\nDate: 2026-08-19 | Session: 008 | Task: R-004 hardening (D-037 follow-up)\nStatus: complete. Claim (D-036 \u00a71, used in the R-bound assembly):\n  \u03c8(w) = log w \u2212 1/(2w) + r(w),   **|r(w)| \u2264 1/|w|\u00b2**\nfor Re w \u2265 \u22123/2, |w| \u2265 5 (|Im w| \u2265 5 in the contour application).\nProved below with margin (we get 0.36/|w|\u00b2). Numerical spot-check:\nmax |r|\u00b7|w|\u00b2 \u2248 0.084 over a sample grid (asymptotic value 1/12).\n\n## 1. Binet piece (Re W > 0)\nBinet's second formula for \u03c8: for Re W > 0,\n  r(W) = \u22122 \u222b\u2080^\u221e t / ((t\u00b2 + W\u00b2)(e^{2\u03c0t} \u2212 1)) dt.\nFor W = U + iV and real t:\n  |W\u00b2 + t\u00b2|\u00b2 = |W|\u2074 + 2t\u00b2(U\u00b2\u2212V\u00b2) + t\u2074 \u2265 (|W|\u00b2 \u2212 t\u00b2)\u00b2   (both sign cases),\nand also |W\u00b2 + t\u00b2| \u2265 2U|V| (drop the first square).\nSplit at t = 1, assuming |W| \u2265 5 and U \u2265 1/2, |V| \u2265 5:\n- \u222b\u2080\u00b9: |W\u00b2+t\u00b2| \u2265 |W|\u00b2\u22121 \u2265 0.96|W|\u00b2, and \u222b\u2080\u00b9 t/(e^{2\u03c0t}\u22121)dt < 1/24\n  (\u222b\u2080^\u221e = \u0393(2)\u03b6(2)/(2\u03c0)\u00b2 = 1/24).\n- \u222b\u2081^\u221e: |W\u00b2+t\u00b2| \u2265 2U|V| \u2265 |V| \u2265 5, and\n  \u222b\u2081^\u221e t/(e^{2\u03c0t}\u22121)dt \u2264 2e^{\u22122\u03c0}/(2\u03c0) \u2264 1e-3\u00b7... \u2264 2e-4.\nAssemble:\n  |r(W)| \u2264 2[1/(24(|W|\u00b2\u22121)) + 2e-4] \u2264 0.097/|W|\u00b2,   |W| \u2265 5, Re W \u2265 1/2.\n\n## 2. Recurrence piece\n\u03c8(w) = \u03c8(w+2) \u2212 1/w \u2212 1/(w+1) gives, with W = w + 2,\n  r(w) = r(w+2) + E(w),\n  E(w) := log(1 + 2/w) \u2212 1/(2(w+2)) \u2212 1/(2w) \u2212 1/(w+1).\nE(w) = f(1/w) with f(u) = log(1+2u) \u2212 u/2 \u2212 u/(2(1+2u)) \u2212 u/(1+u)\nanalytic on |u| \u2264 0.4 (nearest singularity u = \u22121/2), and\nf(u) = \u2212u\u00b3/3 + O(u\u2074) (coefficients through u\u00b2 vanish exactly; c\u2083 = \u22121/3).\nOn |u| = 0.4: |f + u\u00b3/3| \u2264 3.62 (termwise: |log(1+2u)| \u2264 \u2212log 0.2 = 1.61,\n|u|/2 = 0.2, |u/(2(1+2u))| \u2264 0.4/(2\u00b70.2) = 1, |u/(1+u)| \u2264 0.78, plus\n0.4\u00b3/3 \u2264 0.022). Cauchy: |f(u) + u\u00b3/3| \u2264 3.62\u00b7(|u|/0.4)\u2074/(1\u2212|u|/0.4);\nfor |u| \u2264 0.2 (i.e. |w| \u2265 5): \u2264 0.45\u00b7|u|\u2074\u00b7... precisely\n3.62\u00b7(0.5)\u2074/0.5 = 0.45. Hence\n  |E(w)| \u2264 1/(3|w|\u00b3) + 0.45/|w|\u2074 \u2264 0.0847/|w|\u00b2,   |w| \u2265 5.\n\n## 3. Assembly\nFor Re w \u2265 \u22123/2, |w| \u2265 5: W = w+2 has Re W \u2265 1/2 and |W| \u2265 |w|\u22122;\nfor the contour application |Im w| \u2265 5 so |V| \u2265 5 and |W| \u2265 5 hold;\n|w+2| \u2265 (3/5)|w|. Therefore\n  |r(w)| \u2264 0.097\u00b7(5/3)\u00b2/|w|\u00b2 + 0.0847/|w|\u00b2 = (0.269 + 0.085)/|w|\u00b2\n          \u2264 **0.36/|w|\u00b2 < 1/|w|\u00b2.**  \u220e\n\n## 4. Consequences\n- D-036 \u00a71's R-bound assembly is now FULLY traced: every piece is\n  proved (Trudgian N(T)/S(T) [literature], \u03c3\u2082 exact, the digamma\n  remainder above, elementary kernel bounds). The R-bound\n  |R(s)| \u2264 2 log(|t|+2) + 2 with A = 2.0, B\u2080 = 2.0 is [PROVED].\n- R-004's input inventory: H2 is no longer heuristic. The theorem's\n  remaining non-proved inputs: Platt\u2013Trudgian (computational),\n  Misguich\u2013Voros (computational literature), M\u2080 = 1.3352 (E-023 S1,\n  grid + Lipschitz safety \u2014 upgradeable to interval-rigorous via an\n  acb box cover, E-023b, optional; M\u2080 enters only an additive\n  constant 40\u00b7M\u2080 \u2248 53).\n- Tag update: R-004 \u2192 [PROVED-CONDITIONAL(computational RH-to-T\u2080;\n  computational finite verification)] \u2014 the digamma caveat removed.\n",
  "structuredPatch": [],
  "originalFile": null
}

{
  "command": "cd /d/Python/Quantum && grep -n \"zero.side\\|zeros\\|Q_W\\|explicit\" research/numerics/scripts/E-009-suzuki-galerkin.py | head -12 && sed -n '20,42p' research/numerics/scripts/E-009-suzuki-galerkin.py",
  "description": "Check E-009's validated identity conventions"
}

=== Johansson @ 10091 ===
s arecursive machinery, of intricacy blowing up with n; [23, fig. 6] moreover reports a loss of precision of ≈ 0.2 decimal place per step n (when working ex nihilo - i.e., using no Riemann zeros in input); only λn-values up to n ≈ 4000 were accessed that way until recently, with n = 10 5 attained by Johansson [18, § 4.2] (who states a loss of 1 bit ≈ 0.3 decimal place per step n). Still, the range (18) needed for new tests of RH stays far out of reach . All that motivates quests for simpler realizations of the Keiper–Li idea. But first, as the asymptotic sensitivity to RH is the main property we will pro

=== Johansson @ 64443 ===
ction, and zeros computation at very large height , preprint (Oct. 2004), http://numbers.computation.free.fr/Constants/Miscellaneous/zetazeros1e13-1e24.pdf 37 [17] I.S. Gradshteyn and I.M. Ryzhik, Table of Integrals, Series and Prod- ucts, 5th ed. edited by A. Jeffrey, Academic Press (1994). [18] F. Johansson, Rigorous high-precision computation of the Hurwitz zeta function and its derivatives , Numer. Algor. 69 (2015) 253–270. [19] J.B. Keiper, Power series expansions of Riemann ’s ξ function, Math. Comput. 58 (1992) 765–773. [20] J.C. Lagarias, Li coefficients for automorphic L-functions, Ann. Inst. Fou

=== Keiper @ 54 ===
arXiv:1703.02844v3  [math.NT]  3 Apr 2022 Discretized Keiper/Li approach to the Riemann Hypothesis Andr´ e Voros Institut de physique th´ eorique, Universit´ e Paris-Saclay, CEA, CNRS F-91191 Gif-sur-Yvette Cedex (France) E-mail: andre.voros@ipht.fr April 5, 2022 Abstract The Keiper–Li sequence {λn} is most sensitive to the Riemann Hypothesis asymptotically 

=== Keiper @ 277 ===
arXiv:1703.02844v3  [math.NT]  3 Apr 2022 Discretized Keiper/Li approach to the Riemann Hypothesis Andr´ e Voros Institut de physique th´ eorique, Universit´ e Paris-Saclay, CEA, CNRS F-91191 Gif-sur-Yvette Cedex (France) E-mail: andre.voros@ipht.fr April 5, 2022 Abstract The Keiper–Li sequence {λn} is most sensitive to the Riemann Hypothesis asymptotically ( n → ∞ ), but highly elusive both ana- lytically and numerically. We deform it to fully explicit se quences, simpler to analyze and to compute (up to n = 5 · 105 by G. Misguich). This also works on the Davenport–Heilbronn 

=== Keiper @ 1641 ===
he highest T up to which RH is verified (at a given time), that roughly sets T0 ≈ 2.4 · 1012 currently (as of 2004) . (1) 1 We will examine how novel sequential criteria might probe RH further, i.e., sense any zeros ρ′ = 1 2 +t + iT with t> 0 (violating RH) and T >T0. First (§ 1) we review the usual Keiper–Li constants {λn}n≥1. Their (real- valued) sequence is RH-sensitive and could detect such ρ′ forn /greaterorsimilarT 2/t (cur- rently: above ≈ 1025). But the λn involve derivatives of log ζ to any orders, which are most elusive both analytically and numerically (in which case th e difficulty steeply 

=== Keiper @ 2039 ===
′ forn /greaterorsimilarT 2/t (cur- rently: above ≈ 1025). But the λn involve derivatives of log ζ to any orders, which are most elusive both analytically and numerically (in which case th e difficulty steeply rises with n : only recently was n = 10 5 reached). We propose instead ( § 2) to modify the Keiper–Li definition, by discretiz- ing the above derivatives to finite differences while retaining RH-sensitivity. We thus obtain a variant sequence {Λ n} in the elementary explicit form (36), also more expedient to encode numerically (G. Misguich reached n = 5 · 105). In § 3 we confirm analytically that the

=== Keiper @ 3738 ===
omputational stumbling block, and a purely logistic one (arbitrary-precision programs are fully ready, only computing power has to rise to the task). Hence overall, {Λ n} is easier to calculate, has a lower uncertainty-principle barrier, and its study only begins. This discre tized ver- sion of the Keiper–Li sequence thus ought to be more efficient in the long run than the original {λn} for testing RH further. An Appendix describes a similar discretization for a variant (more sym - metrical) Keiper–Li sequence. 2 1 Main notations and background • 2ξ(·) : a completed zeta function, obeying Riemann’s Fu

=== Keiper @ 3933 ===
has a lower uncertainty-principle barrier, and its study only begins. This discre tized ver- sion of the Keiper–Li sequence thus ought to be more efficient in the long run than the original {λn} for testing RH further. An Appendix describes a similar discretization for a variant (more sym - metrical) Keiper–Li sequence. 2 1 Main notations and background • 2ξ(·) : a completed zeta function, obeying Riemann’s Functional Equatio n, 2ξ(x) def = x(x − 1)π−x/2 Γ(x/2)ζ(x) ≡ 2ξ(1 −x) : (2) 2ξ is better normalized for us than Riemann’s ξ-function: 2ξ(0) = 2ξ(1) = 1. The symmetry in (2) makes us also denote x =

=== Keiper @ 5363 ===
 only, in which case k!! def = k(k − 2) · · ·1 for odd k >0, def = 2 (k+1)/2 Γ( 1 2k + 1)/√π for odd k ≷ 0 ( e.g., (−1)!! = 1, (−3)!! = −1). • (j,k,ℓ )! def = (j +k +ℓ)!/ (j!k!ℓ!) (3-index multinomial coefficients). •B2m : Bernoulli numbers, B2m(·) : Bernoulli polynomials ( m = 0, 1, 2,... ). 1.1 The Keiper and Li coefficients In 1992 Keiper [19] considered a real sequence {λn} of generating function ϕ(z) def = log 2ξ(M(z)) ≡ ∞∑ n=1 λK n zn, M (z) def = 1 1 −z, (5) 3 (we write λK n for Keiper’sλn), deduced that λK n ≡n−1 ∑ ρ [1 − (1 − 1/ρ)n], (6) and that RH ⇒ λK n > 0 ( ∀n), then wrote (without proof n

=== Keiper @ 5396 ===
k − 2) · · ·1 for odd k >0, def = 2 (k+1)/2 Γ( 1 2k + 1)/√π for odd k ≷ 0 ( e.g., (−1)!! = 1, (−3)!! = −1). • (j,k,ℓ )! def = (j +k +ℓ)!/ (j!k!ℓ!) (3-index multinomial coefficients). •B2m : Bernoulli numbers, B2m(·) : Bernoulli polynomials ( m = 0, 1, 2,... ). 1.1 The Keiper and Li coefficients In 1992 Keiper [19] considered a real sequence {λn} of generating function ϕ(z) def = log 2ξ(M(z)) ≡ ∞∑ n=1 λK n zn, M (z) def = 1 1 −z, (5) 3 (we write λK n for Keiper’sλn), deduced that λK n ≡n−1 ∑ ρ [1 − (1 − 1/ρ)n], (6) and that RH ⇒ λK n > 0 ( ∀n), then wrote (without proof nor elaboration): “In fact, if we 

=== Keiper @ 5550 ===
x multinomial coefficients). •B2m : Bernoulli numbers, B2m(·) : Bernoulli polynomials ( m = 0, 1, 2,... ). 1.1 The Keiper and Li coefficients In 1992 Keiper [19] considered a real sequence {λn} of generating function ϕ(z) def = log 2ξ(M(z)) ≡ ∞∑ n=1 λK n zn, M (z) def = 1 1 −z, (5) 3 (we write λK n for Keiper’sλn), deduced that λK n ≡n−1 ∑ ρ [1 − (1 − 1/ρ)n], (6) and that RH ⇒ λK n > 0 ( ∀n), then wrote (without proof nor elaboration): “In fact, if we assume the Riemann hypothesis, and further that t he zeros are very evenly distributed, we can show that λm ≈ logm 2 − log(2π) + 1 −γ 2 . ” [for λK m ; m 

=== Keiper @ 6600 ===
 proved the sharp equivalence (Li’s criterion) : RH ⇐ ⇒ λL n ≥ 0 for all n. (11) He also obtained λL n ≡ ∑ ρ [1 − (1 − 1/ρ)n], which in view of (6) entails λL n ≡nλ K n for all n = 1, 2,... ; (12) our superscripts K vs L will disambiguate λn whenever the factor n matters. 1.2 Probing RH through the Keiper–Li constants λn Li’s criterion (11) makes it clear that the Keiper–Li sequence is RH-sensitive: how efficiently can it then serve to test RH? 4 Known results actually imply that, beyond the present frontier (1) , the sequence {λn} may effectively probe RH only in its tail n ≫ 1 and via its asymptotic 

=== Keiper @ 6667 ===
r all n. (11) He also obtained λL n ≡ ∑ ρ [1 − (1 − 1/ρ)n], which in view of (6) entails λL n ≡nλ K n for all n = 1, 2,... ; (12) our superscripts K vs L will disambiguate λn whenever the factor n matters. 1.2 Probing RH through the Keiper–Li constants λn Li’s criterion (11) makes it clear that the Keiper–Li sequence is RH-sensitive: how efficiently can it then serve to test RH? 4 Known results actually imply that, beyond the present frontier (1) , the sequence {λn} may effectively probe RH only in its tail n ≫ 1 and via its asymptotic form for n → ∞. In 2000 Oesterl´ e [26, prop. 2] proved (but left u

=== Keiper @ 7192 ===
ts asymptotic form for n → ∞. In 2000 Oesterl´ e [26, prop. 2] proved (but left unpublished [6, § 2.3]) that Re ρ = 1 2 for all zeros with | Im ρ| ≤ T0 =⇒ λn ≥ 0 for all n ≤T 2 0, (13) and that under RH, [26, § 2] λL n =n( 1 2 logn +c) +o(n)n→∞ with c = 1 2 (γ − log 2π − 1), (14) which concurs with Keiper’s formula (7) but now assuming RH alone . In 2004 Ma´ slanka [22][23] computed a few thousandλL n-values numerically and inferred asymptotic conjectures on them for the case RH tru e. In 2004–2006, inspired by the latter (but unaware of [26]), we used the saddle-point method to draw an asymptotic c

=== Keiper @ 9497 ===
necessitates n /greaterorsimilar2T 2 0, currently implying n /greaterorsimilar1025. (18) It is then no wonder that published λn-plots (having n ≲ 7000) solely reflect the RH-true pattern (16) (already from n ≈ 30) [19][22]. So, whether one would take (11) or (15)–(16) to track violations o f RH, the Keiper–Li sequence {λn} only matters in its asymptotic tail {n ≫ 1}, where the alternative (15)–(16) rules (and enacts Li’s sign proper ty as well). At the same time, theλn are quite elusive analytically [8][10]. Numerically too (see Ma´ slanka [22][23] and Coffey [9]), their evaluation requires arecursive

=== Keiper @ 10306 ===
lues up to n ≈ 4000 were accessed that way until recently, with n = 10 5 attained by Johansson [18, § 4.2] (who states a loss of 1 bit ≈ 0.3 decimal place per step n). Still, the range (18) needed for new tests of RH stays far out of reach . All that motivates quests for simpler realizations of the Keiper–Li idea. But first, as the asymptotic sensitivity to RH is the main property we will prove to generalize, we review that feature for {λn} itself. 1.3 Asymptotic analysis of {λn} (to be generalized) The following derivation of the large- n alternative (15)–(16) for λn readily settles the RH-false cas

=== Keiper @ 14608 ===
s. (3.721(1)), (4.421(1))]. So that all in all, λK n = 1 2 logn +c +o(1), c = 1 2 (γ − log 2π − 1) (under RH true) , (24) amounting to (14). □ 2 An explicit variant to the sequence {λK n } To alleviate the difficulties met with the original sequence {λn} (§ 1.2), we propose to deform it (specifically, Keiper’s form (5)) into a simpler one, still RH-sensitive but of elementary closed form . While the original specification (5) for λn looks rigid, this is only due to an extraneous assumption implied on the mapping M: that the origin z = 0 has to map to x = 1 (the pole of ζ). Indeed, (5) at once built {λn}

=== Keiper @ 19856 ===
n = 1, 2,..., (36) 11 and the latter form is fully explicit : Anm are given by (32), and 2ξ(2m) = (−1)m+1B2m (2m − 3)!! (2π)m ≡ 2(−1)m+1B2m Γ(m − 1 2) πm+1/2, m = 0, 1,... (37) E.g., Λ 1 = 3 2 logπ 3, Λ 2 = 5 24 log [( 2 5 ) 7 311 π4 ] , Λ 3 = 21 80 log [ 525π8 23(32 · 7)11 ] . (38) So, we deformed Keiper’s {λK n } by discretizing the derivatives on log 2 ξ to finite differences anchored at locations 1, {2m} whereξ has known values, in a canonical way basically dictated by the preservation of RH-sensitivity .2 This gave {Λ n} the elementary closed form (36), which is moreover directly computable at an

=== Keiper @ 24143 ===
); hence this integral tends to 0 if R → ∞ while keeping far enough from ordinates of Riemann zeros in a classic fashion (i.e., so that ⏐ ⏐ ⏐1 ζ dζ dx ⏐ ⏐ ⏐(r + iR)<K log2R for all r ∈ [−1, +2], cf. [11, p. 108]), hence (44) results. □ 14 3 Resulting new sequential criterion for RH Like the elusive Keiper–Li sequence, the fully explicit one {Λ n} proves RH- sensitive (just slightly differently). The argument will use the funct ion Φ(X) def = X log ( 1 − 1 X 2 ) + logX + 1 X − 1 ≡ ∫ X ∞ log ( 1 − 1 Y 2 ) dY (46) ≡ (X + 1) log(X + 1) + (X − 1) log(X − 1) − 2X logX (47) made single-valued on C \ [−1, 1]

=== Keiper @ 38460 ===
values for Lχ (and ξχ) at all even, resp. odd, positive integers ac- cording to the even, resp. odd parity of χ. Moreover, Lχ(1) (hence ξχ(1)) is explicitly computable also for even parity [11, chap. 1][34, eq.(10.70)]. 22 • Generalized Riemann Hypothesis (GRH): all zerosρ ofξχ have Re ρ = 1 2. • A Keiper–Li sequence {λχ,n} exists for ξχ in full similarity to {λn} for ξ (applying [8, Cor. 1]). For GRH, the only change in our asymptotic alte rna- tive (15)–(16) affects the constant c in (16) or (24) due to the replacement, in the asymptotic counting function N (T ) from (3) used in § 1.3.2, of the ter

{
  "file_path": "D:\\Python\\Quantum\\research\\derivations\\D-050-T2-tail-estimate.md",
  "content": "# D-050 \u2014 T2 write-up: the finite-height tail, the phase threshold, and what positivity costs\nDate: 2026-08-19 | Session: 008 | Task: T2 (D-049 finite-height tail)\nStatus: complete (analysis). Conclusion: the valley theorem's LOWER\nbounds are unconditional (direct estimates); the UPPER bounds at\nfinite height are exactly Weil-positivity-at-a statements (not provable\nfrom RH-to-T\u2080 alone; measured). Under full RH: everything clean\n(D-049 as written).\n\n## 1. The pair-term phase analysis (the clean core result)\nFor an off-line zero pair \u03c1 = \u03b2+i\u03b3, 1\u2212\u03c1\u0304 (\u03b4 := \u03b2\u2212\u00bd \u2208 (0,\u00bd)), the\ncontribution to Q_W^a(v) is\n  2 m_\u03c1 Re[ v\u0302(\u03b3\u2212i\u03b4)\u00b7conj(v\u0302(\u03b3+i\u03b4)) ].\nFor v supported in (\u2212a,a), write v(x) = e^{-i\u03b3x}u(x): the pair term is\n2m_\u03c1 Re[\u00fb(i\u03b4-ish)\u00b7conj(\u00fb(\u2212i\u03b4-ish))] \u2014 a product of two Laplace-type\ntransforms whose relative phase is \u2248 2\u03b4\u00b7\u27e8x\u27e9_u (first moment of the\nprofile). The pair term is NEGATIVE only if the relative phase can\nreach \u03c0/2, i.e. only if\n  **\u03b4 \u2273 \u03c0/(2a)**  (achievable profile offsets \u27e8x\u27e9 \u2208 (\u2212a,a)).\nHence: **zeros off the line by less than \u03c0/(2a) cannot produce\nnegative form directions at scale a.** This is the quantitative\ncontent of \"finite resolution\": the scale-a operator is blind to\ndeviations below \u03c0/(2a).\n\n## 2. High-frequency directions cannot corrupt low-z observables\nFor the variational quotient q_z(v) = |v\u0302(z)|\u00b2/(\u2016v\u2016\u00b2 + Q(v)), |z| \u2264 Z:\na direction v whose v\u0302-mass sits at height \u03b3\u2080 \u226b T\u2080 has\n|v\u0302(z)|\u00b2 \u2264 4a\u00b2/(\u03b3\u2080\u2212z)\u00b2\u00b7(per-unit) \u2014 so\n  q_z(v) \u2264 2a/(\u03b3\u2080\u2212z)\u00b2\u00b7\u03b7\u207b\u00b9 \u226a 2a\nwhenever the denominator stays above \u03b7\u2016v\u2016\u00b2; and a denominator\ncrossing zero makes q_z NEGATIVE (irrelevant for the sup). A mixed\ndirection v = \u03b1v_hi + \u03b2v_lo has quotient denominator minimizing only\nthrough t = \u03b1/\u03b2 = 0 unless the form's negative content reaches the\nthreshold c\u2080 = 1/(2a) (\u00a73). Hence: **the upper-bound observables\nK(z,z) for z \u2264 Z are sensitive only to the form's negativity at level\n\u2265 1/(2a)** \u2014 small negativity, if any, moves nothing at our digits.\n\n## 3. What the upper bounds cost (the honest inventory)\n- B2's K(z,z) \u2264 2a and B1's K(\u03b3,\u03b3) \u2264 1 require T_a \u2265 (1\u2212\u03b5)I with\n  \u03b5 < 1/(2a): i.e. **Weil positivity of the interval form at level\n  1/(2a)**. Under RH: free (Yoshida). Under RH-to-T\u2080 alone: NOT\n  provable \u2014 an off-line pair above T\u2080 with \u03b4 > \u03c0/(2a) and the wrong\n  phase could defeat it (\u00a71), and nothing known rules that out.\n- It IS measured: \u03bb_a > 0 (E-009b\u2026E-025, floor-caveated) and the\n  valleys themselves (their existence at depth \u2248 1 IS the positivity\n  signature at the \u03b3-frequencies). So the measured valley picture is\n  evidence of Weil positivity at scale a \u2264 12 \u2014 the detector remark\n  (D-048 \u00a76) made quantitative: **an off-line pair at height \u03b3 with\n  \u03b4 > \u03c0/(2a) would flatten/invert the valley at \u03b3 by a computable\n  amount.**\n- The LOWER bounds (B1: K(\u03b3,\u03b3) \u2265 1 \u2212 1/(2a) \u2212 \u2026; B2: K \u2265 2a(1\u2212C'/a);\n  B3: the profile envelope) are UNCONDITIONAL given RH-to-T\u2080: they use\n  only the bump test functions, whose tails are directly summable\n  (|v\u0302\u2080(\u03b3+i\u03c3)| \u2264 2a e^{a\u03c3}/|\u03b3\u2212z|; \u03a3_{\u03b3>T\u2080} \u2264 4a\u00b2e^a\u00b74C\u2080(T\u2080)/T\u2080 \u2248\n  3\u00d710\u207b\u2077 at a=12 \u2014 Lemma T-bump, PROVED).\n\n## 4. Final status of the valley theorem\n| statement | full RH | RH-to-T\u2080 |\n|---|---|---|\n| floor lower bound (valleys at least 1\u22121/(2a) deep) | \u2713 | \u2713 (Lemma T-bump) |\n| floor upper bound K(\u03b3,\u03b3) \u2264 1 | \u2713 | \u27fa positivity at level 1/(2a) \u2014 measured |\n| plateau K = 2a(1\u00b1o(1)) | \u2713 | lower \u2713; upper = positivity |\n| profile envelope | \u2713 | \u2713 |\n| \u0394 = log 2a law | \u2713 | modulo positivity |\nThe detector consequence: our measured K-profiles (valleys at the true\n\u03b3's with floors \u2248 1 and plateau \u2192 2a, a \u2264 12) constitute a numerical\nverification of Weil positivity in the \u210b(T_a) metric to scale 12 \u2014\nindependent of and consistent with the \u03bb_a cliff measurements.\n"
}

{
  "type": "create",
  "filePath": "D:\\Python\\Quantum\\research\\derivations\\D-050-T2-tail-estimate.md",
  "content": "# D-050 \u2014 T2 write-up: the finite-height tail, the phase threshold, and what positivity costs\nDate: 2026-08-19 | Session: 008 | Task: T2 (D-049 finite-height tail)\nStatus: complete (analysis). Conclusion: the valley theorem's LOWER\nbounds are unconditional (direct estimates); the UPPER bounds at\nfinite height are exactly Weil-positivity-at-a statements (not provable\nfrom RH-to-T\u2080 alone; measured). Under full RH: everything clean\n(D-049 as written).\n\n## 1. The pair-term phase analysis (the clean core result)\nFor an off-line zero pair \u03c1 = \u03b2+i\u03b3, 1\u2212\u03c1\u0304 (\u03b4 := \u03b2\u2212\u00bd \u2208 (0,\u00bd)), the\ncontribution to Q_W^a(v) is\n  2 m_\u03c1 Re[ v\u0302(\u03b3\u2212i\u03b4)\u00b7conj(v\u0302(\u03b3+i\u03b4)) ].\nFor v supported in (\u2212a,a), write v(x) = e^{-i\u03b3x}u(x): the pair term is\n2m_\u03c1 Re[\u00fb(i\u03b4-ish)\u00b7conj(\u00fb(\u2212i\u03b4-ish))] \u2014 a product of two Laplace-type\ntransforms whose relative phase is \u2248 2\u03b4\u00b7\u27e8x\u27e9_u (first moment of the\nprofile). The pair term is NEGATIVE only if the relative phase can\nreach \u03c0/2, i.e. only if\n  **\u03b4 \u2273 \u03c0/(2a)**  (achievable profile offsets \u27e8x\u27e9 \u2208 (\u2212a,a)).\nHence: **zeros off the line by less than \u03c0/(2a) cannot produce\nnegative form directions at scale a.** This is the quantitative\ncontent of \"finite resolution\": the scale-a operator is blind to\ndeviations below \u03c0/(2a).\n\n## 2. High-frequency directions cannot corrupt low-z observables\nFor the variational quotient q_z(v) = |v\u0302(z)|\u00b2/(\u2016v\u2016\u00b2 + Q(v)), |z| \u2264 Z:\na direction v whose v\u0302-mass sits at height \u03b3\u2080 \u226b T\u2080 has\n|v\u0302(z)|\u00b2 \u2264 4a\u00b2/(\u03b3\u2080\u2212z)\u00b2\u00b7(per-unit) \u2014 so\n  q_z(v) \u2264 2a/(\u03b3\u2080\u2212z)\u00b2\u00b7\u03b7\u207b\u00b9 \u226a 2a\nwhenever the denominator stays above \u03b7\u2016v\u2016\u00b2; and a denominator\ncrossing zero makes q_z NEGATIVE (irrelevant for the sup). A mixed\ndirection v = \u03b1v_hi + \u03b2v_lo has quotient denominator minimizing only\nthrough t = \u03b1/\u03b2 = 0 unless the form's negative content reaches the\nthreshold c\u2080 = 1/(2a) (\u00a73). Hence: **the upper-bound observables\nK(z,z) for z \u2264 Z are sensitive only to the form's negativity at level\n\u2265 1/(2a)** \u2014 small negativity, if any, moves nothing at our digits.\n\n## 3. What the upper bounds cost (the honest inventory)\n- B2's K(z,z) \u2264 2a and B1's K(\u03b3,\u03b3) \u2264 1 require T_a \u2265 (1\u2212\u03b5)I with\n  \u03b5 < 1/(2a): i.e. **Weil positivity of the interval form at level\n  1/(2a)**. Under RH: free (Yoshida). Under RH-to-T\u2080 alone: NOT\n  provable \u2014 an off-line pair above T\u2080 with \u03b4 > \u03c0/(2a) and the wrong\n  phase could defeat it (\u00a71), and nothing known rules that out.\n- It IS measured: \u03bb_a > 0 (E-009b\u2026E-025, floor-caveated) and the\n  valleys themselves (their existence at depth \u2248 1 IS the positivity\n  signature at the \u03b3-frequencies). So the measured valley picture is\n  evidence of Weil positivity at scale a \u2264 12 \u2014 the detector remark\n  (D-048 \u00a76) made quantitative: **an off-line pair at height \u03b3 with\n  \u03b4 > \u03c0/(2a) would flatten/invert the valley at \u03b3 by a computable\n  amount.**\n- The LOWER bounds (B1: K(\u03b3,\u03b3) \u2265 1 \u2212 1/(2a) \u2212 \u2026; B2: K \u2265 2a(1\u2212C'/a);\n  B3: the profile envelope) are UNCONDITIONAL given RH-to-T\u2080: they use\n  only the bump test functions, whose tails are directly summable\n  (|v\u0302\u2080(\u03b3+i\u03c3)| \u2264 2a e^{a\u03c3}/|\u03b3\u2212z|; \u03a3_{\u03b3>T\u2080} \u2264 4a\u00b2e^a\u00b74C\u2080(T\u2080)/T\u2080 \u2248\n  3\u00d710\u207b\u2077 at a=12 \u2014 Lemma T-bump, PROVED).\n\n## 4. Final status of the valley theorem\n| statement | full RH | RH-to-T\u2080 |\n|---|---|---|\n| floor lower bound (valleys at least 1\u22121/(2a) deep) | \u2713 | \u2713 (Lemma T-bump) |\n| floor upper bound K(\u03b3,\u03b3) \u2264 1 | \u2713 | \u27fa positivity at level 1/(2a) \u2014 measured |\n| plateau K = 2a(1\u00b1o(1)) | \u2713 | lower \u2713; upper = positivity |\n| profile envelope | \u2713 | \u2713 |\n| \u0394 = log 2a law | \u2713 | modulo positivity |\nThe detector consequence: our measured K-profiles (valleys at the true\n\u03b3's with floors \u2248 1 and plateau \u2192 2a, a \u2264 12) constitute a numerical\nverification of Weil positivity in the \u210b(T_a) metric to scale 12 \u2014\nindependent of and consistent with the \u03bb_a cliff measurements.\n",
  "structuredPatch": [],
  "originalFile": null
}

{
  "file_path": "D:\\Python\\Quantum\\research\\paper\\draft.tex",
  "old_string": "On the operator-theoretic side (D-041): the limit operator $D$ exists\nunconditionally as a $J$-self-adjoint operator in a Krein space\n(negative index = number of off-line zero pairs, Bombieri), with\n$\\mathrm{spec}(D) = \\Gamma$; and deficiency-element convergence is\nequivalent to strong resolvent convergence\n$\\bar D_{a,\\theta(a)} \\to D$ (Theorem D1), giving the reduction:\nthe limit formula (1.12) holds for some $\\theta(a), \\phi$ if and only\nif $\\mathrm{spec}(D) \\subset \\mathbb R$. The real-spectrum persistence\nstep is exactly RH (the paywall), as expected.",
  "new_string": "On the operator-theoretic side (D-041): the limit operator $D$ exists\nunconditionally as a $J$-self-adjoint operator in a Krein space\n(negative index = number of off-line zero pairs, Bombieri), with\n$\\mathrm{spec}(D) = \\Gamma$; and deficiency-element convergence is\nequivalent to strong resolvent convergence\n$\\bar D_{a,\\theta(a)} \\to D$ (Theorem D1), giving the reduction:\nthe limit formula (1.12) holds for some $\\theta(a), \\phi$ if and only\nif $\\mathrm{spec}(D) \\subset \\mathbb R$. The real-spectrum persistence\nstep is exactly RH (the paywall), as expected.\n\n\\subsection{The valley theorem (D-048--D-050)}\n\nThe spectral-measure picture above rests on a theorem about the\nreproducing-kernel diagonal $K_a(z,z) = \\langle e_z, T_a^{-1}e_z\\rangle$\nof the model spaces $\\mathcal H(T_a)$.\n\n\\begin{theorem}[valley law; conditional on RH]\nAssume RH. For $a \\ge 1$, $z \\in \\mathbb R$:\n\\begin{enumerate}\n\\item \\emph{(plateau)} $K_a(z,z) \\le 2a$ exactly, and\n$K_a(z,z) \\ge 2a(1 - C'(z,\\delta)/a)$ for\n$\\mathrm{dist}(z,\\Gamma) \\ge \\delta$, with explicit $C'$;\n\\item \\emph{(floors)} at each zero $\\gamma$ with gap $g_\\gamma \\ge 4/a$,\n\\[\n1 - \\tfrac{1}{2a} - C\\tfrac{1+\\log\\gamma}{a^2}\n\\;\\le\\; K_a(\\gamma,\\gamma) \\;\\le\\; 1;\n\\]\n\\item \\emph{(profile)} near a zero, $K_a$ has the universal lower\nenvelope $1/(\\mathrm{sinc}^2((z-\\gamma)a/2) + 1/(2a))$.\n\\end{enumerate}\nIn particular the valley depth $\\Delta(a) = \\log 2a + o(1)$.\n\\end{theorem}\n\n\\begin{proof}[Proof idea (D-049)]\nThe variational identity\n$K_a(z,z) = \\sup_v |\\hat v(z)|^2/(\\|v\\|^2 + Q_W^a(v))$ with the Weil\nexplicit formula $Q_W^a(v) = \\sum_\\gamma m_\\gamma|\\hat v(\\gamma)|^2$\n(the pure comb under RH). Plateau upper bound: $T_a \\ge I$. Floor:\nsingle-term domination above, bump test function below. The\ncombinatorial input is Trudgian's zero-density bound.\n\\end{proof}\n\n\\begin{remark}[the detector content; D-050]\nAn off-line zero pair at height $\\gamma$ with deviation\n$\\delta = \\beta - \\tfrac12$ produces negative form directions if and\nonly if $\\delta > \\pi/(2a)$ (exact computation). Hence the measured\nvalley picture (floors $\\approx 1$ at the true ordinates, plateau\n$\\to 2a$) is a numerical verification of Weil positivity in the\n$\\mathcal H(T_a)$ metric to scale $a = 12$, and the valley profile is\nin principle a detector of off-line zeros with\n$\\delta > \\pi/(2a)$ at computable positions.\n\\end{remark}"
}

{
  "filePath": "D:\\Python\\Quantum\\research\\lean\\NguyenRH1\\NguyenRH1\\LiClosed.lean",
  "oldString": "LiClosed.lean \u2014 tier ii\u2032-7: THE CLOSED finite-height Li theorem (R-004\nendpoint, D-062 \u00a74). `lambda_pos_finite_height_closed`: \u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 from the EIGHT declared hypotheses:\nthe two computational certificates (Platt\u2013Trudgian `RHUpTo`, the finite\nLi verification `LiVerifiedUpTo`) and the six analytic perimeter Props\n(Trudgian N(T)/S(T): `ZeroCountProp` unit-window, `ZeroCountProp2`\ntwo-unit, `ZeroCountGlobalProp` global; the Platt-class zero-location\ncertificate `NoLowZeros`; the M\u2080 interval certificate `MZeroProp`) \u2014\nthe session-012 named analytic hypothesis `SfBoundProp` is now PROVED\n(tier ii\u2032-6, LiSideBounds).\n-/",
  "newString": "LiClosed.lean \u2014 tier ii\u2032-7: THE CLOSED finite-height Li theorem (R-004\nendpoint, D-062 \u00a74). `lambda_pos_finite_height_closed`: \u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 from the SEVEN declared hypotheses:\nthe two computational certificates (Platt\u2013Trudgian `RHUpTo`; the finite\nLi verification `LiVerifiedUpTo` \u2014 E-011/E-015 to 3000 + Johansson 2015\n\u00a7 4.2 to 10\u2075) and the five analytic perimeter Props (Trudgian N(T)/S(T):\n`ZeroCountProp` unit-window, `ZeroCountProp2` two-unit,\n`ZeroCountGlobalProp` global; the Platt-class zero-location certificate\n`NoLowZeros`; the M\u2080 interval certificate `MZeroProp`) \u2014 the session-012\nnamed analytic hypothesis `SfBoundProp` is now PROVED (tier ii\u2032-6,\nLiSideBounds).\n-/",
  "originalFile": "/-\nLiClosed.lean \u2014 tier ii\u2032-7: THE CLOSED finite-height Li theorem (R-004\nendpoint, D-062 \u00a74). `lambda_pos_finite_height_closed`: \u03bb_n > 0 for all\n1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 from the EIGHT declared hypotheses:\nthe two computational certificates (Platt\u2013Trudgian `RHUpTo`, the finite\nLi verification `LiVerifiedUpTo`) and the six analytic perimeter Props\n(Trudgian N(T)/S(T): `ZeroCountProp` unit-window, `ZeroCountProp2`\ntwo-unit, `ZeroCountGlobalProp` global; the Platt-class zero-location\ncertificate `NoLowZeros`; the M\u2080 interval certificate `MZeroProp`) \u2014\nthe session-012 named analytic hypothesis `SfBoundProp` is now PROVED\n(tier ii\u2032-6, LiSideBounds).\n-/\nimport Mathlib\nimport NguyenRH1.LiBasePoints\nimport NguyenRH1.LiSideBounds\n\nopen Zeta23 Complex Filter Topology\n\nnamespace NguyenRH1\n\n/-- **THE CLOSED FINITE-HEIGHT LI THEOREM** (R-004, ii\u2032-7 endpoint):\n\u03bb_n > 0 for ALL 1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074, from the eight\ndeclared hypotheses (two computational certificates + six analytic\nperimeter Props). The session-012 named analytic hypothesis\n`SfBoundProp` is discharged by ii\u2032-6's `sfBoundProp`. -/\ntheorem lambda_pos_finite_height_closed\n    (hRH : RHUpTo (3 * 10 ^ 12)) (hfinite : LiVerifiedUpTo (10 ^ 5))\n    (hZC : ZeroCountProp) (hZC2 : ZeroCountProp2) (hZCG : ZeroCountGlobalProp)\n    (hNLZ : NoLowZeros) (hMZ : MZeroProp) :\n    \u2200 n : \u2115, 1 \u2264 n \u2192 (n : \u211d) \u2264 (3 * 10 ^ 12 - 1 : \u211d) ^ 2 \u2192\n      0 < (liCoeff n).re :=\n  lambda_pos_finite_height_verified hRH hfinite\n    (sfBoundProp hRH hZC hZC2 hZCG hNLZ hMZ)\n\nend NguyenRH1\n",
  "structuredPatch": [
    {
      "oldStart": 1,
      "oldLines": 14,
      "newStart": 1,
      "newLines": 15,
      "lines": [
        " /-",
        " LiClosed.lean \u2014 tier ii\u2032-7: THE CLOSED finite-height Li theorem (R-004",
        " endpoint, D-062 \u00a74). `lambda_pos_finite_height_closed`: \u03bb_n > 0 for all",
        "-1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 from the EIGHT declared hypotheses:",
        "-the two computational certificates (Platt\u2013Trudgian `RHUpTo`, the finite",
        "-Li verification `LiVerifiedUpTo`) and the six analytic perimeter Props",
        "-(Trudgian N(T)/S(T): `ZeroCountProp` unit-window, `ZeroCountProp2`",
        "-two-unit, `ZeroCountGlobalProp` global; the Platt-class zero-location",
        "-certificate `NoLowZeros`; the M\u2080 interval certificate `MZeroProp`) \u2014",
        "-the session-012 named analytic hypothesis `SfBoundProp` is now PROVED",
        "-(tier ii\u2032-6, LiSideBounds).",
        "+1 \u2264 n \u2264 N\u2081 = (3\u00d710\u00b9\u00b2\u22121)\u00b2 \u2248 9\u00d710\u00b2\u2074 from the SEVEN declared hypotheses:",
        "+the two computational certificates (Platt\u2013Trudgian `RHUpTo`; the finite",
        "+Li verification `LiVerifiedUpTo` \u2014 E-011/E-015 to 3000 + Johansson 2015",
        "+\u00a7 4.2 to 10\u2075) and the five analytic perimeter Props (Trudgian N(T)/S(T):",
        "+`ZeroCountProp` unit-window, `ZeroCountProp2` two-unit,",
        "+`ZeroCountGlobalProp` global; the Platt-class zero-location certificate",
        "+`NoLowZeros`; the M\u2080 interval certificate `MZeroProp`) \u2014 the session-012",
        "+named analytic hypothesis `SfBoundProp` is now PROVED (tier ii\u2032-6,",
        "+LiSideBounds).",
        " -/",
        " import Mathlib",
        " import NguyenRH1.LiBasePoints"
      ]
    }
  ],
  "userModified": false,
  "replaceAll": false
}

{
  "todos": [
    {
      "content": "4.A: synthesis + best theorems (D-052)",
      "status": "in_progress",
      "activeForm": "Writing the synthesis"
    },
    {
      "content": "4.B: Davenport\u2013Heilbronn/Epstein sanity gate (D-053)",
      "status": "pending",
      "activeForm": "Running the sanity gate"
    },
    {
      "content": "4.C: numerical stress test (E-027 blind zero detection)",
      "status": "pending",
      "activeForm": "Running E-027 stress test"
    },
    {
      "content": "4.D: error-hunt pass (D-054) + archive updates + commit",
      "status": "pending",
      "activeForm": "Running the error-hunt pass"
    }
  ]
}

{
  "oldTodos": [
    "content='Fork 1: symbol identification analysis (D-045)' status='completed' active_form='Running Fork 1 symbol analysis'",
    "content='Fork 2: spectral-Galerkin sizing study (D-046)' status='completed' active_form='Running Fork 2 sizing study'",
    "content='Joint evaluation of both forks with user' status='in_progress' active_form='Evaluating forks jointly'"
  ],
  "newTodos": [
    "content='4.A: synthesis + best theorems (D-052)' status='in_progress' active_form='Writing the synthesis'",
    "content='4.B: Davenport\u2013Heilbronn/Epstein sanity gate (D-053)' status='pending' active_form='Running the sanity gate'",
    "content='4.C: numerical stress test (E-027 blind zero detection)' status='pending' active_form='Running E-027 stress test'",
    "content='4.D: error-hunt pass (D-054) + archive updates + commit' status='pending' active_form='Running the error-hunt pass'"
  ],
  "cleared": false
}