Author and Priority
From the documentation of the field
This page is the one full account of authorship and priority for the field. It lists what can be checked, and it claims no authority from credentials or affiliation.
Identity and priority
The field rests on the work of Muhammed Ismail. His ORCID is 0009-0000-3713-7105. His public accounts are M-Ismail-ZA and decisional-integrity.
The primary paper, Ismail's Primitives: A Unified Functional Theory of Necessity, Independence, and Sequential Dependence in Adaptive Decision Systems, has the DOI 10.5281/zenodo.23080967 for its current version, V6.2, published on Zenodo on 2026-10-01. The record gives 2025-12-08 as the date the work was first made available. The author's background is set out in the "About Ismail" section of the Glossary site, and is not restated here.
The paper's companion papers, which apply the same primitives across other domains, are listed on the applications page.
What a reader can check
Each row names an artefact, where to find it and what it shows. The rows follow the order of the disciplines on the competence page, so the two can be read side by side.
| Discipline | Artefact | Where to check it |
|---|---|---|
| Formal verification | The Lean 4 project IsmailsPrimitives: 12,667 lines across seven files, with zero sorry, zero axiom and zero opaque |
Repository; verification tiers gives the counts and audit it yourself the commands |
| Novel argument construction | necessity_x1 in SixPrimitives/Phase3.lean, lines 122 to 542, roughly 420 lines, built around an explicit adversarial construction |
The file and line range |
| Novel argument construction | mutual_independence in SixPrimitives/Phase4.lean, which states all thirty ordered pairs in one theorem |
The file, near line 1480 |
| Lower-bound theory | Six minimal witness environments, each with a matching necessity theorem | SixPrimitives/Phase2.lean and Phase3.lean |
| Epistemic scoping | The opening comment of SixPrimitives/Phase5.lean, which states what the phase proves and what it leaves as prerequisites for an implementer |
The first lines of the file |
| Domain translation | The companion papers, each a complete instantiation in a different domain | Applications |
| Navigation of Mathlib at scale | IsmailsGlossary: a plain-English index of all 9,150 modules of Mathlib4, with its own DOI 10.5281/zenodo.21192789 |
Repository |
| Rule-based protocol design | IsmailsProtocols: two evaluation protocols with rules ordered by dependency and cited rule by rule |
Repository; tools |
What the artefacts show
The Glossary indexes all 9,150 Mathlib modules, and necessity_x1 runs to roughly 420 lines built around an explicit adversarial construction. The artefacts are open, and the checks on them are public, so nothing on this page needs to be taken on the author's word.