Asymptotics of conditional-majority information bounds

The receiver threshold and logarithmic message-fiber losses are sublinear. Normalizing the finite combined inequality gives the exact conditional-majority coefficient, retaining all conditional pair and triple savings.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.normalized_bound_tendsto {K : ℕ → ℕ} (small : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ K n) : Filter.Tendsto (fun (n : ℕ) => ((1 - jointWeight * Joint.overlapPenalty) * (1 - ↑(Nat.clog 2 (K n)) / ↑n - 1 / ↑n) + fiberWeight * (1 - (1 + messageLoss - pairSaving) * (↑(Nat.clog 2 (K n)) / ↑n + 1 / ↑n)) + 2 * Shared.receiverRetention n (Nat.clog 2 (K n)) * wideWeight * (1 - ↑(Nat.clog 2 (K n)) / ↑n) - (1 + fiberWeight) * (1 / ↑n + Real.logb 2 ↑(K n) / ↑n)) / (1 + fiberWeight + Shared.receiverRetention n (Nat.clog 2 (K n)) * wideWeight)) Filter.atTop (nhds gateCoefficient)

The normalized finite conditional-majority inequality converges to its coefficient.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.Conditional.eventually_lt_of_combined_bound {K : ℕ → ℕ} (small : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (positive : ∀ᶠ (n : ℕ) in Filter.atTop, 1 ≤ K n) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (g : ℝ), (1 + fiberWeight + Shared.receiverRetention n (Nat.clog 2 (K n)) * wideWeight) * g ≥ (1 - jointWeight * Joint.overlapPenalty) * (↑n - ↑(Nat.clog 2 (K n)) - 1) + fiberWeight * (↑n - (1 + messageLoss - pairSaving) * (↑(Nat.clog 2 (K n)) + 1)) + 2 * Shared.receiverRetention n (Nat.clog 2 (K n)) * wideWeight * (↑n - ↑(Nat.clog 2 (K n))) - (1 + fiberWeight) * (1 + Real.logb 2 ↑(K n)) → (gateCoefficient - ε) * ↑n < g

Every finite receiver loss is absorbed by arbitrary positive linear slack.