# Formal statements in a proof assistant: reading a Lean statement layer by layer and separating 'is a statement' from 'is proved'

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-lean-formal-statement/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-lean-formal-statement-01 · production-20261019-adopted-96



## Goal and scope

Take the source string s: `∀ (a b : Nat), a ≤ b → a < b + 1` as a teaching object and, in an environment E that is fixed explicitly but never executed, explain layer by layer: its bound variables and their types, its hypothesis and conclusion, the core term S that elaboration would have to produce if it succeeded, why S would have type Prop, and what a proof term would have to establish; then give an informal proof of its mathematical content and contrast it with s′: `∀ (a : Nat), a - 1 < a` (a Prop, but false) and s″: `∀ (a : Int), a - 1 < a` (true). Lean is not run at any point, and nothing here claims that any text parses, elaborates, compiles or is proved by Lean.

Works inside the MKO's scope: statement identity includes the Lean version, imports, name environment and local context (assumption a1); Lean is paused by the owner's instruction, so this guide gives only conceptual explanation and hand type analysis and produces no elaboration or kernel receipt (assumption a2). The cited Lean notation and typing rules carry citation_verified; the canonical MKO and its English edition are not changed.





## Givens and symbols


- order_basics
- numeric_evaluation
- def_unfold


- G1 — Environment E=(V,I,N,Γ): V is a specified Lean 4 version (to be recorded in a receipt when Lean work resumes; not pinned here); I is no imports beyond the Lean 4 core prelude; N is the names declared by that prelude; Γ is the empty local context. All four are part of statement identity (MKO assumption a1).
- G2 — Lean is not run in this guide (owner instruction; MKO assumption a2): no parsing, elaboration, type checking or kernel check was executed. Every sentence below about these stages is either a definition of what the stage must establish or a hand analysis conditional on that stage succeeding.
- G3 — The source string s = `∀ (a b : Nat), a ≤ b → a < b + 1`. Declaring a theorem would further require 'theorem t : s := p' with a proof p; this guide discusses only the statement after the colon.
- G4 — Contrast strings s′ = `∀ (a : Nat), a - 1 < a` and s″ = `∀ (a : Int), a - 1 < a`, read in the same E.


- E=(V,I,N,\Gamma) — the environment: Lean version, imports, name environment, local context
- s — the source string (text not yet parsed)
- S — the core term elaboration would produce if it succeeded
- \Gamma\vdash S:\mathrm{Prop} — in Γ, S has type Prop
- p — a candidate proof term of S
- \mathsf{Elab},\ \mathsf{Kernel} — the elaboration and kernel-check stages
- \mathrm{Nat},\ \mathrm{Int} — Lean's natural-number and integer types





## Rules and sources


- order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
- numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
- def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
- def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
- forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
- forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
- imp_intro · prerequisite — →-introduction (discharging a hypothesis): if Q is derived inside a scope that temporarily assumes P, then P⇒Q follows, and P may no longer be used as known.
- case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
- eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
- quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
- mko_lean_formal_statement_def · cited — In a fixed Lean version, with fixed imports, name environment and local context Γ, source syntax s expresses a formal statement if it elaborates successfully to a core term S with Γ⊢S:Prop. A statement and the existence of its checked proof term are separate states. · mko-lean-formal-statement
- mko_proposition_def · cited — A proposition P may be true or false; being a proposition does not mean that P has been proved true. · mko-proposition
- lean_stages · cited — Lean 4 processes source in stages: parsing turns text into syntax; elaboration turns syntax into a core term, resolving names, notation, implicit arguments and type-class instances, and may fail; type checking infers the core term's type; for a theorem declaration the kernel checks that the supplied proof term has the stated type. Success at one stage does not guarantee success at a later one. · Lean Language Reference, Elaboration and Compilation, Sections 2.1-2.3
- lean_core_notation · cited — In Lean 4 core, a ≤ b is notation for LE.le a b, a < b for LT.lt a b, a + b for HAdd.hAdd a b, a - b for HSub.hSub a b, and the numeral 1 for OfNat.ofNat 1; LE.le and LT.lt have type α → α → Prop. + binds more tightly than ≤ and <, which bind more tightly than →; → associates to the right; a ∀ extends as far right as possible; (a b : Nat) declares two bound variables of type Nat. The core prelude provides instances of these classes for Nat and Int. · Lean 4 v4.30.0 Init/Notation.lean; Lean Language Reference Basic Classes; Init.Prelude API
- prop_formation · cited — Rules of Lean's type theory: (i) if Γ⊢A:Prop and Γ⊢B:Prop then Γ⊢(A→B):Prop; (ii) if Γ⊢α:Sort u and Γ,x:α⊢B:Prop then Γ⊢(∀x:α, B):Prop (impredicativity of Prop); Nat : Type and Int : Type, where Type = Sort 1. · Theorem Proving in Lean 4, Chapters 3 and 4, Sections 3.1 and 4.1
- curry_howard · cited — Propositions as types: a proof of ∀x:α, B is a function sending each x:α to a proof of B; a proof of A→B is a function sending each proof of A to a proof of B; p : S means p is a term of type S. · Theorem Proving in Lean 4, Sections 3.1 and 4.1
- nat_trunc_sub · cited — In Lean 4 core, subtraction on Nat is truncated: a−b=0 when a≤b, and the usual difference otherwise; in particular 0−1=0. Subtraction on Int is the usual ring subtraction. · Lean 4 Init.Prelude API, Nat.sub; Lean Language Reference, Integers, Int.sub
- L_main · lemma — For all natural numbers a and b: if a≤b then a<b+1.





## Main derivation

S01 · definitionBefore

s,\ E

After

E=(V,I,N,\Gamma),\quad \Gamma=\varnothing

Conditions: \text{Lean not run (G2)}

Rule: def_intro · Uses: G1, G2

Leaf basis: def_intro + mko_lean_formal_statement_def

First write the environment as a 4-tuple and name it. MKO assumption a1 says that version, imports, declared names and local context all belong to statement identity, so every judgement about s must carry E. G2 records that this tuple is fixed on paper only and no toolchain was invoked.



S02 · definitionBefore

s

After

\mathsf{Parse}(s)\ ;\ \mathsf{Elab}(s)=S\ ;\ \Gamma\vdash S:\mathrm{Prop}\ ;\ \Gamma\vdash p:S\ ;\ \mathsf{Kernel}(p,S)

Conditions: none

Rule: lean_stages · Uses: S01, G3

Leaf basis: lean_stages + def_intro

Name five states: s is parsed; s elaborates to a core term S; S has type Prop; a proof term p:S exists; p passes the kernel check. Each later state presupposes the earlier ones, but no earlier state implies a later one. The misconception identified in the MKO is merging these states into one. At the start of this guide all five are 'not executed'.



S03 · impliesBefore

s=\texttt{∀ (a b : Nat), a ≤ b → a < b + 1}

After

\forall a:\mathrm{Nat},\ \forall b:\mathrm{Nat},\ \bigl((a\le b)\to(a<(b+1))\bigr)

Conditions: \text{notation and precedence of E as cited}

Rule: lean_core_notation · Uses: S02, G3

Leaf basis: lean_core_notation

Read the structure by hand using the cited notation and precedence conventions: (a b : Nat) is two nested universal binders; the ∀ extends to the end of the string; + binds more tightly than <, so a < b + 1 is a<(b+1); ≤ and < bind more tightly than →, so the two sides of → are a≤b and a<b+1. The reading: for all natural numbers a and b, if a≤b then a<b+1. This is a manual reading according to the conventions, not the output of running the parser (G2).



S04 · impliesBefore

\forall a\,b:\mathrm{Nat},\ a\le b\to a<b+1

After

S=\forall a\,b:\mathrm{Nat},\ \mathrm{LE.le}\,a\,b\to\mathrm{LT.lt}\,a\,(\mathrm{HAdd.hAdd}\,b\,(\mathrm{OfNat.ofNat}\,1))

Conditions: \mathsf{Elab}(s)\ \text{succeeds (not run)}

Rule: lean_core_notation · Uses: S03

Leaf basis: lean_core_notation + lean_stages

Describe what elaboration must produce if it succeeds: replace each notation by its constant and fill in the implicit type argument Nat and the instance arguments (LE Nat, LT Nat, HAdd Nat Nat Nat, OfNat Nat 1); the displayed term omits these implicit arguments. This describes elaboration's task; whether it succeeds, and the exact instance names, are not checked here.



S05 · theorem_applicationBefore

S

After

\Gamma\vdash S:\mathrm{Prop}\quad(\text{conditional on}\ \mathsf{Elab}(s)=S)

Conditions: \mathsf{Elab}(s)=S

Rule: prop_formation · Uses: S04

Leaf basis: prop_formation + lean_core_notation

Given the shape from S04, the typing rules show layer by layer that S has type Prop: first the two atomic propositions (S05.1), then the implication (S05.2), finally the two universal quantifiers (S05.3). This is a hand type analysis, not the output of the type checker.



S06 · impliesBefore

\mathsf{Elab}(s)=S\ \wedge\ \Gamma\vdash S:\mathrm{Prop}

After

s\ \text{expresses a formal statement in}\ E

Conditions: \mathsf{Elab}(s)=S\ \text{(not run)}

Rule: mko_lean_formal_statement_def · Uses: S05, S02

Leaf basis: mko_lean_formal_statement_def + lean_stages

Apply the MKO definition as a conditional: if s elaborates in E to S with Γ⊢S:Prop, then s expresses a formal statement in E. The typing half of the antecedent was obtained by hand in S05, assuming elaboration succeeds; elaboration itself was not run (G2). The recorded status is therefore 'expected to express a formal statement in E; elaboration receipt missing'.



S07 · definitionBefore

\Gamma\vdash p:S

After

p=\lambda (a\,b:\mathrm{Nat})\,(h:a\le b).\ q,\quad a,b:\mathrm{Nat},\ h:a\le b\ \vdash\ q:a<b+1

Conditions: none

Rule: curry_howard · Uses: S04

Leaf basis: curry_howard

By propositions as types, a proof term of S is a function: it takes arbitrary a, b : Nat and a proof h of the hypothesis a≤b, and returns a proof q of a<b+1. The bound variables a and b are data and h is the hypothesis; the obligation is to produce, for arbitrary a, b and h, a proof of a<b+1. This is exactly the shape of the informal proof in S09.



S08 · impliesBefore

\forall a\,b,\ a\le b\to a<b+1

After

(a,b)=(3,3):\ 3\le 3\to 3<4;\quad (a,b)=(5,2):\ 5\le 2\to 5<3

Conditions: none

Rule: forall_elim · Uses: S03

Leaf basis: forall_elim + numeric_evaluation

Use two instances to see what the statement says. For a=b=3 the hypothesis 3≤3 holds and the conclusion 3<4 holds too. For a=5, b=2 the hypothesis 5≤2 fails, and the statement demands nothing about 5<3 for this pair (in the classical reading the implication is vacuously true). The hypothesis restricts which pairs the conclusion is claimed for.



S09 · theorem_applicationBefore

\forall a,b\in\mathbb{N},\ a\le b\Rightarrow a<b+1

After

\text{true in}\ \mathbb{N}\ \text{(informal proof)}

Conditions: none

Rule: L_main · Uses: S03

Leaf basis: order_basics + forall_intro + imp_intro

Apply Lemma L_main (proved in S09.1 and S09.2): in the standard natural numbers the mathematical content of the statement holds. This is an informal mathematical proof and corresponds to the plan for constructing q in S07.



S10 · impliesBefore

\text{informal proof of the content of}\ S

After

\mathsf{Parse},\ \mathsf{Elab},\ \mathsf{Kernel}:\ \text{not run};\ p:\ \text{not constructed}

Conditions: none

Rule: mko_lean_formal_statement_def · Uses: S06, S07, S09

Leaf basis: mko_lean_formal_statement_def + lean_stages + mko_proposition_def

Collect the states. S09 proved that the mathematical content of the statement is true in standard ℕ and gave the plan for q in S07; but it is not a Lean proof term and nothing passed a kernel check. So the status table is: parsing not run; elaboration not run; Prop typing by hand analysis only (S05, conditional on elaboration); proof term not constructed; kernel check not run. By the MKO, a formal statement and its checked proof term are separate states, and this guide advances only the conceptual analysis of the former.



S11 · impliesBefore

s'=\texttt{∀ (a : Nat), a - 1 < a}

After

\Gamma\vdash S':\mathrm{Prop}\quad(\text{conditional on}\ \mathsf{Elab}(s'))

Conditions: \mathsf{Elab}(s')\ \text{succeeds (not run)}

Rule: prop_formation · Uses: G4, S05

Leaf basis: prop_formation + lean_core_notation

Redo the type analysis of S05 for s′: a−1 is a value of HSub Nat Nat Nat with type Nat; LT.lt (a−1) a : Prop; quantifying over a : Nat still gives a Prop. So if s′ elaborates, it too expresses a formal statement.



S12 · impliesBefore

\forall a:\mathrm{Nat},\ a-1<a

After

a=0:\ 0-1=0,\ \neg(0<0)\ \Rightarrow\ \neg\forall a,\ a-1<a

Conditions: \text{truncated subtraction on Nat}

Rule: quantifier_negation · Uses: S11

Leaf basis: nat_trunc_sub + quantifier_negation + order_basics

Under truncated subtraction on Nat, a=0 gives 0−1=0 (S12.1), and 0<0 fails (S12.2). A counterexample exists, so by quantifier negation the content of S′ is false in the standard reading. S′ is a Prop (S11) but not a true one: being a proposition does not mean being proved true (mko_proposition_def).



S13 · impliesBefore

s''=\texttt{∀ (a : Int), a - 1 < a}

After

\forall a\in\mathbb{Z},\ a-1<a\ \text{(true)};\quad S''\ne S'

Conditions: \text{ring subtraction on Int}

Rule: order_basics · Uses: G4, S12

Leaf basis: order_basics + nat_trunc_sub

On Int subtraction is the usual ring subtraction. For every integer a, −1<0, and adding a to both sides gives a−1<a, so the content of S″ is true. s′ and s″ differ only in one type name, but the bound variable's type and the subtraction differ, so they are different core terms with different truth values. Types and environment are part of statement identity (MKO assumption a1).



S14 · impliesBefore

t_0=\texttt{a ≤ b → a < b + 1}

After

\text{meaning of}\ t_0\ \text{depends on}\ \Gamma\ \text{and elaborator options}

Conditions: none

Rule: mko_lean_formal_statement_def · Uses: S01, S03

Leaf basis: mko_lean_formal_statement_def + lean_stages

Take the text t0 without binders. If the local context is Γ′=(a b : Nat), t0 would be read as a statement about those two local variables; in E's empty Γ, a and b are not declared names, so elaboration may fail or may treat them differently depending on elaborator options (such as automatic implicit binding), and this guide does not predict which. So a receipt must record Γ and the options; the same text in different contexts is not the same statement.







## Substeps and lemmas

S05.1 · impliesBefore

\Gamma_1=(a:\mathrm{Nat},\ b:\mathrm{Nat})

After

\Gamma_1\vdash b+1:\mathrm{Nat},\ \Gamma_1\vdash a\le b:\mathrm{Prop},\ \Gamma_1\vdash a<b+1:\mathrm{Prop}

Conditions: none

Rule: lean_core_notation · Uses: S04

Leaf basis: lean_core_notation

In the context Γ1 obtained by adding the two bound variables: the output type of HAdd Nat Nat Nat is Nat, so b+1 : Nat; LE.le and LT.lt have type Nat → Nat → Prop, and applying them to two Nat terms gives a Prop.



S05.2 · impliesBefore

\Gamma_1\vdash a\le b:\mathrm{Prop},\ \Gamma_1\vdash a<b+1:\mathrm{Prop}

After

\Gamma_1\vdash (a\le b\to a<b+1):\mathrm{Prop}

Conditions: none

Rule: prop_formation · Uses: S05.1

Leaf basis: prop_formation

By rule (i): an implication between two Props is a Prop.



S05.3 · impliesBefore

\Gamma_1\vdash (a\le b\to a<b+1):\mathrm{Prop}

After

\Gamma\vdash \forall a:\mathrm{Nat},\ \forall b:\mathrm{Nat},\ (a\le b\to a<b+1):\mathrm{Prop}

Conditions: \mathrm{Nat}:\mathrm{Type}=\mathrm{Sort}\ 1

Rule: prop_formation · Uses: S05.2

Leaf basis: prop_formation

Apply rule (ii) twice: first bind b in the context (a:Nat), giving ∀b:Nat, (a≤b → a<b+1) : Prop; then bind a in the empty context Γ. Since Nat : Type and Prop is impredicative, quantifying a Prop over any type gives a Prop. The three sub-steps together give the conclusion of S05.



S09.1 · impliesBefore

0<1

After

b<b+1

Conditions: b\in\mathbb{N}

Rule: order_basics · Uses: order_basics

Leaf basis: order_basics

From 0<1, add b to both sides (order is preserved by addition) to get b<b+1. View ℕ inside ℝ with the same order.



S09.2 · impliesBefore

a\le b,\ b<b+1

After

a<b+1

Conditions: a\le b

Rule: case_analysis · Uses: S09.1, order_basics

Leaf basis: case_analysis + order_basics + eq_replace + imp_intro + forall_intro

a≤b means a<b or a=b. If a<b, transitivity with b<b+1 gives a<b+1; if a=b, replacing b by a in b<b+1 gives a<b+1 directly. Both cases reach the conclusion; since a and b were arbitrary, discharging the hypothesis and generalizing proves L_main.



S12.1 · impliesBefore

0-1\ \text{in Nat}

After

0-1=0

Conditions: 0\le 1

Rule: nat_trunc_sub · Uses: nat_trunc_sub

Leaf basis: nat_trunc_sub

Since 0≤1, truncated subtraction gives 0−1=0, not −1; −1 is not a natural number.



S12.2 · equivalentBefore

0-1<0

After

0<0,\ \text{which is false}

Conditions: none

Rule: eq_replace · Uses: S12.1, order_basics

Leaf basis: eq_replace + order_basics

Replacing 0−1 by 0, the claim 0−1<0 is equivalent to 0<0; by trichotomy, 0=0 rules out 0<0.







## Reverse audits


- S14 · premise_audit · S01, mko_lean_formal_statement_def, lean_stages — This step states only the dependence and claims no actual elaboration result for t0 in any environment.
- S13 · premise_audit · G4, nat_trunc_sub, order_basics — It needs the usual definition of subtraction on Int (cited) and that order is preserved by addition. N6 checks a finite range only and does not replace the universal proof.
- S12.2 · inverse_equivalence · S12.1, eq_replace — Replacing an expression by an equal one does not change truth, so both directions hold.
- S12.1 · premise_audit · nat_trunc_sub — The conclusion depends on the definition of subtraction on Nat; in Int the same expression equals −1 (see S13).
- S12 · premise_audit · nat_trunc_sub, quantifier_negation, mko_proposition_def — It needs the cited definition of truncated subtraction (citation_verified). One counterexample suffices to refute a universal statement (recomputable as N4, N5).
- S11 · premise_audit · G4, prop_formation, lean_core_notation — As in S05 this is a hand analysis conditional on elaboration succeeding; the conclusion goes only as far as 'is a Prop'.
- S10 · premise_audit · S06, S07, S09, mko_lean_formal_statement_def, G2 — The role of this step is to block promotion: mathematical truth and an informal proof do not imply that Γ⊢p:S has been accepted by the kernel.
- S09.2 · premise_audit · S09.1, order_basics, case_analysis, imp_intro, forall_intro — The two cases cover every way a≤b can hold; no converse is claimed (a<b+1 ⇒ a≤b does hold in ℕ, but it is neither used nor proved here).
- S09.1 · premise_audit · order_basics — Only u<v ⇒ u+w<v+w is used.
- S09 · premise_audit · L_main — The conclusion is a mathematical fact about standard ℕ, not about any Lean state; it produces no proof term and passes through no kernel check. N3 is a finite check on the 49 pairs from 0 to 6 only and does not replace the proof of the lemma.
- S08 · premise_audit · S03, forall_elim — Instantiation only applies the universal statement to particular values; two instances cannot prove the universal statement (N1, N2 check only these numbers).
- S07 · premise_audit · S04, curry_howard — This step only describes the shape a proof term must have; no p is constructed and nothing is kernel-checked.
- S06 · premise_audit · S05, mko_lean_formal_statement_def, G2 — This step does not claim the antecedent holds, so the consequent cannot be treated as confirmed. Nor does it claim S is true or proved: being a statement and being proved are separate states.
- S05.3 · premise_audit · S05.2, prop_formation — It needs Nat to be a type (Sort 1) and rule (ii). The conclusion is that S lies in Prop, which says nothing about whether S is provable.
- S05.2 · premise_audit · S05.1, prop_formation — Only both sides being Props is needed; the implication is not claimed to be true.
- S05.1 · premise_audit · lean_core_notation — It needs the cited type signatures of LE, LT and HAdd. It says only that a≤b is a proposition, not that it is true.
- S05 · premise_audit · S04, prop_formation — It needs the conditional premise of S04 and the cited typing rules; if elaboration produced a different term, this analysis would have to be redone.
- S04 · premise_audit · S03, lean_core_notation, G2 — This step is conditional on Elab(s) succeeding. If E lacked any of the instances or notations, elaboration would fail and S would not exist at all.
- S03 · premise_audit · G3, lean_core_notation — The reading depends on the notation and precedence in E; different imports could redefine notation and give a different structure (MKO paragraph 2). It is not claimed that the parser accepts s.
- S02 · premise_audit · lean_stages, mko_lean_formal_statement_def — The division into stages comes from the cited Lean documentation (citation_verified). This step only defines names for the states and claims none of them has been reached.
- S01 · premise_audit · G1, G2, mko_lean_formal_statement_def — This step only names and derives no new fact. V is not pinned yet; that is an open item and does not affect the conditional analysis below, which treats E as a parameter.





## Error controls and negative controls

Four states are not one thingThe misconception identified in the MKO is treating successful parsing, successful elaboration, having type Prop and a kernel-checked proof as one thing. S02 separates them into five states; s′ shows that even if the early states are reached (should elaboration succeed), the statement can be false and so have no proof. This guide contains hand analysis only; no state was executed.

The same text is not the same statements′ and s″ differ only in Nat versus Int, yet they are different core terms, one false and one true (S12, S13); t0 means different things in different local contexts (S14). Comparing statements requires comparing environments and core terms, not strings.

An informal proof is not a checked proof termThe argument in S09 proves the mathematical content and gives a construction plan for the proof term (S07), but it is not a Lean term and has not passed the kernel. Reporting it as 'proved by Lean' would be a false promotion.


- s looks like valid Lean, so it elaborates in every environment → reject — Elaboration depends on version, imports, notation, instances and local context (MKO assumption a1); and elaboration was not run in this guide.
- S has type Prop, so S is proved → reject — S′ is also a Prop, yet it is false at a=0: 0−1=0 and 0<0 fails.
- This guide shows that s compiles and that the theorem is proved by Lean → reject — G2: Lean was not run, and there is no parse, elaboration or kernel receipt.
- s′ and s″ differ only in a type name, so they are the same statement → reject — The types and the subtraction differ; s′ is false at a=0 while s″ is true for every integer.





## Result and limitations

s reads 'for all natural numbers a and b, if a≤b then a<b+1': two Nat bound variables, one hypothesis a≤b and one conclusion a<b+1. If elaboration succeeds in E, the typing rules give the core term S type Prop, so s expresses a formal statement; a proof term must be a function taking a, b and h:a≤b to a proof of a<b+1. Its mathematical content is true in standard ℕ (informal proof). Lean was not run: parsing, elaboration, proof term and kernel check are all 'not executed'. s′ is a Prop but false at a=0 and s″ is true, showing that types and environment belong to statement identity.


- When the owner resumes Lean work, pin the toolchain version and import closure and record parse and elaboration receipts for s, s′ and s″; proving s would require constructing a proof term and obtaining a kernel receipt (MKO formal next).
- The core term shown in S04 omits implicit and instance arguments; its exact form, including instance names, requires actual elaboration. The cited notation, typing rules and truncated subtraction have been checked against official Lean documentation and the listed core sources. Lean was not run and no elaboration or kernel receipt was obtained.





## Verification and source binding

6 declared checks for this guide; only the listed expressions are covered.


- source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
- adopted source SHA-256: 5cb0d5f28f6aea7530d0c886c4ff344564b3ecefcd4d14d3748e25c6afef4cd2
- original source SHA-256: 5cb0d5f28f6aea7530d0c886c4ff344564b3ecefcd4d14d3748e25c6afef4cd2
- Lean: NOT_RUN · independent AI: NOT_MEASURED

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-lean-formal-statement-01.json)