LeanPool.ZhangYeungInequality.Test.Theorem4 #
Imported Lean Pool material for LeanPool.ZhangYeungInequality.Test.Theorem4.
Signature pins for the set-function calculus and cone predicates #
Witness signature pins #
Main statement pins #
Concrete evaluation of the ℚ-valued witness #
The witness values at the 16 subsets of Fin 4, as a compile-time regression
against accidental edits to FWitnessℚ. Each value follows the paper's
table on lines 368-377 at a = 1.
Downstream usage #
shannon_incomplete composes Parts (a) and (b) into a single existential;
theorem4_finite pins the literal non-entropic witness theorem; theorem4
pins the exact closure statement from the paper.