Pairing conjunction gates with overlapping primary supports

Among actual conjunction gates with exactly two distinct direct primary inputs, one can choose gate-disjoint intersecting pairs leaving at most n / 2 gates. This is a finite graph matching argument; no circuit semantic hypothesis is used.

theorem Algebraic.Aggregate.Geometry.Shared.exists_pairing_le_half {n g : ℕ} (p : Program signature n g) : ∃ (P : PrimaryPairing p), (exactTwo p).card ≤ 2 * P.pairs.card + n / 2

Pair exact-two conjunctions so at most half the input count remains unpaired.

theorem Algebraic.Aggregate.Geometry.Shared.exists_pairing_two_mul_le {n g : ℕ} (p : Program signature n g) : ∃ (P : PrimaryPairing p), 2 * (exactTwo p).card ≤ 4 * P.pairs.card + n

A denominator-free version of the maximal pairing bound.