Target Visibility and Condition Cost

Abstract

Exact target visibility carries a canonical target-specific condition cost.

Theorem 1.1 (Visibility determines a unique minimum-norm cost certificate).

$$\begin{array}{c}\forall K,State,Observation:\mathrm{Type},\\ \mathrm{RCLike}(K)\wedge \mathrm{NormedAddCommGroup}(State)\wedge \mathrm{InnerProductSpace}(K,State)\wedge \mathrm{FiniteDimensional}(K,State)\wedge \\ \mathrm{NormedAddCommGroup}(Observation)\wedge \mathrm{InnerProductSpace}(K,Observation)\wedge \mathrm{FiniteDimensional}(K,Observation)\Rightarrow \\ \forall M:\mathrm{LinearMap}(K,State,Observation),v:State,\\ (\forall x,y:State,M(x)=M(y)\Rightarrow ⟨v,x⟩=⟨v,y⟩)⟺(\exists !(s,a):State\times Observation,\\ s\in (\ker (M){)}^{\perp }\wedge \\ {\mathrm{M}}^{\ast }(a)=v\wedge \\ a=M(s)\wedge \\ (\forall b:Observation,{\mathrm{M}}^{\ast }(b)=v\Rightarrow \Vert a\Vert \le \Vert b\Vert )\wedge \\ {\Vert a\Vert }^2=⟨v,s⟩).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Conditioning/TargetVisibilityConditionCost.target_visibility_condition_cost (✓ std3). ∎

Source. Repository-derived.

Commentary.

The measurement map is defined on arbitrary finite-dimensional inner-product spaces over a real or complex scalar field. A target is exactly visible when its Riesz functional is constant on every measurement fiber.

The theorem constructs the state Gramian from the measurement and its adjoint. It then exposes the unique Gram preimage orthogonal to the hidden kernel and the induced observation coefficient.

That coefficient solves the adjoint equation, has minimum norm among all such solutions, and its squared norm equals the target quadratic form on the canonical Gram preimage. This is the target-specific condition cost without introducing a substitute pseudoinverse.

Pinned Mathlib supplies adjoint-range duality, equality of the Gram and adjoint ranges, orthogonal decomposition, and Pythagoras. Repository searches found no existing theorem combining all public clauses.

References

• Truth anchor: D5/S3/Observer/Conditioning/TargetVisibilityConditionCost.target_visibility_condition_cost