Dimensional Analysis Revisited

Stream: maths

[Max Bobbin]

Hello,
I posted a month of so back about a first attempt at formalizing dimensional analysis with an end goal of automating the process of showing dimensional homogeneity. After applying the feedback I recieved, I am happy to show the second iteration of dimensional analysis. The full set of files can be found here. Instead of using inductive I switched to structure to index the exponent and swapped to a general n-tuple.

structure dimension :=
mk ::
(exponent : Π n : ℕ, fin n → rat)

I believe using structure is the correct approach over class, but I wanted to make sure. With this, I could easily define a dimensionless number as:

def dimensionless := dimension.mk (λ (n : ℕ) (x : fin n), (0 : ℚ))

but I was having trouble with defining dimensions. For instance, I want to define time as being a tuple of 1 followed by zeros. Ideally, I would like the number of zeros to be as many as needed. So if I'm talking about the seven common dimensions, its just 1 and six 0s, but if I have more dimensions, it's more zeros to fill the gap. I was looking for any suggestions on how to achieve this.

I also formalized the basis of buckingham pi as:

noncomputable
def number_of_dimensionless_parameters {m n : ℕ} (M : matrix (fin m) (fin n) ℚ): ℕ := n - matrix.rank M

Once I can define the dimensions, I can create an example of using them with the buckingham pi theorem. I was trying to do a quick example to check if it works

example : number_of_dimensionless_parameters !![(1 : ℚ), 0, 1; 0, 1, -1] = 1 :=

but I wasn't entirely sure how to compute the rank of a matrix. I was worried that because matrix.rank has the noncomputable tag, it would be impossible to show, for this example, the rank is 2.

A final note, I was trying to use the option class for addition, but may have done it wrong, because its not of the correct function form when trying to do instances like has_add.

With these problems solved, we should have a dimensional analysis system that can achieve what wolfram alpha can achieve (besides constructing the dimensionless numbers), but in a formally verified environment, which would be awesome. Also, sympy has a dimensional analysis program that can pull equations directly from wikidata and we are looking at setting up a similar automation so we can automatically check the dimensional homogeneity of all the equations in wikidata.

[Eric Wieser]

docs#pi.single gives you the function that's zero at all but one place

[Max Bobbin]

Eric Wieser said:

docs#pi.single gives you the function that's zero at all but one place

Would it be possible to see an MWE of using pi.single or if you could direct to any code that uses it? I'm having trouble understanding how it exactly works with the tuple I defined.

[Eric Wieser]

I would guess you can write

def your_tuple : Π n, fin n → ℚ
| 0 := 0
| (n + 1) := pi.single 0 1

[Eric Wieser]

Or,

def your_tuple (n : ℕ) : fin n.succ → ℚ :=
pi.single 0 1

[Max Bobbin]

Eric Wieser said:

Or,

def your_tuple (n : ℕ) : fin n.succ → ℚ :=
pi.single 0 1

Awesome, this works perfectly. An example of showing dimensional homogeneity:

def length_tuple_constructor  : Π n, fin n → ℚ
| 0 := 0
| (n + 1) := pi.single 0 1
def length := dimension.mk length_tuple_constructor


def area := length^2

theorem length_pow_three_div_length_eq_area
:length^3/length = area :=
begin
  field_simp [length, area],
  funext n i,
  induction n with d,
  simp [length_tuple_constructor],
  field_simp [length_tuple_constructor],
  rw [← one_mul (pi.single 0 1 i), ← mul_assoc, ← mul_assoc, ← sub_mul],
  norm_num,
end

This isn't a mwe, cause it needs the math as well, but my group is quite happy to have something that is on par or better than sympy and mathematica. We are also excited to see how we can make it even better with Lean 4.

[Max Bobbin]

although, I still have to figure out addition

[Eric Wieser]

I don't really understand your model for dimensions; what is n here?

[Yaël Dillies]

The number of dimensions IIUC

[Yaël Dillies]

I think what you want is rather something like by ext; fin_cases; norm_num

[Eric Wieser]

So 2D is length + time, 1D is length, 0D is only dimensionless? What if I want only time?

[Yaël Dillies]

No, sorry, I guess I rather mean number of quantities. So dimensionless is 0.

[Eric Wieser]

I think a better way to represent this type of user-extensible "sorts" of dimensions is with typeclasses

[Eric Wieser]

Such as:

import data.list.basic
import algebra.group.to_additive
import algebra.group.pi
import data.rat.basic

class si_dimension_system (α : Type*) :=
[dec : decidable_eq α]
(time [] : α) -- etc
(length [] : α) -- etc
(mass [] : α) -- etc
(h : [time, length, mass].nodup)

attribute [instance] si_dimension_system.dec

@[derive comm_group]
def dimension (α : Type*) := multiplicative (α → ℚ)

def dimension.length (α) [si_dimension_system α] : dimension α :=
pi.single (si_dimension_system.length α) 1
def dimension.time (α) [si_dimension_system α] : dimension α :=
pi.single (si_dimension_system.time α) 1
def dimension.mass (α) [si_dimension_system α] : dimension α :=
pi.single (si_dimension_system.mass α) 1

open dimension

variables (α : Type*) [si_dimension_system α]
example : length α / length α = 1 := div_self' _

[Eric Wieser]

That means that I can have

inductive your_system
| T | L | M

instance : si_dimension_system your_system := sorry

inductive my_system
| T | L | M | ZULIP_MESSAGE_COUNT

instance : si_dimension_system my_system := sorry

and can then use the same lemmas for each

[Max Bobbin]

I can't attest to the use of your code. I don't understand it and would have to spend some time and play around with it and understand what's going on. However, my thought process along with comments from my previous post, was the n-tuple is the tuple of the dimension exponents, where n signifies the number of dimensions that exists. Commonly it's taken as 7, but you could have more by accounting for other things like a currency dimension. In this case, we define length to be the exponent in the first spot of the tuple, mass to be the second, time the third, and so on. So while you can't talk about time, without having the spot exist for length, the spot for length can be zero. For applications with Buckingham pi, we want to be able to construct a matrix of the exponents of a set of dimensions. For instance

![velocity.exponent^T,distance.exponent^T]

which corresponds to the matrix

[1, 1
 0, 0
 1, 0],

so, while mass does appear in this matrix, it's just a row of zeros and doesn't change the rank. I will look over the code and try to understand it, but I hope that clears up our thought process.

[Matt Diamond]

@Eric Wieser is there anything in TPiL or any other reference about the use of empty square brackets in field names? I've seen it before but I never really understood what that notation does...

class si_dimension_system (α : Type*) :=
[dec : decidable_eq α]
(time [] : α) -- etc
(length [] : α) -- etc
(mass [] : α) -- etc
(h : [time, length, mass].nodup)

[Eric Wieser]

Have a look at #check time with and without the []

[Kevin Buzzard]

IIRC this binder trick might be mentioned in passing in the description of list as an inductive type, where I think it's used

[Eric Wieser]

but you could have more by accounting for other things like a currency dimension

This means that code using your API has to globally agree on how the dimensions are numbered. But we already have a mechanism for global agreement in lean; the typeclass system! has_add provides a way for types to agree on a single spelling for +; so in the same way, my si_dimension_system allows types (here, choices of dimension labelling) to agree on a single spelling for common dimensions

[Eric Wieser]

However, my thought process along with comments from my previous post, was the n-tuple is the tuple of the dimension exponents, where n signifies the number of dimensions that exists.

What's the advantage in your opinion of using Π n : ℕ, fin n → rat here instead of the simpler ℕ → rat?

[Eric Wieser]

I don't understand it and would have to spend some time and play around with it and understand what's going on

If you take one thing away from my code, I recommend it be

@[derive comm_group]
def dimension (α : Type*) := multiplicative (α → ℚ)

This gives you all the semantics of dimension multiplication / division / inverse / dimensionlessness without any effort at all, saving you over 100 lines. multiplicative says "when you multiply this object, add its internal representation".

If you feel strongly about using Π n : ℕ, fin n → rat, then multiplicative (Π n : ℕ, fin n → rat) will work for you,

[Max Bobbin]

I see what you mean. In the coming weeks I will look at implementing this and come back with a version 3. To double check I understand, your si_dimension_system class is like the has_add class and is used to show that your_system and my_system are both talking about the same length, mass, and time? That way we can define properties about the si_dimension_system class and then implement those properties for the system? Would it make sense to split up the si_dimension_system```` class into multiple classes, like has_length, has_mass```, etc? I was wondering if that way is better so that later, a new dimension can be added without disrupting the classes.

[Tyler Josephson ⚛️]

Thanks for the help, @Eric Wieser ! A note on naming convention - we should use “ISQ” rather than “SI” in the class name, since SI refers to units (e.g. seconds, meters, etc.) rather than dimensions (time, length, etc.).

[Eric Wieser]

Yes, splitting up into the classes would be reasonable if you want to do that

[Eric Wieser]

But my guess would be that really you care only about ISQ or ISQ + x