Weakest Target-Direction Experiment Value

Abstract

Experiment value improves the weakest target direction and maximizes finite target-pair coverage, while trace-only gain can remain target-inert.

Theorem 1.1 (Experiments should improve weakest target directions).

$$\begin{array}{r}[\forall K,V:\mathrm{Type},P,W,W_a:\mathrm{LinearEnd}\left(K,V\right),\mathrm{RCLike}\left(K\right)\wedge \mathrm{NormedAddCommGroup}\left(V\right)\wedge \mathrm{InnerProductSpace}\left(K,V\right)\wedge \mathrm{FiniteDimensional}\left(K,V\right)\wedge P\circ P=P\wedge \mathrm{IsSymmetric}\left(P\right)\wedge \mathrm{IsSymmetric}\left(W\right)\wedge \mathrm{IsSymmetric}\left(W_a\right)\wedge \mathrm{Nonempty}\left(\left\{x\ne 0\wedge P\left(x\right)=x\mid x\in V\right\}\right)\wedge \exists \epsilon :\mathbb{R},0<\epsilon \wedge \forall x\in \left\{x\ne 0\wedge P\left(x\right)=x\mid x\in V\right\},\epsilon \le \mathrm{Rayleigh}\left(P\circ W_a\circ P,x\right)\Rightarrow \mathrm{iInfRayleigh}\left(P\circ W\circ P,\left\{x\ne 0\wedge P\left(x\right)=x\mid x\in V\right\}\right)<\mathrm{iInfRayleigh}\left(P\circ (W+W_a)\circ P,\left\{x\ne 0\wedge P\left(x\right)=x\mid x\in V\right\}\right)]\wedge \\ [\mathrm{trace}\left(0\right)<\mathrm{trace}\left(0+\mathrm{diag}\left(0,1\right)\right)\wedge \mathrm{diag}\left(1,0\right)\circ 0\circ \mathrm{diag}\left(1,0\right)=\mathrm{diag}\left(1,0\right)\circ (0+\mathrm{diag}\left(0,1\right))\circ \mathrm{diag}\left(1,0\right)\wedge \exists x,y:\mathrm{Fin}\left(2\right)\to \mathbb{R},x\left(0\right)\ne y\left(0\right)\wedge \mathrm{mulVec}\left(\mathrm{diag}\left(1,0\right)\circ (0+\mathrm{diag}\left(0,1\right))\circ \mathrm{diag}\left(1,0\right),x\right)=\mathrm{mulVec}\left(\mathrm{diag}\left(1,0\right)\circ (0+\mathrm{diag}\left(0,1\right))\circ \mathrm{diag}\left(1,0\right),y\right)]\wedge \\ [\forall X,C,R,Y,A:\mathrm{Type},q:X\to C,e:A\to X\to R,t:X\to Y,\mathrm{Fintype}\left(X\right)\wedge \mathrm{Fintype}\left(A\right)\wedge \mathrm{Nonempty}\left(A\right)\Rightarrow \exists b:A,\forall a:A,\mathrm{ncard}\left(\mathrm{experimentGain}\left(q,e\left(a\right),t\right)\right)\le \mathrm{ncard}\left(\mathrm{experimentGain}\left(q,e\left(b\right),t\right)\right)].\end{array}$$

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

Source. Repository-derived.

Commentary.

On a finite-dimensional real or complex inner-product space, the target projection is idempotent and symmetric, and both Gram operators are symmetric. A uniform positive Rayleigh gain on every nonzero target direction raises the infimum Rayleigh score strictly.

The displayed two-dimensional matrices give the contrast clause. The added operator raises trace in the second coordinate, but target compression to the first coordinate is unchanged and still merges states with distinct first coordinates.

For finite state and candidate types, experimentGain is the canonical set of current target defects removed by a candidate. Finite maximization constructs a candidate whose covered-pair cardinality is maximal.

References

• Truth anchor: D5/S3/ConceptDynamics/ExperimentDesign/WeakestTargetDirectionValue.weakest_target_direction_experiment_value
• Dependency: D5/S3/ConceptDynamics/Experiments/ExperimentRefinementGainMonotone