One-way summaries of rectangle-free functions

A one-way summary depends only on one side of an input partition. Equal summaries give equal function values for every assignment on the other side. Counting its row classes yields a nearly full-input lower bound on the number of summary bits when the other side has only logarithmically many coordinates.

structure Algebraic.Cutwidth.Aggregate.OneWaySummary {n : ℕ} (f : Cslib.BooleanFunction n) (U : Finset (Fin n)) (T : Type u_1) : Type u_1

A summary of the coordinates in U determines the function once the remaining coordinates are known. There is no communication from the other side.

• key : (↥U → Bool) → T

  The message computed from the sending party's coordinate assignment.

• rows_eq (p p' : ↥U → Bool) : self.key p = self.key p' → ∀ (q : ↥Uᶜ → Bool), f (glue U p q) = f (glue U p' q)

  Equal messages give identical output rows on the receiving coordinates.

theorem Algebraic.Cutwidth.Aggregate.card_accepting_le_of_oneWay {n K : ℕ} {f : Cslib.BooleanFunction n} (free : RectangleFree f K) (U : Finset (Fin n)) {T : Type u_1} [Fintype T] (summary : OneWaySummary f U T) : (accepting f).card ≤ Fintype.card T * (K - 1) * 2 ^ Uᶜ.card + 2 ^ U.card * (K - 1)

Rectangle freeness bounds both the large and the small accepting row classes of a deterministic one-way summary.

theorem Algebraic.Cutwidth.Aggregate.input_le_capacity_of_oneWay {n K B : ℕ} {f : Cslib.BooleanFunction n} (free : RectangleFree f K) (dense : 2 ^ (n - 2) ≤ (accepting f).card) (U : Finset (Fin n)) (right : Uᶜ.card = Nat.clog 2 K + 3) {T : Type u_1} [Fintype T] (summary : OneWaySummary f U T) (short : Fintype.card T ≤ 2 ^ B) : n ≤ B + 2 * Nat.clog 2 K + 5

A dense rectangle-free function needs almost n one-way summary bits if the receiver holds clog 2 K + 3 input coordinates.