Large majority fibers of actual one-way circuit messages

The unmatched conjunction summaries have disjoint primary supports. Fixing their majority values leaves a large input set, while rectangle freeness bounds every fiber of the remaining message. The spare output bit is explicitly counted.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.sender_le_of_disjoint_summaries {n K : ℕ} (c : Circuit Aggregate.Geometry.signature n 1) (hK : 0 < K) (free : RectangleFree (c.outputFunction Aggregate.Geometry.interpretation 0) K) (freeNot : RectangleFree (fun (x : Cslib.BitString n) => !c.outputFunction Aggregate.Geometry.interpretation 0 x) K) (U : Finset (Fin n)) (large : 2 * K ≤ 2 ^ Uᶜ.card) (S : Finset (Fin c.size)) (selected : ∀ i ∈ S, Aggregate.Geometry.SelectedPair (c.program.lines i) U) (disjoint : (↑S).Pairwise fun (i j : Fin c.size) => Disjoint (Aggregate.Geometry.primaryInputs (c.program.lines i)) (Aggregate.Geometry.primaryInputs (c.program.lines j))) : ↑U.card + messageLoss * ↑S.card ≤ ↑c.size + 1 + Real.logb 2 ↑K

Disjoint selected conjunction summaries improve the actual sender's message bound.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.input_le_size_of_fibers {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) (P : Aggregate.Geometry.Shared.PrimaryPairing c.program) (disjoint : (↑P.remaining).Pairwise fun (i j : Fin c.size) => Disjoint (Aggregate.Geometry.primaryInputs (c.program.lines i)) (Aggregate.Geometry.primaryInputs (c.program.lines j))) : ↑n + messageLoss * ↑P.remaining.card ≤ ↑c.size + 1 + Real.logb 2 ↑K + (1 + messageLoss) * (↑(Nat.clog 2 K) + 1)

The original unmatched summaries lose at most one large-fiber saving per receiver bit.