Convex-geometry gateway for the MAC time-sharing converse. If a rate pair (R₁, R₂) is bounded coordinate-wise by the time averages (∑ a)/n, (∑ b)/n and, jointly, (∑ c)/n of a family of per-letter pentagons Pᵢ = {(x,y) | 0 ≤ x ≤ aᵢ, 0 ≤ y ≤ bᵢ, x + y ≤ cᵢ}, then (R₁, R₂) lies in the convex hull of ⋃ i, Pᵢ. Requires both single-user bounds a i ≤ c i and b i ≤ c i (see the module note).

Pentagon well-formedness (user 1): macInfo₁ ≤ macInfoBoth, i.e. I(X₁; (X₂, Y)) ≤ I((X₁, X₂); Y). Supplies the a i ≤ c i hypothesis of mac_avgPentagon_mem_convexHull. Proved by the chain rule I((X₂, X₁); Y) = I(X₂; Y) + I(X₁; Y | X₂) (after prodComm) and condMutualInfo_nonneg.

Pentagon well-formedness (user 2): macInfo₂ ≤ macInfoBoth, i.e. I(X₂; (X₁, Y)) ≤ I((X₁, X₂); Y). Supplies the b i ≤ c i hypothesis of mac_avgPentagon_mem_convexHull. Proved by the chain rule I((X₁, X₂); Y) = I(X₁; Y) + I(X₂; Y | X₁) and condMutualInfo_nonneg.

Uniform input law on the message pair: the product of the two uniform message laws.

Per-letter product-channel kernel: given the message pair m, the output law is the product over the n letters of the channel W applied to the encoded pair (encoder₁ m₁ i, encoder₂ m₂ i). The channel input is deterministic in the messages (through the encoders).

Canonical ambient measure for the MAC converse: a uniform message pair passed through the per-letter product channel.

Message-1 projection ω ↦ ω.1.1.

Message-2 projection ω ↦ ω.1.2.

Output projection i ↦ ω ↦ ω.2 i.

The map ω ↦ (Msg₁ ω, Msg₂ ω) is the outer first projection Prod.fst on the ambient.

Codeword → output block kernel: given an encoded input-pair codeword x = (x₁, x₂), the output law is the per-letter product ∏ᵢ W (x₁ i, x₂ i) of the MAC channel.

Memoryless-channel property of the constructed ambient: the per-letter output is conditionally independent of the other letters given the current input pair. @audit:ok

The two messages are independent under the constructed ambient (uniform product input law), hence their mutual information vanishes. @audit:ok

Markov chain (messages) → (encoded inputs) → (outputs) for the constructed ambient. @audit:ok

The MAC converse instantiated at a bare code: for any two-user MAC block code c and Markov channel W, the canonical ambient measure macConverseAmbient c W discharges every hypothesis of the floating converse mac_converse, so the rate pair (log M₁, log M₂) lies in the corner-point region determined by the per-letter conditional and joint mutual informations. The Fano slack is still carried here; it vanishes only in the n → ∞ limit. @audit:ok

Finite-n rate extraction for the weak converse: for a fixed two-user block code whose message counts satisfy ⌈exp (n R₁)⌉ ≤ M₁, ⌈exp (n R₂)⌉ ≤ M₂, chaining the code→ambient converse mac_converse_from_code with n Rⱼ ≤ log Mⱼ moves the rate scaled by n inside the corner-point region determined by the per-letter conditional/joint mutual informations plus the Fano slack. The slack is still symbolic here; the Fano → 0 limit is taken in mac_timesharing_converse.

The ambient joint decode error under macConverseAmbient c W equals the code's average error probability: the ambient was built as uniform(messages) ⊗ per-letter product channel precisely to model uniform-message transmission, so its joint error event has probability averageErrorProb.

The ambient user-1 marginal decode error is at most the joint decode error: the event {msg₁ mis-decoded} is contained in {message pair mis-decoded}.

The ambient user-2 marginal decode error is at most the joint decode error.

Per-letter joint law identification: under the converse ambient macConverseAmbient c W, the joint law of the i-th per-letter triple (X₁ᵢ, X₂ᵢ, Yᵢ) equals the achievability per-coordinate joint macJointDistribution p₁ᵢ p₂ᵢ W of the product of the per-letter input marginals p₁ᵢ = μ.map X₁ᵢ, p₂ᵢ = μ.map X₂ᵢ. The two inputs are independent (functions of the independent uniform messages), and the output is conditionally W-distributed by the per-letter product-channel structure.

Per-letter identification of the user-1 corner information: the ambient per-letter conditional mutual information I(X₁ᵢ; Yᵢ | X₂ᵢ) equals the achievability corner information macInfo₁ of the per-letter product input. This rewrites the user-1 sum term of mac_converse_rate_extract into ∑ᵢ macInfo₁ p₁ᵢ p₂ᵢ W.

Per-letter identification of the user-2 corner information: the ambient per-letter conditional mutual information I(X₂ᵢ; Yᵢ | X₁ᵢ) equals macInfo₂ of the per-letter product input.

Per-letter identification of the sum-corner information: the ambient per-letter joint mutual information I((X₁ᵢ, X₂ᵢ); Yᵢ) equals macInfoBoth of the per-letter product input.