OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/FlowLocal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A genuine C⁴ local flow for the four-dimensional autonomous lift. The path family is identified with its ODE by the proved rescaling uniqueness.

  1. theorem OAI.ContinuumCoulomb.flow_endpoint_deriv_zero line 15
  2. theorem OAI.ContinuumCoulomb.flow_c4_local line 41