Observation Rank Monotonicity

Abstract

Observation-subspace rank is monotone under inclusion.

Theorem 1.1 (Adding observation settings cannot decrease rank).

$$\begin{array}{r}\forall K,V,I:\mathrm{Type},\\ [\mathrm{DivisionRing}(K)],[\mathrm{AddCommGroup}(V)],[\mathrm{Module}(K,V)],\\ [\mathrm{FiniteDimensional}(K,V)],\\ \forall U:I\to \mathrm{Submodule}(K,V),A,B:\mathrm{Set}(I),\\ A\subseteq B\Rightarrow \mathrm{finrank}(K,\mathrm{iSupOnSubtype}(A,U))\le \mathrm{finrank}(K,\mathrm{iSupOnSubtype}(B,U)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Linear/ObservationRankMonotonicity.observation_rank_monotonicity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Each setting contributes a subspace. Inclusion of selected index sets induces inclusion between their indexed subspace suprema, and finite-dimensional rank is monotone along that inclusion.

References

• Truth anchor: D5/S3/Observer/Linear/ObservationRankMonotonicity.observation_rank_monotonicity
• Dependency: D5/S3/Observer/Linear/ObservationRankSubmodularity