Conjunction counts in the permutation entropy bound

For a permutation with nonliteral outputs and affine-output flats of at most 2^r points, distinct outputs give n + h ≤ g + o, biased primary messages give n ≤ g - o - c h₂, and affine pairing gives 2n ≤ g + h₂ + 2r. Here g counts gates, h conjunction gates, o conjunction outputs, h₂ multiple-primary conjunctions, and c = 1 - H₂(1/4). Eliminating o and h₂ leaves (2 + c)g ≥ (2 + 2c)n + h - 2rc. Any lower bound on h therefore improves the total gate bound; the restriction–rank bound supplies h ≥ 2n - D.

theorem Algebraic.Aggregate.Geometry.conjunctionCount_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) (small : ∀ (S : AffineFlat n), (∀ (i : Fin n), AffineOn S (c.outputFunction interpretation i)) → S.carrier.card ≤ 2 ^ r) : (2 + 2 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑n + ↑(conjunctionCount c.program) - 2 * ↑r * Cutwidth.Aggregate.Geometry.Entropy.bitSaving ≤ (2 + Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑c.size

Output counting, biased messages, and affine pairing leave the conjunction count as a free summand in the permutation bound.

theorem Algebraic.Aggregate.Geometry.restriction_entropy_mul_size_lower_bound {n r D : ℕ} (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) (rigid : NonaffineOnFlats (c.eval interpretation) D) (positive : 0 < n) (dimension : D ≤ n) (small : ∀ (S : AffineFlat n), (∀ (i : Fin n), AffineOn S (c.outputFunction interpretation i)) → S.carrier.card ≤ 2 ^ r) : (4 + 2 * Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑n - ↑D - 2 * ↑r * Cutwidth.Aggregate.Geometry.Entropy.bitSaving ≤ (2 + Cutwidth.Aggregate.Geometry.Entropy.bitSaving) * ↑c.size

If no nonzero output component is affine on a flat of 2^D points, the restriction–rank bound turns the conjunction summand into 2n - D.