Combining output rank, message information, and affine restrictions

Nonaffine independent output components require enough conjunction generators. Balanced outputs save primary-message bits, and affine pairing gives a second constraint on the multiple-primary gate count. Eliminating that count improves the three-halves coefficient.

theorem Algebraic.Aggregate.Geometry.entropy_mul_size_lower_bound {n r : ℕ} (c : Circuit signature n n) (bijective : Function.Bijective (c.eval interpretation)) (nonliteral : ∀ (i j : Fin n) (b : Bool), c.outputFunction interpretation i ≠ fun (x : Fin n → Bool) => b ^^ x j) (independent : NonaffineComponents (c.eval interpretation)) (small : ∀ (S : AffineFlat n), (∀ (i : Fin n), AffineOn S (c.outputFunction interpretation i)) → S.carrier.card ≤ 2 ^ r) : (3 + 2 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑n - 2 * ↑r * Cutwidth.Aggregate.Geometry.Entropy.bitSaving ≤ (2 + Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑c.size

Output rank and message bias improve the permutation bound beyond three halves.