prop:block and [eq:Ncount] packaged as block inputs at height $T$

Let $Z$ be a zero configuration, $P$ a parameter choice (taper profile, exponent $\lambda$, ramp width $w$), and $T$ a real height. The window is $\mathcal{Z}(I')$ with $I' = (T - D_0, 2T + D_0]$, $D_0 = \sqrt{T}$, and the window matrix is $A = \sum_{\rho \in \mathcal{Z}(I')} m_\rho u_\rho u_\rho^{\mathsf T}$ with $u_\rho = (\hat\varphi(\gamma_\rho - \tau_k))_{0 \le k < d}$ [eq:AE]. The analytic hypotheses are:

• PhiHatConj: $\hat\varphi(\bar z) = \overline{\hat\varphi(z)}$ for all $z$;
• PhiHatReal: $\hat\varphi$ is real on the real axis;
• PoissonSq ([lem:poisson]): for every real $\gamma$, $\sum_{k \in \mathbb{Z}} \hat\varphi(\gamma - \tau_k)^2 = a L^2$ (as a HasSum);
• $0 < L(T)$ and $0 < a(T) L(T)^2$.

Statement. Under these hypotheses, Assembly.BlockInputs Z P T holds: the record consumed by the abstract Theorem A assembly, consisting of (in hat units $\hat A = A/(aL^2)$) a decomposition $\hat A = P + Q$ with $P \succeq 0$, $\operatorname{rank} P \le s_1 + s_2$, $\operatorname{tr} P \le N_{\mathrm{on}}(I')$, $Q$ Hermitian with $n_+(Q) \le p$, and $N_{\mathrm{on}}(I') + 2p \le N(I')$; and (in tilde units $\tilde A = A/L$) $n_+(\tilde A) \le s_1 + s_2 + p$, $\operatorname{rank} \tilde A \le \#\mathcal{Z}(I')$, and $s_1 + 2 s_2 + 2p \le N(I')$ [eq:Ncount]. Here $s_1, s_2$ count the on-line simple and multiple zeros of the window and $p$ the off-line pairs.

Role. This is the packaging theorem of the module Zeta23.ZeroSide: prop:block (i)+(ii) and [eq:Ncount], stated exactly as Assembly.thmA_abstract consumes them. It feeds eventually_blockInputs_of (the eventually-in-$T$ export used by Main); the analytic hypotheses are discharged from Taper/Poisson in Zeta23/ZeroSide/Final.lean.