1661 -> 1657 - another one bites the dust

Stream: Equational

[Zoltan A. Kocsis (Z.A.K.)]

The nice infinite model shown on the screenshot proves that 1661 does not imply 1657. I think this'll settle1661->1659? negatively as well, and several others. I'm cleaning up / finishing off the Lean proof now.
1661-1657.png

[Zoltan A. Kocsis (Z.A.K.)]

Notes: the operation is basically
$x \diamond y = \begin{cases} x-1 & \text{if }x,y \text{ same parity}, \\ x+1 & \text{if }x,y \text{ opposite parity}.\end{cases}$

Then we have (y◇z)◇y = y when y,z have the same parity, and (y◇z)◇y = y+2 when y,z have opposite parities. Thus, if x,y have the same parity, (x◇y)◇((y◇z)◇y) = (x-1)◇y = x or (x◇y)◇((y◇z)◇y) = (x-1)◇(y+2) = x, i.e. 1661 is satisfied. The other cases are similar.

Of course, this operation ◇ is not well-defined on Nat around 0 and in any case satisfies 1657. But we can "fix" the values around 0 in such a way that 1657 fails while 1661 is retained (that's what the 4 special cases accomplish).

[Kevin Buzzard]

Can you work with Int to fix the issue at 0?

[Zoltan A. Kocsis (Z.A.K.)]

@Kevin Buzzard Yes, and if you do it the naive way, by extending the diamond above to the negatives, the resulting operation does satisfy 1657 (which we do not want).

If you do it the smart way, however, you have less work to do if you just stick with the naturals.

[Zoltan A. Kocsis (Z.A.K.)]

(Speaking of,I tried to be clever by doing an induction proof, but I think the straightforward case analysis will turn out to be nicer in the end :sad: , so I'm moving there now)

[Terence Tao]

It's interesting that this construction is some finite modification (and truncation) of the translation invariant magmas y ◇ x = x + f(x-y) that ended up resolving the 65->1491 anti-implication. I wonder if there is some way to identify equations that not only admit non-trivial translation-invariant models, but also have the ability to locally modify those models to still obey the equation, in order to preserve that law but break some other law.

p.s. when you PR the proof, you can also update the "selected magmas" chapter of the blue[rint to add the example.

[Zoltan A. Kocsis (Z.A.K.)]

It took me longer than expected to structure this proof; I'm sitll not completely happy with it, but it looks like it's done. I'm running checks, will post a PR within the hour.

[Zoltan A. Kocsis (Z.A.K.)]

This is now PR #503.

[David Renshaw]

I opened equational#512 to clean up InfModel_1661.lean a bit.

[David Renshaw]

Looks like it may introduce some conflicts with equational#511.

[Zoltan A. Kocsis (Z.A.K.)]

Okay, so all that 511 does is:

1. Move the main proof (that 1661 is satisfied in the magma I constructed) out of the "1661 does not imply 1657" environment.
2. Runs a few more implications in the end.

[Zoltan A. Kocsis (Z.A.K.)]

511 does not modify the main proof in any other way. It should be easy to update your 512 to be compatible with that (massive thanks for this btw @David Renshaw ).

[Zoltan A. Kocsis (Z.A.K.)]

Good news: it looks like this construction will prove a bunch of other anti-implications too.
I'll have to check the details in the morning but I think I have a patched countermodel to 1701 -> 8.

[David Renshaw]

In equational#524 I use the duality metatheorem some of our duality theory to knock out all of the duals of these implications.

[David Renshaw]

This took somewhat more copy/pasting than I would like. Probably we should make a tactic or macro to handle this kind of thing more automatically.

[David Renshaw]

side note: the eq4314/eq4606 duality is an interesting one: https://teorth.github.io/equational_theories/implications/?4314

[David Renshaw]

it doesn't just flip the order of the operator -- also the equality flips. I gather that this is an artifact of how we are canonicalizing equations and eliminating duplicates.

[Terence Tao]

This might be a good test case on how to implement equational#147. Is there a specific tactic specification that would have been helpful for you?

[Zoltan A. Kocsis (Z.A.K.)]

Progress report: Okay, I couldn't find one single patched countermodel to refute all the potential implications from 1701.
However, I was able to make do with 3 different ones which together cover them all. I'll put them in Lean shortly.

Constructing the right patch to refute 1701->4587 was the most difficult by far, took me a solid 3 hours. But that's another 13 unknowns down, and is also sufficient to conclude that 1167 does not imply 1701.

[Daniel Weber]

Zoltan A. Kocsis (Z.A.K.) said:

Good news: it looks like this construction will prove a bunch of other anti-implications too.
I'll have to check the details in the morning but I think I have a patched countermodel to 1701 -> 8.

Do you think these patched countermodels can be searched for automatically? What kind of operations are used for the infinite part?

[Zoltan A. Kocsis (Z.A.K.)]

@Daniel Weber I don't know yet, for the simple reason that I deliberately looked for equations which looked like 1661, since the same absic infinite models work for them. I started by looking at the unknows of the smallest equations, and hit jackpot at 8. I think it can be tested whether _this_ particular infinite model works for any other implications but I don't know since I didn't have to look hard yet.

[Zoltan A. Kocsis (Z.A.K.)]

As for the patching itself:

one starts with an infinite model of the antecedent, adjoins (or changes, depending on one's perspective; I've been thinking about it as adjoining during the construction, but writing up my proofs from the changing perspective, it's closer to the truth) a counterexample to the consequent. Then one has to determine how the adjoined elements interact with the original ones. In general this is an infinite amount of work but I could make use of the structure of the initial models, which defined the operation by taking equivalence classes mod 2, to kill infinite classes of antecedent counterexamples at once.

[Zoltan A. Kocsis (Z.A.K.)]

In principle, I think this is combinatorial work that can be auttomated but I doubt it's worth the effort until we see whether @Bhavik Mehta 's confluent extension methods can settle all remaining implications or not.

[Zoltan A. Kocsis (Z.A.K.)]

I've been giving some though to a general characterization of magmas on which patching will work, but don't have anything definitive yet.
My starting point is that in a patching candidate for each $z$ there is a small set $L(z)$ so that if $x \diamond y = z$ then $x \in L(z)$ or $y \in L(z)$, but I can't tell whether this'll be necessary or sufficient. Probably not.

[Zoltan A. Kocsis (Z.A.K.)]

Okay, PR#557 is up for the implications of the form 1701 -> ...

[Shreyas Srinivas]

For the counterexamples, I think you might be able to benefit from the split tactic if you use if then else

[Zoltan A. Kocsis (Z.A.K.)]

Okay, I think the modified translation-invariant magma technique will apply to four more equations using the same base model: these are 1659, 2460 and their duals.

[Zoltan A. Kocsis (Z.A.K.)]

The case of 2460 is much more interesting, in that it has a fairly different structure from the other cases I solved so far (whereas 1659 is very similar). But 1659 has more bang for buck, more implications to refute.

[Zoltan A. Kocsis (Z.A.K.)]

That's potentially still 90 more unknowns (plus whatever else transitivity would then settle), but then I'll have to either

1. come up with some more interesting examples of base models on which I can make this technique work; or
2. get a more general understanding of when and why patching works; or
3. accept that this method has run out of steam.

[Terence Tao]

It might be worth writing up some notes on this approach as a chapter to the blueprint describing the general method, giving some examples, and recording some of your empirical observations on what type of patching constructions seem to work well and what types don't. This may help other contributors find ways to adapt the method.