Good first steps into condensed matter physics?

Stream: PhysLean

[Joseph Tooby-Smith]

One of the areas of PhysLean which is not really developed at all is condensed matter physics. I think it would be nice to have one or two things done in this direction within PhysLean to serve as a bit of an impetus.

I don't currently have the time to do this right now, but I wanted to know if anyone had suggestions of some simple things (e.g. undergraduate level) that could get us started in the direction of condensed matter physics. E.g. maybe something to do with lattices, the second quantization etc.

(Somewhat related - a fair while a go I asked in the chat of Physics stack exchange if a question like Kevin's math-overflow question:

Which mathematical definitions should be formalized in Lean?

but physics based would be on-topic... they said no :( as they don't like big-list questions. )

[Joseph Tooby-Smith]

One idea might be the 1D tight binding chain.

[Tyler Josephson ⚛️]

I’d love to see Onsager’s solution to the 2D Ising model. Maybe the transfer matrix techniques he developed would be appropriate for Mathlib?

[Alex Meiburg]

I've also dreamt about Onsager's solution for a while! Another "easy" objective is showing that BEC undergoes a phase transition where it condenses.

(That is, formally: a bunch of identical bosons in a Hamiltonian with a gap, like (say) a harmonic oscillator spectrum. You get the fraction of the population of N particles, as a function of temperature, and then take the limit as N -> infty, and this converges to some function f(T). Prove there's a critical temperature T0 so that for all T >= T0, f(T) = 0, and for all T < T0, f(T) is positive.)

[Alex Meiburg]

I've tried looking into proving this and it's actually quite hard to make totally rigorous, though. Computing and bounding the contributions of the excited states (and showing they're sufficiently small) is usually done with a saddle-point method, which is not rigorous.

[Joseph Tooby-Smith]

Thanks for the suggestions both! Ideally I would like a couple of things which one could knock off in a week or so. Maybe BEC phase transitions are a possibility here, or maybe there is some simpler version.

[Joseph Tooby-Smith]

Looking a bit more into the 1D tight binding chain, I think it might be a good candidate for small place to start.

These notes by David Tong do a pretty good job of explaining it: https://www.damtp.cam.ac.uk/user/tong/aqm/aqmtwo.pdf.

I created a small issue/feature-request on the repo concerning this: https://github.com/HEPLean/PhysLean/issues/523.