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 executable's environment reuses, instead of repeating, a library environment's replay of a 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.

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 is Regula.Checker.Policy.editor_decision_pending.