State and prove Theorem 2.36

[jscanvic]

• Add theorems Finite.Equation28394_implies_Equation2 and Equation28394_not_implies_Equation2 closing INFINITE: State and prove Theorem 2.36 (second Kisielewicz law) of the blueprint in Lean. #125.
• Introduce Equation28394, a fixed version of Equation28393.

[Shreyas4991]

@jscanvic : since this is a draft PR, GitHub won't automatically show this, but an upstream PR might have introduced merge conflicts due to the notation change for Magma. Could you check if merging the main branch into your branch works?

[jscanvic]

@Shreyas4991 It appears to be working after changing the notation.

[Shreyas4991]

The PR is marked as a draft. The CI will automatically run when the PR is not a draft anymore. I have manually run it for now.

[jscanvic]

awaiting-review

[jscanvic]

Uhm apparently the build fails due to 4 newly added theorems in Subgraph.lean which depend on the previous formula for Equation28393. I'm not sure what the way forward is. Keeping the previous one and changing the number for the fixed one?

[Shreyas4991]

is the new equation 23893 a completely different equation from the previous one. If so, how does giving it a different number and retaining the old equation 23893 affect this PR?

[jscanvic]

The two equations are indeed completely different. As far as I can tell, giving the new one a new number would simply require changing it in the blueprint infinite_models.tex.

[Shreyas4991]

Then this would be the path of least resistance. I would recommend it.

[jscanvic]

Alright! I've made the changes from 28393 to 28394.

[teorth]

Actually the equation x = (((y ◇ y) ◇ y) ◇ x) ◇ (y ◇ z) is numbered 28770, and x = (((x ◇ x) ◇ x) ◇ y) ◇ (x ◇ z) is equation 28381. The full list can be found at https://github.com/teorth/equational_theories/blob/main/data/eq_size5.txt . Sorry for screwing up the numbering previously, but this should be the canonical numbering to use going forward.

[jscanvic]

My bad. I wasn't aware of the extended numbering. It should be good now!

[teorth]

Small blueprint issue - one of the references to 28393 in the blueprint now has to be renumbered. Sorry, that should be the last thing and then we can merge!

[jscanvic]

Done!