Lemma 7 — $M$ and $\hat M$ are conditionally independent given $(Z^n,\mathbf F)$ under a degraded-form channel

Let $V:\mathcal X\to\mathcal Y\times\mathcal Z$ be a wiretap channel of the form $V(y,z|x)=V_2(z|x)V_1(y|z)$ for channels $V_2:\mathcal X\to\mathcal Z$ and $V_1:\mathcal Z\to\mathcal Y$. Fix a wiretap code with public feedback and a random message $M$ with any law $\mu$, let $\hat M=d(Y^n)$ and let $\mathbf F$ be the corresponding feedback. Then the induced law $Q_{M\hat MZ^n\mathbf F}$ satisfies the factorization condition

This is what makes the code's law under $V$ an admissible alternative hypothesis $Q$ in Theorem 5.

Formalization Note The factorization is stated without division: $Q(m,\hat m,z,f)\,Q_{Z^n\mathbf F}(z,f)=Q_{MZ^n\mathbf F}(m,z,f)\,Q_{\hat MZ^n\mathbf F}(\hat m,z,f)$ for all $m,\hat m,z,f$.

Differences from the source:

• reading: a random message M (law not specified; Theorem 6 uses the uniform law) → any message law μ on Fin N; reason: the lemma fixes no law and its proof uses none; the uniform case of Theorem 6 is an instance
• encoding: Q_{MM̂|Zⁿ𝐅} = Q_{M|Zⁿ𝐅} × Q_{M̂|Zⁿ𝐅} → Q(m,m̂,z,f)·Q_{Zⁿ𝐅}(z,f) = Q_{MZⁿ𝐅}(m,z,f)·Q_{M̂Zⁿ𝐅}(m̂,z,f); reason: equivalent where Q_{Zⁿ𝐅}(z,f) > 0 and automatic elsewhere
• encoding: a channel V with V(y,z|x) = V₂(z|x)V₁(y|z) → V with hypothesis ∀ x y z, V(y,z|x) = V₂(z|x)·V₁(y|z) for channels V₂, V₁; reason: Lean convention; the same channels
• encoding: (possibly randomized) encoder and feedback mappings, time index t = 1, …, n, messages {1, …, N} → deterministic maps of independent local randomness Ux, Uy of arbitrary type (paper's own representation, proof of Lemma 7), arbitrary feedback alphabet, 0-based rounds, Fin N; reason: Lean convention; the same class of codes
• generalization: discrete (finite) input alphabet X → any type X, with Y and Z finite; reason: neither the statement nor its proof forms a law on X or uses finiteness of X; every finite X is an instance