What's proven

Six primitives, each shown necessary in its own minimal environment. All thirty ordered pairs shown mutually irreplaceable. A verified logical scaffold connecting all six into a cycle — stated plainly where that scaffold is complete and where it still requires domain-specific work.

Checked by a machine, not a reviewer

Why open, not journal-locked

Peer review checks three things: novelty, significance, and rigor. Novelty and significance are judgment calls — this work makes its own case for both, openly, for anyone to weigh directly. Rigor is the one thing review is supposed to guarantee, and for a machine-checked proof, rigor stops being a judgment call: Lean's kernel either accepts a proof or it doesn't, and no reviewer's opinion changes that answer.

What's left, once a kernel rather than a referee settles rigor, is comparison rather than judgment:

A DOI on Zenodo timestamps this publicly and permanently, independent of any journal. Zenodo is backed by CERN and built for perpetuity: the DOI resolves today and will keep resolving. There is no scenario in which the rights are revoked or the work quietly moves behind a paywall — the permanence is structural, not a policy that could change. If an academic at an affiliated institution publishes the same result tomorrow, the DOI already exists — citing it isn't a courtesy, it's what the academy's own norms already require.

This is published under CC BY 4.0 — free to use, cite, and build on, attribution the only requirement. A firm without journal access or academic affiliation should not be the last to find out that a fixed, provable standard already exists. Waiting for a traditional publication cycle to run its course only hands the advantage to whichever competitor reads this page first.

What's in the repository

Everything above is verifiable in one place, not taken on this site's word. The repository holds the complete Lean 4 formalization — seven files, organized in phases, each importing only the phases that came before it, so every definition you meet has already been introduced.

IsmailsPrimitives/
├── SixPrimitives.lean
├── SixPrimitives/
│   ├── Phase0.lean      (framework types)
│   ├── Phase1.lean      (supporting lemmas)
│   ├── Phase2.lean      (trajectory measure & environments)
│   ├── Phase2CMI.lean   (conditional mutual information)
│   ├── Phase3.lean      (Part I — necessity)
│   ├── Phase4.lean      (Part II — independence)
│   └── Phase5.lean      (Part III — sequential dependence)
├── paper/
│   ├── PAPER.md
│   └── Ismails_Primitives.pdf
├── lakefile.lean, lake-manifest.json, lean-toolchain
└── README.md

Alongside the proofs: the paper itself, as a Markdown edition readable directly on GitHub and as a full PDF carrying both appendices omitted from the web edition — a line-by-line table mapping every definition and theorem to its exact Lean identifier, and the proofs verifying that every environment used in Part I actually exhibits the structural property it's claimed to witness. Also included: the exact lakefile, dependency manifest, and Lean toolchain version that reproduce this from a clean clone in a few minutes, and the GitHub Actions workflow that rebuilds and checks the whole thing on every commit — so the green build badge is never more than one push out of date.

The Lean code is released under the MIT License. The paper is CC BY 4.0. Either way: use it, cite it, build on it.

What a POMDP is

A POMDP (Partially Observable Markov Decision Process) has four ingredients: a hidden state (the true situation, unseen), actions (the choices available), observations (noisy, partial signals about the hidden state — all the decision-maker actually gets), and rewards (the consequence of an action in a given state). The defining feature is the gap between state and observation — exactly where several of the six structural failures live.

Why nothing else is more comprehensive: every simpler alternative is this structure with a piece deleted, not a rival to it. Remove the hidden/observed gap and you get an ordinary MDP — which can't even express reward ambiguity, since that requires a hidden parameter learned only through noisy signals. Remove the actions and reward and you get a Hidden Markov Model — a description, not a decision framework. Collapse the state dynamics to nothing and you get a multi-armed bandit. Add a second strategic agent and you get a game — more machinery than a single decision-maker's claim needs. Nothing adds expressive power beyond this structure for this problem; everything else subtracts from it.

The tuple, broken down

Not every primitive needs a genuine gap between S and O. P1, P2, P3, and P6 are about not knowing something. P4 and P5 are about indecision or boundary-crossing despite the state being fully known — the structure correctly degenerating to the fully-observed special case for those two.

Any decision maker, not just AI

A reader meeting six primitives named things like Cross-Context Safety Transfer and Policy Simplification, proven against a POMDP in Lean 4, could reasonably conclude this is a paper about AI — about what a large language model or a learning agent needs before its decisions can be trusted. That conclusion is fair: AI systems making sequential decisions under uncertainty are the most visible, highest-stakes case this result speaks to, and nothing here excludes them.

But the six primitives are proven over the abstract structure of a POMDP — a hidden state, actions, noisy observations, reward — never over anything specific to a model, a training run, or a policy network. That abstraction is what gives the result its reach, and it's why the sections below turn to investment, insurance, and consulting: three domains with no machine learning in view, each still built from the same tuple and paying the same six costs when a primitive goes missing. They illustrate the theory's scope; they don't define its edge. The necessity results bind any sequential decision-making process that lands in Class C, whatever the domain calls itself — that reach, not any single example, is what makes this a unified functional theory.

Three domains, the same formula

S  = {ValueTrap, GenuineValue}     -- is the cheap valuation real or structural decay?
A  = {ActOnScreen, InvestInDiligence}
O  = ScreenMultiple ∈ ℝ            -- headline signal, correlated with but not equal to S
r  = 1/2  if ActOnScreen
     1    if InvestInDiligence and it resolves to GenuineValue
     0    if InvestInDiligence and it resolves to ValueTrap

S  = ReserveLevel ∈ ℝ
A  = ℝ  (dividend/investment/growth action)
F  = { a : ReserveLevel − a ≥ RegulatoryMinimum }   -- feasible set
r(s, a) = payout(a)  if a ∈ F, else −M

S  = {ProcessFailure, PeopleFailure}          -- hidden true root cause
A  = {DiagnoseProcess, DiagnoseIncentive}
O  = InterviewSignal ∈ ℝ                       -- noisy correlate of S
r(s, a) = 1/2 + Δ  if a matches s, else 1/2 − Δ

This environment is in Class C. Under the paper's necessity results, the matching primitive is not optional for it — its absence guarantees regret that grows without bound the longer the process operates, regardless of what the domain calls itself. Full stop.

Looks like succeeding is not the same as succeeding

A process can look like it's succeeding and still be mathematically guaranteed to fail. These aren't in tension — "looks like it's succeeding" and "regret" measure different things.

Regret is the running gap between what was captured and what was achievable — not a score for the latest period. A process can post steady, positive results for a long time while that gap grows underneath it the entire time. In the corridor behind X2, the safe action pays real reward every step, right up until the trap fires. In the regime-switch behind X6, a stale strategy keeps paying a real, positive return — just a smaller one, forever, with no announcement.

For a process lacking a required primitive, this gap doesn't fluctuate. It grows at a fixed rate, without limit, for as long as the process runs.

Time without incident is not evidence the gap has stopped growing.

The 2-foot leap

Every example here is the simplest possible version of its failure, deliberately. A real investment, engagement, or policy has more moving parts, never fewer — and each one is another place for the same failure to hide.

If you cannot make a two-foot leap, you cannot make a ten-foot leap. The two-foot leap isn't a warm-up. It's a floor. A harder jump has never made the underlying requirement optional.

A necessity result proven on the smallest case is a floor that persists into every harder case containing it. That's why these examples stay minimal.

Literature review

The six primitives and the necessity results are this paper's own contribution. The environments they're proven on are not built in a vacuum — each sits inside an existing line of stochastic-control literature. Closest analogues below, domain by domain, so a reader already familiar with that literature can see exactly where this paper's constructions depart from it.

Insurance

Markov/POMDP-shaped control of insurer reserves, dividends, and reinsurance.

• De Finetti, B. (1957). Su un'impostazione alternativa della teoria collettiva del rischio. Transactions of the XVth International Congress of Actuaries.
• Bäuerle, N. & Rieder, U. (2011). Markov Decision Processes with Applications to Finance. Springer.
• Azcue, P. & Muler, N. (2014). Stochastic Optimization in Insurance: A Dynamic Programming Approach. Springer.
• Zeng, L. & Li, M. (2025). Long-Run Average Reward Maximization of a Regulated Regime-Switching Diffusion Model. arXiv:2512.15167 — regulated regime-switching dividend/reinsurance control under a minimum solvency floor.

Investment

Portfolio optimization under a hidden, regime-switching market state.

• Bäuerle, N. & Rieder, U. (2005). Portfolio optimization with unobservable Markov-modulated drift process. Journal of Applied Probability, 42.
• Elliott, R. J. & Siu, T. K. Stochastic switching for partially observable dynamics and optimal asset allocation. Applied Mathematical Finance.
• Sass, J. & Haussmann, U. G. (2004). Optimizing the terminal wealth under partial information. Finance and Stochastics, 8.

Consulting

General POMDP framework

• Kaelbling, L. P., Littman, M. L., & Cassandra, A. R. (1998). Planning and acting in partially observable stochastic domains. Artificial Intelligence, 101. — already cited in the paper itself (Section 4.2).
• Monahan, G. E. (1982). A survey of partially observable Markov decision processes. Management Science, 28.

The Open Challenge

Failure does not mean success

Proving a process fails without something is not the same claim as proving that having it guarantees success. These sit on opposite sides of the same mathematics. Confusing them is its own mistake.

Objective vs. subjective

Necessity is a lower bound. It holds regardless of what a decision-maker wants — no goal variable, no domain, no opinion about what "winning" means required.

Success is an upper bound. It says what a specific approach can achieve — and "achieve" requires first naming what's being optimized for. That naming isn't mathematics. It's a domain deciding what it wants.

What success means, by domain

Same recipe, different emphasis

The six primitives required to avoid failure don't change across these three. What changes is emphasis — which primitives must be held robustly, not just adequately, and which domain-specific variables layer on top — depending on which success is being built toward.

✓ = fully required, same as every other domain. ★ = the flagship case worked through on the previous page — where that domain's emphasis is sharpest, not where the other five stop mattering.

Who is Muhammed Ismail

Ismail is 36, based in South Africa, and entirely self-taught — in mathematics, in economics, in the mechanics of business, and in enough psychology to notice what happened next.

In September 2025, while trying to understand his own decision-making rather than anyone else's, he noticed that his reasoning kept passing through the same six-step pattern, regardless of what the decision was about. For a while that observation stayed a personal heuristic — a way of checking his own thinking before acting on it. What changed was recognizing that the pattern wasn't just useful. It looked like it could be proven.

He had no formal training in mathematics before that point. He taught himself what a proof at this level required, in roughly the order he needed it. By April 2026 the result existed as a prose corpus, largely complete.

Proving it, though, made something else clear: this wasn't shaping up to be a simple theorem. The same structure kept holding as Ismail tested it against a wide range of industries and disciplines — not as a loose analogy, but as what the finished paper's own title now calls it: a Unified Functional Theory. Unified, because the same handful of structural failures recur across investing, operations, public policy, and reinforcement learning alike, with one proof serving all of them at once. Functional, because what's being characterized is what a decision process has to do under uncertainty — never which field it happens to sit in. The claim is a deliberately narrow one, though: it holds for a specific, defined class of environments — what the papers call Class C — sequential decisions made under real uncertainty, where information is incomplete, conditions shift, and mistakes aren't always reversible. No more, no less.

That is where the difficulty started. An independent researcher with no institutional affiliation, presenting a result that needs specialists in formal logic and decision theory to evaluate the mathematics — and separate specialists again for each domain the mathematics was shown to reach — has no realistic route through traditional peer review on any usable timeline. So the mathematics was rebuilt instead as a Lean 4 formalization: something a kernel checks deterministically, without needing to check the author first. Learning Mathlib well enough to do that produced two things — the 12,700-line proof this site describes, and, as a byproduct of the learning itself, Ismail's Glossary. Every paper written since has been re-anchored to that verified core as its foundation.

None of this is the conventional route into a result like this. It is the route available to someone starting with no institution behind him and no formal mathematics in front of him. The reason it does not need to be taken on faith is the same reason stated at the start of this paper: nothing here rests on who proved it. It rests on whether Lean's kernel accepted it. It did.

More from Muhammed Ismail

This paper is one part of a larger, ongoing body of work. Two threads continue past it: a reference project built in the same Lean 4 ecosystem, and further papers that extend the six primitives themselves into domains further still from the ones illustrated above.

Ismail's Glossary

A complete navigation index for Mathlib, the Lean 4 library this paper's proof is built on.

Mathlib is one of the largest libraries of formalized mathematics in existence — over 9,150 modules, with no plain-language map of what any of them contain. Ismail's Glossary gives every module a short, human-readable description, an interactive atlas of how its 32 domains relate, and a progressive reference for learning Lean itself, so navigating the library no longer requires already knowing what you're looking for.

Extending Ismail's Primitives

The necessity results proven here are stated abstractly enough to travel beyond business decision-making entirely. Companion papers have since applied the same six primitives to developmental psychology, to psychotherapy, and to economic coordination theory. The developmental-psychology paper argues that Erikson's psychosocial stages, Maslow's motivational hierarchy, and Bowlby's attachment phases independently converge on the same six-stage sequence proven necessary here — evidence, on that reading, of shared underlying structure rather than analogy. Further papers are in preparation.

• Ismail, M. (2026). Ismail's Primitives and Human Development: A Functional Isomorphism Between a Lean-Verified Computational Theory and Developmental Psychology. doi.org/10.5281/zenodo.21257553
• Ismail, M. (2026). Ismail's Primitives: An Emotional Adaptation Theory for Therapy Discovered through Functional Isomorphism. doi.org/10.5281/zenodo.21289914
• Ismail, M. (2026). Ismail's Primitives: Lean-verified Economic Adaptation Theory. doi.org/10.5281/zenodo.21289756

Who Builds the Bridge