Checked example🔗

import Lean
/-! # Reflexivity

Reflexivity declared with unchecked, ill-typed evidence. -/
open Lean Elab Command
set_option debug.skipKernelTC true in
run_cmd liftCoreM <| Lean.addDecl (.thmDecl {
  name := `reflexive
  levelParams := []
  type := mkForall `n .default (mkConst ``Nat)
    (mkApp3 (mkConst ``Eq [Level.succ Level.zero]) (mkConst ``Nat) (mkBVar 0) (mkBVar 0))
  value := mkConst ``True.intro })

[INCOMPLETE[kernel-admission]] while replaying declaration 'reflexive':
(kernel) declaration type mismatch, 'reflexive' has type
  True
but it is expected to have type
  ∀ (n : Nat), Eq n n

- import Lean
- /-! # Reflexivity
- 
- Reflexivity declared with unchecked, ill-typed evidence. -/
- open Lean Elab Command
- set_option debug.skipKernelTC true in
- run_cmd liftCoreM <| Lean.addDecl (.thmDecl {
-   name := `reflexive
-   levelParams := []
-   type := mkForall `n .default (mkConst ``Nat)
-     (mkApp3 (mkConst ``Eq [Level.succ Level.zero]) (mkConst ``Nat) (mkBVar 0) (mkBVar 0))
-   value := mkConst ``True.intro })
+ /-! # Reflexivity
+ 
+ Reflexivity for every natural number. -/
+ theorem reflexive (n : Nat) : n = n := rfl

/-! # Reflexivity

Reflexivity for every natural number. -/
theorem reflexive (n : Nat) : n = n := rfl

The correction replaces ill-typed unchecked evidence with a checked proof of the same reflexivity statement.

Checked by a fresh whole-project audit of <example> (axiomGate): violating run incomplete, corrected run completed.

How to fix it🔗

1. Remove uses of debug.skipKernelTC, addDecl with unchecked values, or other metaprograms that add unchecked declarations; state and prove the theorem normally.

2. Do not edit sources while an audit runs; rerun it.

3. For an editor pending result, run lake lint (or lake lint -- --fresh).

4. Rename an owned declaration that shares its name with another module's constant unless both are theorems of the same statement, universe parameters and mutual block, such as an equation lemma Lean realizes in each module that needs it; admission checks each owned copy that is not identical to the replayed or trusted one.

Why it matters🔗

Successful elaboration alone is not checked admission: metaprograms and debug options can store declarations the kernel never checked. An accepted result must rest on kernel-checked evidence for the exact frozen sources.

What triggers it🔗

Before accepting proof evidence the checker replays every owned logical declaration and its owned dependencies through Lean's kernel (Admission.validate); an environment reuses, instead of repeating, an earlier environment's replay of a claimed library module over the identical import closure and frozen .olean parts (including .olean.private). Each replayed module's own copy of a name is checked: a lemma Lean realizes in two modules, such as an equation lemma, is admitted when the copies are theorems of the same statement, universe parameters and mutual block and each owned copy that is not identical to the replayed or trusted one passes the kernel with a proof that does not reach its own name and reaches the same axioms. A declaration that fails replay, source or .olean bytes that changed after they were frozen, or a required authentication that failed is reported here with impact incomplete.

In the editor, this rule marks results that need fresh evidence only the project command collects, and those messages name lake lint. The editor also reports it, as incomplete, when its own analysis of a declaration fails or the module has elaboration errors.

In a file with a module header, the editor also reports a decision kind as incomplete when its decided function gives the implementation an argument that applies, to the variable of that function, a constant that the environment has only as an axiom. Lean gives such a file an imported theorem in that form, and the projection function of a proof field is a theorem, so the editor cannot tell whether the argument is a field (limitations of RG1007). The message names lake lint, which reads the kind.

In such a file the editor also reports its reading of the functions that the two sides of a decision registration share as incomplete, when a function with a result of Bool or BEq could be shared only below an imported function whose value the file does not have (limitations of RG1009). The message names lake lint, which has each value.

Required proof shape🔗

The replayed declaration must type-check in the kernel with exactly its stated type and value.

What a passing result establishes🔗

Every owned logical declaration and its owned dependencies passed kernel replay (every other copy of a theorem that another loaded module also declares is identical to the replayed or trusted one, or passed the kernel's check under a fresh name with a proof that does not reach its own name and reaches the same axioms), and the frozen sources were unchanged during the audit. A failed admission or changed source is incomplete and never accepted.

It does not establish:

• Imported, unowned dependencies are not replayed; they remain the declared trusted base.

• Incremental admission does not establish fresh source elaboration.

It leaves these review obligations open: R-QUALIFY.

Configuration and exceptions🔗

No option waives admission. A failed generated-role authentication cannot waive RG1001 or RG1006.

Limitations and unsupported cases🔗

This page's example is a diagnostic demonstration: the violating run is INCOMPLETE by design and is not accepted negative evidence. Its corrected counterpart passed a completed positive check.

Sources🔗

Normative clauses

standard §7.3 Clean Elaboration and Diagnostics

Checklist rows

DECL-01, DECL-02, FOUND-05, SCOPE-02, TYPE-01, THEOREM-01, THEOREM-03, THEOREM-07, DECL-03, DECL-04, COMP-02, COMP-04, BUILD-01, BUILD-04

Detector, policy and proof sources

lean/Regula/Checker/Admission.lean, lean/Regula/Checker/SourceAudit.lean, lean/Regula/Checker/SourceBinding.lean

Proved linkage

Acceptance side only: an accepted run satisfies RegulaPolicy.AdmissionOK. The editor's deferral to the project audit of a result that needs generated-role evidence is Regula.Checker.Policy.editor_decision_pending. Its deferral of a decision kind that it does not read is operational collector code (hiddenField? in Regula.Collect), which that theorem does not cover: the collector records the registration with no failure of its kind, so the editor decision reports no RG1007 finding for that record, and the linter reports the reading as incomplete. Its deferral of the shared functions that it does not read is operational collector code too (sharedReading in Regula.Collect): that record names no shared function with a result of Bool or BEq, so the editor decision reports no RG1009 finding for it.