{
  "file_path": "D:\\Python\\Quantum\\research\\numerics\\scripts\\E-027-detector.py",
  "limit": 8,
  "offset": 70
}

{
  "type": "text",
  "file": {
    "filePath": "D:\\Python\\Quantum\\research\\paper\\draft.tex",
    "content": "\\section{Formal verification}\n\nThe inherited density theorem \\cite{anthropic2026riemann} is formally\nverified in Lean~4 (repository \\texttt{zeta-23-lean}, tag v1.0); this\nproject performed a full \\texttt{lake} rebuild (9010 jobs) and a live\n\\texttt{\\#print axioms} audit of all comparator statements, confirming\nthe published axiom profile verbatim: no axioms beyond \\texttt{propext},\n\\texttt{Classical.choice}, and \\texttt{Quot.sound}, with \\texttt{sorry}\noccurring only in the trusted challenge-statement stubs.\n\nThe new results of this paper are being formalized in the companion\npackage \\texttt{NguyenRH1} (same toolchain, path-linked to the vendored\n\\texttt{zeta-23-lean} and its \\textsc{Mathlib} build; no new axioms are\nintroduced anywhere). The first tier is complete: the archimedean lower\nbound for $S_\\infty(n)$ and the margin convexity are now machine-proved\n(\\texttt{sInfty\\_lower\\_bound}, \\texttt{marginTilde\\_convex}, and the\nchain-rule identity \\texttt{chain\\_rule\\_sqrt\\_shift}), each with axiom\nprofile exactly the three standard axioms above. A design note on the\nconvexity proof: the pen-and-paper argument uses eleven one-variable\nsign conditions, but the Lean development proves an eight-block\n$\\psi$-table plus a separate analytic bound for the $I_I$ term\n($\\widetilde B_4$); the divergence from the eleven-row table is that\n$\\widetilde B_4$ is not concave, so it is excluded from the $\\psi$\nmachinery and bounded directly. That direct bound is itself a worked\nexample of this project's measured-to-traced conversion: the grid\ncheck of E-029 (maximum $2n\\,|\\widetilde B_4''(n)| = 0.189$ on\n$[20, 10^4]$, with the decay argument covering the tail) is superseded\nby a fully analytic factor-monotonicity proof of the sufficient\ninequality $\\widetilde\\psi''(s) - \\widetilde\\psi'(s)/s \\le 1.316 < 2$\nfor $s \\ge \\sqrt{20}$, i.e.\\ $\\widetilde B_4''(n) < 1/(2n)$ for all\n$n \\ge 20$ (\\texttt{iimaj\\_bracket\\_bound},\n\\texttt{IIMaj\\_deriv2\\_lt}).\n\nThe remaining tiers, in order of increasing formalization cost:\n(ii) the traced contour bound for $|S_f(n)|$ (requires explicit $N(T)$,\n$S(T)$, and partial-fraction bounds for $\\zeta'/\\zeta$ --- a nontrivial\nbut finite library task); (iii) the valley theorem (requires a formal\nmodel-space/reproducing-kernel infrastructure that does not currently\nexist in \\textsc{Mathlib}); (iv) the Wiener--Hopf reduction\n(Section~3.2), whose remaining steps are open mathematics rather than\nformalization work. The finite-height Li theorem is, by design,\n\\emph{conditional} on computations (Platt--Trudgian's interval\narithmetic; the Li-coefficient verifications); formalizing the\n\\emph{reduction} would leave exactly those computational certificates\nas trusted inputs, which we regard as the honest formal target.\n\n\\bibliographystyle{plain}\n\\bibliography{references}\n\\end{document}",
    "numLines": 49,
    "startLine": 509,
    "totalLines": 557
  }
}