Counting the conjunction marks removed by shared controls

Fixing a shared variable removes both endpoints of a selected exact-two pair from the remaining-primary count. The other remaining marks form a subset of the original multiple-primary marks.

theorem Algebraic.Aggregate.Geometry.Shared.remainingCount_eq_card_filter {n g : ℕ} (p : Program signature n g) (fixed : Finset (Fin n)) : remainingCount p fixed = {gate : Fin g | remainingMark (p.lines gate) fixed = true}.card

The recursive remaining count is the cardinality of its actual gate-index set.

theorem Algebraic.Aggregate.Geometry.Shared.multiPrimary_of_remainingMark {n g : ℕ} (line : Line signature n g) (fixed : Finset (Fin n)) (remaining : remainingMark line fixed = true) : multiPrimary line = true

A mark surviving coordinate fixing was already an original multiple-primary mark.

theorem Algebraic.Aggregate.Geometry.Shared.remainingMark_eq_false_of_exactTwo {n g : ℕ} (line : Line signature n g) (fixed : Finset (Fin n)) (two : (primaryInputs line).card = 2) (hit : ∃ j ∈ primaryInputs line, j ∈ fixed) : remainingMark line fixed = false

Fixing any one variable of an exact-two support leaves at most one variable.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.remainingCount_add_le {n g : ℕ} (p : Program signature n g) (P : PrimaryPairing p) (fixed : Finset (Fin n)) (hit : ∀ e ∈ P.pairs, ∃ j ∈ primaryInputs (p.lines e.1), j ∈ primaryInputs (p.lines e.2) ∧ j ∈ fixed) : remainingCount p fixed + 2 * P.pairs.card ≤ multiCount p

Removing every selected pair's common coordinate saves two original marks per pair.