What must a decision-maker get right, structurally, to avoid failure under uncertainty?

A structure can have the property before anyone verifies it. Verifying it is the service.

Every business decision area is in Class C, because information is incomplete, commitments are often irreversible, options can be comfortable without being best, some limits cannot be traded and markets change. One situation is enough.

Six situations, six primitives

A decision structure faces up to six situations, P1 to P6, and each has a matching capability, X1 to X6. The theory applies to environments in Class C, which show at least one of the six.

Failure has one shape

Where the matching capability is missing, loss grows in proportion to time, whatever else the structure does well. The paper calls this linear regret. If the best available option pays 100 each period and a structure captures 90, the gap is 10 every period: 10 after one period, 100 after ten, 1,000 after a hundred.

A good year can hide the gap. A process that lacks a required capability can post steady, positive results for a long time while the gap grows underneath.

Three parts

Parts I and II hold without conditions.

Machine-checked

Lean 4 checks every step. The proof runs to 12,667 lines in seven files, with zero sorry, zero custom axiom and zero opaque definitions as of 2026-10-24, and it rests on Mathlib’s axioms alone. Anyone can rebuild it from the Lean repository. The paper is licensed CC BY 4.0 and the Lean code MIT.

A small risk that repeats

At a 5% chance each time, the chance of having made the irreversible mistake at least once is 64.2% after 20 times and 92.3% after 50.

1. 1

   Literacity’s work

   Every finding names the public criterion it rests on.

2. 2

   The field

   Each criterion says what a decision structure must show to possess one primitive, and names the Lean definitions it rests on.

3. 3

   The paper

   The criteria rest on numbered results, and the paper’s appendix maps each result to a Lean identifier.

4. 4

   The Lean proof

   Each result is a named theorem, with a file and a line.

5. 5

   The axioms

   Lean’s kernel checks every step from Mathlib’s axioms alone.

The necessity theorems

All thirty independence results follow from mutual_independence at Phase4.lean, line 1480.

Three commands anyone can run

From the root of the Lean repository.

Totals 12,667 lines across seven files as of 2026-10-24.

Prints nothing.

Prints one line, in Phase2.lean, which raises an instance-search time limit.

What the audit reads

The audit looks at how decisions are made, so it proceeds without access to what the decisions were about. The material is the organisation’s decision records: past decisions with their evidence, the framework in use, the decision process in effect, and the templates and procedures for new decisions. The sample is chosen by a rule fixed before the evidence is read and includes one case that succeeded, one that failed and one still in progress. Case materials stay private, and only the fact and date of a pass are public.

The verification statement

Where you stand out

Ten lines a verified firm can say

1. 1Our decision structure has the six capabilities that machine-checked mathematics shows every sound structure needs.
2. 2No other adviser holds this verification. Check the registry.
3. 3Our edge is rigor: the mathematics behind our advice is open for you to check.
4. 4Every line of our advice traces to the axioms, and anyone can rebuild the proof.
5. 5Our verification was carried out by the team at Literacity and approved by the mathematician who proved the primitives.
6. 6Our verification is dated, names what was checked and can be confirmed by anyone.
7. 7The audit examines how decisions are made, and the case materials stay private.
8. 8We re-verify, so the claim stays current.
9. 9Every case study we show says how it matches your situation on six points.
10. 10Every proposal we write shows its evidence for each of the six.

If you advise others, all ten lines apply. If you run an organisation and want to show your board, lenders or partners how you decide, the first eight apply.

A verified firm can point clients and partners to the mathematics and invite them to check it.

The registry is empty today. The first cohort will be published by Q2 2027.

1. 1

   Discovery

   Scope is agreed after this step.

2. 2

   Audit

   The evidence is reviewed against the public criteria.

3. 3

   Findings

   Each finding cites the public criterion it rests on, so the client can check it against the field.

4. 4

   Build support

   Where the audit found gaps. The client chooses its own tools.

5. 5

   Verdict

   A pass means possession of all six primitives.

6. 6

   Statement and registry

   On a pass, a public statement records the verification, and the registry lists it.

7. 7

   Re-verification

   A verdict applies at a date.

Scope is agreed for each engagement after the discovery call, because a small business and a large corporation differ in the processes in scope, the evidence available and the terms that apply.

Muhammed Ismail is a theoretical mathematician in South Africa. He proved that six structural capabilities are necessary for a decision-maker to avoid failure under uncertainty, checked the proof in Lean 4, and owns and directs Literacity, the service that applies it.

In September 2025 Ismail noticed that his own decisions followed a recurring six-step pattern, which he first treated as a personal heuristic. He asked whether the pattern could be proved. He then answered his own question by proving it in Lean 4.

1. September 2025Noticed the pattern.
2. 28 January 2026First companion paper.
3. 8 April 2026Second companion paper.
4. May to June 2026Moved the work into Lean 4.
5. July 2026Released Ismail’s Primitives and the Glossary.

The record: six papers on Zenodo under CC BY 4.0, three public repositories (IsmailsPrimitives, IsmailsGlossary and IsmailsProtocols) and the Lean proof.

The team

Literacity is a team whose work rests on one body of research, Ismail’s, from start to finish. The team carries out every audit. Ismail founded and leads Literacity, trains the team in the research and is the final arbiter of every verification. Literacity Pty Ltd, registration number 2016/135857/07, was founded in 2016 and is owned and directed by him.

The approving role rests on public artefacts, and Ismail’s own approval rests on the same ones. Another person can take the role by presenting artefacts of the same type and depth. As of 2026-10-22 no one else has presented that proof.

Three public accounts

They are kept separate so Literacity’s work can be checked against open material.