Fixing shared primary controls

Each selected pair contributes a common primary coordinate. Fixing that coordinate makes both primary supports unary and forces one entire gate output. Gate-disjoint pairs provide distinct constant-output witnesses for the independent equations.

theorem Algebraic.Aggregate.Geometry.Shared.lineFunction_lines {n g : ℕ} (p : Program signature n g) (i : Fin g) : lineFunction p (p.lines i) = p.gateFunction interpretation i

The widened actual line computes precisely its indexed gate output.

theorem Algebraic.Aggregate.Geometry.Shared.exists_controlling_value {n g : ℕ} (p : Program signature n g) (line : Line signature n g) (conjunction : Op.isConjunction line.op = true) (j : Fin n) (primary : j ∈ primaryInputs line) : ∃ (b : Bool), ∀ (S : AffineFlat n), (∀ x ∈ S.carrier, x j = b) → ConstantOn S (lineFunction p line)

Every primary literal of a conjunction has a value forcing the whole line.

theorem Algebraic.Aggregate.Geometry.Shared.card_le_constantCount {n g : ℕ} (p : Program signature n g) (S : AffineFlat n) (killed : Finset (Fin g)) (constant : ∀ i ∈ killed, ConstantOn S (p.gateFunction interpretation i)) : killed.card ≤ constantCount p S

A finite set of constant gates contributes its full cardinality to the count.

theorem Algebraic.Aggregate.Geometry.Shared.PrimaryPairing.exists_preprocess {n g : ℕ} (p : Program signature n g) (P : PrimaryPairing p) : ∃ (S : AffineFlat n) (d : ℕ), 2 ^ d * S.carrier.card = 2 ^ n ∧ d ≤ P.pairs.card ∧ d ≤ constantCount p S ∧ ∀ e ∈ P.pairs, ∃ j ∈ primaryInputs (p.lines e.1), j ∈ primaryInputs (p.lines e.2) ∧ ConstantOn S fun (x : Fin n → Bool) => x j

Shared controls can be fixed before circuit elimination, paying at most one equation per pair and obtaining at least as many distinct constant gate outputs.