PICLyapunovCert
plain-language theorem explainer
Plasma physicists cite the PICLyapunovCert structure to certify that the Lyapunov exponent at each PIC resolution rung k stays positive and scales exactly by phi inverse on each rung increment. The declaration packages three properties of the lyapunovAt function into a reusable certificate type. It is a bare structure definition with no internal proof steps.
Claim. A structure $C$ such that the Lyapunov exponent function satisfies $0 < lyapunovAt(k)$ for every natural number $k$, together with the scaling relations $lyapunovAt(k+1) = lyapunovAt(k) · ϕ^{-1}$ and $lyapunovAt(k+1)/lyapunovAt(k) = ϕ^{-1}$.
background
The PIC Simulation Lyapunov module analyzes particle-in-cell simulations of plasma kinetics for their Lyapunov exponents on the phi-ladder. The upstream definition lyapunovAt sets the exponent at rung k to referenceExponent times phi to the power of minus k. The module doc states that adjacent doubling of macro-particles per Debye cell reduces numerical heating by phi squared, matching recognition lattice scaling, with empirical support from Dawson 1983 and Birdsall-Langdon 2004.
proof idea
This is a structure definition that directly encodes the three properties: positivity of lyapunovAt at every rung, the one-step multiplicative scaling by phi inverse, and the equivalent adjacent ratio. No lemmas are applied; the structure serves as a type for the certificate constructed downstream.
why it matters
This certificate feeds the definition of picLyapunovCert, which instantiates it using the positivity and ratio lemmas for lyapunovAt. It fills the structural prediction that PIC Lyapunov times sit on the phi-ladder, linking to the eight-tick octave and phi self-similarity in the Recognition framework. It touches the open question of empirical validation in plasma simulations against the phi squared scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.