The mathematical foundations thread

[hyperpolymath]

A standing thread for the statistics underneath the analyses — critique invited, rigour appreciated, literature welcome.

What is already machine-checked. Three properties are proved in Agda (proofs/agda/, checked in CI, no postulates or holes):

• the Benjamini–Hochberg adjustment over exact rationals, as bh_adjust computes it;
• the TSS and RLE size-factor scaling algebra over exact rationals;
• PERMANOVA's permutation bookkeeping: the reported min_p_value is the true 1/(B+1) floor and is attained, and a term's p-value is withheld exactly when no within-block permutation exchanges its labels.

Open ground this thread exists to work:

• Zero replacement. clr_welch uses GBM replacement (zCompositions::cmultRepl) with a replacement_delta cap; the Bayesian multiplicative alternative is on the roadmap. When is an imputed value a measurement, and what should a result say about how many it had?
• The negative-binomial GLM's dispersion behaviour at the bounds (theta pinned to 1e7 or 1e-8 is reported as boundary, not silently Poisson) — and the proposed glmGamPoi-style shrinkage.
• Compositional questions more broadly: CLR vs ILR as the working transform, prevalence filtering before zero replacement, and what a fold change even means when the denominator is a geometric mean.
• Exactness: which p-values deserve exact computation rather than the asymptotic default, and where higher-precision floats are the honest middle ground.

If you think a property in here deserves a proof — or that one of the proved properties is vacuous — say so in reply.