IxVM kernel: hot/cold split try_extract_nat — extract App arm

`try_extract_nat` ran 1.12M rows at width 45, charging 2.68% of UTF-8
`_proof_1_8` total FFT. The App arm (list_lookup + address_eq +
recursive try_extract_nat + klimbs_succ) is the widest match arm; the
Lit / Const / default arms are leaf compares.

Factor App into `try_extract_nat_app(f, a, addrs)`. Main extractor
narrows to leaf-arm width. Cold fn only charges App-arm rows.

Measured on UTF-8 `_proof_1_8`:
  37.62B → 37.31B (-0.8%)
  Nat.add_comm unchanged.

Author: arthurpaulino

Ix/IxVM/Kernel/Primitive.lean

@@ -1293,19 +1293,25 @@ def primitive := ⟦
           1 => (1, store(ListNode.Nil)),
           0 => (0, store(ListNode.Nil)),
         },
-      KExprNode.App(f, a) =>
-        match load(f) {
-          KExprNode.Const(idx, _) =>
-            let head_addr_ = list_lookup(addrs, idx);
-            match address_eq(head_addr_, nat_succ_addr()) {
-              1 =>
-                match try_extract_nat(a, addrs) {
-                  (1, pred_limbs) => (1, klimbs_succ(pred_limbs)),
-                  _ => (0, store(ListNode.Nil)),
-                },
-              0 => (0, store(ListNode.Nil)),
+      KExprNode.App(f, a) => try_extract_nat_app(f, a, addrs),
+      _ => (0, store(ListNode.Nil)),
+    }
+  }
+
+  -- Cold-extracted App arm: list_lookup + address_eq + recursive
+  -- try_extract_nat + klimbs_succ is the widest arm; pulling it out lets
+  -- `try_extract_nat`'s main width drop to the leaf-arm width.
+  fn try_extract_nat_app(f: KExpr, a: KExpr, addrs: List‹Addr›) -> (G, KLimbs) {
+    match load(f) {
+      KExprNode.Const(idx, _) =>
+        let head_addr_ = list_lookup(addrs, idx);
+        match address_eq(head_addr_, nat_succ_addr()) {
+          1 =>
+            match try_extract_nat(a, addrs) {
+              (1, pred_limbs) => (1, klimbs_succ(pred_limbs)),
+              _ => (0, store(ListNode.Nil)),
             },
-          _ => (0, store(ListNode.Nil)),
+          0 => (0, store(ListNode.Nil)),
         },
       _ => (0, store(ListNode.Nil)),
     }