Module native_decide 

native_decide, re-proved by the LOGOS kernel’s own evaluation.

Lean’s proof

Lean 4.14.0 closes a closed decidable goal p with native_decide in two declarations (Lean.Elab.Tactic.evalNativeDecide):

def     T._nativeDecide_1 : Bool := Decidable.decide p inst
theorem T : p := of_decide_eq_true p inst
                    (Lean.ofReduceBool T._nativeDecide_1 Bool.true (Eq.refl.{1} Bool Bool.true))

Lean.ofReduceBool d b h : d = b is an axiom, and Lean’s kernel accepts Eq.refl b as h : Lean.reduceBool d = b only by running the compiled d: the proof rests on the compiler, and #print axioms names Lean.ofReduceBool.

The re-derivation

The step Lean hands to its compiler is a closed decision, and the LOGOS kernel decides it itself. The leaf is read as

of_decide_eq_true p inst (Eq.refl.{1} Bool Bool.true)

which checks exactly when the kernel converts Bool.true with Decidable.decide p inst: its own reduction and certified accelerations, in the primary kernel and in the independent re-checker. The statement is untouched; the justification of one step changes from Lean’s compiled evaluation to LOGOS’s kernel evaluation, and the result discloses it. A decision the kernel evaluates to Bool.false is a conversion mismatch, and the claim is refused; one it cannot finish within its budget is a resource limit. Neither is ever trusted.

What is a leaf

Structure, never a name alone. An export expression is a leaf when it is of_decide_eq_true p inst (Lean.ofReduceBool d Bool.true (Eq.refl.{1} Bool Bool.true)) and the export declares

• Lean.ofReduceBool as an axiom stating ∀ a b : Bool, Lean.reduceBool a = b → a = b, over an opaque Lean.reduceBool : Bool → Bool;
• of_decide_eq_true as a theorem stating ∀ (p : Prop) (inst : Decidable p), Decidable.decide p inst = true → p, with Decidable.decide : ∀ p : Prop, Decidable p → Bool;
• d as a definition without universe parameters, of type Bool, whose value is Decidable.decide p inst for the same p and inst, expression for expression (binder names and binder annotations aside);
• Bool as an inductive whose constructors are Bool.false and Bool.true, and Eq as an inductive whose one constructor is Eq.refl.

Every other mention of Lean.ofReduceBool is read as exported and rests on the axiom; the assumption policy refuses it.

Where it applies

The LOGOS import surface (import_with, hence the pipeline and the package) reads every leaf of an export this way and lists each re-derivation in its report. The Lean Kernel Arena protocol (check_str, run_cli) reads the export exactly as exported. A package discloses the re-derived leaves of its target’s closure as INFORMATION_CATEGORY information changes, and a replay recomputes that disclosure from the carried export and refuses a package whose manifest does not state it exactly.

Structs

Elimination

What a target’s closure rests on once its leaves are re-derived.

NativeDecision

One recognized leaf: Lean’s appeal to its compiler, and the pieces its re-derivation keeps.

NativeDecisions

The native decisions of one export.

Rederivation

One declaration whose type or value holds re-derived leaves.

Constants

ELIMINATED_AXIOM

The trust escape a re-derived leaf no longer rests on, as Lean’s #print axioms names it.

INFORMATION_CATEGORY

The information-change category a re-derivation is disclosed under.

METHOD

How a disclosed step was re-derived.