The exponential bound for the actual normalized signed family

Bernoulli's inequality gives the coarser alphabet size ⌊ε⁻¹¹⌋ + 1, which is already sufficient without the logarithmic grid-count estimate. The elementary inequality log t ≤ t / 2 then absorbs this alphabet and the length bound into exp (8 ε⁻³).

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.log_le_half {t : ℝ} (ht : 0 < t) : Real.log t ≤ t / 2

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.uniformBound_lt_exp {t : ℝ} (ht : 1 ≤ t) : ↑((⌊t ^ 11⌋₊ + 2) ^ ⌊t ^ 2⌋₊) < Real.exp (8 * t ^ 3)

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags_card_lt_exp (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 1 < D) (hε : 0 < ε) (hεone : ε ≤ 1) : ↑(signedTags upper P D ε label).card < Real.exp (8 * ε⁻¹ ^ 3)

The actual accepted profiles, including the empty profile, satisfy the source exponential family-size bound. Neither correct geometric labelling nor a cardinality premise is needed, and the estimate is uniform in P and D.

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags_card_lt_exp_source (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 2 ≤ D) (hε : 0 < ε) (hεsmall : ε < 1 / 8) : ↑(signedTags upper P D ε label).card < Real.exp (8 * ε⁻¹ ^ 3)

The source range D ≥ 2, 0 < ε < 1/8 is an immediate specialization.