## Stream: new members

### Topic: Math physics in Lean

#### Kevin Sullivan (May 17 2019 at 16:35):

One of the main use cases for abstract math is physics. Suppose I want to do physics formally using Lean. One of the mathematical structures I'd like to work with is that of the real Euclidean space. Can you help me understand how close or far we are from being able to represent real Euclidean spaces in Lean, including objects such as points and vectors, operations such as vector-vector and point-vector addition, and transformations such as rigid body motions and affine transformations more generally? (Beneath this question lies the fact that, for me at least, without many examples, it's hard to know what I can do with the bits and snippets I find out there, e.g., reals as Cauchy sequences, etc.)

#### Mario Carneiro (May 17 2019 at 16:36):

right now we are fairly close, but we are still working in some ridiculous generality

#### Mario Carneiro (May 17 2019 at 16:37):

we have normed vector spaces, but not much about finite dimensional vector spaces and even less about R^n specifically

#### Kevin Sullivan (May 17 2019 at 17:41):

we have normed vector spaces, but not much about finite dimensional vector spaces and even less about R^n specifically

Mario, Thanks. Do you have any guidance on how to gain an understanding of (1) what's already done---if only what files to look at, but better yet some applications that use them, or even better yet, papers about them, (2) what would need to be done to get to the point where we could model finite Euclidean spaces, particularly over the reals, even if only as a special case?

#### Kevin Buzzard (May 17 2019 at 17:42):

I would just fire up a new file and start writing. All the infrastructure you need should be there, as far as I know, it's just that nobody really did $\mathbb{R}^n$ yet.

#### Kevin Buzzard (May 17 2019 at 17:42):

They're not keen on all these concrete examples ;-)

#### Kevin Buzzard (May 17 2019 at 17:43):

You might find that $\mathbb{R}^n$ automatically becomes a real vector space, so a bunch of what you're hoping to find might just magically appear.

#### Kevin Buzzard (May 17 2019 at 18:05):

Feel free to ask questions -- I think this is a very attainable goal.

#### Kevin Buzzard (May 17 2019 at 18:13):

import data.real.basic algebra.pi_instances

def ℝspace (n : ℕ) := fin n → ℝ

instance (n : ℕ): add_comm_group (ℝspace n) := by unfold ℝspace; apply_instance
noncomputable instance (n : ℕ): vector_space ℝ (ℝspace n) := by dunfold ℝspace; apply_instance

variables (n : ℕ) (v w : ℝspace n) (r : ℝ)

#check v + w -- adding vectors
#check r • v -- scalar times vector


#### Johan Commelin (May 17 2019 at 18:15):

@Kevin Sullivan Further tips: the search function on Github and in VScode can be really useful. If those fail, just ask about a specific concept here, and we'll be able to tell you if it's in the library. You will hit things that are missing quite soon. But it is hard to tell what they are without starting out on a Lean file.

#### Kevin Buzzard (May 17 2019 at 18:16):

And feel free to change the name of Rspace! I just had to write something...

#### Kevin Sullivan (May 24 2019 at 01:59):

And feel free to change the name of Rspace! I just had to write something...

Thank you, Kevin, Johan, Mario. I'm working through your suggestions. A question comes up. What is the conceptual difference between field and discrete_field? The latter is a term I perhaps should know but don't know from my limited studies of algebra.

#### Keeley Hoek (May 24 2019 at 02:02):

I think the rule is discrete_field is a maths field and we should all pretend field doesn't exist (and we'd change the name if it wasn't in core).

Ok, I see.

#### Kevin Sullivan (May 24 2019 at 14:57):

And feel free to change the name of Rspace! I just had to write something...

Ok, so I have started typing. The aim is to develop at least a formal sketch of a formalization of affine spaces. Here's how I started, and I immediately ran into a few questions, which I pose here.

You will recall that an affine space comprises a vector space V over a field K and a nonempty set, A, of points, with an addition operation, + : point -> vector -> point, satisfying a few axioms (e.g., \all p, p + 0 = p). My implementation strategy is to build on what's already in the libraries. So here's how I started.

class affine_space
(P : Type)                                                  -- points
(K: Type) [discrete_field K]               -- scalars
(G : Type) [add_comm_group G]    -- vectors
(V : vector_space K G) :=                     -- K vector space over G
(add : P → G → P)


I initially typed "add : P → V → P", but of course V isn't a type. On the other hand, P → G → P looks odd. Indeed, even the presence of G in my definition seems a bit weird, as mathematical texts would not mention additive groups when defining affine spaces. So, question #1: does "add : P → G → P" look right? I'd like to be sure that I start with a sound typeclass specification before building all the rest of it.

Question #2: I've chosen to use "has-a" relations rather than "is-a", (using object-oriented lexicon), to define affine_space. By this I mean that I incorporate P, K, G, and V as field values rather than by using "extends" to "inherit" these structures. The rational is that an affine space "has a" vector space but not "is a" vector space. So does the structure I've defined "look right" to those of you who design these kinds of libraries?

Thank you!
Kevin

#### Mario Carneiro (May 24 2019 at 15:05):

Q1: The convention would be to call G V, and call V nothing (put it in square brackets)

#### Kevin Sullivan (May 24 2019 at 15:07):

Q1: The convention would be to call G V, and call V nothing (put it in square brackets)

Perfect, thank you.

#### Reid Barton (May 24 2019 at 15:10):

And P would probably go last

#### Johan Commelin (May 24 2019 at 15:15):

Unfortunately we only have mul_action... so you can't use that class (in a clean way).

#### Johan Commelin (May 24 2019 at 15:18):

It would probably make sense to setup a general theory of torsors... and then define an affine space to be a torsor of a vector space.

#### Johan Commelin (May 24 2019 at 15:20):

You would be able to reuse the general setup for things like quantities (mass, length, &c are torsors under units real). I'm far from being a (mathematical) physicist, so I have no idea if that would be useful.

#### Neil Strickland (May 24 2019 at 15:21):

Let's ignore for the moment the fact that you want to use additive notation. Then the natural thing would be to start with the class mul_action G X from src/group_theory/group_action.lean, and extend it to give a class principal_action involving a "division" map X → X → G such that (y / x) • x = y. You might need some other axioms, or they might follow automatically, especially in the case where G is a group. Then you could specialise to the case where G is the additive group of a vector space.

It's also possible to leave G out of the picture and axiomatize everything in terms of the subset of parallelograms in X ^ 4; then you recover G as a quotient of X ^ 2.

Ideally we should have a class for additive actions that is magically connected to the class for multiplicative actions, so we don't have to prove essentially the same results twice. We have similar things in some closely related contexts, but not this one. But it would not be hard for you to define add_action by hand, just following the example of mul_action.

#### Johan Commelin (May 24 2019 at 15:22):

The reason I did not define add_action is notation...

#### Johan Commelin (May 24 2019 at 15:22):

We can't reuse + for these, even though that would be very natural.

#### Kevin Sullivan (May 24 2019 at 15:29):

I'm listening. I've incorporated comments down through Reid Barton's to arrive at the following. But I'm open to reworking it entirely in light of the subsequent comments. Feedback sought on both the current formulation, as well as on the subsequent comments. My overall aim is to develop a formalization in terms of which to express mathematical physics, starting with the classical (Newtonian) case.

class affine_space
(K: Type) [discrete_field K]
(V : Type) [add_comm_group V] [vector_space K V] :=
(P : Type)
(add : P → V → P)
(right_zero : ∀ (p : P), add p 0 = p)
(unique : ∀ (p q : P), ∃ (a : V),
(q = add p a) ∧
(∀ (a b : V), (q = add p a) → (q = add p b) → a = b))


#### Mario Carneiro (May 24 2019 at 15:32):

unique has a name clash in the variables

#### Mario Carneiro (May 24 2019 at 15:33):

also don't use /\ in an axiom if you can avoid it - use two axioms

#### Reid Barton (May 24 2019 at 15:33):

You probably want to replace unique anyways with a second operation sub : P -> P -> V and whatever axioms are necessary to characterize it uniquely

^ that

#### Reid Barton (May 24 2019 at 15:37):

∀ (p : P), ∀ (a b : V), can be simply ∀ (p : P) (a b : V),

#### Reid Barton (May 24 2019 at 15:37):

but now this is getting into just style things

#### Kevin Sullivan (May 24 2019 at 15:45):

but now this is getting into just style things

So here's where I've gotten to.

class affine_space
(K: Type) [discrete_field K]
(V : Type) [add_comm_group V] [vector_space K V] :=
(P : Type)
(add : P → V → P)
(right_zero : ∀ (p : P), add p 0 = p)
(sub : P → P → V)
(sub_exists : ∀ (p q : P), ∃ (a : V),  a = sub q p)
(sub_unique : (∀ (p q : P) (a b : V), (q = add p a) → (q = add p b) → a = b))


I can work the details of the axioms from here. I guess the remaining pending question is whether this is a good start on an affine space library or whether to revert to a more general theory of torsors with the affine space case as a special case. Or to go with the suggestion by Neil Strickland. The torsor direction is intriguing as our aim is to formalize aspects of physics and metrology, and, indeed, things like time, location, and voltage are torsors. I don't have a strong intuition for how hard it'd be to go in this direction given what's already in the libraries, nor what tradeoffs would be involved in eventually using such a formalization as a target for a physical denotational semantics of programming code (which is where we're headed with this work). Comments/thoughts welcome.

#### Kevin Sullivan (May 24 2019 at 17:21):

It would probably make sense to setup a general theory of torsors... and then define an affine space to be a torsor of a vector space.

Is something like this what you had in mind?

class torsor
(X : Type) [inhabited X] :=
(add : G → X → X)
(left_zero : ∀ (x : X), add 0 x = x)
(sub : ∀ (x1 x2 : X), ∃ d, x2 = add d x1)
(sub_unique : ∀ (g1 g2 : G) (x1 x2 : X), x2 = add g1 x1 → x2 = add g2 x1 → g1 = g2)

class affine_space
(K: Type)  [discrete_field K]
(V : Type) [add_comm_group V] [vector_space K V]
(P : Type) [inhabited P]
extends torsor V P


#### Mario Carneiro (May 24 2019 at 17:24):

sub still isn't a function... are you expecting to be able to define the function after the fact?

#### Mario Carneiro (May 24 2019 at 17:24):

that's how it's done in maths but in lean it doesn't work as well

#### Reid Barton (May 24 2019 at 17:56):

From a math (or a mathlib) perspective it certainly makes sense to define torsors in general and then define affine spaces as torsors over a vector space. But if you're just prototyping for now then there's no need to try to do everything in maximal generality from the start.

#### Reid Barton (May 24 2019 at 18:01):

(Warning: mathematician, not a physicist)
The way I eventually learned to think about units is as independent ways in which we believe physics is scale-invariant. For example in Newtonian physics I guess there are seven independent "dimensions" (not sure what the official term is), one per SI unit: time, length, mass, charge and so on. Each of these corresponds to a separate action of units real (or what a mathematician would call G_m) on physical quantities, so that all together we have actions of units real x ... x units real. For example a length is a vector in the vector space on which the copy of units real corresponding to length acts in the tautological way ($t$ acts by multiplication by $t$), and all the other copies act trivially.

#### Reid Barton (May 24 2019 at 18:03):

If we call this representation $L$, then a "length squared" is a vector in $L \otimes L$, which is again one-dimensional over the reals but has the action of length scaling where $t$ acts as multiplication as $t^2$.
In this way time, length, etc. are quantities that belong to non-isomorphic representations of the big group (units real)^7, so there is no way that you can confuse them.

#### Kevin Sullivan (May 24 2019 at 18:22):

sub still isn't a function... are you expecting to be able to define the function after the fact?

Oops. How's this?

class torsor
(X : Type) [inhabited X] :=
(add : G → X → X)
(left_zero : ∀ (x : X), add 0 x = x)
(diff_exists : ∀ (x1 x2 : X), ∃ d, x2 = add d x1)
(diff_unique : ∀ (g1 g2 : G) (x1 x2 : X), x2 = add g1 x1 → x2 = add g2 x1 → g1 = g2)
(sub : X → X → G)
(sub_add : ∀ (x1 x2 : X), add (sub x2 x1) x1 = x2)


#### Johan Commelin (May 24 2019 at 18:22):

diff_exists is now redundant. And you can rephrase diff_unique using sub, I guess.

#### Neil Strickland (May 24 2019 at 18:23):

Here's a similar but slightly different perspective. The special relativity model says that spacetime is an affine space V. This can be formulated in terms of parallelograms, which are quadruples of events that can be characterised by certain idealised physical properties. The parallelogram structure gives an equivalence relation on V × V with quotient T say, and gives a vector space structure on T. Experimental properties characterise the light cone C ⊂ T and divide T \ C into subsets  T₊, T₋ and T₀ of future, past and spacelike vectors. Let L' be the space of homogeneous quadratic functions on T that vanish on the light cone. This is one-dimensional and has a canonical half-space of forms that are positive on timelike vectors. This gives us a canonical oriented square root L with L ⊗ L = L', and measurements of time and distance naturally take values in L. (In this framework, times and distances are automatically identified via the speed of light.)

#### Kevin Sullivan (May 25 2019 at 01:28):

diff_exists is now redundant. And you can rephrase diff_unique using sub, I guess.

Edited as follows:

class torsor
(X : Type) [inhabited X] :=
(add : G → X → X)
(left_zero : ∀ (x : X), add 0 x = x)
(sub : X → X → G)
(add_diff : ∀ (x1 x2 : X), add (sub x2 x1) x1 = x2)
(diff_unique : ∀ (g1 g2 : G) (x1 x2 : X), g1 = sub x2 x1 → g2 = sub x2 x1 → g1 = g2)


Any comments on field names vs prevailing conventions?

#### Kevin Sullivan (May 25 2019 at 01:34):

Here's a similar but slightly different perspective. The special relativity model says that spacetime is an affine space V. This can be formulated in terms of parallelograms, which are quadruples of events that can be characterised by certain idealised physical properties. The parallelogram structure gives an equivalence relation on V × V with quotient T say, and gives a vector space structure on T. Experimental properties characterise the light cone C ⊂ T and divide T \ C into subsets  T₊, T₋ and T₀ of future, past and spacelike vectors. Let L' be the space of homogeneous quadratic functions on T that vanish on the light cone. This is one-dimensional and has a canonical half-space of forms that are positive on timelike vectors. This gives us a canonical oriented square root L with L ⊗ L = L', and measurements of time and distance naturally take values in L. (In this framework, times and distances are automatically identified via the speed of light.)

Neil,

Thank you for your suggestion. For formalizing basic metrology (units of measure) and classical dynamics, my guess is that the formalization of the ordinary definition of torsors and affine spaces as torsors over vector spaces will suffice. However, we mean to develop a physical semantics of code for cyber-physical systems in general, eventually to include systems that are subject to relativistic effects (satellites, space missions, etc). We might well circle back around to the path you suggest. In the meantime I will try to acquaint myself with the material you highlight. Thank you.

#### Mario Carneiro (May 25 2019 at 01:36):

diff_unique is now just transitivity

#### Mario Carneiro (May 25 2019 at 01:37):

I think what you could say is add g x = y <-> sub x y = g

#### Mario Carneiro (May 25 2019 at 01:38):

or you could express it as the two cancellation laws add (sub x y) y = x and sub (add g x) x = g

Last updated: May 14 2021 at 13:24 UTC