Verification tiers
From the documentation of the field
Not every claim on this site rests on the same kind of support. This page says what machine verification in Lean 4, the strongest kind, establishes. It then sorts the field's claims into tiers, so a reader knows how each is supported.
What Lean 4 checks
Lean 4 is a proof assistant, and Mathlib is its large library of formalised mathematics. A proof is accepted only when the Lean kernel, a small program, has checked every step. Nothing is accepted on reputation, and no person's judgement enters the check. In this project every theorem is proved from Mathlib's own axioms, the same foundational axioms that every Mathlib result rests on.
Four constructs would leave a result unproved or assumed, and the repository contains none of them. A sorry is a placeholder that promises a proof later. An axiom adds a new assumption without proof. An opaque definition hides its contents from the checker. A linter suppression switches off an automated warning.
What can be counted
As of the repository state on 2026-10-01, the Lean source is 12,667 lines across seven files:
| File | Lines | Contents |
|---|---|---|
SixPrimitives/Phase0.lean |
259 | Framework types and the six failure conditions |
SixPrimitives/Phase1.lean |
1,603 | Supporting lemmas in probability and analysis |
SixPrimitives/Phase2.lean |
4,842 | Trajectory measure and the witness environments |
SixPrimitives/Phase2CMI.lean |
1,029 | Conditional mutual information |
SixPrimitives/Phase3.lean |
2,600 | Part I, necessity |
SixPrimitives/Phase4.lean |
1,534 | Part II, independence |
SixPrimitives/Phase5.lean |
800 | Part III, sequential dependence |
Across those files there are zero sorry, zero axiom, zero opaque and zero linter suppressions. The toolchain is leanprover/lean4:v4.30.0, built against Mathlib v4.30.0. The code contains one set_option, in Phase2.lean, which raises a time limit for instance search. It does not switch off any check.
Every one of these facts is countable by a reader. Audit it yourself shows how.
What machine verification establishes
Given the definitions, every theorem follows. No step is missing, and no assumption is hidden beyond Mathlib's axioms. For Parts I and II this holds without conditions: they are proofs about the minimal witness environments, and Lean also proves that each witness environment exhibits the structural property it is said to witness, and so satisfies the formal Class C predicate. For Part III the theorems are machine-verified but conditional. Each states its hypotheses, and the Implementation Obligations are hypotheses that the paper states and does not discharge.
It also puts every reader on the same footing. Anyone can rebuild the project and obtain the same result, and the checks are public.
Questions beside the formal check
The formal check establishes what the theorems say. Five further questions sit beside it, and each has its own answer.
- Definitions and their plain meaning. Lean proves what the definitions say. The definitions are public, and a reader can set each beside its plain reading. Audit it yourself begins there.
- Membership. Whether a given organisation is in Class C is a question of fact about a real structure. The field's position on business decision-making is an argument, set out on the Class C page, and it is not a theorem.
- Assessment. A specific assessment applies the definitions to a real structure with judgement. Error theory sets out where an assessment is checked.
- Larger environments. The theory (Ismail's Primitives) applies to any environment containing a difficulty, however complex. The formalisation proves it in the smallest environment that exhibits each difficulty, and the step to larger environments is the standard reduction of lower-bound theory.
- Sufficiency. Part III is a formally-verified bridge towards sufficiency, and it is conditional by design. See necessity and sufficiency.
The four tiers
Every claim on this site sits in one of four tiers, which are Ismail's own.
| Tier | What it covers | Examples | How it is examined |
|---|---|---|---|
| Machine-verified | Results the Lean kernel has verified. For Part III the results are verified conditional on their stated hypotheses. | Part I necessity and Part II independence in the minimal witness environments; the witness environments' satisfaction of the formal Class C predicate; Part III, with its Implementation Obligations; the line and construct counts | Rebuild the project; read the statements, definitions and stated hypotheses |
| Paper-proved | Results established by argument in the paper, or taken from the standard literature the paper relies on, and not formalised in Lean | The reduction that carries a result from the minimal environment to any larger environment containing the same difficulty | Read the argument in the paper and in the lower-bound literature it draws on |
| Domain readings | The theory read into a domain, or into plain language | The plain-language meanings of the definitions; the position that business decision-making sits inside Class C; the mapping of methodologies to the primitives of Ismail's Primitives; error theory; the criteria pages' lists of evidence | Test the reading against counterexamples and better arguments |
| Guide-invented methods | Methods devised for carrying out an assessment, such as how evidence is gathered and weighed | None appear on these pages. The field states criteria and not methods. | Not applicable here |
Sources the site cites, such as the Dossier's articles, sit outside the tiers of the theory (Ismail's Primitives): they are evidence about the world, given with their source and date and read through the Credibility Checker.
A machine-verified claim can be checked by building the code. The other three tiers cannot, and no amount of machine verification changes that.
| The field | |
|---|---|
| Pages | The QuestionField definitionClass CWhy a POMDPNecessity and sufficiencyVerification tiersAudit it yourselfMethodologiesCompetenceError theoryThree-party verificationAdjacent fields |