feat(opening): bound affine binder messages - #72
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b2d4a0e71f
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| If a finite message decoder represents every solution of one binary affine | ||
| equation on `n + 1` coordinates, its message space contains at least `2^n` | ||
| elements. |
There was a problem hiding this comment.
For an affine equation whose entire linear part is zero, the solution set has either no elements or 2^(n + 1) elements, rather than the asserted 2^n; completeWord avoids this case by implicitly fixing the pivot coefficient to 1. Consequently, this theorem covers only normalized equations with a chosen nonzero pivot, not every binary affine equation as its public contract claims. State that assumption explicitly here, or model the full coefficient vector and require the selected pivot coefficient to be nonzero.
AGENTS.md reference: AGENTS.md:L21-L22
Useful? React with 👍 / 👎.
1 participant
What does this change?
Proves that any deterministic no-response decoder covering every solution of one binary affine equation on
n + 1coordinates needs at least2^nmessages, hence at leastnmessage bits. The coverage hypothesis excludes structured subsets and later interaction.How was it tested?
lake build --wfailpasses on stacked tip16b7318lake lintpasses on stacked tip16b7318sorryor new axioms, or this PR does not change Lean proofsgit diff --checkpasses