feat(opening): bind four affine coordinates

[windsornguyen]

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

What does this change?

Defines a deterministic three-bit binder for four binary coordinates satisfying one affine equation, and proves exact decoding plus radius-one checksum separation. No prover response is sent after the public coordinate challenge.

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
• Decoder and checksum equations compile as kernel-checked theorems