Upper bound for the common retention fraction

A receiving side can only discard designated triples. Its exact retention fraction lies below one, allowing the disjoint-pair savings to use the same multiplier.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.receiverRetention_le_one {n k : ℕ} (range : k + 4 ≤ n) : Shared.receiverRetention n k ≤ 1

The common receiving-side retention factor never exceeds one.