Research proof index

Finite tail-sum formula for natural-valued writer cost under a pathwise upper bound. If every execution path of oa incurs cost at most n, then the tail probabilities vanish above n, so the infinite tail sum truncates to Finset.range n.

This lemma proves the final algebraic step in the DG25 Theorem 3.1 proof. It shows that if R > e + 1, then e * (R / (R - 1)) < e + 1. The intuition is that the fraction R / (R - 1) is always greater than 1, but as R gets larger, it gets closer to 1. The hypothesis R > e + 1 provides a strong enough bound to ensure the product e * (fraction) do...

The k-th coefficient (k < deg φ) of a gadget-decomposition block is exactly the corresponding digit of the corresponding input coefficient.

The base-b gadget decomposition is a lawful gadget decomposition.

Each gadget-decomposition block is ℓ₂²-short: its centered squared-ℓ₂ norm is at most (deg φ)·(b-1)² (each of the deg φ coefficients contributes at most (b-1)²).

ℓ₂² shortness of G⁻¹. The full gadget decomposition has centered squared-ℓ₂ norm at most (rows·digits)·(deg φ)·(b-1)².