Retaining multiple-primary conjunction messages

Designate two primary inputs at each marked gate and apply exact pair averaging. The actual selected-pair predicate may hold at additional gates, so its count is at least the designated-pair score.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Joint.exists_subset_selectedPair_ratio {n g a : ℕ} (p : Program Aggregate.Geometry.signature n g) (ha : 2 ≤ a) (han : a ≤ n) : ∃ (U : Finset (Fin n)), U.card = a ∧ ↑a * (↑a - 1) / (↑n * (↑n - 1)) * ↑(Aggregate.Geometry.multiCount p) ≤ ↑{i : Fin g | Aggregate.Geometry.SelectedPair (p.lines i) U}.card

A sending side retains the expected fraction of the circuit's marked gates.