The squared reproducing kernel as a function of the time offset u = t − s alone: k(u)² = (2W sincN(2Wu))² = sin(2πWu)²/(π²u²). bandKernel depends on (t, s) only through t − s, so this loses nothing (bandKernel_norm_sq_eq) while making the evenness and the total energy ∫_ℝ k² = 2W statable as one-variable facts.

The one-sided energy tail ψ(a) = ∫_{u>a} k(u)² du of the reproducing kernel.

This is the quantity the window deficit is built from: for t in [0,T], the kernel energy that [0,T] fails to capture is exactly ψ(t) + ψ(T−t) (setIntegral_bandKernelSq_window). Two bounds control it, and their crossing at a = 1/(2W) is what produces the logarithm: ψ(a) ≤ W (bandKernelTail_le_const, from the total energy 2W) and ψ(a) ≤ 1/(π²a) (bandKernelTail_le_inv, from |sin| ≤ 1).

The trace deficit of the time-and-band limiting operator against its window is O(log WT): the reproducing kernel k(t − s) = sin(2πW(t−s))/(π(t−s)) loses only logarithmically much of its energy ‖k_t‖² = 2W off the window [0,T].

This is the operator-free, non-asymptotic core of the Landau-Widom second moment tr A − tr A² = O(log WT): the double integral is tr A² once the Parseval template of tsum_inner_timeBandLimitingOp_eq is polarized, and 2WT is tr A exactly (tsum_inner_timeBandLimitingOp_eq), so the difference bounded here is the second moment ∑ λₙ(1 − λₙ).

The mechanism is two facts about k and nothing else — no sinc theory, no spectral theory, no Schatten API. The tail ψ(a) = ∫_{u>a} k(u)² du obeys ψ(a) ≤ W (total energy ∫_ℝ k² = 2W, by bandKernelSq_integral, split by evenness) and ψ(a) ≤ 1/(π²a) (from |sin| ≤ 1); the deficit is exactly 2∫₀ᵀ ψ (bandKernel_window_deficit_eq), and splitting that integral at a₀ = 1/(2W) — the first bound below a₀, the second above — gives 1 + (2/π²)·log(1+2WT). The constant stated is the looser 2 + log(1+2WT), which absorbs the 2WT < 1 branch without a case split at the headline.

Scope: this is the deficit bound, an explicit inequality at every fixed T and W with no WT → ∞ limit anywhere in it, and it is stated with a named constant rather than under an ∃ C. It is one piece of the Landau-Pollak-Slepian concentration, not the whole of it: reaching that composes the polarized Parseval identity ∑ᵢ ‖A bᵢ‖² = ∫₀ᵀ∫₀ᵀ |k(t−s)|² (reading the double integral as tr A², tsum_norm_timeBandLimitingOp_sq_eq) with the eigenbasis bridge of tsum_prolateEigenvalues_eq (reading either moment against prolateEigenvalues). What this bound settles is that the analytic content of the second moment is elementary calculus, not missing theory.

The tail estimate was re-derived rather than taken on trust: ∫_{[0,T]} k(t−s)² ds = 2W − ψ(t) − ψ(T−t) by substituting u = t − s and reflecting the far tail through the evenness of k², so the deficit is 2∫₀ᵀψ as claimed. Non-vacuity is real, not formal: ∫∫ ≥ 0 always, so at ∫∫ = 0 the claim would read 2WT ≤ 2 + log(1+2WT), false for large T — the bound has content, and 2 + log(1+2WT) = o(T) keeps it useful to the consumers. Two structurally different degenerate boundaries were checked: T = 0 gives 0 ≤ 2, and 2WT < 1 gives 2∫₀ᵀψ ≤ 2WT ≤ 1, the branch the constant 2 absorbs. hW : 0 < W is regularity (it keeps log(1+2WT) off its junk branch), not load-bearing. @audit:ok

The reproducing kernel is itself band-limited. Its Fourier transform is the spectral boxcar specBoxcar t (1/(2W)) (fourier_shiftSinc_toLp), whose support [-1/(2Δ), 1/(2Δ)] is exactly the band [-W,W] at Δ = 1/(2W); membership in bandLimitSubspace W is then the definition of that subspace as a Fourier comap. This is what lets P_W Q_T k_t be read as A k_t below. @audit:ok

‖A f‖² ≤ ⟪A f, f⟫: the operator inequality A² ≤ A for A = P_W Q_T P_W, proved from the two facts that build A — P_W is a contraction and Q_T is a self-adjoint idempotent — rather than from any spectral calculus. @audit:ok

The second moment of the time-and-band limiting operator along any complete orthonormal basis is exactly the energy of the reproducing kernel over the window square: tr A² = ∫₀ᵀ∫₀ᵀ |k(t−s)|² ds dt. Together with tsum_inner_timeBandLimitingOp_eq (tr A = 2WT) this identifies both moments of A with explicit kernel integrals.

Since A is self-adjoint, ‖A bᵢ‖² = ⟪A² bᵢ, bᵢ⟫, so the left side is the second moment; for an eigenbasis it is ∑ₙ λₙ².

The mechanism is the Parseval template of tsum_inner_timeBandLimitingOp_eq, applied one level deeper. Peeling A's outer P_W off ‖A bᵢ‖² = ⟪Q_T P_W bᵢ, P_W Q_T P_W bᵢ⟫ and using the reproducing property twice turns each term into ∫₀ᵀ ⟪A k_t, bᵢ⟫⟪bᵢ, k_t⟫ dt, whose sum over the basis is ⟪A k_t, k_t⟫ by HilbertBasis.hasSum_inner_mul_inner; the kernel is band-limited (bandLimitProj_bandKernelLp), so that quadratic form collapses to ‖Q_T k_t‖², the inner integral. Unlike the first moment the summands here are not pointwise nonnegative, so the swap is integral_tsum rather than Tonelli, dominated by ∑ᵢ ‖Fᵢ(t)‖ ≤ 2W (AM-GM plus Parseval on each factor). No trace-class, Schatten, or spectral theory is used, and no cyclicity of the trace: the identity is proved for A = P_W Q_T P_W directly, never routed through Q_T P_W Q_T.

Scope: this is an exact identity at every fixed T, W, with no WT → ∞ limit in it, quantified over every Hilbert basis of L²(ℝ;ℂ) — not a bound, not a specialization to a constructed basis. It is one piece of the Landau-Pollak-Slepian concentration, not the whole of it: reading either moment against prolateEigenvalues goes through the eigenbasis multiplicity bridge (tsum_prolateEigenvalues_eq), and the count #{λₙ > c} composes both moments via a Chebyshev split (prolateCount_le / le_prolateCount).

The reading of the left side as tr A² was checked rather than assumed: A is self-adjoint in-tree (timeBandLimitingOp_isSelfAdjoint, consumed in the body), so ⟪A²bᵢ, bᵢ⟫ = ⟪A bᵢ, A bᵢ⟫ = ‖A bᵢ‖², and the identity is proved basis-independently — which is what makes the eigenbasis instance available for free once that basis is built. The quantification is not vacuous in form only: E ≠ 0 is in-tree (timeBandLimitingOp_ne_zero, bandKernelLp_norm_sq = 2W > 0), so every HilbertBasis of it is inhabited, and exists_hilbertBasis_tsum_norm_timeBandLimitingOp_sq_eq witnesses one. @audit:ok

The Landau-Widom second moment, non-asymptotically: tr A − tr A² ≤ 2 + log(1 + 2WT) along any complete orthonormal basis: the time-and-band limiting operator differs from a projection by only logarithmically much. For an eigenbasis the left side is ∑ₙ λₙ(1 − λₙ), the quantity that measures how far the prolate spectrum is from the 0/1 cliff.

Everything on the left is an exact identity — tr A = 2WT (tsum_inner_timeBandLimitingOp_eq) and tr A² = ∫₀ᵀ∫₀ᵀ|k(t−s)|² (tsum_norm_timeBandLimitingOp_sq_eq) — so the content is the elementary kernel-tail estimate bandKernel_window_deficit_le. Splitting the tsum of a difference needs both families summable: the first is summable because its terms are nonnegative with partial sums capped by 2WT (summable_inner_timeBandLimitingOp_self), and the second is dominated by it termwise via A² ≤ A (norm_timeBandLimitingOp_sq_le_inner).

Scope: this is a bound at every fixed T, W with a named constant and no WT → ∞ limit, quantified over every Hilbert basis. Composed with the eigenbasis multiplicity bridge (tsum_prolateEigenvalues_eq, reading this sum as ∑ₙ λₙ(1 − λₙ)) and the Chebyshev split from the second moment to the count (prolateCount_le / le_prolateCount), this gives the Landau–Pollak–Slepian count concentration #{n | λₙ > c} = 2WT + O(log WT).

Textbook Landau-Widom is an asymptotic equality tr A − tr A² ~ (1/π²)·log(2WT); this is only a one-sided upper bound with a loose constant — strictly weaker. That weaker form is nevertheless sufficient: with 0 ≤ λ ≤ 1 (timeBandLimitingOp_norm_le_one plus inner_timeBandLimitingOp_self_nonneg), tr A = 2WT exactly, and tr A − tr A² ≤ D, the split #{λ>c} − ∑_{λ>c}λ = ∑_{λ>c}(1−λ) ≤ D/c gives #{λ>c} ≤ 2WT + D/c, and ∑_{λ≤c}λ ≤ D/(1−c) gives #{λ>c} ≥ 2WT − D/(1−c). Both halves of #{λ>c} = 2WT + O(log WT) — the converse's and the achievability's — thus follow from the upper bound alone at any fixed c; at c = 1/2 the error is 2D. Neither the sharp constant nor a matching lower bound on the second moment is needed: the textbook Landau-Widom asymptotic equality is stronger than what its consumers require. .re hides no sign error — A = P_W Q_T P_W is positive semidefinite, so ⟪A bᵢ, bᵢ⟫ is real (inner_timeBandLimitingOp_self_nonneg) and .re discards nothing. @audit:ok

Non-vacuity of the two identities above, machine-checked rather than asserted: a Hilbert basis of L²(ℝ;ℂ) exists (exists_hilbertBasis), so both the second-moment identity and the Landau-Widom bound are statements about a real object and not empty quantifications. @audit:ok