Small fibres of two-sided rectangle-free messages #
If the receiving side has at least 2K assignments, every message fibre has fewer
than K assignments: one of the two colors appears in at least K columns.
theorem
Algebraic.Cutwidth.Aggregate.Geometry.Entropy.card_fibre_lt_of_rectangleFree_both
{n K : ℕ}
{f : Cslib.BooleanFunction n}
(hK : 0 < K)
(free : RectangleFree f K)
(freeNot : RectangleFree (fun (x : Cslib.BitString n) => !f x) K)
(U : Finset (Fin n))
(large : 2 * K ≤ 2 ^ Uᶜ.card)
{T : Type u_1}
(summary : OneWaySummary f U T)
(message : T)
:
Two-sided rectangle freeness bounds every fibre of an exact one-way message.