Experiment Identifiability

Abstract

A target is identifiable exactly when it factors through the joint experiment readout, equivalently when experiment-indistinguishability implies equal targets.

Theorem 1.1 (Target identifiability has three equivalent forms).

$$\begin{array}{r}\forall S,X,Y:\mathrm{Type},R:S\to \mathrm{Type},\\ e:\forall u:S,X\to R_u,t:X\to Y,\\ \mathrm{Nonempty}\left(X\right)\Rightarrow \mathrm{TFAE}[\exists f:\prod _{u:S}{R}_u\to Y,t=f\circ \mathrm{jointReadout}\left(e\right),\\ \mathrm{jointKernel}\left(e\right)\subseteq \mathrm{targetKernel}\left(t\right),\\ \forall x,y:X,(\forall u:S,e\left(u,x\right)=e\left(u,y\right))\Rightarrow t\left(x\right)=t\left(y\right)].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Experiment/ExperimentIdentifiability.identifiable_tfae (✓ std3). ∎

Source. Repository-derived.

Commentary.

An experiment family records one response for every index, and its joint readout collects those responses into a dependent tuple. The target is identifiable when a single factor map recovers the target value from that complete response tuple.

The joint kernel contains exactly the state pairs that every experiment fails to distinguish. Containment in the target kernel says that each such pair has the same target value, which is the pointwise fiber-constancy condition in the third clause.

On a nonempty state space, the answerability criterion turns fiber constancy into a factor through the joint readout. Membership in the joint kernel is componentwise equality across all experiment indices, completing the equivalence with kernel containment.

The Boolean examples separate the boundary: an identity experiment identifies the identity target, while a constant experiment fails factorization, kernel containment, and fiber constancy.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiment/ExperimentIdentifiability.identifiable_tfae
• Dependency: D5/S0/Rewriting/Quotients/AnswerabilityCriterion
• Dependency: D5/S3/ConceptDynamics/Faithfulness/JointFaithfulnessLeibnizCriterion