Theorem 4: Shannon incompleteness at n = 4

Theorem 4 of [@zhangyeung1998, §II, eq. 26] is the scientific payoff of the Zhang-Yeung inequality: the Shannon outer bound Γ_n strictly contains the set of entropy functions of n discrete random variables for n ≥ 4. At n = 4 the witness is explicit (paper lines 368-377): a concrete rational-valued set function on the 16 subsets of Fin 4 that satisfies the three Shannon-cone axioms (paper eq. 11) but violates the Zhang-Yeung inequality (paper eq. 21) at the canonical labeling.

The milestone lands four ingredients:

• Parts (a), (b) -- pure set-function arithmetic. The witness FWitnessℚ : Finset (Fin 4) → ℚ satisfies shannonCone FWitness and fails zhangYeungHolds FWitness. Both are decidable finite checks.
• Part (c), the bridge -- for any four discrete random variables X : ∀ i : Fin 4, Ω → S i, possibly with different finite codomains S : Fin 4 → Type u, their entropy function entropyFn X μ : Finset (Fin 4) → ℝ satisfies zhangYeungHolds at every permutation of the four coordinates. This is a direct restatement of M3's ZhangYeung.zhangYeung in the set-function language the closure proof consumes.
• Part (d), the exact theorem -- the headline separation. The public theorem4 is now the paper's exact n = 4 closure statement ∃ F ∈ Γ_4, F ∉ closure(Γ_4^*), with theorem4_ge_four lifting it to all n ≥ 4.

Main definitions

• ZhangYeung.IF, ZhangYeung.condIF, ZhangYeung.deltaF: the set-function information-theoretic calculus (unconditional mutual info, conditional mutual info, and the Zhang-Yeung delta at the set-function level).
• ZhangYeung.shannonCone: the Shannon outer bound Γ_4 (paper eq. 11) stated as a predicate on Finset (Fin 4) → ℝ.
• ZhangYeung.shannonRegionN, ZhangYeung.entropyRegionN, ZhangYeung.almostEntropicRegionN: the set-level Shannon, entropic, and almost-entropic regions on Finset (Fin n) → ℝ.
• ZhangYeung.zhangYeungAt: the Zhang-Yeung inequality (paper eq. 21) at a specific 4-tuple labeling.
• ZhangYeung.zhangYeungHolds: the Zhang-Yeung cone tildeΓ_4 (paper eq. 25), expressed as zhangYeungAt at every permutation of Fin 4.
• ZhangYeung.FWitnessℚ: the paper's n = 4 counterexample, as a ℚ-valued set function with a = 1.
• ZhangYeung.FWitness: the ℝ-cast of FWitnessℚ.
• ZhangYeung.entropyFn, ZhangYeung.entropyFnN: the four-variable and generic set-function views of joint entropy.

Main statements

• ZhangYeung.shannonCone_of_witness -- Part (a): FWitness lies in the Shannon cone.
• ZhangYeung.not_zhangYeungHolds_witness -- Part (b): FWitness fails the Zhang-Yeung inequality at the canonical permutation.
• ZhangYeung.shannon_incomplete -- intermediate form: there exists a set function in Γ_4 that is not in tildeΓ_4.
• ZhangYeung.zhangYeungAt_entropyFn, ZhangYeung.zhangYeungHolds_of_entropy -- Part (c), the bridge: every entropy function of four discrete random variables lies in tildeΓ_4.
• ZhangYeung.theorem4_finite -- the finite auxiliary separation, excluding FWitness from the literal entropy region.
• ZhangYeung.theorem4 -- the exact paper-level n = 4 statement ∃ F ∈ Γ_4, F ∉ closure(Γ_4^*).
• ZhangYeung.theorem4_ge_four -- the exact paper-level n ≥ 4 statement ∃ F ∈ Γ_n, F ∉ closure(Γ_n^*).
• ZhangYeung.theorem4_seqClosure -- the sequence-level surrogate over tildeΓ_4 retained as a supporting lemma.
• ZhangYeung.shannon_incomplete_ge_four -- the stronger cone-level corollary ∃ F ∈ Γ_n, F ∉ tildeΓ_n.

Implementation notes

The witness is defined first over ℚ so that Parts (a) and (b) reduce to finite rational arithmetic before casting to ℝ at the witness boundary. FWitness is a plain pointwise cast fun S => (FWitnessℚ S : ℝ); the companion lemma FWitness_eq_cast trivializes downstream push_cast/norm_cast work. Fixing a = 1 collapses the paper's parametric family into a single ℚ-valued function without losing any content: theorem4 and theorem4_ge_four are existential separations, so the homogeneity the paper uses a to exhibit is vacuous at that level.

The Zhang-Yeung cone is quantified over Equiv.Perm (Fin 4) to match paper eq. (25) literally; the specific violation uses the permutation Equiv.swap 0 2 * Equiv.swap 1 3 sending (0, 1, 2, 3) ↦ (2, 3, 0, 1), which instantiates zhangYeungAt F (σ 0) (σ 1) (σ 2) (σ 3) as zhangYeungAt F 2 3 0 1 -- exactly the labeling the paper evaluates on lines 378-388. Permutation evaluation (σ 0, σ 1, σ 2, σ 3) is discharged by decide once and reused.

The bridge binds the four codomains as a heterogeneous family S : Fin 4 → Type u at a single universe u and consumes M3's ZhangYeung.zhangYeung directly. Each per-subset bridge lemma (entropyFn_empty, entropyFn_singleton, entropyFn_pair, entropyFn_triple, entropyFn_quad) transports across an explicit Equiv between a Finset-indexed subtype of Fin 4 and a standard Fin k, invoking PFR's entropy_comp_of_injective to move H[·; μ] under that transport. The exact theorem then packages this bridge through ZhangYeung/EntropyRegion.lean: closure (Γ_4^*) sits inside the closed Zhang-Yeung region, while FWitness sits outside it.

References

• [@zhangyeung1998, §II, Theorem 4 and its proof, lines 358-388] -- statement, witness construction, and Zhang-Yeung violation verification.
• [@zhangyeung1998, §II, definition of tildeΓ_4 at eq. (25), lines 339-355] -- the Zhang-Yeung cone.
• [@zhangyeung1998, §II, Shannon cone Γ_n at eq. (11)] -- the three Shannon-cone axioms.

Tags

Shannon entropy, non-Shannon information inequality, Zhang-Yeung, Shannon incompleteness, entropic region

Set-function information-theoretic calculus

Paper eqs. (3)-(5), restated at the set-function level on Finset (Fin 4) → ℝ. These mirror the random-variable-level information measures PFR exposes (I[X : Y], I[X : Y | Z]) but do not require any measure-theoretic context.

def ZhangYeung.IF (F : Finset (Fin 4) → ℝ) (α β : Finset (Fin 4)) : ℝ

Set-function mutual information: IF(α; β) = F α + F β - F (α ∪ β). When F is the entropy function of a discrete random-variable family (with F ∅ = 0), this coincides with I[X_α : X_β].

Equations

• ZhangYeung.IF F α β = F α + F β - F (α ∪ β)

def ZhangYeung.condIF (F : Finset (Fin 4) → ℝ) (α β γ : Finset (Fin 4)) : ℝ

Set-function conditional mutual information: `condIF(α; β | γ) = F (α ∪ γ) + F (β ∪ γ)

• F (α ∪ β ∪ γ) - F γ. When Fis the entropy function of a discrete random-variable family, this coincides withI[X_α : X_β | X_γ]`.

Equations

• ZhangYeung.condIF F α β γ = F (α ∪ γ) + F (β ∪ γ) - F (α ∪ β ∪ γ) - F γ

def ZhangYeung.deltaF (F : Finset (Fin 4) → ℝ) (i j k l : Fin 4) : ℝ

Set-function Zhang-Yeung delta at a 4-tuple of coordinates: deltaF(i, j | k, l) = IF({i}; {j}) - condIF({i}; {j} | {k}) - condIF({i}; {j} | {l}). Mirrors ZhangYeung.delta at the set-function level.

Equations

• ZhangYeung.deltaF F i j k l = ZhangYeung.IF F {i} {j} - ZhangYeung.condIF F {i} {j} {k} - ZhangYeung.condIF F {i} {j} {l}

Shannon and Zhang-Yeung cone predicates

def ZhangYeung.shannonCone (F : Finset (Fin 4) → ℝ) : Prop

The Shannon outer bound Γ_4 from [@zhangyeung1998, eq. 11]: a set function lies in Γ_4 iff it vanishes on the empty set, is monotone under subset inclusion, and is submodular.

Equations

• ZhangYeung.shannonCone F = (F ∅ = 0 ∧ (∀ (α β : Finset (Fin 4)), α ⊆ β → F α ≤ F β) ∧ ∀ (α β : Finset (Fin 4)), F (α ∪ β) + F (α ∩ β) ≤ F α + F β)

def ZhangYeung.zhangYeungAt (F : Finset (Fin 4) → ℝ) (i j k l : Fin 4) : Prop

The Zhang-Yeung inequality at a specific 4-tuple labeling (paper eq. 21):

deltaF F i j k l ≤ (1/2) * (IF F {k} {l} + IF F {k} ({i} ∪ {j}) + condIF F {i} {j} {k} - condIF F {i} {j} {l}).

This is the set-function-level restatement of ZhangYeung.zhangYeung.

Equations

• One or more equations did not get rendered due to their size.

def ZhangYeung.zhangYeungHolds (F : Finset (Fin 4) → ℝ) : Prop

The Zhang-Yeung cone tildeΓ_4 from [@zhangyeung1998, eq. 25]: a set function F lies in tildeΓ_4 iff zhangYeungAt F (π 0) (π 1) (π 2) (π 3) holds at every permutation π of Fin 4.

Equations

• ZhangYeung.zhangYeungHolds F = ∀ (π : Equiv.Perm (Fin 4)), ZhangYeung.zhangYeungAt F (π 0) (π 1) (π 2) (π 3)

The paper's n = 4 counterexample witness

The witness FWitnessℚ is the a = 1 specialization of the parametric witness on paper lines 368-377: zero on the empty set, 2 on singletons, 4 on {0, 1}, 3 on the other five pairs, and 4 on all triples and the 4-set. It is implemented as a cascade of if-then-else on cardinality, with a special case for {0, 1}, so the finite witness checks stay explicit and reducible on all 16 subsets of Fin 4.

def ZhangYeung.FWitnessℚ : Finset (Fin 4) → ℚ

The ℚ-valued Zhang-Yeung counterexample witness (paper lines 368-377, specialized to a = 1):

FWitnessℚ ∅ = 0, FWitnessℚ {i} = 2, FWitnessℚ {0, 1} = 4, FWitnessℚ {i, j} = 3 for other pairs, FWitnessℚ S = 4 for triples and the 4-set.

Living over ℚ so the witness arithmetic stays exact before the final cast to ℝ.

Equations

• ZhangYeung.FWitnessℚ S = if S.card = 0 then 0 else if S.card = 1 then 2 else if S = {0, 1} then 4 else if S.card = 2 then 3 else 4

noncomputable def ZhangYeung.FWitness : Finset (Fin 4) → ℝ

The ℝ-cast of FWitnessℚ, used in the main statements shannonCone_of_witness, not_zhangYeungHolds_witness, shannon_incomplete, theorem4_finite, theorem4, and theorem4_ge_four.

Equations

• ZhangYeung.FWitness S = ↑(ZhangYeung.FWitnessℚ S)

theorem ZhangYeung.FWitness_eq_cast (S : Finset (Fin 4)) : FWitness S = ↑(FWitnessℚ S)

Definitional-shape lemma: FWitness is the pointwise ℚ → ℝ cast of FWitnessℚ. Used to push FWitness into FWitnessℚ-shaped goals before closing them over ℚ.

Part (a): the witness lies in the Shannon cone

theorem ZhangYeung.shannonCone_of_witness : shannonCone FWitness

Part (a) of Theorem 4: the witness satisfies the three Shannon-cone axioms (paper eq. 11). The empty-set and monotonicity checks close by finite decide over the ℚ-valued witness, while submodularity is proved structurally by decomposing the witness into a cardinality profile plus one exceptional pair bonus.

Part (b): the witness violates the Zhang-Yeung inequality

theorem ZhangYeung.not_zhangYeungHolds_witness : ¬zhangYeungHolds FWitness

Part (b) of Theorem 4: the witness fails the Zhang-Yeung inequality at the canonical labeling (i, j, k, l) = (2, 3, 0, 1) (paper lines 378-388). The permutation exhibiting the violation is σ = Equiv.swap 0 2 * Equiv.swap 1 3; after permutation evaluation the obligation is the canonical failure not_zhangYeungAt_witness_canonical.

theorem ZhangYeung.shannon_incomplete : ∃ (F : Finset (Fin 4) → ℝ), shannonCone F ∧ ¬zhangYeungHolds F

Intermediate conclusion (pre-bridge): the Shannon cone strictly contains the Zhang-Yeung cone, Γ_4 ⊋ tildeΓ_4. Part (a) and Part (b) combined. This remains a useful stronger auxiliary: theorem4_finite strengthens it to exclusion from the literal entropy region, while theorem4 packages the exact closure statement from the paper.

Part (c): the bridge from the random-variable form (M3) to the set-function form

theorem ZhangYeung.entropyFn_empty {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] (X : (i : Fin 4) → Ω → S i) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : entropyFn X μ ∅ = 0

Per-subset bridge lemma at the empty subset: entropyFn X μ ∅ = 0. The subtype {j // j ∈ (∅ : Finset (Fin 4))} is empty, so the dependent-product codomain ∀ j : ∅, S j.1 is a subsingleton; the joint tuple is constant, and its entropy is zero.

theorem ZhangYeung.entropyFn_singleton {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), Finite (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] (X : (i : Fin 4) → Ω → S i) (μ : MeasureTheory.Measure Ω) (hX : ∀ (i : Fin 4), Measurable (X i)) (i : Fin 4) : entropyFn X μ {i} = H[X i; μ]

Per-subset bridge lemma at a singleton subset: entropyFn X μ {i} = H[X i; μ]. The joint tuple over the single-element subset {i} is, up to a measurable bijection into S i, just X i.

theorem ZhangYeung.entropyFn_pair {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), Finite (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] (X : (i : Fin 4) → Ω → S i) (μ : MeasureTheory.Measure Ω) (hX : ∀ (i : Fin 4), Measurable (X i)) {i j : Fin 4} (h : i ≠ j) : entropyFn X μ {i, j} = H[prod (X i) (X j); μ]

Per-subset bridge lemma at a two-element subset: entropyFn X μ {i, j} = H[⟨X i, X j⟩; μ] for i ≠ j. The joint tuple over {i, j} is measurably bijective with the pair (X i, X j).

theorem ZhangYeung.entropyFn_triple {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), Finite (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] (X : (i : Fin 4) → Ω → S i) (μ : MeasureTheory.Measure Ω) (hX : ∀ (i : Fin 4), Measurable (X i)) {i j k : Fin 4} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) : entropyFn X μ {i, j, k} = H[prod (X i) (prod (X j) (X k)); μ]

Per-subset bridge lemma at a three-element subset: entropyFn X μ {i, j, k} = H[⟨X i, ⟨X j, X k⟩⟩; μ] for pairwise distinct i, j, k. The joint tuple over {i, j, k} is measurably bijective with the triple (X i, (X j, X k)).

theorem ZhangYeung.entropyFn_quad {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), Finite (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] (X : (i : Fin 4) → Ω → S i) (μ : MeasureTheory.Measure Ω) (hX : ∀ (i : Fin 4), Measurable (X i)) : entropyFn X μ {0, 1, 2, 3} = H[prod (X 0) (prod (X 1) (prod (X 2) (X 3))); μ]

Per-subset bridge lemma at the full four-element subset: entropyFn X μ {0, 1, 2, 3} = H[⟨X 0, ⟨X 1, ⟨X 2, X 3⟩⟩⟩; μ]. The joint tuple over the full index set is measurably bijective with the right-associated 4-tuple.

theorem ZhangYeung.zhangYeungAt_entropyFn {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), Finite (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] {X : (i : Fin 4) → Ω → S i} (hX : ∀ (i : Fin 4), Measurable (X i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (π : Equiv.Perm (Fin 4)) : zhangYeungAt (entropyFn X μ) (π 0) (π 1) (π 2) (π 3)

The permutation-indexed bridge: at any permutation π of Fin 4, the entropy function satisfies the Zhang-Yeung inequality (paper eq. 21) at the labeling (π 0, π 1, π 2, π 3). Proved by unfolding zhangYeungAt, rewriting each entropyFn evaluation into a joint entropy via the per-subset bridge lemmas, and matching the resulting inequality against M3's ZhangYeung.zhangYeung applied to (X (π 0), X (π 1), X (π 2), X (π 3)).

theorem ZhangYeung.zhangYeungHolds_of_entropy {Ω : Type u_1} [MeasurableSpace Ω] {S : Fin 4 → Type u} [(i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), Finite (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] {X : (i : Fin 4) → Ω → S i} (hX : ∀ (i : Fin 4), Measurable (X i)) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : zhangYeungHolds (entropyFn X μ)

Part (c), the full bridge: the entropy function of any four-variable random-variable family lies in tildeΓ_4. One-line wrapper around zhangYeungAt_entropyFn.

Part (d): Theorem 4

theorem ZhangYeung.theorem4_finite : ∃ (F : Finset (Fin 4) → ℝ), shannonCone F ∧ ∀ {Ω : Type u} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {S : Fin 4 → Type u} [inst_2 : (i : Fin 4) → MeasurableSpace (S i)] [∀ (i : Fin 4), Finite (S i)] [∀ (i : Fin 4), MeasurableSingletonClass (S i)] (X : (i : Fin 4) → Ω → S i), (∀ (i : Fin 4), Measurable (X i)) → F ≠ entropyFn X μ

Finite auxiliary form of Theorem 4 at n = 4: the witness lies in Γ_4 but is not the entropy function of any single four-variable discrete family. The exact paper-level closure statement is the later theorem theorem4.

Closure form

Each inequality zhangYeungAt F (π 0) (π 1) (π 2) (π 3) is a finite linear inequality among the coordinate evaluations F α, hence defines a closed subset of Finset (Fin 4) → ℝ in the pointwise topology. Their intersection is the closed Zhang-Yeung region tildeΓ_4. Since every four-variable entropy function lies in tildeΓ_4 by zhangYeungHolds_of_entropy, the almost-entropic region closure (Γ_4^*) lies there as well, while the explicit witness does not. This yields the exact paper-level theorem theorem4. The sequence-level surrogate is retained separately as theorem4_seqClosure.

theorem ZhangYeung.zhangYeungHolds_of_tendsto {F_seq : ℕ → Finset (Fin 4) → ℝ} {F : Finset (Fin 4) → ℝ} (h_seq : ∀ (k : ℕ), zhangYeungHolds (F_seq k)) (h_lim : ∀ (α : Finset (Fin 4)), Filter.Tendsto (fun (k : ℕ) => F_seq k α) Filter.atTop (nhds (F α))) : zhangYeungHolds F

zhangYeungHolds is closed under pointwise convergence: if each F_seq k lies in tildeΓ_4 and F_seq k α → F α pointwise, then F lies in tildeΓ_4 too. The inequality zhangYeungAt F is a finite ≤ between continuous linear combinations of coordinate evaluations, hence preserved under pointwise limits.

theorem ZhangYeung.theorem4 : ∃ F ∈ shannonRegionN 4, F ∉ almostEntropicRegionN 4

Theorem 4 of [@zhangyeung1998, §II, eq. 26] at n = 4. The Shannon outer bound Γ_4 strictly contains the closure of the entropic region: there exists a set function in Γ_4 that is not almost entropic. The non-membership claim is universe-polymorphic: for every universe u, FWitness ∉ almostEntropicRegionN.{u} 4, since the closedness argument in zhangYeungRegion_4 lives entirely at the level of Finset (Fin 4) → ℝ.

theorem ZhangYeung.theorem4_seqClosure : ∃ (F : Finset (Fin 4) → ℝ), shannonCone F ∧ ∀ (F_seq : ℕ → Finset (Fin 4) → ℝ), (∀ (k : ℕ), zhangYeungHolds (F_seq k)) → (∀ (α : Finset (Fin 4)), Filter.Tendsto (fun (k : ℕ) => F_seq k α) Filter.atTop (nhds (F α))) → False

Sequence-level strengthening of the witness exclusion: FWitness is not the pointwise limit of any sequence of set functions in tildeΓ_4. This auxiliary is stronger than theorem4, but it is phrased in the larger Zhang-Yeung cone rather than in closure (Γ_4^*).

n ≥ 4 extension

The witness FWitnessN is the lift of FWitness along the canonical embedding Fin 4 ↪ Fin n via Finset.preimage. It still lies in the Shannon cone and still violates the Zhang-Yeung inequality at the lifted canonical labeling (Fin.castLE hn 2, Fin.castLE hn 3, Fin.castLE hn 0, Fin.castLE hn 1). The exact paper-level n ≥ 4 theorem then follows by restricting any hypothetical almost-entropic realization back down to the first four coordinates. The generic cone predicates zhangYeungAtN and zhangYeungHoldsN consumed below live in ZhangYeung.EntropyRegion.

noncomputable def ZhangYeung.FWitnessN {n : ℕ} (hn : 4 ≤ n) (α : Finset (Fin n)) : ℝ

The n = 4 witness lifted to Fin n for n ≥ 4: FWitnessN hn α evaluates FWitness on the preimage of α under the canonical embedding Fin 4 ↪ Fin n. Equivalent to FWitness applied to the intersection of α with the initial segment {0, 1, 2, 3 : Fin n}.

Equations

• ZhangYeung.FWitnessN hn α = ZhangYeung.FWitness (α.preimage (Fin.castLE hn) ⋯)

theorem ZhangYeung.shannonCone_of_witness_n {n : ℕ} (hn : 4 ≤ n) : shannonConeN (FWitnessN hn)

The lifted witness lies in Γ_n: each Shannon-cone axiom transports across Finset.preimage via preimage_empty, monotone_preimage, preimage_union, and preimage_inter, and then reduces to the base shannonCone_of_witness.

theorem ZhangYeung.restrictFirstFour_witness_n {n : ℕ} (hn : 4 ≤ n) : restrictFirstFour hn (FWitnessN hn) = FWitness

Restricting the lifted witness back to the first four coordinates recovers the base witness.

theorem ZhangYeung.not_zhangYeungHolds_witness_n {n : ℕ} (hn : 4 ≤ n) : ¬zhangYeungHoldsN (FWitnessN hn)

Part (b) lifted to Fin n: the lifted witness fails zhangYeungHoldsN at the lifted canonical labeling.

theorem ZhangYeung.shannon_incomplete_ge_four (n : ℕ) (hn : 4 ≤ n) : ∃ (F : Finset (Fin n) → ℝ), shannonConeN F ∧ ¬zhangYeungHoldsN F

Stronger cone-level corollary for n ≥ 4: the lifted witness separates Γ_n from the Fin n-indexed Zhang-Yeung cone. Since closure (Γ_n^*) ⊆ tildeΓ_n, this strictly strengthens the exact paper-level theorem theorem4_ge_four.

theorem ZhangYeung.theorem4_ge_four (n : ℕ) (hn : 4 ≤ n) : ∃ F ∈ shannonRegionN n, F ∉ almostEntropicRegionN n

Theorem 4 of [@zhangyeung1998, §II, eq. 26] for all n ≥ 4. The Shannon outer bound Γ_n strictly contains the closure of the entropic region: there exists a set function in Γ_n that is not almost entropic. The non-membership claim is universe-polymorphic: for every universe u, FWitnessN hn ∉ almostEntropicRegionN.{u} n, by restricting any hypothetical almost-entropic realization back down to the first four coordinates and applying the n = 4 exclusion.