feat(ClassicalMechanics): add geometric kinetic energy for the harmonic oscillator

[nateabr]

I add a geometric notion of kinetic energy for the harmonic oscillator in a new file, building on the geometric ConfigurationSpace. The metric-induced kinetic energy is defined coordinate-free and parametric in any pseudo-Riemannian metric, and I then construct the oscillator's own mass metric and show it reproduces the standard KE formula.

Some challenges I ran into:

• No inner product on tangent spaces. My first version wrote ⟪v, w⟫ directly on velocities, which doesn't compile, as Mathlib deliberately withholds inner-product/normed instances from TangentSpace. I resolved this with an explicit coordinate identification tangentCoord. I tried installing instances but the instance route creates diamonds.
• Smoothness of the metric. fun_prop couldn't discharge this, because it can't see that the global chart inverse has identity derivative. I added a dedicated lemma establishing exactly that, which collapses the metric to a constant in the chart, after which smoothness is immediate.
• Declaration ordering / defeq. The tangent identification and its finite-dimensional instance had to precede geometricKineticEnergy (whose type already demands them), and I needed a file-scoped set_option backward.isDefEq.respectTransparency false for the tangent≡model identification.

---

Developed with assistance from AI; all mathematics and proofs were reviewed and verified to compile.

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[nateabr]

t-classical-mechanics

[jstoobysmith]

I think abbreviation is wrong here, I think you should be using local notation.

[jstoobysmith]

This should likely go in the Basic.lean file

[jstoobysmith]

Along with the results below (they are not about the kinetic energy)

[jstoobysmith]

I think Mathlib now has RiemannianMetric, so we should probably use this. But should we define an explicit version of this on ConfigurationSpace rather than keeping it a free variable (i.e. move below the definition of the metric).

[jstoobysmith]

Would probably make this a RiemannianMetric. Also would collapse this down to one line, instead of having the arguments spread across different lines.

[nateabr]

Thank you for your comments @jstoobysmith. I hope I have addressed them in the latest commit.

I have moved the parts not pertaining to KE into basic.lean.

Moving to the mathlib remannian metric required a significant rewrite and a new set of proof obligations, therefore I would appreciate if you could take another look to see if I've done things correctly.

I do believe that it was the right design choice to switch as it did not lead to any diamonds, maybe we should rethink physlib's own implementation of the metric in light of this.

-awaiting-author

[jstoobysmith]

This looks good! We probably actually want such a metric on things like Space aswell. I agree we need to rethink the pseudo-reimannian metric in Physlib.

[nateabr]

I will try to add a todo with regards to this after scoping out the relevant files.

Thank you for your review.