Four kinds of evidence

Proved in a world, checked computation, supported by simulation, confirmed on the real world: four different things, never merged into one score.

Why keep them apart

“It is proved” can mean very different things. Slean keeps four kinds of evidence apart, and every result says which kind it is.

Four kinds of evidence

Kind	What it means	Example in Slean
Proved in a world	A Lean theorem about a world’s exact definition. True for that world, unconditionally.	Traffic: the number of cars is conserved for every ring size.
Checked computation	A finite fact the kernel evaluated, such as a counterexample or a periodic orbit.	Rule 30’s counterexample 001 → 111; the period-16 glider.
Supported by simulation	No counterexample found in a stated search. It is a conjecture, kept as an open brick.	A regularity seen in every simulation tried, without a proof: it stays an open conjecture.
Confirmed on the real world	A prediction registered before the data that settles it, evaluated by a frozen rule. It is the only kind that says anything about nature.	None yet. It is milestone M5 on the roadmap.

Kind

What it means

Example in Slean

Proved in a world

A Lean theorem about a world’s exact definition. True for that world, unconditionally.

Traffic: the number of cars is conserved for every ring size.

Checked computation

A finite fact the kernel evaluated, such as a counterexample or a periodic orbit.

Rule 30’s counterexample 001 → 111; the period-16 glider.

Supported by simulation

No counterexample found in a stated search. It is a conjecture, kept as an open brick.

A regularity seen in every simulation tried, without a proof: it stays an open conjecture.

Confirmed on the real world

A prediction registered before the data that settles it, evaluated by a frozen rule. It is the only kind that says anything about nature.

None yet. It is milestone M5 on the roadmap.

Slean never merges them into one score.

Reading the table

Proved in a world: the traffic law holds for every ring size of rule 184. It is a theorem about an exact definition, nothing more.
Checked computation: the rule 30 counterexample, or a glider that comes back after 16 steps. A finite fact that the kernel evaluated.
Supported by simulation: no exception found in a declared search. It is a conjecture, kept as an open brick.
Confirmed on the real world: a prediction registered before the data that settles it exists, evaluated by a rule fixed in advance. It is the only kind that says anything about nature.

What Slean does not claim

A law proved in a cellular automaton is not a law of nature. Today Slean produces the first two kinds, and sometimes the third. The fourth will come with milestone M5 of the roadmap. On the way to physics, Slean makes the gap between the first kind and the last explicit; it does not erase it.