Audit it yourself

From the documentation of the field

The mathematics in this field is machine-verified in Lean 4, and the checks are public. In a complex environment, a structure that lacks one of the six primitives of Ismail's Primitives incurs linear regret (the necessity result, proved in SixPrimitives/Phase3.lean). The theorems in the code are the simplest case, in the smallest environments, which is where an impossibility result is cleanest. The theory applies to any environment, however complex, in which the difficulty occurs. Nobody is expected to redo the formalisation, because the formalisation is the check. This page is a route through the code for a reader who wants to evaluate the checks for themselves, by reading what each theorem says and what it rests on. It assumes no Lean knowledge at the start.

All line numbers refer to the IsmailsPrimitives repository as of the commit dated 2026-10-01 (ff3f039). They move when files change. Build instructions are on the references page.

What the kernel has checked and what a reader reads

The Lean kernel has checked the proof bodies, and a proof either passes or does not. What a reader does is read the statements: what each theorem says, and how the definitions it rests on relate to their plain readings. The audit surface is therefore the theorem statements plus the definitions they rest on, directly and indirectly. A reader who understands the statements and the definitions has understood the result, because the proofs behind them are checked.

The code is organised so that each file imports only earlier files. Reading from Phase0.lean to Phase5.lean meets every definition before it is used. A statement-first reader will jump around instead, and the sections below show where to go.

Step 1: check the counts

From the repository root:

wc -l SixPrimitives/*.lean
grep -rnw -e sorry -e axiom -e opaque SixPrimitives/
grep -rn "set_option" SixPrimitives/

The line counts should total 12,667 across the seven phase files. The second command should print nothing. The third should print one line, in Phase2.lean, which raises an instance-search time limit. Verification tiers explains why those counts matter and what they do not show.

Step 2: read Phase0

SixPrimitives/Phase0.lean has 259 lines and is the natural first read, because the definitions every theorem rests on are stated there. It defines:

• the structures Env (line 32) and Algorithm (line 50), which are the POMDP and the decision-maker, as set out in why a POMDP;
• the six failure conditions, LacksX₁ to LacksX₆, at lines 69, 74, 80, 85, 94 and 99, which state what it means to lack each capability;
• the possession predicates, which define possessing a capability as not lacking it, along with a stronger "robust" form;
• the six structural properties, HasP₁ to HasP₆, at lines 168, 174, 181, 196, 205 and 210;
• InClassC at line 218, which says an environment belongs to Class C if it has at least one of the six properties.

A reader question on InClassC. The clauses for P₁ and P₆ are existential. The P₁ clause asks for some second environment that disagrees about the best action, and the P₆ clause asks for some sequence of environments that starts at the given one and changes between two consecutive times. Neither asks for a property of the given environment alone. Ask what that does to the formal membership test. The paper's own test for a real process is the set of six structural checks in its Section 4, and InClassC is best read as typed shorthand for them. No theorem in Phases 3 to 5 takes InClassC as a premise, and the field leaves the refinement of this boundary for later work.

Phase0 is not the whole definitional surface. A theorem's statement also mentions definitions that live elsewhere, as the next section shows.

Step 3: a worked example, X₁

The necessity theorem for X₁ is necessity_x1 in SixPrimitives/Phase3.lean. It starts at line 122 and the proof runs to line 542, and the statement is the thirteen lines before the proof begins. In plain terms it says: take any algorithm over two actions and Boolean observations that is a Markov kernel, run it in each of two witness environments, and suppose the failure condition LacksX₁ holds for the sequence miSeq. Then there is a positive constant c such that, from some point on, the combined regret in the two environments is at least c times the elapsed time.

The statement refers directly to these definitions:

Each of those rests on further definitions. regret is built from algValue (Phase2, line 1600) and optValue, which in turn rest on algValue' (Phase2, line 1123) and the trajectory measure trajMeasure (Phase2, line 204). miSeq uses actionMarginal (Phase2, line 1143). A thorough audit follows these chains to the bottom.

One detail rewards a close read. miSeq carries a name inherited from Phase0, which refers to mutual information, but as written in the source it is the total-variation distance between the algorithm's action distributions in the two environments. The paper says so itself, in its list of caveats, and explains that the proof uses a total-variation surrogate in place of Shannon mutual information.

The same exercise for all six

Three of the six statements (X₂, X₃ and X₆) do not name the Phase0 failure condition. X₃ and X₆ restate its content directly, with the constants made explicit, and a reader can check by eye that each restated hypothesis matches the Phase0 definition. X₂ is stated against a different quantity on purpose. The general condition in Phase0 is written for the unconditional danger probability, which in a trap environment decays toward zero as trajectories are absorbed, whatever the surviving trajectories do. The theorem therefore uses the conditional danger probability, and the paper records this in a remark titled as a naming note, not literally LacksX₂, and again in its list of caveats. Part II applies the Phase0 predicate LacksX₂ to that same conditional sequence, at Phase4.lean lines 746 to 769 and 1494 to 1498.

Four of the theorems have companion versions. necessity_x2_parametric (line 1223) generalises the danger action, and necessity_x4_explicit_bound, necessity_x5_explicit_bound and necessity_x6_explicit_bound (lines 1662, 1885 and 2437) give explicit constants.

Walking through two definitions

Two failure conditions, in plain English, each with the questions a reader should put to it.

LacksX₂

The definition is at Phase0, line 74. It says there is a positive number δ such that a danger-probability sequence is at least δ at every step k. The paper applies it, and states the necessity theorem, against the conditional danger probability, condDangerProbSeq, for the reason given above.

In the witness environment env₂, the process walks down a corridor. One action moves it forward and pays normally. The other action, the danger action, drops it permanently into a trap that pays nothing. The conditional danger probability at step k is the probability that the algorithm plays the danger action at step k, given that it has not yet fallen into the trap, and it is defined as 0 where survival is already impossible. So the condition says that at every step where the process is still alive, it takes the irreversible action with some fixed minimum probability and never learns to stop.

Questions to ask: is a floor on the conditional danger probability, at every step, a fair rendering of "keeps taking the action that locks in permanent loss"? Why a fixed floor and not a rate that merely declines too slowly? The paper uses stronger standards for possession elsewhere. Phase0 defines robust possession of X₂ as the danger probability tending to zero, and the necessity result needs only the floor.

LacksX₄

The definition is at Phase0, line 85. It says there is a positive number ε such that the long-run lower limit of the conditional entropy is at least ε. In the witness environment env₄ there is one state and two actions. One action pays 1 and the other pays 0, so the better action is plain. condEntSeqX4 measures how unpredictable the algorithm's choice at step t is, given everything it has seen so far. So the condition says that the algorithm keeps hedging indefinitely, even though the evidence has long since settled which option is better.

Questions to ask: is persistent randomness in the choice a fair rendering of failing to commit? The condition uses the long-run lower limit, so an algorithm that returns to full commitment infinitely often is not classed as lacking X₄. Is that the right reading? The theorem also runs one way: lacking X₄ forces linear regret. An algorithm that commits firmly to the wrong option has zero entropy and also has linear regret, and the theorem does not claim to cover it. Does that matter for how the capability is described?

Checking the witnesses

A necessity theorem about a witness environment is only useful if the environment really exhibits the structural property it witnesses. Lean proves that too. The witness lemmas are env₁_0_hasP₁ (Phase2, line 1731), env₂_hasP₂ (line 1956), env₃_hasP₃ (line 2114), env₄_hasP₄ (line 3760), env₅_hasP₅ (line 3862) and env₆_hasP₆ (line 3980). The matching _inClassC lemmas, which show that each witness satisfies the formal predicate, are at lines 1740, 1976, 2161, 3768, 3872 and 3989.

Beyond Part I

The master theorem of Part II is mutual_independence, at Phase4.lean line 1480. Its statement is a conjunction of thirty claims of the form LacksXᵢ, grouped by primitive of Ismail's Primitives. Each group says which of the five other challenger algorithms lack that primitive, and together the groups cover all thirty ordered pairs. Part III is in Phase5.lean, with the six links as iet1_forward (line 222) through iet6_non_reversible (line 786). Each link has a forward, a reverse and a non-reversibility theorem, and the theorems state their hypotheses openly. Necessity and sufficiency says what they establish.

Reporting a discrepancy

If you find a place where a statement says something other than what it appears to say, or a claim on this site that does not match what the code establishes, write to decisionalintegrity@outlook.com, quoting the file and line. An argument that a seventh primitive beyond Ismail's Primitives exists is not a discrepancy with the existing results. It would be a separate result, and the Class C page sets out the bar it would have to meet.