Re-proving native_decide facts in Lean's kernel: a study of 16 public packages and a converter

Lean's native_decide proves a decidable proposition by running compiled code and records the result as an axiom, which Mathlib forbids and which lake check and Comparator in Lean 4.35, as well as the independent proof checkers, reject. NativeTrust re-proves such recorded facts in Lean's kernel, with only the standard axioms and without editing the projects that contain them. Where a definition blocks kernel evaluation and a version proved equal to it is available, such as a fuel-indexed form of well-founded recursion, the converter evaluates a copy that uses it and proves the copy equal to the original, usually by congruence. Of 52,821 native facts in 16 public packages, 98.0% were converted in our study. Three packages account for most of the facts, and without them the rate is 65.9%. Nearly every converted fact needed nothing beyond plain kernel evaluation. The failures come mostly from string processing at check time and from resource limits, which were usually reached in the converter's own search for ways to split a check rather than in the kernel. For projects that keep the tactic, a single import and a source rewriter remove the native axioms that the kernel can prove within a budget.