picLyapunovCert
plain-language theorem explainer
The declaration assembles three theorems on the Lyapunov exponent in PIC plasma simulations into the PICLyapunovCert structure. Plasma physicists studying numerical heating across macro-particle resolutions would cite it to record that adjacent doublings of N_ppc reduce the exponent by exactly phi inverse. The construction is a direct one-line wrapper that populates the structure fields from the positivity, successor-ratio, and adjacent-ratio lemmas.
Claim. Let $k$ range over natural numbers and let $phi$ be the golden ratio. Let $lambda(k)$ be the Lyapunov exponent at resolution level $k$. The certificate asserts $lambda(k) > 0$, $lambda(k+1) = lambda(k) phi^{-1}$, and $lambda(k+1)/lambda(k) = phi^{-1}$ for every $k$.
background
The module treats particle-in-cell simulations of plasma kinetics. The function lyapunovAt(k) is defined via referenceExponent and equals phi raised to the power minus k. The structure PICLyapunovCert packages three properties: strict positivity of lyapunovAt at every level, the one-step multiplicative scaling by phi inverse, and the equivalent adjacent ratio equality. Upstream theorems establish these facts separately: lyapunovAt_pos uses zpow positivity of phi, while lyapunovAt_succ_ratio and lyapunovAt_adjacent_ratio reduce the scaling claims to algebraic identities on integer exponents.
proof idea
The definition is a one-line wrapper that applies lyapunovAt_pos, lyapunovAt_succ_ratio, and lyapunovAt_adjacent_ratio to fill the three fields of the PICLyapunovCert structure.
why it matters
This certificate records the phi-ladder scaling of Lyapunov times between adjacent PIC resolutions, extending the coronal Lyapunov time result. It supplies the concrete instance needed to connect numerical plasma convergence (Dawson 1983; Birdsall-Langdon 2004) to the recognition lattice phi^2 heating reduction. No downstream theorems yet consume it, leaving open its use in larger proofs that close the eight-tick octave or mass-ladder derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.