Lean pattern: asymptotic number theory as explicit core lemma + filter_upwards

For 'for all large p' theorems (e.g. Vinogradov's least non-residue n_p ≤ p^{1/(2√e)+ε}), split the proof: (1) a deterministic lemma with all the conditions on P = (p:ℝ) as explicit real hypotheses (P^c/2 ≥ 2, log(P^c/2) ≥ K, P^{1/2+δ}/4 ≥ 1/κ, √P(2+log P) < κ/2·P^{1/2+δ}); (2) the asymptotic theorem picks parameters, proves each condition ∀ᶠ P : ℝ in atTop from tendsto_rpow_atTop, .atTop_div_const, Real.tendsto_log_atTop.comp, and (isLittleO_log_rpow_atTop hδ).bound (c := κ/8), bundles them with filter_upwards [...] with P h0 h1 h2 ..., then pulls back to ℕ with tendsto_natCast_atTop_atTop.eventually E. Choose the free parameter so a key quantity is exact: x := y^(1/θ) gives log x / log y = 1/θ on the nose, which avoids floor slack inside the log. Numeric facts about e^{1/2}: Real.quadratic_le_exp_of_nonneg (≥ 1.625) and Real.exp_one_lt_d9 squared (< 2). Real.pi_gt_three needs Mathlib.Analysis.Real.Pi.Bounds imported.