feat(checksum): classify radius-one syndromes

[windsornguyen]

Explain what this changes, why it is needed, and anything reviewers should
verify. Link an issue when one exists.

What does this change?

Proves that radius-one syndrome decoding is injective exactly when every parity-check column is nonzero and the nonzero scaled columns are pairwise distinct. This is the finite-field projective classification; Hamming (1950) is cited only for its binary specialization.

How was it tested?

• lake build --wfail passes on stacked tip 16b7318
• lake lint passes on stacked tip 16b7318
• No sorry or new axioms, or this PR does not change Lean proofs
• git diff --check passes
• The specialized module compiles with lake env lean