For a Markov channel each fiber W x is a probability measure, so its singleton masses sum to 1 over the finite output alphabet.

Cross-entropy form of klDivPmf: for a sub-probability-free pmf P (only required non-negative and summing to 1) and a full-support pmf Q, klDivPmf P Q equals the cross-entropy minus the entropy of P. Unlike klDivPmf_eq_log_diff_sum, P may vanish.

Keystone bridge (I = H(Y) − H(Y|X)): for p ∈ stdSimplex, the channel mutual information equals the output entropy minus the weighted conditional entropy of the fibers.

The one-sided (right) directional derivative of t ↦ I(p_t; W).toReal at t = 0 along the segment p_t := (1 - t) • p + t • δ_a towards the Dirac input at a equals D(W(a)‖q*) − I(p; W) (the envelope/Danskin cancellation: the moving reference q_{p_t} contributes nothing because ∑_b (dq/dt)(b) = 0).

Stated as a HasDerivWithinAt over Set.Ici 0 (right derivative), NOT a two-sided HasDerivAt. The two-sided form is FALSE for boundary achievers: when p a = 0, for t < 0 the segment leaves the simplex (p_t a = t < 0), pmfToMeasure clamps the negative coordinate via ENNReal.ofReal to 0, giving the non-probability measure (1 - t) • pmfToMeasure p, so I(p_t; W).toReal no longer follows the smooth simplex functional and develops a corner at 0 (left derivative ≠ right derivative). Concrete refutation: α = β = Bool, p = δ_false, a = true, any channel with W false full support and W true ≠ W false; the right derivative is D(W true‖W false) > 0, but the left branch is the non-probability functional t ↦ (klDiv ((1-t) • J) ((1-t)² • (J)) ).toReal (here the input-deterministic joint J equals the product measure), whose derivative at 0 does not match. The one-sided form is also exactly what the downstream first-order optimality argument consumes (cf. csiszar_first_order_condition, which uses the 𝓝[>] 0 slope). @audit:ok

Capacity saddle point: for a capacity-achieving input p with full-support output q* := outputDistribution (pmfToMeasure p) W, every input symbol a satisfies D(W(a)‖q*) ≤ capacity W. Carved out as a shared lemma for reuse across the channel-coding converse family. @audit:ok

The expectation of the per-letter log-likelihood ratio log (W a)(·) − log q*(·) under the channel fiber W a is the discrete KL divergence D(W a ‖ q*).

Uniform bound on the per-letter log-likelihood ratio log (W a)(b) − log q*(b) across the finite input/output alphabets; an n-independent variance bound for the information density.

Per-codeword Chebyshev bound: for block length n ≥ 1, the channel-output mass of the high-LLR set for codeword m is at most B² / (δ/2)² · (1/n), where B := llrUnifBound W p is an n-independent uniform bound on the per-letter log-likelihood ratios. Uses the saddle point klDiv_channel_le_capacity for the uniform mean bound.

The average high-LLR tail mass vanishes as the block length grows, using the non-i.i.d. Chebyshev concentration (meas_ge_le_variance_div_sq + variance_sum_pi) with the i.i.d. reference q*^n and threshold n·(capacity W + δ/2). Depends on the saddle point klDiv_channel_le_capacity for the uniform per-codeword mean bound.

Wolfowitz strong converse (asymptotic): for a memoryless channel W over finite alphabets, if the rate log (M n) / n eventually exceeds capacity W + δ (with δ > 0), then the average error probability tends to 1.

The capacity-achieving input p (existing by exists_capacity_achiever) is received explicitly together with the regularity precondition hq_pos (full-support output, so the log-likelihood ratios are well-defined); both are preconditions, not load-bearing hypotheses. @audit:ok

An operationally achievable rate is at most the capacity: if for every target error ε > 0 all large enough block lengths carry a code with at least exp (n R) messages and average error below ε, then R ≤ capacity W.

This is the contrapositive of channelCoding_strong_converse_asymptotic: were capacity W < R, the codes would have rate eventually above capacity W + (R - capacity W), forcing their average error to tend to 1 and contradicting the ε-small errors. The capacity achiever p and the full-support output hq_pos are the preconditions of the strong converse, passed through unchanged. @audit:ok