For V = prolateEigenspaceSup T W c (0 < c), there is a ℂ-orthonormal basis u of V together with a band-limited real encoder family h (real representatives of u) and a receiver test-function family φ, [0, T]-supported and pointwise-orthonormal, such that for every coefficient vector v : Fin (prolateCount T W c) → ℝ the receiver's recovered energy equals the time-limited energy of the corresponding V-combination: ∑ᵢ (∫ (∑ⱼ vⱼ hⱼ)·φᵢ)² = ‖Q_T (∑ⱼ vⱼ uⱼ)‖², with Q_T = (timeLimitSubspace T).starProjection.

The φ family is the [0, T]-supported real orthonormal basis of S = span_ℝ {Q_T uⱼ}; the energy identity holds because the time-limited encoders Q_T uⱼ span S, so the receiver recovers the full time-limited energy of any V-combination. @audit:ok

The cross-map A v = (∫ (∑ⱼ vⱼ hⱼ)·φᵢ)ᵢ sending encoder coefficients to receiver observations is bounded below by √c: c ∑ᵢ vᵢ² ≤ ∑ᵢ (A v)ᵢ². This is the hbdd input to ShannonHartleyPreequalizer.exists_preequalizer (once A is read as an endomorphism of EuclideanSpace ℝ (Fin (prolateCount T W c)), where ‖v‖² = ∑ᵢ vᵢ² and ‖A v‖² = ∑ᵢ (A v)ᵢ²), which then yields the norm-controlled pre-equalizer ‖a‖² ≤ (1/c) ‖x‖².

The bound is the energy identity of exists_testFn_family composed with the time-window energy concentration le_norm_timeLimitProj_sq_of_mem (c ‖w‖² ≤ ‖Q_T w‖² on V) and ‖∑ⱼ vⱼ uⱼ‖² = ∑ⱼ vⱼ² (u is ℂ-orthonormal, v real). @audit:ok

A discrete AWGN code on prolateCount T W c observations lifts to a continuous-time code, giving a lower bound on contAwgnMaxMessages.

Given a discrete AwgnCode on k = prolateCount T W c observations at per-observation power c·T·P/k whose every message decodes with error < ε, the receiver cross-map A of exists_crossMap_lower_bound (bounded below by √c) is invertible with norm control (exists_preequalizer), so each discrete codeword xₘ has a band-limited pre-image bₘ. The signals ∑ⱼ (bₘ)ⱼ hⱼ are then band-limited codewords of a ContAwgnCode whose observations equal xₘ exactly; the error probability transports unchanged, and le_csSup (via the wall-free contAwgnMaxMessages_bddAbove) turns the discrete message count into the lower bound.

@audit:ok

The per-window rate log(contAwgnMaxMessages T)/T is bounded above (the operational capacity is finite): from the Bessel converse the message count grows no faster than exp(T·P/(N₀(1-ε))), so the rate is capped near P/(N₀(1-ε)).

The per-ε rate is nonnegative: contAwgnMaxMessages is a ℕ, so its log is ≥ 0.

The core per-ε achievability step: the closed form is below the operational rate at level ε. @audit:ok

The operational capacity is at least the Shannon-Hartley closed form (achievability, ≥).

The infimum over ε reduces (via le_ciInf over the phantom-free subtype ↥(Set.Ioo 0 1)) to the per-ε bound sh_le_contAwgnRate, which builds continuous-time band-limited codewords out of a discrete AwgnCode on prolateCount T W c observations (contAwgnMaxMessages_ge_of_awgnCode) fed by the block awgn_channel_coding_theorem, and reads off the ≈ 2WT degrees-of-freedom count prolateCount_div_tendsto (from le_prolateCount / prolateCount_le) through a limsup comparison.

The achievability half needs only that prolateCount T W c / T converges to 2W (the crude two-sided count), not the tight Landau-Pollak-Slepian concentration. The infimum is taken over the phantom-free subtype ↥(Set.Ioo 0 1): the bounded binder ⨅ ε ∈ Set.Ioo 0 1 would instead pick up the phantom sInf ∅ = 0 from every ε ∉ (0,1) on the conditionally-complete ℝ, collapsing the capacity to 0.

Hypotheses hW/hN₀/hP are regularity-only (not load-bearing).

@audit:ok (sorryAx-free; signature scan regularity-only, no load-bearing hyp. The block awgn_channel_coding_theorem's only non-rate hypothesis h_meas is discharged by the theorem AWGN.isAwgnChannelMeasurable N, not leaked into this signature; the load-bearing awgn_capacity_closed_form (h_bridge_gauss/h_bdd/h_max_ent) is off-path — 0 transitive references from this headline.)