Sinc synthesis at grid spacing Δ = T/n: the band-limited signal interpolating the sample values a : Fin n → ℝ at the nodes t_i = i·(T/n). This is the synthesis direction (build a band-limited function from finitely many samples), dual to the analysis direction of whittaker_shannon_bandlimited.

sincN of a difference of natural-number casts is the Kronecker delta.

At a sample node t = j·(T/n), the sinc synthesis recovers the sample value exactly: all sinc cross-terms vanish (sincN at nonzero integers is 0).

The spectral boxcar Δ · e^{-2πi c ξ} supported on [-1/(2Δ), 1/(2Δ)]. This is the L²-Fourier transform of the shifted, dilated normalized sinc t ↦ sincN((t - c)/Δ).

Dilated boxcar integral: rescaling the fundamental-interval identity integral_exp_boxcar_eq_sincN to the band [-1/(2Δ), 1/(2Δ)].

The spectral boxcar lies in every Lᵖ: it is bounded by Δ on a compact set.

Pointwise inverse Fourier transform of the spectral boxcar is the shifted, dilated sinc.

The complexified shifted, dilated sinc lies in L² (it is the inverse transform of an L¹ ∩ L² boxcar).

The abstract L²-Fourier transform of the sinc's canonical Lp representative is the boxcar's canonical Lp representative.

Boxcar orthogonality (Plancherel on the band): the L² inner product of two spectral boxcars collapses to Δ · sincN((c - c')/Δ).

The complexified synthesis lies in L² (a finite sum of L² shifted sincs).

The synthesis's canonical Lp representative decomposes as the finite Lp combination ∑ᵢ aᵢ • (shifted sinc)ᵢ.

The sinc synthesis is band-limited to [-W, W] provided the sample count satisfies the Nyquist bound n ≤ 2WT: each shifted sincN(·/Δ) (spacing Δ = T/n) has spectrum supported in [-1/(2Δ), 1/(2Δ)] = [-n/(2T), n/(2T)], and n/(2T) ≤ W.

@audit:ok

The squared synthesis is integrable on the whole line (it lies in L²).

@audit:ok

Parseval / sinc self-reproducing energy identity: the whole-line energy of the sinc synthesis equals Δ · ∑ᵢ (a i)² with Δ = T/n. Follows from the sinc orthogonality ∫ sincN((t-iΔ)/Δ)·sincN((t-jΔ)/Δ) dt = Δ·δᵢⱼ.

@audit:ok

The crude rate bound via Bessel's inequality alone, for codes with at least one observation: log M is capped by (T·P + 1)/N₀ plus the Fano terms, uniformly in the observation count k. This is where Bessel meets awgn_converse, and where ln(1+x) ≤ x discards the k-dependence.

With no observations at all the receiver learns nothing: every message is decoded to the same one, so the average error is exactly (M-1)/M.

The message-count set is bounded above — the BddAbove obligation needed to lower-bound contAwgnMaxMessages via le_csSup.

It closes by Bessel's inequality alone, without the ≈ 2WT degrees-of-freedom count. The test family testFn is orthonormal, so for every codeword

`∑ᵢ (observation m i)² = ∑ᵢ ⟨encoder m, testFn i⟩² ≤ ‖encoder m‖₂² ≤ T·P`,

uniformly in the observation count k — no spacing, rate or bandwidth hypothesis enters, and the whole-line encoder_power supplies the right-hand side directly. That energy bound feeds awgn_converse on the induced discrete code contAwgnToAwgnCode (per-observation power P' = (T·P + 1)/k, whose power_constraint holds by construction; the +1 keeps it strictly positive when P = 0), and log(1+x) ≤ x collapses the k-dependence:

`(k/2)·log(1 + 2(T·P+1)/(k·N₀)) ≤ (T·P+1)/N₀`.

Rearranging the Fano terms against ε < 1 gives log M ≤ ((T·P+1)/N₀ + log 2)/(1-ε), a bound free of k, so the message set is capped. Two degenerate branches sit outside that argument and are handled separately: M < 2 (below the converse's range) and k = 0, where the receiver observes nothing, every message decodes to the same one, the average error is exactly (M-1)/M, and ε < 1 alone caps M ≤ 1/(1-ε).

That the bandwidth constraint is unused here is the point rather than an oversight: hW is the only hypothesis the proof never touches, and it is retained solely to keep the signature uniform with the rest of the sandwich (W itself still appears, via ContAwgnCode T W P M). The proof in fact reads neither encoder_bandlimited nor testFn_support: orthonormality of testFn plus the whole-line encoder_power are the only structure fields the bound needs.

This bound is deliberately crude, and its crudeness is load-bearing evidence rather than a shortcoming: it caps the rate at P/N₀, which ln(1+x) ≤ x makes strictly larger than bandlimitedAwgnCapacity W N₀ P. Boundedness is free; the exact constant is not, and it is the part that still needs the prolate eigenvalue count (see contAwgn_eq_shannonHartley).

Hypotheses are regularity-only (not load-bearing).

@audit:ok