9.1 What Lean accepts

This repository is pinned to Lean 4.32.0. For a closed proposition \(P\), the current native_decide implementation compiles and evaluates the Boolean Decidable.decide P. When the executable result is true, Lean adds a fresh auxiliary axiom

and the ordinary theorem of_decide_eq_true derives \(P\). This is the behavior documented in the pinned Lean implementation and in Lean’s trusted-code-base guidance.

The kernel checks the type of the auxiliary axiom and every theorem-level step from that equality to the mathematical consumer. It does not replay the native execution that supplied the equality. Consequently the compiler, runtime, code-generation backend, linked executable implementations, and platform enter the trusted base for these leaves. The fact that Lean records the generated declaration as a logically usable, non-unsafe axiom is not a certificate that its proposition is true. In particular, a successful independent kernel checker can check the proof only relative to these explicit axioms; it cannot reconstruct their native executions from the proof objects alone.

Here a native-decision certificate therefore means three distinct pieces:

1. a closed, inspectable finite predicate \(P\);

2. an ordinary Lean soundness theorem saying that \(P\) implies the paper-facing mathematical claim; and

3. a compiler-trusted assertion that Decidable.decide P returned true.

Only the first two pieces are kernel-checked in the usual proof-producing sense. Replacing the third with ordinary reduction or a proof-producing certificate is the native-retirement step.