The finite pairing and entropy lower bound

The actual circuit messages have small fibres by dispersion. Averaging designated primary-input pairs exposes biased coordinates; the resulting entropy saving combines with the monochromatic affine restriction bound.

theorem Algebraic.Cutwidth.Aggregate.Geometry.input_le_size_of_pair_entropy {n a K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (ha : 2 ≤ a) (han : a ≤ n) (hK : 0 < K) (free : RectangleFree (c.outputFunction Aggregate.Geometry.interpretation 0) K) (freeNot : RectangleFree (fun (x : Cslib.BitString n) => !c.outputFunction Aggregate.Geometry.interpretation 0 x) K) (large : 2 * K ≤ 2 ^ (n - a)) : ↑n ≤ ↑c.size + 1 + ↑(n - a) + Real.logb 2 ↑K - ↑a * (↑a - 1) / (↑n * (↑n - 1)) * ↑(Aggregate.Geometry.multiCount c.program) * Entropy.bitSaving

The actual circuit's biased messages give an exact finite information bound.

theorem Algebraic.Cutwidth.Aggregate.Geometry.disperse_not {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : FlatSumsetDisperser f K) : FlatSumsetDisperser (fun (x : Cslib.BitString n) => !f x) K

Dispersion is preserved by complementing the output.

theorem Algebraic.Cutwidth.Aggregate.Geometry.input_le_size_of_entropy {n K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (hK : 0 < K) (disperse : FlatSumsetDisperser (c.outputFunction Aggregate.Geometry.interpretation 0) K) (range : Nat.clog 2 K + 3 ≤ n) : ↑n ≤ ↑c.size + 1 + ↑(Nat.clog 2 K + 1) + Real.logb 2 ↑K - pairRetention n (Nat.clog 2 K) * ↑(Aggregate.Geometry.multiCount c.program) * Entropy.bitSaving

The finite entropy inequality for the standard logarithmic receiving side.

theorem Algebraic.Cutwidth.Aggregate.Geometry.size_lowerBound_of_sumsetDisperser {n K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (hK : 0 < K) (disperse : FlatSumsetDisperser (c.outputFunction Aggregate.Geometry.interpretation 0) K) (range : Nat.clog 2 K + 3 ≤ n) : have k := Nat.clog 2 K; have d := Entropy.bitSaving * pairRetention n k; (1 + 2 * d) * ↑n - 2 * d * ↑k - ↑k - 2 - Real.logb 2 ↑K ≤ (1 + d) * ↑c.size

Affine pairing and biased gate messages give the stronger finite gate bound.