Competence

From the documentation of the field

The mathematics in this field is machine-verified in Lean 4, and the checks are public. Why nobody is expected to redo the formalisation is set out in audit it yourself. A reader can evaluate those checks for themselves. This page says what that takes, what is needed beyond it to assess a real structure or to extend the results, and how a person shows that they have it. The bar is high. It is uncommon, and it is not out of reach. Every discipline named here is taught, published and learnable. What is uncommon is the combination.

Qualification by proof

The people who approve an application of this work, and who evaluate an engagement afterwards, hold those roles on proof. The proof is trackable artefacts: public, dated, versioned and reproducible, so that anyone can inspect them without trusting the holder. A formal development that rebuilds, a repository with a visible history, and a paper whose numbered results are each mapped to a formal identifier are examples.

A credential, an institutional affiliation or a referral does not count. A credential shows what someone was trained in. A referral shows that someone is willing to vouch. Neither shows that the person can do the work. Ismail's Credibility Checker applies the same reasoning to claims, in its rules on social signals and on institutional authority.

The reason is specific to this field. The results are impossibility theorems. For a structure in Class C that lacks a required capability, loss grows in proportion to time, however well the rest of the structure is built. An approval that anyone holding the right credential or the right referral could give would let a missing capability pass unseen. The approval has to mean something that can be checked, and proof is what makes it checkable.

The author holds the approving role on this basis, and the artefacts are listed on the author page. Any other person can step into the approving role, or into the evaluating role, by presenting artefacts of the same type and at the same depth in each discipline below. The roles are open to a person who can present that proof. They are closed to one who cannot, whatever else that person holds. The field does not depend on any one person, including its founder.

Five roles

The competence required depends on what a person is doing.

Role	What it involves	What it needs
Evaluating the checks	Reading theorem statements and definitions, following each definition to where it is defined, confirming the counts, and rebuilding the project. Audit it yourself is the route.	Enough Lean 4 to read statements and definitions, and enough probability and information theory to read a definition against its plain meaning. It does not need the ability to write proofs, because the kernel has checked them.
Assessing a structure	Applying the field's tests to a real structure: deciding which of the six difficulties are present, telling a mechanism from an artefact, and stating a verdict with its scope.	Everything needed for evaluating the checks, plus knowledge of how decisions are actually made in the setting being assessed, the discipline of keeping proved, argued and read claims apart, and a working grasp of error theory.
Approving	Judging that an application of the work uses the definitions and the theorems the way the mathematics requires. This is the second link in three-party verification.	The assessing role, at the depth set out in the table on proof below, shown by artefacts.
Evaluating an engagement	Taking an engagement apart after it ends: establishing where the primitives of Ismail's Primitives were applied, in what capacity and with what output, and measuring the effect in the client's situation against the published standard. This is the third link.	The assessing role, at the same depth, shown by artefacts, and independence from the application being evaluated. It does not need the client to understand the mathematics.
Extending the theory (Ismail's Primitives)	Constructing new results: new environments, new lower bounds, further links.	All of the disciplines below at the level of construction, not only reading.

A person who can recite the six capabilities but cannot read the definitions behind them is not qualified to assess. That is the sense of "a qualified person" on the field definition page.

The disciplines

Discipline	Specific pieces required	Where it appears in the work
Formal verification in Lean 4 and Mathlib	Reading statements and definitions; finding a definition in a library of roughly nine thousand modules; reading structures built from kernels and measures; running a reproducible build. For extension, writing proofs at the scale of this project, about 12,700 lines.	Every file. A plain-English navigation index of Mathlib's modules exists, Ismail's Glossary, and it is listed on the references page.
Measure-theoretic probability	Markov kernels; a probability measure over whole histories of states, actions and observations; conditional probability and conditional expectation; total-variation distance.	The trajectory measure, `trajMeasure`, built from `oneStepKernel`, is the space in which every theorem is stated.
Information theory over finite alphabets	Entropy, conditional entropy, mutual information, Kullback–Leibler divergence, and Fano's inequality.	The proofs for X₁ and X₄ rest on them, and the failure condition for X₄ is stated in terms of conditional entropy.
Lower-bound theory for sequential decisions	Regret; minimal adversarial environments; two-world indistinguishability arguments of the Le Cam kind; the logic of minimax lower bounds.	All six necessity theorems. Without this, the results can be read but not understood.
Novel argument construction	Building a lower-bound argument to fit a new structural difficulty, and finding the reduction that lets many results share a few lemmas.	The six necessity proofs, which use different arguments, and the independence reduction that serves all thirty pairs.
Real and convex analysis	Limits, including the long-run upper and lower limits; Kronecker's lemma; concavity of the binary entropy function; Jensen's inequality.	Supporting lemmas in `Phase1.lean` and `Phase2CMI.lean`, and the closing steps of the X₄ proof.
Stochastic processes and martingales	Filtrations, the Doob martingale construction, and the Azuma–Hoeffding inequality.	The closing link of the cycle in `Phase5.lean`, from X₆ back to X₁.
Domain translation	Relabelling the abstract environment, algorithm and reward term for term into a domain, while keeping the epistemic tier of each claim visible.	The companion papers, and every assessment, which is a translation of this kind.
Consilience argumentation	Judging whether independent lines of evidence converge for a shared structural reason and not by coincidence of surface.	Arguments for Class C membership.
Epistemic scoping and version discipline	Keeping separate what is machine-verified, what is paper-proved, what is a domain reading and what is a guide-invented method. Recording corrections against versions.	The verification tiers, and every verdict.
Architectural design of a research programme	Structuring interdependent results and documents so that each dependency is explicit and consumed.	The six-phase dependency graph of the Lean project.
Rule-based protocol design	Building evaluation rules ordered by dependency and cited rule by rule.	The two protocols described under review discipline.
Knowledge of the domain assessed	Enough fluency in the setting being assessed to see its real decisions, constraints and commitments, and to recognise the six difficulties in that setting's own terms.	The step from the definitions to a real structure, which is what Class C and error theory are about.
Software and data engineering	Pinned toolchains, continuous builds, version discipline, and versioned exports that track the toolchain, the library snapshot and the release separately.	The repository's build, the dated line counts, and the Glossary.
Technical writing	Stating results, definitions and scope so that another person can check them.	The paper, its appendices, and these pages.

Depth, and what proof looks like

The depth terms below are Ismail's. Each is paired with the kind of artefact that shows it, and the pairing is the point: a depth is claimed only where an artefact demonstrates it.

Discipline	Depth	What proof looks like
Formal verification in Lean 4 and Mathlib	Advanced	A public, versioned development of substantial size that rebuilds, with no unproved placeholders, added axioms, hidden definitions or suppressed warnings, and with continuous integration.
Novel argument construction	Advanced	Published proofs of distinct lower-bound results built by different arguments, with a reduction that collapses many results into a few shared lemmas.
Lower-bound theory for sequential decisions	Advanced	Minimal adversarial environments with matching necessity theorems, published with their proofs.
Measure-theoretic probability	Advanced, for the constructions the work uses	A reusable infrastructure, such as a trajectory measure over histories, used as the ambient space of downstream theorems.
Information theory	Advanced, for finite-alphabet decision problems	Entropy, Fano-type and divergence tools built and deployed inside published proofs.
Domain translation	Distinctive	Complete instantiations of the abstract framework in more than one domain, citing primary sources and preserving the epistemic tier of each claim.
Architectural design of a research programme	Distinctive	A multi-document programme with explicit dependencies between results.
Epistemic scoping and version discipline	Distinctive	A consistent four-tier scheme applied across documents, with corrections recorded against versions.
Rule-based protocol design	Distinctive	Published evaluation protocols with rules ordered by dependency and cited rule by rule.
Consilience argumentation	Proficient	Arguments showing independent lines of inquiry converging for a structural reason.
Real analysis, convex analysis, stochastic processes	Proficient	Named lemmas and constructions used in published proofs, such as Kronecker's lemma, entropy concavity, and filtration and martingale constructions.
Technical writing	Proficient	Paper-length exposition with definitions, theorem statements, proof sketches, and a table mapping each numbered result to its formal identifier.
Knowledge of the domain assessed	Reading-level fluency	Accurate use of primary sources across the domain's sub-fields, checkable by anyone who follows the citations.
Software and data engineering	Working	Public repositories with pinned toolchains, reproducible builds and continuous integration, and versioned exports.

What "uncommon, not impossible" means

The first four disciplines in the first table are the core, and the rest support them. Each is a standard subject with textbooks, courses and public literature. What is uncommon is holding formal verification at scale, measure-theoretic probability, information theory and lower-bound design together, and then adding domain knowledge and the habit of scoping claims that assessment needs. A team can hold that combination jointly, for instance a verification engineer, a probabilist and someone who knows the setting. Where a team does, the proof is the artefacts of its members, discipline by discipline.

Evaluating the checks asks for far less than building the formalisation, because the kernel has already done the checking. What is public is the ability to evaluate it: every statement, definition and proof is open to inspection. Competence is still needed to read the definitions and to apply them to a real structure, and that is where a reader's knowledge matters.

Where competence enters the verification chain

The three links of three-party verification each need some of this competence. The first link is performed by the Lean kernel, which anyone can run. Whoever performs the middle link holds the approving role, on proof. Whoever performs the final link holds the evaluating role, on proof, and is not the person who approved the application being evaluated. A client does not need this competence to receive an evaluation. A client commissions an evaluator who has it.

The field
Pages	The QuestionField definitionClass CWhy a POMDPNecessity and sufficiencyVerification tiersAudit it yourselfMethodologiesCompetenceError theoryThree-party verificationAdjacent fields