Likely misformalization in `Wikipedia/HardyLittlewood.lean`: unconditional `∏'` for conditionally convergent constant

### Describe the misformalization
`FirstHardyLittlewoodConjectureFor` in `FormalConjectures/Wikipedia/HardyLittlewood.lean:63` defines `C_P` with `∏' q : {q // q.Prime ∧ 3 ≤ q}`.

Same defect class as #5255: `∏'` is `tprod`, unconditional. Junk `1` if not `Multipliable`. Here log-factor is `O(1/q)`, `∑ 1/p` diverges, so product is conditionally convergent only in increasing-prime order. Formal constant is `0` or junk.

Permalink: `FormalConjectures/Wikipedia/HardyLittlewood.lean#L63`
Related: #5255 (Bateman-Horn), #4996 (covers =O vs ∼, not this product)

### Trivial proof/disproof
No full disproof yet, by analogy to #5255 disproof (`X²+1` vs `4X²+1` giving same `1/2`): any two constellations with same `k` but different true constants will get same junk value here.

### Suggested fix
Same as #5255: replace with `N ↦ ∏ q in Nat.primesBelow N, ...` and state `∃ C > 0, Tendsto ... (𝓝 C) ∧ ...`, or otherwise make order explicit.

`ArtinPrimitiveRootsConjecture.lean:63` checked — `1/p(p-1)` is summable, `∏'` valid there. Only Hardy-Littlewood needs fix among the `∏'` hits.

### Additional context
Found by `grep ∏'` audit (5 hits). `lake` build not run locally — statement-only change.

### Choose either option
- [X] I plan on working on this issue