feat(proofs): unify Agda suite, audit gates, and run-notices catalogue

[arena-ai-coding-agent]

Summary

This PR unifies the full formal-verification Agda proof suite, resolves module and audit collisions across the estate, and imports the memory/numerics audit and run-notices catalogue.

Changes Included

1. Unify Agda Formal Verification Suite ():

   • Imports and type-checks all 22 modules across the codebase in a single gate entry:
     • Numeric Core (Issue Add a validated Julia statistics layer with exact counts/rationals and higher precision #1): Prelude, Proportions, ExactCounts, PermutationTest, BenjaminiHochberg, DecimalRounding
     • Composition (Issue feat(analysis): Advanced zero handling — glmGamPoi dispersion, Bayesian multiplicative replacement, multiplicative replacement with delta  #21): Composition.Tree, Composition.Node, Composition.Sum
     • ILR Bases (Issue feat(analysis): ILR basis — phylogenetic ILR (PhILR), sequential binary partition (SBP), balance dendrogram  #20): ILR.SBP, ILR.Contrast, ILR.Kernel, ILR.Invariance, ILR.Orthonormal, ILR.Comb, ILR.Integer
     • Evidence Mode (Issue feat(ui): Full Evidence Mode — epistemic editor, fiber visualizer #7): Evidence.Prelude, Evidence.Residual, Evidence.Echo, Evidence.Warrant, Evidence.Signed, Evidence.Decision
   • Uses non-polluting namespace imports to avoid symbol collisions (e.g. Sign).

2. Gate Machinery & Self-Test Harmonization:

   • proofs/tests/axiom-audit.sh: Audits all 23 modules under MetaManifold/, verifying --safe, zero postulates, no FFI/holes, and 100% reachability from MetaManifold.All.
   • proofs/tests/gate-selftest.sh: Verified 10/10 mutation and control checks reject deliberate breakages and accept the pristine tree.

3. Memory, Numerics, and Backend Audit:

   • Adds docs/audit/2026-09-26-memory-numerics-warning-audit.md (21-finding read-and-trace audit).
   • Adds docs/notices/README.md and docs/notices/catalogue.md (60-item run-notice taxonomy and contracts).
   • Updates .gitignore to track docs/notices/.

4. Hygiene & Governance:

   • SPDX licence headers added across all new documentation (docs/statistics/formal-verification.md, proofs/HANDOFF.md, proofs/PROOF-STATUS.md).
   • Clean formatting (scripts/check-format.sh -> OK on 502 files).

Verification

Check	Result
proofs/bootstrap.sh	OK (all 23 modules checked cleanly)
proofs/tests/axiom-audit.sh	OK (23/23 reachable, clean)
proofs/tests/gate-selftest.sh	10/10 controls pass
scripts/check-spdx.sh	OK (381 files covered)
scripts/check-format.sh	OK (502 files checked)

[coderabbitai]

Important

Review skipped

Bot user detected.

To trigger a single review, invoke the @coderabbitai review command.

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 8a83fd9a-0212-4248-83ed-c0d84e06dab7

You can disable this status message by setting the reviews.review_status to false in the CodeRabbit configuration file.

Use the checkbox below for a quick retry:

• 🔍 Trigger review

---

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

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