Suspension Event Decomposition

Abstract

A positive-roof suspension flow splits uniquely into event count and residual phase.

Theorem 1.1 (Continuous time has a unique event-phase decomposition).

$$\begin{array}{c}\forall K:\mathrm{Type},\\ [\mathrm{TopologicalSpace}\left(K\right)],[\mathrm{CompactSpace}\left(K\right)],\\ T:\mathrm{Homeomorph}\left(K,K\right),r:K\to \mathbb{R},\\ \mathrm{Continuous}\left(r\right)\wedge (\forall x:K,0<r\left(x\right)),\\ k:K,u:RoofCoordinate,t:\mathbb{R},0\le t\\ \Rightarrow \exists !normal:\mathbb{N}\times RoofCoordinate,\\ \mathrm{birkhoffSum}\left(T,r,\mathrm{fst}\left(normal\right),k\right)\le \mathrm{physicalHeight}\left(r,k,u\right)+t\wedge \\ \mathrm{physicalHeight}\left(r,k,u\right)+t<\mathrm{birkhoffSum}\left(T,r,\mathrm{fst}\left(normal\right)+1,k\right)\wedge \\ \mathrm{physicalHeight}\left(r,\mathrm{iterate}\left(T,\mathrm{fst}\left(normal\right),k\right),\mathrm{snd}\left(normal\right)\right)=\mathrm{physicalHeight}\left(r,k,u\right)+t-\mathrm{birkhoffSum}\left(T,r,\mathrm{fst}\left(normal\right),k\right)\wedge \\ \mathrm{suspensionFlow}\left(T,r,t,\mathrm{canonicalSuspensionClass}\left(T,r,k,u\right)\right)=\mathrm{canonicalSuspensionClass}\left(T,r,\mathrm{iterate}\left(T,\mathrm{fst}\left(normal\right),k\right),\mathrm{snd}\left(normal\right)\right)\wedge \\ \mathrm{physicalHeight}\left(r,k,u\right)+t=\mathrm{birkhoffSum}\left(T,r,\mathrm{fst}\left(normal\right),k\right)+\mathrm{physicalHeight}\left(r,\mathrm{iterate}\left(T,\mathrm{fst}\left(normal\right),k\right),\mathrm{snd}\left(normal\right)\right).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Dynamics/SuspensionEventDecomposition.continuous_time_discrete_event_decomposition (✓ std3). ∎

Source. Repository-derived.

Commentary.

The frozen suspension carrier uses a normalized leaf coordinate. Multiplication by the positive roof gives its nonnegative physical phase, so no separate sign hypothesis is needed.

Literal forward translation is first performed on a private nonnegative-height cover. Normalization respects every roof crossing and transports the translated class back to the canonical suspension quotient.

Compactness and roof positivity force the Birkhoff sums past the translated physical phase. The least crossing index supplies both half-open bounds; division by the final positive roof produces the residual leaf coordinate.

The bounds determine the event count uniquely, while positivity makes physical height injective within the final leaf. Thus the discrete count and residual coordinate are jointly unique and recover the complete translated time coordinate.

References

• Truth anchor: D5/S3/Observer/Dynamics/SuspensionEventDecomposition.continuous_time_discrete_event_decomposition
• Dependency: D5/S3/Observer/Dynamics/MinimalSuspensionContinuum