lyapunovAt_adjacent_ratio
plain-language theorem explainer
Lyapunov exponents at adjacent PIC resolution rungs stand in the fixed ratio phi inverse. Plasma kineticists running particle-in-cell simulations cite the result to confirm that numerical heating follows the recognition lattice scaling. The short proof rewrites the ratio via the successor lemma and clears the common factor with field simplification after positivity.
Claim. For every natural number $k$, the ratio of the Lyapunov exponent at rung $k+1$ to the Lyapunov exponent at rung $k$ equals $phi^{-1}$, where the exponent at rung $k$ is defined as referenceExponent times $phi$ to the power of minus $k$.
background
The module treats Lyapunov times in particle-in-cell plasma simulations as lying on the phi-ladder. Higher rung corresponds to more macro-particles per Debye cell, lower numerical heating, and smaller Lyapunov exponent. The local setting extends coronal Lyapunov predictions by requiring that adjacent doubling of resolution reduces heating by phi squared, matching empirical PIC benchmarks.
proof idea
One-line wrapper that applies lyapunovAt_succ_ratio to replace the numerator, then invokes field_simp with the non-zero condition supplied by lyapunovAt_pos k.
why it matters
Supplies the adjacent_ratio field inside picLyapunovCert, completing the structural certificate for PIC Lyapunov exponents. This step confirms the phi-ladder scaling for plasma kinetics and aligns with the self-similar fixed point phi together with the recognition composition law. The result sits downstream of the successor ratio and feeds the assembled certificate without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.