Lemmas

[ndattani]

• [x] In the newest version, two Lemmas have red font to indicate that Tin had them marked as having bit flipping in a yellow LyX note, but did not have them listed as needing bit flipping in the part outside of the LyX note (i.e. the part that counts). Do these need bit flipping?
• [x] Do we really need the new Lemma 2, now that we have the table? It would be nice to simplify the proof down to as few lemmas as possible. Ideally it would just be 1 theorem, or if not possible, then 2-3 Lemmas. We can have 5-6 Lemmas if necessary, but I prefer 5 instead of 6, if possible.
• [x] What is the logic behind where the horizontal lines are placed in the Table? At first it looks like it's categorized in terms of how many coefficients appear in the last column, because the cases with 4 coefficients in the last column, and 3 coefficients in the last column, both are in their own sections. But then for the cases with 2 or 1 or 0 coefficients in the last column, they are not separated in the same way.

[agu1729]

1) Yes, they need bit flipping. I have filled in the table accordingly and removed the yellow LyX notes. We might also need to write down the effect of flipping one bit , because currently Lemma 0 only deals with flipping two bits. We write this as a comment after the Lemma with all negative coefficients because this is the only quadratisation on which we need to flip an odd number of bits.

2) At first I proved the two lemmas in completely different ways and so preferred keeping them separately. Now I see that although the proof for Lemma 2 is more complicated, it can be modified so that it also works for Lemma 1, so we can merge them with no problem. I am updating the proof in my tex file.

I have changed the lemma numbers after merging and the table is updated accordingly.

3) Sorry about that. I do not intend to place the horizontal lines at all and they might be there due to my copy-and-paste error when I was adding rows to the table. I have now edited them so that the table is categorised in terms of the number of coefficients appearing in the last column.

[ndattani]

• [x] Yes I had also noticed yesterday that one of the table entries said 3 bits should be flipped, not 2 or 4, but I forgot to write that down. So the lemma for 1 bit-flip may be another action item for you.
• [x] I see. So the lemma formerly known as "Lemma 2" was more complicated to prove, but once that proof is done, it also covers Lemma 1. Then we only need one lemma, but in the proof of that lemma we can certainly have two parts: (1) conditions of Lemma 1 + simple roof, (2) more general conditions covering both Lemma 1 and former Lemma 2 + complicated proof. It's up to you if you think this would be valuable to have the simple proof in there as well as the complicated one. I usually prefer "more" rather than "less", but your time is very valuable, and it's up to you if you think this would be worth doing.
  • [x] Thanks for fixing the horizontal lines.
  • [x] Check to see that no more of the Lemmas are "redundant". Maybe write a very short script that tries to do bit flipping for every possible type of bit flip: (b1 & b2), (b1 and b3), (b1 and b3 and b4) etc.... , and see if any combination of bit-flips leads to any of the lemmas having the same formula!
  • [ ] In the table, the FIRST time Lemma 2 appears, it is already saying "bits flipped: b4". Same with Lemma 3 and 4. It is a bit odd that bits are being flipped for the FIRST case. Ideally the first case would be proven, and then all future cases can be obtained by bit flipping. I guess the reason for this, was that it was easiest to PROVE these 3 lemmas based on certain conditions on the alphas ?? Is much harder to prove these Lemmas with other conditions? Maybe there's some conditions that make the Lemmas even simpler to prove?

[agu1729]

1) Sure, I shall do this. 2) Now there is no need for two proofs. Actually the proof is not enlightening so I do not think we need to do both. The simple proof starts with the line "By symmetry WLOG b1<=b2<=b3<=b4" while the complicated proof starts with the line "By symmetry WLOG b2<=b3<=b4" (because the former Lemma 2 has less symmetry) and then both proofs go on to check all possible cases: 5 for the simple proof (0000, 0001, 0011, 0111, 1111) and 8 for the complicated proof (b1 can be 0 or 1 and b2b3b4 can be 000, 001, 011, 111). The simple proof was in an old version of the tex file but now is removed because we do not need it any more. 4) I think it might be easier to check this by hand. I shall do this. 5) This is because the table is not how we do the casework (please see the beginning 'list of cases' here. The 'first' case does not appear first in the table because the table is sorted by the number of coefficients in each column but this was not how we categorise the cases when we prove the lemma. Other versions of the lemma under bit flipping should have similar difficulty to prove (because we just check all 2^4 = 16 possibilities for b1b2b3b4) and we proved it in the way we have it now because that is how we first came up with it. We do not need to make any changes because the table shows that we have covered all cases.

[ndattani]

Thank you so much Tin. For (3), are you sure it's easier to prove this by hand? Even if you proved it by hand (like you did in your email to me about why 3 and 4 are not equivalent), someone would have to read the proof and think about whether or not they agree with it, whereas a quick script that just prints out all quadratizations for all possible bit flips, would make it very obvious by inspection that two formulas are not equivalent. It would also show us new forms of the quads, which might be useful. Maybe some symbolic computation software like Mathematica, which has the "FullSimplify" function, would do these substitutions and then deal with the expanding and refactoring automatically.

[ndattani]

• [ ] I have now significantly simplified Eqs. 3 and 4 so that they fit on a lot less space. It took me too many hours to do this. Maybe it would have been better to just do FullSimplify[ ] in Mathematica, but I'm not sure if that would have worked. I now think that these two expressions:

can each be combined into single sums. Can you try it Tin? Whether by hand or in Mathematica?

Edit: I have now got the first one combined into one sum:

But I'm sure it can be made much better. The r,s are always opposite of the p,q: so it's like r=(p+2)mod4 and s=(r+2)mod4. I just think that if you look at it, the second person's look at it may help to find something more elegant.

[agu1729]

For (3), we have seen that Lemma 4 and Lemma 5 are not equivalent because they work for cases where the number of cubic coefficients in (-a1234, 0) are different, but this number is invariant under flipping bits.

The same proof can be used to show that no two lemmas are equivalent up to flipping bits. The numbers of cubic coefficients in (-a1234, 0) for cases covered by the lemmas are

Lemma 1: 0 or 1 or 2 or 3 or 4 (but there must be an even number of cubic coefficients on each side of -a1234/2) Lemma 2 (flip one bit): 0 Lemma 3: 2 Lemma 4: 3 or 4 Lemma 5: 4

Since these values are different, we indeed need all five lemmas.

[ndattani]

• [ ] Final forms of all Lemmas should be checked in a program that can be distributed with the paper, so that formulas can always be easily verified.
• [ ] Line 3 of Example 1 contains a b1b2 term, but maybe should not.