(FL) tensor algebra

[Norman Megill]

-------- Forwarded Message --------
Subject: tensor algebra
Date: Fri, 22 May 2020 14:05:07 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

Can you post that:

I want to make some proofs in tensor algebra but I don't want to put them in a mathbox of m'y own. Is it possible to put them in the Commons part.

--
FL


This is not our practice and seems unfair to others whose work starts in mathboxes, but other people can give their opinions.

Norm

[Jim Kingdon]

If the goal is to write some proofs (which is fun!) and make them public on the website, a mathbox would achieve those two things. For a while I was maybe a little bit worried about where to put proofs, or whether I "believe in" (whatever that means) mathboxes, or naming, or whatever organizational issue, but when I get down to writing the proofs and getting people to collaborate, it becomes a lot easier to solve the problems which are really in the way, and sort of shrug about the things which maybe I might want to propose changing some day, but where for now I can just use current patterns (in this case, a mathbox, unless there is something I misunderstand about how we usually operate).

[Alexander van der Vekens]

I do not know what is meant by "Commons part": there is no "Part" in set.mm having this (or a similar) title. Is it the main body of set.mm (parts 1-17)? Then I would disagree with putting new theorems/concepts into the main body before they are mature enough and reviewed by others. If, however, there shall be a new part called "Commons" between the main body and the mathboxes, a kind of "Mathbox for everyone" (maybe becoming section 21.2 instead of a part by itself), then I think this could be a good idea, which I considered myself already before (in other posts).

Alexander

[Norman Megill]

-------- Forwarded Message --------

Subject: Tensors
Date: Sat, 23 May 2020 14:12:40 +0200 (CEST)
From: fl
To: Megill Norman

 Hi Norm,

Can you post this:

so it seems people agree for a tensor algebra development in the Commons part. If Norm has no further concerns, we can begin

--
FL


As was already mentioned, there is no section called "Commons". There is a section called "(Future - to be reviewed and classified)" that possibly could be renamed as discussed here:
https://groups.google.com/d/msg/metamath/UwTUuNPgaB0/NdWefzG4AgAJ
The purpose of this section is to provide a place for theorems needed by 2 or more mathboxes that otherwise don't currently have a place elsewhere in set.mm. While I'm not rejecting your proposal out of hand, your work would not immediately be needed by 2 mathboxes, and to me it doesn't really fit in with the purpose of this section. I would prefer that you use a mathbox like everyone else.

Nonetheless, if we are to place your work directly in the main part of set.mm, it needs to be of high quality and vetted. It would be good if you post here the new definitions you propose and provide a description or outline of what theorems you intend to prove. Could you do that? Thanks.

Norm

[Alexander van der Vekens]

On Saturday, May 23, 2020 at 11:52:50 PM UTC+2, Norman Megill wrote:

...

As was already mentioned, there is no section called "Commons". There is a section called "(Future - to be reviewed and classified)" that possibly could be renamed as discussed here:
https://groups.google.com/d/msg/metamath/UwTUuNPgaB0/NdWefzG4AgAJ
The purpose of this section is to provide a place for theorems needed by 2 or more mathboxes that otherwise don't currently have a place elsewhere in set.mm. While I'm not rejecting your proposal out of hand, your work would not immediately be needed by 2 mathboxes, and to me it doesn't really fit in with the purpose of this section. I would prefer that you use a mathbox like everyone else.

I was not aware of section "(Future - to be reviewed and classified)" until now (sorry, Norm, that I did not noticed it in your post on April 25, 2020).  In this post, it is written:

3. Note that we already have a section called "(Future - to be reviewed and classified)" http://us.metamath.org/mpeuni/mmtheorems.html#dtl:17.3 that was added primarily for the purpose of the "Commons" you mention. If people think that renaming it to "Commons" would be more intuitive, that's fine with me. Maybe "(Commons - to be reviewed and classified eventually)".

I would propose to move this section into part PART 21  SUPPLEMENTARY MATERIAL (USER'S MATHBOXES), maybe as section "21.2 Mathbox for Commons". In the section header, it could be described in more detail what this section contains and how it should be used: definitions/theorems to be reviewed and classified eventually, not yet mature enough to be contained in the main body of set.mm, processed by more than one person, used in a personal mathbox, etc. - and which rules should be obeyed (additional content should be available in a personal mathbox for some time before, review during a PR recommended, contents should not be deleted or significantly modified without asking the contributor, etc.). The main reason to treat this section as mathbox is that the definitions/theorems of this section should be treated as if they were contained in a mathbox (e.g. should not be used by minimize by default). According to the existing rule, the definitions/theorems of this section should be moved to the main body if they are used in at least 2 personal mathboxes. As I have written already before, the definitions/theorems of this section could be regarded as "release candidates" for the main body of set.mm.

Nonetheless, if we are to place your work directly in the main part of set.mm, it needs to be of high quality and vetted. It would be good if you post here the new definitions you propose and provide a description or outline of what theorems you intend to prove. Could you do that? Thanks.

I agree with Norm that the general rule should still be to provide new proposals in a (personal) mathbox first (to demonstrate a certain amount of maturity). Exceptions could be granted if such a demonstration is provided on another way, e.g. by a post in the Google group as Norm proposed, or as "issue" in GitHub.

Alexander