Polyploid Allele Complementarity

Abstract

Mixed polyploid genotypes obstruct Boolean allele complementarity.

Theorem 1.1 (Allele events overlap exactly beyond haploidy).

$$\begin{array}{c}(\forall p:Nat,2\le p\Rightarrow \mathrm{Nonempty}\left(\mathrm{intersection}\left(\{g:\mathrm{Fin}\left(p\right)\to Bool\mid \exists i:\mathrm{Fin}\left(p\right),\mathrm{apply}\left(g,i\right)=false\},\{g:\mathrm{Fin}\left(p\right)\to Bool\mid \exists i:\mathrm{Fin}\left(p\right),\mathrm{apply}\left(g,i\right)=true\}\right)\right))\wedge \\ (\forall p:Nat,1\le p\Rightarrow (\{g:\mathrm{Fin}\left(p\right)\to Bool\mid \exists i:\mathrm{Fin}\left(p\right),\mathrm{apply}\left(g,i\right)=true\}=\mathrm{complement}\left(\{g:\mathrm{Fin}\left(p\right)\to Bool\mid \exists i:\mathrm{Fin}\left(p\right),\mathrm{apply}\left(g,i\right)=false\}\right)⟺p=1)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Negation/PolyploidAlleleComplementarity.polyploid_allele_events_overlap_and_haploid_complement (✓ std3). ∎

Source. Repository-derived.

Commentary.

A biallelic p-copy genotype is a function from Fin(p) to Bool. For p at least two, an explicit mixed genotype has one false locus and one true locus, so both allele-presence events occur.

For every nonempty genotype carrier, the true-allele event is the set complement of the false-allele event exactly when p equals one. At higher ploidy the same mixed genotype prevents equality.

The predicates and their carrier are displayed directly; no genotype event is defined in terms of the claimed intersection or complement relation.

References

• Truth anchor: D5/S3/ConceptDynamics/Negation/PolyploidAlleleComplementarity.polyploid_allele_events_overlap_and_haploid_complement