The con-leche proof idea

1. Introduction

1.1. What is proved

con-leche is a checker for Lean 4. It reads an export of a Lean environment, the stream: every definition, theorem and inductive type, in the official kernel’s own terms. It accepts or rejects the stream, checking what the official kernel checks (on a few features it declines instead; Section 7). It comes with a proof, written in Lean itself, of what an acceptance means: every environment the checker accepts has a model in set theoryConLeche/MainTheorem.lean:L96-L9996theorem model_exists (V : Type w) [SetTheory V]
97 (pins : List NatOpPinSet) (ds : Array Declaration) (env : Env)
98 (accepted : checkDecls .verified pins ds = .ok env) :
99 Nonempty (Model V env) := by
. Each constant is assigned a setConLeche/Denotes.lean:L269-L289269structure Model (V : Type w) [SetTheory V] (env : Env) where
270 /-- the set a constant denotes, per level assignment -/
271 cval : Name → (LevelParam → Nat) → V
272 /-- every stored constant is a member of what its type denotes, at
273 every level assignment (and every variable environment — the type
274 is closed) -/
275 mem : ∀ c ∈ env.consts, ∀ (φ : LevelParam → Nat) (ρ : BVarIdx → V),
276 ∃ T, Denotes cval env φ ρ c.toConstantVal.type T ∧ cval c.name φ ∈ˢ T
277 /-- whatever the built-in `False` denotes is the empty set -/
278 false_empty : ∀ (φ : LevelParam → Nat) (ρ : BVarIdx → V) (F : V),
279 Denotes cval env φ ρ (.const falseName []) F → F = empty
280 /-- whatever the built-in `Eq` denotes is set equality: at a type `A`
281 of the universe the level `u` names, and two of its members `a` and
282 `b`, `@Eq.{u} A a b` denotes the truth value of `a = b`. The three
283 membership premises are the graph's domains — `Eq`'s denotation is a
284 three-fold graph over `univ (Level.eval φ u)`, then over `A`, then
285 over `A` again, and a graph read off its domain says nothing -/
286 eq_equality : ∀ (u : Level) (φ : LevelParam → Nat) (ρ : BVarIdx → V) (E A a b : V),
287 Denotes cval env φ ρ (.const eqName [u]) E →
288 A ∈ˢ univ (Level.eval φ u) → a ∈ˢ A → b ∈ˢ A →
289 app (app (app E A) a) b = eqv a b
, each type denotes a set, and every stored constant is a member of the set its type denotes. The constant False denotes the empty set, and Eq denotes set equality, so every equation the checker accepts is an equality of sets. Hence no accepted environment holds a proof of False, and every accepted theorem is true in the model.

1.2. The shape of the argument

The theorem is relative to a model of an abstract set theory, a structure with membership, extensionality, the usual set-forming operations and a chain of universes closed under themConLeche/SetTheory/Core.lean:L95-L100 95/-- A model of set theory of exactly the strength the checker needs:
96membership, the six ZF⁻ axioms (extensionality, pairing, union, power
97set, regularity, Lean-level replacement), and an ω-chain of
98Grothendieck universes. Infinity is derivable; choice is inherited
99from the meta-logic (`Classical.choice`); see the module docstring. -/
100class SetTheory (V : Type u) where
. By Gödel’s second incompleteness theorem, Lean cannot prove that such a structure exists. The assumption is standard, though: it follows from the existence of ω many inaccessible cardinals, the hypothesis of the Lean development of Carneiro’s model of Lean (Section 8; §7 of OVERVIEW.md says more).

The usual way to prove such a statement, given a typing judgement for the type theory, has two steps: show that the checker accepts only derivable judgements, and show that derivable judgements are true in the model. The first step needs the metatheory of the type theory: that reduction preserves types (subject reduction), that reduction is confluent, that a function type determines its domain and codomain (injectivity of Π), and that a term has one type up to definitional equality. Our proof needs none of it.

Nor does it have a typing judgement. In its place is a description of what the checker does: three inductively defined relations, one for reductionConLeche/Rules/Rel.lean:L101101inductive Red (env : Env) : Nat → Expr → Expr → Prop where
, one for the verdicts of the definitional-equality testConLeche/Rules/Rel.lean:L358358inductive DefEq (env : Env) : Nat → Expr → Expr → Prop where
and one for type inferenceConLeche/Rules/Rel.lean:L549549inductive Infer (env : Env) : Grade → Nat → Expr → Expr → Prop where
(six in the real proof, where premises about lists get relations of their own; Section 7). Their rules are exactly the moves the checker makes, and each rule’s premises are what the checker verified at that point. On the model side there is a total, term-directed interpretationwhitepaper/Fragment/Interp.lean:L139-L146139noncomputable def interp (M : Name → List Nat → V) (φ : Name → Nat) : (Nat → V) → Expr → V
140 | ρ, .bvar i => ρ i
141 | _, .sort u => typeU (u.eval φ)
142 | _, .const c ls => M c (ls.map (Level.eval φ))
143 | ρ, .app f a => app (interp M φ ρ f) (interp M φ ρ a)
144 | ρ, .lam A b => lamV (interp M φ ρ A) fun x => interp M φ (cons x ρ) b
145 | ρ, .pi A B => piV (interp M φ ρ A) fun x => interp M φ (cons x ρ) B
146 | ρ, .letE _ v b => interp M φ (cons (interp M φ ρ v) ρ) b
: every term denotes a set, well-typed or not, and the interpretation uses nothing beyond what is in the term itself. In particular it uses no typing information, nothing that would have to be inferred. Where a typing judgement would say “this term has that type”, there is a semantic invariantwhitepaper/Fragment/WellDenoted.lean:L58-L7858def WellDenoted : (Nat → V) → Expr → Prop
59 | _, .bvar _ => True
60 | _, .sort _ => True
61 | _, .const _ _ => True
62 | ρ, .app f a =>
63 WellDenoted ρ f ∧ WellDenoted ρ a ∧
64 ∃ (p : Bool) (A : V) (B : V → V),
65 interp M φ ρ f ∈ˢ piR p A B ∧ interp M φ ρ a ∈ˢ A ∧
66 (p = true → ∀ x, x ∈ˢ A → B x ∈ˢ univ 0) ∧ (p = false → IsTy A)
67 | ρ, .lam A b =>
68 WellDenoted ρ A ∧ IsTy (interp M φ ρ A) ∧
69 (∀ x, x ∈ˢ interp M φ ρ A → WellDenoted (cons x ρ) b) ∧
70 ∃ B : V → V,
71 (∀ x, x ∈ˢ interp M φ ρ A → interp M φ (cons x ρ) b ∈ˢ B x) ∧
72 (∀ x, x ∈ˢ interp M φ ρ A → IsTy (B x))
73 | ρ, .pi A B =>
74 WellDenoted ρ A ∧ IsTy (interp M φ ρ A) ∧
75 (∀ x, x ∈ˢ interp M φ ρ A → WellDenoted (cons x ρ) B) ∧
76 (∀ x, x ∈ˢ interp M φ ρ A → IsTy (interp M φ (cons x ρ) B))
77 | ρ, .letE _ v b =>
78 WellDenoted ρ v ∧ WellDenoted (cons (interp M φ ρ v) ρ) b
on the term’s set, imposed at every subterm: every application applies a function to a member of its domain, every binder’s domain is a type, and so on. One induction over the three relationswhitepaper/Fragment/Sound.lean:L2322-L23262322theorem soundness [LevelOracle] (m : EnvModel V env) (φ : Name → Nat) :
2323 (∀ {Γ : List Expr} {e e' : Expr}, Red env Γ e e' → RedSem m φ Γ e e') ∧
2324 (∀ {Γ : List Expr} {a b : Expr}, DefEq env Γ a b → DefEqSem m φ Γ a b) ∧
2325 (∀ {Γ : List Expr} {e T : Expr}, Infer env Γ e T → InferSem m φ Γ e T) :=
2326 ⟨red_sound, defeq_sound, infer_sound⟩
then proves three claims at once. A reduction step preserves the denotation and the semantic invariant; a verdict “definitionally equal” means that the two sides denote the same set; and an inferred type contains the term, that is, the term’s set is a member of the type’s set.

1.3. How to interpret a ∀ or a lambda

At every binder the interpretation has to decide how to interpret a ∀ or a lambda. In Lean, ∀ x : A, B is a type of functions when B is a type and a proposition when B is a proposition, and in the model these are different kinds of sets. A function type is a set of graphs. A proposition is a truth value, a set with at most one element: the model has one distinguished set, the point, which every proof of every proposition denotes, so proof irrelevance is built in. The two cases look the same on the page, and telling them apart by the sort of B would take type inference. Our interpretation instead reads the answer off the valueswhitepaper/Fragment/Lib.lean:L477-L481477/-- **The function space, regime read off the fibres.** -/
478noncomputable def piV (A : V) (B : V → V) : V := piR (propB A B) A B
479
480/-- **The abstraction, regime read off the body values.** -/
481noncomputable def lamV (A : V) (F : V → V) : V := lamR (ptB A F) A F
: a ∀ denotes a truth value exactly when every one of its fibres (the set B denotes at a member of the domain) is a truth value, and a lambda denotes the point exactly when every value of its body is the point. The terms are Lean’s own.

Over a non-empty domain this reading agrees with the sort of the body. Over an empty domain it does not: fun h => h.elim, of type False → Nat, denotes the point although its type has sort Type (Section 2.5). This shapes the soundness claims: a reduction or an equality claims nothing about a term that denotes the point (Section 2.7). It also costs two checks that the official kernel never makes (Section 2.8): the checker compares the types of two bodies at lambda congruence and η, and, in one rare case of ι-reduction, it compares a constructor application with the recursor’s arguments and type-checks its fields.

1.4. This document

This document is a pen-and-paper account of that argument on a simplified fragment of the checker. The fragment has no projections, no number or string literals, no mutual inductive types, nesting only one container deep and not under a binder (Section 5 describes the full check, without proof), no quotients, no axioms, no built-in copies of False, Eq, Nat and their kin (the real checker pins these rather than reading them from the stream), no distinction between a theorem and a definition, and none of the checker’s performance devices (memo tables, fuel, the parallel check phase). Section 7 lists every omission with one sentence on what the real proof does about it. The fragment is verified in Lean in a small development of its own, whitepaper/Fragment/, which imports nothing from the main proof and is parametric in the same kind of abstract set theory. The underlined source links lead into the real proof and into that development.

The rest is in seven parts. §2 presents the fragment without an environment: terms and universe levels, the three relations, the abstract set theory, the interpretation, the semantic invariant, and the three claims with their proof. The routine cases of the proof are listed briefly; the cases where the reading of a binder matters, or where a syntactic proof would fail, are discussed in full. §2 ends with the checks that other checkers skip and with a cheaper mode of inference. The claims (Section 2.7) are a good place to start reading. §3 adds the environment, the constants that refer to it, and its definitions: what is stored, what is checked, how a definition unfolds, and the model that grows with it. §4 adds inductive types as least fixed points in the model, their recursors and reduction rules, large elimination, and the consistency corollary: no accepted environment stores a constant whose type is an inductive proposition with no constructors. §5 changes tack. It describes in full con-leche’s check for nested inductive types, whose constructors mention the type being defined inside another one, as in List (Tree α), and their generated recursors, and only sketches how the model extends to them. §6 shows that two features of Lean’s definitional equality that the fragment drops, η for structures and unit-likeness, follow from the extensionality of the model, with one proof case each. §7 lists what was left out, and how the real proof differs from the fragment where they share a feature. Section 8 relates the argument to earlier work.

2. The fragment without an environment

This section presents the core of the argument on a fragment of Lean without an environment: first the terms, the levels and the three relations that say what the checker does; then the set theory, the interpretation, the semantic invariant that replaces a typing judgement, and the three soundness claims with their proofs. Everything here is verified in the fragment’s own Lean development and linked, alongside its counterpart in the real proof.

2.1. Terms

The terms of the fragment are the official kernel’s terms, minus what Section 7 leaves out:

A termwhitepaper/Fragment/Syntax.lean:L29-L4829/-- Terms. -/
30inductive Expr where
31 /-- A bound variable, by de Bruijn index. -/
32 | bvar (i : Nat)
33 /-- The sort `Sort l`. -/
34 | sort (l : Level)
35 /-- A constant of the environment at a level instantiation. -/
36 | const (c : Name) (ls : List Level)
37 /-- Application. -/
38 | app (f a : Expr)
39 /-- Abstraction `fun (x : A) => b`. -/
40 | lam (A b : Expr)
41 /-- The Π-type `(x : A) → B`. -/
42 | pi (A B : Expr)
43 /-- `let x : ty := v; b`. Kept as Lean stores it: the
44 checker substitutes the value (`Red.zeta`, `Infer.letE`), and the
45 interpretation reads the body at the value's value, ignoring the type
46 (`Interp.lean`), as con-leche's `Denotes` `let` rule does. -/
47 | letE (ty v b : Expr)
48 deriving DecidableEq
is a variable $𝑥$; a sort $\text{𝖲𝗈𝗋𝗍}𝑢$ at a universe level $𝑢$ (Section 2.2), with $\text{𝖯𝗋𝗈𝗉}=\text{𝖲𝗈𝗋𝗍}0$; an application $𝑓𝑎$; a function $𝜆𝑥:𝐴.𝑏$; a dependent function type, or Π-type, $\forall 𝑥:𝐴.𝐵$, written $𝐴\to 𝐵$ when $𝑥$ does not occur in $𝐵$; or a let-expression $\text{𝗅𝖾𝗍}𝑥:𝑇≔𝑣;𝑏$. Types are terms; there is no separate class. A sequence of binders, such as the lambdas of $𝜆𝑥:𝐴.𝜆𝑦:𝐵.𝑒$, is a telescope.

The paper writes named variables, with the usual conventions: terms are taken up to renaming of bound variables, and $𝐵\left[𝑥≔𝑎\right]$ is the capture-avoiding substitutionwhitepaper/Fragment/Syntax.lean:L65-L7565/-- Instantiate the bound variable `k` by `a` (and lower the indices
66above it): `e.inst a` is `e[x := a]` for the innermost binder. -/
67def inst : Expr → Expr → (k : Nat := 0) → Expr
68 | bvar i, a, k =>
69 if i < k then bvar i else if i = k then liftN k a else bvar (i - 1)
70 | sort u, _, _ => sort u
71 | const c ls, _, _ => const c ls
72 | app f b, a, k => app (inst f a k) (inst b a k)
73 | lam A b, a, k => lam (inst A a k) (inst b a (k + 1))
74 | pi A B, a, k => pi (inst A a k) (inst B a (k + 1))
75 | letE T v b, a, k => letE (inst T a k) (inst v a k) (inst b a (k + 1))
of $𝑎$ for $𝑥$. The Lean fragment uses de Bruijn indices instead (a variable is the number of binders between its occurrence and its own), and a rule that mentions the types of the variables in scope carries a context $\mathrm{\Gamma }$, a list of those types. No rule in this paper needs index arithmetic in its named form.

2.2. Levels

Universe levelswhitepaper/Fragment/Level.lean:L29-L4329/-- Universe levels (`Lean.Level` without `mvar`). -/
30inductive Level where
31 /-- `Prop`'s level, `0`. -/
32 | zero
33 /-- The successor level `u + 1`. -/
34 | succ (l : Level)
35 /-- The maximum `max u v`. -/
36 | max (a b : Level)
37 /-- The impredicative maximum: `imax u v` is `0` when `v` is `0`,
38 else `max u v` — so a `∀` whose codomain is a proposition is a
39 proposition whatever its domain's level. -/
40 | imax (a b : Level)
41 /-- A level parameter of the enclosing declaration. -/
42 | param (n : Name)
43 deriving DecidableEq, Repr
are Lean’s, without metavariablesConLeche/Kernel/Expr.lean:L39-L4439inductive Level where
40 | zero
41 | succ (u : Level)
42 | max (u v : Level)
43 | imax (u v : Level)
44 | param (n : Name)
:

with $𝑝$ a level parameter of the enclosing declaration. A level means a natural numberwhitepaper/Fragment/Level.lean:L50-L5650/-- The value of a level under a *valuation* `φ` of its parameters. -/
51def eval (φ : Name → Nat) : Level → Nat
52 | zero => 0
53 | succ l => eval φ l + 1
54 | max a b => Max.max (eval φ a) (eval φ b)
55 | imax a b => imaxNat (eval φ a) (eval φ b)
56 | param n => φ n
once a valuation $𝜑$ fixes the parameters: $0$, successor, maximum, and $imax\left(𝑢,𝑣\right)$ is $0$ when $𝑣$ is $0$ and $max\left(𝑢,𝑣\right)$ otherwise (as in con-lecheConLeche/Verify/Level.lean:L26-L3126@[expose] def eval (φ : Name → Nat) : Level → Nat
27 | .zero => 0
28 | .succ l => eval φ l + 1
29 | .max l r => Max.max (eval φ l) (eval φ r)
30 | .imax l r => if eval φ r = 0 then 0 else Max.max (eval φ l) (eval φ r)
31 | .param n => φ n
). The impredicative maximum is what makes $\forall 𝑥:𝐴.𝐵$ a proposition whenever $𝐵$ is one, whatever the level of $𝐴$: its sort is $\text{𝖲𝗈𝗋𝗍}\left(imax\left(𝑢,𝑣\right)\right)$ (rule pi in Section 2.3).

The level oracle. The checker decides $𝑢\le 𝑣$ and $𝑢=𝑣$ between levels with an algorithm. This paper does not present that algorithm and does not verify it. It assumes two Boolean functionswhitepaper/Fragment/Level.lean:L130-L145130/-- **The level oracle** — the checker's decision procedures for `≤` and
131`=` on levels, assumed sound and complete with respect to `eval`: a
132parameter of the development, never defined here. (`le` is what the
133inductive installs of the environment section consume; the env-free
134fragment uses `eq` alone.) -/
135class LevelOracle where
136 /-- `le u v = true` decides `u ≤ v` at every valuation. -/
137 le : Level → Level → Bool
138 /-- `eq u v = true` decides `u = v` at every valuation. -/
139 eq : Level → Level → Bool
140 /-- Soundness and completeness of `le`. -/
141 le_iff : ∀ a b : Level, le a b = true ↔ ∀ φ : Name → Nat, Level.eval φ a ≤ Level.eval φ b
142 /-- Soundness and completeness of `eq`. -/
143 eq_iff : ∀ a b : Level, eq a b = true ↔ ∀ φ : Name → Nat, Level.eval φ a = Level.eval φ b
144
145namespace Level
with a specification: $𝑢\le 𝑣$ is answered yes exactly when the value of $𝑢$ is at most the value of $𝑣$ at every valuation, and $𝑢=𝑣$ exactly when the values agree at every valuation (the real $\le$ConLeche/Kernel/Level.lean:L144-L146144/-- Decide `l ≤ r` semantically; `none` is an exhausted comparison. -/
145def leq (l r : Level) : Option Bool :=
146 leqCore defaultFuel (simplify l) (simplify r) 0
, the real $=$ConLeche/Kernel/Level.lean:L164-L167164def isEquiv (l r : Level) : Option Bool := do
165 if l == r then pure true
166 else if simplify l = simplify r then pure true
167 else if ← leq l r then leq r l else pure false
and their soundnessConLeche/Verify/Level.lean:L173-L174173theorem leq_sound {l r : Level} (h : leq l r = some true) :
174 ∀ φ, eval φ l ≤ eval φ r := by
proofsConLeche/Verify/Level.lean:L201-L202201theorem isEquiv_sound {l r : Level} (h : isEquiv l r = some true) :
202 ∀ φ, eval φ l = eval φ r := by
). We write $𝑢\doteq 𝑣$ for “the oracle says $𝑢=𝑣$”.

2.3. The three relations

The checker is described by three relations over terms, defined together by inference rules: reduction $\mathrm{\Gamma }⊢𝑒⇝{𝑒}^{\prime }$, definitional equality $\mathrm{\Gamma }⊢𝑎\equiv 𝑏$, and inference $\mathrm{\Gamma }⊢𝑒\Rightarrow 𝑇$. A context $\mathrm{\Gamma }$ lists the variables in scope with their types. The complete rule sets are one mutual inductive definitionwhitepaper/Fragment/Rules.lean:L56-L79856mutual
57
58/-- **Reduction**: the head steps of the checker's `whnf`, chained. -/
59inductive Red (env : Env) : List Expr → Expr → Expr → Prop where
60 /-- No step (`Red.refl`, `Rel.lean:106`). -/
61 | refl {Γ : List Expr} {e : Expr} : Red env Γ e e
62 /-- Chaining (`Red.trans`, `Rel.lean:111`). A reduction is a
63 denotation identity, so chaining costs nothing semantically. -/
64 | trans {Γ : List Expr} {e₁ e₂ e₃ : Expr} :
65 Red env Γ e₁ e₂ → Red env Γ e₂ e₃ → Red env Γ e₁ e₃
66 /-- Head reduction inside an application (`Red.appFn`,
67 `Rel.lean:116`): the head is reduced before a redex is looked for. -/
68 | appFn {Γ : List Expr} {f f' a : Expr} :
69 Red env Γ f f' → Red env Γ (app f a) (app f' a)
70 /-- **β**: at every binder, with **no premise** — no
71 inference of the argument, no comparison with the binder's domain.
72 This is Lean's own β (`whnf_core`). The model needs no premise
73 (`Sound.lean`, `Red.beta_sound`): a reduction claims nothing of a
74 redex that denotes the point, and a redex that does not has a lambda that
75 does not, so a graph, which determines its domain: the argument lies
76 in the lambda's domain because it lies in the domain of the slot the
77 semantic invariant gives the application.
78 -/
79 | beta {Γ : List Expr} {A b a : Expr} :
80 Red env Γ (app (lam A b) a) (b.inst a)
81 /-- **ζ**: a `let` reduces to its body with the value
82 substituted, with no certificate, as β (con-leche's `whnfCore` on
83 `.letE`, S0's `inst1M b v`; official `whnf_core`). Unlike β it
84 needs no case split on the point: the `let` and its reduct denote
85 alike at every environment (`interp_zeta`). -/
86 | zeta {Γ : List Expr} {T v b : Expr} :
87 Red env Γ (letE T v b) (b.inst v)
88 /-- **δ** (`Red.delta`, `Rel.lean:140`): a definition unfolds to its
89 value, at the use's level instantiation. (With `appFn`, an applied
90 definition unfolds at its head.) -/
91 | delta {Γ : List Expr} {c : Name} {ls : List Level} {ci : ConstInfo} {v : Expr} :
92 env.find? c = some ci → ci.value? = some v →
93 ls.length = ci.lparams.length →
94 Red env Γ (const c ls) (v.instL ci.lparams ls)
95 /-- **ι** (`Red.iota`, `Rel.lean:200`): a stored recursor applied to
… 703 more lines, as in con-lecheConLeche/Rules/Rel.lean:L97-L101 97mutual
98
99/-- **Reduction**: the head steps of `whnfCore` and the `whnf` loop,
100chained. -/
101inductive Red (env : Env) : Nat → Expr → Expr → Prop where
.

How to read them. The three relations describe what the checker does. $\mathrm{\Gamma }⊢𝑎\equiv 𝑏$ means that on the terms $𝑎$ and $𝑏$ the checker’s equality test answers yes. $\mathrm{\Gamma }⊢𝑒\Rightarrow 𝑇$ means that, asked for the type of $𝑒$, the checker returns $𝑇$. We write $\Rightarrow$ rather than the customary colon so that it is not read as a typing judgement, which this paper does not have. Every relation is stated in the accepting direction only; nothing says what the checker rejects. A rule’s premises are exactly what the checker did at that site: the recursive calls it made, and the tests whose outcome fixes the shape of the conclusion.

A convention: a chain such as $\mathrm{\Gamma }⊢𝑎\Rightarrow 𝑇⇝𝑒$ abbreviates consecutive premises in the same context, one per arrow, the right end of each arrow being the subject of the next; here $\mathrm{\Gamma }⊢𝑎\Rightarrow 𝑇$ and $\mathrm{\Gamma }⊢𝑇⇝𝑒$. Chains of any length are read the same way.

2.3.1. Reduction

Reduction chains the head steps the checker makes when it normalises a term. It is reflexive and transitivewhitepaper/Fragment/Rules.lean:L58-L6958/-- **Reduction**: the head steps of the checker's `whnf`, chained. -/
59inductive Red (env : Env) : List Expr → Expr → Expr → Prop where
60 /-- No step (`Red.refl`, `Rel.lean:106`). -/
61 | refl {Γ : List Expr} {e : Expr} : Red env Γ e e
62 /-- Chaining (`Red.trans`, `Rel.lean:111`). A reduction is a
63 denotation identity, so chaining costs nothing semantically. -/
64 | trans {Γ : List Expr} {e₁ e₂ e₃ : Expr} :
65 Red env Γ e₁ e₂ → Red env Γ e₂ e₃ → Red env Γ e₁ e₃
66 /-- Head reduction inside an application (`Red.appFn`,
67 `Rel.lean:116`): the head is reduced before a redex is looked for. -/
68 | appFn {Γ : List Expr} {f f' a : Expr} :
69 Red env Γ f f' → Red env Γ (app f a) (app f' a)
, and it reaches inside the headConLeche/Rules/Rel.lean:L101-L117101inductive Red (env : Env) : Nat → Expr → Expr → Prop where
102 /-- Every `pure e` exit: the value clauses of `whnfCoreBody`
103 (`Kernel/Core.lean`), the stuck fallbacks (`:1003`, `:1033-1035`),
104 an uncertified redex (`:1001`), `iotaRec = none` (`:1003`), the
105 loop's fixpoint (`whnfStep`'s `pure e₁`, `:1088`). -/
106 | refl {d : Nat} {e : Expr} : Red env d e e
107 /-- The recursive `whnfCore` continuations after β/ι/proj
108 (`Core.lean:990`, `:997`, `:1002`, `:1033`), the `whnf` loop
109 (`whnfLoop`, `:1091-1095`), and the major's preparation chain
110 (`prepareMajor`, `:785-807`). -/
111 | trans {d : Nat} {e₁ e₂ e₃ : Expr} :
112 Red env d e₁ e₂ → Red env d e₂ e₃ → Red env d e₁ e₃
113 /-- Head normalisation inside an application (`whnfCoreBody`'s
114 `.app` clause, `Kernel/Core.lean`: `whnfCore f` before the redex
115 tests). -/
116 | appFn {d : Nat} {f f' a : Expr} :
117 Red env d f f' → Red env d (.app f a) (.app f' a)
of an application.

$𝛽$whitepaper/Fragment/Rules.lean:L70-L8070 /-- **β**: at every binder, with **no premise** — no
71 inference of the argument, no comparison with the binder's domain.
72 This is Lean's own β (`whnf_core`). The model needs no premise
73 (`Sound.lean`, `Red.beta_sound`): a reduction claims nothing of a
74 redex that denotes the point, and a redex that does not has a lambda that
75 does not, so a graph, which determines its domain: the argument lies
76 in the lambda's domain because it lies in the domain of the slot the
77 semantic invariant gives the application.
78 -/
79 | beta {Γ : List Expr} {A b a : Expr} :
80 Red env Γ (app (lam A b) a) (b.inst a)
fires at every redex, and $𝜁$whitepaper/Fragment/Rules.lean:L81-L8781 /-- **ζ**: a `let` reduces to its body with the value
82 substituted, with no certificate, as β (con-leche's `whnfCore` on
83 `.letE`, S0's `inst1M b v`; official `whnf_core`). Unlike β it
84 needs no case split on the point: the `let` and its reduct denote
85 alike at every environment (`interp_zeta`). -/
86 | zeta {Γ : List Expr} {T v b : Expr} :
87 Red env Γ (letE T v b) (b.inst v)
substitutes a let-binding’s value into its body; neither has a premise.

As in the official kernel, $𝛽$ has no premise, although its soundness needs the argument to lie in the domain of the lambda; Section 2.6 shows where that comes from. $𝜁$ is simpler: a let-expression always denotes what its body with the value substituted denotes.

2.3.2. Definitional equality

The checker’s equality testwhitepaper/Fragment/Rules.lean:L547-L566547inductive DefEq (env : Env) : List Expr → Expr → Expr → Prop where
548 /-- The syntactic fast path (`DefEq.refl`, `Rel.lean:362`). -/
549 | refl {Γ : List Expr} {a : Expr} : DefEq env Γ a a
550 /-- Symmetry (`DefEq.symm`, `Rel.lean:365`). Not a checker move: the
551 constructor from which every right-hand variant of a one-sided rule
552 is derived. -/
553 | symm {Γ : List Expr} {a b : Expr} : DefEq env Γ a b → DefEq env Γ b a
554 /-- **Reduce the left side, then continue** (`DefEq.redL`,
555 `Rel.lean:370`): the recursive structure of `isDefEq` — head
556 normalisation of either side (with `symm`) and every lazy-δ
557 continuation. -/
558 | redL {Γ : List Expr} {a a' b : Expr} :
559 Red env Γ a a' → DefEq env Γ a' b → DefEq env Γ a b
560 /-- Two sorts, by the level oracle (`DefEq.sort`, `Rel.lean:373`). -/
561 | sort {Γ : List Expr} {u v : Level} :
562 LevelOracle.eq u v = true → DefEq env Γ (sort u) (sort v)
563 /-- Two constants of the same name at oracle-equal levels
564 (`DefEq.const`, `Rel.lean:384`). -/
565 | const {Γ : List Expr} {c : Name} {ls ls' : List Level} :
566 Level.eqList ls ls' = true → DefEq env Γ (const c ls) (const c ls')
is reflexive and symmetric. The checker never takes a symmetry step; the rule is there so that each one-sided rule below (red-l, $𝜂$) need be written once, and its mirror image follows. The test interleaves with reduction in one way: reduce the left side, then continue. Sorts are compared through the level oracleConLeche/Rules/Rel.lean:L372-L374372 /-- Two sorts (`Core.lean:1581`). -/
373 | sort {d : Nat} {u v : Level} :
374 Level.isEquiv u v = some true → DefEq env d (.sort u) (.sort v)
.

The congruences descend into the two binders and into applications. Domains are compared first, then the bodies, under the right-hand domain. For $\forall$whitepaper/Fragment/Rules.lean:L567-L575567 /-- `∀`-congruence (`DefEq.forallE`, `Rel.lean:399`): domains, then
568 bodies under the RIGHT domain, and nothing else. A
569 `∀`'s value is a function of its domain's and its fibres' values
570 (`SetLib.piV`: the propositional function space exactly when every fibre is
571 a truth value), and both are types, never the point, so the
572 premises' claims apply everywhere (`Sound.lean`, `DefEq.pi_sound`). -/
573 | pi {Γ : List Expr} {A₁ B₁ A₂ B₂ : Expr} :
574 DefEq env Γ A₁ A₂ → DefEq env (A₂ :: Γ) B₁ B₂ →
575 DefEq env Γ (pi A₁ B₁) (pi A₂ B₂)
that is all.

Two lambdas are compared as two lambda telescopes, by an auxiliary relation $\mathrm{\Gamma }⊢𝑎{\equiv }_{𝜆}𝑏$. The checker descends level by levelwhitepaper/Fragment/Rules.lean:L701-L714701inductive DefEqLams (env : Env) : List Expr → Expr → Expr → Prop where
702 /-- Syntactically equal sides (the checker's `a == b` fast path). -/
703 | refl {Γ : List Expr} {a : Expr} : DefEqLams env Γ a a
704 /-- The innermost level: `DefEq.lam`'s premises — domains, bodies,
705 and the bodies' inferred types. -/
706 | inner {Γ : List Expr} {A₁ b₁ A₂ b₂ t₁ t₂ : Expr} :
707 DefEq env Γ A₁ A₂ → DefEq env (A₂ :: Γ) b₁ b₂ →
708 Infer env (A₂ :: Γ) b₁ t₁ → Infer env (A₂ :: Γ) b₂ t₂ → DefEq env (A₂ :: Γ) t₁ t₂ →
709 DefEqLams env Γ (lam A₁ b₁) (lam A₂ b₂)
710 /-- An outer level: the domains, and the bodies by this relation —
711 no inference, no type comparison. -/
712 | outer {Γ : List Expr} {A₁ b₁ A₂ b₂ : Expr} :
713 DefEq env Γ A₁ A₂ → DefEqLams env (A₂ :: Γ) b₁ b₂ →
714 DefEqLams env Γ (lam A₁ b₁) (lam A₂ b₂)
while both bodies are lambdas, comparing the domains at each level (lam-outer). At the innermost level, where the descent stops, it also infers the types of the two bodieswhitepaper/Fragment/Rules.lean:L704-L709704 /-- The innermost level: `DefEq.lam`'s premises — domains, bodies,
705 and the bodies' inferred types. -/
706 | inner {Γ : List Expr} {A₁ b₁ A₂ b₂ t₁ t₂ : Expr} :
707 DefEq env Γ A₁ A₂ → DefEq env (A₂ :: Γ) b₁ b₂ →
708 Infer env (A₂ :: Γ) b₁ t₁ → Infer env (A₂ :: Γ) b₂ t₂ → DefEq env (A₂ :: Γ) t₁ t₂ →
709 DefEqLams env Γ (lam A₁ b₁) (lam A₂ b₂)
under the binder and compares them (lam). That comparison is a check the official kernel does not make. Such checks are typeset in one colour, like this, throughout the paper; a reader who ignores the coloured premises sees the official kernel’s rule. Section 2.8 explains why they are there, and why the outer levels need none.

(Two syntactically equal terms are also related by ${\equiv }_{𝜆}$.) A lambda against a term $𝑏$ that is not a lambda is tried by $𝜂$whitepaper/Fragment/Rules.lean:L640-L653640 /-- **η** (`DefEq.eta`, `Rel.lean:430`): a lambda against a term `b`
641 whose inferred type reduces to a `∀` with a definitionally equal
642 domain, when the lambda's body is `b` applied to the variable — and,
643 **typed** as lambda congruence is, the lambda's body's inferred
644 type is definitionally equal to the `∀`'s body, so that the lambda's body
645 and `b` applied lie in one type. Sound because a member of a
646 function space is the abstraction of its applications
647 (`SetLib.lamV_eta`). -/
648 | eta {Γ : List Expr} {A₁ b₁ b tb A₂ B t₁ : Expr} :
649 Infer env Γ b tb → Red env Γ tb (pi A₂ B) →
650 DefEq env Γ A₂ A₁ →
651 DefEq env (A₁ :: Γ) b₁ (app (b.liftN 1) (bvar 0)) →
652 Infer env (A₁ :: Γ) b₁ t₁ → DefEq env (A₁ :: Γ) t₁ B →
653 DefEq env Γ (lam A₁ b₁) b
. The type of $𝑏$ is inferred and reduced to a $\forall$, its domain is compared with the lambda’s, and the body is compared with $𝑏$ applied to the bound variable. As at the innermost level of lambda congruence, the type of the lambda’s body is inferred and compared with the $\forall$‘s body. Two terms are equal by proof irrelevancewhitepaper/Fragment/Rules.lean:L654-L663654 /-- **Proof irrelevance** (`DefEq.proofIrrel`, `Rel.lean:452`): both
655 sides' inferred types have sort `Prop`. **The two types are never
656 compared**: the model justifies that, because every proof denotes the
657 one point. -/
658 | proofIrrel {Γ : List Expr} {a ta tta b tb ttb : Expr} {u v : Level} :
659 Infer env Γ a ta → Infer env Γ ta tta → Red env Γ tta (sort u) →
660 LevelOracle.eq u .zero = true →
661 Infer env Γ b tb → Infer env Γ tb ttb → Red env Γ ttb (sort v) →
662 LevelOracle.eq v .zero = true →
663 DefEq env Γ a b
when both are proofs: each one’s type has type $\text{𝖲𝗈𝗋𝗍}𝑢$ with $𝑢$ oracle-equal to $0$.

Proof irrelevance. The rule compares the sorts of the two types, and never the two types. The official kernel also compares ${𝑇}_{𝑎}$ with ${𝑇}_{𝑏}$, so that $𝑎$ and $𝑏$ are proofs of the same proposition. This checker does not, and so accepts strictly more than Lean at this one site. The model justifies it: every proof denotes the point, so two proofs of two propositions denote the same set.

The list has no transitivity rulewhitepaper/Fragment/Rules.lean:L529-L546529/-- **Definitional equality**: the verdict `true` of the checker's
530`isDefEq`.
531
532**There is no `trans` rule, deliberately** (`Rel.lean:334-357`).
533The relation is the checker's verdict on two terms that are
534well-formed *together*, a fact no rule states because well-formedness
535is semantic (`WellDenoted`) and may not enter this inductive. Every
536rule respects one discipline instead: **the subject of each `DefEq`
537premise is a subterm of the conclusion or is produced by a `Red` or
538`Infer` premise** (a reduct, an inferred type), so the soundness proof
539always has the premise's terms — and their invariant — in hand. A
540`trans` rule is the unique rule that would break it: its middle term
541comes from nowhere, so nothing supplies its invariant, and the
542induction has nothing to apply the hypothesis to. Nor does the
543checker chain through an arbitrary middle term: every comparison it
544makes is one of the rules below, and its one way to chain is
545"reduce, then continue": `redL`.
546-/
, and none can be addedConLeche/Rules/Rel.lean:L334-L357334/-- **Definitional equality**: the verdict `true` of `isDefEq`.
335
336**There is no `trans` rule, deliberately, and none can be added**
337(task #309, the experiment recorded in DESIGN.md). The relation is
338not an equivalence on terms: it is the checker's verdict, and the
339checker only ever compares terms that are well-formed *together* — a
340fact the rules never state, because well-formedness (scoping, the
341readability of the terms, the grading of the reading) is semantic
342and may not enter this inductive. Every rule respects one syntactic
343discipline instead: **the subject of each `DefEq` premise is either a
344subterm of the conclusion or is produced by an existence-form `Red` /
345`Infer` premise** (a reduct, an inferred type), so the soundness proof
346(`ConLeche/Model/Rules/Sound.lean`) always has the premise's terms in
347hand. `trans` is the unique rule that would break it: its middle
348term comes from nowhere, and with it two rules that are each sound
349alone meet — `fvar` compares free variables by index only (their
350types are not compared, as the checker does not), while
351`proofFast` *reads* a head's stored data to decide "definitely a
352proof" — and derive `DefEq env d (.fvar i ty) (.fvar i' ty')` for
353every `i`, `i'`, which no model satisfies. The recursive-structure rules
354(`redL`, `natSucc`, `eta`, `structUnit`) are therefore not a
355proof-engineering convenience but what keeps the relation sound; the
356one chaining that is sound, "reduce, then continue", is `redL`, and
357its right-hand and δ variants are derived in `Derived.lean`. -/
; Section 2.7 explains why. Instead of chaining equalities, the checker chains reductions: it reduces a side, then continues (red-l).

2.3.3. Inference

A variable’s type is read off the contextwhitepaper/Fragment/Rules.lean:L740-L748740inductive Infer (env : Env) : List Expr → Expr → Expr → Prop where
741 /-- A bound variable's type is its context entry, lifted over the
742 binders in between (`Infer.fvar`, `Rel.lean:555`; the real checker
743 reads the type off the free variable). -/
744 | bvar {Γ : List Expr} {i : Nat} {A : Expr} :
745 Γ[i]? = some A → Infer env Γ (bvar i) (A.liftN (i + 1))
746 /-- `Sort u : Sort (u + 1)` (`Infer.sort`, `Rel.lean:551`). -/
747 | sort {Γ : List Expr} {u : Level} :
748 Infer env Γ (sort u) (sort (.succ u))
, and a sort has the next sortConLeche/Rules/Rel.lean:L549-L565549inductive Infer (env : Env) : Grade → Nat → Expr → Expr → Prop where
550 /-- `Core.lean:1114` / `:1294`. -/
551 | sort {g : Grade} {d : Nat} {u : Level} :
552 Infer env g d (.sort u) (.sort (.succ u))
553 /-- `Kernel/Core.lean` / `:1295-1297`: an opened variable's stored
554 type, at the leaf scope check. -/
555 | fvar {g : Grade} {d idx : Nat} {ty : Expr} :
556 idx < d → Infer env g d (.fvar idx ty) ty
557 /-- `Kernel/Core.lean` / `:1298-1309`: a stored constant that is
558 not a projection table, at the right level arity. -/
559 | const {g : Grade} {d : Nat} {n : Name} {us : List Level}
560 {ci : ConstantInfo} :
561 env.find? n = some ci → ci.isTowerEntry = false →
562 us.length = ci.toConstantVal.levelParams.length →
563 Infer env g d (.const n us)
564 (ci.toConstantVal.type.instantiateLevelParams
565 ci.toConstantVal.levelParams us)
. The rules of this subsection are the checker’s full inference. The checker also has a cheaper mode, infer_only, which skips some of their checks; Section 2.9 presents it.

The two binder ruleswhitepaper/Fragment/Rules.lean:L754-L771754 /-- **`∀`-formation** (`Infer.forallE`, `Rel.lean:576`): the domain's
755 type reduces to a sort `u`, the body's type (under the domain)
756 reduces to a sort `v`, the result is `Sort (imax u v)`. Nothing is
757 checked beyond Lean's own rule. -/
758 | pi {Γ : List Expr} {A B s t : Expr} {u v : Level} :
759 Infer env Γ A s → Red env Γ s (sort u) →
760 Infer env (A :: Γ) B t → Red env (A :: Γ) t (sort v) →
761 Infer env Γ (pi A B) (sort (.imax u v))
762 /-- **Lambda** (`Infer.lam`, `Rel.lean:589`): the domain's type reduces to
763 a sort, the body is inferred under the domain, and the result is the
764 `∀` of the body's type — Lean's own rule. The body's type's sort is
765 not computed: an inferred type is a type (`InferSem`), which is all
766 the `∀`'s invariant asks of it, and the body's value is read by the
767 interpretation, not by its sort. -/
768 | lam {Γ : List Expr} {A b s bt : Expr} {u : Level} :
769 Infer env Γ A s → Red env Γ s (sort u) →
770 Infer env (A :: Γ) b bt →
771 Infer env Γ (lam A b) (pi A bt)
are Lean’s own. For a $\forall$, the domain’s type must reduce to a sort $\text{𝖲𝗈𝗋𝗍}𝑢$ and the body’s type, under the domain, to a sort $\text{𝖲𝗈𝗋𝗍}𝑣$; the result is $\text{𝖲𝗈𝗋𝗍}\left(imax\left(𝑢,𝑣\right)\right)$. For a lambda, the domain’s type must reduce to a sort, and the result is the $\forall$ of the body’s inferred type; the sort of that type is not computed.

An application infers the head’s typewhitepaper/Fragment/Rules.lean:L772-L781772 /-- **Application** (`Infer.app`, `Rel.lean:617`): the head's type
773 reduces to a `∀`, and the argument's inferred type is definitionally
774 equal to its domain. This is where a syntactic proof would need
775 Π-injectivity and the semantic one does not: the `∀` the head's type
776 reduces to *is* a function space, and membership in it is what the
777 model needs (`Sound.lean`, `infer_sound`'s `app` case). -/
778 | app {Γ : List Expr} {f a tf A B ta : Expr} :
779 Infer env Γ f tf → Red env Γ tf (pi A B) →
780 Infer env Γ a ta → DefEq env Γ ta A →
781 Infer env Γ (app f a) (B.inst a)
, reduces it to a $\forall$, infers the argument’s type and compares it with the domainConLeche/Rules/Rel.lean:L617-L621617 | app {g : Grade} {d : Nat} {f a tf ty body ta : Expr} :
618 Infer env g d f tf → Red env d tf (.forallE ty body) →
619 (g = .full → Infer env .full d a ta) →
620 (g = .full → DefEq env d ta ty) →
621 Infer env g d (.app f a) (body.instantiate1 a)
. A let-expressionwhitepaper/Fragment/Rules.lean:L782-L796782 /-- **`let`, by substitution** (official `infer_let`
783 with the body instantiated rather than opened at a let-variable, as
784 the checker does): the type's type reduces to a
785 sort, the value's inferred type is definitionally equal to the type,
786 and the result is the inferred type of the body with the value
787 substituted. The two checks on the value are Lean's (they reject
788 `let x : T := v; b` with `v : T` false even where the body ignores
789 `x`); the soundness proof does not use them (`Sound.lean`,
790 `Infer.letE_sound`), because `interp` reads no type and the body is
791 inferred at the value itself. -/
792 | letE {Γ : List Expr} {T v b s tv B : Expr} {u : Level} :
793 Infer env Γ T s → Red env Γ s (sort u) →
794 Infer env Γ v tv → DefEq env Γ tv T →
795 Infer env Γ (b.inst v) B →
796 Infer env Γ (letE T v b) B
checks that its type has a sort and that its value’s type agrees with it, as Lean does, and then infers the type of the body with the value substituted.

Reducing to a $\forall$. The application rule reduces the inferred type of $𝑓$ until a $\forall$ is syntactically there. It does not take a type of $𝑓$ that is a $\forall$ up to definitional equality and argue that its domain is the right one. That argument is where a syntactic soundness proof needs injectivity of $\forall$, the property that $\forall 𝑥:𝐴.𝐵\equiv \forall 𝑥:{𝐴}^{\prime }.{𝐵}^{\prime }$ forces $𝐴\equiv {𝐴}^{\prime }$. Our proof never needs it, and the model does not validate it: $\forall 𝑥:𝐴.\text{𝖳𝗋𝗎𝖾}$ and $\forall 𝑥:{𝐴}^{\prime }.\text{𝖳𝗋𝗎𝖾}$ denote the same truth value whatever $𝐴$ and ${𝐴}^{\prime }$ are. Our proof argues instead that the head denotes a member of what the $\forall$ denotes, because reduction preserves denotations; that the argument denotes a member of the domain, by the comparison premise; and that applying a member of a function space to a member of its domain lands in the fibre. The second half of this section carries this out.

The let-expression. The two checks on the value are what Lean runs, and they decide verdicts: they reject a let-expression whose value does not have the stated type even where the body ignores it. The soundness proof does not use them (Section 2.7): the interpretation reads no type, and the body is inferred with the value itself in place of the variable.

2.4. The set theory we assume

The other side of the argument is a set theory. We do not construct one. The reader is given an axiomatised theory, a type of sets with the operations and laws listed below, and is promised that nothing beyond these laws is used. The theory is stated in Lean’s own logic, so it is higher-order: separation takes any predicate of that logic, and graphs and function spaces are formed from any function of it. It is deliberately not minimal: graphs, dependent function spaces and the universe chain, which a minimal axiom system would construct, are assumed outright with their laws, because how they are built does not matter to the argument. The promise is literal: in the Lean fragment the structure is a class, SetLibwhitepaper/Fragment/Lib.lean:L56-L12656/-- **The set theory we assume.** A type of sets `V` with the
57operators and laws the fragment's proof uses. The theory is stated in
58Lean's logic, so separation is available for every predicate of that
59logic, and the function-space laws quantify over functions on the
60sets. -/
61class SetLib (V : Type u) where
62 /-- Membership. -/
63 Mem : V → V → Prop
64 /-- Extensionality. -/
65 ext : ∀ {x y : V}, (∀ z, Mem z x ↔ Mem z y) → x = y
66 /-- Separation: the members of `A` that satisfy `P`. -/
67 sep : V → (V → Prop) → V
68 /-- The members of a separation. -/
69 mem_sep : ∀ {A : V} {P : V → Prop} {z : V}, Mem z (sep A P) ↔ Mem z A ∧ P z
70 /-- A distinguished set, subject to the point's three laws below. It
71 is the one proof of every true proposition. -/
72 pt : V
73 /-- The one-element set `{pt}`. -/
74 one : V
75 /-- The members of `{pt}`. -/
76 mem_one : ∀ {z : V}, Mem z one ↔ z = pt
77 /-- The universe chain: `univ n` sizes `Sort n`, which denotes the
78 types among its members, `typeU n`. -/
79 univ : Nat → V
80 /-- `univ 0` is the set of subsets of `{pt}` — the truth values. -/
81 mem_univ_zero : ∀ {T : V}, Mem T (univ 0) ↔ ∀ z, Mem z T → z = pt
82 /-- Each universe is a member of the next. -/
83 univ_mem_succ : ∀ n : Nat, Mem (univ n) (univ (n + 1))
84 /-- Cumulativity. -/
85 univ_mono : ∀ {m n : Nat} {x : V}, m ≤ n → Mem x (univ m) → Mem x (univ n)
86 /-- The graph of a function on a domain. -/
87 graph : (V → V) → V → V
88 /-- The dependent function space: the graphs over `A` with values
89 in the fibres `B`. -/
90 piSet : V → (V → V) → V
91 /-- Application. On the point it is the point (a proof applied to
92 anything is a proof); on a graph it reads the graph. -/
93 app : V → V → V
94 /-- A proof applied is the proof. -/
95 app_pt : ∀ a : V, app pt a = pt
… 31 more lines, and every theorem of the fragment is proved against that class.

The laws come in four groups.

Sets, membership, extensionality, separation. A type $𝑉$ of sets with a membership relation $𝑥\in 𝑦$; extensionalitywhitepaper/Fragment/Lib.lean:L64-L6564 /-- Extensionality. -/
65 ext : ∀ {x y : V}, (∀ z, Mem z x ↔ Mem z y) → x = y
: two sets with the same members are equal; and separationwhitepaper/Fragment/Lib.lean:L66-L6966 /-- Separation: the members of `A` that satisfy `P`. -/
67 sep : V → (V → Prop) → V
68 /-- The members of a separation. -/
69 mem_sep : ∀ {A : V} {P : V → Prop} {z : V}, Mem z (sep A P) ↔ Mem z A ∧ P z
: for every set $𝐴$ and every property $𝑃$ of sets, a set $\left\{𝑥\in 𝐴|𝑃\left(𝑥\right)\right\}$ whose members are the members of $𝐴$ that satisfy $𝑃$. A property here is any predicate on sets expressible in Lean’s type theory, the logic the theory is stated in, not only a first-order formula.

The point and the truth values. A distinguished set $\text{𝗉𝗍}$, the point, and its singleton $\left\{\text{𝗉𝗍}\right\}$whitepaper/Fragment/Lib.lean:L73-L7673 /-- The one-element set `{pt}`. -/
74 one : V
75 /-- The members of `{pt}`. -/
76 mem_one : ∀ {z : V}, Mem z one ↔ z = pt
. The point will be the one proof of every true proposition. For a proposition $𝑃$ of the ambient logic we write $tv\left(𝑃\right)$ for the separation $\left\{𝑥\in \left\{\text{𝗉𝗍}\right\}|𝑃\right\}$ and call it the truth value of $𝑃$whitepaper/Fragment/Lib.lean:L142-L144142/-- The truth value of a proposition: `{pt}` if it holds, `∅` if
143not. -/
144def truthVal (P : Prop) : V := sep one (fun _ => P)
. Its only possible member is the point, which it has exactly when $𝑃$ holds, so $tv\left(𝑃\right)=\left\{\text{𝗉𝗍}\right\}$ when $𝑃$ is true and $tv\left(𝑃\right)=\varnothing$ when it is false. This is an abbreviation, not an axiom. The point itself obeys three lawswhitepaper/Fragment/Lib.lean:L120-L126120 /-- **The point's laws** (1): the point is not a truth value — it has
121 a member other than itself. -/
122 pt_not_mem_univ_zero : ¬ Mem pt (univ 0)
123 /-- (2): the point has at most one member. -/
124 pt_subsingleton : ∀ {x y : V}, Mem x pt → Mem y pt → x = y
125 /-- (3): no graph is a member of the point. -/
126 graph_not_mem_pt : ∀ {F : V → V} {A : V}, ¬ Mem (graph F A) pt
: it is not a truth value (it has a member other than itself), it has at most one member, and no graph (below) is a member of it.

The universes. A chain of setswhitepaper/Fragment/Lib.lean:L77-L8577 /-- The universe chain: `univ n` sizes `Sort n`, which denotes the
78 types among its members, `typeU n`. -/
79 univ : Nat → V
80 /-- `univ 0` is the set of subsets of `{pt}` — the truth values. -/
81 mem_univ_zero : ∀ {T : V}, Mem T (univ 0) ↔ ∀ z, Mem z T → z = pt
82 /-- Each universe is a member of the next. -/
83 univ_mem_succ : ∀ n : Nat, Mem (univ n) (univ (n + 1))
84 /-- Cumulativity. -/
85 univ_mono : ∀ {m n : Nat} {x : V}, m ≤ n → Mem x (univ m) → Mem x (univ n)
${\mathrm{𝒰︀}}_0,{\mathrm{𝒰︀}}_1,{\mathrm{𝒰︀}}_2,\dots$, with ${\mathrm{𝒰︀}}_0$ the set of truth values, the subsets of $\left\{\text{𝗉𝗍}\right\}$. Each ${\mathrm{𝒰︀}}_{𝑛}$ is a member of ${\mathrm{𝒰︀}}_{𝑛+1}$. The chain is cumulative (a member of ${\mathrm{𝒰︀}}_{𝑚}$ is a member of every later ${\mathrm{𝒰︀}}_{𝑛}$), and every universe is closed under separationwhitepaper/Fragment/Lib.lean:L118-L119118 /-- Closure of the universes under separation. -/
119 sep_mem_univ : ∀ {n : Nat} {A : V} {P : V → Prop}, Mem A (univ n) → Mem (sep A P) (univ n)
.

Graphs, function spaces, application. For a function $𝐹$ from sets to sets (a function of the meta-theory, not a set) and a set $𝐴$, a set $graph\left(𝐹,𝐴\right)$; for a set $𝐴$ and a family $𝐵$ of sets indexed by sets, again a function of the meta-theory, a set $\mathrm{\Pi }\left(𝐴,𝐵\right)$, the dependent function space; and for two sets $𝑓$ and $𝑎$ a set $𝑓\cdot 𝑎$, the applicationwhitepaper/Fragment/Lib.lean:L86-L9386 /-- The graph of a function on a domain. -/
87 graph : (V → V) → V → V
88 /-- The dependent function space: the graphs over `A` with values
89 in the fibres `B`. -/
90 piSet : V → (V → V) → V
91 /-- Application. On the point it is the point (a proof applied to
92 anything is a proof); on a graph it reads the graph. -/
93 app : V → V → V
. Their laws:

• $\text{𝗉𝗍}\cdot 𝑎=\text{𝗉𝗍}$: a proof applied to anything is the proofwhitepaper/Fragment/Lib.lean:L94-L9594 /-- A proof applied is the proof. -/
  95 app_pt : ∀ a : V, app pt a = pt
  .
• βwhitepaper/Fragment/Lib.lean:L96-L9796 /-- β: a graph applied on its domain computes. -/
  97 app_graph : ∀ {F : V → V} {A a : V}, Mem a A → app (graph F A) a = F a
  : if $𝑎\in 𝐴$ then $graph\left(𝐹,𝐴\right)\cdot 𝑎=𝐹\left(𝑎\right)$.
• $graph\left(𝐹,𝐴\right)\ne \text{𝗉𝗍}$: a graph is never the pointwhitepaper/Fragment/Lib.lean:L98-L9998 /-- A graph is never the point. -/
  99 graph_ne_pt : ∀ {F : V → V} {A : V}, graph F A ≠ pt
  .
• Congruencewhitepaper/Fragment/Lib.lean:L100-L103100 /-- A graph depends only on the function's values on the domain. -/
  101 graph_congr : ∀ {F F' : V → V} {A : V}, (∀ x, Mem x A → F x = F' x) → graph F A = graph F' A
  102 /-- A function space depends only on the fibres over the domain. -/
  103 piSet_congr : ∀ {A : V} {B B' : V → V}, (∀ x, Mem x A → B x = B' x) → piSet A B = piSet A B'
  : $graph\left(𝐹,𝐴\right)$ depends only on the values of $𝐹$ on $𝐴$, and $\mathrm{\Pi }\left(𝐴,𝐵\right)$ only on the values of $𝐵$ on $𝐴$.
• Introductionwhitepaper/Fragment/Lib.lean:L104-L106104 /-- Introduction: fibre-wise members abstract into the space. -/
  105 graph_mem_piSet : ∀ {A : V} {F B : V → V},
  106 (∀ x, Mem x A → Mem (F x) (B x)) → Mem (graph F A) (piSet A B)
  : if $𝐹\left(𝑥\right)\in 𝐵\left(𝑥\right)$ for every $𝑥\in 𝐴$, then $graph\left(𝐹,𝐴\right)\in \mathrm{\Pi }\left(𝐴,𝐵\right)$.
• Eliminationwhitepaper/Fragment/Lib.lean:L107-L108107 /-- Elimination. -/
  108 app_mem_piSet : ∀ {A f a : V} {B : V → V}, Mem f (piSet A B) → Mem a A → Mem (app f a) (B a)
  : if $𝑓\in \mathrm{\Pi }\left(𝐴,𝐵\right)$ and $𝑎\in 𝐴$, then $𝑓\cdot 𝑎\in 𝐵\left(𝑎\right)$.
• ηwhitepaper/Fragment/Lib.lean:L109-L110109 /-- η: a member of a function space is the graph of its applications. -/
  110 graph_app_eq : ∀ {A f : V} {B : V → V}, Mem f (piSet A B) → graph (fun x => app f x) A = f
  : if $𝑓\in \mathrm{\Pi }\left(𝐴,𝐵\right)$, then $graph\left(𝑥\mapsto 𝑓\cdot 𝑥,𝐴\right)=𝑓$.
• Domain uniquenesswhitepaper/Fragment/Lib.lean:L111-L113111 /-- A graph determines its domain. -/
  112 piSet_dom_unique : ∀ {A A' f : V} {B B' : V → V},
  113 Mem f (piSet A B) → Mem f (piSet A' B') → A = A'
  : if $𝑓\in \mathrm{\Pi }\left(𝐴,𝐵\right)$ and $𝑓\in \mathrm{\Pi }\left({𝐴}^{\prime },{𝐵}^{\prime }\right)$, then $𝐴={𝐴}^{\prime }$.
• Closurewhitepaper/Fragment/Lib.lean:L114-L117114 /-- Closure of the positive universes under dependent function
  115 spaces. -/
  116 piSet_mem_univ : ∀ {n : Nat} {A : V} {B : V → V}, n ≠ 0 →
  117 Mem A (univ n) → (∀ x, Mem x A → Mem (B x) (univ n)) → Mem (piSet A B) (univ n)
  : for $𝑛\ne 0$, if $𝐴\in {\mathrm{𝒰︀}}_{𝑛}$ and $𝐵\left(𝑥\right)\in {\mathrm{𝒰︀}}_{𝑛}$ for every $𝑥\in 𝐴$, then $\mathrm{\Pi }\left(𝐴,𝐵\right)\in {\mathrm{𝒰︀}}_{𝑛}$.

This is all this section needs. When inductive types arrive, §4 extends the theory.

Two of these laws are design choices. The first is that application of the point is the point. In the model a proof of a proposition is the point, and a proof of $\forall 𝑥:𝐴.𝑃$ is again the point, not a function. The law makes application one operation that does the right thing on both kinds of value, so the interpretation of $𝑓𝑎$ need not know which kind it is applying. The second is that a graph is never the point: a function and a proof are never the same set. A value that is known to be in a function space, or merely known not to be the point, is therefore a graph, and by domain uniqueness a graph carries its own domain. This is what lets β fire with no premise at all.

One law is deliberately restricted: closure of a universe under function spaces is stated for ${\mathrm{𝒰︀}}_1,{\mathrm{𝒰︀}}_2,\dots$ and not for ${\mathrm{𝒰︀}}_0$. A proposition $\forall 𝑥:𝐴.𝑃$ has no function space in the model. It has a truth value, and a truth value is in ${\mathrm{𝒰︀}}_0$ whatever $𝐴$ is. This is the model’s impredicativitywhitepaper/Fragment/Lib.lean:L275-L278275/-- **Impredicativity**: a function space landing in `Prop` is a truth value,
276whatever its domain. -/
277theorem piR_true_mem_univ_zero {A : V} {B : V → V} :
278 piR true A B ∈ˢ (univ 0 : V) := truthVal_mem_univ_zero _
.

2.5. The interpretation

Every term denotes a set. The interpretation is total, defined on every term, well-typed or not, and term-directed: it is a structural recursion on the term, consulting no derivation and no type. It takes two parameters:

• a valuation $𝜑$ of the level parameters (Section 2.2);
• a variable environment $𝜌$, assigning a set to every variable in scope.

We write $⟦𝑒{⟧}_{𝜌}$ for the set the term $𝑒$ denotes under $𝜌$ ($𝜑$ stays implicit), and $𝜌,𝑥\mapsto 𝑣$ for $𝜌$ extended with the value $𝑣$ for the variable $𝑥$. The clauseswhitepaper/Fragment/Interp.lean:L138-L146138/-- **The interpretation**: total, term-directed, reading no type. -/
139noncomputable def interp (M : Name → List Nat → V) (φ : Name → Nat) : (Nat → V) → Expr → V
140 | ρ, .bvar i => ρ i
141 | _, .sort u => typeU (u.eval φ)
142 | _, .const c ls => M c (ls.map (Level.eval φ))
143 | ρ, .app f a => app (interp M φ ρ f) (interp M φ ρ a)
144 | ρ, .lam A b => lamV (interp M φ ρ A) fun x => interp M φ (cons x ρ) b
145 | ρ, .pi A B => piV (interp M φ ρ A) fun x => interp M φ (cons x ρ) B
146 | ρ, .letE _ v b => interp M φ (cons (interp M φ ρ v) ρ) b
:

with $𝜑\left(𝑢\right)$ the value of the level $𝑢$ at the valuation, and ${\mathrm{𝒯︀}}_{𝑛}$ the sets a sort denotes, below. The two binder clauses choose between two readings by the valueswhitepaper/Fragment/Lib.lean:L469-L481469open Classical in
470/-- Is every fibre over the domain a truth value? -/
471noncomputable def propB (A : V) (B : V → V) : Bool := decide (∀ x, x ∈ˢ A → B x ∈ˢ univ 0)
472
473open Classical in
474/-- Is every body value over the domain the point? -/
475noncomputable def ptB (A : V) (F : V → V) : Bool := decide (∀ x, x ∈ˢ A → F x = pt)
476
477/-- **The function space, regime read off the fibres.** -/
478noncomputable def piV (A : V) (B : V → V) : V := piR (propB A B) A B
479
480/-- **The abstraction, regime read off the body values.** -/
481noncomputable def lamV (A : V) (F : V → V) : V := lamR (ptB A F) A F
:

Here ${\mathrm{\Pi }}_0\left(𝐴,𝐵\right)$ is the propositional function spacewhitepaper/Fragment/Lib.lean:L185-L191185/-- **The propositional function space** `Π₀(A, B)`: the truth value "every
186fibre is `{pt}`". When the fibres are truth values it is their
187intersection `⋂ x ∈ A, B x` (the empty intersection being `{pt}`):
188`{pt}` exactly when every fibre is, `∅` otherwise — the function space of
189subsets of a singleton. Reducible, so proofs that unfold `piR true`
190keep working. -/
191abbrev piProp (A : V) (B : V → V) : V := truthVal (∀ x, x ∈ˢ A → B x = one)
, $tv\left(\forall 𝑣\in 𝐴.𝐵\left(𝑣\right)=\left\{\text{𝗉𝗍}\right\}\right)$. When the fibres $𝐵\left(𝑣\right)$ are truth values it is their intersection ${\bigcap }_{𝑣\in 𝐴}𝐵\left(𝑣\right)$ (the empty intersection being $\left\{\text{𝗉𝗍}\right\}$), which is $\left\{\text{𝗉𝗍}\right\}$ exactly when every fibre is and $\varnothing$ otherwise: the function space of subsets of a singleton. A let reads its body at the value’s value, and its type is not read, as no type is read anywhere.

So a binder has two readings. When the body is not a proposition, a lambda is a graph and a $\forall$ is a set of such graphs, a function space. When it is, a lambda is a proof, hence the point, and a $\forall$ is a proposition, true when every fibre (the set $⟦𝐵{⟧}_{𝜌,𝑥\mapsto 𝑣}$ at a $𝑣\in ⟦𝐴{⟧}_{𝜌}$) is $\left\{\text{𝗉𝗍}\right\}$. Which reading applies is decided by the values the body takes over the domain, and by nothing else. The interpretation does not know the sort of $𝐵$, and does not compute it.

The empty domain. Over a non-empty domain the values choose the reading the sort of the body would choose. Over an empty domain there are no values, and both clauses take their first case: a function space over an empty domain is $\left\{\text{𝗉𝗍}\right\}$whitepaper/Fragment/Lib.lean:L625-L631625/-- Over an empty domain the function space is `{pt}`. -/
626theorem piV_of_empty {A : V} {B : V → V} (h : ∀ x, ¬ x ∈ˢ A) : piV A B = one := by
627 unfold piV
628 rw [propB_eq_true.mpr fun x hx => absurd hx (h x), piR_true]
629 exact ext fun z => by
630 rw [mem_truthVal, mem_one]
631 exact ⟨fun h' => h'.1, fun h' => ⟨h', fun x hx => absurd hx (h x)⟩⟩
, and an abstraction over one is the pointwhitepaper/Fragment/Lib.lean:L633-L635633/-- Over an empty domain the abstraction is the point. -/
634theorem lamV_of_empty {A : V} {F : V → V} (h : ∀ x, ¬ x ∈ˢ A) : lamV A F = pt :=
635 lamV_eq_pt fun x hx => absurd hx (h x)
, whatever the sort of the body. So False → Nat, a type of sort Type, denotes $\left\{\text{𝗉𝗍}\right\}$, and its inhabitant fun h => h.elim denotes the point. A function space over an inhabited domain can do the same: Nat → False → Nat has $\left\{\text{𝗉𝗍}\right\}$ as every fibre and is itself $\left\{\text{𝗉𝗍}\right\}$whitepaper/Fragment/Probe.lean:L52-L5452/-- `Nat → False → Nat`: every fibre is `{pt}`, so the function space is the
53truth value `{pt}`, although its sort is `Type`. -/
54theorem piV_const_one {A : V} : piV A (fun _ => one) = one := by
, and fun n h => h.elim is the point. No other reading over the empty domain does better. Whether the codomain is a proposition there is a fact about the syntax, not about any value, and reading an empty Π-type as a function space instead would make the proposition False → False denote a one-element set of graphs, which no truth value is.

What a sort denotes. A set is a typewhitepaper/Fragment/Lib.lean:L298-L302298/-- A **strict** set: not the point, and the point is not a member. -/
299def Strict (X : V) : Prop := X ≠ pt ∧ ¬ pt ∈ˢ X
300
301/-- A **type**: a truth value, or a strict set. -/
302def IsTy (X : V) : Prop := X ∈ˢ univ 0 ∨ Strict X
when it is a truth value or strict, that is, neither the point nor a set holding the point. The members of a type are all the point or none of itwhitepaper/Fragment/Lib.lean:L359-L364359/-- The members of a type are all the point or none of them. -/
360theorem IsTy.eq_of_ne_pt {T x y : V} (hT : IsTy T) (hx : x ∈ˢ T) (hy : y ∈ˢ T)
361 (h : x ≠ pt → y ≠ pt → x = y) : x = y := by
362 rcases hT with hT | hT
363 · rw [eq_pt_of_mem_univ_zero hT hx, eq_pt_of_mem_univ_zero hT hy]
364 · exact h (ne_pt_of_mem_strict hT hx) (ne_pt_of_mem_strict hT hy)
, and this is the one fact about types the soundness proof reads. A sort denotes the types of its universewhitepaper/Fragment/Lib.lean:L304-L306304/-- **What `Sort n` denotes**: the truth values at `0`, the members of
305`univ n` that are types above. -/
306def typeU (n : Nat) : V := if n = 0 then univ 0 else sep (univ n) IsTy
: ${\mathrm{𝒯︀}}_0={\mathrm{𝒰︀}}_0$, the truth values, and ${\mathrm{𝒯︀}}_{𝑛}$ for $𝑛\ge 1$ the members of ${\mathrm{𝒰︀}}_{𝑛}$ that are types. These are cumulative, and ${\mathrm{𝒯︀}}_{𝑛+1}$ holds the truth values too. It must, since a function space over an empty domain is $\left\{\text{𝗉𝗍}\right\}$, which is no strict setwhitepaper/Fragment/ValueReading.lean:L58-L6358/-- A function space over an empty domain is `{pt}`, which is no strict set;
59so a positive sort, which holds `False → Nat`, holds a set that is not
60strict. -/
61theorem piV_empty_not_strict {A : V} {B : V → V} (h : ∀ x, ¬ x ∈ˢ A) :
62 ¬ Strict (piV A B) := by
63 rw [piV_of_empty h]; exact fun hs => hs.2 (mem_one.mpr rfl)
. The point is no type, so no sort holds it.

This is the whole of the interpretation. Nothing had to be well-typed, no typing judgement was consulted, and there is no partiality to discharge. The next subsection says what replaces typing. Three lemmas about the interpretation are needed later, each proved by induction on the term. Substituting a term for a variablewhitepaper/Fragment/Interp.lean:L242-L246242/-- **The β-substitution lemma**: substituting for the innermost
243variable is consing its value. -/
244theorem interp_inst0 (e a : Expr) (ρ : Nat → V) :
245 interp M φ ρ (e.inst a) = interp M φ (cons (interp M φ ρ a) ρ) e := by
246 rw [interp_inst, shiftE_zero_zero, instE_zero]
is extending the environment with the term’s value, $⟦𝑏\left[𝑥≔𝑎\right]{⟧}_{𝜌}=⟦𝑏{⟧}_{𝜌,𝑥\mapsto ⟦𝑎{⟧}_{𝜌}}$; hence a let denotes what its $𝜁$-reduct denoteswhitepaper/Fragment/Interp.lean:L248-L253248/-- **ζ is an identity**: a `let` denotes what its body with the value
249substituted denotes — at every environment, the point included (as β
250is at a lambda that is a graph; ζ has no lambda that could be the point). -/
251theorem interp_zeta (T v b : Expr) (ρ : Nat → V) :
252 interp M φ ρ (.letE T v b) = interp M φ ρ (b.inst v) := by
253 rw [interp_letE, interp_inst0]
, at every environment; and a term does not see a variable it does not mentionwhitepaper/Fragment/Hygiene.lean:L464-L467464/-- **Variables.** The interpretation of a term closed below `k` reads
465the environment below `k` only. -/
466theorem interp_closedAt {k : Nat} {e : Expr} (he : e.closedAt k = true) {ρ ρ' : Nat → V}
467 (h : ∀ i, i < k → ρ i = ρ' i) : interp M φ ρ e = interp M φ ρ' e := by
.

2.6. The semantic invariant

There is no typing judgement in the proof. In its place is a predicate on terms, the semantic invariant: a term is well-denotedwhitepaper/Fragment/WellDenoted.lean:L55-L7855/-- **The semantic invariant** (see the module docstring): a binder's
56domain is a type; a binder's codomain fibres are types; an application
57in the graph regime has a type as its slot's domain. -/
58def WellDenoted : (Nat → V) → Expr → Prop
59 | _, .bvar _ => True
60 | _, .sort _ => True
61 | _, .const _ _ => True
62 | ρ, .app f a =>
63 WellDenoted ρ f ∧ WellDenoted ρ a ∧
64 ∃ (p : Bool) (A : V) (B : V → V),
65 interp M φ ρ f ∈ˢ piR p A B ∧ interp M φ ρ a ∈ˢ A ∧
66 (p = true → ∀ x, x ∈ˢ A → B x ∈ˢ univ 0) ∧ (p = false → IsTy A)
67 | ρ, .lam A b =>
68 WellDenoted ρ A ∧ IsTy (interp M φ ρ A) ∧
69 (∀ x, x ∈ˢ interp M φ ρ A → WellDenoted (cons x ρ) b) ∧
70 ∃ B : V → V,
71 (∀ x, x ∈ˢ interp M φ ρ A → interp M φ (cons x ρ) b ∈ˢ B x) ∧
72 (∀ x, x ∈ˢ interp M φ ρ A → IsTy (B x))
73 | ρ, .pi A B =>
74 WellDenoted ρ A ∧ IsTy (interp M φ ρ A) ∧
75 (∀ x, x ∈ˢ interp M φ ρ A → WellDenoted (cons x ρ) B) ∧
76 (∀ x, x ∈ˢ interp M φ ρ A → IsTy (interp M φ (cons x ρ) B))
77 | ρ, .letE _ v b =>
78 WellDenoted ρ v ∧ WellDenoted (cons (interp M φ ρ v) ρ) b
when its applications and binders respect domains. It is stated under a valuation $𝜑$ and an environment $𝜌$, like the interpretation, by recursion on the term: it holds of a term when it holds of the subterms and one condition on the term’s own shape is met. We write $𝜌\vDash 𝑒$ for “$𝑒$ is well-denoted under $𝜌$” ($𝜑$ is fixed throughout). Variables and sorts are always well-denoted, and

In app, $𝑃$ is either a function space $\mathrm{\Pi }\left({𝐴}^{\prime },{𝐵}^{\prime }\right)$ whose domain ${𝐴}^{\prime }$ is a type, or a propositional function space ${\mathrm{\Pi }}_0\left({𝐴}^{\prime },{𝐵}^{\prime }\right)$ whose fibres are truth values. In lam, $𝐵$ is some family of types bounding the body’s values, its codomain. In words: an application applies a function, or a proof of a propositional $\forall$, to a member of its domain; a binder’s domain is a type; a lambda’s values lie in a bounded family of types, and a $\forall$‘s fibres are types. The invariant records which sets are types, and that is what makes the choice between the two readings agree with membership. An abstraction is a member of the function spacewhitepaper/Fragment/Lib.lean:L552-L558552/-- **Introduction**: body values in fibres that are types abstract into
553the function space. Where every fibre is a truth value every body value is
554the point, and so is the abstraction; where one fibre is not, it is
555strict, its body value is not the point, and the abstraction is the
556graph. -/
557theorem lamV_mem {A : V} {F B : V → V} (hF : ∀ x, x ∈ˢ A → F x ∈ˢ B x)
558 (hB : ∀ x, x ∈ˢ A → IsTy (B x)) : lamV A F ∈ˢ piV A B := by
of a family of types bounding its values: if every fibre is a truth value, every value is the point and so is the abstraction; if one fibre is not, it is strict, the body’s value there is not the point, and the abstraction is the graph.

The semantic invariant is transported by substitutionwhitepaper/Fragment/WellDenoted.lean:L196-L199196theorem WellDenoted_inst0 {e a : Expr} {ρ : Nat → V} (ha : WellDenoted M φ ρ a) :
197 WellDenoted M φ ρ (e.inst a) ↔ WellDenoted M φ (cons (interp M φ ρ a) ρ) e := by
198 have h := WellDenoted_inst M φ e a 0 ρ (by rwa [shiftE_zero_zero])
199 rwa [shiftE_zero_zero, instE_zero] at h
: $𝑏\left[𝑥≔𝑎\right]$ is well-denoted under $𝜌$ exactly when $𝑏$ is well-denoted under $𝜌,𝑥\mapsto ⟦𝑎{⟧}_{𝜌}$, provided $𝑎$ itself is. The proof is by induction on the term, using the interpretation’s substitution lemma; no typing derivation is involved.

A context $\mathrm{\Gamma }$, the list of the types of the variables in scope, is satisfiedwhitepaper/Fragment/WellDenoted.lean:L252-L259252/-- **Satisfaction of a context**: every entry is a well-denoted type
253under the environment beyond it, and the variable's value is a member
254of it. The semantic `Γ ⊢`. -/
255def Sat : List Expr → (Nat → V) → Prop
256 | [], _ => True
257 | A :: Γ, ρ =>
258 Sat Γ (fun i => ρ (i + 1)) ∧ WellDenoted M φ (fun i => ρ (i + 1)) A ∧
259 IsTy (interp M φ (fun i => ρ (i + 1)) A) ∧ ρ 0 ∈ˢ interp M φ (fun i => ρ (i + 1)) A
by $𝜌$ when every entry is well-denoted under the environment beyond it, denotes a type there, and has the variable’s value as a member. This is the semantic reading of “$\mathrm{\Gamma }$ is a well-formed context”, and it is the only thing the claims below assume about the context.

The first non-routine step is β. Take a well-denoted redex $\left(𝜆𝑥:𝐴.𝑏\right)𝑎$. From the application rule we know that the lambda’s value lies in some $𝑃$ whose domain ${𝐴}^{\prime }$ contains $⟦𝑎{⟧}_{𝜌}$; from the lambda rule we know that the body is bounded over $⟦𝐴{⟧}_{𝜌}$. For the β law we need $⟦𝑎{⟧}_{𝜌}\in ⟦𝐴{⟧}_{𝜌}$, the argument in the lambda’s own domain, and the semantic invariant has given us ${𝐴}^{\prime }$, not $𝐴$.

For a redex that does denote the point there is no such lemma. Its lambda may be the point, which carries no domain, and its argument may lie anywhere. Such a redex is well-denoted, and its reduct need not be: $\left(𝜆𝑥:𝐴.𝑔\left(𝑘𝑥\right)\right)𝑎$whitepaper/Fragment/EtaIota.lean:L707-L724707open EtaWit in
708/-- **Eta on the reduct of the major is outside the claims**.
709The major `maj := (fun x : A => g (k x)) a` is well-denoted
710and the point (a lambda that is the point constrains nothing, so `a` may
711lie outside `A`), and it β-reduces to `maj' := g (k a)`, which is not
712well-denoted (`k` is a graph over `A`). The redex `rec minor maj` is
713well-denoted and not the point. Eta-expanding the major's reduct,
714`minor (p0 maj')`, breaks the reduction claim; eta-expanding the major
715as it stands, `minor (p0 maj)`, satisfies it. So the checker's eta
716path must not reduce the major first (lean4#15371 expands before the
717major's `whnf`). -/
718theorem etaIota_reduced_major_witness [LevelOracle] (φ : Name → Nat) (env : Env)
719 (Γ : List Expr) :
720 Red env Γ maj maj' ∧
721 (∀ ρ : Nat → V, WellDenoted (witM (V := V)) φ ρ redex2 ∧ interp witM φ ρ redex2 ≠ pt ∧
722 interp witM φ ρ maj = pt) ∧
723 ¬ RedSem (EnvModel.empty (witM (V := V))) φ [] redex2 etaRed2 ∧
724 RedSem (EnvModel.empty (witM (V := V))) φ [] redex2 eta2 := by
, with a lambda that is the point and an argument $𝑎$ outside the domain $𝐴$ of the graph $𝑘$, reduces to $𝑔\left(𝑘𝑎\right)$, which is not well-denoted. So the reduction claim below says nothing about a term that denotes the point, and β needs no premise. Section 2.7 shows that the other rules need no more than such a claim.

Why no sort holds the point. The claims below rely on one fact: an inferred type is a type, so it is never the point. It also keeps β sound on stored values. A stored constant $𝑐:\text{𝖲𝗈𝗋𝗍}1$ whose value is the ill-typed redex $\left(𝜆ℎ:\left(\forall 𝑃:\text{𝖯𝗋𝗈𝗉}.𝑃\right).ℎ\right)\text{𝖯𝗋𝗈𝗉}$ reduces by δ and β to $\text{𝖯𝗋𝗈𝗉}$. The redex denotes the point (its lambda is an abstraction over an empty domain), and $\text{𝖯𝗋𝗈𝗉}$ does not. Such an environment has no modelwhitepaper/Fragment/UniformBeta.lean:L76-L8076/-- **The witness has no model**: the environment
77`c : Sort 1 := (λ (h : ∀ P : Prop, P). h) Prop` — its value denotes the
78point (an abstraction over an empty domain), and `Sort 1`'s members are
79types. -/
80theorem badEnv_no_model (m : EnvModel V badEnv) : False := by
: the constant’s set would have to be the point and a member of ${\mathrm{𝒯︀}}_1$, which holds no point.

2.7. The three claims and their proof

Reduction and equality assume the semantic invariant; inference establishes it. The inference rules are the ones that check a term’s shape, so their soundness proves that the term’s applications and binders respect domains; the other two relations are handed well-denoted terms and pass the semantic invariant along. The first two claims are also conditional on the point: they say nothing about a term that denotes it.

Why the claims may say nothing about the point. A claim that is silent about the point is only useful if every rule that uses a premise’s claim has that premise not the point, or does not need the claim there. Every rule falls into one of four cases.

1. The subject is a type, never the point. The reductions of an inferred type to a sort or a $\forall$ (in the binder rules, in app, in $𝜂$, in proof irrelevance), the comparisons of two types (an argument’s type with a domain in app, a domain with a domain in the congruences, the checker’s type comparisons in $𝜄$), the fibres compared in $\forall$-congruence. The third claim made each subject a type, so the conditional claim applies outright.
2. The subject is not the point by hypothesis. trans passes the first claim’s denotation on to the second; head reduces the head of an application that is not the point, which is therefore not the point either; red-l reduces a side of an equality that is not the point; app compares the heads of two applications that are not the point.
3. The two sides share a type, so they are both the point or neither. app’s arguments: the heads are one graph, whose domain is a type and holds both arguments. ι’s comparisons and its major premise (Section 4) are of the same kind. The bodies of lambda congruence and $𝜂$ are the one place where nothing else supplies a common type, and that is why those rules compare the bodies’ types (Section 2.8).
4. The step is an identity everywhere. β on a redex that is not the point (Lemma 1), $𝜁$ and δ (Section 3) claim nothing beyond what holds at every environment.

This is the statement the environment section builds on: a declaration is accepted when its value’s inferred type is definitionally equal to its declared type, and the corollary, with the second claim, puts the value’s set into the declared type’s set.

Proofs that are not proofs. The proof asks whether a term’s value is the point, never whether the term is a proof in Lean’s sense (except in the proof-irrelevance rule, whose claim turns out to be empty), and it learns that only through a type the term lies in. So a term whose value is the point is treated like a proof whatever the sort of its type, also when its value is the point only at some values of a variablewhitepaper/Fragment/Probe.lean:L65-L7265/-- `fun (P : Prop) (h : P) => c`, for `c` not the point: a graph, whose
66application at `False` is the point (an abstraction over an empty
67domain) and at `True` is not — a body whose point-ness varies with the
68variable. -/
69theorem mixed_lam {c : V} (hc : c ≠ pt) :
70 lamV (typeU 0) (fun P => lamV P fun _ => c) ≠ pt ∧
71 SetLib.app (lamV (typeU 0) (fun P => lamV P fun _ => c)) (truthVal False) = pt ∧
72 SetLib.app (lamV (typeU 0) (fun P => lamV P fun _ => c)) one ≠ pt := by
.

The three claims are proved together, by one structural inductionwhitepaper/Fragment/Sound.lean:L2202-L23112202theorem red_sound [LevelOracle] : ∀ {Γ : List Expr} {e e' : Expr},
2203 Red env Γ e e' → RedSem m φ Γ e e'
2204 | _, _, _, .refl => Red.refl_sound
2205 | _, _, _, .trans h₁ h₂ => Red.trans_sound (red_sound h₁) (red_sound h₂)
2206 | _, _, _, .appFn h => Red.appFn_sound (red_sound h)
2207 | _, _, _, .beta => Red.beta_sound
2208 | _, _, _, .zeta => Red.zeta_sound
2209 | _, _, _, .delta hfind hv hls => Red.delta_sound hfind hv hls
2210 | _, _, _, .iota hfind hkind hus hlen hpis hmaj hmeq hrl hctor hinst hcij husj hmlen hpis' hresM
2211 hIM hDM hdoms' htys' hI' hD' hlv hP hres hshape hrps hX =>
2212 Red.iota_sound rfl rfl hfind hkind hus hlen hpis (red_sound hmaj) hmeq hrl hctor hinst hcij husj
2213 hmlen hpis' hresM (infer_sound hIM) (defeq_sound hDM)
2214 hdoms' htys' (fun p hp => infer_sound (hI' p hp)) (fun p hp => defeq_sound (hD' p hp))
2215 hlv (fun p hp => defeq_sound (hP p hp)) hres hshape hrps
2216 (fun p hp => defeq_sound (hX p hp))
2217 | _, _, _, .iotaProp hfind hkind hus hlen hpis hmaj hmeq hrl hctor hinst hcij husj hmlen hpis' hresM
2218 hdoms' htys' hI' hD' hlv hP hres hshape hrps hX hI hlsI hpisI hsort hu =>
2219 Red.iotaProp_sound rfl rfl hfind hkind hus hlen hpis (red_sound hmaj) hmeq hrl hctor hinst hcij husj
2220 hmlen hpis' hresM hdoms' htys' (fun p hp => infer_sound (hI' p hp))
2221 (fun p hp => defeq_sound (hD' p hp)) hlv (fun p hp => defeq_sound (hP p hp)) hres hshape hrps
2222 (fun p hp => defeq_sound (hX p hp)) hI hlsI hpisI hsort hu
2223 | _, _, _, .iotaNested hfind hkind hus hlen hpis hmaj hmeq hrl hctor hinst hcij hcijk husj hmlen
2224 hpis' hresM hIM hDM hdoms' htys' hI' hD' _ _ _ hres hshape hrps hX =>
2225 Red.iotaNested_sound rfl rfl hfind hkind hus hlen hpis (red_sound hmaj) hmeq hrl hctor hinst
2226 hcij hcijk husj hmlen hpis' hresM (infer_sound hIM)
2227 (defeq_sound hDM) hdoms' htys' (fun p hp => infer_sound (hI' p hp))
2228 (fun p hp => defeq_sound (hD' p hp)) hres hshape hrps (fun p hp => defeq_sound (hX p hp))
2229 | _, _, _, .iotaSlot hfind hkind hus hlen hpis hmaj hmeq hrl hctor hinst hcij husj hmlen hpis' hresM
2230 hdoms' htys' hI' hD' hlv hP hres hshape hrps hX =>
2231 Red.iotaSlot_sound rfl rfl hfind hkind hus hlen hpis (red_sound hmaj) hmeq hrl hctor hinst hcij husj
2232 hmlen hpis' hresM hdoms' htys' (fun p hp => infer_sound (hI' p hp))
2233 (fun p hp => defeq_sound (hD' p hp)) hlv (fun p hp => defeq_sound (hP p hp)) hres hshape hrps
2234 (fun p hp => defeq_sound (hX p hp))
2235 | _, _, _, .iotaNestedSlot hfind hkind hus hlen hpis hmaj hmeq hrl hctor hinst hcij hcijk husj hmlen
2236 hpis' hresM hdoms' htys' hI' hD' _ _ _ hres hshape hrps hX =>
2237 Red.iotaNestedSlot_sound rfl rfl hfind hkind hus hlen hpis (red_sound hmaj) hmeq hrl hctor hinst
2238 hcij hcijk husj hmlen hpis' hresM hdoms' htys' (fun p hp => infer_sound (hI' p hp))
2239 (fun p hp => defeq_sound (hD' p hp)) hres hshape hrps (fun p hp => defeq_sound (hX p hp))
2240 | _, _, _, .iotaStrict hfind hkind hus hlen hpis hmaj hmeq hrl hctor hinst hcij husj hmlen hpis'
2241 hresM hdM hI₀ hk₀ hls₀ hd₀ hpis₀ hlvl hlv hP hres hshape hrps hX =>
… 70 more lines over the three mutually inductive relations (as in con-lecheConLeche/Model/Rules/Sound.lean:L49-L5049theorem red_sound (hin : RulesInputs V m φ) :
50 ∀ {d : Nat} {e e' : Expr}, Red env d e e' → RedSem m φ d e e'
). Every rule is one case, and every case is a lemma about that rule alone, with the induction hypothesis for each premise as an assumption. The routine cases are listed at the end; the others follow.