Static Exact Experiment Design

Abstract

Two complementary change experiments are jointly exact, and every exact static selection contains both.

Theorem 1.1 (Both complementary experiments are necessary and sufficient).

$$\begin{array}{r}\forall m:\mathrm{Fin}(3),E_X(m):=\mathrm{decide}(m=1),\\ \forall m:\mathrm{Fin}(3),E_Y(m):=\mathrm{decide}(m=2),\\ \forall e:Bool,m:\mathrm{Fin}(3),q(e,m):=\mathrm{if}(e,E_Y(m),E_X(m)),\\ (\forall e:Bool,\neg \mathrm{Injective}(\mathrm{readoutAt}(q,e)))\wedge \mathrm{Injective}(\mathrm{jointReadout}(q))\wedge (\forall J:\mathrm{Finset}(Bool),\mathrm{Injective}(\mathrm{jointReadout}(\mathrm{restrict}(q,J)))\Rightarrow J=\{false,true\}).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ExperimentDesign/StaticExactExperimentDesign.static_exact_design (✓ std3). ∎

Source. Repository-derived.

Commentary.

The state carrier has three model labels. The false experiment role detects only label one, while the true role detects only label two.

Each response alone merges two labels. Their canonical joint readout is injective, and an injective static selection of the two roles must be the full Boolean selection.

References

• Truth anchor: D5/S3/ConceptDynamics/ExperimentDesign/StaticExactExperimentDesign.static_exact_design
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion