Introduction

The Binary Indexed Tree (BIT), also known as the Fenwick Tree, stands as one of the most elegant data structures in computer science for efficiently handling prefix sum queries and point updates. Despite its widespread adoption in competitive programming and practical applications, understanding why this structure works correctly requires a rigorous mathematical examination. This article presents a comprehensive proof of the Binary Indexed Tree's correctness, focusing on the fundamental properties of the lowbit operation that makes this data structure possible.

The Binary Indexed Tree Template

Before diving into the proof, let us establish the standard implementation that will serve as our reference throughout this analysis. The following code represents the canonical Binary Indexed Tree template used in our correctness verification:

void add(int x, int k) {
    for (; x <= n; x += lowbit(x)) {
        tree[x] += k;
    }
}

int query(int x) {
    int res = 0;
    for (; x; x -= lowbit(x)) {
        res += tree[x];
    }
    return res;
}

In this implementation, the add function updates the tree by adding value k to position x and all relevant parent nodes. The query function computes the prefix sum from index 1 to x by accumulating values from the appropriate tree nodes.

Problem Statement and Definitions

To formalize our proof, we introduce the following definitions and notation:

  • Let A denote the index of the value being inserted into the Binary Indexed Tree (the tree array)
  • Let B denote the index we intend to query for the prefix sum
  • Both A and B are strictly positive integers (A ≠ 0 and B ≠ 0)

We define two auxiliary functions:

  • P(x, y): A function representing the result of incrementing x by its lowbit value y times (self-increment operation)
  • M(x, y): A function representing the result of decrementing x by its lowbit value y times (self-decrement operation)

The Core Theorem

The correctness of the Binary Indexed Tree hinges on proving the following fundamental properties:

Property 1: No Over-Counting for Larger Indices

When A > B, for all non-negative integers y₁ and y₂, the following holds:

$$\forall y_1, y_2 \geq 0, \quad P(A, y_1) \neq M(B, y_2)$$

This property ensures that when querying the prefix sum up to index B, any values inserted at indices greater than B will never be included in the computation. This is crucial for maintaining the accuracy of prefix sum queries.

Property 2: Exact Counting for Valid Indices

When A ≤ B, there exists exactly one pair of non-negative integers (y₁, y₂) such that:

$$P(A, y_1) = M(B, y_2)$$

This property guarantees that every value inserted at an index less than or equal to B will be counted exactly once in the prefix sum query. This ensures completeness without duplication.

Intuitive Interpretation

In practical terms, these properties ensure that when computing the prefix sum for index B:

  • Values inserted at indices greater than B are never included in the result
  • Values inserted at indices less than or equal to B are included exactly once

This behavior is precisely what we expect from a correct prefix sum data structure.

Fundamental Property of the Lowbit Operation

To prove the core theorem, we must first understand a critical property of the lowbit operation in binary representation.

The Binary Transformation Property

When a number undergoes repeated lowbit increment operations:

  • When a bit at position i changes from 0 to 1, all bits at positions less than i become 0
  • During the increment process, every bit that is 1 (except the leftmost) will eventually become 0

Conversely, when a number undergoes repeated lowbit decrement operations:

  • When a bit at position i changes from 1 to 0, all bits at positions less than i become 0
  • During the decrement process, every bit that is 1 will eventually become 0

Illustrative Example

Consider the binary number 1011000 (which equals 88 in decimal):

  • Its lowbit value is 0001000 (8 in decimal)
  • After one lowbit increment: 1011000 + 0001000 = 1100000 (96 in decimal)
  • Notice that bit position 5 (counting from right, 0-indexed) changed from 0 to 1
  • All bits to the right of position 5 became 0

This property is fundamental to understanding why the Binary Indexed Tree traversal patterns work correctly. The proof of this property follows directly from the definition of lowbit as x & (-x), which isolates the rightmost 1-bit in the binary representation.

Proof of the Core Theorem

Case 1: A > B (Indices Greater Than Query Range)

Claim: When A > B, for all y₁, y₂ ≥ 0, we have P(A, y₁) > M(B, y₂).

Proof:
Since the lowbit operation always produces a positive value (lowbit(x) > 0 for all x > 0), the function P(A, y₁) is strictly non-decreasing with respect to y₁, and M(B, y₂) is strictly non-increasing with respect to y₂.

Given that A > B initially:

  • P(A, 0) = A > B = M(B, 0)
  • For any y₁ > 0: P(A, y₁) ≥ A > B ≥ M(B, y₂) for any y₂ ≥ 0

Therefore, the traversal paths of the update operation (starting from A) and the query operation (starting from B) never intersect when A > B. This proves that values inserted at indices greater than the query index will never contribute to the query result.

Case 2: A = B (Exact Index Match)

Claim: When A = B, P(A, y₁) = M(B, y₂) if and only if y₁ = 0 and y₂ = 0.

Proof:
Since lowbit is strictly positive for all positive integers:

  • For any y₁ ≥ 1: P(A, y₁) > A
  • For any y₂ ≥ 1: M(B, y₂) < B

Given A = B:

  • When y₁ = 0 and y₂ = 0: P(A, 0) = A = B = M(B, 0) ✓
  • When y₁ ≥ 1 or y₂ ≥ 1: P(A, y₁) > A = B > M(B, y₂) ✗

This demonstrates that when the update index exactly matches the query index, the value is counted exactly once (at the initial position before any traversal).

Case 3: A < B (Indices Within Query Range)

Claim: When A < B, there exists exactly one pair (y₁, y₂) such that P(A, y₁) = M(B, y₂).

Proof:

Let us represent A and B in binary form:

  • A = Σᵢ₌₀ⁿ aᵢ × 2ⁱ where aᵢ ∈ {0, 1}
  • B = Σᵢ₌₀ⁿ bᵢ × 2ⁱ where bᵢ ∈ {0, 1}

In binary notation:

  • A = (aₙaₙ₋₁...a₂a₁a₀)₂
  • B = (bₙbₙ₋₁...b₂b₁b₀)₂

Since A < B, there must exist a position j such that:

  • aⱼ = 0 and bⱼ = 1
  • For all positions k > j: aₖ = bₖ

Now, consider the lowbit increment operation on A:

  • By the fundamental property of lowbit established earlier, there exists some y₁ such that after y₁ lowbit increments, position j in A changes from 0 to 1
  • At this point, all positions less than j become 0
  • The resulting value A' = P(A, y₁) has the form where bit j is 1 and all lower bits are 0

Similarly, for B undergoing lowbit decrement:

  • There exists some y₂ such that after y₂ lowbit decrements, we reach a value B' = M(B, y₂) where bit j is 1 and all lower bits are 0
  • Since bits above position j are identical for both A and B, the traversal will converge at the same value

Therefore, there exists a unique meeting point where P(A, y₁) = M(B, y₂), ensuring that the value inserted at index A is counted exactly once in the prefix sum query for index B.

Conclusion

Through this rigorous mathematical analysis, we have established the correctness of the Binary Indexed Tree data structure. The proof demonstrates that:

  1. Soundness: Values at indices greater than the query range never contaminate the prefix sum result
  2. Completeness: Every value at indices within the query range contributes exactly once to the result
  3. Efficiency: The lowbit-based traversal ensures O(log n) time complexity for both update and query operations

The elegance of the Binary Indexed Tree lies in its use of binary representation properties to achieve efficient prefix sum computation. The lowbit operation serves as the key mechanism that enables the tree structure to implicitly encode the necessary aggregation relationships without explicit tree pointers.

This proof not only validates the correctness of the Binary Indexed Tree but also provides insight into why this data structure is both efficient and reliable for a wide range of applications, from frequency counting to range sum queries in competitive programming and database systems.

Summary

The Binary Indexed Tree's correctness fundamentally relies on the mathematical properties of binary number representation and the lowbit operation. By proving that update and query traversals intersect exactly when the update index is within the query range, we establish the theoretical foundation for this widely-used data structure's reliability and efficiency.