The per-coordinate broadcast joint law on U × α × β₁ × β₂: the compProd chain pU → K → W (U ∼ pU, X ∣ U ∼ K, (Y₁, Y₂) ∣ X ∼ W), reshaped from the left-nested (U × α) × (β₁ × β₂) to the right-nested quadruple.

The i.i.d. broadcast ambient measure: Measure.infinitePi (fun _ ↦ bcJointDistribution pU K W).

The cloud coordinate ω ↦ (ω i).1.

The satellite input coordinate ω ↦ (ω i).2.1.

The first-receiver output coordinate ω ↦ (ω i).2.2.1.

The second-receiver output coordinate ω ↦ (ω i).2.2.2.

The cloud information I(U; Y₂) = H(U) + H(Y₂) − H(U, Y₂) of the per-coordinate joint law. This is the achievable rate of receiver 2, which decodes the cloud tier alone.

The satellite conditional information I(X; Y₁ ∣ U) = H(U, X) + H(U, Y₁) − H(U, X, Y₁) − H(U) of the per-coordinate joint law. This is the achievable rate of receiver 1, which decodes the satellite tier on top of the cloud U. Unlike the MAC macInfo, this is a genuine four-entropy conditional mutual information, not a plain three-term unconditional one.

A length-n cloud codebook: for each cloud message w₂ a cloud codeword Uⁿ(w₂).

A length-n satellite codebook: for each message pair (w₁, w₂) a satellite codeword Xⁿ(w₁, w₂). Definitionally the BroadcastCode joint encoder.

The cloud codebook law: pU-i.i.d. over all M₂ · n cloud letters.

The satellite codebook law conditional on the cloud codebook u: each satellite letter Xₗ(w₁, w₂) is drawn from K (u w₂ l), independently across pairs and letters. This is the conditional product Πᵢ K(Uᵢ) at the heart of superposition coding — the single point of departure from the MAC flat-product ensemble.

The joint two-tier codebook law on (cloud, satellite) pairs: draw the cloud codebook from bcCloudCodebookMeasure, then the satellite codebook conditionally from bcSatelliteCodebookMeasure.

The map of a coordinate selector under the BC ambient measure equals the map of the selector under the per-coordinate joint law.

Mutual independence of any coordinate selector under the BC ambient measure.

Identical distribution of a coordinate selector across indices.

Entropy of a coordinate selector under the BC ambient measure equals its entropy under the per-coordinate joint law.

The per-coordinate BC joint law has positive singleton mass.

Positivity of any coordinate-selector marginal singleton, reduced to the per-coordinate joint positivity via a chosen fiber witness.

The U-marginal of the BC joint law is pU.

The (U, X)-marginal singleton mass of the BC joint law factorizes as pU {u} · K u {x}.

Per-sequence conditional mass bound: for a typical cloud u and a satellite x whose (U, X)-pair sequence is typical, the conditional-product mass of x is at most exp(−n (H(U, X) − H(U) − 2ε)).

Slice-cardinality bound: the number of satellites x making (u, x, y₁) jointly typical is at most exp(n (H(X, (U, Y₁)) − H(U, Y₁) + 2ε)).

Conditional-slice satellite typicality probability bound for the superposition covering argument. For a fixed typical cloud codeword u and a fixed typical received word y₁, the probability under the conditional product law Πᵢ K(uᵢ) that an independently drawn satellite x is jointly typical with (u, y₁) is at most exp(−n (I(X; Y₁ ∣ U) − 4ε)). This is the receiver-1 "wrong satellite, correct cloud" sub-event of the superposition random-coding argument (Cover–Thomas); the exponent matches bcInfo₁, with the 4ε slack the sum of the four entropy-typicality windows (matching the 3ε slack of the MAC lemmas macJTS_indep_prob_le_*). Full support (hpU/hK/hW) is a regularity precondition of the AEP mass bounds, not load-bearing. @audit:ok

Receiver-2 (cloud tier) joint-typical decoder. Given a received word y₂, returns the unique cloud message w₂ whose codeword Uⁿ(w₂) is jointly typical with y₂, falling back to ⟨0, hM₂⟩ if no such w₂ exists or it is not unique. This is a single-user joint-typical decoder over the cloud codebook — receiver 2 never needs the satellite tier.

Receiver-1 superposition joint-typical decoder. Given a received word y₁, returns the unique message pair (w₁, w₂) such that the cloud/satellite/output triple (Uⁿ(w₂), Xⁿ(w₁, w₂), y₁) is jointly typical, falling back to (⟨0, hM₁⟩, ⟨0, hM₂⟩) otherwise. The typical-set argument order bcUs, bcXs, bcY₁s matches the covering bound bc_conditional_slice_prob_le.

Bundle a cloud codebook cU and satellite codebook cX into a BroadcastCode: cX is the joint encoder, receiver 1 uses the superposition joint decoder, receiver 2 the cloud decoder.