Jet Numbers: A Verified Algebra of Derivatives

We present a formally verified treatment of jet numbers — algebraic objects that carry a value together with its derivatives to a fixed order. A 2-jet encodes \((f, f', f'')\) in a single element, with arithmetic operations following the Leibniz rule: \((fg)' = f'g + fg'\) and the generalized second-order formula \((fg)'' = f''g + 2f'g' + fg''\). We prove 15 theorems establishing the fundamental properties of jet arithmetic: additivity and multiplicativity of the value projection, scalar linearity of derivatives, squaring rules for first and second derivatives, and identity behavior. The proofs are formalized in the Platonic proof language (38 verified declarations) and are fully exportable to Lean 4.

Keywords: Jet spaces, automatic differentiation, Taylor expansions, formal verification, differential algebra

MSC 2020: 58A20 (Jets), 65D25 (Numerical differentiation), 68V15 (Theorem proving)