1. Start with a checked case🔗

Prepare a local checkout

You need an authorized checkout of this repository and elan, which provides Lean and Lake. Follow the official Lean installation instructions if you do not have those tools. The repository's lean-toolchain selects Lean 4.28.0. This preview is not yet an anonymous public installation.

Open a terminal at the repository root, where lakefile.toml and examples/valid.json live, then run:

lake build
lake exe slean validate examples/valid.json

Expected validate output:

{"case_id":"synthetic-decision-1","events":10,"ok":true}

events: 10 counts entries in the complete journal, including two restricted to the owner. It does not mean ten experiments or ten confirmed results.

Read the result, not just “ok”

Show the agent-safe view:

lake exe slean view examples/valid.json agent

In the returned JSON, find observations[0] (status: "measured", value: "0.002", unit: "ratio") and decisions[0] (result: "promote"). The value remains a decimal string to avoid implicit rounding. event-1 freezes the rule; the observation is event-4, the assessment is event-6, and the decision is event-7.

You have answered one precise question: does the recorded promotion follow an earlier observation that matches the frozen protocol? For this synthetic case, yes. The next chapter explains the links and comparison Slean checks. A successful validate does not certify the sensor, artifact file, or truth of the claim.

See a concrete rejection

Run a copy of the case whose observation unit has changed:

lake exe slean validate examples/unit-mismatch.json

The command exits nonzero and prints:

{"error":{"code":"metric_unit","event_id":"event-4","message":"observation metric or unit differs from frozen protocol","object_id":"observation-1"},"ok":false}

event_id locates the failure in the journal; metric_unit means the observation's metric or unit no longer matches the protocol. Continue to read the decision and distinguish an invalid case from one whose result is simply unknown.