Observer Innovation Equation

Abstract

A strict Gram spectral-floor drop identifies the unique innovation zero.

Theorem 1.1 (The new Gram floor is the unique innovation zero).

$$\forall K\in \mathrm{Type}\left(\right),V\in \mathrm{Type}\left(\right),iota\in \mathrm{Type}\left(\right),feature\in \mathrm{Sum}\left(iota,\mathrm{Unit}\left(\right)\right)\to V,alphaOld\in \mathrm{Real}\left(\right),alphaNew\in \mathrm{Real}\left(\right),letoldGram=\mathrm{gram}\left(K,\mathrm{compose}\left(feature,\mathrm{inl}\left(\right)\right)\right);letfullGram=\mathrm{gram}\left(K,feature\right);letcoupling=\mathrm{matrix}\left(\mathrm{lambda}\left(i,\mathrm{lambda}\left(u,\mathrm{inner}\left(K,feature\left(\mathrm{inl}\left(i\right)\right),feature\left(\mathrm{inr}\left(\mathrm{unit}\left(\right)\right)\right)\right)\right)\right)\right);letinnovation=\mathrm{lambda}\left(a,\mathrm{inner}\left(K,feature\left(\mathrm{inr}\left(\mathrm{unit}\left(\right)\right)\right),feature\left(\mathrm{inr}\left(\mathrm{unit}\left(\right)\right)\right)\right)-\mathrm{complex}\left(K,a\right)-\mathrm{entry}\left(\mathrm{multiply}\left(\mathrm{conjTranspose}\left(coupling\right),\mathrm{inverse}\left(oldGram-\mathrm{scalarMatrix}\left(K,iota,a\right)\right),coupling\right),\mathrm{unit}\left(\right),\mathrm{unit}\left(\right)\right)\right);\left(\left(\left(\left(\left(\left(\left(\left(\mathrm{RCLike}\left(K\right)\wedge \mathrm{NormedAddCommGroup}\left(V\right)\right)\wedge \mathrm{InnerProductSpace}\left(K,V\right)\right)\wedge \mathrm{Fintype}\left(iota\right)\right)\wedge \mathrm{DecidableEq}\left(iota\right)\right)\wedge \left(\forall a\in \mathrm{Real}\left(\right),\mathrm{PosDef}\left(oldGram-\mathrm{scalarMatrix}\left(K,iota,a\right)\right)\iff a<alphaOld\right)\right)\wedge \left(\forall a\in \mathrm{Real}\left(\right),\mathrm{PosSemidef}\left(fullGram-\mathrm{scalarMatrix}\left(K,\mathrm{Sum}\left(iota,\mathrm{Unit}\left(\right)\right),a\right)\right)\iff a\le alphaNew\right)\right)\wedge \left(\forall a\in \mathrm{Real}\left(\right),\mathrm{PosDef}\left(fullGram-\mathrm{scalarMatrix}\left(K,\mathrm{Sum}\left(iota,\mathrm{Unit}\left(\right)\right),a\right)\right)\iff a<alphaNew\right)\right)\wedge alphaNew<alphaOld\right)\Rightarrow \left(innovation\left(alphaNew\right)=0\wedge \left(\forall a\in \mathrm{Real}\left(\right),\left(a<alphaOld\wedge innovation\left(a\right)=0\right)\Rightarrow a=alphaNew\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/BlockStructure/ObserverInnovationEquation.observer_innovation_equation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The old and extended matrices are constructed from one indexed feature family by the canonical Gram operation. The three displayed floor equivalences are the positive-definite and positive-semidefinite threshold characterizations of their least eigenvalues.

Pinned Mathlib supplies the canonical Gram matrix, the Schur positivity equivalence, and the block determinant factorization. At the new floor the extended determinant vanishes while the old block remains invertible, forcing the innovation to vanish; the same factorization and the floor thresholds prove uniqueness below the old floor.

Repository and pinned-library searches found related Schur-energy and block-positivity declarations, but no exact innovation-root theorem on the source-constructed real-or-complex Gram carrier.

References

• Truth anchor: D5/S3/Observer/BlockStructure/ObserverInnovationEquation.observer_innovation_equation