A Two-Thirds Hyperbolicity Wedge for Jensen Polynomials of Riemann's Xi-Function

Version 1.1 of a proof candidate establishing an absolute constant K > 0 such that n² log(n+2) ≥ Kd³ implies that the degree-d Jensen polynomial based at n for Riemann's xi-function has exactly d distinct negative real zeros. The argument combines sectorial saddle-point asymptotics, a six-match Jacobi finite-free-convolution model, complex Hermite–Genocchi interpolation, and a non-perturbative sign-transfer argument. The accompanying public repository provides Lean 4 source, exact calculations, theorem-to-evidence maps, and reproducibility records. The headline Lean theorem retains explicitly typed Jacobi, Martínez-Finkelshtein–Morales–Perales, and Marcus–Spielman–Srivastava literature inputs. This result does not prove the Riemann hypothesis and does not locate zeros of the zeta function. The papers and Lean formalization were developed with substantial artificial-intelligence assistance, primarily from OpenAI GPT-5.6 Sol Pro; additional models assisted with adversarial testing and AI-only technical review. Wolfram Mathematica 15.0.1, executed by the author, supplied clean-room computational corroboration of selected symbolic identities and exact algebraic calculations. AI systems are not authors. No human mathematical review or peer review is claimed. Version 1.1 is an attribution-only revision of Version 1.0; the mathematical content and frozen Version 1.0 reviewer evidence are unchanged.