Experiment Value Is Kernel Reduction

Abstract

An experiment is valuable when it removes target residual pairs, independently of the nominal size of its response space.

Lemma 1.1 (No target residual pair is equivalent to factorization).

$$\begin{array}{r}\forall E,X,R,Y:\mathrm{Type},\\ A:\mathrm{Set}\left(E\right),r:E\to \left(X\to R\right),t:X\to Y,\\ \mathrm{Nonempty}\left(X\right)\Rightarrow \mathrm{TargetIdentifiable}\left(A,r,t\right)⟺\exists f:(\forall a:A,R)\to Y,t=f\circ \mathrm{jointReadout}\left(\mathrm{restrict}\left(r,A\right)\right).\end{array}$$

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

Source. Repository-derived.

Commentary.

A target residual pair consists of two states that every allowed experiment treats alike even though the target separates them. Target identifiability is exactly the absence of such a pair.

For a nonempty state space, absence of residual pairs says that the target is constant on every fiber of the joint allowed-experiment readout. The existing identifiability criterion then supplies a single map that recovers the target from the complete response tuple, and any such factorization rules out a residual pair.

Indexing the joint response tuple by the subtype of allowed experiments ensures that the factorization uses precisely the admitted family, not experiments outside it.

Theorem 1.2 (Experiment value is reduction of the target residual kernel).

$$\begin{array}{r}(\mathrm{card}\left(\mathrm{Fin}\left(1000\right)\right)>\mathrm{card}\left(Bool\right)\wedge \\ \mathrm{residualPairs}\left(\varnothing ,large,target\right)=\mathrm{residualPairs}\left(univ,large,target\right)\wedge \\ (\mathrm{TargetIdentifiable}\left(\varnothing ,large,target\right)⟺\mathrm{TargetIdentifiable}\left(univ,large,target\right)))\wedge \\ (\mathrm{card}\left(Bool\right)=2\wedge \\ \mathrm{residualPairs}\left(\varnothing ,bit,target\right)=\{(false,true),(true,false)\}\wedge \\ \mathrm{residualPairs}\left(univ,bit,target\right)=\varnothing \wedge \\ \neg \mathrm{TargetIdentifiable}\left(\varnothing ,bit,target\right)\wedge \mathrm{TargetIdentifiable}\left(univ,bit,target\right)).\end{array}$$

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

Source. Repository-derived.

Commentary.

On the Boolean state space, the large-output experiment is constant: both states receive the same element of a response type with one thousand symbols. Allowing that experiment therefore leaves the residual-pair set unchanged and does not improve target identifiability.

With no allowed bit experiment, the identity target has exactly the two ordered off-diagonal Boolean residual pairs. Once the identity bit experiment is allowed, equal responses force equal states, so the residual-pair set becomes empty and the target is identifiable.

Thus a two-symbol response can be decisive while a strictly larger response space is inert. The mathematical value of the experiment is the target-relevant kernel it removes, rather than the cardinality of its nominal output alphabet.

References

• Truth anchor: D5/S3/ConceptDynamics/Experiment/ExperimentValueIsKernelReduction.experiment_value_is_kernel_reduction
• Truth anchor: D5/S3/ConceptDynamics/Experiment/ExperimentValueIsKernelReduction.targetIdentifiable_iff_factorization
• Dependency: D5/S3/ConceptDynamics/Experiment/ExperimentIdentifiability