Receiver-2 two-event Bonferroni bound: when the pair m is sent, the receiver-2 per-pair error probability of the cloud joint-typical decoder is bounded by the correct-cloud atypical event E0 plus the wrong-cloud alias union bound. This is the single-user errorProbAt_le_E1_plus_E2 applied along the β₂-projection fun i ↦ (y i).2 of the block output.

Receiver-2 cloud independent-pair bound: under the product of the cloud block law and the Y₂ block law (the random-coding measure for a wrong cloud codeword drawn independently of the received output), the probability of joint typicality is at most exp(−n (I(U; Y₂) − 3ε)). A wrapper of the single-user jointlyTypicalSet_indep_prob_le with the exponent rewritten into the bcInfo₂ form; full support is a regularity precondition, not load-bearing.

The two-receiver output pair coordinate ω ↦ (ω i).2.2 : β₁ × β₂.

Finite-sum change of variables under a pushforward.

The BC per-coordinate joint law singleton mass: ν{(u, a, y₁, y₂)} = pU{u} · K(u){a} · W(a){(y₁, y₂)}.

The U-block law under the BC ambient measure equals Measure.pi pU.

The per-coordinate (U, X, Ypair)-reshaped joint law singleton mass factorizes as pU{u} · K(u){a} · W(a){yp}.

The (U, X, Ypair)-split block-law singleton mass factorizes over coordinates as a product of the per-coordinate reshaped joint masses.

Master superposition channel fold: the (U, X, Ypair)-split block law of a finite set T equals the average over the cloud codeword u ~ pUⁿ and the conditional satellite codeword x ~ Πₗ K(uₗ) of the paired-channel mass of the corresponding slice of T. This is the BC analogue of mac_chan_fold_triple_set, with the conditional (superposition) satellite law replacing the second MAC input's flat product.

Channel fold on the (U, Y₂) axes, in β₂-marginal form: the Y₂-block law of a finite set T equals the cloud/satellite/channel average of the β₂-projected channel mass. Derived from the master fold by projecting out U, X, and the β₁-output. This is the receiver-2 analytic core: the pair output is marginalized to β₂.

Receiver-2 wrong-cloud averaged swap: for a wrong cloud message w₂' ≠ m.2, the two-tier random-codebook average of the wrong-cloud alias event (drawn independently of the transmitted satellite cX m) equals the independent product law (U-block) ⊗ (Y₂-block), and is therefore at most exp(−n (I(U; Y₂) − 3ε)). Combines the satellite single-row marginal (measurePreserving_eval), the cloud two-row marginal (codebook_marginal_two), the (U, Y₂) channel fold, and the independent-pair bound bc_cloud_indep_prob_le.

Channel fold on the (U, Y₂) axes, in joint form: the joint (U, Y₂)-block law of a finite set T equals the cloud/satellite/channel average of the β₂-projected channel mass, retaining the cloud block u inside the slice. Derived from the master fold by projecting out X and the β₁-output while keeping U. This is the receiver-2 correct-cloud analytic core, where the transmitted cloud both indexes the slice and steers the satellite (the U-preserving counterpart of bc_chan_fold_Y₂_set).

Receiver-2 correct-cloud averaged swap for the E0 event: the two-tier random-codebook average of the correct-cloud atypical event equals the joint (U, Y₂)-block law of the atypical set, because the correct cloud cU m.2 steers the satellite, so (cU m.2, Y₂) follows the ambient joint law (not the independent product). Combines the satellite single-row marginal (measurePreserving_eval), the cloud single-row marginal (codebook_marginal_one), and the joint (U, Y₂) channel fold (bc_chan_fold_UY₂_set). This is an equality; the typicality LLN that makes the joint mass vanish is established separately in bc_E0₂_vanishing.

Receiver-1 three-event Bonferroni bound: when the pair m is sent, the receiver-1 per-pair error probability of the superposition joint-typical decoder is bounded by three sub-events along the β₁-projection fun i ↦ (y i).1 of the block output:

• E0 — the correct triple (Uⁿ(m₂), Xⁿ(m), y₁) is not jointly typical;
• E_b (wrong satellite, correct cloud) — some m₁' ≠ m₁ makes (Uⁿ(m₂), Xⁿ(m₁', m₂), y₁) jointly typical;
• E_c (wrong cloud, any satellite) — some cloud alias m₂' ≠ m₂ with any m₁' makes (Uⁿ(m₂'), Xⁿ(m₁', m₂'), y₁) jointly typical.

Because a wrong-cloud alias steers its satellite from an independent cloud, the two "correct cloud / wrong cloud" families collapse the four MAC alias events into three: the MAC E1/E2/E3 split is absorbed as E_b (m₂' = m₂, m₁' ≠ m₁) and E_c (m₂' ≠ m₂, any m₁'). This is the receiver-1 analogue of mac_errorProbAt_le_bonferroni4 reworked to the superposition decoder; E_b/E_c are left as raw measure terms for the exponent-bounding legs.

Channel fold on the (U, Y₁) axes, in β₁-marginal form: the Y₁-block law of a finite set T equals the cloud/satellite/channel average of the β₁-projected channel mass. The receiver-1 analogue of bc_chan_fold_Y₂_set. @audit:ok

The joint information I((U, X); Y₁) = H(U, X) + H(Y₁) − H(U, X, Y₁) of the per-coordinate joint law. This is the exponent of the receiver-1 wrong-cloud error: a wrong cloud alias carries an independent (U, X) pair, so the false-alarm exponent is the full joint information I((U, X); Y₁), and it is this quantity that caps the rate sum R₁ + R₂. @audit:ok

The (U, X)-split block-law singleton mass factorizes as pUⁿ{u} · Kⁿ(u){x}, derived from the ambient block law of the paired (U, X) coordinate. @audit:ok

Receiver-1 wrong-cloud independent-pair bound: the distributed average over an independent (U, X) pair and the Y₁-block law of the jointly-typical event is at most exp(−n (I((U, X); Y₁) − 3ε)). BC instantiation of macJTS_indep_prob_le_both with the axes (U, X) ⟂ Y₁. @audit:ok

Conditional-slice satellite covering bound with the typicality hypotheses removed: when u or y₁ is atypical the slice is empty (joint typicality forces both marginals typical), so the bound holds vacuously; when both are typical it is exactly bc_conditional_slice_prob_le. @audit:ok

Receiver-1 wrong-satellite/correct-cloud averaged swap for the E_b event: for a wrong satellite index m₁' ≠ m.1 (same cloud column m.2), the two-tier random-codebook average of the wrong-satellite alias event is at most exp(−n (I(X; Y₁ ∣ U) − 4ε)). Both the transmitted satellite cX m (channel driver) and the alias cX (m₁', m.2) are drawn i.i.d. from the same cloud column m.2; averaging out the alias inside the channel integral yields the conditional covering bound bc_conditional_slice_prob_le_uncond. @audit:ok

Receiver-1 wrong-cloud averaged swap for the E_c event: for a wrong cloud message p.1 ≠ m.2 (with any satellite index p.2), the two-tier random-codebook average of the wrong-cloud alias event is at most exp(−n (I((U, X); Y₁) − 3ε)). The wrong cloud cU p.1 and its satellite cX (p.2, p.1) are drawn independently of the transmitted (cX m)-driven channel, giving the independent-pair bound bc_joint_indep_prob_le. @audit:ok