Actual Transfer Jordan Chains

Abstract

The transfer loss layers count actual Jordan chains on its transient Fitting summand.

Theorem 1.1 (Actual chains realize the rank-loss profile).

$$\forall Y\in Type,tau\in \mathrm{Function}\left(Y,Y\right),\mathrm{Finite}\left(Y\right)\Rightarrow \left(\exists I\in Type,hI\in \mathrm{Fintype}\left(I\right),s\in \mathrm{Function}\left(I,\mathrm{PNat}\left(\right)\right),b\in \mathrm{Basis}\left(\mathrm{Positions}\left(I,s\right),\mathrm{Complex}\left(\right),\mathrm{transientSubspace}\left(tau,\mathrm{card}\left(Y\right)\right)\right),\left(\forall m\in \mathrm{Nat}\left(\right),i\in I,j\in \mathrm{Fin}\left(s\left(i\right)\right),\mathrm{apply}\left(\mathrm{pow}\left(\mathrm{transientTransfer}\left(tau,\mathrm{card}\left(Y\right)\right),m\right),b\left(i,j\right)\right)=\mathrm{ite}\left(\mathrm{add}\left(j,m\right)<s\left(i\right),b\left(i,\mathrm{add}\left(j,m\right)\right),0\right)\right)\wedge \left(\mathrm{Sizes}\left(I,s\right)=\mathrm{transferZeroBlocks}\left(tau\right)\wedge \left(\forall k\in \mathrm{Nat}\left(\right),0<k\Rightarrow \left(\left(\mathrm{informationLossLayer}\left(tau,k\right)=\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{finrank}\left(\mathrm{Complex}\left(\right),\mathrm{range}\left(\mathrm{pow}\left(\mathrm{transferOperator}\left(tau\right),k\right)\right)\right)\right)\wedge \mathrm{informationLossLayer}\left(tau,k\right)=\mathrm{blockCountAtLeast}\left(\mathrm{Sizes}\left(I,s\right),k\right)\right)\wedge \left(\mathrm{blockCountExactly}\left(\mathrm{Sizes}\left(I,s\right),k\right)=\mathrm{natSub}\left(\mathrm{informationLossLayer}\left(tau,k\right),\mathrm{informationLossLayer}\left(tau,\mathrm{add}\left(k,1\right)\right)\right)\wedge \mathrm{totalInformationLoss}\left(tau\right)=\mathrm{natSub}\left(\mathrm{card}\left(Y\right),\mathrm{card}\left(\mathrm{PeriodicCore}\left(tau\right)\right)\right)\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

For every finite Y and arbitrary self-map tau, work over the complex numbers and put n=card(Y). Positions(I,s) is the dependent sum of Fin(s(i)) over the finite type I, with s(i) positive. Sizes(I,s) is the multiset mapping s over all of I, retaining multiplicities. The basis belongs to transientSubspace(tau,n), the generalized zero-eigenspace. The conditional basis vector is used only when its index is in range. natSub means truncated natural subtraction and pred is the natural predecessor.

The general nilpotent chain theorem supplies the actual basis and iterate ranks. Rank-nullity computes its kernel tower; the existing finite tower uniqueness theorem identifies its positive size multiset with transferZeroBlocks(tau). Thus the profile in the existing information loss theorem now has a basis of actual chains. All four source equality leaves are retained. totalInformationLoss is the finite-support sum of positive loss layers, as defined by the existing finite-map theory.

References

• Truth anchor: D5/S3/ObserverMemory/FunctionalGraphs/ActualTransferJordanChains.information_loss_layers_from_actual_jordan_chains
• Dependency: D5/S1/Eigenstructure/NilpotentJordanChains
• Dependency: D5/S3/ObserverMemory/FunctionalGraphs/InformationLossJordanLayers