diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean
index 8c0d204..3e0cd9f 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/verification/Proofs/AxiomCheck.lean
@@ -5,6 +5,7 @@ import Proofs.Completeness
 #print axioms LTLAcc.kbelow_pos
 #print axioms LTLAcc.kbelow_lt
 #print axioms LTLAcc.le_two_kbelow
+#print axioms LTLAcc.kbelow_pow2
 #print axioms LTLAcc.MTH
 #print axioms LTLAcc.Root
 #print axioms LTLAcc.ConsRec
diff --git a/verification/Proofs/Basic.lean b/verification/Proofs/Basic.lean
index 0cf4bf1..bce2c64 100644
--- a/verification/Proofs/Basic.lean
+++ b/verification/Proofs/Basic.lean
@@ -57,6 +57,20 @@ theorem le_two_kbelow (n : Nat) (h : 2 ≤ n) : n ≤ 2 * kbelow n := by
       have := ih h2
       omega
 
+/-- `kbelow` is a genuine power of two. Together with `kbelow_lt` and
+    `le_two_kbelow` (`2^j = k < n ≤ 2k = 2^(j+1)`) this pins `kbelow n`
+    as THE largest power of two strictly below `n` — the RFC 9162 split
+    point, uniquely determined. -/
+theorem kbelow_pow2 (n : Nat) : ∃ j, kbelow n = 2 ^ j := by
+  induction n using kbelow.induct with
+  | case1 n hle => exact ⟨0, by rw [kbelow]; simp only [if_pos hle]⟩
+  | case2 n hgt ih =>
+      obtain ⟨j, hj⟩ := ih
+      refine ⟨j + 1, ?_⟩
+      rw [kbelow]
+      simp only [if_neg hgt]
+      rw [hj, Nat.pow_succ, Nat.mul_comm]
+
 /-- `MTH` (paper §5.3): the RFC 9162 tree head over a leaf-data list.
     `MTH [] = H(ε)`, `MTH [d] = hleaf d`, and for `n ≥ 2` the split at
     `k = kbelow n`. -/
diff --git a/verification/Proofs/Basic.olean b/verification/Proofs/Basic.olean
index 932db21..7422fe1 100644
Binary files a/verification/Proofs/Basic.olean and b/verification/Proofs/Basic.olean differ
diff --git a/verification/Proofs/Completeness.olean b/verification/Proofs/Completeness.olean
index 95ee8a9..cb54ae8 100644
Binary files a/verification/Proofs/Completeness.olean and b/verification/Proofs/Completeness.olean differ
diff --git a/verification/check.sh b/verification/check.sh
index 637b463..452c047 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -26,6 +26,7 @@ declare -A CONES=(
   [LTLAcc.kbelow_pos]="propext, Quot.sound"
   [LTLAcc.kbelow_lt]="propext, Quot.sound"
   [LTLAcc.le_two_kbelow]="propext, Quot.sound"
+  [LTLAcc.kbelow_pow2]="propext, Quot.sound"
   [LTLAcc.MTH]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.Root]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.ConsRec]="propext, LTLAcc.sha256, Quot.sound"