feat(analysis): PhILR, SBP and balance-dendrogram ILR bases with Agda proofs (#20) - #75
Merged
Merged
Conversation
Adds the Agda proof suite (Agda 2.6.4.3, stdlib 2.1, --safe --without-K,
no postulates) and the verification plan that fixes its scope:
- Composition.{Tree,Node,Sum}: shared vocabulary for #20 and #21
- ILR.SBP: SBP rows of a tree, Egozcue-Pawlowsky-Glahn conditions
- ILR.Contrast: centred, orthogonal, norm^2 = r s (r+s), from SBP row
- ILR.Kernel: injectivity on centred vectors under Cancellable
- ILR.Invariance / Orthonormal: via named LogHom / Normaliser seams
- ILR.Comb: comb tree = MetaManifold's Helmert default
- ILR.Integer: positive weights discharge the hypothesis; signed-weight
counterexample; philr's known-answer SBP
- scripts/check-proofs.sh + CI 'proofs' job with negative controls
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…#20) One engine (src/analysis/ilr_basis.jl) for the three bases that were refused as deferred: each basis is a rooted binary tree and balances are clade sums, O(D) per sample, no dense basis. Validation refuses non-bifurcating/unrooted trees, invalid SBPs (Egozcue & Pawlowsky-Glahn 2005) and taxa mismatches; provenance records tree/SBP SHA-256, dendrogram method and weights; >3 distinct SBPs raise a DANGER. The default Helmert basis and config hashes are unchanged. Tests: known answers, 17 expectations recomputed every run by an independent Julia reference (test/fixtures/ilr/ilr_reference.jl), R-gated philr/compositions/robCompositions cross-checks, negative controls, and scaling tests at 100/1000/10000 taxa. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
…20) Each ILR basis requires its own input (tree path, SBP path, dendrogram method) and forbids the others'; non-ILR normalization forbids all of them; SBP history entries must be SHA-256 hex. Mirrors _validate_ilr_inputs exactly; legacy documents still validate. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Required inputs sit next to the basis select; philr weights and SBP history are Evidence-Mode only; switching basis clears the other bases' inputs. ilrInputProblems mirrors the backend contract, pinned by tests/unit/ilr-basis-contract.test.ts. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
bench/ilr_bases/benchmark.jl times CLR, default ILR and the three bases at 100/1000/10000 taxa and warns over 5 min or 1 GiB (informational). bench/ilr_bases/regression_gate.jl measures the PR base and head on the same runner, interleaved A B A B, and fails if head allocates >10% more or its minimum time is >10% slower. A committed baseline cannot carry a 10% gate across shared runners. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com>
|
Important Review skippedBot user detected. To trigger a single review, invoke the ⚙️ Run configurationConfiguration used: Organization UI Review profile: ASSERTIVE Plan: Advanced Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
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 |
hyperpolymath
approved these changes
Sep 26, 2026
hyperpolymath
marked this pull request as ready for review
September 26, 2026 09:47
arena-ai-coding-agent Bot
pushed a commit
that referenced
this pull request
Sep 26, 2026
Resolves the .gitignore clash by keeping both additions: upstream's docs/formal/ negations plus this branch's docs/triage/ negations and the derived-patches ignore.
arena-ai-coding-agent Bot
pushed a commit
that referenced
this pull request
Sep 26, 2026
Owner asked to close the branch (selector correction). Archive its true delta (e33e10f..d94ecd4, 41 files) as a verified byte-exact patch plus restore instructions, and correct the report: the branch was stale docs (predates the DOI/ILR merges), not DOI-deleting — a merge would not have reverted PR #74/#75. The README.md deletion and missing SPDX headers were the real reasons to close it.
hyperpolymath
added a commit
that referenced
this pull request
Sep 26, 2026
…67 archive (#76) ## Summary Triages the notification backlog (see `docs/triage/2026-09-26-notification-backlog.md`). Docs + tooling only; no application-logic changes. **Already done alongside (not in this diff):** - Closed fork #73 as a wrong-base duplicate of parent #7 (same branch, clean upstream). - Owner merged fork #75 mid-triage → fork #20 auto-closed. Post-merge verification still owed once CI runs. - Deleted stale branch `arena/01a0db67` at owner's request after archiving it here. ## Changes - `docs/triage/2026-09-26-notification-backlog.md` — every open PR/issue on fork + parent triaged; CI outage diagnosed (file-based workflows `startup_failure` repo-wide since 2026-09-25 22:19 UTC; settings/platform-side, owner steps in runbook). - `docs/triage/pr7-split/` — parent #7's 319-file change as 14 disjoint stacks (`STACKS.md` review guide, `RUNBOOK.md` with merge-as-is vs stacked-PRs options, `make-stacks.sh` regenerates + verifies: disjoint, full coverage, sequential apply reproduces the branch tree exactly). - `docs/triage/db67-rescue/` — archived deleted branch as a verified byte-exact patch + restore instructions. - `.gitignore` — track `docs/triage/`, ignore derived 4.5 MB stack patches. ## Verification - `scripts/check-spdx.sh`: OK (new .md/.sh carry fork-series headers). - Format essentials (LF, final newline, no trailing WS in non-prose): clean. - `make-stacks.sh`: 14 stacks, disjoint, cover all 319 files, reproduce branch tree exactly. - `db67-rescue/deleted-branch.patch`: recreates the deleted branch tree exactly. ## Note on CI File-based workflows cannot start repo-wide right now (the outage diagnosed in the report), so expect `startup_failure` — unrelated to this docs-only change. Re-run once the owner fixes Actions. --------- Co-authored-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.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
1 participant
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.
Implements #20 (ILR bases: phylogenetic/PhILR, sequential binary partition, balance dendrogram) with an Agda proof layer shared with the #21 zero-handling work.
What changes
src/analysis/ilr_basis.jl: every basis is a rooted binary tree; balances are clade sums in one post-order pass (O(D)per sample, no dense basis matrix). Pure Julia, no new dependency (philr/compositions/robCompositions are not inrenv.lock).ilrInputProblems). Configs without the new fields hash exactly as before; the default Helmert balances are byte-identical.proofs/agda/(newproofsCI job): contrast sums, orthonormality, injectivity (with its positive-weight hypothesis), scale/perturbation invariance, comb = Helmert, SBP validity. Mapped to tests indocs/formal/verification-plan.md.test/fixtures/ilr/ilr_reference.jl) recomputes all 17 committed expectations (philr ×9,compositions::ilr, Rhclustvariation/merges/balances) every run; R cross-checks where the packages exist; negative controls.bench/ilr_bases/benchmark.jl(100/1 000/10 000 taxa, warns >5 min / >1 GiB, informational) and a PR-only gate (bench/ilr_bases/regression_gate.jl) that measures base vs head on the same runner, interleaved A B A B, and fails on >10 % more allocation or >10 % slower minimum time for CLR and default ILR. Why not a committed baseline: cross-host timings are noise (the repo's existing policy); allocations are deterministic, and same-runner A/B cancels runner drift.IlrBasisInputs.tsx).docs/compliance/standards-alignment.md).Please note
config/ci/lint_source.jl; Agda proofs type-check locally; frontend: 613 tests pass. CI is the first execution of the Julia tests, the reference and the benchmarks.startup_failure:ci.ymlhas failed to start on every branch since ~2026-09-25 22:19, before this PR. Needs a look from someone with admin access (Actions settings / allowed actions / org policy).Execution.prepare_analysis_tableisO(D²)time and transient allocation per sample (freshlog_col[1:i]slice per balance; ~400 MB per sample at 10 000 taxa). Kept byte-identical here; the comb tree reproduces it inO(D)and could replace it separately.allOfiflacksrequired;bun run typecheckfails with TS5090; a CladeCumulus JSX error; remaining Python (test_exact_summariesshells topython3fractions;install.jlpipx cutadapt/multiqc) is awaiting an owner decision.Closes #20 once CI is green.