Affine restrictions with paired gate charges

A nonconstant internal affine predecessor can be fixed to a conjunction's controlling value. This makes both the predecessor and the new gate permanently constant. Only multiple-primary conjunctions can need a restriction without an internal partner.

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

Processing an actual program keeps every gate affine, charging each affine restriction to two newly constant gates or to one gate and one multiple-primary mark.

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

Every signed AND/OR/XOR program has a nonempty monochromatic affine flat of codimension at most half the gate count plus half its multiple-primary count, plus one. The exact cardinality identity records the codimension without rounding logarithms.