ElectrostaticVlasov - GitLite

KO | EN

gitlite — search

#containers #json #data-science #monitoring #react-native #gemini #php #gpt #ai-agent #terminal

ElectrostaticVlasov

(★ 12)

End-to-end formally verified solvers for the electrostatic Vlasov equation in 1x1v, 1x2v, 1x3v, 2x2v, 2x3v, and 3x3v (i.e. 2D to 6D) phase space.

File Explorer

ZIP Download

- es_vlasov_1x1v.c
- es_vlasov_1x2v.c
- es_vlasov_1x3v.c
- es_vlasov_2x2v.c
- es_vlasov_2x3v.c
- es_vlasov_3x3v.c
- es_vlasov_1x1v.lean
- es_vlasov_1x2v.lean
- es_vlasov_1x3v.lean
- es_vlasov_2x2v.lean
- es_vlasov_2x3v.lean
- es_vlasov_3x3v.lean
- es_vlasov_1x1v.mov
- es_vlasov_1x2v.mov
- es_vlasov_1x3v.mov
- es_vlasov_2x2v.mov
- es_vlasov_2x3v.mov
- es_vlasov_3x3v.mov
- es_vlasov_1x1v.rkt
- es_vlasov_1x2v.rkt
- es_vlasov_1x3v.rkt
- es_vlasov_2x2v.rkt
- es_vlasov_2x3v.rkt
- es_vlasov_3x3v.rkt
.gitattributes
final_phase_space.png
LICENSE
README.md

# Use via CDN

jsDelivr

jsDelivr serves any public GitHub repository as a CDN with zero setup. Pick a version and a file to get a ready-to-paste link and snippet.

Version

File

Link

Example

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

## Highlights

* End-to-end formally verified solvers for the electrostatic Vlasov equation (collisionless Boltzmann equation for the one-particle distribution function in phase space, coupled to a fixed electrostatic potential), in 1x1v, 1x2v, 1x3v, 2x2v, 2x3v, and 3x3v (i.e. from 2D phase space with 1 configuration space dimension and 1 velocity space dimension, to full 6D phase space with 3 configuration space dimensions and 3 velocity space dimensions).
* **Took ~123 seconds for Lanyon to generate everything**.
  * ~10 seconds for the electrostatic Vlasov equation in 1x1v, ~15 seconds for the electrostatic Vlasov equation in 1x2v, ~21 seconds for the electrostatic Vlasov equation in 1x3v, ~17 seconds for the electrostatic Vlasov equation in 2x2v, ~32 seconds for the electrostatic Vlasov equation in 2x3v, and ~28 seconds for the electrostatic Vlasov equation in 3x3v.
  * Real-time screen captures are shown in `/screencaps`.
* **18,589 lines of Lean 4 code** to prove end-to-end correctness properties.
  * 1,101 for the electrostatic Vlasov equation in 1x1v, 2,039 for the electrostatic Vlasov equation in 1x2v, 3,313 for the electrostatic Vlasov equation in 1x3v, 2,747 for the electrostatic Vlasov equation in 2x2v, 4,216 for the electrostatic Vlasov equation in 2x3v, 5,173 for the electrostatic Vlasov equation in 3x3v.
* **450 total definitions** and **312 total theorems**.
* **12,143 lines of formally verified C code**.
  * 856 for the electrostatic Vlasov equation in 1x1v, 1,414 for the electrostatic Vlasov equation in 1x2v, 2,100 for the electrostatic Vlasov equation in 1x3v, 1,880 for the electrostatic Vlasov equation in 2x2v, 2,653 for the electrostatic Vlasov equation in 2x3v, and 3,240 for the electrostatic Vlasov equation in 3x3v.

## Further Details

The most general form of the electrostatic Vlasov equation for a single (charged) particle species ${\alpha}$ is:

$$ \frac{\partial f_{\alpha}}{\partial t} + \mathbf{v}_{\alpha} \cdot \frac{\partial f_{\alpha}}{\partial \mathbf{x}} + \frac{q_{\alpha} \mathbf{E}}{m_{\alpha}} \cdot \frac{\partial f_{\alpha}}{\partial \mathbf{v}} = 0 $$

for one-particle distribution function ${f_{\alpha}}$, configuration space coordinates ${\mathbf{x}}$, velocity space coordinates ${\mathbf{v}}$, particle charge ${q_{\alpha}}$, particle mass ${m_{\alpha}}$, and electric field ${\mathbf{E}}$. This is often made self-consistent by coupling to the Poisson equation:

$$ \nabla^2 \phi + \frac{\rho}{\varepsilon} = 0 $$

for electrostatic potential ${\phi}$, electric charge density ${\rho}$, and electric permittivity ${\varepsilon}$, to obtain the *Vlasov-Poisson system*. In this particular case, however, we consider a fixed electrostatic potential only, and leave rigorous investigation of the full Vlasov-Poisson system for a future Lanyon research note!

![Phase space plot of a double potential well problem for the 1x1v electrostatic Vlasov equation](https://raw.githubusercontent.com/lanyonai/ElectrostaticVlasov/main/final_phase_space.png)