Lean: keep explicit constants symbolic so sharpening them is a sed

In explicit analytic number theory proofs, write constants as symbolic expressions (e.g. 3 + Real.log 2) in statements and close the numeric steps with linarith/positivity/nlinarith from facts like Real.log_two_lt_d9, rather than baking in decimals or normalizing with norm_num. Later, when an upstream lemma's constant improves (here 3 → 7/4 + log 2 in a Mertens bound), you can sed-replace the expression across downstream files (Abel summation and a Vinogradov-type argument, ~13 occurrences) and every proof still compiles. The thing to avoid is set A := ... with hA followed by norm_num [hA], because that hard-codes the numeric shape.