The evidence ladder

Evidence isn't binary, and the most useful thing a verification tool can do is tell you honestly how strong each piece of it is. mathema ranks every supported claim by how it was established, from a proof that covers every input in the declared domain down to a sentence someone wrote in a docstring, and it never lets a weaker result be reported as a stronger one.

The rungs, strongest first

Rung	Verdict	What established it
derive, derive:brute_force, derive:math_only	proven	A proof. The body was lifted to a symbolic expression and the claim settled over the whole declared domain (derive); every point of a finite domain was checked (brute_force); or the mathematics was proven and the record reports that line alone, with the computation and what it does with a missing input outside its remit (math_only).
examine	proven	A proof from the function's structure, with nothing lifted: a guard that rejects before the body runs, or a body that writes nothing outside itself.
derive:extensive	proven	The same, reached only by the deeper search you opt into with extensive=True.
derive:brute_force:within_float64	proven	Every point of a finite domain was run and the claim held at each to within float64's precision: at a point with no exact value the float64 result misses the relation by at most 8 unit roundoffs of the value compared against, plus the function's relative condition number times the magnitude of the value it returned there, where both can be read, and a larger miss is not this rung: not counted, so unknown, or a holds on derive:brute_force under a declared tolerance; the record states the largest delta. A point lands here when it has no exact value, including when a decision the body takes on a float (a comparison, a branch, a rounding, a dict key) goes one way in the exact reading and the other in the function's own float run; where every decision goes the same way, the point stays exact. Nothing was left untried, which puts it above sampling; a difference smaller than the stated delta would not show, which puts it below an exact proof.
probe:semi_analytical, probe:algorithmic, probe:minimal_example, probe:counterfactual	holds (n=...)	The real function survived n trials whose inputs were chosen by analysis, such as the points where a denominator vanishes, by a technique specific to the claim, by fuzzing that shrinks what it finds, or by refilling a missing value to see what the function would have done.
probe, probe:lifted_numeric	holds (n=...)	The real function survived n seeded random trials; or, where the claim takes a derivative, integral, sum or limit that running the code cannot give, mathema's own symbolic reconstruction of the function survived n trials (probe:lifted_numeric, and the note says so).
axiom	trusted	A definition row in a compendium, trusted rather than adjudicated: it counts as much as a plain holds, never more.
documented	none	Stated intent that a person has accepted with mathema accept --intent.
declared	none	Stated intent (a docstring summary, an Intent: block, an intent: field) that no person has accepted yet, the weakest rung there is.

derive and examine share the top rung, a proof either way; the informed probing routes share a rung too: they draw on different information, and none is stronger than another. A language's own derive strategy reports derive: followed by its mechanism's name and ranks with derive:extensive; one that names no mechanism (derive:language) ranks with derive. The ladder is defined in the engine as mathema.conjecture.EVIDENCE_LADDER, and a route mathema does not recognise, such as one from a verification technique you have plugged in yourself, ranks below everything it does.

A proof is the mathematics; [float] is the computation

A proven from the derive route means the claim holds in exact real arithmetic over the declared domain, with infinity as infinity, and nothing more. It does not say the computation in float64 gets the same answer. That is a separate claim, and mathema makes it for you: every claim the derive route proves spawns a companion named <name>[float], in the numerical stability family, adjudicated on the probe route against the real code. A printed record shows it as the computation line under the claim, beside the mathematics line that carries the proof; the record file keeps it as its own row, <name>[float]. The companion runs the relation at every corner of the declared domain and at sampled interior points. A raise, a NaN, or an inf or a loss of precision where the relation fails on the executed values falsifies it, with that point as the witness. An unbounded direction runs to the claim's |inf| when one is declared, and otherwise out to float64's maximum (sys.float_info.max, about 1.8e308), sampled log-uniformly so moderate magnitudes are visited too.

import mathema
from mathema.conjecture import claim


def one(x: float) -> float:
    """One, computed the long way round."""
    return (x + 1.0) - x


for law, route in [("for x in [0, 1e6], f(x) == 1", "derive"),
                   ("f(x) == 1", "derive"),
                   ("f(x) == 1", "derive:math_only")]:
    rec = mathema.check(one, claims=[claim(law, name="one", route=route)])
    for p in rec.probes:
        print(f"{route:16} {p.name:10} {p.verdict:9} "
              f"{p.counterexample or ''}".rstrip())

derive           one        proven
derive           one[float] holds
derive           missing[x] holds
derive           one        proven
derive           one[float] falsified x = -1.7976931348623157e+308
derive           missing[x] holds
derive:math_only one        proven

(x + 1) - x is 1 for every real x, so all three proofs stand. The third row of the first block is the policy row mathema writes for a float's nan (what f does with a value that is not there); it holds because f gives nan back. In float64 the + 1 is lost once |x| passes 2^53, so the companion of the unbounded claim is falsified, and its row names the stratum: mathematics sound, its computation numerically unstable (implementation:numerical-instability). Two claims, two verdicts, and the companion gates mathema verify like any other claim. Which remedies apply depends on what the condition number at the witness says. Here it says the loss is the code's: (x + 1) - x is a well-conditioned way to write 1, and the precision goes in the arithmetic rather than in the inputs, so the companion is not accepted on its own. The ways out are to fix the code, to accept the whole claim as a discovery (the proven row and its companion retire together under one acceptance, the witness kept, and the claim no longer counts as proven), to narrow the claim's domain knowingly (edit it, then accept it --as superseded), or to state the claim with route="derive:math_only" ([derive:math_only] in a docstring), which reports the mathematics line only, leaves the computation and its policies (what f does with a missing input) outside its remit, and records the opt-out on the proof's row, which is why the last block above has a single row. Where the loss is inherent in the inputs instead (no float64 computation could do better at the witness), the companion may be accepted alone as a discovery with mathema accept.

Whenever the companion fails along an unbounded direction, as the one above does at -1.8e308, the note also offers let |inf| be B, whatever the conditioning says and whether the witness was a lost digit, an overflow, a NaN or a raise. The binding bounds only the computation and never the proof, which stays over the full domain. mathema runs the claim under the binding before offering it and offers it only where the computation line then holds: B is the condition number's own bound where it gives one and it holds, and otherwise the largest power of ten below the witness's magnitude at which the run holds, found by bisection on the exponent in at most ten runs, which are filed apart from the claim's own evidence. For (x + 1) - x over the reals that is let |inf| be 1e+15, since x + 1.0 is exact below 2^53; where no power of ten holds, nothing is offered.

The companion is written to the verified record beside its parent, with meta.mathema.companion_of naming it. It is never part of the declared layer: it is respawned from its parent on every adjudication, so it does not enter the claims fingerprint and is not repopulated as a claim of its own. A limit or an integral is a statement about the mathematics and spawns no companion.

What sits off the ladder

The ladder ranks how a claim came to be supported. Four other outcomes are reported alongside it, and none of them is a weak form of support:

Verdict	Means
falsified	A counterexample was found by running the function, and it is kept permanently. A falsification is equally definitive whichever route found it.
unknown	An adjudication ran and decided nothing either way, for instance a proof attempt that could not close.
skipped	The claim could not be adjudicated at all, for a reason the record names.
invalidated	A claim that was once proven or holds could no longer be established after the code changed, and the record says what it used to be.

A falsified verdict is knowledge rather than failure: it tells you exactly where the function and the claim part ways, and the accept workflow lets a person decide whether that is a bug in the code or a discovery about the specification.

Why the rungs are kept apart

A result that holds on a thousand random inputs and a result that holds for every input are different kinds of knowledge, and a report that blurs them is telling you what you want to hear. So every verdict carries its route, a holds always carries its trial count, a derive attempt that cannot close hands the claim to the probe route with the reason it stopped kept in the record (a sampled holds never passes itself off as a proof), and a symbolic disproof that nothing can reproduce against the real function, even compared exactly, comes back unknown and flagged instead of falsified, since it more likely points at a fault in the engine than in your code.

Claim-driven development has the full verdict vocabulary, and the derive route covers which functions can reach the top rung.