Conditional entropy of actual one-way messages

A fixed-size receiving set retains a weighted collection of narrow and wide summaries. The unmatched disjoint pairs lose at most one member per receiver coordinate, so their majority event supports all three information savings.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.card_subtype_fiber_le {X : Type u_1} {Y : Type u_2} [Fintype X] (event : Finset X) (key : X → Y) (y : Y) : {x : ↥event | key ↑x = y}.card ≤ {x : X | key x = y}.card

Restricting the domain of a message cannot enlarge its fibers.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.sender_le_of_conditional_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 : S ⊆ Joint.retainedTwo c.program 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 - pairSaving) * ↑S.card + pairSaving * ↑(Joint.retainedTwo c.program U).card + tripleSaving * ↑(Joint.retainedWide c.program U).card ≤ ↑c.size + 1 + Real.logb 2 ↑K

Conditional entropy strengthens the sender bound on the same majority event.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.input_le_size_of_conditional_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) (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 + Shared.receiverRetention n (Nat.clog 2 K) * ((messageLoss - pairSaving) * ↑P.remaining.card + pairSaving * ↑(Aggregate.Geometry.Shared.exactTwo c.program).card + tripleSaving * ↑(Joint.retainedWide c.program Finset.univ).card) ≤ ↑c.size + 1 + Real.logb 2 ↑K + (1 + messageLoss - pairSaving) * (↑(Nat.clog 2 K) + 1)

Weighted cut retention and disjoint-pair loss give the conditional finite inequality.