Complete Dominance and Observation Nonfaithfulness

Abstract

Complete dominance between distinct realized genotypes requires a nonfaithful observation language and disappears under a separating readout.

Theorem 1.1 (Complete dominance requires observation nonfaithfulness).

$$\begin{array}{r}\forall A,C,X,I:\mathrm{Type},\\ O:I\to \mathrm{Type},\\ realization:Sym2\left(A\right)\to C\to X,\\ q:(\forall i:I,X\to O_i),\\ a,b:A,c:C,\\ (\mathrm{realization}\left(s\left(a,a\right),c\right)\ne \mathrm{realization}\left(s\left(a,b\right),c\right)\wedge \mathrm{jointReadout}\left(q,\mathrm{realization}\left(s\left(a,a\right),c\right)\right)=\mathrm{jointReadout}\left(q,\mathrm{realization}\left(s\left(a,b\right),c\right)\right)\wedge \mathrm{jointReadout}\left(q,\mathrm{realization}\left(s\left(a,b\right),c\right)\right)\ne \mathrm{jointReadout}\left(q,\mathrm{realization}\left(s\left(b,b\right),c\right)\right))\Rightarrow \\ (\neg \mathrm{InjOn}\left(\mathrm{jointReadout}\left(q\right),\{\mathrm{realization}\left(s\left(a,a\right),c\right),\mathrm{realization}\left(s\left(a,b\right),c\right),\mathrm{realization}\left(s\left(b,b\right),c\right)\}\right)\wedge (\forall i:I,\neg \mathrm{Injective}\left((g:Sym2\left(A\right)\mapsto q\left(i,\mathrm{realization}\left(g,c\right)\right))\right))\wedge \exists d:X\to \mathrm{Prop},d\left(\mathrm{realization}\left(s\left(a,a\right),c\right)\right)\ne d\left(\mathrm{realization}\left(s\left(a,b\right),c\right)\right)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Faithfulness/CompleteDominanceObservationNonfaithfulness.complete_dominance_observation_nonfaithfulness (✓ std3). ∎

Source. Repository-derived.

Commentary.

A deterministic realization maps unordered diploid genotypes and a context to internal states. The canonical joint readout collects all coordinates of the chosen observation language.

Complete dominance identifies the profiles of the left homozygote and heterozygote while separating the heterozygote from the right homozygote. If the first two internal states are distinct, their shared profile makes the language noninjective on the three relevant states.

Consequently no coordinate already present can be injective on all genotypes under this realization and context. The equality predicate of the first state supplies another readout that distinguishes the latent pair, making the dependence on observation language explicit.

References

• Truth anchor: D5/S3/ConceptDynamics/Faithfulness/CompleteDominanceObservationNonfaithfulness.complete_dominance_observation_nonfaithfulness
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion