theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.eventually_rpow_le_scaled_floor_rpow (ε t u : ℝ) (hε : 0 < ε) (hu : 0 < u) (htu : t < u) : ∃ (N₀ : ℕ), 2 ≤ N₀ ∧ ∀ (N : ℕ), N₀ ≤ N → ↑N ^ t ≤ ↑⌊ε * ↑N⌋₊ ^ u

Fixed-scale floor transport with a strict exponent gap. Parameters precede the threshold.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachC10ProductSupport_scaled_floor_eventually (ε γ : ℝ) (hε : 0 < ε) (hγ : γ < 1 / 3) : ∃ (N₀ : ℕ), ∀ (N : ℕ), N₀ ≤ N → ∀ (b : ℝ), ∀ m ∈ goldbachC10ProductSupport N b (↑N ^ γ), ↑m ≤ ↑⌊ε * ↑N⌋₊ ^ (2 / 3)

The actual B10 support fits the smaller Pan endpoint for fixed epsilon and gamma.