Affine savings from shared primary controls

Gate-disjoint pairs of exact-two-primary conjunctions sharing a variable save one additional unit each in the affine codimension charge. A maximal pairing leaves at most half the input count unpaired. All statements concern actual circuits, with no restriction on fan-in, fanout, depth, literal repetitions, or internal inputs.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.exists_affine_restriction {n g : ℕ} (p : Program signature n g) (P : PrimaryPairing p) : ∃ (S : AffineFlat n) (d : ℕ), (∀ (i : Fin g), AffineOn S (p.gateFunction interpretation i)) ∧ 2 ^ d * S.carrier.card = 2 ^ n ∧ 2 * d + P.pairs.card ≤ g + multiCount p

Preprocessing shared primary controls improves the actual affine restriction charge by one unit per gate-disjoint intersecting pair.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.exists_monochromatic_affine {n g : ℕ} (p : Program signature n g) (P : PrimaryPairing p) (out : Wire n g) : ∃ (S : AffineFlat n) (d : ℕ), ConstantOn S (p.wireFunction interpretation out) ∧ 2 ^ d * S.carrier.card = 2 ^ n ∧ 2 * d + P.pairs.card ≤ g + multiCount p + 2

Fixing the final affine output costs at most one further equation.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.two_mul_input_add_pairs_le {n g : ℕ} (p : Program signature n g) (P : PrimaryPairing p) (out : Wire n g) {K : ℕ} (disperse : Cutwidth.FlatSumsetDisperser (p.wireFunction interpretation out) K) : 2 * n + P.pairs.card ≤ g + multiCount p + 2 * Nat.clog 2 K

A sumset disperser pays one extra affine-charge unit for each shared-control pair.

theorem Algebraic.Aggregate.Geometry.Shared.seven_mul_input_add_two_mul_exactTwo_le {n g : ℕ} (p : Program signature n g) (out : Wire n g) {K : ℕ} (disperse : Cutwidth.FlatSumsetDisperser (p.wireFunction interpretation out) K) : 7 * n + 2 * (exactTwo p).card ≤ 4 * g + 4 * multiCount p + 8 * Nat.clog 2 K

Eliminating the finite matching parameter gives a stronger geometric inequality in the actual total and exact-two-primary gate counts.