A de Branges chain formalization toward the Riemann Hypothesis: architecture and explicitly axiomatic analytic steps

We describe a formalization architecture toward the Riemann Hypothesis along a de Branges chain strategy: the spectral measure of a zeta-associated Hamiltonian satisfies the Szegő condition; by Lagarias's equivalence this implies RH. Alternatively, a narrowing-strip statement implies RH directly via an $\varepsilon$-argument.