Anthony Bordg (Jul 03 2019 at 16:58): Anthony Bordg (Jul 03 2019 at 16:58):@Hanna Lachnitt is working on the Deutsch-Jozsa algorithm.
Hanna Lachnitt (Aug 23 2019 at 17:17):@Yijun He I now its a long shot but have you have you already proven anything about the parity of a number in relation to bin_rep? In particular, I want to show that if the kth position in the binary representation is 0, then the result of the division I of this number by 2^(m-k) is even where m is the total number of bits. (Intuitively this is clear, if we cut off the bit after k digits and the last one is 0 then the resulting number is even)
Yijun He (Aug 24 2019 at 00:47):Not yet, but I have proved something similar: select_index_div_2 in my Quantum_Fourier_Transform.thy shows that only the last bit of select_index is cut off when we divide a number by 2, and select_index_eq_bin_rep in the same file shows that select_index is exactly the same as bin_rep (except one gives booleans, and the other give 1 and 0s). Therefore the method in select_index_div_2 might also help prove parity results about bin_rep.
Anthony Bordg (Aug 24 2019 at 09:16):Not yet, but I have proved something similar:
select_index_div_2in myQuantum_Fourier_Transform.thyshows that only the last bit ofselect_indexis cut off when we divide a number by 2, andselect_index_eq_bin_repin the same file shows thatselect_indexis exactly the same asbin_rep(except one gives booleans, and the other give 1 and 0s). Therefore the method inselect_index_div_2might also help prove parity results aboutbin_rep.
select_index_div_2 is in Measurement.thy
Hanna Lachnitt (Aug 24 2019 at 09:26):Great thanks a lot. I guess with a little induction this should help me a lot. Also that select_index bin_rep thing is something I was thinking of proving at some point :D
Anthony Bordg (Oct 14 2019 at 16:13):@Yijun He @Hanna Lachnitt
PR #19 and #20 have been merged.
The master branch has been tidied up.
Next is Hanna's Qft.
Last updated: Nov 02 2025 at 16:23 UTC