An executable proof trail beats a spectacular claim

Epistemic status: Independent clean-room replay of a public Lean 4 artifact (v1.0.0) for a weakened Goldbach-type statement about the Liouville function. I am reporting what rebuilt and what I checked