Evaluate
Evidence and checks
The 1–5 rank describes how a component's checker reaches a pass or fail result. At 1, it checks the format of an answer supplied with the test input. At 5, it computes a verdict from the component's declared requirements. This is called verdict independence. It does not rate maturity, the amount of code executed or correctness outside those requirements.
Each of the 88 components lists its evidence class, rank and scope limit. The class identifies the method used to check it. The scope limit states what the result can establish. The classes below are ordered by component count, with an explanation of each method and its limits.
For mathematical results, use the maths reading guide and the current results and open questions. Each result has its own assumptions and evidence boundary; all eight original problems remain open.
How the components are checked
Components use different checks because the public examples include different kinds of material. Verified source imports compare copied files with their recorded origins. Computed projections and fixture replays use public test inputs in place of private data or live services. Contract validators check declared requirements. External tool runs invoke programs such as Lean or statistics software and record their results. The class names identify these methods; they are not quality ratings.
rank 5 · 39rank 4 · 22rank 3 · 27
A Contract validator receives rank 5 when it checks the component's full declared requirements without relying on a pass or fail answer in the test input. An External tool run receives rank 4: it runs a program such as Lean and checks its exit code and selected output within a stated scope. These ranks describe the checks performed; they do not rank the programs' usefulness or the strength of their mathematical results. The separate Runs real tools marker identifies external tool runs and in-process computation.
Tool runs and runtime computations Runs real tools
Examples include compiling Lean through Lake, evaluating forecasts on sample market data and running a small NumPy model. These components receive rank 4 because the recorded checks cover a limited run. The Runs real tools marker identifies them; it does not extend the stated scope of their results.
Computed projection (27)
A deterministic projection verified by recomputing it from source rather than by a live run; negative cases are policy checks, not real-world validation. Rank 3: the code computes the result, but failure coverage is partial.
Verified source import (21)
A public source body is copied and validated against its origin byte for byte; the check fails on a missing target, a placeholder digest, an unverified body, or a launch or whole-system equivalence overclaim. Rank 5: a fully independent provenance verdict.
Contract validator (20)
The harness derives the verdict over the component's whole declared public contract and can fail with no answer supplied by the fixture. Rank 5: the most independent check on this slice.
Bounded runtime computation (11) Runs real tools
Real in-process computation runs over public inputs with predicted-versus-actual checks and negative cases, scoped to a declared toy runtime. Rank 4: genuine computation, capped at the bounds of that toy scope.
External tool run (9) Runs real tools
A real external tool, such as Lean or Lake, is run and its return code plus output checks are witnessed over a deliberately small scope. Rank 4: genuine execution, capped because the witness is bounded, not a general proof.