Proof obligation for `verify_sign_correct` in `LatticeCrypto/Falcon/Security.lean`

[quangvdao]

A proof in LatticeCrypto/Falcon/Security.lean contains a sorry.

Goal: Replace the sorry with a complete proof.

Link to the sorry on GitHub

Code Snippet:

The proof relies on:
1. The NTRU equation ensuring `s₁ + s₂ · h = c mod q`.
2. The norm bound from `ffSampling` ensuring `‖(s₁, s₂)‖₂² ≤ ⌊β²⌋`.
3. The compress/decompress roundtrip preserving `s₂`. -/
theorem verify_sign_correct (pk : PublicKey p) (sk : SecretKey p)