diff --git a/README.adoc b/README.adoc
index 824338d..93cbc35 100644
--- a/README.adoc
+++ b/README.adoc
@@ -305,3 +305,23 @@ If you use ZeroProb.jl in research, please cite:
 * **Author:** Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 * **GitHub:** https://github.com/hyperpolymath/ZeroProb.jl
 * **Issues:** https://github.com/hyperpolymath/ZeroProb.jl/issues
+
+== Applications in practice
+
+The worked case is permutation testing, as in MetaManifold's PERMANOVA
+integration (the theorems:
+link:https://github.com/hyperpolymath/MetaManifold-WebUI/blob/7d5e9a4/proofs/agda/MetaManifold/Permanova.agda[proofs/agda/MetaManifold/Permanova.agda],
+pinned on the fork's `main` at 7d5e9a4 and proposed upstream as
+link:https://github.com/JoshuaJewell/MetaManifold-WebUI/pull/55[PR #55],
+with the Julia oracle at
+link:https://github.com/hyperpolymath/MetaManifold-WebUI/blob/7d5e9a4/test/unit/test_permanova.jl[test/unit/test_permanova.jl]):
+for `B` permutations the smallest attainable p-value is the
+*floor* `1/(B+1)` -- attained exactly when no permutation reaches the
+observed statistic -- and the proved theorems pin that floor. What ZeroProb
+adds in practice is the honest language around it: a p-value at the floor is
+near-zero but *not* measure-zero, and any claim of the form "essentially
+impossible" must survive the same scrutiny as a density-ratio or
+epsilon-neighbourhood argument. Pipelines that report "p = 0" for
+insufficient permutations are publishing a measure-zero claim about a
+discrete test -- this library is where that claim goes to be checked
+before it reaches a figure.