Asymptotics of majority-fiber and entropy counting

The receiving threshold and every logarithmic loss are sublinear. Normalizing the finite combined inequality therefore gives the exact majority-fiber gate coefficient, with no additional assumptions on the circuit geometry.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.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) + Shared.receiverRetention n (Nat.clog 2 (K n)) * fiberWeight * (1 - ↑(Nat.clog 2 (K n)) / ↑n - 1 / ↑n - messageLoss * (↑(Nat.clog 2 (K n)) / ↑n + 1 / ↑n)) + 2 * Shared.receiverRetention n (Nat.clog 2 (K n)) * Shared.wideSaving * (1 - ↑(Nat.clog 2 (K n)) / ↑n) - (1 + Shared.receiverRetention n (Nat.clog 2 (K n)) * fiberWeight) * (1 / ↑n + Real.logb 2 ↑(K n) / ↑n)) / (1 + Shared.receiverRetention n (Nat.clog 2 (K n)) * (Shared.wideSaving + fiberWeight))) Filter.atTop (nhds gateCoefficient)

The normalized finite majority-fiber bound converges to its exact coefficient.

theorem Algebraic.Cutwidth.Aggregate.Geometry.Fiber.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 + Shared.receiverRetention n (Nat.clog 2 (K n)) * (Shared.wideSaving + fiberWeight)) * g ≥ (1 - jointWeight * Joint.overlapPenalty) * (↑n - ↑(Nat.clog 2 (K n)) - 1) + Shared.receiverRetention n (Nat.clog 2 (K n)) * fiberWeight * (↑n - ↑(Nat.clog 2 (K n)) - 1 - messageLoss * (↑(Nat.clog 2 (K n)) + 1)) + 2 * Shared.receiverRetention n (Nat.clog 2 (K n)) * Shared.wideSaving * (↑n - ↑(Nat.clog 2 (K n))) - (1 + Shared.receiverRetention n (Nat.clog 2 (K n)) * fiberWeight) * (1 + Real.logb 2 ↑(K n)) → (gateCoefficient - ε) * ↑n < g

Every finite threshold loss is absorbed by an arbitrary positive linear slack.