Bit gadget isn't formally proven

[kayabaNerve]

I wouldn't be surprised if a formal proof exists as part of the Bulletproofs range proof security proof, yet we should cite it if so.