From c9af375567b29efdc671315d43878d4df48526e9 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 10:31:50 +0100 Subject: [PATCH 1/2] docs: an Applications-in-practice section -- the discipline earned on a real pipeline Appends a worked real-world case to README.adoc: the concrete situation in an amplicon-sequencing pipeline in production use where the type, the OND discipline or the algebra earns its keep -- and what the untyped or undisciplined alternative gets wrong. Documentation only; no code changes. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- README.adoc | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/README.adoc b/README.adoc index 824338d..5600081 100644 --- a/README.adoc +++ b/README.adoc @@ -305,3 +305,17 @@ If you use ZeroProb.jl in research, please cite: * **Author:** Jonathan D.A. Jewell * **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: 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. From bf71be9737b786083deb28fac4baf21ba2d55701 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Thu, 15 Oct 2026 10:47:34 +0100 Subject: [PATCH 2/2] docs: link the PERMANOVA worked case directly (CodeRabbit, PR #63) The section named MetaManifold's PERMANOVA integration without a link. It now points at the theorems where they live, pinned: the fork's proofs/agda/MetaManifold/Permanova.agda at 7d5e9a4, the upstream proposal PR #55, and the Julia oracle test_permanova.jl -- so a reader can check the floor lemma and its oracle from the sentence that cites them. Generated by Mistral Vibe. Co-Authored-By: Mistral Vibe --- README.adoc | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/README.adoc b/README.adoc index 5600081..93cbc35 100644 --- a/README.adoc +++ b/README.adoc @@ -309,7 +309,13 @@ If you use ZeroProb.jl in research, please cite: == Applications in practice The worked case is permutation testing, as in MetaManifold's PERMANOVA -integration: for `B` permutations the smallest attainable p-value is the +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