Positive Invariant Metric Selection

Abstract

Zero real drift, unit spectrum, and a positive invariant metric are equivalent.

Theorem 1.1 (Positive metric selection is equivalent to zero drift).

$$\begin{gathered} \begin{array}{c}\forall \delta ,\gamma ,P:\mathbb{R},\\ 0<P\Rightarrow \\ \mathrm{let}u:\mathbb{C}=\exp ((\delta +i\gamma )\cdot P);\mathrm{let}v:\mathbb{C}=\exp (-((\delta +i\gamma )\cdot P));\mathrm{let}M:\mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{C})=\mathrm{diagonal}([u,v]);\\ \mathrm{ListTFAE}([\delta =0, \\ \forall \lambda :\mathbb{C},\lambda \in \mathrm{spectrum}(\mathbb{C},M),\Vert \lambda \Vert =1, \\ \exists H:\mathrm{Matrix}(\mathrm{Fin}(2),\mathrm{Fin}(2),\mathbb{C}),\mathrm{PosDef}(H)\wedge M^{\ast }\cdot H\cdot M=H]).\end{array} \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Algebra/PositiveInvariantMetricSelection.positive_invariant_metric_selection (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two diagonal modes are constructed from real drift, oscillation, and a strictly positive period.

The equivalence retains all three clauses: zero drift, unit norm for every spectral value, and preservation of a positive definite Hermitian metric.

References

• Truth anchor: D5/S3/ConceptDynamics/Algebra/PositiveInvariantMetricSelection.positive_invariant_metric_selection