The finite shared-control circuit lower bound

Actual narrow and wide conjunction messages receive their separate information charges. A single averaged cut preserves a common triple fraction of both classes. The old affine count and the new shared-control count eliminate both gate classes.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.sender_le_size_of_refined_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 - Joint.overlapPenalty) * ↑U.card ≤ ↑c.size + 1 + Real.logb 2 ↑K - Joint.gateSaving * ↑(Joint.retainedTwo c.program U).card - wideSaving * ↑(Joint.retainedWide c.program U).card

The actual sending side receives separate narrow and wide message savings.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.input_le_size_of_triple_entropy {n a K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (ha : 3 ≤ 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 - Joint.overlapPenalty) * ↑a ≤ ↑c.size + 1 + Real.logb 2 ↑K - Joint.tripleRetention n a * (Joint.gateSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + wideSaving * ↑(Joint.retainedWide c.program Finset.univ).card)

One averaged cut retains the same triple fraction of both original gate classes.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.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 + 4 ≤ n) : (1 - Joint.overlapPenalty) * (↑n - ↑(Nat.clog 2 K) - 1) ≤ ↑c.size + 1 + Real.logb 2 ↑K - receiverRetention n (Nat.clog 2 K) * (Joint.gateSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + wideSaving * ↑(Joint.retainedWide c.program Finset.univ).card)

A logarithmic receiving side gives the finite refined information inequality.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Shared.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 + 4 ≤ n) : have k := Nat.clog 2 K; have a := receiverRetention n k; (1 - Joint.overlapPenalty) * (↑n - ↑k - 1) + a * (Joint.gateSaving / 2 + 3 * wideSaving / 2) * ↑n - 2 * a * wideSaving * ↑k - 1 - Real.logb 2 ↑K ≤ (1 + a * wideSaving) * ↑c.size

The unrestricted signed basis satisfies the shared-control finite lower bound.