wrong formalization of boyle's law in lean

Stream: Natural sciences

[Bulhwi Cha]

import Mathlib.Data.Real.Basic

lemma Boyle
    -- Variables
    (P1 P2 V1 V2 T1 T2 n1 n2 R : ℝ)
    -- Assumptions
    (a1 : P1 * V1 = n1 * R * T1)
    (a2 : P2 * V2 = n2 * R * T2)
    (a3 : T1 = T2)
    (a4 : n1 = n2) :
    -- Conjecture
    P1 * V1 = P2 * V2 := by
  rw [a3] at a1
  rw [a4] at a1
  exact (rfl.congr (Eq.symm a2)).mp a1

lemma just_a_random_example (x₁ x₂ y₁ y₂ z₁ z₂ w₁ w₂ k : ℝ)
    (h₁ : x₁ * y₁ = w₁ * k * z₁) (h₂ : x₂ * y₂ = w₂ * k * z₂)
    (h₃ : z₁ = z₂) (h₄ : w₁ = w₂) : x₁ * y₁ = x₂ * y₂ := by
  rw [h₁, h₂, h₃, h₄]

theorem Boyle_is_just_a_random_example : Boyle = just_a_random_example := rfl

I think the lemma Boyle should be removed from LeanChemicalTheories. It's not a correct formalization of Boyle's law; it's merely an example of using rewriting. We need to formally define the pressure and the volume of a confined ideal gas. Then we should use those definitions to state Boyle's law correctly in Lean. But currently, I have no idea how to define them.

[Scott Morrison]

Presumably one defines an ideal gas as some limit of systems with non-interacting particles with velocities assumed to follow Maxwell's distribution. (i.e. blackboxing as a hypothesis how they actually end up in that distribution). Then calculating the pressure is "just" some integration problem. I suspect mathlib is not ready to support this calculation yet, but perhaps it is close.

[Yury G. Kudryashov]

One can define

axiom idealGasConst : Real

structure IdealGasState where
  pressure volume temperature amount : {x : Real // 0 < x}
  law : pressure * volume = amount * idealGasConst * temperature

then write

theorem IdealGasState.boyle (a b : IdealGasState) (ht : a.temperature = b.temperature)
    (hn : a.amount = b.amount) : a.pressure * a.volume = b.pressure * b.volume := by
  rw [...]

theorem IdealGasState.charles (a b : IdealGasState) (hp : a.pressure = b.pressure)
    (hn : a.amount = b.amount) : a.volume * b.temperature = b.volume * a.temperature := by
  rw [...]

-- similarly for Avogadro's and Gay-Lussac's

Of course, these implications are not deep results.

[Yury G. Kudryashov]

(you may need R > 0 for some of these)

[Yury G. Kudryashov]

But this (with a couple more definitions) allows one to talk about, e.g., efficiency of different thermodynamic cycles.

[Yury G. Kudryashov]

Probably, a better approach would be

-- TODO: should we require positivity
structure GasState where
  pressure volume temperature amount : {x : Real // 0 < x}

namespace GasState

def IsIdeal : pressure * volume = R * amount * temeperature

def IsothermalOn (f : X -> GasState) (s : Set X) : Prop :=
  ∀ a ∈ s, ∀ b ∈ s, (f a).temperature = (f b).temperature

theorem IsothermalOn.boyle {f : X → GasState} {s : Set X} (h : IsothermalOn f s) {a b : X}
    (ha : a ∈ s) (hb : b ∈ s) (h' : (f a).amount = (f b).amount) : (f a).pressure * (f a).volume = (f b).pressure * (f b).volume :=

[Yury G. Kudryashov]

I guess, one can start with this and formalize, e.g., Carnot's theorem https://en.wikipedia.org/wiki/Carnot%27s_theorem_(thermodynamics)

[Yury G. Kudryashov]

Disclaimer: I'm very far from being an expert in chemistry or physics.

[Tyler Josephson ⚛️]

@Max Bobbin pointed this out when we first wrote up that proof of Boyle's Law - indeed, this is, mathematically speaking, not that interesting. I still like it for illustrating Lean to newcomers - indeed, it only illustrates the rewrite tactic, but this is handy in an oral presentation setting to an audience with zero background in theorem proving.

We have a more rigorous treatment here, where we use structures. But we still have a long ways to go to connect this to either classical or statistical thermodynamics.

[Bulhwi Cha]

Tyler Josephson ⚛️ said:

Max Bobbin pointed this out when we first wrote up that proof of Boyle's Law - indeed, this is, mathematically speaking, not that interesting. I still like it for illustrating Lean to newcomers - indeed, it only illustrates the rewrite tactic, but this is handy in an oral presentation setting to an audience with zero background in theorem proving.

I think this "proof" of Boyle's law is misleading. This lemma doesn't "prove" Boyle's law; it only proves that just_a_random_example is true.

[Yury G. Kudryashov]

It proves that Boyles' law follows from the ideal gas equation. The docstring should clearly indicate that.

[Bulhwi Cha]

It still doesn't mention the definitions of the pressure and the volume of a confined ideal gas. Without these definitions
, variables such as P1 and V1 can't have physical meanings; they become nothing but real numbers.

[Bulhwi Cha]

I should also point out that @David⚛️'s formalization of the Darcy-Weisbach equation has the same problem. Where's the definition of force? Premises like h₃ : F = f₁ * P * L * U^2 are not definitions. These formalizations are all underspecifications!

Tomas Skrivan said:

I'm looking forward to seeing a refactored version where it is clear what are the assumptions, definitions and empirical facts!

[Shreyas Srinivas]

I don't understand. In what sense is pressure or volume unspecified from a math formalisation PoV?

[Shreyas Srinivas]

as far as thermodynamics is concerned these are just some state variables right?

[Scott Morrison]

I remain pretty unclear what formalization of physics and/or chemistry is even meant to mean. Formalization of mathematical physics I think I do understand: e.g. you define symplectic manifolds "properly", and then add a paragraph to the doc-string that begins "Hamiltonian mechanics describes physical systems via a symplectic manifold ..."

[Scott Morrison]

Or e.g. my formalisation of the CHSH inequalities file#Algebra/Star/CHSH. It is a fact about ordered *-algebras, and then the "physics" that is not just maths all belongs in doc-strings.

[Scott Morrison]

I mean, there is lots of serious physics that is not formalizable because we don't understand the mathematics underlying it clearly enough yet, but I don't think this part of physics is relevant to the discussion here.

[Shreyas Srinivas]

I do wonder if we can have a formalization of units in lean (more specifically dimensionality analysis of an expression). I know types play a role in CS not entirely unlike units in a physics in the sense that if the types of objects don't match up then you can't perform operations on them. But units are a little more complicated than that. For each unit, you also have its inverse (second and second^{-1} I.e. hertz) further you have cancellation laws that allow you to multiply a speed object (with units m/s) with a time object (of unit s) to give a distance object (unit m)

[Shreyas Srinivas]

Basically such a type checking would not allow addition of two quantities of different units. But at the same time it could deduce the units of a product of quantities and allow for inverses, and require that equality only work for quantities of the same unit.

[Shreyas Srinivas]

To this extent a math formalization of physics would also exclude malformed equations.

[Eric Wieser]

There are already threads about dimensional analysis elsewhere

[Bulhwi Cha]

Shreyas Srinivas said:

I don't understand. In what sense is pressure or volume unspecified from a math formalisation PoV?

I'll give you an example. I think it's still an underspecification, but this is the best I can do at the moment.

Let $g$ be a gas, whatever that means. We specify the motion of the $g$ on the time interval $\left[ 0, \ \infty \right)$ as follows:

• $n = \mathrm{partN} \ g \in \N$ is the number of the particles that make up the gas $g$.
• $\vec{\mathrm{s}}_g : \mathrm{Fin} \ n \rightarrow \R_{\ge 0} \rightarrow \R^3$ is the motion of the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.
• $\vec{\mathrm{s}}_g \left( i \right) : \R_{\ge 0} \rightarrow \R^3$ is the motion of the $i$-th particle of the gas $g$ on the time interval $\left[ 0, \ \infty \right)$. It has a continuous first derivative.
• $\vec{\mathrm{s}}_g \left( i, \ t \right) = \vec{\mathrm{s}}_g \left( i \right) \left( t \right) \in \R^3$ is the position of the $i$-th particle of the gas $g$ at time $t$.

We specify the volume of the gas $g$ as follows:

• $C_{\mathrm{bot}} = \left\{ \left( x, \ y, \ z \right) \in \R^3 \ \middle| \ x^2 + y^2 \le 1 \wedge z = 0 \right\}$ is the bottom base of the right circular cylinder $C$.
• $C_{\mathrm{side}} = \left\{ \left( x, \ y, \ z \right) \in \R^3 \ \middle| \ x^2 + y^2 = 1 \wedge 0 \le z \le 2 \right\}$ is the side of the cylinder $C$.
• $h_{\mathrm{top}}: \R_{\ge 0} \rightarrow \left[ 0, \ 2\right]$ is the height of the surface $S_{\mathrm{top}}$ on the time interval $\left[ 0, \ \infty \right)$. It has a continuous first derivative.
• $S_{\mathrm{top}} : \R_{\ge 0} \rightarrow \mathrm{Set} \ \R^3, \ t \mapsto \left\{ \left( x, \ y, \ z \right) \in \R^3 \ \middle| \ x^2 + y^2 \le 1 \wedge z = h_{\mathrm{top}}\left( t \right) \right\}$ is the top base of the control surface $S$ on the time interval $\left[ 0, \ \infty \right)$.
• $S_{\mathrm{side}} : \R_{\ge 0} \rightarrow \mathrm{Set} \ \R^3, \ t \mapsto \left\{ \left( x, \ y, \ z \right) \in \R^3 \ \middle| \ x^2 + y^2 = 1 \wedge 0 \le z \le h_{\mathrm{top}}\left( t \right) \right\}$ is the side of the control surface $S$ on the time interval $\left[ 0, \ \infty \right)$.
• $S : \R_{\ge 0} \rightarrow \mathrm{Set} \ \R^3, \ t \mapsto S_{\mathrm{top}} \left( t \right) \cup S_{\mathrm{side}} \left( t \right) \cup C_{\mathrm{bot}}$ is the control surface of the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.
• $D : \R_{\ge 0} \rightarrow \mathrm{Set} \ \R^3, \ t \mapsto \left\{ \left( x, \ y, \ z \right) \in \R^3 \ \middle| \ x^2 + y^2 \le 1 \wedge 0 \le z \le h_{\mathrm{top}}\left( t \right) \right\}$ is the control region of the gas $g$ on the time interval $\left[ 0, \ \infty \right)$. Its boundary is the control surface $S$.
• $V : \R_{\ge 0} \rightarrow \R_{\ge 0}, \ t \mapsto \iiint_{D \left( t \right)} {dV}$ is the volume of the gas on the time interval $\left[ 0, \ \infty \right)$.

[Bulhwi Cha]

Let $h_{\mathrm{side}} : S_{\mathrm{side}} \left( 0 \right) \rightarrow \left( t : \R_{\ge 0} \right) \rightarrow \left[ 0, \ h_{\mathrm{top}}\left( t \right) \right]$ be the height of each point in the surface $S_{\mathrm{side}}$ on the time interval $\left[ 0, \ \infty \right)$. Assume $h_{\mathrm{side}} \left( \vec{\mathrm{r}} \right) : \left( t : \R_{\ge 0} \right) \rightarrow \left[ 0, \ h_{\mathrm{top}}\left( t \right) \right]$ has a continuous first derivative for all $\vec{\mathrm{r}} \in S_{\mathrm{side}} \left( 0 \right)$.

We now specify $\vec{\mathrm{s}}_S : S \left( 0 \right) \rightarrow \left( t : \R_{\ge 0} \right) \rightarrow S \left( t \right)$, the motion of the control surface $S$ on the time interval $\left[ 0, \ \infty \right)$. For all $t \in \R_{\ge 0}$ and $\left( x, \ y, \ z \right) \in S \left( 0 \right)$, the following holds:

$$\begin{split} \vec{\mathrm{s}}_S \left( \left( x, \ y, \ z \right), \ t \right) = \begin{dcases} \left( x, \ y, \ h_{\mathrm{top}} \left( t \right) \right) &\text{if } \left( x, \ y, \ z \right) \in S_{\mathrm{top}} \left( 0 \right) \\ \left( x, \ y, \ h_{\mathrm{side}} \left( \left( x, \ y, \ z \right), \ t \right) \right) &\text{if } \left( x, \ y, \ z \right) \in S_{\mathrm{side}} \left( 0 \right) \\ \left( x, \ y, \ z \right) &\text{if } \left( x, \ y, \ z \right) \in C_{\mathrm{bot}} \end{dcases} \end{split}$$

I'll specify later the pressure applied to the surface $S$ by the gas $g$ on the time interval $\left[ 0, \ \infty \right)$. Please tell me if you find something wrong.

boyles_law.jpg pressure_and_volume.jpg

[Scott Morrison]

Why are you talking about all these particular surfaces? There's no cylinder in Boyle's law!

[Bulhwi Cha]

Shreyas Srinivas said:

I don't understand. In what sense is pressure or volume unspecified from a math formalisation PoV?

But there's a closed system that contains an ideal gas in Boyle's law. I'm only giving an example of specifying the pressure and volume of a gas.

[Scott Morrison]

But then you're not giving Boyle's law --- you're giving an example.

[Bulhwi Cha]

I know, but that's the best thing I can do now. Hmm, maybe I should change the name of the image file.

[Shreyas Srinivas]

None of this is necessary for Boyle's law. For starters, as soon as you build a formalisation of gases as collections of particles, you are entering the realm of statistical mechanics. While the notion of ideal gas is often introduced as a collection of particles in a container that undergo random motion with perfectly elastic collisions everywhere, you don't need any of it to describe the theory of classical thermodynamics

[Shreyas Srinivas]

Secondly, as Scott points out you have a definition for a very specific container.

[Shreyas Srinivas]

As far as I recall my classical thermodynamics, the theory works perfectly well as long as you can assign values to the state variables and process variables, without ever looking under the hood.

[Bulhwi Cha]

Shreyas Srinivas said:

Secondly, as Scott points out you have a definition for a very specific container.

It's an example, not a definition. I can't come up with a definition at the moment.

[Shreyas Srinivas]

This is not to say that these state and process variables cannot be interpreted via statistical mechanics. Just that the macroscopic theory is perfectly fine without them.

[Shreyas Srinivas]

From the classical perspective, concepts like pressure, volume, and temperature are state variables that can be measured in some way. Nothing more.

[Bulhwi Cha]

I've never taken a class on statistical mechanics. Perhaps this was the reason I was unsatisfied with the classical explanation for gas laws.

[Bulhwi Cha]

Shreyas Srinivas said:

None of this is necessary for Boyle's law. For starters, as soon as you build a formalisation of gases as particles, you are entering the realm of statistical mechanics.

Statistical mechanics might be what I've been wanting to study and formalize.

[Bulhwi Cha]

(By the way, I also need to study undergraduate and graduate mathematics properly.)

[Shreyas Srinivas]

There is a small caveat with the ideal gas law: you don't entirely exclude the concept of particles. The n in PV = nRT typically refers to the number of moles of the gas in question. But beyond that none of the statistical definitions of P, V, or T are necessary for understanding laws about ideal gases.

[Bulhwi Cha]

Bulhwi Cha said:

I'll specify later the pressure applied to the surface $S$ by the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.

• $p : \mathrm{Fin} \ n \rightarrow \left( t : \R_{\ge 0} \right) \rightarrow S \left( t \right) \rightarrow \R$ is the pressure applied to the surface $S$ by the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.
• $p \left( i \right) : \left( t : \R_{\ge 0} \right) \rightarrow S \left( t \right) \rightarrow \R$ is the pressure applied to the surface $S$ by the $i$-th particle of the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.
• $p \left( i, \ t \right) = p \left( i \right) \left( t \right) : S \left( t \right) \rightarrow \R$ is the pressure applied to the surface $S \left( t \right)$ by the $i$-th particle of the gas $g$ at time $t$. It has continuous first partial derivatives.
• $p \left( i, \ t, \ \left( x, \ y, \ z \right) \right) = p \left( i \right) \left( t \right) \left( x, \ y, \ z \right) \in \R$ is the pressure applied to the point $\left( x, \ y, \ z \right)$ in the surface $S \left( t \right)$ by the $i$-th particle of the gas $g$ at time $t$.
• $p_{\mathrm{net}} : \left( t : \R_{\ge 0} \right) \rightarrow S \left( t \right) \rightarrow \R, \ t \mapsto \left( x, \ y, \ z \right) \mapsto \sum_{i \in \mathrm{Fin} \ n} {p \left( i, \ t, \ \left( x, \ y, \ z \right) \right)}$ is the net pressure applied to the surface $S$ by all particles of the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.

Edit: I changed $p_{\mathrm{top}}$ and $p_{\mathrm{top, \ net}}$ to $p$ and $p_{\mathrm{net}}$, respectively.

[Shreyas Srinivas]

Okay, another issue here : what does it mean for a particle to apply pressure on some surface. why the top surface (ideal gases exert the same pressure on all sides of their container).

[Shreyas Srinivas]

Pressure is a macroscopic quantity that is the cumulative effect of some fraction of the gas particles colliding against the walls of the container at any given time with some velocity distribution.

[Yury G. Kudryashov]

Again, there are two steps:

1. We say that the state of an ideal gas has parameters $(P, V, n, T)$ satisfying $PV=nRT$, where $R$ is a constant. Then we deduce Boyle's law, define isothermic/adiabatic processes, prove Carnot's theorem etc. For this part, "pressure", "volume", "work" etc can be just names.
2. We start with some model (e.g., a collection of particles interacting in some ways), then define pressure, volume, temperature. Then we prove that these quantities satisfy $PV=nRT$. This step is very nontrivial but it can be done separately. Also, there are a few open problems around...

Of course, docstrings should be improved to clearly differentiate between 2 steps.

[Shreyas Srinivas]

Yury G. Kudryashov said:

Again, there are two steps ...

Agreed, especially with point 2. In particular the following:

it can be done separately

When Charles or Boyle developed their laws, I am not sure statistical mechanics was even a thing yet.

[Bulhwi Cha]

Shreyas Srinivas said:

Okay, another issue here : what does it mean for a particle to apply pressure on some surface. why the top surface (ideal gases exert the same pressure on all sides of their container).

I wanted to write an equation about the normal force $\vec{\mathrm{F}}_{\mathrm{top, \ N}}$. The unit normal $\vec{\mathrm{n}} : \left( t : \R_{\ge 0} \right) \rightarrow S \left( t \right) \rightarrow \R^3$ to the surface $S$ satisfies the following:

$$\forall t \in \R_{\ge 0}, \ \forall \vec{\mathrm{r}} \in S_{\mathrm{top}} \left( t \right), \ \vec{\mathrm{n}} \left( t, \ \vec{\mathrm{r}} \right) = \left( 0, \ 0, \ 1 \right)$$

$\vec{\mathrm{F}}_{\mathrm{top, \ N}} : \R_{\ge 0} \rightarrow \R^3, \ t \mapsto \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) \vec{\mathrm{n}} \ dS$ is the normal force exerted on the surface $S_{\mathrm{top}}$ by the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.

For all $t \in \R_{\ge 0}$, the following holds:

$$\begin{split} \vec{\mathrm{F}}_{\mathrm{top, \ N}} \left( t \right) & = \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) \vec{\mathrm{n}} \ dS \\ & = \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) \left( 0, \ 0, \ 1 \right) dS \\ & = \left( \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) dS \right) \left( 0, \ 0, \ 1 \right) \end{split}$$

This equation and the definition of the net pressure $p_{\mathrm{net}}$ will help you understand what it means "for a particle to apply pressure on some surface."

[Bulhwi Cha]

@Scott Morrison said:

But then you're not giving Boyle's law --- you're giving an example.

Let $A_{\mathrm{top}} = \pi \cdot 1^2 = \pi$ be the area of the surface $S_\mathrm{top}$ and $P : \R_{\ge 0} \rightarrow \R, \ t \mapsto \lVert \vec{\mathrm{F}}_{\mathrm{top, \ N}} \left( t \right) \rVert / A_{\mathrm{top}}$ the (average) net pressure applied to the surface $S$ by all particles of the gas $g$ on the time interval $\left[ 0, \ \infty \right)$. The gas $g$ obeys Boyle's law on the time interval $\left[ 0, \ \infty \right)$ if and only if the following holds:

$$\exists k \in \R, \ \forall t \in \R_{\ge 0}, \ P \left( t \right) V \left( t \right) = k$$

[Shreyas Srinivas]

Bulhwi Cha said:

Shreyas Srinivas said:

Okay, another issue here : what does it mean for a particle to apply pressure on some surface. why the top surface (ideal gases exert the same pressure on all sides of their container).

Pressure is a macroscopic quantity that is the cumulative effect of some fraction of the gas particles colliding against the walls of the container at any given time with some velocity distribution.

I wanted to write an equation about the force $\vec{\mathrm{F}}_{\mathrm{top}}$. The unit normal $\vec{\mathrm{n}} : \left( t : \R_{\ge 0} \right) \rightarrow S_{\mathrm{top}} \left( t \right) \rightarrow \R^3$ to the surface $S_{\mathrm{top}}$ is simple:

$$\vec{\mathrm{n}} \left( t, \ \left( x, \ y, \ z \right) \right) = \left( 0, \ 0, \ 1 \right).$$

$\vec{\mathrm{F}}_{\mathrm{top}} : \R_{\ge 0} \rightarrow \R^3, \ t \mapsto \sum_{i \in \mathrm{Fin} \ n} {\iint_{S_{\mathrm{top}} \left( t \right)} p \left( i, \ t, \ \left( x, \ y, \ z \right) \right) \vec{\mathrm{n}} \ dS}$ is the force exerted on the surface $S_{\mathrm{top}}$ by the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.

For all $t \in \R_{\ge 0}$, the following holds:

$$\begin{split} \vec{\mathrm{F}}_{\mathrm{top}} \left( t \right) & = \sum_{i \in \mathrm{Fin} \ n} {\iint_{S_{\mathrm{top}} \left( t \right)} p_{\mathrm{top}} \left( i, \ t, \ \left( x, \ y, \ z \right) \right) \vec{\mathrm{n}} \ dS} \\ & = \sum_{i \in \mathrm{Fin} \ n} {\iint_{S_{\mathrm{top}} \left( t \right)} p_{\mathrm{top}} \left( i, \ t, \ \left( x, \ y, \ z \right) \right) \left( 0, \ 0, \ 1 \right) dS} \\ & = \left( \sum_{i \in \mathrm{Fin} \ n} {\iint_{S_{\mathrm{top}} \left( t \right)} p_{\mathrm{top}} \left( i, \ t, \ \left( x, \ y, \ z \right) \right) dS} \right) \left( 0, \ 0, \ 1 \right) \\ \end{split}$$

These definitions are not making sense anymore. In ideal gases, you assume that the particles make perfectly elastic instantaneous collisions, which causes an instantaneous change in the momentum. How are you getting a "force" out of this? How are you making the kind of continuity assumptions you would like to have for integrals. Secondly, you will almost certainly never get Boyle's law in that form, for the simple reason that at the microscopic level, the quantities you describe are all random variables. At best you might say that in expectation, the RV corresponding to pressure is constant under equilibrium conditions.

[Shreyas Srinivas]

Oh, and if you want to make predictions, then usually $n \sim 6.022 \times 10^{23}$.

[Shreyas Srinivas]

I guess what I really want to say is that statistical mechanics is hard enough without trying to reinvent everything from scratch.

[Bulhwi Cha]

Shreyas Srinivas said:

These definitions are not making sense anymore. In ideal gases, you assume that the particles make perfectly elastic instantaneous collisions, which causes an instantaneous change in the momentum. How are you getting a "force" out of this? How are you making the kind of continuity assumptions you would like to have for integrals.

Can you first show me formalized definitions of a gas, a particle, a force, pressure, and volume? Maybe then I can figure out where I got those wrong.

[Bulhwi Cha]

Shreyas Srinivas said:

I guess what I really want to say is that statistical mechanics is hard enough without trying to reinvent everything from scratch.

Well, I didn't plan to spend the entire day writing the above messages. Also, I didn't reinvent anything.

[Shreyas Srinivas]

Bulhwi Cha said:

Can you first show me formal-mathematical definitions of gas, pressure, volume, and force?

These are physical concepts. Unless you fix your model, you don't have mathematical definitions for these quantities. Fixing a model usually involves making some choices about what you "know" about the systems you analyse. For instance, choosing some elementary variables that you can measure using an instruments that follow some accepted standard of measurement, and relations between them that you deduce empirically. Using this model you make predictions for the motion of various point particles, and real bodies that might work like point particles upto suitable approximation. For another example, in your undergrad mechanics lesson, you might start with a model of point particles with masses, positions, frames of reference, and a concept of time (in the newtonian sense) and then deduce newton's laws empirically. Or you are Lagrange and decide that everything obeys the stationary action principle w.r.t some suitably defined lagrangian, which you have to choose carefully for each system.

In the case of the study of gases, the basic concepts might be some of the variables you describe like pressure, temperature and volume ,which can be measured by instruments like a barometer, thermometer, or just gradations on a transparent vessel. If you are a late 18th century natural philosopher, you might know about some earlier versions of these measurements by observation or visiting your nearest workshop. You then want to get precise in quantifying these measurements. Then you conduct experiments, and based on the results you posit some laws (Charles' law, Boyle's law etc). Or you are Ludwig Boltzmann in the late 19th century, and all this work is already available to you, along with the notion that gases are composed of elementary particles moving randomly and colliding with each other and the walls of the container (Daniel Bernoulli). You want to work out how the random behaviour of these particles gives rise to the measurements that we observe in the form of pressure and temperature. So you invent statistical mechanics that tries to quantify these properties in terms of the ensemble behaviour of these randomly moving particles and you get another set of definitions for pressure and temperature.

[Bulhwi Cha]

Shreyas Srinivas said:

How are you getting a "force" out of this?

Okay, then what do you mean by this?

[Shreyas Srinivas]

When you model an ideal gas (as Bernoulli did), you make certain idealised assumptions. See this link which is the wikipedia page for the Kinetic theory of gases.

[Shreyas Srinivas]

In particular, collisions are instantaneous and perfectly elastic, and it goes without saying, newtons' laws apply for the newtonian definition of "force" which equates it to the rate of change of momentum. Suppose a particle is headed towards the wall of a container, upto the instant of collision, and then, immediately after the instant of collision it is headed the other way, what force was imparted by the wall to the particle?

[Bulhwi Cha]

Shreyas Srinivas said:

Suppose a particle is headed towards the wall of a container, upto the instant of collision, and then, immediately after the instant of collision it is headed the other way, what force was imparted by the wall to the particle?

We don't know what the direction and magnitude of that force were. But you can divide that force vector into a normal force and a frictional force, right? We can represent the normal force exerted by the particle on the surface with which it collided as a surface integral of the pressure applied to that surface by the particle.

[Bulhwi Cha]

Shreyas Srinivas said:

How are you making the kind of continuity assumptions you would like to have for integrals.

By looking at my engineering mathematics textbook?

Secondly, you will almost certainly never get Boyle's law in that form,

Okay, I just adapted the statement from https://github.com/ATOMSLab/LeanChemicalTheories/blob/cec46762a297f678d171e79a45899f139b437550/src/thermodynamics/basic.lean#L44C1-L44C109.

[Shreyas Srinivas]

That statement makes no reference to time instants

[Bulhwi Cha]

I said I adapted it from LeanChemicalTheories.

[Bulhwi Cha]

I modified a message: I added the word "normal" to the force $\vec{\mathrm{F}}_{\mathrm{top}}$ and changed its notation to $\vec{\mathrm{F}}_{\mathrm{top, \ N}}$.

Edited message

Bulhwi Cha said:

Shreyas Srinivas said:

Okay, another issue here : what does it mean for a particle to apply pressure on some surface. why the top surface (ideal gases exert the same pressure on all sides of their container).

Pressure is a macroscopic quantity that is the cumulative effect of some fraction of the gas particles colliding against the walls of the container at any given time with some velocity distribution.

I wanted to write an equation about the normal force $\vec{\mathrm{F}}_{\mathrm{top, \ N}}$. The unit normal $\vec{\mathrm{n}} : \left( t : \R_{\ge 0} \right) \rightarrow S \left( t \right) \rightarrow \R^3$ to the surface $S$ satisfies the following:

$$\forall t \in \R_{\ge 0}, \ \forall \vec{\mathrm{r}} \in S_{\mathrm{top}} \left( t \right), \ \vec{\mathrm{n}} \left( t, \ \vec{\mathrm{r}} \right) = \left( 0, \ 0, \ 1 \right)$$

$\vec{\mathrm{F}}_{\mathrm{top, \ N}} : \R_{\ge 0} \rightarrow \R^3, \ t \mapsto \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) \vec{\mathrm{n}} \ dS$ is the normal force exerted on the surface $S_{\mathrm{top}}$ by the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.

For all $t \in \R_{\ge 0}$, the following holds:

$$\begin{split} \vec{\mathrm{F}}_{\mathrm{top, \ N}} \left( t \right) & = \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) \vec{\mathrm{n}} \ dS \\ & = \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) \left( 0, \ 0, \ 1 \right) dS \\ & = \left( \iint_{S_{\mathrm{top}} \left( t \right)} p_\mathrm{net} \left( t, \ \left( x, \ y, \ z \right) \right) dS \right) \left( 0, \ 0, \ 1 \right) \end{split}$$

[Bolton Bailey]

Shreyas Srinivas said:

When you model an ideal gas (as Bernoulli did), you make certain idealised assumptions. See this link which is the wikipedia page for the Kinetic theory of gases.

I wonder what assumptions derived from the kinetic theory are needed. Clearly we need something like isotropy, otherwise in a rectangular box with one direction longer than the other, the orientation of the particle's motion affects the pressure. Do we need an assumption about the distribution of the particles speeds as well, or is it ok to assume that particles have arbitrary speeds?

[Bolton Bailey]

Am I right in saying there will have to be some application of the divergence theorem? We have this in mathlib, right?

[Bulhwi Cha]

We have Mathlib.MeasureTheory.Integral.DivergenceTheorem.

[Bulhwi Cha]

@Bolton Bailey I need surface integrals of scalar-valued functions, surface integrals of vector fields, and triple integrals.

[Bulhwi Cha]

Bulhwi Cha said:

• $p_{\mathrm{top, \ net}} : \R_{\ge 0} \rightarrow \R, \ t \mapsto \sum_{i \in \mathrm{Fin} \ n} {\iint_{S_{\mathrm{top}} \left( t \right)} p \left( i, \ t, \ \left( x, \ y, \ z \right) \right) dS}$ is the net pressure applied to the surface $S_{\mathrm{top}}$ by the gas $g$ on the time interval $\left[ 0, \ \infty \right)$.

I removed $p_{\mathrm{top, \ net}}$. It's weird and we don't need it.

[Tyler Josephson ⚛️]

Yury G. Kudryashov said:

Of course, docstrings should be improved to clearly differentiate between 2 steps.

Indeed, we can clean up the docstring that to clarifying that this is a proof that an ideal gas obeys Boyle’s Law. It shouldn’t be seen as a derivation of either the ideal gas law or Boyle’s Law.

[Tyler Josephson ⚛️]

Scott Morrison said:

I remain pretty unclear what formalization of physics and/or chemistry is even meant to mean. Formalization of mathematical physics I think I do understand: e.g. you define symplectic manifolds "properly", and then add a paragraph to the doc-string that begins "Hamiltonian mechanics describes physical systems via a symplectic manifold ..."

From my perspective, it’s clarifying to recognize the gap between physical reality and the models we use to describe reality. For now, I only hope to be formalizing those models.

After all, what if I asked the question, “Is Boyle’s Law true, in reality?” The answer is quickly “no,” at least not all the time. It might be true of ideal gases, but non-ideal gases exist that violate Boyle’s Law. In fact, no gas is actually ideal, if you were to measure its properties with sufficient precision. The ideal gas law is a useful model that describes many gases quite well, and it’s an insightful model that helps us build many other useful models. Indeed, most practicing scientists and engineers care deeply about whether a theory is accurate - I love the BET theory of adsorption and we formalized it’s derivation in Lean, but a colleague asked me “why?” because “it’s not true” (meaning it assumes things that most physical systems don’t follow). It’s an elegant theory, but how closely do physical systems follow it?

I also make a distinction between formalizing and axiomatizing in science (I came up with this distinction on my own - if someone else in literature has done this before, there might be different language out there that I should probably use). Axiomatization is essentially Hilbert’s 6th Problem - how do we define the minimal set of axioms that can describe all of physical reality, and then prove it? Formalization sets aside the goal of defining the minimal set of axioms, and instead aims to precisely define the models scientists and engineers use and show how they logically arise from certain assumptions, as well as precisely demonstrate the relationships among different models / derivations.

In the latter view, I don’t need to start with molecules or even more fundamental microstates. I can start with a chemical reactor that’s defined as X and then prove that X has properties Y and Z. Or I might start with a cell or an ecosystem or a planetary system that’s defined as X and then prove that it has properties Y and Z. If one of these X’s leverages ideas from elsewhere in science (maybe my reactor has a mixture of ideal gases), then better to show those connections, but we don’t need to have the foundation fully set before we start writing proofs.

[Bulhwi Cha]

Perhaps we have somewhat different goals. I want to axiomatize physics and then formalize it. No luck so far.

[Tyler Josephson ⚛️]

Definitely need to read the literature on this then. Search for Hilbert’s 6th Problem and you’ll be able to find how others have made progress on this (usually without proof assistants though)

[Bulhwi Cha]

@Tyler Josephson ⚛️ It'll take quite a long time. I want to read the literature and relevant textbooks, but I need to learn programming first to develop a video game.

[Max Bobbin]

Bulhwi Cha said:

Perhaps we have somewhat different goals. I want to axiomatize physics and then formalize it. No luck so far.

Just had time to read through all of this and add some thoughts:

On Boyles Law As was pointed out, we have a different "formalization" which is "more correct." here. I put this in air quotes because I can think of other ways to go about defining thermodynamics to arrive at Boyle's Law. However, the base question becomes how do we go about defining things? I answer my thoughts on this later.

On what formalization of science looks like
I think, regardless of our current goals now, a full team working on SciLib will be, at its heart, working towards Hilbert's Sixth problem. However, I don't think that solving Hilbert's Sixth problem will be done in a linear fashion. By this I mean, it will be impossible to start SciLib by guessing a set of Axioms and attempting to build science off of it. Instead, I think the better idea is to start at the end and work backward. This entails picking an aspect of the natural sciences, defining it in its most "useless" form, and then picking parts of it to define.

For example, the original Boyle's Law was, as you said, nothing impressive. It doesn't capture anything about science and was merely a proof of the relation between equations. However, by starting with such a simple theorem, we can work backward to a more general definition. We do this by picking a part of it and asking how to define it. We can pick pressure and ask how we should define pressure instead of just postulating it as a real number. Thermodynamics is an interesting example because we instantly get to a point where we have to figure out how to define natural phenomena. The new formalization of thermodynamics defines a structure called thermo_system which is defined as:

structure thermo_system (α) [nontrivial α]:=

(pressure : α → ℝ)
(volume : α → ℝ)
(temperature : α → ℝ)
(substance_amount : α → ℝ)
(internal_energy : α → ℝ)

The idea here is to define a system as a set of parameters that are functions from the states of the system to the real numbers. This works when we want to capture Boyle's Law, but it doesn't seem to be good enough for other applications. For one, this definition of pressure doesn't make reference to force or a surface the force acts on. Further, this definition seems hard to work with if we wanted to implement it for other applications, like the Navier-Stokes equation. To come upon a useful definition of pressure, it helps to try to define pressure for a couple different theorems in ways that work for each theorem and then try to generalize all those definitions into one definition.

[Max Bobbin]

Thermodynamics is a hard example to see this full plan because we instantly run into the headache of defining pressure, volume, temperature, etc. in a general way. Take, as an example, defining a CSTR with a first-order reaction. We could start with this:

theorem CSTR
--all the variables as real numbers
(hrec: r = k*C_A)
(mass_balance: accum = in-out+gen)
(hgen: gen = V*r)
(Haccum: accum = 0)
:
goal :=

the goal here isn't important. From this, we can pick a part of it and try to generalize it. My first thought would be the reaction rate. We could start by generalizing the rate constant as something like:

def rate_constant (A E R : ℝ) :=  λ T : ℝ, A*exp(-E*R/T)

Our next thought could be generalizing this definition further, by recognizing that there are different functions to model the temperature dependence of the rate constant. So, we want the rate constant to be defined as some function that takes in a temperature and outputs a real number. Instead, maybe the rate constant should be incorporated in the definition of the reaction rate:

def reaction_rate {n : N} (k : ℝ→ ℝ) (f : (fin n → ℝ) → ℝ) := λ (T : ℝ) (x : fin n → ℝ), k T * f x

[Tomas Skrivan]

Thermodynamical system is usually determined by a function for internal energy which is as a function of entropy, volume and substance amount(s). Entropy can be converted to temperature and volume can be transformed to pressure by Legendre transform. Therefore specifying pressure and volume seems to me redundant.

I would define thermodynamical system as:

structure thermo_system (α) :=
  (volume : α → ℝ)
  (entropy : α → ℝ)
  (substance_amount : α → ℝ)
  (internal_energy : α → ℝ)
  (entVolSubMap : ℝ×ℝ×ℝ → α)
  (consistent : LeftInverse entVolSubMap (fun a => (entropy a, volume a, substance_amount a))
                ∧
                RightInverse entVolSubMap (fun a => (entropy a, volume a, substance_amount a)))

With this definition you can define pressure as:

def pressure (s : thermo_system α) (a : α) : ℝ :=
  fun a => deriv (dV : ℝ) =>
    s.internal_energy entVolSubMap (s.entropy a, s.volume a + dV, s.substance_amount a)

For example, this can be taken as a starting definition to formalize all the Maxwell's relations. You probably need some convexity and smoothness condition on internal_energy though.

[Eric Wieser]

What do you envisage α being here?

[Eric Wieser]

Is what you have equivalent to the following?

structure thermo_state :=
  (volume : ℝ)
  (entropy : ℝ)
  (substance_amount : ℝ)

structure thermo_system :=
  (internal_energy : thermo_state → ℝ)

def pressure (s : thermo_system) (a : thermo_state) : ℝ :=
  deriv $ fun (dV : ℝ) => s.internal_energy {a with volume := a.volume + dV}

[Tomas Skrivan]

I'm assuming that you parameterize it over a general type α for additional flexibility.

Maybe the definition should be a little bit more complicated to render this parametrization useful. The type α is a general state which admits decomposition α ≅ ℝ×ℝ×β which is entropy, volume and anything extra like amounts of substances. You want to allow for arbitrary number of different substances.

[Tomas Skrivan]

But you are right that it might be unnecessarily complicated. It might be better to define it as:

structure thermo_state (β : Type) :=
  (volume : ℝ)
  (entropy : ℝ)
  (extra_state : β)

structure thermo_system (β : Type) :=
  (internal_energy : thermo_state β → ℝ)

[Notification Bot]

6 messages were moved from this topic to #Natural sciences > Bernoulli's Principle by Tyler Josephson ⚛️.

[Tyler Josephson ⚛️]

I initially thought internal energy would be as relevant as V and S, but I’ve been looking into some informal efforts to formalize thermodynamics, and finding that perhaps they would be stratified like @Tomas Skrivan is suggesting. But if we really want to dig deep into the foundations (rather than build engineering-relevant proofs right away), I think this might be a good place to start: https://arxiv.org/abs/cond-mat/9708200. The literature review alone is perspective-shaping - there are many (dozens) of formalization attempts with nuanced differences and limitations.

[Tyler Josephson ⚛️]

Section VII summarizes the 15 axioms required.

[Bulhwi Cha]

Bulhwi Cha said:

Quote

import Mathlib.Data.Real.Basic

lemma Boyle
    -- Variables
    (P1 P2 V1 V2 T1 T2 n1 n2 R : ℝ)
    -- Assumptions
    (a1 : P1 * V1 = n1 * R * T1)
    (a2 : P2 * V2 = n2 * R * T2)
    (a3 : T1 = T2)
    (a4 : n1 = n2) :
    -- Conjecture
    P1 * V1 = P2 * V2 := by
  rw [a3] at a1
  rw [a4] at a1
  exact (rfl.congr (Eq.symm a2)).mp a1

lemma just_a_random_example (x₁ x₂ y₁ y₂ z₁ z₂ w₁ w₂ k : ℝ)
    (h₁ : x₁ * y₁ = w₁ * k * z₁) (h₂ : x₂ * y₂ = w₂ * k * z₂)
    (h₃ : z₁ = z₂) (h₄ : w₁ = w₂) : x₁ * y₁ = x₂ * y₂ := by
  rw [h₁, h₂, h₃, h₄]

theorem Boyle_is_just_a_random_example : Boyle = just_a_random_example := rfl

I think the lemma Boyle should be removed from LeanChemicalTheories. It's not a correct formalization of Boyle's law; it's merely an example of using rewriting. We need to formally define the pressure and the volume of a confined ideal gas. Then we should use those definitions to state Boyle's law correctly in Lean. But currently, I have no idea how to define them.

Perhaps the following code will further clarify that the lemma Boyle is equal to some statement that makes sense but doesn't describe the relationship between pressure and volume of a confined gas. In the lemma this_isn't_Boyle, the real variable R_mul_inv represents the reciprocal of R, the gas constant.

import Mathlib.Data.Real.Basic

lemma Boyle
    -- Variables
    (P1 P2 V1 V2 T1 T2 n1 n2 R : ℝ)
    -- Assumptions
    (a1 : P1 * V1 = n1 * R * T1)
    (a2 : P2 * V2 = n2 * R * T2)
    (a3 : T1 = T2)
    (a4 : n1 = n2) :
    -- Conjecture
    P1 * V1 = P2 * V2 := by
  rw [a3] at a1
  rw [a4] at a1
  exact (rfl.congr (Eq.symm a2)).mp a1

lemma this_isn't_Boyle
    -- Variables
    (n1 n2 T1 T2 V1 V2 P1 P2 R_mul_inv : ℝ)
    -- Assumptions
    (a1 : n1 * T1 = P1 * R_mul_inv * V1)
    (a2 : n2 * T2 = P2 * R_mul_inv * V2)
    (a3 : V1 = V2)
    (a4 : P1 = P2) :
    -- Conjecture
    n1 * T1 = n2 * T2 := by
  rw [a1, a2, a3, a4]

theorem Boyle_eq_this_isn't_Boyle : Boyle = this_isn't_Boyle := rfl

[Alex Meiburg]

I just came across this topic. There is definitely a "standard" and precise formalization of these concepts, at least that's the impression I have from my background as a condensed matter theorist! :)

Something along the lines of what Tomas Skirvan or Eric Wieser described, but that's not quite the most standard way to do it. It's really best to start with the microcanonical ensemble, n/V/E. Then the other parameterizations (such as n/V/T) come from Legendre transforms.

All that you really as an "input" to the problem is a microstate Hamiltonian, possibly parameterized by some extrinsic factors (here, those would be volume V and particle number n). Then everything can be derived from the Hamiltonian. The really "classic" way to do this is to take the amount of phase space under a given energy limit as the (exponential of) the entropy, and the move on from there, but the one I see pretty much always these days -- and the one that works better with the quantum case -- is to use a partition function as the fundamental quantity.

[Alex Meiburg]

This is what I sketched up this morning. This lines up with the standard "proof" of the ideal gas law that I've seen in several textbooks.

import Mathlib

noncomputable section

section ThermodynamicEnsemble

/-- The Hamiltonian for a microcanonical ensemble, parameterized by any extrinsic parameters of data D. (Since it's an arbitrary type, 'T' would be nice, but we use 'D' for data to avoid confusion with temperature.) We define Hamiltonians as an energy function on a real manifold, whose dimension n possibly depends on the data D.
  * Energy is a WithTop ℝ, ⊤ is used to mean "excluded as a possibility in phase space".
  * This formalization does exclude the possibility of discrete degrees of freedom; it is not _completely_ general. A better formalization would have an arbitrary measurable space.
-/
structure MicroHamiltonian (D : Type) :=
  dim : D → ℕ
  H : (d : D) → (Fin (dim d) → ℝ) → WithTop ℝ

variable {D : Type} (H : MicroHamiltonian D) (d : D)

/-- The partition function corresponding to a given MicroHamiltonian. This is a function taking a thermodynamic β, not a temperature.
It also depends on the data D defining the system extrinsincs.

 * Ideally this would be an NNReal, but ∫ (NNReal) doesn't work right now, so it would just be a separate proof anyway
-/
def PartitionZ (β : ℝ) : ℝ :=
  ∫ (config : Fin (H.dim d) → ℝ),
    let E := H.H d config
    if h : E = ⊤ then 0 else Real.exp (-β * (E.untop h))

/-- The partition function as a function of temperature T instead of β. -/
def PartitionZT (T : ℝ) : ℝ :=
  PartitionZ H d (1/T)

/-- The Internal Energy, U or E, defined as -∂(ln Z)/∂β. Parameterized here with β. -/
def InternalU (β : ℝ) : ℝ :=
  -deriv (fun β' ↦ (PartitionZ H d β').log) β

/-- The Helmholtz Free Energy, -T * ln Z. Also denoted F. Parameterized here with temperature T, not β. -/
def HelmholtzA (T : ℝ) : ℝ :=
  -T * (PartitionZT H d T).log

/-- The entropy, defined as the -∂A/∂T. Function of T. -/
def EntropyS (T : ℝ) : ℝ :=
  -deriv (HelmholtzA H d) T

/-- The entropy, defined as ln Z + β*U. Function of β. -/
def EntropySβ (β : ℝ) : ℝ :=
  (PartitionZ H d β).log + β * InternalU H d β

/-- The two definitions of entropy, in terms of T or β, are equivalent. -/
theorem entropy_A_eq_entropy_Z (T β : ℝ) (h : T * β = 1) : EntropyS H d T = EntropySβ H d β := by
  sorry --this can be proven now

end ThermodynamicEnsemble

--! Specializing to a system of particles in space

section NumberVolumeEnsemble

/-- The standard microcanonical ensemble Hamiltonian, where the data is the particle number N and the volume V. -/
abbrev NVEHamiltonian : Type := MicroHamiltonian (ℕ × ℝ)

variable (H : NVEHamiltonian) (d : ℕ × ℝ)

/-- Pressure, as a function of T. Defined as the conjugate variable to volume. -/
def Pressure (T : ℝ) : ℝ :=
  let (n, V) := d;
  -deriv (fun V' ↦ HelmholtzA H (n, V') T) V

/-- Pressure is equivalently T * (∂S/∂V), for any Hamiltonian. -/
theorem P_eq_T_dS_dV (T : ℝ) :
    let (n, V) := d;
    Pressure H d T = T * deriv (fun V' ↦ EntropyS H (n, V') T) V := by
  sorry

end NumberVolumeEnsemble

--! Specializing to an ideal gas of distinguishable particles.
section IdealGas

/-- The Hamiltonian for an ideal gas: particles live in a cube of volume V^(1/3), and each contributes an energy p^2/2.
The per-particle mass is normalized to 1. -/
def IdealGas : NVEHamiltonian where
  --The dimension of the manifold is 6 times the number of particles: three for position, three for momentum.
  dim d := 6 * d.fst
  --The energy is ∞ if any positions are outside the cube, otherwise it's the sum of the momenta squared over 2.
  H := fun (n, V) config ↦
    let R := V^(1/3) / 2
    if ∀ (i : Fin n) (ax : Fin 3), |config ⟨6*i + ax, by linarith [i.2, ax.2]⟩| <= R then
      ∑ (i : Fin n) (ax : Fin 3), config ⟨6*i + ax + 3, by linarith [i.2, ax.2]⟩^2 / (2 : ℝ)
    else
      ⊤

/-- The ideal gas law: PV = nRT. In our unitsless system, R = (3/2) ... (I think?)-/
theorem IdealGasLaw (n : ℕ) (V T : ℝ) :
    let P := Pressure IdealGas (n,V) T;
    let R := 3/2; --need to double check this value
    P * V = n * R * T := by
  sorry --this can now be proved

-- Now proving Boyle's Law ("for an ideal gas with a fixed particle number, P and V are inversely proportional")
-- is a fast consequence of the ideal gas law.

end IdealGas

[Alex Meiburg]

I have a couple comments there for how the definitions could be slightly improved. But this illustrates pretty well, I think, how thermodynamics can be formalized with a pretty high level of rigor. And then there are natural adaptions -- within this framework -- to, say, a photon gas, which would typically be the next thing to study.

(I'm also pretty sure that a couple of those theorems would require some additional hypotheses, like T != 0 or V > 0, to actually be correct.)

[Alex Meiburg]

One thing that's not ideal is that IdealGas still takes a cube-shaped control volume as part of its definition. The best way I could think of to handle this would be like this:

• First, define a predicate IsThermodynamic indicating that a quantity depends on the Hamiltonian only through its partition function. So Z, E, S etc would all be thermodynamic quantities. A quantity like "average position" is not thermodynamic.
• Generalize IdealGas to any reasonably nice shaped region R of space with volume V. Then, show that any two IdealGas R produce the exact same PartitionZ, so they will agree on all IsThermodynamic quantities.
• If we wanted to get reaaaallly fancy, we could define an IdealGas as the quotient of these types by the "equal volume" relation. Then we can use Quot.lift to apply PartitionZ to the quotient type, and all other quantities are manifestly shape-invariant.

But really, this is also kind of why ideal gases are strange sometimes. Many interesting systems are not shape invariant. As soon as you have any particle interaction at all, the shape does matter. So I think in terms of really "getting thermodynamics formalized" this is a much lower priority than it might look, even if its seems unasthetic.

[Kim Morrison]

It would be great if you could extract out of this pithy descriptions of what you'd like changed in the measure theory library to make things smoother --- what exactly is wrong with NNReal here? Could the WithTop interact more smoothly with the integrals (i.e. without an if)? What is required to use an arbitrary measureable space for the configuration space?

[Alex Meiburg]

The thing that would most need changing is me: I learned me some measure theory in undergrad, but haven't really touched it since then, and Lean's API to it looks scary and unfamiliar. But I can understand an expression like ∫ x : ℝ × ℝ, f x and work with that! :) I think what I want is something _vaguely_ like,

structure MicroHamiltonian (D : Type) :=
  X : D → MeasurableSpace
  H : (d : D) → (X d) → ℝ

def PartitionZ (β : ℝ) : ℝ :=
  ∫ (config : X d), Real.exp (-β * H.H d config h)

... but I'm 99% sure that's not using "MeasurableSpace" correctly, and I don't understand it well enough to fix it. (If someone would show me the right thing, that would be great.)

Then IdealGas would have something like,

X d :=
   let (n,V) := d;
   (Set.Icc 0 V^(1/3))^(3*n) × ℝ^(3*n)

where that ^(3*n)s means I want the 6n dimensional space that's [0,V^(1/3)] on the first 3n coordinates and ℝ on the other 3n coordinates. I think this could be expressed as (Fin (3*n) → Set.Icc 0 V^(1/3)) × (Fin (3*n) → ℝ) but I don't know if there's something cleaner. With this, I wouldn't need any of the WithTop nonsense. :)

[Alex Meiburg]

The ∫ (NNReal) comment was referring to the fact that you can't take an integral of NNReals and get an NNReal, because integrals are defined on NormedAddCommGroup, and NNReal is just a semigroup, not a group. In my particular case, I think I could get it by wrapping the whole integral (as a real) into an NNReal, with MeasureTheory.integral_exp_pos as the proof part.

[Eric Wieser]

@Yury G. Kudryashov and I have briefly discussed how to generalized NormedAddCommGroup to additive monoids, but it's a lot of work with previously no motivation

[Alex Meiburg]

It's not a big deal if it's absent here, since it's really just the one application (the partition function is nonnegative), and it's fine just having that unbundled I think

[Eric Wieser]

Probably a natural stepping stone is to unbundle the additive group structure and write [AddCommGroup X] [NormedSpace' X] or something

[Alex Meiburg]

Actually: really what's probably more important this application, actually, is that PartitionZ is strictly _positive_ (which is true as long as the measure of the whole configuration space is nonzero). Because if Z = 0, then the log is undefined (well, zero) and nondifferentiable and everything falls apart.

Probably MicroHamiltonian should have that as a requirement, that the configuration space is never measure zero. (And that H is integrable, I guess?)

[Eric Wieser]

If you can tolerate ENNReal, perhaps you want docs#MeasureTheory.lintegral ?

[Alex Meiburg]

I "don't really care" in the sense that everything I want to do will be a continuous (in fact, analytic), integrable, positive function on a (measurable subset of) R^n, so I know the values will be finite and generally well-behaved. Which would you recommend?

[Tyler Josephson ⚛️]

We’ve generally been content with avoiding NNReal and just using Real with an additional non-negativity or positivity constraint, since so many more theorems are available for Reals. But many things naturally lend themselves to have type NNReal (T, V, and N would all be such cases).

[Tyler Josephson ⚛️]

And it does make sense to prevent things like subtracting “number of molecules” and getting a negative number.

[Alex Meiburg]

I've got 99% of the proof of the ideal gas law, starting from the Hamiltonian $\sum_i \frac{||p_i||^2}{2}$ and the constraints that $|x| \le \frac{V^{1/3}}{2}$. I'm pretty happy about this. It's really "rigorous" physics, I think!

https://github.com/Timeroot/Lean-QuantumInfo/blob/main/StatMech/IdealGas.lean

There are two sorries left. One is a stupid integrability condition to use Fubini's theorem - I say stupid because I later go on to prove the value of the double integral, I'm sure the same ideas still apply; but I think I can fix it by converting to lintegral, using Tonelli's theorem (which only requires measurability, which is easy), and then back to integral. I'll take care of that one soon

The other sorry is some measure theory thing that I can't understand, and would like help with if possible. It amounts to proving measureSpaceOfInnerProductSpace = MeasureSpace.pi as the stated goal, of course with many implicit instances hidden in there. Here it's really that the left side is the measure on PiLp 2 (S -> Real) for a fintype S, as an inner product space, while the right side is just the pi mesaure on S -> Real. Any tips (or even a proof? Feel free to clone my repo and try!) would be very appreciated! If someone tells me that this is nowhere enough to go off of, I can try to make a mwe in the future

[Eric Wieser]

It sounds like you've committed defeq abuse if you're equating those measures on different types

[Eric Wieser]

There ought to be an equiv in the equality to cast between the types

[Alex Meiburg]

Great, knocked those out. No sorries! :tada:

I believe this formalization properly captures the notion of ideal gases, starting from their microscopic nature. That said, there are a couple of points that I recognize could be better:

• The IdealGas is currently stated as living in a cube of volume V centered at the origin. As discussed earlier in this thread (well, over a year ago), the statistical behavior of an ideal gas should be independent of the shape of the container. While this is a slight inelegance, I don't see it as a big problem: for _any_ gas with inter-particle interactions, the shape of the box matters. (The relevant theorem would be proving something like, if the box is "much larger" compared to the particle interaction range in "all directions", then the partition function approaches some limiting value that is independent of the shape of the box. But even finding what "much larger" should mean is very delicate.)
• The partition function, as stated, actually describes an ideal gas of N _distinguishable_ particles. Typically it is stated in terms of _indistinguishable_ particles, which adds a factor of $1/N!$ to the partition function Z, and an additive constant $-log(N!)$ to the entropy S. But this doesn't affect any relations involving P, V, n, T, U, F, heat capacity, and so on. This mostly matters where you want to talk about varying the particle number n and the chemical potential μ. That brings a host of other questions though (namely, that n is discrete but it is typically treated as differentiable anyway.)
• There are no units :smile: and the particles have a mass of "1". This means the ideal gas constant, R, is just "1" as well.

[Alex Meiburg]

theorem statement (with necessary defs):

/-- The Hamiltonian for a microcanonical ensemble, parameterized by any extrinsic parameters of data D.
  Since it's an arbitrary type, 'T' would be nice, but we use 'D' for data to avoid confusion with temperature.
  We define Hamiltonians as an energy function on a real manifold, whose dimension n possibly depends on the data D.
  Energy is a WithTop ℝ, ⊤ is used to mean "excluded as a possibility in phase space".
  This formalization does exclude the possibility of discrete degrees of freedom; it is not _completely_ general.
  A better formalization could have an arbitrary measurable space.
-/
structure MicroHamiltonian (D : Type) where
  --For extrinsic parameters D (e.g. the number of particles of different chemical species, the shape of the box),
  --how many continuous degrees of freedom are there?
  dim : D → Type
  --We require that the number of degrees of freedom is finite.
  [dim_fin : ∀ d, Fintype (dim d)]
  --Given the configuration, what is its energy?
  H : {d : D} → (dim d → ℝ) → WithTop ℝ

abbrev NVEHamiltonian := MicroHamiltonian (ℕ × ℝ)

def PartitionZ (β : ℝ) : ℝ :=
  ∫ (config : H.dim d → ℝ),
    let E := H.H config
    if h : E = ⊤ then 0 else Real.exp (-β * (E.untop h))

/-- The partition function as a function of temperature T instead of β. -/
def PartitionZT (T : ℝ) : ℝ :=
  PartitionZ H d (1/T)

/-- The Helmholtz Free Energy, -T * ln Z. Also denoted F. Parameterized here with temperature T, not β. -/
def HelmholtzA (T : ℝ) : ℝ :=
  -T * (PartitionZT H d T).log

/-- Pressure, as a function of T. Defined as the conjugate variable to volume. -/
def Pressure (T : ℝ) : ℝ :=
  let (n, V) := d;
  -deriv (fun V' ↦ HelmholtzA H (n, V') T) V

/-- The Hamiltonian for an ideal gas: particles live in a cube of volume V^(1/3), and each contributes an energy p^2/2.
The per-particle mass is normalized to 1. -/
def IdealGas : NVEHamiltonian where
  --The dimension of the manifold is 6 times the number of particles: three for position, three for momentum.
  dim := fun (n,_) ↦ Fin n × (Fin 3 ⊕ Fin 3)
  --The energy is ∞ if any positions are outside the cube, otherwise it's the sum of the momenta squared over 2.
  H := fun {d} config ↦
    let (n,V) := d
    let R := V^(1/3:ℝ) / 2 --half-sidelength of a cubical box
    if ∀ (i : Fin n) (ax : Fin 3), |config (i,.inl ax)| <= R then
      ∑ (i : Fin n) (ax : Fin 3), config (i,.inr ax)^2 / (2 : ℝ)
    else
      ⊤

/-- The ideal gas law: PV = nRT. In our unitsless system, R = 1.-/
theorem IdealGasLaw (hV : 0 < V) (hT : 0 < T) :
    let P := IdealGas.Pressure (n,V) T;
    let R := 1;
    P * V = n * R * T := by <snip>

[Kim Morrison]

Can one replace 3 with any 0 < k in the proof?

[Alex Meiburg]

Yes, that would be easy, there's nothing here using three dimensions in particular. That's a good idea

[Kim Morrison]

Do you think it would be possible to strengthen this to some form of iff? e.g. characterising the exponent 2 in the kinetic energy? (Just thinking about ways to demonstrate that "we're really proving something".)

[Kim Morrison]

(but first --- this is cool!)

[Alex Meiburg]

Hmm. Changing the exponent from 2 is actually very difficult - in the sense of, difficult to study by physics standards too, not just formalized math. The integrals stop being Gaussians and don't have a closed form any more. The one other tractable case is an exponent of 1, which is the photon gas, and I had been thinking that would be a reasonable next step to try.

If your gut feeling is that the final statement would look stronger if you could compare it with a different model, what I think would be a really interesting result would to be work out a Bose gas. In principle it models the ideal gas but when the particles are Bosons (and inherently, it is quantum, although one doesn't really need any quantum theory to start studying it). It has a correction to the ideal gas law at low temperatures, and in particular, it has a phase transition which would be a wonderfully cool thing to prove. That would be a considerably larger project, but not outrageous.

[Alex Meiburg]

The most physically 'relevant' model to try next would be something that takes particle interactions into account. But even the simplest models of that (e.g. van der Waals) have big issues where they're only approximately accurate, they have "stability" issues, etc

[Adomas Baliuka]

I noticed that Mathlib does not have the Legendre transform. Do mathematicians know about it or use it enough that it would be justifiably included?

If so, which version would one want? Wikipedia seems to have two ways of doing it. One could have some some generalizations/specializations (maybe one would actually want to specify the domain and explicitly assume convexity, etc.) of def LegendreT (f : ℝ → ℝ) : ℝ → ℝ := fun p ↦ ⨆ x, p * x - f x (top of Wikipedia article). Alternatively, one could use the symplectic geometry way (bottom of Wikipedia article).

I guess most uses in physics are actually more properly covered by the symplectic geometry version? Maybe there's some more uses I'm not aware of.