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.

The axioms of each owned declaration that the foundation rules (RG1001 to RG1005) read are computed in the replayed kernel: those reached through the types and values of the constants it uses and the constructors of each inductive type. Lean records a table of axioms for each module when it is compiled, and collectAxioms reads it for an imported declaration. Each step of collectAxioms is a step of that computation, so a table computed from the replayed constants records no axiom the declaration does not reach. Admission therefore reports here, with impact incomplete, a declaration for which collectAxioms reports such an axiom, and names the declaration and the two axiom sets. A table that omits an axiom is reported, not failed: it is no finding, since Lean's own computation of a table can omit axioms reached through an inductive type's constructors (RG1005), and the rules decide on the replayed axioms. A project audit counts such declarations in its summary (axiom tables:), and its --verbose line of each, the JSON report and the self-audit give the two sets and the omitted axioms.

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). A function with such a result is shared only where each side reaches it. So where one side is read completely and reaches none, nothing can be shared, and the editor gives no notice. It gives the notice where it searches the two sides, finds no shared function with such a result (RG1009), and one of two cases holds. Each side reaches an imported constant, a function or not, whose value the search of that side would read and the file does not have. Or one side reaches one, and the other side reaches a function with such a result that RG1009 counts. 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.

The axioms the foundation rules read for each owned declaration are exactly those it reaches in the replayed kernel, and no axiom that collectAxioms reports for it is outside them; each axiom it omits is reported. An unsafe or partial declaration, which replay does not check, is read as the audited environment keeps it.

Proved about the executed definitions: the axioms computed for a declaration are exactly those it reaches among the constants the search reads (KernelAxioms.axiomTable_some, KernelAxioms.ReachesAxiom), and the account's count of omissions is exactly the inventory's declarations that record one (Account.checked_account).

It does not establish:

• Imported dependencies that the audit does not own, those outside the root package's Git work tree, are not replayed; they remain the declared trusted base, and the account names each of them. The axioms a declaration reaches through them are read from their constants as imported.

• Modules under the checker's reserved prefixes (Regula, RegulaPolicy) in an owned path dependency are the checker's own code, whose source is the checker's own text: the audit does not inspect them and replays one only where it imports a replayed module, so the account names the dependency that provides them among the trusted dependencies.

• 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/RegulaPolicy/KernelAxioms.lean, lean/Regula/Checker/SourceAudit.lean, lean/Regula/Checker/SourceBinding.lean

Proved linkage

Acceptance side only: an accepted run satisfies RegulaPolicy.AdmissionOK. Admission runs three registered decisions: Admission.checkHeader (checked_checkHeader, two-way), Admission.admitReplay (admitReplay_eq_ok, checked_admitReplay, one-way) and Admission.checkTable (checked_checkTable, two-way), and mem_required states the required keys. These theorems are about the request that the decisions take. The module data, the replay set, the reported and reused modules, the lookup kept, the import of the replay base, shared and the replayed kernel are observed or trusted, as the section "Receipt validation: decisions and observing pass" of the guide of proofs and boundaries says. 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.