Dependencies

Advective derivative of a scalar field: \((\mathbf{v}\cdot \nabla )f = \sum _i v_i\, \frac{\partial f}{\partial x_i}\).

Advective derivative of a vector field: \(((\mathbf{v}\cdot \nabla )\mathbf{F})_j = \sum _i v_i\, \frac{\partial F_j}{\partial x_i}\).

The \(i\)-th standard basis vector \(\mathbf{e}_i = \mathrm{Pi.single}\; i\; 1\).

A conducting medium: \(\sigma {\gt} 0\) introduces damping.

Curl of a vector field: \((\nabla \! \times \! \mathbf{F})_k = \varepsilon _{kij}\, \frac{\partial F_j}{\partial x_i}\), defined by explicit pattern matching on the three components.

Major radius \(R = x_0\) from a point \((R, \varphi , Z)\).

Vertical coordinate \(Z = x_2\).

A lossless dielectric: general \(\varepsilon , \mu \) with \(\sigma = 0\).

Divergence of a vector field: \((\nabla \! \cdot \! \mathbf{F})(x) = \sum _{i=0}^{2} \frac{\partial F_i}{\partial x_i}(x)\).

Pointwise addition of vector fields.

Pointwise cross product of two vector fields: \((\mathbf{F}\times \mathbf{G})(x) = \mathbf{F}(x)\times \mathbf{G}(x)\).

Pointwise dot product of two vector fields.

Pointwise negation of a vector field.

Pointwise subtraction of vector fields.

Fluid constants: density \(\rho {\gt} 0\), dynamic viscosity \(\mu \ge 0\).

Kinematic viscosity \(\nu = \mu /\rho \).

FRC equilibrium: radial profiles \(p(R)\), \(B_z(R)\), \(B_\theta (R)\) satisfying radial pressure balance with field reversal at the separatrix.

Gradient of a scalar field: \((\nabla f)(x)_i = \frac{\partial f}{\partial x_i}(x)\).

The Grad-Shafranov equation for tokamak equilibrium: \(\Delta ^*\psi = -\mu _0 R^2 p'(\psi ) - g(\psi )g'(\psi )\).

The Grad-Shafranov operator: \(\Delta ^*\psi = \frac{\partial ^2 \psi }{\partial R^2} - \frac{1}{R}\frac{\partial \psi }{\partial R} + \frac{\partial ^2 \psi }{\partial Z^2}\).

Magnetic field from flux: \(\mathbf{B} = (-\frac{1}{R}\frac{\partial \psi }{\partial Z},\; \frac{g(\psi )}{R},\; \frac{1}{R}\frac{\partial \psi }{\partial R})\).

Pressure profile \(p(x) = p(\psi (x))\).

The ideal MHD system: mass conservation, momentum (\(\rho \frac{D \mathbf{v}}{D t} = \mathbf{J}\times \mathbf{B} - \nabla p\)), adiabatic energy, induction (\(\frac{\partial \mathbf{B}}{\partial t} = \nabla \! \times \! (\mathbf{v}\times \mathbf{B})\)), \(\nabla \! \cdot \! \mathbf{B} = 0\), and Ampère’s law (\(\nabla \! \times \! \mathbf{B} = \mu _0\mathbf{J}\)).

Incompressible Navier-Stokes: \(\nabla \! \cdot \! \mathbf{v} = 0\) and \(\rho \frac{D \mathbf{v}}{D t} = -\nabla p + \mu \nabla ^2\mathbf{v} + \mathbf{f}\).

A scalar field is axisymmetric: \(\frac{\partial f}{\partial \varphi } = 0\).

A scalar field is \(C^2\): \(\mathrm{ContDiff}\; \mathbb {R}\; 2\; f\).

A vector field is \(C^2\): each component \(y \mapsto F(y)_j\) is \(\mathrm{ContDiff}\; \mathbb {R}\; 2\).

Lorentz force per unit volume: \(\mathbf{f} = \rho _c\, \mathbf{E} + \mathbf{J}\times \mathbf{B}\).

Material derivative of a scalar field: \(\frac{D f}{D t} = \frac{\partial f}{\partial t} + (\mathbf{v}\cdot \nabla )f\).

Material derivative of a vector field: \(\left(\frac{D \mathbf{F}}{D t}\right)_j = \frac{\partial F_j}{\partial t} + ((\mathbf{v}\cdot \nabla )\mathbf{F})_j\).

Maxwell’s equations in a linear medium, packaging: Gauss’s law (\(\nabla \! \cdot \! \mathbf{E} = \rho /\varepsilon \)), no monopoles (\(\nabla \! \cdot \! \mathbf{B} = 0\)), Faraday (\(\nabla \! \times \! \mathbf{E} = -\frac{\partial \mathbf{B}}{\partial t}\)), and Ampère-Maxwell (\(\nabla \! \times \! \mathbf{B} = \mu (\mathbf{J}_{\mathrm{free}} + \sigma \mathbf{E}) + \mu \varepsilon \frac{\partial \mathbf{E}}{\partial t}\)).

Parameters of a linear, isotropic, homogeneous electromagnetic medium: permittivity \(\varepsilon {\gt} 0\), permeability \(\mu {\gt} 0\), conductivity \(\sigma \ge 0\).

Wave speed in the medium: \(v = 1/\sqrt{\mu \varepsilon }\).

Squared wave speed: \(v^2 = 1/(\mu \varepsilon )\).

Physical constants: vacuum permeability \(\mu _0 {\gt} 0\) and adiabatic index \(\gamma {\gt} 1\).

Static MHD equilibrium: \(\nabla p = \mathbf{J}\times \mathbf{B}\) with \(\nabla \! \times \! \mathbf{B} = \mu _0\mathbf{J}\) and \(\nabla \! \cdot \! \mathbf{B} = 0\).

Smoothness bundle for vorticity/pressure derivations: \(C^3\) velocity, curl-time commutativity, and divergence-time commutativity.

Ohm’s law parameters: resistivity \(\eta \ge 0\).

Partial derivative of a scalar field: \(\frac{\partial f}{\partial x_i}(x) = (\mathrm{fderiv}\; \mathbb {R}\; f\; x)(\mathbf{e}_i)\).

Second partial derivative of a scalar field: \(\frac{\partial ^2 f}{\partial x_i^2}\).

Partial derivative of a vector field component: \(\frac{\partial F_j}{\partial x_i}(x) = (\mathrm{fderiv}\; \mathbb {R}\; (y \mapsto F(y)_j)\; x)(\mathbf{e}_i)\).

Second partial derivative of a vector field component: \(\frac{\partial ^2 F_j}{\partial x_i^2}\).

A plasma species with charge \(q\) and mass \(m {\gt} 0\).

Poloidal flux function \(\psi (R, Z)\) with \(C^2\) smoothness and axisymmetry.

Resistive MHD: same as ideal but with \(\mathbf{E} + \mathbf{v}\times \mathbf{B} = \eta \mathbf{J}\). Induction becomes \(\frac{\partial \mathbf{B}}{\partial t} = \nabla \! \times \! (\mathbf{v}\times \mathbf{B} - \eta \mathbf{J})\).

RMF drive parameters: amplitude \(B_\omega {\gt} 0\), frequency \(\omega {\gt} 0\).

A Rotamak: FRC sustained by a rotating magnetic field with 1D Ampère’s law \(dB_z/dR = -\mu _0 J_\theta \).

A scalar field \(f : \mathbb {R}^3 \to \mathbb {R}\).

Scalar Laplacian: \((\nabla ^2_sf)(x) = \sum _{i=0}^{2} \frac{\partial ^2 f}{\partial x_i^2}(x)\).

Scalar–vector field multiplication: \((c\mathbf{F})(x) = c(x)\, \mathbf{F}(x)\).

A source-free Maxwell system: \(\rho = 0\), \(\mathbf{J}_{\mathrm{free}} = 0\).

Smoothness hypotheses for the wave equation derivation: curl-time commutativity, \(C^2\) conditions for fields and their time derivatives, and differentiability of time derivatives.

Time-dependent pointwise addition.

Time-dependent pointwise cross product.

A time-dependent scalar field \(f : \mathbb {R}\to \mathbb {R}^3 \to \mathbb {R}\).

Time-dependent scalar–vector multiplication.

A time-dependent vector field \(\mathbf{F} : \mathbb {R}\to \mathbb {R}^3 \to \mathbb {R}^3\).

Time derivative of a time-dependent scalar field: \(\frac{\partial f}{\partial t}(t, x) = \mathrm{deriv}\; (s \mapsto f(s, x))\; t\).

Second time derivative of a scalar field: \(\frac{\partial ^2 f}{\partial t^2}\).

Time derivative of a time-dependent vector field component: \(\frac{\partial F_j}{\partial t}(t, x) = \mathrm{deriv}\; (s \mapsto F(s, x)_j)\; t\).

Second time derivative of a vector field component: \(\frac{\partial ^2 F_j}{\partial t^2}\).

Two-fluid equations for a single species: continuity and momentum.

Vacuum medium: \(\varepsilon = \varepsilon _0\), \(\mu = \mu _0\), \(\sigma = 0\).

A point or vector in \(\mathbb {R}^3\): the type \(\mathrm{Fin}\, 3 \to \mathbb {R}\).

Cross product of two vectors: wraps Mathlib’s crossProduct.

Dot product of two vectors: wraps Mathlib’s dotProduct.

A vector field \(\mathbf{F} : \mathbb {R}^3 \to \mathbb {R}^3\).

Vector Laplacian: \((\nabla ^2\mathbf{F})(x)_j = \sum _{i=0}^{2} \frac{\partial ^2 F_j}{\partial x_i^2}(x)\).

Vorticity: \(\mathbf{\omega }(t,x) = \nabla \! \times \! \mathbf{v}(t,x)\).

In source-free systems, \(\nabla \! \times \! \mathbf{B} = \mu \sigma \mathbf{E} + \mu \varepsilon \frac{\partial \mathbf{E}}{\partial t}\).

\(\mathbf{a}\times \mathbf{b} = -(\mathbf{b}\times \mathbf{a})\).

Anti-commutativity at the field level.

\((\mathbf{a}\times \mathbf{b})\cdot \mathbf{b} = 0\).

\(\mathbf{a}\cdot (\mathbf{a}\times \mathbf{b}) = 0\).

For \(C^2\) scalar fields, mixed partial derivatives commute (Clairaut/Schwarz):

Connects to Mathlib’s IsSymmSndFDerivAt via the chain rule for CLM evaluation.

\((\mathbf{F}(x)\times \mathbf{G}(x))\cdot \mathbf{G}(x) = 0\).

\(\mathbf{F}(x)\cdot (\mathbf{F}(x)\times \mathbf{G}(x)) = 0\).

\(\nu \ge 0\).

\(\rho \ne 0\).

\(\rho {\gt} 0\).

In source-free systems, \(\nabla \! \cdot \! \mathbf{E} = 0\).

\(C^2\) vector field components are differentiable at every point.

\(\varepsilon \ne 0\).

\(\mu \varepsilon {\gt} 0\).

\(\mu \ne 0\).

\(v^2 {\gt} 0\) since \(\mu , \varepsilon {\gt} 0\).

\(\gamma {\gt} 0\).

\(\mu _0 \ne 0\).

\(\mu _0 {\gt} 0\).

Partial derivatives of \(C^2\) vector fields are differentiable.

\(\mathbf{B}\cdot \nabla p = 0\): magnetic field lines lie on pressure surfaces.

\(\nabla ^2\mathbf{B} = \mu \varepsilon \, \frac{\partial ^2 \mathbf{B}}{\partial t^2} + \mu \sigma \, \frac{\partial \mathbf{B}}{\partial t}\) (telegraph equation).

\(\nabla ^2\mathbf{E} = \mu \varepsilon \, \frac{\partial ^2 \mathbf{E}}{\partial t^2} + \mu \sigma \, \frac{\partial \mathbf{E}}{\partial t}\) (telegraph equation).

\(\nabla \! \cdot \! (\rho \mathbf{v}) = 0\) since \(\rho \) is constant and \(\nabla \! \cdot \! \mathbf{v} = 0\).

\(\nabla \! \times \! (\mathbf{F} + \mathbf{G}) = \nabla \! \times \! \mathbf{F} + \nabla \! \times \! \mathbf{G}\), given differentiability of components.

\(\nabla \! \times \! ((\mathbf{v}\cdot \nabla )\mathbf{v}) = (\mathbf{v}\cdot \nabla )\mathbf{\omega } - (\mathbf{\omega }\cdot \nabla )\mathbf{v}\) for divergence-free \(\mathbf{v}\). The cornerstone identity for vorticity dynamics.

\(\nabla \! \times \! (c\, \mathbf{F}) = c\, (\nabla \! \times \! \mathbf{F})\), given differentiability of components.

\(\nabla \! \times \! (\nabla \! \times \! \mathbf{F}) = \nabla (\nabla \! \cdot \! \mathbf{F}) - \nabla ^2\mathbf{F}\). The critical identity for deriving wave equations. Proved component-by-component using symmetry of mixed partials.

\(\nabla \! \times \! (\nabla f) = 0\) for \(C^2\) scalar fields. Each component \(\frac{\partial }{\partial x_i}\frac{\partial f}{\partial x_j} - \frac{\partial }{\partial x_j}\frac{\partial f}{\partial x_i} = 0\) by symmetry of mixed partials.

\(\nabla \! \times \! (-\mathbf{F}) = -(\nabla \! \times \! \mathbf{F})\).

\(\nabla \! \times \! (\nabla \! \times \! \mathbf{E}) = -\frac{\partial }{\partial t}(\nabla \! \times \! \mathbf{B})\).

\(\nabla \! \times \! (\nabla p) = 0\).

\(\nabla \! \times \! (\nabla ^2\mathbf{v}) = \nabla ^2(\nabla \! \times \! \mathbf{v})\) for sufficiently smooth incompressible velocity fields.

\(\nabla ^2\mathbf{B} = \mu \varepsilon \, \frac{\partial ^2 \mathbf{B}}{\partial t^2}\) in a lossless dielectric.

\(\nabla ^2\mathbf{E} = \mu \varepsilon \, \frac{\partial ^2 \mathbf{E}}{\partial t^2}\) in a lossless dielectric.

\(v^2 = 1/(\mu \varepsilon )\) in a dielectric.

\(\nabla \! \cdot \! \mathbf{B} = 0\) at all times (from the solenoidal axiom).

\(\nabla \! \cdot \! \mathbf{\omega } = 0\): vorticity is solenoidal.

\(\nabla \! \cdot \! (\nabla \! \times \! \mathbf{F}) = 0\) for \(C^2\) vector fields. Expands to a sum of mixed partials that cancel pairwise.

When \(\mu = 0\): \(\rho \frac{D \mathbf{v}}{D t} = -\nabla p + \mathbf{f}\).

When \(\mu = 0\): \(\frac{D \mathbf{v}}{D t} = -\frac{1}{\rho }\nabla p + \frac{1}{\rho }\mathbf{f}\).

\(\nabla p = (1/\mu _0)(\nabla \! \times \! \mathbf{B})\times \mathbf{B}\).

\(\beta = 1\) at the separatrix: \(2\mu _0 p(R_s) = B_{\mathrm{ext}}^2\).

With \(B_\theta = 0\): \(\frac{dp}{dR} + \frac{1}{\mu _0}B_z\frac{dB_z}{dR} = 0\).

\(p(R) = (B_{\mathrm{ext}}^2 - B_z(R)^2)/(2\mu _0)\) when total pressure is conserved.

Derived by taking curl of Ampère, substituting Faraday, and using curl linearity.

Derived by taking curl of Faraday, applying curl-curl identity with \(\nabla \! \cdot \! \mathbf{E}=0\), and substituting Ampère’s law.

\(g\) is constant on flux surfaces.

The Grad-Shafranov equation implies \(\nabla p = \mathbf{J}\times \mathbf{B}\) in cylindrical geometry (\(R \ne 0\)).

If \(\psi (x) = \psi (y)\), then \(p(x) = p(y)\): pressure is constant on flux surfaces.

When \(p(\psi ) = p_0\psi \) and \(g^2(\psi ) = g_0^2 + 2\alpha \psi \) are linear, the GS equation becomes \(\Delta ^*\psi = -\mu _0 R^2 p_0 - \alpha \).

If \(\frac{\partial \mathbf{B}}{\partial t} = -\nabla \! \times \! \mathbf{E}\) and \(\mathbf{E} = -\mathbf{v}\times \mathbf{B}\) (ideal Ohm’s law), then \(\frac{\partial \mathbf{B}}{\partial t} = \nabla \! \times \! (\mathbf{v}\times \mathbf{B})\).

\(\mathbf{J}\cdot \nabla p = 0\): current lines lie on pressure surfaces.

\(\mathbf{J} = (1/\mu _0)\, \nabla \! \times \! \mathbf{B}\).

\(\mathbf{f}_L\cdot \mathbf{B} = \rho _c(\mathbf{E}\cdot \mathbf{B})\) because \((\mathbf{J}\times \mathbf{B})\cdot \mathbf{B} = 0\).

\(\nabla p = (1/\mu _0)((\mathbf{B}\cdot \nabla )\mathbf{B} - \nabla (|\mathbf{B}|^2/2))\): separates magnetic tension and magnetic pressure.

\(\frac{D \mathbf{v}}{D t} = -\frac{1}{\rho }\nabla p + \nu \nabla ^2\mathbf{v} + \frac{1}{\rho }\mathbf{f}\).

The pressure is determined as a constraint enforcing incompressibility.

\(\frac{\partial \mathbf{B}}{\partial t} = \nabla \! \times \! (\mathbf{v}\times \mathbf{B}) - \eta \, \nabla \! \times \! \mathbf{J}\): splits convection and diffusion terms.

When \(\eta = 0\), the resistive induction equation reduces to the ideal one.

Inside the separatrix where \(B_z\) decreases (\(dB_z/dR {\lt} 0\)), the toroidal current \(J_\theta {\gt} 0\).

\(\nabla ^2\mathbf{B} = \mu _0\varepsilon _0\, \frac{\partial ^2 \mathbf{B}}{\partial t^2}\) in vacuum.

\(\nabla ^2\mathbf{E} = \mu _0\varepsilon _0\, \frac{\partial ^2 \mathbf{E}}{\partial t^2}\) in vacuum (\(\sigma = 0\)).

\(c = 1/\sqrt{\mu _0\varepsilon _0}\).

The vortex stretching term \((\mathbf{\omega }\cdot \nabla )\mathbf{v}\) is unique to 3D.