Diagonal-Algebra Similarity Obstruction

Abstract

Similar transition matrices need not admit a diagonal-algebra-preserving similarity.

Theorem 1.1 (Similar transition matrices can differ as based systems).

$$\begin{array}{c}(\exists P,Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(8\right),\mathrm{Fin}\left(8\right),\mathbb{C}\right),\\ PQ=I\wedge QP=I\wedge \\ \mathrm{complexTransitionMatrix}\left(tauA\right)P=P\mathrm{complexTransitionMatrix}\left(tauB\right))\wedge \\ \neg (\exists P,Q:\mathrm{Matrix}\left(\mathrm{Fin}\left(8\right),\mathrm{Fin}\left(8\right),\mathbb{C}\right),\\ PQ=I\wedge QP=I\wedge \\ \mathrm{complexTransitionMatrix}\left(tauA\right)P=P\mathrm{complexTransitionMatrix}\left(tauB\right)\wedge \\ (\forall d:\mathrm{Fin}\left(8\right)\to \mathbb{C},\exists d^{\prime }:\mathrm{Fin}\left(8\right)\to \mathbb{C},P\mathrm{diag}\left(d\right)Q=\mathrm{diag}\left(d^{\prime }\right))\wedge \\ (\forall d:\mathrm{Fin}\left(8\right)\to \mathbb{C},\exists d^{\prime }:\mathrm{Fin}\left(8\right)\to \mathbb{C},Q\mathrm{diag}\left(d\right)P=\mathrm{diag}\left(d^{\prime }\right))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Linearization/DiagonalAlgebraSimilarityObstruction.same_linear_class_without_diagonal_algebra_similarity (✓ std3). ∎

Source. Repository-derived.

Commentary.

The maps tauA and tauB are imported from the canonical eight-state countermodel. Their complex transition matrices use the standard basis: column y is the coordinate vector indexed by tau(y).

The first public conjunct gives an explicit complex change of basis and two-sided inverse intertwining the transition matrices. This is the source’s common complex linear similarity class, and hence its common Jordan form.

The second public conjunct rules out any such change of basis that also conjugates every standard diagonal matrix to a diagonal matrix in both directions. Thus the quantified property is directly about the full diagonal algebra, not a definition by graph conjugacy.

The proof applies the frozen integral similarity certificate after entrywise complex casting. Conversely, conjugated coordinate diagonals force each matrix column onto a distinct coordinate row, producing a permutation conjugacy forbidden by the frozen function-graph countermodel.

References

• Truth anchor: D5/S3/ObserverMemory/Linearization/DiagonalAlgebraSimilarityObstruction.same_linear_class_without_diagonal_algebra_similarity
• Dependency: D5/S3/ObserverMemory/InverseLimits/FunctionGraphLinearSimilarity