Eventual validity of the near-halving parameter guard

The binary logarithm of the target length eventually dominates three iterated ceiling logarithms plus fifteen. Consequently the finite guard required by the rounded parameter choice eventually holds. This numeric fact alone asserts neither extraction nor polynomial-time evaluation.

theorem Algebraic.Cutwidth.Extractor.eventually_gammaBlockSizeGuard : ∀ᶠ (b : ℕ) in Filter.atTop, GammaBlockSizeGuard b

Every sufficiently large target length satisfies the exact finite size guard.