partial def: #eval выдаёт 111, а rfl и decide падают. Есть ли проверяемый путь без ofReduceBool?

У меня небольшой аудит-инструмент, toolchain leanprover/lean4:v4.15.0. Счётчик шагов — partial def, потому что доказательства завершения ни у кого нет:

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 проходит чисто, и #eval Audit.collatzSteps 27 выдаёт 111. Но в отдельном файле:

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

Оба варианта отклоняются. В сообщении сказано, что терм не редуцируется до ожидаемого значения. Я подозревал аргумент по умолчанию и экземпляр Inhabited. Явное указание acc и добавление экземпляра ничего не изменили.

native_decide принимает оба, но тогда #print axioms показывает Lean.ofReduceBool, а это мне не подходит.

Два вопроса:

1. Почему скомпилированный код может это вычислить, а ядро и decide — нет?
2. Есть ли способ получить факт об этой функции, проверенный ядром, без её переписывания, например с fuel?