Structure of the Chiral Anomaly in the Real-Time Henstock–Kurzweil Framework: Exact Ward Identity and Regulator Universality

A structural analysis of the ABJ chiral anomaly in real (Minkowski) time within the Henstock–Kurzweil (HK) framework. The entire α-dependence of the truncated fermionic partition function is shown to be localised in a single factor exp(2iα tr_M γ₅), which is exactly 1 at every finite mode level; the universal regulator factor arising when the truncation is removed equals 1 for every admissible profile. The geometric coefficient c_d(A) (the Seeley–DeWitt coefficient) enters through an explicit hypothesis and is not derived. The construction is carried out with no Wick rotation, as a Berezin integral over the truncated Grassmann algebra of the modes of a finite mode lattice. Four statements are proved in full and machine-checked in Lean 4 without `sorry`, without `admit` and without new axioms: (A) the truncated real-time Berezin partition function is well defined, equals the determinant of the truncated Dirac operator up to the real-time phase iN_M, is holomorphic in the retained modes of the background field and obeys an explicit modulus bound; (B) the chiral transformation acts on the truncated Grassmann algebra as an invertible linear map whose Jacobian is exp(2iα tr_M γ₅), and tr_M γ₅ = 0 exactly at every finite truncation level, so the Jacobian is exactly 1; (C) consequently the classical chiral Ward identity is exact at every finite truncation level; (D) the anomaly appears only when the truncation is removed after a regulator has been inserted into the mode sum: the regularised difference of two shifted mode sums has a nonzero limit, and the coefficient extracted from it is ∫₀^∞ (−f′(s)) ds = f(0) = 1 in d = 2 and ∫₀^∞ s f″(s) ds = f(0) = 1 in d = 4; (E) this coefficient is the same for every admissible regulator profile, which is the Adler–Bardeen statement in the present framework. The geometric (Dirac-trace) prefactors q²/2π and q²/16π² enter through an explicitly displayed hypothesis and are not derived here; the topological interpretation (F) is stated as a discussion, and only the uniqueness of the topological charge is proved. A "honest report" section records exactly where each proof stops. Lean 4 formalisation: eight modules, 42 registered declarations, all depending only on [propext, Classical.choice, Quot.sound]; no sorry, no admit, no new axioms. Numerical verification script is deterministic (dense linear algebra and Gauss–Legendre quadrature, no Monte Carlo).