docs(research): record affine opening boundary - #73
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: 19f0880708
ℹ️ 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".
| The later symbolic proof explains the search result. Hamming's binary | ||
| condition uses nonzero, pairwise-distinct check columns (1950, Section 3, | ||
| pp. 150-154). Lean proves the finite-field projective generalization: |
There was a problem hiding this comment.
This borrowed condition is cited only by surname, year, section, and pages here and in the duplicate citation in canonical-opening-theorem-index.md; both omit the source title and publication/edition information required by the repository’s provenance rules. Identify it fully—for example, Hamming, Error Detecting and Error Correcting Codes, Bell System Technical Journal 29(2), 1950—while retaining the precise section and pages.
AGENTS.md reference: AGENTS.md:L42-L43
Useful? React with 👍 / 👎.
| tensor instantiation `FourAxisAffine.exactStep` groups a | ||
| `2 x 2 x 2 x 2` tensor into four inner-slice contractions; one public | ||
| coordinate challenge emits a two-axis child. There is no prover response after |
There was a problem hiding this comment.
When outerWord parent = 0—for example, because either outer weight vector is zero—FourAxisAffine.step does not emit an Open2 child: it accepts a zero claim or rejects a nonzero claim without using the coordinate challenge. Therefore the asserted four-to-two emission only occurs under the missing outerWord parent ≠ 0 assumption; state that condition or describe the terminal branch explicitly.
AGENTS.md reference: AGENTS.md:L21-L22
Useful? React with 👍 / 👎.
| An affine equation on `n + 1` binary coordinates leaves `n` free coordinates. | ||
| Lean proves that a deterministic no-response decoder representing every | ||
| solution needs at least `2^n` messages. When the messages are `r`-bit strings, | ||
| it derives `n <= r`. |
There was a problem hiding this comment.
A general binary affine equation need not leave exactly n free coordinates: the zero-coefficient equation is either inconsistent or leaves all n + 1 coordinates free. The formal theorem avoids this by constructing equations with an implicit unit coefficient at the selected pivot, so this summary and its duplicate in the theorem index should explicitly restrict the lower bound to a nonzero equation with such a pivot.
AGENTS.md reference: AGENTS.md:L21-L22
Useful? React with 👍 / 👎.
| `unbatchedTensorOpening_not_clockClosing` proves that the sufficient inequality | ||
| `Lambda^t < t` is impossible when `2 <= Lambda`. The companion winner-cost | ||
| theorem states the corresponding natural-number mass bound. |
There was a problem hiding this comment.
The companion theorem unbatchedTensorOpening_winnerCost_not_lt_parentMass requires 1 < axisLength, but this exact-scope ledger describes its natural-number mass bound without that hypothesis. Record the axis-length restriction so readers do not treat the stated theorem as having fewer assumptions than its Lean declaration.
AGENTS.md reference: AGENTS.md:L21-L22
Useful? React with 👍 / 👎.
1 participant
What does this change?
Updates the research ledger with the exact affine four-to-two construction, its cardinality-optimal finite baseline, and the remaining asymptotic boundary. It explicitly records that no current theorem supplies square-log compression, operational realization, or evidence for
P != NP.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