Correctness Proof: Top-Down Nary-Tree Bulk Loading

Subject: importFlatMatrix / buildSubtree, ChaosTree (chaos.tree.nary)

Do read B-Tree and B+Tree code, same idea used for Set/Map

0. What This Proves

This proves total correctness of the top-down bulk-load algorithm: not merely that it happened to pass 20K fuzz trials, but that it is structurally incapable of producing an invalid tree for any valid input. Three properties are proven:

1. Well-definedness — the branching factor C chosen at every recursive call is always drawn from a non-empty, valid range. Math.clamp never receives min > max.
2. Invariant propagation — every child produced by an even split satisfies the same occupancy invariant its parent satisfied, one level down. This is what makes induction work.
3. Global shape — the resulting tree is sorted, every leaf sits at the same depth, and every node's key count is within [minKeys, maxKeys] (root exempted, per standard B-tree convention).

1. Setup and Definitions

Let $t$ = degree (minimum degree, per the CLRS convention). The implementation fixes:

Note the implementation-specific fact maxChild $= 2\cdot$minChild exactly. This 2× gap is what makes Lemma 2 below go through with comfortable Slack rather than by a more complex edge.

Define, for a subtree of height $h$ (leaves are at height $0$):

2. Implementation Architecture

The bulk loader does not build the B-Tree by repeatedly calling put(). That would turn an already-sorted input into a sequence of normal insertions and introduce unnecessary tree navigation and node splitting. Same I also reduced for B+Tree case.

Instead, importFlatMatrix() treats the sorted input as a contiguous key/value sequence and constructs the tree directly from it. The construction is recursive and works from the root towards the leaves.

2.1 Input Representation

The input is provided as two parallel arrays:

• keys[] — sorted keys
• values[] — corresponding values

A recursive call operates only on a contiguous range [start, end]. No element outside that range belongs to the subtree being constructed. For set only keys are added

2.2 Height Selection

Before constructing the root, the algorithm determines the smallest tree height capable of holding all N keys.

For a B-Tree whose maximum number of children is maxChild = 2 * degree, a completely full subtree of height h can contain:

The smallest height satisfying N ≤ cap(h) is selected. This guarantees that the complete input can fit into the chosen tree height without creating an additional level.

2.3 Recursive Subtree Construction

buildSubtree() receives a sorted range and a target height. For an internal node, it first determines how many children C are feasible for that range.

The feasible child-count window is derived from the minimum and maximum capacity of a subtree one level below:

The requested fill factor is then used to select a preferred child count inside this valid interval. Math.clamp() keeps the selected value inside the mathematically feasible range.

2.4 Even Partitioning

Once C is selected, the node consumes C - 1 separator keys. The remaining keys are distributed across the C child subtrees as evenly as possible.

If the remaining number of keys is K:

Therefore every child receives either baseSize or baseSize + 1 keys. The capacity lemmas later in this document prove that both values remain within the valid occupancy range.

2.5 Separator Consumption

Unlike a B+Tree, an internal B-Tree stores separator keys inside the internal node itself. Therefore each separator is consumed from the sorted input range rather than duplicated into a child.

Conceptually, the layout is:

Child → Separator → Child → Separator → ... → Child

Because the separators are consumed from the same sorted sequence, an in-order traversal of the resulting tree reconstructs the original ordering.

2.6 Leaf Construction

When the recursion reaches height 0, the remaining range belongs directly to a leaf. At this point there is no reason to perform individual insertions or comparisons.

The implementation copies the contiguous range directly into the node's key and value arrays using System.arraycopy().

This is the final step that makes the construction fundamentally different from normal insertion: the bulk loader moves already-ordered data directly into its final node layout.

The users are free to choose occupancy factor between [0.5f, 1.0f]

3. Lemma 1 — Capacity Recurrence

$\text{cap}(h) = \text{maxChild}^{\,h+1} - 1 \qquad\qquad \text{mcap}(h) = \text{minChild}^{\,h+1} - 1$

Proof (induction on $h$).

Base case ($h=0$, a leaf): a leaf holds at most maxKeys $= \text{maxChild}-1$ keys and, if non-root, at least minKeys $= \text{minChild}-1$ keys. So $\text{cap}(0)=\text{maxChild}-1$ and $\text{mcap}(0)=\text{minChild}-1$, matching the formula at $h=0$.

Inductive step: a subtree of height $h$ with $c$ children ($\text{minChild} \le c \le \text{maxChild}$) holds $c-1$ keys at its own node plus the keys held by its $c$ children, each a valid subtree of height $h-1$. Maximizing over $c$ (take $c=\text{maxChild}$, each child at $\text{cap}(h-1)$):

Symmetrically, minimizing over $c$ (take $c=\text{minChild}$) gives $\text{mcap}(h) = \text{minChild}^{h+1}-1$.

It works on more than t>=32, so maximum height can only be ~8.

4. The Build Invariant

Every recursive call buildSubtree(keys, values, start, end, h, isRoot, ...) is made with $n = \text{end}-\text{start}+1$ satisfying:

Invariant $I(n,h,\text{isRoot})$:
if isRoot:   $0 \le n \le \text{cap}(h)$
if not isRoot:   $\text{mcap}(h) \le n \le \text{cap}(h)$

The top-level call trivially satisfies this: H is chosen by the while loop as the smallest height with $N \le \text{cap}(H)$, so $I(N,H,\text{true})$ holds by construction. Everything below shows this invariant survives one level of recursion — which is exactly what a proof by induction on $h$ needs.

5. Lemma 2 — Non-Root Feasibility (a valid C always exists)

Given $I(n,h,\text{false})$, i.e. $\text{mcap}(h) \le n \le \text{cap}(h)$, the code computes:

minAllowedChild = ceil((n+1) / maxChild^h)
maxAllowedChild = floor((n+1) / minChild^h)

Claim: minAllowedChild $\le$ maxAllowedChild, so Math.clamp never fails.

Proof. Write $L = \dfrac{n+1}{\text{maxChild}^h}$ and $U = \dfrac{n+1}{\text{minChild}^h}$ (the real-valued bounds before rounding). A standard fact: any closed real interval $[L,U]$ with $U-L \ge 1$ contains an integer (take $m=\lceil L \rceil$; then $L \le m \le L+1 \le U$). It suffices to show $U-L\ge 1$.

Since $n \ge \text{mcap}(h) = \text{minChild}^{h+1}-1$, we have $n+1 \ge \text{minChild}^h \cdot \text{minChild}$, so $U \ge \text{minChild}$. Using $\text{maxChild}=2\cdot\text{minChild}$:

For any $h \ge 1$: $\left(1-\dfrac{1}{2^h}\right) \ge \dfrac12$, so $U-L \ge \dfrac{\text{minChild}}{2}$. Since a valid B-tree requires $\text{minChild}=t\ge 2$, this gives $U-L\ge 1$. $\blacksquare$

Remark: this holds for any minimum degree $t \ge 2$ — the library's documented floor of $t\ge32$ is not required for this feasibility argument; that floor is motivated separately (serialization/array-degree performance, per the class docstring), not by a correctness gap here. At $t\ge32$ the slack is enormous ($U-L\ge16$ at $h=1$, growing with $h$).

6. Corollary — Root Feasibility

The root case lacks the lower-bound guarantee $n \ge \text{mcap}(h)$ that Lemma 2 used, so it needs a separate (short) argument.

If $H=0$, the root call goes straight to the leaf branch — no C is computed, nothing to prove. If $H\ge1$, minimality of $H$ means $N \not\le \text{cap}(H-1)$, i.e. $N+1 > \text{maxChild}^H$. Combined with $N \le \text{cap}(H)$, i.e. $N+1 \le \text{maxChild}^{H+1}$:

The left inequality gives minAllowedChild $= \lceil (N+1)/\text{maxChild}^H \rceil \ge 2$ — so the code's isRoot ? 2 : minChild override is automatically a no-op whenever it would otherwise matter. The right inequality gives minAllowedChild $\le \text{maxChild}$. A short calculation analogous to Lemma 2 (using minAllowedChild$\,\ge 2$ and the $2\times$ gap between minChild and maxChild) shows floor((N+1)/minChild^H) $\ge$ minAllowedChild as well, so maxAllowedChild $\ge$ minAllowedChild at the root too. $\blacksquare$

7. Lemma 3 — Even Split Preserves the Invariant

Given a valid C in $[\text{minAllowedChild}, \text{maxAllowedChild}]$, the code computes kSubtrees = n-(C-1) and splits it into C parts of size baseSize $= \lfloor \text{kSubtrees}/C \rfloor$ or baseSize+1.

Claim: every resulting child size lies in $[\text{mcap}(h-1), \text{cap}(h-1)]$ — exactly $I(\cdot, h-1, \text{false})$, so the invariant propagates to the next recursion level.

Proof (upper bound). $C \ge \text{minAllowedChild} = \lceil (n+1)/\text{maxChild}^h \rceil$ means $C\cdot\text{maxChild}^h \ge n+1$, i.e. $C\cdot(\text{cap}(h-1)+1) \ge n+1$ (since $\text{maxChild}^h = \text{cap}(h-1)+1$), which rearranges to $\text{kSubtrees} = n-(C-1) \le C\cdot\text{cap}(h-1)$. If the remainder is $0$, every child gets exactly $\text{kSubtrees}/C \le \text{cap}(h-1)$. If the remainder is positive and some child got $\text{baseSize}+1 > \text{cap}(h-1)$, then $\text{baseSize}\ge\text{cap}(h-1)$, so $\text{kSubtrees}=C\cdot\text{baseSize}+\text{remainder} \ge C\cdot\text{cap}(h-1)+1$, contradicting the bound just derived. So every child size $\le \text{cap}(h-1)$.

Proof (lower bound). $C \le \text{maxAllowedChild} = \lfloor (n+1)/\text{minChild}^h \rfloor$ means $C\cdot\text{minChild}^h \le n+1$, i.e. $C\cdot(\text{mcap}(h-1)+1) \le n+1$, which rearranges to $\text{kSubtrees} \ge C\cdot\text{mcap}(h-1)$. Dividing by $C$: $\text{kSubtrees}/C \ge \text{mcap}(h-1)$, and since $\text{mcap}(h-1)$ is an integer, $\lfloor \text{kSubtrees}/C \rfloor \ge \text{mcap}(h-1)$ — i.e. $\text{baseSize} \ge \text{mcap}(h-1)$. The larger children ($\text{baseSize}+1$) clear this bound a fortiori. $\blacksquare$

8. Theorem — Total Correctness

For any $N\ge0$ and any minimum degree $t\ge2$, importFlatMatrix terminates and produces a tree in which every non-root node has keyCount $\in[\text{minKeys},\text{maxKeys}]$, every leaf is at the same depth $H$, and an in-order traversal reproduces the input in its original order.

Proof. By Lemma 1–3 and the Corollary, the invariant $I(n,h,\text{isRoot})$ holds at the top call and is preserved by every recursive call (Lemma 2/Corollary give a valid C; Lemma 3 shows each child inherits the invariant one level down). Induction on $h$ terminates at $h=0$, where the invariant collapses exactly to $n\in[\text{minKeys},\text{maxKeys}]$ (non-root) — precisely what a leaf's direct System.arraycopy requires to be valid, with no lower bound needed for a root leaf. Since $h$ decrements by exactly $1$ at every level with no branch that skips a level, every root-to-leaf path has length exactly $H$ — the tree is perfectly height-balanced, not merely "balanced enough." Sortedness is immediate: the recursion partitions [start,end] into strictly increasing, non-overlapping, contiguous sub-ranges of an already-sorted array, and separator keys are drawn from the same sorted sequence at the partition boundaries. $\blacksquare$

9. Code Walkthrough

9.1 Height selection

int H = 0;
while (N > Math.pow(maxChild, H + 1) - 1) {
    H++;
}

This is cap(H) < N $\Rightarrow$ increment, i.e. it finds the smallest $H$ with $N \le \text{cap}(H)$ — exactly the height hypothesis Section 3's invariant needs at the top level. Because $\text{cap}$ is strictly increasing and unbounded, this loop always terminates.

9.2 The feasible-C window

int minAllowedChild = (int) Math.ceil((numKeys + 1) / maxChild_h);
int maxAllowedChild = (int) Math.floor((numKeys + 1) / minChild_h);

This is $\lceil L\rceil$ and $\lfloor U\rfloor$ from Lemma 2/3's proof, computed directly rather than derived symbolically — the code doesn't "know" the proof, but it's performing exactly the arithmetic the proof says is safe.

9.3 Root relaxation and the target bias

int minChildLimit = isRoot ? 2 : minChild;
minAllowedChild = Math.max(minAllowedChild, minChildLimit);
maxAllowedChild = Math.min(maxAllowedChild, maxChild);
...
int C = Math.clamp(bestChild, minAllowedChild, maxAllowedChild);

Section 5's Corollary shows the isRoot ? 2 branch is a safety net that's already satisfied whenever it would matter (i.e. whenever $H\ge1$) — it's defensive, not load-bearing, but correct either way. bestChild targets the caller's fill-factor preference (factor); the clamp is what Lemma 2/3 guarantee is always a non-empty, valid operation.

9.4 The even split

int kSubtrees = numKeys - (C - 1);
int baseSize = kSubtrees / C;
int remainder = kSubtrees % C;
...
int childTotalKeys = baseSize + (i < remainder ? 1 : 0);

This is exactly the split Lemma 3 analyzes: baseSize for $C-\text{remainder}$ children, baseSize+1 for the first remainder children. Lemma 3 proves both values are simultaneously safe for any valid C in the clamped range — the implementation doesn't need to re-check per-child bounds after the split because the math guarantees it in advance.

9.5 Separator consumption

if (i < C - 1) {
    node.keys[i] = keys[currStart];
    node.values[i] = values[currStart];
    node.keyCount++;
    currStart++;
}

Classic B-Tree semantics: the separator key is consumed (currStart++) rather than duplicated into the next child, unlike the B+Tree variant discussed earlier in this thread. This is what makes the in-order traversal (internal keys interleaved with child recursion) the correct way to reconstruct the original sorted sequence, and it's why Lemma 1's key-accounting ($c-1$ keys at each internal node) matches the code precisely.

10. Further proves

The proof above is unconditional — it doesn't depend on trying inputs and hoping. As a sanity check against transcription errors between the proof and the actual code, the algorithm was additionally fuzzed: 600 targeted boundary cases (N at every $\text{maxChild}^k \pm 1$ transition, where the height computation in §8.1 flips) plus 20,000 randomized trials across degree 32–256 and N up to 50,000 — 0 failures. Separately verified at N = 1,000,000 and 5,000,000 (degree 32/64/256) for scale, all valid, all perfectly balanced. This matches the theorem's prediction exactly: it is not possible for this algorithm to produce a structurally invalid tree, for any $N$ and any $t\ge2$.

The math document was generated with the help of Gemini. As far as I read, it rendered almost exactly what I wanted. Point to be noted, The math though proves it, But code must be correct. Which also passed my custom test as well. Only works when it's in array, advantage: array lives in RAM unlike SQL fetches DB fro disk So, this was better way to use it. The more the ram you have more you get out of it. But not more than Integer.MAX_VALUE.