Adding proof of Kochen-Specker paradox to Mathlib?

Stream: mathlib4

[Vedant Gupta]

Hi everyone! I'm a senior at Brown, and recently finished Rob Lewis' class on formal proof and verification. For my course project, I formalized the Kochen-Specker paradox (which is used to prove the Strong Free Will Theorem) using Lean4 & Mathlib.

I would love to add this to Mathlib if that is of interest, and am hoping to get some advice on this here. My code for the project is **here**.

In writing this project, I had to prove some helper lemmas that I was surprised to not find in Mathlib (my apologies if I missed something here!). I'm listing these below to gauge whether they would be helpful additions:

1 - The cross product of orthogonal unit vectors is a unit vector (more generally, the relation between the norms of vectors and the norm of their cross product)
2 - Transformation of vectors under a member of an orthogonal group preserves norms and dot products.

[Ruben Van de Velde]

I think the helper lemmas definitely should go into mathlib. For the main result - Wikipedia states it in a very quantum physics way, not sure if that's an issue / if that's also the case for your formalisation

[Vedant Gupta]

I see, thanks! For the main result, I use the statement at the bottom of page 227 in this paper by Simon Kochen, which makes sense independent of any physics concepts. This version states that:

It’s impossible to color every point on the surface of a sphere using only two colors (red and blue) in such a way that, for any three points that are mutually perpendicular wrt the center (like the tips of the x, y, and z axes), exactly one point is red and the other two are blue.

[Vedant Gupta]

Would this theorem (as stated above) be an appropriate addition to Mathlib?

[Joseph Myers]

Regarding the helper lemmas suggested:

• We don't have much at all on cross products (more could certainly be added), they were just added to mathlib to check off an entry from the undergrad list.
• For transformations under a member of an orthogonal group, maybe this is about there being multiple ways to express the same thing. If your orthogonal group is defined using LinearIsometryEquiv on an inner product space, we already have that it preserves norms and inner product; I suppose you're using something else such as Matrix.orthogonalGroup?

[Vedant Gupta]

Yup I am using Matrix.orthogonalGroup, I didn't realize that LinearIsometryEquiv would have given me more helper lemmas at the time.
I would love to contribute the cross product lemma and the Kochen-Specker paradox (if appropriate) to Mathlib. I haven't contributed to Mathlib before, so any guidance would be very appreciated!

[Notification Bot]

This topic was moved here from #new members > Adding proof of Kochen-Specker paradox to Mathlib? by Rob Lewis.

[Rob Lewis]

@Vedant Gupta and I just had a quick chat about this and I'm moving this thread to #mathlib4 for the sake of visibility!

[Kim Morrison]

The paradox itself, as stated above, could perhaps go in Archive?

[Vedant Gupta]

I see! I think a lemma proving that the cross product of two vectors (a, b) has norm |a||b|sin(theta) would be a useful addition to Mathlib. Should I open a PR to add that to the existing CrossProduct.Lean file in Mathlib?

And then if/when that goes through I could open a PR to add Kochen-Specker to the Archive folder?

[Thomas Browning]

Maybe not into the existing CrossProduct.lean file since that would drastically increase the imports, I think. But it would be good to have this result and also the formula for the dot product.

[Vedant Gupta]

how about I make a new file in the LinearAlgebra folder?

[Vedant Gupta]

Could I please get write access to non-master branches of Mathlib? My github username is Mr-vedant-gupta

[Kim Morrison]

@Vedant Gupta, please check your (email) inbox.

[Vedant Gupta]

(deleted)

[Vedant Gupta]

I've made a PR. @Thomas Browning I've added the code to the existing CrossProduct.lean file as I only use two additional imports (though this was sufficient to trigger the large-imports flag). Also, I believe the corresponding formula for dot products already exists in Mathlib (see Geometry/Euclidean/Angle/Unoriented/Basic.lean). Please let me know if I should still shift the cross product norm result to a separate file.

[Yaël Dillies]

Pro-tip: You can write #20920 and have Zulip display it as #20920

[Thomas Browning]

It shouldn't go in CrossProduct.lean since that requires importing a lot of analysis into CrossProduct.lean (hence the large-import flag). I'm not sure where the best place for it is, but potentially somewhere in Geometry/Euclidean/Angle?

[Vedant Gupta]

Geometry/Euclidean/Angle/Unoriented/Basic.leanlooks like the best fit?

[Thomas Browning]

Perhaps. You can try moving the results to that file and see how the imports are affected.

[Vedant Gupta]

I have to add the following two imports to Geometry/Euclidean/Angle/Unoriented/Basic.lean:

import Mathlib.LinearAlgebra.CrossProduct
import Mathlib.Analysis.InnerProductSpace.PiL2

This is still triggering the large-imports flag but the percentage increase in imports is significantly smaller (3.75% vs 70%). Thematically, this seems like the best file placement too. Is the increase in imports acceptable?

[Ruben Van de Velde]

Probably. Your reviewer will check

[Vedant Gupta]

PR #20920 (with results on Cross Products) is in. Should I begin another PR to now add Kochen-Specker to the archive section?

[Johan Commelin]

Sounds good, I guess