• Page

References

From the documentation of the field

This page lists the papers, the Lean 4 repository, the tools and the other sources this site rests on. Each entry gives a title, an identifier and a short note on where the site uses it.

The primary paper

Ismail's Primitives: A Unified Functional Theory of Necessity, Independence, and Sequential Dependence in Adaptive Decision Systems. Muhammed Ismail (ORCID 0009-0000-3713-7105). V6.2, published on Zenodo on 2026-10-01. DOI 10.5281/zenodo.23080967. Licence: CC BY 4.0.

This is the paper behind every result on the site. The figures captioned "Ismail's Primitives, V6.2" on the field definition and necessity and sufficiency pages are taken from it. The author and priority page gives the dates and the account details.

The Lean 4 repository

IsmailsPrimitives. The machine-checked Lean 4 and Mathlib formalisation of the paper. Licence: MIT for the Lean code. The repository is listed on the Zenodo record as software that supplements the paper.

The seven files that carry the results are linked from the pages that use them:

Part File Used for
Definitions Phase0.lean The environment, the algorithm, the six failure conditions and Class C
Supporting lemmas Phase1.lean, Phase2.lean, Phase2CMI.lean Probability and analysis, the trajectory measure, the witness environments, conditional mutual information
Part I, necessity Phase3.lean The six necessity theorems
Part II, independence Phase4.lean mutual_independence, the thirty ordered pairs
Part III, sequential dependence Phase5.lean The six links of the cycle

Line numbers quoted on the site refer to the repository as of the commit dated 2026-10-01 (ff3f039).

Building the project

The toolchain is leanprover/lean4:v4.30.0, built against Mathlib v4.30.0. Install Lean through elan, then run:

git clone https://github.com/M-Ismail-ZA/IsmailsPrimitives.git
cd IsmailsPrimitives
lake update
lake exe cache get
lake build

A build that finishes without error means the Lean kernel has checked every theorem. Audit it yourself gives the checks to run once the build passes, and verification tiers says what the build establishes.

Companion papers

The companion papers apply the same primitives in other domains. The applications page describes each.

Ismail's Glossary. A plain-English navigation index of all 9,150 modules of Mathlib4, with its own DOI 10.5281/zenodo.21192789 and an interactive site. The competence page refers to it as a help for reading the Lean files. It is an independent community resource and not an official product of the Lean or Mathlib projects.

The review protocols

IsmailsProtocols. The repository holding the two protocols this site uses on its own writing: Ismail's Credibility Checker and Ismail AI Review. The review discipline page says how they are applied.

  • The Credibility Checker's rules are backed by its evidence audit.
  • Rule content is released under CC BY 4.0. Ismail AI Review's catalogue is adapted from the Wikipedia essay Signs of AI writing by WikiProject AI Cleanup, used under CC BY-SA 4.0, and the share-alike term carries forward.

The author's profile

The Dossier

The 26 sources behind the problem statement are listed with their links, dates and independence ratings in the Dossier, under Appendix B, and each has its own page under entries. Appendix C lists the further sources that were reviewed and held in reserve.

Lean 4 and Mathlib

  • Lean 4, the proof assistant.
  • Mathlib, the library of formalised mathematics that the project builds on. The only axioms the proofs rest on are Mathlib's own.