feat: Initialization of Cyber-Physical Systems library , with Lyapuno…

[BasharHamade12]

Summary

This PR introduces the initial Cyber-Physical Systems (CPS) / Control Theory module to be included as part of the Cslib library.

Changes

New Definitions — Discrete Linear State Space Systems

• Basic structure and definitions for Discrete-Time Linear Dynamical Systems using the state-space representation x(k+1) = A·x(k) + B·u(k)
• System evolution function, state equation property, and zero-input utilities

Main Result — Lyapunov Asymptotic Stability

Proof of the following stability theorem:

Given a discrete-time linear system with zero input and a state transition matrix A whose spectral radius is strictly less than 1, the state converges to 0 as k → ∞.

The proof is built on top of:

• Gelfand's spectral radius formula
• The squeeze theorem

Key intermediate lemmas include:

• state_evolution_zero_input — state evolution under zero input
• bound_x_norm — norm bound on the state
• gelfand_eventually_bounded — eventual boundedness via Gelfand's formula

Files Changed

• Cslib.lean — added imports for the new CPS module
• Cslib/CPS/DiscreteLinearTime/AsymptoticStability.lean — asymptotic stability proof (255 lines)
• Cslib/CPS/DiscreteLinearTime/Basic.lean — basic definitions (105 lines)
• references.bib — added reference: Feedback Systems by Åström & Murray (2008)

Notes & Future Work

This is intended as a first contribution of many. Additional control theory results have already been formalized and are planned for future PRs, including:

• Observability
• Reachability
• Z-transform

The goal of this PR is to lay a solid foundation aligned with Cslib's intentions and vision, and to open the door for a broader control theory library within the Lean/Mathlib ecosystem.