Formalizing Ising's result about 1D lattices

Stream: new members

[Thomas C.]

I've been looking for a nice result to formalize to try to get some practice on Lean and I think this one might be a good fit: formalizing the absence of phase transition on the 1 dimensional Ising model.

This is a result that Ising proved in his thesis in 1924 (as explained in this paper), and now we know a trick (the so-called transfer matrix method) which makes it easier to derive.

I think this result could be formalized following the proof given in the section 2.1 of this document:

1. We define the "partition function" $Z_n$ for a cyclic chain of size $n$ — this function depends on several real parameters
2. Using the transfer matrix method as described in the document, we derive an expression for $Z_n$ of the form $\lambda_1^n + \lambda_2^n$ (this is basic algebra on the real numbers).
3. Using this expression, we could also derive the value of the average magnetization and its limit, and how it is continuous (as a function of the external field) for positive temperatures, discontinuous at $T = 0$.

The thing is I don't have experience with Lean and I don't know how to tackle this on my own.

Are there some people here who might be interested in working on it with me?

Also, people with more experience could help identifying what would be needed to formalize this.

[Yan Yablonovskiy 🇺🇦]

If you like you can check out the project at https://github.com/james18lpc/GibbsMeasure

To do this properly in lean i think is fairly/very complicated so i would not suggest this as a first formalised result or for practice. It would be a significant contribution I think.

Edit: In particular the way to do this would be via the link of the average magnetisation and uniqueness of the gibbs measure, the case on the integers as a graph being a special case. There is a lot in the proof you quote that is cited knowledge with regards to that, but it isn't in Lean at all. The project i linked is working towards such results, having defined a Gibbs measure but still needing a lot of work for characterising the uniqueness.