Warrant

Warrant is a property of the check, not of the number. A grid sample over a continuous action range and an exhaustive enumeration over a declared finite set can both report that no policy flips. Only the second decided it.

Prover	What it does	Label
1	pen-and-paper theorem, within stated hypotheses	PROVED
2	symbolic computation: closed-form identities, algebraic non-existence	PROVED
3 · enumeration	exhaustive enumeration over a finite domain	PROVED, with a completeness certificate
3 · validated	validated numerics over a compact domain	CERTIFIED
3 · sample	sampling a continuum	CORROBORATED

research/warrant_ledger.md carries the canonical version of this table, with the evidence each warrant requires and the tier a number is known to. An action sweep over a continuous range is a finite grid over an infinite domain, so it samples. A policy enumeration over a declared finite set enumerates. EFESelector reports CORROBORATED and EnumeratedEfeSearch reports PROVED for that reason.

CERTIFIED sits between the two. Validated numerics prove a universal over a compact domain, and the proof carries the bound it was computed with. Borrowing PROVED overclaims. Borrowing CORROBORATED throws the bound away.

Warrant

Bases: Enum

How well a claim is warranted, by the prover class that produced it.

PROVED — the claim is decided. A pen-and-paper theorem within its stated hypotheses (Prover 1), a symbolic identity (Prover 2), or a finite domain enumerated in full, where ¬∃ ≡ ∀¬ (Prover 3 · enumeration). Under that last one it is earned only with a completeness certificate. Without one the enumeration is a sample wearing a decision's label.

CERTIFIED — validated numerics prove a universal over a compact domain by construction (Prover 3 · validated). Stronger than a sample, weaker than a decision, and it carries the bound it was computed with. Collapsing it into PROVED overclaims. Collapsing it into CORROBORATED throws the bound away.

CORROBORATED — a sample of a continuum (Prover 3 · sample). It exhibits existence and refutes a universal by counterexample. It never decides one, at any sample count.

Orthogonal to outcome. A check reports both, and the three levels print in distinct vocabulary so a corroborative green run is visibly that.

What a check emits

A registered falsifier does not pass. It fires or it does not, and PASS is absent from the vocabulary rather than disambiguated by a column beside it.

Outcome has five values because five things can happen to a falsifier, and they are not interchangeable. It ran and did not fire, so the claim survives it. It fired, and the refutation is the result. It ran and the ordering came out genuinely undetermined, because the two quantities' intervals overlap. It was void by construction and could not have fired here, so it is evidence for nothing and is not a survivor. Or it was measured elsewhere and did not run here at all. Collapsing the last three loses the survivor accounting, and burns the word a real tie needs.

Tier says what the check was measured against, and cuts across the other two rather than ranking them. An EXACT closed-form reference can be sampled, and an exhaustive enumeration can produce a COMPUTED number.

A check that never ran carries no warrant. CORROBORATED means sampling-grade evidence was obtained, so attributing it to a falsifier that sampled nothing claims evidence that does not exist. The warrant is None there and prints as —, enforced at construction.

A PROVED report needs evidence, enforced at construction. There are two kinds, one per decisive prover. CompletenessCertificate backs an exhaustive enumeration over a finite domain. SymbolicReduction backs a theorem or a symbolic identity (Provers 1 and 2), which decide by argument and enumerate nothing, so a certificate is the wrong evidence for them rather than a missing one. The weaker levels need none, because a bound and a sample carry their story in detail. Report PROVED with nothing behind it and the constructor raises.

Those two are the only things the evidence tuple accepts. A path naming where the proof lives is the plausible substitute, and it satisfies a presence check exactly as well as a certificate does. So the constructor checks every item's kind. Checking only the first would let a claim over several enumerations carry one certificate and three references to a write-up. The weaker levels are held to the same rule. They need no evidence, so a tuple on one of them is something the report says it is carrying.

Outcome

Bases: Enum

What a registered falsifier did, independent of how well it was warranted.

A falsifier does not pass. It fires or it does not, and the words are chosen so that a run cannot be read as a column of PASS with the interesting distinctions flattened out of it.

NOT_TRIGGERED — it ran, the condition did not obtain, the claim survives it. FIRED — the condition obtained. The claim is refuted, and that is the result. NOT_RESOLVED — it ran and the ordering is genuinely undetermined, because the two quantities' intervals overlap. Narrow on purpose: this is a measured tie, not a stand-in for a check that did not run. NOT_APPLICABLE — void by construction. It could not have fired here, so it is evidence for nothing and does not count among the survivors. NOT_RUN_HERE — measured elsewhere, or not yet. The detail says where.

The last two never ran, so they carry no warrant. CheckReport enforces that.

Tier

Bases: Enum

What the check was measured against.

EXACT — a closed-form reference at machine precision. BOUNDED — a stated bar, or a certified bracket. COMPUTED — no statable bar. The word for such a number is computed, never certified.

Cuts across warrant and outcome rather than ranking them. An EXACT reference can be sampled (Prover 3 · sample) and a COMPUTED number can come out of an exhaustive enumeration (Prover 3 · enumeration).

CompletenessCertificate dataclass

CompletenessCertificate(
    expected: int,
    visited: int,
    warrant: Warrant,
    action_set_size: int,
    horizon: int,
    action_set_version: str,
)

Evidence an enumeration was exhaustive: expected vs visited (ADR-030).

Two independent facts, and a PROVED warrant needs both. Domain: expected == action_set_size ** horizon, so the set quantified over is the declared one. Coverage: visited == expected, so it was enumerated in full. They come apart wherever visited is a loop-carried counter rather than an array's length, which is where a padding bug lives, and coverage alone is what carries the Prover 3 · enumeration licence.

The certificate names its set. expected on its own conflates the base with the exponent — 81 is 9**2 and 3**4 — so a bare count is not self-describing and two certificates over different sets cannot be told apart. Carrying the size, the horizon and the version fixes that at the type rather than in the surrounding prose (standing prohibition 9).

A partial enumeration sampled its set, so its warrant is CORROBORATED. Pairing PROVED with a shortfall does not construct.

Parameters:

Name	Type	Description	Default
expected	int	the policy count the search was obliged to visit — |A|^H, supplied rather than derived, so the domain check compares two routes.	required
visited	int	how many it actually visited.	required
warrant	Warrant	the prover class the enumeration earns.	required
action_set_size	int	the declared action count — |A|.	required
horizon	int	the sequence length — H.	required
action_set_version	str	the declared set's version tag.	required

Raises:

Type	Description
ValueError	if the warrant is PROVED and either precondition fails.

domain_declared property

domain_declared: bool

Whether expected is the declared set's own |A|^H.

complete property

complete: bool

Whether every expected policy was visited.

__post_init__

__post_init__() -> None

Reject a PROVED certificate failing domain or coverage.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __post_init__(self) -> None:
    """Reject a ``PROVED`` certificate failing domain or coverage."""
    if self.warrant is not Warrant.PROVED:
        return
    if not self.domain_declared:
        raise ValueError(
            f"a PROVED certificate must quantify over the declared set, got "
            f"expected={self.expected} against |A|^H = "
            f"{self.action_set_size}^{self.horizon} = "
            f"{self.action_set_size**self.horizon} for set "
            f"{self.action_set_version!r}. The count and the set have come apart."
        )
    if not self.complete:
        raise ValueError(
            f"a PROVED certificate must be complete, got expected="
            f"{self.expected} against visited={self.visited}. A partial "
            "enumeration sampled its set, so its warrant is CORROBORATED."
        )

__str__

__str__() -> str

The certificate as a one-line warrant string in its own vocabulary.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __str__(self) -> str:
    """The certificate as a one-line warrant string in its own vocabulary."""
    return (
        f"{self.warrant.value} (set {self.action_set_version}, "
        f"|A|^H = {self.action_set_size}^{self.horizon} = {self.expected}, "
        f"visited {self.visited})"
    )

CheckReport dataclass

CheckReport(
    name: str,
    warrant: Warrant | None,
    outcome: Outcome,
    tier: Tier,
    detail: str,
    evidence: tuple[Evidence, ...] = (),
    provenance: tuple[Provenance, ...] = (),
)

One check's result: what it found, how well, and against what.

A record rather than a return value. Frozen, because editing a report after the check ran is editing the finding.

Parameters:

Name	Type	Description	Default
name	str	which check this is, as it appears in the summary.	required
warrant	Warrant | None	the prover class behind the claim, or None where the check produced no evidence to classify.	required
outcome	Outcome	what the falsifier did.	required
tier	Tier	what the check was measured against.	required
detail	str	why it reports what it reports, in one line. Required, so a report cannot be a bare outcome with extra fields.	required
evidence	tuple[Evidence, ...]	what backs the claim, as a tuple of CompletenessCertificate and SymbolicReduction. Required non-empty when the warrant is PROVED and unused otherwise. A tuple rather than one item because a claim quantified over several enumerations rests on all their certificates, and carrying one of them understates what was checked.	()
provenance	tuple[Provenance, ...]	which ref registered the claim and which one measured it, as a tuple. Required non-empty when the warrant is PROVED, unused otherwise. A tuple on the same argument the evidence is one: a claim resting on two registrations rests on both, and carrying one of them understates what a reviewer has to check.	()

Raises:

Type	Description
ValueError	if the warrant is PROVED and no evidence or no provenance was given, if a check that never ran here carries a warrant anyway, if the evidence or the provenance is not a tuple, or if an item in either is not one of the kinds it accepts.

__post_init__

__post_init__() -> None

Reject a claim with nothing behind it, at either of two strengths.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __post_init__(self) -> None:
    """Reject a claim with nothing behind it, at either of two strengths."""
    if not isinstance(self.evidence, tuple):
        raise ValueError(
            f"check {self.name!r} passed evidence as "
            f"{type(self.evidence).__name__}. Evidence is a tuple, so a claim "
            "resting on several enumerations can carry all of their certificates. "
            "Wrap a single one: (certificate,)."
        )
    if self.evidence:
        for item in self.evidence:
            if not isinstance(item, _EVIDENCE_TYPES):
                raise ValueError(
                    f"check {self.name!r} carries a "
                    f"{type(item).__name__} as evidence. There are two kinds, one "
                    "per decisive prover: a CompletenessCertificate for an "
                    "exhaustive enumeration (Prover 3 · enumeration), a "
                    "SymbolicReduction for a theorem or a symbolic identity "
                    "(Provers 1 and 2). Anything "
                    "else satisfies the PROVED precondition by being present and "
                    "backs nothing."
                )
    if not isinstance(self.provenance, tuple):
        raise ValueError(
            f"check {self.name!r} passed provenance as "
            f"{type(self.provenance).__name__}. Provenance is a tuple, so a claim "
            "resting on two registrations can carry both. Wrap a single one: "
            "(provenance,)."
        )
    for item in self.provenance:
        if not isinstance(item, Provenance):
            raise ValueError(
                f"check {self.name!r} carries a {type(item).__name__} as "
                "provenance. A bare ref, or a sentence saying the bar came first, "
                "satisfies the precondition by being present and leaves a reviewer "
                "with one end of an ordering and no way to check it. Pass a "
                "Provenance, which validates both refs and says what was "
                "registered at the first of them."
            )
    if self.warrant is Warrant.PROVED and len(self.evidence) == 0:
        raise ValueError(
            f"check {self.name!r} reports PROVED with no evidence. A decided "
            "universal needs something statable behind it: a completeness "
            "certificate for an exhaustive enumeration (Prover 3 · enumeration), a "
            "SymbolicReduction for a theorem or a symbolic identity (Provers 1 "
            "and 2). Report CERTIFIED for a bound over a compact domain, "
            "CORROBORATED for a sample."
        )
    if self.warrant is Warrant.PROVED and len(self.provenance) == 0:
        raise ValueError(
            f"check {self.name!r} reports PROVED with no provenance. A decided "
            "universal says which ref registered the claim and which one measured "
            "it, so a reader can check that the bar was fixed before the number "
            "existed rather than take the ordering on trust. Registering and "
            "measuring at one ref is allowed and renders as such. Report CERTIFIED "
            "or CORROBORATED where there was no registration at all."
        )
    if self.outcome not in _TESTED_HERE and self.warrant is not None:
        raise ValueError(
            f"check {self.name!r} is {self.outcome.value} and carries the warrant "
            f"{self.warrant.value}. It produced no evidence here, so there is no "
            "prover class to report. Leave the warrant None."
        )

__str__

__str__() -> str

The report as one summary line, in the warrant's own vocabulary.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __str__(self) -> str:
    """The report as one summary line, in the warrant's own vocabulary."""
    warrant = self.warrant.value if self.warrant else "—"
    line = (
        f"{self.name}: {self.outcome.value} "
        f"({warrant}, tier {self.tier.value}). {self.detail}"
    )
    if not self.provenance:
        return line
    return f"{line} {' '.join(str(item) for item in self.provenance)}"

Evidence a symbolic claim carries

A CAS is a checker, not a witness. It establishes that one expression equals another, and it has nothing to say about whether those expressions are the ones the analytic claim is about. The warrant ledger records that step as a human obligation, which is the condition on Prover 2 being theorem-grade at all.

SymbolicReduction is where the obligation is discharged rather than assumed. correspondence names where the setup was analytically checked against the problem: a hand derivation by file and line, or a dated registration result. A field that cannot be filled honestly is the signal to report CORROBORATED and say why, so the type is not a formality. Blank fields do not construct.

Blank means blank to a reader rather than empty to str.strip(), which strips the whitespace and leaves the zero-width formatting characters behind. A field that is not text, one holding only whitespace, one holding only zero-width characters, and one carrying a line break into a one-line render are all refused. assumptions is checked entry by entry, and the message names which entry.

assumptions carries the scope. An identity contingent on smoothness, on positivity, or on an expansion being formal rather than convergent is a different claim from one that is not, and the difference belongs beside the evidence instead of in the algebra a reader would have to redo.

SymbolicReduction dataclass

SymbolicReduction(
    claim: str,
    correspondence: str,
    assumptions: tuple[str, ...] = (),
)

What backs a Prover 2 claim: the correspondence a CAS cannot supply.

A CAS checks that one expression equals another. It does not check that those expressions are the ones the analytic claim is about. That step is a human obligation, named as such in the warrant ledger, and this is where it is recorded instead of assumed. A reduction is evidence for CheckReport on the same terms as a completeness certificate, and the two are interchangeable there.

Parameters:

Name	Type	Description	Default
claim	str	the analytic statement, in words, that the symbolic identity stands for.	required
correspondence	str	where the symbolic setup was analytically checked against the problem it stands for. A hand derivation by file and line, or a dated registration result.	required
assumptions	tuple[str, ...]	what the reduction assumed, one condition per entry. The scope travels with the evidence, so the contingency is visible without reading the algebra.	()

Raises:

Type	Description
ValueError	if the assumptions are not a tuple, or if the claim, the correspondence or any assumption is not one-line text with a visible character in it.

__post_init__

__post_init__() -> None

Reject a reduction that records no obligation to have discharged.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __post_init__(self) -> None:
    """Reject a reduction that records no obligation to have discharged."""
    if not isinstance(self.assumptions, tuple):
        raise ValueError(
            "symbolic reduction passed assumptions as "
            f"{type(self.assumptions).__name__}. Assumptions are a tuple, so a "
            "bare string records one condition per character and the identity's "
            "scope reads as gibberish. Wrap a single one: (assumption,)."
        )
    for name, value in (
        ("claim", self.claim),
        ("correspondence", self.correspondence),
    ):
        _reject_unreadable(
            "symbolic reduction",
            name,
            value,
            "Prover 2 is theorem-grade only where the symbolic setup was hand "
            "derived against the analytic problem, so a reduction naming neither "
            "the statement nor where it was checked backs nothing. Fill both, or "
            "report CORROBORATED and say why in the check's detail.",
        )
    for position, assumption in enumerate(self.assumptions, start=1):
        _reject_unreadable(
            "symbolic reduction",
            f"assumption {position}",
            assumption,
            "An entry nobody filled in is scope a reader cannot check, and it "
            "renders as a gap in the list rather than as a caveat. Say what the "
            "condition is, or drop the entry.",
        )

__str__

__str__() -> str

The reduction as one line: the claim, where it was checked, its scope.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __str__(self) -> str:
    """The reduction as one line: the claim, where it was checked, its scope."""
    scope = (
        f"assuming {'; '.join(self.assumptions)}"
        if self.assumptions
        else "no assumptions recorded"
    )
    return f"symbolic: {self.claim} (per {self.correspondence}, {scope})"

Registration, and the ordering it claims

Evidence says a claim was decided. It does not say when the bar was set, and a bar chosen after the number is visible decides nothing at all. Provenance is the pointer a reviewer follows to check: the ref where the prediction, the bar or the derivation was registered, the ref whose tree produced the number, and one line saying what they will find at the first of them.

A ref is a git commit SHA, an http(s) URL or a DOI. A path, a branch, a tag and HEAD are refused. Each of them satisfies a presence check exactly as well as a commit does, and each resolves to a different tree every time it is read. A URL is taken to be a permalink; one that tracks a branch has the same defect and the type cannot tell the two apart.

Where the two refs name one commit, the render says the ordering is not established by history. Registering and measuring together is not refused. It is what happens whenever a check and the derivation behind it land in one go, and the honest reading is that the ordering rests on the surrounding prose rather than on anything a reviewer can verify. An abbreviated ref counts as the same commit, or lengthening one of the two hashes would walk away from the marker while naming the same thing.

What the type cannot do is order two refs. Equality is checkable in a string and ordering is not, so a registration written after the fact renders exactly like one written before. That is a git merge-base --is-ancestor away, which is a reviewer's job or a test's, and is the reason the refs are refs.

Provenance dataclass

Provenance(
    registered_at: str, measured_at: str, registered: str
)

Which ref registered a claim, and which one measured it.

A number checked against a bar is worth reading only if the bar was fixed before the number existed. A report says what was decided and how well it was decided, and nothing in it says when the bar was set. This is the ref a reviewer opens to find out.

Where the two refs name one commit, the render says so. Registering and measuring together is not refused. The ordering then rests on the account the surrounding prose gives, and the marker is what stops a reader taking it for something the history shows.

History orders two refs. A string cannot. Equality is checkable here and ordering is not, so a registered_at that in fact came after measured_at renders exactly like one that came before. Establishing the direction is a reviewer, or a test, running git merge-base --is-ancestor.

Parameters:

Name	Type	Description	Default
registered_at	str	the ref where the prediction, the bar or the derivation was registered. A git commit SHA, an http(s) URL, or a DOI. A URL is taken to be a permalink. One that tracks a branch moves, which is the defect that rules a bare path out.	required
measured_at	str	the ref whose tree produced the number, in the same three shapes.	required
registered	str	what a reviewer will find at registered_at, in one line. A ref on its own sends them to a diff and leaves them to work out which part of it was the registration.	required

Raises:

Type	Description
ValueError	if either ref is not one-line text in one of the three shapes, or if registered is not one-line text with a visible character in it.

same_ref property

same_ref: bool

Whether the two refs name one commit, so history orders nothing.

An abbreviation counts. Without that, lengthening one of the two hashes walks away from the marker while still naming the same commit.

__post_init__

__post_init__() -> None

Reject a ref that resolves to nothing, and a statement nobody wrote.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __post_init__(self) -> None:
    """Reject a ref that resolves to nothing, and a statement nobody wrote."""
    for name, value in (
        ("registered_at", self.registered_at),
        ("measured_at", self.measured_at),
    ):
        _reject_unreadable(
            "provenance",
            name,
            value,
            "The ordering is the whole content of a provenance, so one end of it "
            "missing records no ordering at all. Give the ref, or report "
            "CORROBORATED and say in the check's detail why there is none.",
        )
        _reject_unresolvable(name, value)
    _reject_unreadable(
        "provenance",
        "registered",
        self.registered,
        "A bare ref sends a reviewer to a diff and leaves them to work out which "
        "part of it was the registration. Say what they will find there.",
    )

__str__

__str__() -> str

The provenance as one line: what was registered, where, against what.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def __str__(self) -> str:
    """The provenance as one line: what was registered, where, against what."""
    if self.same_ref:
        return (
            f"provenance: {self.registered} (registered and measured at "
            f"{self.registered_at}, so the ordering is not established by history)"
        )
    return (
        f"provenance: {self.registered} "
        f"(registered at {self.registered_at}, measured at {self.measured_at})"
    )

The evidence union

Evidence names the two kinds together. CheckReport.evidence is annotated as a tuple of it, so the admissible types are declared once, and a caller building reports of its own has a name to annotate against.

The union and the runtime guard are separate declarations. A third evidence kind needs a member added to both. A type added to one alone annotates as evidence and then refuses to construct, or constructs and reads as evidence of a kind nothing declared.

Evidence module-attribute

Evidence = CompletenessCertificate | SymbolicReduction

What backs a PROVED claim, one member per decisive prover the suite runs.

A completeness certificate decides by exhausting a finite domain. A symbolic reduction decides by identity (Provers 1 and 2) and enumerates nothing, so a certificate is the wrong evidence for it rather than a missing one.

Reading a run

Registering four falsifiers and testing two is a different claim from testing four, and one number cannot carry both. The header separates them and names how many fired. The rows underneath say what warrant the tested ones carried, so a run that survived everything without deciding anything reads as exactly that.

4 registered, 2 tested here, none fired
   PROVED        NOT TRIGGERED   2
   —             NOT APPLICABLE  1
   —             NOT RUN HERE    1

check_summary

check_summary(reports: Sequence[CheckReport]) -> str

Counts per (warrant, outcome) across a run, as a block of lines.

The header carries the accounting a reader needs first: how many falsifiers were registered, how many this run actually tested, and how many fired. Registering four and testing two is a different claim from testing four, and one number cannot say both. The rows underneath say what warrant the tested ones carried, so a run that survived everything without deciding anything prints as exactly that.

Pairs with no checks are left out, so the block is as long as the run was varied. Ordering follows the enum declarations rather than the input, so two runs of the same suite produce the same text. Checks with no warrant sort last, under —.

Parameters:

Name	Type	Description	Default
reports	Sequence[CheckReport]	the run's reports, in any order.	required

Returns:

Type	Description
str	A newline-separated block: the accounting line, then one row per occupied pair.

Source code in packages/warrantlib/src/warrantlib/__init__.py

def check_summary(reports: Sequence[CheckReport]) -> str:
    """Counts per ``(warrant, outcome)`` across a run, as a block of lines.

    The header carries the accounting a reader needs first: how many falsifiers were
    registered, how many this run actually tested, and how many fired. Registering four
    and testing two is a different claim from testing four, and one number cannot say
    both. The rows underneath say what warrant the tested ones carried, so a run that
    survived everything without deciding anything prints as exactly that.

    Pairs with no checks are left out, so the block is as long as the run was varied.
    Ordering follows the enum declarations rather than the input, so two runs of the
    same suite produce the same text. Checks with no warrant sort last, under ``—``.

    Args:
        reports: the run's reports, in any order.

    Returns:
        A newline-separated block: the accounting line, then one row per occupied pair.
    """
    counts = Counter((report.warrant, report.outcome) for report in reports)
    tested = sum(1 for report in reports if report.outcome in _TESTED_HERE)
    fired = sum(1 for report in reports if report.outcome is Outcome.FIRED)
    lines = [
        f"{len(reports)} registered, {tested} tested here, "
        f"{f'{fired} fired' if fired else 'none fired'}"
    ]
    lines += [
        f"   {(warrant.value if warrant else '—'):<13} "
        f"{outcome.value:<15} {counts[warrant, outcome]}"
        for warrant in (*Warrant, None)
        for outcome in Outcome
        if counts[warrant, outcome]
    ]
    return "\n".join(lines)