A length-n codebook for one MAC user: a function from message indices to length-n words. Two codebooks (one per user) make up a MACCode.

Joint-typical pair decoder. Given a received word y, returns the unique message pair (m₁, m₂) such that (c₁ m₁, c₂ m₂, y) ∈ macJointlyTypicalSet …, falling back to (⟨0, hM₁⟩, ⟨0, hM₂⟩) if either no such pair exists or it is not unique.

Bundle two codebooks + the joint-typical pair decoder into a MACCode.

Four-event Bonferroni bound for the joint-typical pair decoder: when the pair (m₁, m₂) is sent, the per-pair error probability is bounded by the four error events:

• E0 — the correct codeword triple (c₁ m₁, c₂ m₂, y) is not jointly typical;
• E1 — some user-1 alias m₁' ≠ m₁ (with user 2 correct) is jointly typical;
• E2 — some user-2 alias m₂' ≠ m₂ (with user 1 correct) is jointly typical;
• E3 — some pair (m₁', m₂') with both indices wrong is jointly typical.

The block output law is ν = Measure.pi (i ↦ W (c₁ m₁ i, c₂ m₂ i)). This is the two-codebook / four-event generalization of the single-user errorProbAt_le_E1_plus_E2; the two-codebook averaging consumes the four terms term by term.

I(X₁; (X₂, Y)) = H(X₁) + H(X₂, Y) − H(X₁, X₂, Y) for the per-coordinate joint.

I(X₂; (X₁, Y)) = H(X₂) + H(X₁, Y) − H(X₁, X₂, Y).

I((X₁, X₂); Y) = H(X₁, X₂) + H(Y) − H(X₁, X₂, Y).

Product-measure slice expansion over the first factor (finite alphabets).

A finite-alphabet measure of a set equals the indicator sum over singletons.

The first-input marginal of the per-coordinate MAC joint law is p₁.

The per-coordinate MAC joint law singleton mass: ν{(a₁, a₂, b)} = p₁{a₁} · p₂{a₂} · W(a₁, a₂){b}.

The per-coordinate (X₂, Y) marginal singleton mass: ν_{X₂Y}{(a₂, b)} = p₂{a₂} · ∑_{a₁} p₁{a₁} W(a₁, a₂){b}.

The X₁-block law under the MAC ambient measure equals Measure.pi p₁.

The (X₂, Y)-joint-block law singleton mass factorizes over coordinates as a product of the per-coordinate (X₂, Y) marginal masses.

Pair-channel conditional-output fold-in, in singleton form: the (X₂, Y)-joint block-law mass at (x₂, y) equals the average over the true user-1 codeword x₁ ~ p₁ⁿ of the paired-channel output mass at y, weighted by the user-2 codeword mass. This is where the two-codebook averaging does its work: the true user-1 input is marginalized out of the pair channel W(·, x₂ i) to recover the conditional (X₂, Y) output law.

Set-level version of the conditional-output fold-in: the (X₂, Y)-joint block law of a finite set T equals the user-2-weighted average over the true user-1 codeword of the paired-channel mass of the x₂-slice of T.

The second-input marginal of the per-coordinate MAC joint law is p₂.

The X₂-block law under the MAC ambient measure equals Measure.pi p₂.

Full-triple split block-law singleton mass factorizes over coordinates as a product of the per-coordinate MAC joint masses.

Master pair-channel fold on the full triple: the full-triple split block law of a finite set T equals the average over the true codeword pair (x₁, x₂) ~ p₁ⁿ ⊗ p₂ⁿ of the paired-channel mass of the corresponding slice of T.

The (X₁, Y)-split joint block-law fold, derived from the master triple fold by projecting out X₂.

The Y-block-law fold, derived from the master triple fold by projecting out both inputs.

The (X₁, X₂)-split joint block-law singleton mass equals p₁ⁿ{x₁} · p₂ⁿ{x₂}, derived from the master triple fold by projecting out the output.

The user-2 independent-pair bound macJTS_indep_prob_le_X2, restated over the split product X₂-block ⊗ (X₁, Y)-joint-block: the jointly typical set is described as a preimage under the reshaping (x₂, (x₁, y)) ↦ (x₁, x₂, y) instead of a reshaped product.

The both-users independent-pair bound macJTS_indep_prob_le_both, restated over the split product (X₁, X₂)-joint-block ⊗ Y-block: the jointly typical set is described as a preimage under the reshaping ((x₁, x₂), y) ↦ (x₁, x₂, y) instead of a reshaped product.