Repository navigation
feat(math-foundry): certified E1 pattern catalogue and guarded baseline fallback - #1694
Merged
AdaWorldAPI merged 3 commits intoOct 22, 2026
Conversation
|
Important Review skippedAuto reviews are disabled on base/target branches other than the default branch. Please check the settings in the CodeRabbit UI or the ⚙️ Run configuration
You can disable this status message by setting the Use the checkbox below for a quick retry:
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 22, 2026 06:57
AdaWorldAPI
merged commit Oct 22, 2026
3e7ffcf
into
lab/math-foundry-1-proof-replay-20261022
10 checks passed
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. |
This was referenced Oct 22, 2026
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 22, 2026
…xecuted P0 falsifiers #1696 merged (df214bb), so #1694/#1695 are no longer stranded; the contradictory-premise counterexample has been executed (14 vs 21 by premise order) and is fixed for linear E1 in #1698 (11ca3fe), together with the checked-overflow range guard. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01G22yT6htkcdyXsihxxXdrg
This was referenced Oct 23, 2026
Merged
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 26, 2026
…endent invalidation falsifier Corrects the binding-store wording: the generalized Quack Binding Store is planned/unbuilt, while numeric binding, RelAlg let reuse (#1649, #1653), witnessed DR populations (#1666), typed DR method binding (#1701/#1708) and compiled mathematical recipes (#1693/#1694/#1707/ #1740) exist in production or lab. Notes #1666 Pop's witness refusal in B.7(5). Replaces "a property change is harmless" with the three-way invalidation rule, and adds the falsifier it needs to the P2 lab: a property read by R's criteria is mutated; the reused R2 keeps 1,032 rows vs 31 fresh and a downstream read differs, silently (`--controls`, seed 0x0D0D_F00D). Disable run red (skipping the mutation fails the non-vacuity assertion). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
AdaWorldAPI
pushed a commit
that referenced
this pull request
Oct 26, 2026
…, P2) Links the existing implementation spine with source and status: #1649, #1653, #1659, #1666, #1681, #1685, #1693, #1694 (landed via #1696/#1698), #1701/#1703 (via #1708), #1707, #1740. Separates production (Quack numeric binding, CompiledProgram, mask-risc terminals, r2il procedures, the contract's SetProgram type) from lab. Names the smallest missing seams with their owners: D-NFR-1 frame on a bound Query (needs NFR-OP-1), an input-generation dependency witness for kept planes (binding store; witness type is NFR-OP-3, so no new Pop), and the D-NFR-2 codebook generation. Shows how one certified recipe applies to many witnessed bindings without copying populations, re-reads the DuckDB harvest against what exists, and states the authorization boundary. Documentation only. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X6y3drwKSE2zSgoexheLFX
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.
Stack 2/3 — certified pattern catalogue and trusted fallback
Stack base: #1693 /
lab/math-foundry-1-proof-replay-20261022. Foundation: merged #1690 Stage B E1. This PR's diff is incremental only.Catalogueholding E1 proof capsules under a FULL semantic key (goal, target variable, premises with coefficients/order), a target/ABI fingerprint and a caller-supplied source/coordinate/scope witness.promoterechecks the capsule, independently evaluates E1 against existing i128 oracle for a small sample, and requires a caller-supplied amortization cost gate. This is a lab policy, not formal statistical certification of hardware timings.execute_orperforms cache lookup and guarded R2IL execution with no egglog. Cache miss, stale binding, changed ABI/target or execution refusal run the trusted caller-provided baseline. No hidden data write.Important boundary: caller-provided witness fields are not independent source attestation; no production admission is claimed. Candidate is the already supported E1 exact-integer program, not an arbitrary user-discovered law.
Review: draft pending CI, local Rust tests not executed from this environment. Commands from
crates/egglog-r2il-probe:cargo test,cargo fmt --check,cargo clippy --all-targets -- -D warnings. No autonomous merge.Next stacked PR: historical source metadata and a falsifiable 27-atom mathematical heritage study.