Mixed entropy inequalities for the large-fiber lower bound

Scalar circuits retain both the marginal and shared-graph message estimates. For permutations, constant conjunction-output messages cost zero; output rank then gives two inequalities with the same narrow and wide gate counts.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.input_le_size_of_marginal_entropy {n K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (hK : 0 < K) (disperse : FlatSumsetDisperser (c.outputFunction Aggregate.Geometry.interpretation 0) K) (range : Nat.clog 2 K + 4 ≤ n) : ↑n - ↑(Nat.clog 2 K) - 1 ≤ ↑c.size + 1 + Real.logb 2 ↑K - Shared.receiverRetention n (Nat.clog 2 K) * (Entropy.bitSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + Shared.wideSaving * ↑(Joint.retainedWide c.program Finset.univ).card)

A logarithmic receiving side retains separate marginal narrow and wide savings.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.three_mul_input_add_marginal_le_two_mul_size {n : ℕ} (c : Circuit Aggregate.Geometry.signature n n) (bijective : Function.Bijective (c.eval Aggregate.Geometry.interpretation)) (nonliteral : ∀ (i j : Fin n) (b : Bool), c.outputFunction Aggregate.Geometry.interpretation i ≠ fun (x : Fin n → Bool) => b ^^ x j) (independent : Aggregate.Geometry.NonaffineComponents (c.eval Aggregate.Geometry.interpretation)) : 3 * ↑n + Entropy.bitSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + Shared.wideSaving * ↑(Joint.retainedWide c.program Finset.univ).card ≤ 2 * ↑c.size

Nonaffine permutation outputs combine with the separate marginal message savings.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.three_sub_penalty_mul_input_add_joint_le_two_mul_size {n : ℕ} (c : Circuit Aggregate.Geometry.signature n n) (bijective : Function.Bijective (c.eval Aggregate.Geometry.interpretation)) (nonliteral : ∀ (i j : Fin n) (b : Bool), c.outputFunction Aggregate.Geometry.interpretation i ≠ fun (x : Fin n → Bool) => b ^^ x j) (independent : Aggregate.Geometry.NonaffineComponents (c.eval Aggregate.Geometry.interpretation)) : (3 - Joint.overlapPenalty) * ↑n + Joint.gateSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + Shared.wideSaving * ↑(Joint.retainedWide c.program Finset.univ).card ≤ 2 * ↑c.size

Nonaffine permutation outputs also retain the joint support-graph savings.