Information-Loss Layers and Zero Jordan Chains

Abstract

Observable loss layers are the rank drops and zero-block layers of a finite self-map.

Theorem 1.1 (Information loss recovers every zero-block layer and its total).

$$\forall Y\in Type,tau\in \mathrm{Function}\left(Y,Y\right),k\in \mathrm{Nat}\left(\right),\left(\mathrm{Finite}\left(Y\right)\wedge 0<k\right)\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{transferZeroBlocks}\left(tau\right),k\right)\right)\wedge \left(\mathrm{blockCountExactly}\left(\mathrm{transferZeroBlocks}\left(tau\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)$$

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

Source. Repository-derived.

Commentary.

Let tau be a self-map of a finite carrier Y and let k be positive. The multiset transferZeroBlocks(tau) is constructed from consecutive rank-loss layers, rather than supplied as a parameter.

The k-th observable loss equals the drop between the preceding and current transfer ranks and also counts zero blocks of size at least k. Blocks of exact size k are the difference of consecutive loss layers.

The finite carrier stabilizes by card(Y), so totalInformationLoss is the finite support realization of the source’s sum over all positive layers. It equals card(Y) minus the periodic-core card.

Theorem 8.3 is proved internally: the conjugate-partition construction has the same complete power-kernel tower as the canonical transfer operator. At the finite stabilization exponent, the Fitting transient subspace is that kernel, its restricted transfer is nilpotent, and every restricted power kernel is linearly equivalent to the corresponding ambient kernel. This binds the constructed multiset to the actual generalized zero-eigenspace. Mathlib’s Nat-valued telescoping theorem supplies the total-loss summation step.

References

• Truth anchor: D5/S3/ObserverMemory/FunctionalGraphs/InformationLossJordanLayers.information_loss_layers_and_zero_jordan_chains
• Dependency: D5/S3/ContinuousObservables/TransientObservableFilter
• Dependency: D5/S3/ObserverMemory/FunctionalGraphs/TraceRankJordanRecovery