Maximal pairing of exact-two conjunction gates

A maximum-cardinality pairing leaves gates whose two-element primary supports are pairwise disjoint. Counting those supports bounds the unmatched remainder.

theorem Algebraic.Aggregate.Geometry.Shared.mem_exactTwo {n g : ℕ} {p : Program signature n g} {i : Fin g} : i ∈ exactTwo p ↔ Op.isConjunction (p.lines i).op = true ∧ (primaryInputs (p.lines i)).card = 2

Membership gives the conjunction form and exact primary cardinality.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.used_subset {n g : ℕ} {p : Program signature n g} (P : PrimaryPairing p) : P.used ⊆ exactTwo p

Every paired gate belongs to the exact-two family.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.card_used {n g : ℕ} {p : Program signature n g} (P : PrimaryPairing p) : P.used.card = 2 * P.pairs.card

Pairwise disjoint endpoints count exactly twice the number of pairs.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.not_mem_used {n g : ℕ} {p : Program signature n g} (P : PrimaryPairing p) {i : Fin g} (hi : i ∈ P.remaining) : i ∉ P.used

A remaining gate is not an endpoint of a selected pair.

theorem Algebraic.Aggregate.Geometry.Shared.exists_pairing_disjoint_remaining {n g : ℕ} (p : Program signature n g) : ∃ (P : PrimaryPairing p), (↑P.remaining).Pairwise fun (i j : Fin g) => Disjoint (primaryInputs (p.lines i)) (primaryInputs (p.lines j))

A pairing with disjoint remaining primary supports always exists.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.card_remaining_le {n g : ℕ} {p : Program signature n g} (P : PrimaryPairing p) (disjoint : (↑P.remaining).Pairwise fun (i j : Fin g) => Disjoint (primaryInputs (p.lines i)) (primaryInputs (p.lines j))) : P.remaining.card ≤ n / 2

Disjoint two-element supports leave at most half as many gates as inputs.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.card_exactTwo {n g : ℕ} {p : Program signature n g} (P : PrimaryPairing p) : (exactTwo p).card = 2 * P.pairs.card + P.remaining.card

The exact-two count splits into twice the pair count and the remainder.