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.

[Joseph Tooby-Smith]

I ended up formalizing this, and putting together a quick note on it here:

https://notes.physlean.com/Condensed-matter/The-tight-binding-chain/#TightBindingChain

I'll like share this on social media at some point to try and get more people interested in this project (if anyone has any other ideas of how to do this - please let me know :)).

[Shlok Vaibhav]

Hi Joseph, Alex, Tyler!
Got interested in this project after seeing your paper on formalizing Wick's theorem. I was going through the code on tight-binding lemmas and came here to ask a doubt. First, few observations:
image.png
On line 94 of attached image, a portion of line is  ∑ n : Fin T.N, (|n⟩⟨n + 1| where |n⟩⟨n + 1| is the matrix defined at line 76:
noncomputable def localizedComp {T : TightBindingChain} (m n : Fin T.N) :  ...
My confusion is : in this definition, m and n are both elements of Fin T.N whereas on line 94, n=n+1 so when n takes the largest value = T.N, |n⟩⟨n + 1| should not be defined as N+1 is not part of Fin T.N and the matrix localizedComp is not defined for this integer but lean doesn't throw any compilation error. What is the resolution? Thanks!

[Joseph Tooby-Smith]

Hey! Welcome to the project Shlok.!

The resolution is the following:

This version of the tight binding model in that file assumes cyclic boundary conditions. The + in |n⟩⟨n + 1| is addition in Fin T.N, which is defined to be addition modulo T.N.

The largest value in Fin T.N is T.N-1, and in that highlighted sum the term |T.N - 1⟩⟨(T.N - 1) + 1| is equal to |T.N - 1⟩⟨0|.

[Shlok Vaibhav]

Thanks! So the definition of addition in Fin takes care of it.

[Joseph Tooby-Smith]

Yep :). The example below is completely explicit version of this:

import Mathlib

example : (2 : Fin 3) + (1 : Fin 3) = (0 : Fin 3) := by
  rfl

[Shlok Vaibhav]

Ah I see, should have thought of testing it. This is the first code I'm reading in lean 4 thinking I will just familiarize myself with the tactics and types that are being used in this tight-binding context so don't have any hands on as of now :sweat_smile: Thanks again for quick reply!

[Joseph Tooby-Smith]

No worries - always happy to answer questions :). Maybe we should change the doc-string of hamiltonian to something like:

/-- The Hamiltonian of the tight binding chain with periodic
  boundary conditions is given by `E₀ ∑ n, |n⟩⟨n| - t ∑ n, (|n⟩⟨n + 1| + |n + 1⟩⟨n|)`.
 The periodic boundary conditions is manifested by the `+` in `n + 1` being
  within `Fin T.N` (that is modulo `T.N`).
-/

[Shlok Vaibhav]

In the tight-binding lean code, The hermiticity semiformal result is currently stated on line 101 as :
image.png

semiformal_result "BUEDT" hamiltonian_hermitian (ψ φ : T.HilbertSpace) :

    ⟪T.hamiltonian ψ, φ⟫_ℂ = ⟪ψ, T.hamiltonian φ⟫_ℂ

If I consider a very simple case of T.hamiltonian = |T.N⟩⟨T.N| so I have to prove:
⟪|T.N⟩⟨T.N| ψ, φ⟫_ℂ = ⟪ψ, |T.N⟩⟨T.N| φ⟫_ℂ

I can think of two ways to prove this, first, |T.N⟩⟨T.N| can be shown to be equal to ((|T.N⟩⟨T.N|)^T)* but you won't have written the statement of hermiticity in terms of inner products if this could be done.
The other way I can think of is expanding φ and ψ in the eigenbasis localizedState, |n⟩ so that
⟪|T.N⟩⟨T.N| $\sum_{n} \alpha_{n,\psi} |n⟩$, $\sum_m \alpha_{m,\phi} |m⟩$⟫_ℂ = ⟪$\sum_n \alpha_{n,\psi} |n⟩$, |T.N⟩⟨T.N| $\sum_m \alpha_{m,\psi} |m⟩$ ⟫_ℂ where $\alpha_{n,\psi} =⟨n|\psi⟩$
which should, after applying a series of simp only tactics reduce to

$\sum_n \sum_m \alpha^*_{n,\psi}\alpha_{m,\phi}$ ⟪|T.N⟩⟨T.N||n⟩, |m⟩ ⟫_ℂ =$\sum_n \sum_m\alpha^*_{n,\psi} \alpha_{m,\phi}$⟪ |n⟩, |T.N⟩⟨T.N| |m⟩ ⟫_ℂ

since |T.N⟩⟨T.N| |m⟩ is defined on line 89 under lemma localizedComp_apply_localizedState, the LHS and RHS might be shown equal after some tactics. Is this a correct and good strategy?

[Joseph Tooby-Smith]

Yes, I think this is a good and correct strategy. It might be nice to break the prove up a bit and write a general lemma relating ⟪ |n⟩, |p⟩⟨k| |m⟩ ⟫_ℂ to ⟪|p⟩⟨k| |n⟩, |m⟩ ⟫_ℂ, and then use the basis of localized states.

[Joseph Tooby-Smith]

I suspect if you show that ((|T.N⟩⟨T.N|)^T)* = |T.N⟩⟨T.N| (more properly written as
Matrix.conjTranspose (|T.N⟩⟨T.N|) = |T.N⟩⟨T.N|) this todo item should also follow from it using the appropriate lemmas e.g.
docs#LinearMap.adjoint_inner_left, docs#Matrix.toEuclideanLin_conjTranspose_eq_adjoint etc.

[Shlok Vaibhav]

Right, I think it will be useful later to have hopping matrices results in localized eigenbasis. I could prove ⟪ |n⟩, |p⟩⟨k| |m⟩ ⟫_ℂ = ⟪|k⟩⟨p| |n⟩, |m⟩ ⟫_ℂ
and from there, hermiticity of hopping matrix |p⟩⟨k|+|k⟩⟨p| but need to do this with the hopping parameter T.t included
image.png

/-- Shown that |p⟩⟨k| and |k⟩⟨p| are identical matrices (since hopping parameter has been excluded)

in the localized (euclidean) eigenbasis
-/

lemma Ham_off_diag_eq_local (m n k p : Fin T.N):

  ⟪|n⟩ , |p⟩⟨k| |m⟩  ⟫_ℂ = ⟪|k⟩⟨p| |n⟩ ,  |m⟩ ⟫_ℂ :=

  by

  simp only [localizedComp_apply_localizedState]  /- Simplifies both sides to two ite equations-/

  split_ifs with h1 h2 h3                         /- resulting in four subgoals-/

  · simp only [localizedState_orthonormal_eq_ite]                  /- k=m and p=n-/

    rw[h1, h2]

    simp

  · simp only [localizedState_orthonormal_eq_ite,inner_zero_left]  /- k=m and ¬(p=n) -/

    rw [eq_comm] at h2

    simp

    exact h2

  · simp only [localizedState_orthonormal_eq_ite,inner_zero_right] /- ¬(k=m) and p=n -/

    symm

    simp

    exact h1

  · simp                                                           /- ¬(k=m) and ¬(p=n) -/

/-- The hermiticity of hopping matrix between arbitrary |p⟩ and |k⟩ is proven

in the localized (euclidean) eigenbasis
-/

lemma Ham_off_diag_hermit_local (m n k p : Fin T.N):

  ⟪|n⟩ , (|p⟩⟨k|+|k⟩⟨p|) |m⟩  ⟫_ℂ = ⟪(|p⟩⟨k|+|k⟩⟨p|) |n⟩ ,  |m⟩ ⟫_ℂ :=

  by

  simp only [smul_add,LinearMap.add_apply]

  rw [inner_add_right, inner_add_left]

  simp only[Ham_off_diag_eq_local]

  rw[add_comm]

/-- The hermiticity of on-site energy is proven

 in the localized (euclidean) eigenbasis

 -/

lemma Ham_diag_hermit_local (m n k : Fin T.N):

  ⟪|n⟩ , (|k⟩⟨k|) |m⟩  ⟫_ℂ = ⟪(|k⟩⟨k|) |n⟩ ,  |m⟩ ⟫_ℂ :=

  by

  simp only[Ham_off_diag_eq_local]

[Joseph Tooby-Smith]

This looks good to me! I'm not sure I understand your comment about the hopping parameter though? Do you mean, you really want to show that
T.t (|p⟩⟨k|+|k⟩⟨p|) is hermitian? If so, I think this should be a simple consequence of what you have already. But in any case, this all looks good!

(Also a quick side comment, the doc-string of your first result is slightly wrong, as you show that |p⟩⟨k| and |k⟩⟨p| are adjoint to one another but not equal :)).

[Shlok Vaibhav]

Do you mean, you really want to show that T.t (|p⟩⟨k|+|k⟩⟨p|) is hermitian?

I meant proving it for a hopping parameter that can take complex values (in case we later want to prove results related to complex hopping values like use of Peierels substitution, we dont have to rederive all lemmas from scratch). Is this a right thought whose time has come? Or something that should be tackled later?

[Shlok Vaibhav]

Ohh right! It's Adjoint. Thanks for correcting!

[Joseph Tooby-Smith]

Ah! Thank you for explaining! Yes I think this is good - and maybe we should generalise this whole file to have a complex hopping value, and then where needed (which might not be anywhere) restrict to the real case. I think now is a good time for this

[Joseph Tooby-Smith]

Maybe another nice thing to do in this direction would be tight-binding for graphene:

This paper seems to give a pretty straightforward description.

[Shlok Vaibhav]

That's a good idea! To make the unit cell 2-d (or later, N-d) plus the ubiquity of Graphene and derivative structures.

[Joseph Tooby-Smith]

Can't claim it was all my idea :) - came out of conversations I was having with others. But yeah, seems like a good natural extension

[Shlok Vaibhav]

Had been trying to prove the semiformal result on the orthogonality of the energy eigenstates.
Was hoping to finish it this weekend but reached the point where I have a single goal I'm stuck at : (k1, k2: Fin T.N)

⊢ Complex.exp (2 * Complex.I * ↑Real.pi * (↑↑k2 - ↑↑k1) / ↑T.N) ≠ 1

I can prove that -1< (↑↑k2 - ↑↑k1) / ↑T.N <1 and also not zero since pairwise keyword is used. This will show that the argument is not a multiple of 2 pi i. Will try to see some sample code on proving such exponent inequalities on github or deepseek.
Spent few hours on this but was not able to find correct tactics for it or any strategy to come with a different statement. Deep Seek Prover V2 could do it but not relying on it so as to learn the language so this theorem will likely get pushed to the coming week.
image.png

[Joseph Tooby-Smith]

You are trying to solve the following, right (where you T.N is just N here)?

import Mathlib

example (N : ℕ) (k1 k2 : Fin N) (h : k1 ≠ k2) :
       Complex.exp (2 * Complex.I * ↑Real.pi * (↑↑k2 - ↑↑k1) / ↑N) ≠ 1 := by
   sorry

I have a solution to this, but am not going to share it unless you ask (since you are trying to learn :)), but the first three lines of my solution are:

  by_contra hn
  rw [Complex.exp_eq_one_iff] at hn  -- found using rw? at hn
  obtain ⟨m, h⟩ := hn

The rest is a long but straight forward calculation using things like omega and field_simp.

[Shlok Vaibhav]

sorry for leaving this hanging, got bogged down in office work since last few weeks, the theorem i have been working on is to prove the orthogonality of eigenstates of tight binding.

lemma exp_k1_neq_k2 (k1 k2 : Fin T.N) (h : k1 ≠ k2) :
  Complex.exp (2 * Complex.I * ↑Real.pi * (↑↑k2 - ↑↑k1) / ↑T.N) ≠ 1 := by
  by_contra hn
  rw [Complex.exp_eq_one_iff] at hn  -- found using rw? at hn
  obtain ⟨m, h1⟩ := hn
  have h3: ↑m * (2 * ↑Real.pi * Complex.I) = (2 * ↑Real.pi * Complex.I) * ↑m := by
    simp only [mul_assoc, mul_comm]
  have h4: (2 * ↑Real.pi * Complex.I) * ↑m = (2  * Complex.I * ↑Real.pi) * ↑m := by
    ring
  rw [h3] at h1
  rw [h4] at h1
  #check h1

  have h5: Complex.I * ↑Real.pi * (↑↑k2 - ↑↑k1) / ↑T.N = Complex.I * ↑Real.pi * ↑m := by
    linear_combination h1/2
  have h6: Complex.I * ↑Real.pi * (↑↑k2 - ↑↑k1)/ ↑T.N * ↑T.N  = Complex.I * ↑Real.pi * ↑m * ↑T.N  := by
    linear_combination h5 * ↑T.N
  have h7: Complex.I * ↑Real.pi * (↑↑k2 - ↑↑k1)  = Complex.I * ↑Real.pi * ↑m * ↑T.N  := by
    rw [@div_mul_cancel_of_invertible] at h6
    exact h6

  have h8: Complex.I *(Real.pi * (↑↑k2 - ↑↑k1))  = Complex.I *(Real.pi * (↑m * ↑T.N))  := by
    simp only [mul_assoc] at h7
    exact h7


  have h9: k2 - k1 = m * T.N := by
    simp only [mul_eq_mul_left_iff, Complex.I_ne_zero,mul_eq_mul_left_iff,Complex.ofReal_eq_zero,or_false,Real.pi_ne_zero] at h8
    exact h8

image.png
I am stuck at type mismatch since quite some time, I am not able to either get the type of h8 changed to that of h9 or change the h9 lemma to match the type of h8. Once the types are matched, i can show

$$-1\le m \le 1$$

since k1, k2 are in Fin T.N and m is not 0 as

$$k1\neq k2$$

which proves that m is not an integer and hence the hn statement is false, which completes the proof by contradiction
But i now anticipate if i am not having these types matched, i wont be able to use properties of integers to prove these either. Hence decided to post this query here and get my understanding clear

[Joseph Tooby-Smith]

The problem is that in h9 everything is an integer, but in h8 everything is a complex number, so to prove h9 you need to cast from the integers to the complex numbers:

have h9: k2 - k1 = m * T.N := by
    simp only [mul_eq_mul_left_iff, Complex.I_ne_zero,mul_eq_mul_left_iff,Complex.ofReal_eq_zero,or_false,Real.pi_ne_zero] at h8
    rw [← Int.cast_inj (α := ℂ)] -- rewrites the equation in complex numbers
    simp only [Int.cast_sub, Int.cast_natCast, Int.cast_mul]
    exact h8

[Shlok Vaibhav]

Thanks! I couldn't think of this earlier but now I see it's more manageable to upconvert h9 type instead to complex as part of proof