LINEAR-GREEDY HYBRID: Refute 1323->2744

[teorth]

Proof can be found either at https://leanprover.zulipchat.com/#narrow/channel/458659-Equational/topic/1323/near/481475622 or in the blueprint at #810.

When done, mark appropriate theorems in the blueprint with \lean and \leanok tags and remove the appropriate conjectures from Conjectures.lean.

[mjtb49]

The 1898 -> 2710 implication has been superseded by the proof of 1729 -> 817.

[teorth]

Fair point, but I'll keep the claim for now as any refutation of 1323->2744 will likely also give 1898->2710 almost for free, and the proof may be a warmup for the more complicated 1729->817.

[amirlb]

claim

[teorth]

I've realized that due to some changes in the proof over time, the 1898->2710 implication no longer comes "for free" from the 1323->2744, so given that it is also implied by 1729->817, I have now removed it.

[amirlb]

Trying to formalize the outline of the proof in Lean, it pointed out a miscalculation in lemma 15.3: When trying to prove Ly Ry x = R_Sy x in the case where x and y are both non-squares with the same square, in the next-to-last sentence in the proof, equation 3 reduces to (ϕ_a(a + c) y, a) = (-x, a). But we have x = ϕ_a(c) y, and the ϕ's don't cancel out.

This problem is solved by replacing ℚ* with a group ℤ/2 × G for some large-enough abelian group G, and requiring that the relation between ϕ_a(a + b) and ϕ_a(b) is flipping the first coordinate instead of inversion.

Do you think this change would break other parts of the proof? What properties does G need to have to prevent collisions? I'll probably implement the direct sum of in infinite number of copies of ℤ/2 for the squares part, would it be enough to take as G as well?

[amirlb]

Seems to me that the simplest fix in the blueprint is to change 15.2 to say phi(a+b) = -phi(b). The formal proof will probably use some variant on the free group, like other formalizations in this project.

[teorth]

Yes, I think that fixes it. Thanks for locating the issue! I've updated the blueprint accordingly.

[amirlb]

propose #1021