The operational achievability predicate for the MAC rate pair (R₁, R₂): for every target error ε' > 0 there is a block length N such that for all n ≥ N there is a length-n two-user code with at least ⌈exp (n R₁)⌉ / ⌈exp (n R₂)⌉ messages per user whose average error probability is < ε'. This is the ∀ ε'-abstraction of the conclusion of mac_achievability.

The corner-point pentagon of the independent product input p₁ ⊗ p₂: rate pairs with 0 ≤ R₁, 0 ≤ R₂, R₁ ≤ macInfo₁, R₂ ≤ macInfo₂, R₁ + R₂ ≤ macInfoBoth.

The operational MAC capacity region: the topological closure of the achievable set. The exact-rate achievable set is not closed (boundary Pareto faces enter only in the closure), so the capacity region is defined as its closure.

Achievability is a down-set in the rate pair: a lower rate pair is easier. @audit:ok

The strict interior of a pentagon is achievable: a rate pair strictly inside the corner-point region of a full-support product input p₁ ⊗ p₂ is achievable. This is the ∀ ε'-abstraction of mac_achievability. @audit:ok

The zero rate pair (0, 0) is achievable: the trivial single-message code (M₁ = M₂ = 1) never errs, because Fin 1 × Fin 1 has a unique message pair, so the decoder is always correct and the average error probability is 0. @audit:ok

Transport a code's average error probability along a block-length equality.

Block concatenation of a length-n₁ code (user counts Ka₁, Ka₂) and a length-n₂ code (user counts Kb₁, Kb₂) into a length-n₁ + n₂ code with user counts Ka₁·Kb₁, Ka₂·Kb₂. User messages are paired via finProdFinEquiv, codewords are concatenated with Fin.append, and the joint decoder splits the received block at n₁ and decodes each half independently.

Pointwise error of the concatenated code is bounded by the union bound of the two block errors: the concatenated block law factors as a product over the split Fin (n₁ + n₂) ≃ Fin n₁ ⊕ Fin n₂, and the joint error event is contained in the union of the two block error cylinders.

Average error of the concatenated code is bounded by the sum of the two block averages. Averaging the pointwise union bound over all message pairs and factoring the product sum.

Time-sharing achievability of the convex hull, in strict-rate form: any rate pair strictly below a convex combination of two achievable rate pairs is itself achievable, realized operationally by concatenating a length-n₁ code (rate (a₁, a₂)) and a length-n₂ code (rate (b₁, b₂)) with n₁ = ⌊lam·n⌋. The strict gap R₁ < lam·a₁ + (1-lam)·b₁ absorbs the O(1)/n rounding of the block split; the exact-rate form, by contrast, is false at boundary points. This suffices to make macCapacityRegion convex via closure of the strict-interior achievable set.

A rate pair whose strictly-smaller (in both coordinates) perturbations are all achievable lies in the capacity region. The perturbed points (p.1 - ε, p.2 - ε) form a sequence in the achievable set converging to p, so p is in its closure. @audit:ok

The capacity region is closed (it is defined as a closure). @audit:ok

The capacity region is convex. Convexity of the closure follows from time-sharing: the segment between any two achievable points lies in the closure (via mac_timesharing_strict), and this lifts to closure points by a sequential limit. @audit:ok

Achievability on the single-user axis with user 1 silent: the rate pair (0, R₂) with R₂ < macInfo₂ is achievable. This is the R₁ = 0 specialization of the achievability engine: R₁ = 0 forces M₁ = ⌈exp (n·0)⌉ = 1, so the two alias terms carrying the (M₁ - 1) factor (E1, E3) collapse to 0 and only the correct-pair atypicality E0 (AEP) and the user-2 alias E2 (controlled by R₂ < macInfo₂) remain. The corner conditions R₁ < macInfo₁ and R₁ + R₂ < macInfoBoth of mac_achievability are therefore not needed; the first of them fails outright when macInfo₁ ≤ 0. @audit:ok

Achievability on the single-user axis with user 2 silent: the rate pair (R₁, 0) with R₁ < macInfo₁ is achievable. Symmetric to mac_rate₂_achievable: R₂ = 0 forces M₂ = 1, collapsing the (M₂ - 1)-carrying alias terms (E2, E3) and leaving only E0 (AEP) and the user-1 alias E1 (controlled by R₁ < macInfo₁). @audit:ok

Every rate pair of a full-support product input's pentagon lies in the capacity region. Strictly-interior points are directly achievable (mac_strict_interior_achievable); every other point is a limit of interior points via a convex combination toward an interior witness. @audit:ok

Time-sharing achievability for the MAC in convex-hull form (Cover–Thomas): the closed convex hull of the per-input pentagons of full-support product inputs is contained in the operational capacity region. @audit:ok

Every rate pair of an arbitrary probability product input's pentagon lies in the capacity region. The full-support case is mac_pentagon_subset_capacityRegion; the general case smooths the input toward the uniform anchor and passes to the limit.

Time-sharing achievability for the MAC in convex-hull form, over all probability inputs: the closed convex hull of the per-input pentagons of all probability product inputs is contained in the operational capacity region. Upgrades mac_achievability_region from full-support inputs.