Horizon Effective Index

Abstract

Effective Hankel defect indices obey positivity, product, sum, and boundary laws.

Theorem 1.1 (Finite Hankel horizon effective index).

$$\begin{array}{c}(\forall n\in \mathbb{N},H\in {\mathbb{R}}^{n\times n},\mathrm{IsFiniteHankel}(H)\wedge \mathrm{IsStrictlyContractive}(H)\Rightarrow \\ \mathrm{IsUnit}(\mathrm{horizonDefect}(H))\wedge 0<\det (\mathrm{horizonDefect}(H))\wedge \\ 0<\mathrm{horizonEffectiveIndex}(H)\wedge \mathrm{horizonEffectiveIndex}(H)=\prod _{i\in \mathrm{Fin}(n)}{1-\mathrm{finiteSingularValue}(H,i{)}^2}^{-1}\wedge \\ \log (\mathrm{horizonEffectiveIndex}(H))=-\log (\det (\mathrm{horizonDefect}(H))))\wedge \\ (\forall m,n\in \mathbb{N},H\in {\mathbb{R}}^{m\times m},K\in {\mathbb{R}}^{n\times n},\mathrm{horizonEffectiveIndex}(\mathrm{orthogonalSum}(H,K))=\mathrm{horizonEffectiveIndex}(H)\times \mathrm{horizonEffectiveIndex}(K))\wedge \\ (\forall n\in \mathbb{N},\mathrm{horizonEffectiveIndex}(0_{n\times n})=1)\wedge \\ (\mathrm{Tendsto}((\sigma \mapsto {1-{\sigma }^2}^{-1}),\mathrm{nhdsWithin}(1,\mathrm{Iio}(1)),atTop))\wedge \\ (\exists H\in {\mathbb{R}}^{1\times 1},\mathrm{IsFiniteHankel}(H)\wedge \mathrm{IsStrictlyContractive}(H)\wedge \mathrm{horizonEffectiveIndex}(H)=1).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/Pick/HorizonEffectiveIndex.finite_hankel_horizon_effective_index (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite square real matrices model the finite-rank Hankel operators. Strict contraction is stated by requiring every spectrally defined singular value to be below one.

The characteristic polynomial of the Hermitian Gram matrix, evaluated at one, gives the singular-value product for the defect determinant. Positivity makes the defect invertible and proves the reciprocal determinant and logarithmic formulas.

Block determinants give orthogonal-sum multiplicativity, the zero matrix gives normalization and an explicit inhabited Hankel example, and the reciprocal singular factor tends to infinity at the contractive boundary.

The declaration formalizes only the effective information index. It does not claim that a Jones index has been constructed.

References

• Truth anchor: D5/S3/Weil/Pick/HorizonEffectiveIndex.finite_hankel_horizon_effective_index