Proofs/permanova permutations by hyperpolymath · Pull Request #127 · hyperpolymath/MetaManifold-WebUI

hyperpolymath · 2026-10-15T02:04:29Z

Summary

Adds proofs/agda/MetaManifold/Permanova.agda: machine-checked proofs of the two things run_permanova in src/analysis/analysis.jl decides for itself rather than taking from vegan — the reported min_p_value (the 1/(B+1) floor, never raised by more permutations, and attained) and which terms have their p-value withheld (_varies_within_any_block, exactly when no within-block permutation exchanges the term's labels). With the import in All.agda (so the axiom audit reaches it), the README's PERMANOVA section and theorem-to-code map entries, and the Agda CI job's comment.

The Julia side this branch originally carried (the CLR method chain, the vsearch helper, the server entry-point tests) reached main refined through the upstream syncs — as #112, #113 and the occupancy line — so nothing of it is re-landed here.

Branch repair

The branch as first opened was built on upstream's history and carried three superseded commits, so it was CONFLICTING against main — which is also why no workflow posted a check: with no merge ref, GitHub cannot start a pull_request workflow at all, and only the external scanners ran. The branch is now a single commit rebased onto current main; every content change is byte-identical to the original rebase commit (e9bb4e2, whose conflict resolution already kept main's side of every touched file — both sides were identical, so the diff applies clean).

Type of change

🐛 Bug fix (non-breaking change that fixes an issue)
✨ New feature (non-breaking change that adds functionality)
💥 Breaking change (would change existing behaviour)
🕳️ Soundness fix (fixes a checker/proof false-negative)
📖 Documentation
🧹 Refactor / tech debt (behaviour-preserving)
⚡ Performance
🔧 Build / CI / tooling (a new machine-checked proof module and its CI wiring; no runtime code changes)

How has this been verified?

CI on this PR: the Agda proofs job type-checks MetaManifold/All.agda (which now imports Permanova) with the pinned Agda 2.6.4.3 + agda-stdlib 2.1, and the Julia tests job runs the full unit suite including test/unit/test_permanova.jl, the code the theorems model.
The proof file is byte-identical to e9bb4e2's, whose theorems were checked there; the only re-applied deltas are the All.agda import, the README entries and the ci.yml comment, each applied mechanically from that commit's diff.

Checklist

My commits are signed (git commit -S). — the signing key's passphrase was not available in the session that produced this commit
I ran the project's own checks/tests locally and they pass. — the Julia pin tests and root-shape suite pass locally; the Agda type-check is CI's pinned toolchain, which is authoritative here
New files carry the correct SPDX-License-Identifier (code/config MPL-2.0, prose CC-BY-SA-4.0); I did not relicense existing files. — Permanova.agda carries AGPL-3.0-only, matching every other file under proofs/agda/
Docs are updated, and no public claim now overstates what the code does. — the proofs README gains the PERMANOVA section and theorem-to-code map entries
I have not introduced a soundness hole (or I have flagged where I might have). — no postulates, no holes; --safe --without-K as everywhere else in the tree

Notes for reviewers

Nothing here changes runtime behaviour; the risk surface is the Agda job's type-check and the axiom audit. If this unit is later proposed upstream, it should be re-cut fresh from upstream main per the absorption register's runbook, not replayed from this fork branch.

Generated by Mistral Vibe.
Co-Authored-By: Mistral Vibe vibe@mistral.ai

coderabbitai · 2026-10-15T02:04:40Z

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 13 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

⚙️ Run configuration

Configuration used: Organization UI
Review profile: ASSERTIVE
Plan: Advanced
Run ID: 914e80c3-b4cd-4b28-a7e7-ecf2842f6db2

📥 Commits

Reviewing files that changed from the base of the PR and between e2dfa05 and fee3a9b.

📒 Files selected for processing: 4

.github/workflows/ci.yml
proofs/agda/MetaManifold/All.agda
proofs/agda/MetaManifold/Permanova.agda
proofs/agda/README.md

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

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

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

hyperpolymath · 2026-10-15T02:37:09Z

Conflicts with main resolved by rebasing onto the current tip (single commit 3809be0).

What the resolution did, and why: the branch's Julia-side work -- the CLR linear model (clr_welch), the prevalence filter, the complete-separation refusal, the significance statuses, the config warning -- reached main refined through the upstream syncs (verified: main's differential.jl already carries the complete-separation paths; was_computed carries the full status set; test/unit/test_permanova.jl is already there). So every conflicted file takes main's side, and what lands is only what was genuinely new on the branch:

proofs/agda/MetaManifold/Permanova.agda (new) -- the two things run_permanova decides for itself rather than taking from vegan: the reported min_p_value (the 1/(B+1) floor, never raised by more permutations) and which terms have their p-value withheld (_varies_within_any_block, exactly when no within-block permutation exchanges the term's labels);
its import in All.agda, so the axiom audit reaches it;
the README's PERMANOVA sections and theorem-to-code map;
the Agda proofs job's comment in ci.yml names it (the branch's version of that job still used third-party actions, refused by this account's allow-list; main's pinned structure kept).

Verified locally: the full proof tree type-checks under Agda 2.6.4.3 + stdlib 2.1 (agda MetaManifold/All.agda, clean), proofs/tests/axiom-audit.sh reports 5 modules reachable and clean, and test/unit/test_install_pins.jl passes 222/222.

Known collateral: the Julia tests job will fail at Build frontend until #140 (the #124 React 19/vite 8 repair) merges -- that breakage is main's, not this branch's; the Agda proofs job, which is what this PR is about, is green locally and should be green in CI.

hyperpolymath · 2026-10-15T02:49:46Z

@coderabbitai review

coderabbitai · 2026-10-15T02:49:52Z

⚠️ Action not completed

Review rate limited.

Note: CodeRabbit is an incremental review system and does not re-review already reviewed commits. This command is applicable only when automatic reviews are paused.

The two things run_permanova decides for itself rather than taking from vegan, proved: the reported min_p_value (the 1/(B+1) floor, never raised by more permutations) and which terms have their p-value withheld (_varies_within_any_block, exactly when no within-block permutation exchanges the term's labels). Rebuilt for this fork's main: the branch this PR carried was based on upstream's history with three superseded commits whose content main already absorbed (#106, #112, #113), so it conflicted and no workflow could post a check. The proof file is byte-identical to the branch's; the import in All.agda, the README's PERMANOVA section and theorem-to-code map entries, and the Agda job's comment are re-applied onto main's side of each file (both sides were identical, so the diff applies clean). Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>

sonarqubecloud · 2026-10-15T03:36:11Z

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud

13 conflicted files, all the fork's sync-policy set. This branch's PERMANOVA proof content already landed on main via #127/#154 (Permanova.agda is byte-identical), so main's versions win throughout; the net tree change against main is upstream's vsearch entry-point test, not yet absorbed. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe <vibe@mistral.ai>

hyperpolymath force-pushed the proofs/permanova-permutations branch from f59842c to 3809be0 Compare October 15, 2026 02:36

hyperpolymath force-pushed the proofs/permanova-permutations branch from 3c16cdb to e9bb4e2 Compare October 15, 2026 03:02

hyperpolymath force-pushed the proofs/permanova-permutations branch from e9bb4e2 to 161d86a Compare October 15, 2026 03:28

Merge branch 'main' into proofs/permanova-permutations

fee3a9b

hyperpolymath merged commit 016d46d into main Oct 15, 2026
14 checks passed

hyperpolymath deleted the proofs/permanova-permutations branch October 15, 2026 03:56

Navigation Menu

Repository navigation

Proofs/permanova permutations - #127

Proofs/permanova permutations#127
hyperpolymath merged 2 commits into
mainfrom
proofs/permanova-permutations

hyperpolymath commented Oct 15, 2026 •

edited

Loading

Uh oh!

coderabbitai Bot commented Oct 15, 2026 •

edited

Loading

Review limit reached

Uh oh!

hyperpolymath commented Oct 15, 2026

Uh oh!

hyperpolymath commented Oct 15, 2026

Uh oh!

coderabbitai Bot commented Oct 15, 2026 •

edited

Loading

Uh oh!

sonarqubecloud Bot commented Oct 15, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

hyperpolymath commented Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Branch repair

Type of change

How has this been verified?

Checklist

Notes for reviewers

Uh oh!

coderabbitai Bot commented Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Review limit reached

Uh oh!

hyperpolymath commented Oct 15, 2026

Uh oh!

hyperpolymath commented Oct 15, 2026

Uh oh!

coderabbitai Bot commented Oct 15, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

sonarqubecloud Bot commented Oct 15, 2026

Quality Gate passed

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

hyperpolymath commented Oct 15, 2026 •

edited

Loading

coderabbitai Bot commented Oct 15, 2026 •

edited

Loading

coderabbitai Bot commented Oct 15, 2026 •

edited

Loading