The finite joint-message circuit lower bound

Actual gate summaries receive a normalized joint weight. Retaining designated primary pairs and bounding all message fibres gives an information inequality, which combines with the existing paired affine restriction theorem.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.sender_le_size_of_joint_messages {n K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (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) (U : Finset (Fin n)) (large : 2 * K ≤ 2 ^ Uᶜ.card) : (1 - overlapPenalty) * ↑U.card ≤ ↑c.size + 1 + Real.logb 2 ↑K - gateSaving * ↑{i : Fin c.size | Aggregate.Geometry.SelectedPair (c.program.lines i) U}.card

Joint counting improves the information bound for the actual sending side.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.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)) : (1 - overlapPenalty) * ↑a ≤ ↑c.size + 1 + Real.logb 2 ↑K - gateSaving * (↑a * (↑a - 1) / (↑n * (↑n - 1)) * ↑(Aggregate.Geometry.multiCount c.program))

Averaging retains the joint saving from a fraction of all multiple-primary gates.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.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) : (1 - overlapPenalty) * (↑n - ↑(Nat.clog 2 K) - 1) ≤ ↑c.size + 1 + Real.logb 2 ↑K - gateSaving * (pairRetention n (Nat.clog 2 K) * ↑(Aggregate.Geometry.multiCount c.program))

The logarithmic receiving side gives the exact finite joint information inequality.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.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 := gateSaving * pairRetention n k; (1 - overlapPenalty + 2 * d) * ↑n - 2 * d * ↑k - (1 - overlapPenalty) * (↑k + 1) - 1 - Real.logb 2 ↑K ≤ (1 + d) * ↑c.size

The whole unbounded basis obeys the stronger finite pairing and joint-message bound.