Repository navigation
Make the proof-gate and R-bridge claims match the tree; first CI run - #1
Merged
Merged
Conversation
- Add proofs/tests/gate-selftest.sh: every reject/ control must fail Agda for the reason on its EXPECT line, and each of the seven axiom-audit checks must fire on a planted defect (clean copy as positive control). - Add proofs/PROOF-STATUS.md: proved vs tested vs open, per property. - Mark axiom-audit.sh executable (100644 died with exit 126 in the gate). - README / R-SUNSET: the RCall extension and the R oracle are planned, not shipped; the multinomial lives in CompositionalCounts.jl. - Repoint dangling proofs/residue/*.residue references to PROOF-STATUS.md. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01WpM43to7Y8kCFbxyHvQ5Tp
Contributor
|
Navigate logical layers of code changes, visualize relationships, and explore their blast radius. Note Currently processing new changes in this PR. This may take a few minutes, please wait... ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: 📒 Files selected for processing (8)
✨ Finishing Touches 💡 1📝 Generate docstrings 💡
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 |
Contributor
|
❌ Failed to create Coding Agent finishing-touch task. Please try again. |
Contributor
|
Autopilot could not be updated. Open Coding to check access and billing. |
Owner
Author
|
@coderabbitai review |
Contributor
|
hyperpolymath
added a commit
that referenced
this pull request
Oct 2, 2026
…elf-test (18 controls); PROOF-STATUS; axiom-audit executable Rebased onto PR #1. The two self-tests are merged: the theorem mutants and StepUp controls from this branch, plus one audit control per axiom-audit check from PR #1. Each audit control must fail with its named finding. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019Y6e175rh1LbrsEhQvCrJ1
hyperpolymath
added a commit
that referenced
this pull request
Oct 2, 2026
Proves P5, the Benjamini–Hochberg step-up, and makes the gate self-test cover every audit check. **What changes** - New `proofs/agda/CompositionalDA/BenjaminiHochberg/StepUp.agda` proves three properties over exact rationals ℚᵘ: q ≥ p, q ≤ 1, and order preservation (p_i ≤ p_j ⇒ q_i ≤ q_j). - They hold on the sorted sequence and also at the original indices, via a permutation. - Named assumption: the input is sorted descending and every p is in [0, 1]. The sort itself is not verified, and nothing about floating point is proved. - `proofs/tests/gate-selftest.sh` now has 18 controls: - 7 theorem mutants; - 7 audit plants, one per `axiom-audit.sh` check. Each must fail **with its named finding**; - 3 `reject/` files; - the pristine tree. - This merges PR #1's audit plants with this branch's theorem mutants. - `proofs/PROOF-STATUS.md` and `proofs/residue/*.residue` separate what is proved, what is tested, and what is open. - `README.md` no longer says the BH proofs cover only the scaling step. **Verified locally (Agda 2.7.0.1, stdlib 2ffa8b7d, Julia 1.12)** - `proofs/bootstrap.sh`: exit 0, 7 modules, audit clean. - `proofs/tests/gate-selftest.sh`: exit 0, 18/18. A planted wrong reason on one audit control is reported as FAIL (17/18). - `Pkg.test()`: 43/43. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_019Y6e175rh1LbrsEhQvCrJ1 Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
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.
First PR against the new
main(created fromwip/core-p1-p5@ 62fb833), so CI runs for the first time — it had 0 runs because it only triggers onmain, tags and PRs.What changes
proofs/tests/gate-selftest.sh(was linked from the README and called by CI, but missing): eachproofs/agda/reject/*.agdamust fail Agda for the reason on its-- EXPECT:line; each of the 7axiom-audit.shchecks must fire on a planted defect, with an unmodified copy as positive control.proofs/PROOF-STATUS.md(linked, missing): proved vs tested vs open, per property. States that the BH proofs cover the scaling step only and that P5 is tested, not proved.axiom-audit.shcommitted100755— at100644the gate died with exit 126.docs/R-SUNSET.md: the RCall extension and R oracle are planned, not in the tree; the multinomial is out of scope here (CompositionalCounts.jl, Proposal: Multinomial and Dirichlet-Multinomial regression as an external package (pure-Julia backend) JoshuaJewell/MetaManifold-WebUI#22).proofs/residue/*.residuereferences repointed.Verified locally:
Pkg.test()passes;proofs/bootstrap.sh --check→axiom-audit: clean,proofs: OK;gate-selftest.sh→ 3 controls rejected, 7 audit checks fire. Mutant check: disabling the audit's postulate check makes the self-test fail withaudit check 'postulate' missed its planted defect.🤖 Generated with Claude Code
https://claude.ai/code/session_01WpM43to7Y8kCFbxyHvQ5Tp