Repository navigation
board, dr-math: D-DRMC-5 already certifies associativity; correct two stale claims - #1738
Merged
Merged
Conversation
… stale claims 6ad966d said no DR64 certificate exists. relcomp::certify_reassociation (D-DRMC-5) certifies reassociation of a Boolean composition chain with an egglog-checked proof and a digest-bound lowering; re-run green (12 relcomp tests). NoCertifiedCompiler is the single-operand admit_recipe path only. RECIPE_ADMISSION.md carried the same stale sentence. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
|
Important
This repository does not receive automatic reviews because it has fewer than 10 stars. ⚙️ Run configuration
Warning Billing warning: we have not been able to collect payment for this subscription for more than 72 hours. Please update the payment method or pay any pending invoices in Billing to avoid service interruption. Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
AdaWorldAPI
marked this pull request as ready for review
October 23, 2026 10:28
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 23, 2026
… file attribution Catch-up entries from the merge commits; hygiene-only PRs (#1727, #1728, #1730, #1732-#1735) get none. #1738 is a correction and gets one. D-TGA-5's row named src/squash.rs under #1736; #1736 added only tests/squash_gate.rs, and the gate moved to src/squash.rs in #1739. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VncKoyG6JkpsoqhqTGTv3f
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 23, 2026
…ents recipe.rs and tests/contract_handoff.rs said no certified-compiler boundary exists for DR64 laws. The single-operand admit_recipe path still has no certifier, but relcomp::certify_reassociation (#1707) certifies one law: associativity of Boolean-Distinct composition over a DR64 chain. #1738 corrected two other sites; these two remained. Comments only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
This was referenced Oct 23, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes a false claim that reached
mainwith #1736.Commit
6ad966d1says "no certificate exists for DR64". That is not true.relcomp::certify_reassociation(D-DRMC-5, commits a554da1 and 903e664) certifies the reassociation of a Boolean relation-composition chain end to end:RecipeCertificateis bound to thelowering_digest.I re-ran the crate on 2026-10-23: 37 tests green, 12 of them in
relcomp.NoCertifiedCompileris returned only by the single-operandadmit_recipepath.Changes
.claude/board/entries/2026-10-23-coresearch-thought-git-markov.md: strike the stale line, state what D-DRMC-5 covers, and list what is still open:crates/dr-math-binding-probe/RECIPE_ADMISSION.md: the same stale sentence, scoped to the single-operand path.Docs only; no code changes.
Generated by Claude Code