theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.oneNine_power_iff_source_exponent (r q : ℕ) : r ^ 10 ≤ q ^ 9 ↔ ↑r ≤ ↑q ^ (19 / 10 - 1)

Exact real-exponent version of the integer-power carrier test, including zero inputs.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.D19_pos_iff_source_oneNine (N : ℕ) : 0 < D19 N ↔ ∃ (p : ℕ) (r : ℕ) (q : ℕ), p ≤ N ∧ Nat.Prime p ∧ (r = 1 ∨ Nat.Prime r) ∧ Nat.Prime q ∧ N = p + r * q ∧ ↑r ≤ ↑q ^ (19 / 10 - 1)

The actual D19 carrier is positive exactly when the paper's literal proposition holds.