Entropy savings from designated primary-input pairs #
Averaging selects a coordinate partition that retains many designated pairs. Each retained pair biases one bit of the actual one-way message. The small-fibre and weighted-counting bounds then yield an exact finite communication inequality.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Entropy.input_le_bits_of_pair_summaries
{n a K : ℕ}
{f : Cslib.BooleanFunction n}
(ha : 2 ≤ a)
(han : a ≤ n)
(hK : 0 < K)
(free : RectangleFree f K)
(freeNot : RectangleFree (fun (x : Cslib.BitString n) => !f x) K)
(large : 2 * K ≤ 2 ^ (n - a))
{ι : Type u_1}
{J : Type u_2}
[Fintype ι]
[Fintype J]
(embed : J ↪ ι)
(left right : J → Fin n)
(distinct : ∀ (j : J), left j ≠ right j)
(summaries : (U : Finset (Fin n)) → OneWaySummary f U (ι → Bool))
(rare : ι → Bool)
(bias :
∀ (U : Finset (Fin n)) (j : J),
left j ∈ U → right j ∈ U → 4 * {x : ↥U → Bool | (summaries U).key x (embed j) = rare (embed j)}.card ≤ 2 ^ U.card)
:
Pair averaging and exact message semantics imply the finite entropy inequality.