Unfortunately (like many other authors) Fenwick does a very bad job of explaining his work (the Binary Indexed Tree) in the original text. The paper lacks a proper formal proof of why this structure should work and only provides examples. This seems to be a very widespread issue regarding this topic and no tutorial or blog post out there seems to prove the correctness of this beast.
Just to be clear, I'm not looking for intuition or an explanation of how this data structure works, I already know that, what I am asking for is a formal proof that says a tree built this way will do what it is supposed to do correctly.
There is already another question here, with a very detailed and well-written answer that still doesn't provide a proof (though the question didn't really ask for proof either) and also seems to rely on a logic much different from what is presented in the original paper so please do not mark this as a duplicate.