# Update 2026-07-13: COUNT lower bound now UNCONDITIONAL in Lean

`BBMSTLower.eventually_log_irreducible_count_lower` proves, with NO BBMST hypothesis:

    (log 2 / 4096) * k * sqrt(k / log(k+1)) <= log |IrreducibleOfSize k|

along explicit dense frame sizes, i.e. exp(Omega(k^(3/2)/sqrt(log k))) strong
irreducible modulus sets. Sorry-free; axioms exactly [propext, Classical.choice, Quot.sound].

To re-verify (see BBMST_LOWER_REPRODUCE.md):
    tar -xzf erdos1189_bbmst_lower_lean_source.tar.gz && lake exe cache get && lake build
    lake env lean Research/BBMSTLowerAudit.lean

Independently re-verified on separate hardware 2026-07-13 (build clean, axioms standard,
no sorry/admit/native_decide). Remaining for full end-to-end: the matching UPPER bound.
