proofs(agda): PERMANOVA's p-value floor and which terms are withheld (rebased onto main)

The branch's Julia-side work -- the CLR linear model, the prevalence
filter, the complete-separation refusal, the significance statuses, the
config warning -- reached main refined through the upstream syncs, so
this rebase keeps main's side of every conflicted file and lands only
what was genuinely new on the branch:

- proofs/agda/MetaManifold/Permanova.agda: 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 names it.

The proofs depend on main's test/unit/test_permanova.jl, which is
already there; the Julia code the theorems model is byte-identical to
what the earlier syncs landed.

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

Author: hyperpolymath

.github/workflows/ci.yml

@@ -300,8 +300,9 @@ jobs:
           slug: JoshuaJewell/MetaManifold-WebUI
           fail_ci_if_error: false
 
-  # Machine-checked proofs of the Benjamini-Hochberg adjustment and the TSS/RLE
-  # scaling algebra (proofs/agda, proofs/agda/README.md).
+  # Machine-checked proofs of the Benjamini-Hochberg adjustment, the TSS/RLE
+  # scaling algebra and PERMANOVA's permutation bookkeeping (proofs/agda,
+  # proofs/agda/README.md).
   # Agda publishes no 2.6.4.3 binary, and agda-stdlib 2.1 requires Agda 2.6.4.x,
   # so the pair comes from Debian trixie, which packages exactly that pair with
   # pre-built library interfaces. The image is pinned by digest and the two

proofs/agda/MetaManifold/All.agda

@@ -12,3 +12,4 @@ module MetaManifold.All where
 import MetaManifold.Prelude
 import MetaManifold.BenjaminiHochberg
 import MetaManifold.Scaling
+import MetaManifold.Permanova