Dominance Nontransitivity Countermodel

Abstract

A real phenotype on three unordered diploid genotypes makes complete dominance cyclic and nontransitive.

Theorem 1.1 (Complete dominance need not be transitive).

$$\begin{gathered} \exists a,b,d\in Fin(3),\exists P:Sym2(Fin(3))\Rightarrow \mathbb{R}, \\ a\ne b\wedge b\ne d\wedge a\ne d\wedge \\ P(s(a,a))=0\wedge P(s(a,b))=0\wedge P(s(b,b))=1\wedge \\ P(s(b,d))=1\wedge P(s(d,d))=2\wedge P(s(a,d))=2\wedge \\ (\ker (P,s(a,a),s(a,b))\wedge \neg \ker (P,s(a,b),s(b,b)))\wedge (\ker (P,s(b,b),s(b,d))\wedge \neg \ker (P,s(b,d),s(d,d)))\wedge \\ \neg (\ker (P,s(a,a),s(a,d))\wedge \neg \ker (P,s(a,d),s(d,d)))\wedge (\ker (P,s(d,d),s(d,a))\wedge \neg \ker (P,s(d,a),s(a,a))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementAlgebra/DominanceNontransitivityCountermodel.complete_dominance_not_transitive (✓ std3). ∎

Source. Repository-derived.

Commentary.

The displayed real phenotype is defined on the canonical symmetric square of three alleles. Each dominance edge is displayed using the source kernel condition, including the closing edge of the directed cycle.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementAlgebra/DominanceNontransitivityCountermodel.complete_dominance_not_transitive
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition