# Verification report: AIM-ANALYSIS-0138 Author: Alper Ferudun, Mercury Software GmbH. Date: 28 September 2026. Result: complete proofs of the explicit BMV zero-location theorems. Basis: originating-researcher self-audit; not independent peer review or proof-assistant verification. ## Scope For strictly positive-definite Hermitian matrices A,B and positive integer m, the paper treats Tr((A+zB)^m), with matrix power before trace. It proves a sharp universal region under lB<=A<=uB in every finite dimension, boundary commutation rigidity and an optimal uniform Hurwitz threshold. In dimension two it proves an exact factorization, simplicity for nonproportional pairs, a trace-ratio stability criterion, and precise half-plane counts. Real roots are classified in all dimensions. The region is a UNION of two disks, not an intersection. Its universal quantifier lets the pair depend on the proposed zero. Prescribed Loewner bounds need not be exact extrema for every interior witness. The threshold sharpness construction does attain the prescribed extrema. Congruence is not substituted for similarity of trace powers. The trace-ratio criterion is not valid verbatim in dimensions three and above. The AIM question is open-ended: theorem scope is resolved, but the entire source programme is not declared closed. This is not a new proof of the BMV coefficient-positivity theorem and not a singular-matrix extension. ## Exact and floating diagnostics The standard-library checker performs 1580 exact finite diagnostics: - 486 comparisons between cyclotomic factorization and direct matrix powers. - 450 rational polynomial gcd/squarefreeness tests. - 640 odd-derivative, positivity and equality tests. - Four explicit boundary, Routh and invalid-generalization examples. The isolated Python 3.9 and 3.13 reports match byte for byte. Assertions remain enabled. These tests do not constitute formal verification of the universal statements; the written proofs are the basis for those claims. The separate NumPy experiment checks 3168 roots in dimensions 2-7, 544 dimension-two half-plane counts, 1015 constructive witnesses, 23 boundary witnesses and 84 threshold cases. Floating checks are noncertifying and are not proof dependencies. Seed, tolerances and residuals are preserved in its report. ## Corrections recorded before publication The first exact checker incorrectly demanded strict positivity of an odd derivative even when a sampled pair was proportional and A+xB=0. The proof already covered this case. The checker was corrected, and the three observed zero-derivative exceptions are recorded, not discarded. During manuscript preparation, a sentence after the exact root-count formula was corrected: an imaginary pair arising at a later factor may coexist with right-half-plane pairs from earlier factors. Only at the first-factor stability threshold are all remaining pairs left-half-plane pairs. The root-count formula and its proof were unchanged. For m=9, r=2+sqrt(3), A=diag(1,r), B=diag(r,1), one has q=1/3, with the j=0 pair on the right, j=1 imaginary, and j=2,3 on the left. The pre-publication originals and the revision acceptance receipt are retained for provenance. ## Manuscript and package checks Seven pages. The native LaTeX compiler and Tectonic export succeeded. All seven rendered final pages were visually inspected. The final TeX log has no overfull/underfull boxes, missing characters, unresolved references or LaTeX warnings. Only the author's name appears in the author line; company/contact details are in the footnote. AI assistance is disclosed in ordinary prose, not under a separate heading. The release build receipt binds the reviewed PDF, isolated diagnostics and source archive. The ZIP includes original source and verification materials, not third-party source PDFs/HTML or account information. ## Prior art and limitations Classical Schur, power-sum and quadratic-stability methods are credited. The inherited commuting example is not advertised as newly discovered. A bounded primary-source search did not locate the combined formulation; folklore and unlocated prior art are not excluded. No absolute-priority, endorsement, formal-verification or peer-review claim is made. A DOI does not certify mathematical correctness.