Target-Relative Experiment Superiority

Abstract

Incomparable experiments each serve a target that the other does not.

Theorem 1.1 (Incomparable experiments have opposite target advantages).

$$\begin{gathered} \forall X,E_1,E_2:\mathrm{Type}, \\ {q}_1:X\to E_1,q_2:X\to E_2, \\ (\neg \mathrm{Refines}\left(q_1,q_2\right)\wedge \neg \mathrm{Refines}\left(q_2,q_1\right))\Rightarrow \\ ((\exists t_1:X\to E_1,\mathrm{Refines}\left(t_1,q_1\right)\wedge \neg \mathrm{Refines}\left(t_1,q_2\right))\wedge (\exists t_2:X\to E_2,\mathrm{Refines}\left(t_2,q_2\right)\wedge \neg \mathrm{Refines}\left(t_2,q_1\right))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiments/TargetRelativeExperimentSuperiority.incomparable_experiments_have_opposite_target_advantages (✓ std3). ∎

Source. Repository-derived.

Commentary.

Choose the first experiment itself as the first target. Reflexivity makes that target available from the first experiment, while the assumed non-refinement excludes it from the second.

Choosing the second experiment itself gives the symmetric witness. Both directional target advantages occur in the public conclusion.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiments/TargetRelativeExperimentSuperiority.incomparable_experiments_have_opposite_target_advantages
• Dependency: D5/S3/ConceptDynamics/Refinement/RefinementReflexivity