Combining conditional-majority entropy with shared-control geometry

The same primary pairing supplies both the geometric saving and a product majority event. Its residual narrow and wide summaries retain entropy savings, which combine with both unconditional message inequalities using positive weights.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.size_lowerBound_of_sumsetDisperser {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) : have k := Nat.clog 2 K; have a := Shared.receiverRetention n k; (1 - jointWeight * Joint.overlapPenalty) * (↑n - ↑k - 1) + fiberWeight * (↑n - (1 + messageLoss - pairSaving) * (↑k + 1)) + 2 * a * wideWeight * (↑n - ↑k) - (1 + fiberWeight) * (1 + Real.logb 2 ↑K) ≤ (1 + fiberWeight + a * wideWeight) * ↑c.size

Conditional pair and triple savings improve the scalar finite circuit inequality.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.inversionNumerator_mul_input_sub_le {n r : ℕ} (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)) (small : ∀ (S : Aggregate.Geometry.AffineFlat n), (∀ (i : Fin n), Aggregate.Geometry.AffineOn S (c.outputFunction Aggregate.Geometry.interpretation i)) → S.carrier.card ≤ 2 ^ r) : inversionNumerator * ↑n - 2 * wideWeight * ↑r ≤ inversionDenominator * ↑c.size

Conditional-majority entropy combines with output rank and simultaneous affine geometry.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.inversionCoefficient_mul_sub_le_size {n r : ℕ} (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)) (small : ∀ (S : Aggregate.Geometry.AffineFlat n), (∀ (i : Fin n), Aggregate.Geometry.AffineOn S (c.outputFunction Aggregate.Geometry.interpretation i)) → S.carrier.card ≤ 2 ^ r) : inversionCoefficient * ↑n - 2 * wideWeight * ↑r / inversionDenominator ≤ ↑c.size

The exact multioutput coefficient retains the affine-flat dimension penalty.