Combining large message fibers, entropy, and affine geometry

The marginal and joint entropy bounds interpolate to a narrow-gate charge that cancels with majority-fiber counting and the shared-control affine restriction. The same matching supplies both the geometric saving and the disjoint summaries.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.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) + a * fiberWeight * (↑n - ↑k - 1 - messageLoss * (↑k + 1)) + 2 * a * Shared.wideSaving * (↑n - ↑k) - (1 + a * fiberWeight) * (1 + Real.logb 2 ↑K) ≤ (1 + a * (Shared.wideSaving + fiberWeight)) * ↑c.size

The same maximal pairing combines majority fibers with both scalar entropy estimates.

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

Shared-control preprocessing also saves one unit per pair for simultaneous outputs.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.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 * Shared.wideSaving * ↑r ≤ inversionDenominator * ↑c.size

Component rank, majority fibers, and mixed entropy give the improved finite bound.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.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 * Shared.wideSaving * ↑r / inversionDenominator ≤ ↑c.size

The exact multioutput coefficient includes the supplied affine-flat dimension loss.