Multioutput lower bounds for permutations

Balanced distinct outputs occupy gates outside the multiple-primary conjunction class. Combining this output count with affine pairing gives a coefficient of three halves whenever the computed permutation has only small affine restrictions.

theorem Algebraic.Aggregate.Geometry.two_mul_input_le_size_add_multi_of_affine_restrictions {n m r : ℕ} (c : Circuit signature n m) (small : ∀ (S : AffineFlat n), (∀ (i : Fin m), AffineOn S (c.outputFunction interpretation i)) → S.carrier.card ≤ 2 ^ r) : 2 * n ≤ c.size + multiCount c.program + 2 * r

Small simultaneous affine restrictions force the paired gate charge.

theorem Algebraic.Aggregate.Geometry.three_mul_input_le_two_mul_size {n r : ℕ} (c : Circuit signature n n) (bijective : Function.Bijective (c.eval interpretation)) (nonprojection : ∀ (i j : Fin n), c.outputFunction interpretation i ≠ fun (x : Fin n → Bool) => x j) (small : ∀ (S : AffineFlat n), (∀ (i : Fin n), AffineOn S (c.outputFunction interpretation i)) → S.carrier.card ≤ 2 ^ r) : 3 * n ≤ 2 * c.size + 2 * r

A permutation with nonprojection coordinates and affine flats of size at most 2^r requires at least (3n-2r)/2 signed unbounded AND/OR/XOR gates.