Unit-circle nonvanishing for rational Hartogs-triangle polynomials

For every coprime pair m>n>=1, the polynomial in Edholm–Mathew Conjecture 4.20 has no root on the unit circle and exactly m-n roots in the punctured unit disc, counted with multiplicity. A finite coefficient reindexing gives a sum of squared floor-polynomial values, and an adjacent-polynomial difference makes it strictly positive. The source coefficient bridge and full polynomial theorem are proved in Lean; older kernel identities are credited. AI-assisted preprint by Myeongjin Kang, with no affiliation. Internal AI review is not external journal peer review. The accompanying Lean certificate covers the precise scoped main statement; inspect the formal endpoint, assumptions and provenance in the supporting package. Prior-art investigations are documented bounded searches, not worldwide-priority certification. Original prose is offered under CC BY 4.0 and original code/Lean under MIT; third-party rights and existing notices are preserved. The public supporting ZIP contains original proof sources and verification evidence, with bibliographic links and hashes instead of redistributed third-party source manuscripts. Recorded prior-art/source-access limits: Actual full June2026 target and published Almughrabi2023 body read. Older weighted roots-of-unity identity explicitly credited; no previous full strict boundary conclusion found. Source-mentioned in-preparation successor not located/read; unpublished or absolute worldwide priority not certified.