Lesson 08
What the Axeyum Kernel checks
Which judgments belong inside a proof kernel, and which services belong outside it?
The Axeyum Kernel is an independent Rust checker for a selected Lean-core term language. It checks explicit declarations; it does not provide Lean's full interactive environment.
After this lesson, you should be able to
- Describe type checking, reduction, definitional equality, and declaration admission.
- Explain weak head normal form and why full normalization is not always needed.
- State the current boundary between the Axeyum Kernel and Lean.
8.1
The kernel checks terms against types
A declaration supplies a name, a type, and, for a theorem or definition, a term. The kernel checks that the type is well formed and that the term has that type before adding the declaration to its environment.
Later declarations can refer to the accepted name. Their validity then depends on the earlier declaration and on the rules the kernel used to admit it.
8.2
Computation participates in equality
A kernel must recognize that (fun x => x) 3 and 3 are the same by computation. This relation is definitional equality. It follows from reduction and unfolding rules rather than from a separately named theorem.
Weak head normal form, abbreviated WHNF, reduces enough to expose a term's outer shape. If the checker needs to know whether a type is a function, it can stop once the function form is visible instead of reducing every nested expression.
8.3
Declarations expose assumptions
An axiom or opaque declaration has no checked proof body available to the kernel. The environment must therefore treat it as trusted. Dependency analysis can follow references from a theorem and report the trusted declarations it reaches.
An empty axiom footprint describes that dependency walk. It does not establish that the theorem's prose summary is accurate, that imported terms were reconstructed correctly, or that the kernel implementation is bug-free.
8.4
Lean is a reference and import source
The Axeyum Kernel checks selected Lean-core terms, universes, inductive declarations, recursors, reduction, and definitional equality in Rust. It can consume selected exports from Lean, but Lean does not run as the checker for that path.
The kernel has no general Lean elaborator, tactic language, editor integration, or interactive goal state. A comparison with Lean must keep those missing services visible.
Worked example
Check the identity proof
Consider the term fun P => fun h => h with claimed type (P : Prop) → P → P.
- Bind P
The outer function accepts a proposition P.
- Bind h
The inner function accepts h with type P.
- Check the body
The body returns h, which has the required result type P.
- Assemble the type
The inner function has type P → P, and the outer function works for every P : Prop.
Result. The term has the claimed type and proves that every proposition implies itself.
8.5
Check your understanding
Answer each question before opening the explanation.
1 What is the difference between definitional equality and a proved equality theorem?
Definitional equality follows from the kernel's computation rules; a theorem equality requires a proof term.
2 Why is the Axeyum Kernel not a replacement for the Lean user environment?
It checks a selected core term language but lacks Lean's general elaborator, tactics, editor services, and interactive goals.
Concept wiki
Terms in this lesson
- Proof kernel The small part of a proof system that checks declarations and proof terms.
- Reduction Computing a term according to the core language's evaluation rules.
- WHNF A term reduced enough to expose its outermost form.
- Definitional equality Equality determined by the core computation rules rather than by a separate theorem.
- Proof term A term whose type is the proposition it proves.
- TCB The code and assumptions that must be correct for a result to be valid.
- Soundness The property that accepted results are valid under the stated semantics.