partial def: #eval gives 111, but rfl and decide fail. Any checked route without ofReduceBool?

I have a small audit tool, toolchain leanprover/lean4:v4.15.0. The step counter is a partial def, since nobody has a termination proof:

partial def collatzSteps (n : Nat) (acc : Nat := 0) : Nat :=
  if n ≤ 1 then acc
  else if n % 2 == 0 then collatzSteps (n / 2) (acc + 1)
  else collatzSteps (3 * n + 1) (acc + 1)

def withinBudget (n : Nat) : Bool :=
  decide (collatzSteps n ≤ budget)

lake build is clean and #eval Audit.collatzSteps 27 gives 111. But in a separate file:

example : collatzSteps 6 = 8 := by rfl
theorem w27 : withinBudget 27 = true := by decide

Both are rejected. The message says the term does not reduce to the expected value. I suspected the default argument and the Inhabited instance. Writing acc explicitly and adding an instance changed nothing.

native_decide accepts both, but #print axioms then shows Lean.ofReduceBool, which I do not accept.

Two questions:

1. Why can the compiled code evaluate this while the kernel and decide cannot?
2. Is there any way to get a kernel-checked fact about this function, short of rewriting it, for instance with fuel?