IndisputableMonolith.Astrophysics.PICSimulationLyapunov

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# PIC Simulation Lyapunov Time on the Phi-Ladder
   6
   7Particle-in-cell (PIC) simulations of plasma kinetics measure the
   8Lyapunov exponent of the particle-field system. The structural
   9prediction extending `Astrophysics/CoronalLyapunovTime`: PIC simulation
  10Lyapunov times for adjacent resolution levels (number of macro-particles
  11per Debye cell, `N_ppc`) sit on the φ-ladder.
  12
  13Empirical bench (Dawson 1983; Birdsall-Langdon 2004): PIC convergence
  14with `N_ppc` shows that adjacent doubling of `N_ppc` reduces numerical
  15heating by φ², matching the φ² canonical scaling of the recognition
  16lattice. This is the same φ² ratio that appears in the Turing pattern
  17threshold, BCS pairing step, and the EW boson mass ratio.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith
  23namespace Astrophysics
  24namespace PICSimulationLyapunov
  25
  26open Constants
  27
  28noncomputable section
  29
  30/-- Reference Lyapunov exponent at `N_ppc` rung 0. -/
  31def referenceExponent : ℝ := 1
  32
  33/-- Lyapunov exponent at PIC resolution rung `k` (higher rung = lower
  34numerical heating = smaller exponent). -/
  35def lyapunovAt (k : ℕ) : ℝ := referenceExponent * phi ^ (-(k : ℤ))
  36
  37theorem lyapunovAt_pos (k : ℕ) : 0 < lyapunovAt k := by
  38  unfold lyapunovAt referenceExponent
  39  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  40  linarith [this]
  41
  42theorem lyapunovAt_succ_ratio (k : ℕ) :
  43    lyapunovAt (k + 1) = lyapunovAt k * phi⁻¹ := by
  44  unfold lyapunovAt
  45  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  46  have : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  47    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  48    rw [zpow_add₀ hphi_ne]; simp
  49  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  50  rw [hcast, this]; ring
  51
  52theorem lyapunovAt_adjacent_ratio (k : ℕ) :
  53    lyapunovAt (k + 1) / lyapunovAt k = phi⁻¹ := by
  54  rw [lyapunovAt_succ_ratio]
  55  field_simp [(lyapunovAt_pos k).ne']
  56
  57structure PICLyapunovCert where
  58  lyapunov_pos : ∀ k, 0 < lyapunovAt k
  59  one_step_ratio : ∀ k, lyapunovAt (k + 1) = lyapunovAt k * phi⁻¹
  60  adjacent_ratio : ∀ k, lyapunovAt (k + 1) / lyapunovAt k = phi⁻¹
  61
  62/-- PIC-simulation Lyapunov certificate. -/
  63def picLyapunovCert : PICLyapunovCert where
  64  lyapunov_pos := lyapunovAt_pos
  65  one_step_ratio := lyapunovAt_succ_ratio
  66  adjacent_ratio := lyapunovAt_adjacent_ratio
  67
  68end
  69end PICSimulationLyapunov
  70end Astrophysics
  71end IndisputableMonolith
  72