Tracker: formalize CPP slow-manifold theory in Lean

[krystophny]

Goal

Formalize the literature-level CPP slow-manifold theory in Lean. The end product should state and prove the theorem that the canonical Pauli particle has a slow invariant manifold carrying guiding-center dynamics under explicit magnetic-field, scale-separation, and initialization hypotheses. The proof should also state the numerical consequence used by SIMPLE: CPP timesteps resolve the slow reduced motion and the implicit solve, not the full CP gyro-orbit.

This is a planning tracker. It should be split before implementation. Do not treat it as one PR-sized task.

Public references

• Xiao and Qin, Slow manifolds of classical Pauli particle enable structure-preserving geometric algorithms for guiding center dynamics, Computer Physics Communications 265, 107981, 2021. DOI: 10.1016/j.cpc.2021.107981.
• Mathlib manifold integral-curve infrastructure: Mathlib.Geometry.Manifold.IntegralCurve.*.
• Mathlib ODE infrastructure: Mathlib.Analysis.ODE.PicardLindelof, Mathlib.Analysis.ODE.Gronwall.
• Mathlib implicit-function infrastructure: Mathlib.Analysis.Calculus.ImplicitFunction.*.
• Mathlib differential forms on normed spaces: Mathlib.Analysis.Calculus.DifferentialForm.*.

Theorem to extract first

Write the exact theorem statement before any Lean code beyond scaffolding.

The first pass should answer these points from Xiao and Qin, with equation numbers:

• What is the small parameter? Name whether it is epsilon, rho_star, 1/q, or a nondimensional gyroperiod ratio.
• What phase space is used? State coordinates, canonical symplectic form, and Hamiltonian.
• What regularity is assumed for A(q), B(q), b(q), and the metric? State the required C^r order.
• What domain is used? Exclude B = 0, coordinate singularities, wall crossings, and metric degeneracy.
• What object is called the slow manifold? Decide whether the paper uses an exact invariant graph, an asymptotic invariant graph, or a formal slow manifold.
• What stability class is used? Do not assume Fenichel normal hyperbolicity until the paper supports it. Hamiltonian gyro motion is elliptic, so center-manifold or averaging machinery may be the right abstraction.
• What is proven about reduced dynamics? State the order of agreement with guiding-center equations.
• What initialization hypothesis puts CPP on or near the slow manifold?
• What numerical theorem supports large CPP timesteps? Separate the continuous slow-manifold theorem from the discrete midpoint algorithm.

Atomic split to file

• [lean-cpp-01] Extract the CPP slow-manifold theorem from Xiao-Qin: produce a theorem inventory with assumptions, definitions, and equation references.
• [lean-cpp-02] Create the Lean project and CI target: add a small Lean workspace, pinned toolchain, mathlib dependency, and a CI job that checks the proof files.
• [lean-cpp-03] Formalize finite-dimensional canonical phase space: define q,p, canonical pairing, gradients, and Hamiltonian vector fields in coordinates.
• [lean-cpp-04] Formalize the CPP Hamiltonian: define H_CPP = 1/2 (p - Q A(q))^T g^{-1}(q) (p - Q A(q)) + mu B(q) under abstract smooth-field assumptions.
• [lean-cpp-05] Prove the CPP Hamilton equations: derive qdot and pdot from H_CPP, including all metric, vector-potential, and mu B terms.
• [lean-cpp-06] Define the scale-separated CPP problem: introduce the small parameter, bounded field constants, and the compact regular domain.
• [lean-cpp-07] Classify the slow-manifold theorem needed: prove or import the precise finite-dimensional theorem used by Xiao-Qin, after deciding between invariant graph, center manifold, averaging, or another statement.
• [lean-cpp-08] Prove CPP slow-manifold existence: apply the theorem to the CPP vector field and construct the slow graph with explicit hypotheses.
• [lean-cpp-09] Prove reduced dynamics agrees with guiding-center dynamics: state and prove the order of agreement between the CPP slow flow and GC equations.
• [lean-cpp-10] Formalize CPP initialization: prove the parallel-only CPP initialization lies on the leading slow manifold and quantify the defect for finite epsilon.
• [lean-cpp-11] Formalize implicit midpoint for CPP: define the discrete map as the implicit midpoint method for H_CPP and prove its symplecticity in canonical coordinates.
• [lean-cpp-12] State the large-step CPP condition: prove or state, with assumptions, that CPP timestep restrictions come from slow-flow accuracy and nonlinear-solve convergence, not CP gyro-orbit resolution.
• [lean-cpp-13] Connect the proof to SIMPLE notation: map SIMPLE's normalized ro0, mu, vpar, z(4), z(5), and MODEL_CPP_SYM residual to the Lean definitions.
• [lean-cpp-14] Add code-facing proof certificates: export small theorem statements or generated checks that can guard the CPP Jacobian and midpoint residual used in src/orbit_cpp_canonical.f90.

Parallelization map

These lanes can run in parallel after [lean-cpp-01] fixes the theorem names and symbols.

• Literature lane: [lean-cpp-01], then review [lean-cpp-07], [lean-cpp-08], [lean-cpp-09].
• Lean infrastructure lane: [lean-cpp-02] can start immediately.
• Coordinate Hamiltonian lane: [lean-cpp-03], [lean-cpp-04], [lean-cpp-05] can proceed once the theorem inventory fixes notation.
• Analysis lane: [lean-cpp-06], [lean-cpp-07], [lean-cpp-08] is the long pole. It should be split further if the slow-manifold theorem is not already close to mathlib.
• Guiding-center lane: [lean-cpp-09], [lean-cpp-10] depends on the coordinate Hamiltonian lane and the theorem classification.
• Discrete algorithm lane: [lean-cpp-11], [lean-cpp-12] depends on the coordinate Hamiltonian lane but not on the full slow-manifold proof.
• SIMPLE binding lane: [lean-cpp-13], [lean-cpp-14] depends on the coordinate Hamiltonian lane and can start before the full analysis lane finishes.

Critical path

1. Extract the theorem exactly from Xiao-Qin.
2. Decide the slow-manifold mechanism: invariant graph, formal asymptotic slow manifold, center manifold, averaging, or normal hyperbolicity.
3. Formalize the supporting theorem in Lean.
4. Apply it to the CPP Hamiltonian.
5. Prove agreement with GC equations.
6. Add the discrete midpoint and SIMPLE binding layers.

The risk is concentrated in steps 2 and 3. If the theorem requires a new center-manifold or averaging library, that library is its own research project.

First deliverable

The first PR should not contain the full proof. It should contain:

• a Lean project that builds;
• one file with definitions for finite-dimensional canonical coordinates;
• one file with theorem names marked as declarations only if needed for planning;
• a markdown theorem inventory generated from the public paper, with equation references and no private notes.

Acceptance

This tracker is complete when every item in the atomic split is filed as an implementation issue or explicitly dropped with a reason. Each child issue must be independently reviewable and must name its Lean files, theorem names, and verification command.

Non-goals

• Do not formalize VMEC, Boozer splines, or wall geometry in the first proof.
• Do not prove full CP gyro-resolution error bounds as part of the CPP slow-manifold proof.
• Do not replace the theorem extraction with a generic Fenichel statement unless the paper's hypotheses match it.
• Do not mix the code bug in orbit_cpp_canonical with the Lean theorem work; link code-facing certificates only after the definitions are stable.

[krystophny]

Started this. Repo: gitlab.tugraz.at/plasma/proj/cpp-derivation (Lean 4 + Mathlib, lake math project, builds green).

Scaffolded the atomic split. Status:

• lean-cpp-01 theorem inventory: done. Correction to the premise: Xiao-Qin (CPC 265, 2021; arXiv:2006.03818) states the slow-manifold idea and demonstrates it numerically, but proves none of the existence, regularity, error-order, or step-size claims. The rigorous backbone is Burby-Hirvijoki (arXiv:2104.02190): nearly-periodic systems, Kruskal roto-rate U(1) symmetry, adiabatic invariant with a Hessian-positivity normal-stability condition. The fast gyromotion is elliptic, so the mechanism is averaging / adiabatic invariant, not Fenichel normal hyperbolicity (as already noted above).
• lean-cpp-02 project + CI: done (pinned toolchain, mathlib cache, GitLab CI build job).
• lean-cpp-03, lean-cpp-04 phase space + Hamiltonian: done. H = (1/2m)(p_i - qc A_i) g^{ij} (p_j - qc A_j) + mu|B| with abstract smooth-field hypotheses (g symmetric positive definite with inverse field, A, |B| all C^infty).
• lean-cpp-05 Hamilton equations: stated and assembled; two gradient lemmas (quadratic-form momentum gradient, configuration chain rule) remain sorry. Pure Mathlib calculus, no literature dependency.
• lean-cpp-06, lean-cpp-07 scale-separated problem + classification: done.
• lean-cpp-08, lean-cpp-09 slow-manifold existence + guiding-center agreement: statements present, proofs sorry, gated on the Burby-Hirvijoki read (small-parameter normalization, normal-stability hypothesis and time horizon, agreement order).
• lean-cpp-13 SIMPLE binding: done. ro0, ro0_bar, qc = charge/(c ro0), mu, z(4:5), and the MODEL_CPP_SYM implicit-midpoint residual bound to the Lean definitions.
• lean-cpp-10, lean-cpp-11, lean-cpp-12, lean-cpp-14: not started.

Build is green with four sorry obligations, none in any definition or statement.

Next: discharge the two lean-cpp-05 gradient lemmas (literature-independent), then read Burby-Hirvijoki in full to fix the SlowManifold hypotheses and prove 08/09.

[krystophny]

Closing as superseded: this targets the abandoned feature/simple-6d-port CP/CPP pusher (orbit_cpp_*.f90, orbit_model 5/6/8), which was explicitly dropped by #429. None of the referenced files/models exist on main.