Fixed Observation Dominance Asymmetry

Abstract

Complete dominance is asymmetric under one fixed indexed observation language.

Theorem 1.1 (Fixed-observation complete dominance is asymmetric).

$$\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{let}profile:=\mathrm{jointReadout}\left(q\right),\\ \mathrm{dominates}\left(l:A,r:A\right):\mathrm{Prop}:=(\mathrm{profile}\left(\mathrm{realization}\left(s\left(l,l\right),c\right)\right)=\mathrm{profile}\left(\mathrm{realization}\left(s\left(l,r\right),c\right)\right)\wedge \mathrm{profile}\left(\mathrm{realization}\left(s\left(l,r\right),c\right)\right)\ne \mathrm{profile}\left(\mathrm{realization}\left(s\left(r,r\right),c\right)\right))\mathrm{in}\\ \mathrm{dominates}\left(a,b\right)\Rightarrow \neg \mathrm{dominates}\left(b,a\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/RefinementGeometry/FixedObservationDominanceAsymmetry.fixed_observation_dominance_asymmetric (✓ std3). ∎

Source. Repository-derived.

Commentary.

Diploid genotypes are unordered pairs of alleles. The deterministic realization map sends each genotype and context to an internal state, and the canonical joint readout constructs the fixed observation language’s profile.

Dominance of the left allele means that the left homozygote and shared heterozygote have equal profiles while that heterozygote and the right homozygote have unequal profiles. Reversing dominance would require the latter two profiles to be equal, which is impossible.

References

• Truth anchor: D5/S3/ConceptDynamics/RefinementGeometry/FixedObservationDominanceAsymmetry.fixed_observation_dominance_asymmetric
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion