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.