Zelnick Research / Series / About
Symmetry, motion & conserved quantities
An inspectable journey from a physical model to a computation and a small formal definition.
v1.1 · 2026-11-11 · Demonstration content
A question worth following
What stays unchanged while everything else moves? This worked demonstration follows that question through a simple oscillator, a numerical experiment, and a small formal definition. It shows how an explanation and its supporting material can live together.
Demonstration content. The files are usable examples, not original research attributed to the site owner.
Start with a clear model
Take a mass attached to an ideal spring. Let x denote displacement, v velocity, m a positive mass, and k a positive spring constant. Its mechanical energy is
For the ideal differential equation, differentiating this expression along a solution gives zero. That statement has assumptions: the model is isolated, the parameters are constant, and the solution obeys the equations of motion.
Follow the computation
The Python experiment uses velocity-Verlet integration. It writes the state and energy to a CSV, so the numerical error can be inspected separately from the conservation law of the continuous model.
Try a smaller time step and compare the maximum energy deviation. The example uses only the Python standard library.
Inspect the oscillator source or compare the analytic state.
The Lean example defines a squared norm on natural numbers and proves that exchanging its coordinates leaves the value unchanged. This gives a modest, inspectable formal artifact. It is not a formal proof of the oscillator model or of Noether’s theorem.
No Lean validation report is attached to this demonstration. The source is available to inspect and check in a suitable Lean environment.
What the example establishes
The analytic calculation explains conservation for the stated ideal oscillator. The numerical script approximates that motion. The notebook illustrates two energy evaluations, while the Lean file records a different algebraic symmetry. Keeping these scopes explicit makes each artifact easier to interpret.
Use the references to explore the deeper relationship between continuous symmetries and conserved quantities.
Files in this version
Download this version as a ZIP
References
- Conservation of Energy, The Feynman Lectures on Physics I.4 — Richard P. Feynman, Robert B. Leighton and Matthew Sands, 1963
- Invariant Variation Problems (English translation) — Emmy Noether; translated by M. A. Tavel, 1918 / translation 2005
- Validating a Lean Proof — Lean project, n.d.
Demonstration content (2026). Symmetry, motion & conserved quantities. v1.1. Zelnick Research. https://research.zelnick.pw/work/symmetry-and-conservation/?version=v1.1
Interactive version selection and file previews require JavaScript. This fallback shows v1.1.