Trace-Rank Jordan Recovery

Abstract

Complete transfer traces and ranks recover the periodic and zero-block profiles.

Theorem 1.1 (Rank differences recover zero blocks).

$$\forall Y\in Type,tau\in \mathrm{Function}\left(Y,Y\right),zeroBlocks\in \mathrm{BlockMultiset}\left(\right),k\in \mathrm{Nat}\left(\right),\left(\mathrm{Finite}\left(Y\right)\wedge \left(\left(\forall j\in \mathrm{Nat}\left(\right),\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),j\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right)=\mathrm{natSub}\left(\mathrm{blockProfileDimension}\left(zeroBlocks\right),\mathrm{blockKernelTower}\left(zeroBlocks,j\right)\right)\right)\wedge 0<k\right)\right)\Rightarrow \left(\mathrm{natSub}\left(\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),\mathrm{pred}\left(k\right)\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right),\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),k\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right)\right)=\mathrm{blockCountAtLeast}\left(zeroBlocks,k\right)\wedge \mathrm{blockCountExactly}\left(zeroBlocks,k\right)=\mathrm{natSub}\left(\mathrm{natSub}\left(\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),\mathrm{pred}\left(k\right)\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right),\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),k\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right)\right),\mathrm{natSub}\left(\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),\mathrm{pred}\left(\mathrm{add}\left(k,1\right)\right)\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right),\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),\mathrm{add}\left(k,1\right)\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/FunctionalGraphs/TraceRankJordanRecovery.rank_difference_recovers_zero_blocks (✓ std3). ∎

Source. Repository-derived.

Commentary.

At every positive index, successive residual ranks count zero blocks of at least that size, and the next difference counts exact size.

Theorem 1.2 (Trace and rank spectra determine the Jordan profile).

$$\forall YLeft\in Type,YRight\in Type,tau\in \mathrm{Function}\left(YLeft,YLeft\right),sigma\in \mathrm{Function}\left(YRight,YRight\right),cycleCountsLeft\in \mathrm{Function}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right),cycleCountsRight\in \mathrm{Function}\left(\mathrm{Nat}\left(\right),\mathrm{Nat}\left(\right)\right),zeroBlocksLeft\in \mathrm{BlockMultiset}\left(\right),zeroBlocksRight\in \mathrm{BlockMultiset}\left(\right),\left(\mathrm{Finite}\left(YLeft\right)\wedge \left(\mathrm{Finite}\left(YRight\right)\wedge \left(\left(\forall r\in \mathrm{Nat}\left(\right),0<r\Rightarrow \mathrm{trace}\left(\mathrm{Complex}\left(\right),\mathrm{Finsupp}\left(YLeft,\mathrm{Complex}\left(\right)\right),\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),r\right)\right)=\mathrm{trace}\left(\mathrm{Complex}\left(\right),\mathrm{Finsupp}\left(YRight,\mathrm{Complex}\left(\right)\right),\mathrm{pow}\left(\mathrm{transferOperator}\left(sigma\right),r\right)\right)\right)\wedge \left(\left(\forall k\in \mathrm{Nat}\left(\right),\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),k\right)\right)\right)=\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(sigma\right),k\right)\right)\right)\right)\wedge \left(\mathrm{apply}\left(cycleCountsLeft,0\right)=0\wedge \left(\mathrm{apply}\left(cycleCountsRight,0\right)=0\wedge \left(\left(\forall r\in \mathrm{Nat}\left(\right),0<r\Rightarrow \mathrm{trace}\left(\mathrm{Complex}\left(\right),\mathrm{Finsupp}\left(YLeft,\mathrm{Complex}\left(\right)\right),\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),r\right)\right)=\mathrm{finsetSum}\left(\mathrm{divisors}\left(r\right),\mathrm{lambda}\left(\mathrm{typed}\left(d,\mathrm{Nat}\left(\right)\right),\mathrm{natCast}\left(\mathrm{Complex}\left(\right),\mathrm{mul}\left(d,\mathrm{apply}\left(cycleCountsLeft,d\right)\right)\right)\right)\right)\right)\wedge \left(\left(\forall r\in \mathrm{Nat}\left(\right),0<r\Rightarrow \mathrm{trace}\left(\mathrm{Complex}\left(\right),\mathrm{Finsupp}\left(YRight,\mathrm{Complex}\left(\right)\right),\mathrm{pow}\left(\mathrm{transferOperator}\left(sigma\right),r\right)\right)=\mathrm{finsetSum}\left(\mathrm{divisors}\left(r\right),\mathrm{lambda}\left(\mathrm{typed}\left(d,\mathrm{Nat}\left(\right)\right),\mathrm{natCast}\left(\mathrm{Complex}\left(\right),\mathrm{mul}\left(d,\mathrm{apply}\left(cycleCountsRight,d\right)\right)\right)\right)\right)\right)\wedge \left(\left(\forall k\in \mathrm{Nat}\left(\right),\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),k\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right)=\mathrm{natSub}\left(\mathrm{blockProfileDimension}\left(zeroBlocksLeft\right),\mathrm{blockKernelTower}\left(zeroBlocksLeft,k\right)\right)\right)\wedge \left(\forall k\in \mathrm{Nat}\left(\right),\mathrm{natSub}\left(\mathrm{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(sigma\right),k\right)\right)\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(sigma\right)\right)\right)=\mathrm{natSub}\left(\mathrm{blockProfileDimension}\left(zeroBlocksRight\right),\mathrm{blockKernelTower}\left(zeroBlocksRight,k\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(cycleCountsLeft=cycleCountsRight\wedge zeroBlocksLeft=zeroBlocksRight\right)$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/FunctionalGraphs/TraceRankJordanRecovery.trace_rank_spectra_determine_jordan_profile (✓ std3). ∎

Source. Repository-derived.

Commentary.

Möbius inversion uniquely recovers periodic cycle counts from traces. Stable-image ranks recover the periodic dimension, after which all residual ranks uniquely recover the nilpotent zero-block multiset.

References

• Truth anchor: D5/S3/ObserverMemory/FunctionalGraphs/TraceRankJordanRecovery.rank_difference_recovers_zero_blocks
• Truth anchor: D5/S3/ObserverMemory/FunctionalGraphs/TraceRankJordanRecovery.trace_rank_spectra_determine_jordan_profile
• Dependency: D5/S3/Estimation/ExperimentCost/KernelTowerNilpotentRecovery
• Dependency: D5/S3/ObserverMemory/FunctionalGraphs/FiniteFunctionalGraphFittingDecomposition