[hyperpolymath]

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 Make the proof-gate and R-bridge claims match the tree; first CI run #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.ai/code/session_019Y6e175rh1LbrsEhQvCrJ1

[coderabbitai]

Navigate logical layers of code changes, visualize relationships, and explore their blast radius.

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 9deb2bc0-52b9-4c52-9422-1373f618933c

📥 Commits

Reviewing files that changed from the base of the PR and between 81bbd10 and 238c95a.

📒 Files selected for processing (7)

• README.md
• proofs/PROOF-STATUS.md
• proofs/agda/CompositionalDA/All.agda
• proofs/agda/CompositionalDA/BenjaminiHochberg/StepUp.agda
• proofs/residue/benjamini-hochberg.residue
• proofs/residue/clr.residue
• proofs/tests/gate-selftest.sh

Included review availability: This review used your included allowance. Your plan provides up to 1 included review per hour; 0 remain after this review.

📜 Recent review details

⏰ Context from checks skipped due to timeout. (3)

• GitHub Check: Julia 1.12
• GitHub Check: Agda proofs (2.7.0.1)
• GitHub Check: Julia 1.10

🧰 Additional context used

🪛 ast-grep (0.45.3)

proofs/tests/gate-selftest.sh

[error] 137-137: A variable, parameter expansion, or command-substitution result is passed as the command string to bash -c / sh -c, so its value is re-parsed by the shell. If any part of that value is attacker-controlled (arguments, environment, file contents, network output), it allows arbitrary command execution. Do not interpolate dynamic data into -c: pass the script as a fixed literal and forward untrusted values as positional arguments (bash -c 'program ""' _ "$value"), invoke the target program directly with proper quoting, or restrict input to a validated allowlist first.
Context: "$mutator"
Note: [CWE-78] Improper Neutralization of Special Elements used in an OS Command ('OS Command Injection').

(bash-c-variable-injection-bash)

🪛 LanguageTool

proofs/PROOF-STATUS.md

[style] ~22-~22: Would you like to use the Oxford spelling “normalizes”? The spelling ‘normalises’ is also correct.
Context: ....0tag exists. >proofs/bootstrap.sh` normalises the name and refuses any other revision...

(OXFORD_SPELLING_Z_NOT_S)

---

[uncategorized] ~32-~32: The official name of this software platform is spelled with a capital “H”.
Context: ...for the count | The CI job proofs in .github/workflows/ci.yml runs exactly those fi...

(GITHUB)

---

[style] ~48-~48: Would you like to use the Oxford spelling “parametrized”? The spelling ‘parametrised’ is also correct.
Context: ...ransform Module CompositionalDA.CLR, parametrised by a commutative ring R, a commutativ...

(OXFORD_SPELLING_Z_NOT_S)

---

[style] ~93-~93: Would you like to use the Oxford spelling “generalized”? The spelling ‘generalised’ is also correct.
Context: ...kup, 1≤ratio, ratio-antitone| the generalised forms the fouradjust-*` theorems are ...

(OXFORD_SPELLING_Z_NOT_S)

---

[misspelling] ~96-~96: This word is normally spelled as one.
Context: ...at test/property_bh.jl reads), in the sub-module Unsorted p π where `π : Permutation m...

(EN_COMPOUNDS_SUB_MODULE)

---

[duplication] ~96-~96: Possible typo: you repeated a word.
Context: ... in the sub-module Unsorted p π where π : Permutation m m stands for `ord = sortperm(q; rev = tr...

(ENGLISH_WORD_REPEAT_RULE)

---

[style] ~130-~130: Would you like to use the Oxford spelling “formalized”? The spelling ‘formalised’ is also correct.
Context: ...e reals is one is a fact about ℝ, not formalised. | | Reciprocal R n — n · ι ≈ 1 |...

(OXFORD_SPELLING_Z_NOT_S)

---

[uncategorized] ~162-~162: A comma may be missing after the conjunctive/linking adverb ‘Likewise’.
Context: ...lowance for this, not a proved bound. Likewise the real-valued clr in src/ against...

(SENT_START_CONJUNCTIVE_LINKING_ADVERB_COMMA)

---

[grammar] ~231-~231: The word ‘install’ is not a noun.
Context: ...ball's data/ directory; it prints the install steps and fails if the version differs....

(A_INSTALL)

🪛 Shellcheck (0.11.0)

proofs/tests/gate-selftest.sh

[info] 209-209: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 212-212: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 215-215: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 220-220: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 223-223: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 226-226: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 229-229: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 234-234: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 237-237: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 240-240: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 243-243: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 246-246: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 249-249: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

---

[info] 252-252: Expressions don't expand in single quotes, use double quotes for that.

(SC2016)

🔇 Additional comments (8)

proofs/tests/gate-selftest.sh (2)

264-264: Check the audit output in the pristine control separately.

run_gate && run_audit sends both outputs to $WORK/out.txt. If run_audit fails, its output replaces the gate output, and the diagnostics stay correct. This control is correct.

---

5-130: LGTM!

proofs/agda/CompositionalDA/BenjaminiHochberg/StepUp.agda (1)

81-280: LGTM!

proofs/agda/CompositionalDA/All.agda (1)

18-18: LGTM!

README.md (1)

37-40: LGTM!

proofs/PROOF-STATUS.md (1)

1-265: LGTM!

proofs/residue/benjamini-hochberg.residue (1)

1-125: LGTM!

proofs/residue/clr.residue (1)

1-96: LGTM!

---

📝 Summary

Summary by CodeRabbit

• New Features

  • Added formal proofs for the Benjamini–Hochberg step-up adjustment over exact rational values, including bounds and monotonicity when inputs are sorted.
  • Added results for mapping those properties back to original input order, assuming the supplied ordering is correct.

• Documentation

  • Clarified which properties are proved, tested or remain unverified, including limits around sorting and floating-point behaviour.

• Tests

  • Strengthened proof-gate checks to require both expected rejections of flawed proofs and acceptance of the unchanged proof set.

Walkthrough

The PR adds Agda proofs for Benjamini–Hochberg step-up adjustment over exact rationals, documents proof claims and remaining obligations, and replaces the proof gate self-test with stricter mutation and acceptance controls.

Changes

Proof model and validation

Layer / File(s)	Summary
Benjamini–Hochberg step-up model proofs/agda/CompositionalDA/BenjaminiHochberg/StepUp.agda, proofs/agda/CompositionalDA/All.agda, README.md	Adds a running-minimum adjustment model and proofs for bounds, descending order, tie handling, and monotonicity. The unsorted interface maps adjusted values through a supplied permutation. The gate imports the module, and the README states the sorted-input assumption and floating-point limitation.
Proof status and obligations proofs/PROOF-STATUS.md, proofs/residue/benjamini-hochberg.residue, proofs/residue/clr.residue	Documents Agda and Julia results, assumptions, gate results, and work not done. Adds residue records for Benjamini–Hochberg and CLR proof obligations.
Proof gate self-test proofs/tests/gate-selftest.sh	Uses a temporary proof-tree copy to check mutation application, expected rejection status and findings, negative controls, and pristine-tree acceptance.

Priority: ⬇️ Low

Estimated code review effort: 4 (Complex) | ~45 minutes

Change: Other

Merge Risk: ⚪ Minimal · up to 238c9

The proof and gate changes are ready for normal merge checks; the suggested per-control reset is not needed for the current controls.

Security Architecture Review

Security architecture risk: 🔵 Low · up to 238c9

The visible change is confined to formal guarantees and proof validation. One allocation-failure path can escape the self-test's disposable workspace, but normal CI still runs the pinned proof gate independently. No remotely reachable attack path was established.

Retained concerns

• Low · reliability · inferred: The self-test no longer terminates automatically when temporary-workspace allocation fails. An empty WORK value makes reset_tree delete or copy into absolute /agda and /tests paths before its library-file check can terminate execution. This breaks disposable-workspace ownership on the failure path. Damage requires corresponding filesystem authority; no privilege escalation or demonstrated remote trigger was established.

Security review details

Security Blast Radius

• inferred — The identified failure path affects the filesystem accessible to the user running the self-test, not an established tenant or service boundary. The reviewed CI context is a hosted proof-validation job with read-only repository permissions; those token permissions do not themselves constrain local filesystem access.

Trust Boundaries and Controls

• observed — CI verifies the downloaded Agda release checksum, sets its executable path, then runs bootstrap and the production proof check before the self-test. This independent enforcement counters interpreting the self-test's fallback library resolution as a demonstrated CI proof-gate bypass.
• observed — The self-test already accepted an environment-selected Agda executable and executed repository-defined mutation snippets before this PR. Head continues to use hardcoded snippets rather than introducing a caller-supplied mutation interface.

Hardening Proposals

• proposed — Make workspace allocation, copying and restoration explicitly fail-closed, and validate workspace identity before destructive cleanup. This would preserve disposable-tree ownership during setup and recovery failures.

🚥 Pre-merge checks | ✅ 5

✅ Passed checks (5 passed)

Check name	Status	Explanation
Title check	✅ Passed	The title clearly identifies the main changes: the Benjamini–Hochberg step-up proof and comprehensive gate self-test coverage.
Description check	✅ Passed	The description directly explains the new Agda proof, audit controls, updated proof-status records, and reported verification results.
Docstring Coverage	✅ Passed	Docstring coverage is 100.00% which is sufficient. The required threshold is 80.00%. Docstring coverage is scoped to functions touched by this diff. Analyzed 8 functions across 1 files. (6 skipped: 6 …
Linked Issues check	✅ Passed	Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check	✅ Passed	Check skipped because no linked issues were found for this pull request.

✨ Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

• Autopilot · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Autopilot is currently an internal CodeRabbit preview.

---

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{A rabbit checks each proof in turn,
Exact fractions mark the way.
Step-up values meet their bounds,
While open claims stay on display.
The gate tests changes, pass or fail,
Then hops away at close of day.}

_{Comment @coderabbitai help to get the list of available commands.}