Receiver-2 single-letterization for the BC converse: with Uᵢ = (W₂, Y₂^{i-1}), the message–output mutual information obeys I(W₂; Y₂ⁿ) ≤ ∑ᵢ I(Uᵢ; Y_{2,i}). Pure chain-rule plumbing on a prefix conditioner — no Csiszár identity, no degradedness. Typed analogue of bc_converse_bound_a.

Receiver-1 corner bound of the BC converse at the message level: under a uniform W₁, log |M₁| ≤ I(W₁; (W₂, Y₁ⁿ)) + h(Pe₁) + Pe₁ · log(|M₁| − 1), with Pe₁ the receiver-1 error probability of the Y₁-only decoder.

Receiver-2 corner bound of the BC converse at the message level: under a uniform W₂, log |M₂| ≤ I(W₂; Y₂ⁿ) + h(Pe₂) + Pe₂ · log(|M₂| − 1), with Pe₂ the receiver-2 error probability.

Message-level Fano outer bound for the broadcast channel: for uniform messages decoded by per-receiver decoders, the rate pair satisfies the two message-level Fano information bounds, packaged as InBCCapacityRegion. The single-letterization that turns this into the textbook degraded-BC converse is bc_degraded_converse.

Receiver-1 input-level single-letterization of the BC converse, via term-by-term degradedness: under a memoryless broadcast channel with the conditioning message W₂ upstream of the channel and physical degradedness X → Y₁ → Y₂, the conditional block input–output mutual information collapses to the per-letter auxiliary-variable sum I(Xⁿ; Y₁ⁿ | W₂) ≤ ∑ᵢ I(Xᵢ; Y_{1,i} | Uᵢ) with Uᵢ = (W₂, Y₂^{i-1}).

Proof (entropy-difference route, mirroring the MAC single-letterization condMutualInfo_singleletter_le_of_memoryless): both sides reduce to conditional-entropy differences H(Y₁ | ·) − H(Y₁ | ·, X). The joint-output memoryless hypothesis h_memo collapses every "noise" term H(Y₁ᵢ | …, Xᵢ) to the common H(Y₁ᵢ | Xᵢ) on both sides, so those cancel; what remains is H(Y₁ⁿ | W₂) ≤ ∑ᵢ H(Y₁ᵢ | W₂, Y₂^{i-1}), which holds term-by-term via the LHS chain rule and the conditioner swap H(Y₁ᵢ | W₂, Y₁^{<i}) ≤ H(Y₁ᵢ | W₂, Y₂^{<i}) (block-prefix degradedness h_deg_block plus conditioning-reduces-entropy).

The two structural preconditions encode the channel, not the conclusion:

• h_memo — joint-output memoryless: Y₁ᵢ ⫫ (W₂, X^{≠i}, Y₁^{≠i}, Y₂^{≠i}) | Xᵢ. It blocks the conditioning message W₂ and all other letters (including the degraded outputs Y₂^{≠i}) at Xᵢ. Blocking Y₂^{≠i} is needed by the entropy-difference route: it collapses the RHS noise term H(Y₁ᵢ | W₂, Y₂^{<i}, Xᵢ) to the common H(Y₁ᵢ | Xᵢ).
• h_deg_block — block-prefix degradedness: Y₁ᵢ ⫫ Y₂^{<i} | (W₂, Y₁^{<i}). This is the d-separation consequence of physical per-letter degradedness X → Y₁ → Y₂ together with memorylessness; per-letter degradedness Y₂ⱼ ⫫ Xⱼ | Y₁ⱼ alone is insufficient (it is satisfied by the documented n = 2 collider counterexample — an early degraded output leaking a later letter's input — which breaks the bound), and deriving the block form from the per-letter form needs graphoid / d-separation machinery absent from Mathlib, so it is taken as a structural precondition (parity with h_memo). This is the hypothesis that rules out the collider counterexample (it fails there: Y₁₁ ⫫ Y₂₀ | (·, Y₁₀) is false when Y₁₁ = Y₂₀), whereas the strengthened h_memo still holds in it.

Both are regularity / structural preconditions (true in the operational degraded-memoryless setup where Xⁿ = encoder (W₁, W₂)), not load-bearing.

@audit:ok

Receiver-1 single-letterized corner bound of the BC converse: the message–output mutual information I(W₁; (W₂, Y₁ⁿ)) is bounded by the per-letter auxiliary-variable sum ∑ᵢ I(Xᵢ; Y_{1,i} | Uᵢ) with Uᵢ = (W₂, Y₂^{i-1}), Xᵢ = (encoder (W₁, W₂))ᵢ.

Reduction: independence gives I(W₁; (W₂, Y₁ⁿ)) = I(W₁; Y₁ⁿ | W₂); data processing along W₁ → Xⁿ → Y₁ⁿ (conditioned on W₂) gives ≤ I(Xⁿ; Y₁ⁿ | W₂); then the input-level single-letterization bc_input_singleletterize closes the bound.

@audit:ok

Single-letter outer bound for the degraded broadcast channel (Cover–Thomas): for uniform, independent messages sent over a degraded memoryless broadcast channel X → Y₁ → Y₂ and decoded per receiver, the rate pair (log |M₁|, log |M₂|) lies in the auxiliary-variable capacity region whose information bounds are the per-letter channel sums ∑ᵢ I(Xᵢ; Y_{1,i} | Uᵢ) (receiver 1) and ∑ᵢ I(Uᵢ; Y_{2,i}) (receiver 2), with Uᵢ = (W₂, Y₂^{i-1}), plus the Fano error slack.

The degradedness and memoryless structure are preconditions (parity with the single-user channel_coding_converse_general_memoryless_pure and mac_converse). The operational instantiation — building μ from uniform messages through the encoder and the channel — is a separate wrapper, not part of this statement.

@audit:ok