Completely Recessive Selection Order

Abstract

Completely recessive selection first appears at the ploidy order.

Theorem 1.1 (The selection signal has exact ploidy order).

$$\begin{gathered} \forall p\in \mathbb{N},s,x\in \mathbb{R}, \\ 1\le p\wedge 0<s\wedge s\le 1\wedge 0\le x\wedge x\le 1\wedge (s<1\vee x<1)\Rightarrow \\ \mathrm{let}(\mathrm{allRecessiveFrequency}(k:\mathbb{N},y:\mathbb{R}):=y^k, \\ \mathrm{meanFitness}(k:\mathbb{N},y:\mathbb{R}):=1-\mathrm{allRecessiveFrequency}(k,y)\cdot 1+\mathrm{allRecessiveFrequency}(k,y)\cdot 1-s, \\ \mathrm{selectedAlleleMass}(k:\mathbb{N},y:\mathbb{R}):=y-\mathrm{allRecessiveFrequency}(k,y)\cdot 1+\mathrm{allRecessiveFrequency}(k,y)\cdot 1-s, \\ \mathrm{updatedFrequency}(k:\mathbb{N},y:\mathbb{R}):=\frac{\mathrm{selectedAlleleMass}(k,y)}{\mathrm{meanFitness}(k,y)}, \\ \mathrm{selectionChange}(k:\mathbb{N},y:\mathbb{R}):=\mathrm{updatedFrequency}(k,y)-y) \\ \mathrm{meanFitness}(p,x)=1-s\cdot x^p\wedge \\ \mathrm{updatedFrequency}(p,x)=\frac{x-s\cdot x^p}{1-s\cdot x^p}\wedge \\ \mathrm{selectionChange}(p,x)=\frac{-s\cdot x^p\cdot 1-x}{1-s\cdot x^p}\wedge \\ \mathrm{IsBigOAtZero}(y,\mathrm{selectionChange}(p,y)--s\cdot y^p,y^{p+1})\wedge \\ \mathrm{analyticOrderAt}(\mathrm{selectionChange}(p),0)=p\wedge \\ \forall q\in \mathbb{N},p<q\Rightarrow \mathrm{analyticOrderAt}(\mathrm{selectionChange}(p),0)<\mathrm{analyticOrderAt}(\mathrm{selectionChange}(q),0). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S0/Asymptotics/EscapeProbability/CompletelyRecessiveSelectionOrder.completely_recessive_selection_order (✓ std3). ∎

Source. Repository-derived.

Commentary.

The all-recessive class has frequency x^p and fitness 1-s; the remaining class has fitness one. Mean fitness and selected allele mass are constructed from those two classes before normalization.

Positive selection is required for the exact-order clause: at s=0 the change vanishes identically. The frequency lies in [0,1], and the single endpoint s=x=1 is excluded because mean fitness is zero there.

The local remainder is big-O of x^(p+1). Mathlib’s analytic vanishing order records the nonzero degree-p leading factor, and the final clause makes the increase with ploidy explicit.

References

• Truth anchor: D5/S0/Asymptotics/EscapeProbability/CompletelyRecessiveSelectionOrder.completely_recessive_selection_order