API reference

Generated directly from docstrings, so it never drifts from what the code actually does.

mathema

mathema

mathema: Claim-Driven Development, turning software intent into verifiable evidence.

import mathema
r = mathema.check(my_function, claims=["f(-x) == -f(x)"])
print(r)
mathema.write_spec(my_function, claims=[...])   # also writes the record

State a claim, verify it against the real function, keep the record. Every claim is adjudicated on one of two evidence routes: derive lifts the function's body to a sympy expression and decides the claim algebraically (proven is exact, not sampled, see symbolic.py), or probe calls the real function on sampled/seeded inputs and checks the claim numerically (holds (n=...)/falsified, see probing.py). A function that can't be lifted (a loop, a non-scalar parameter, ...) still gets probe-route coverage; derive is strictly stronger evidence where it applies, not a replacement for probe. Every claim binds to the function's identity hashes so a later change is caught, not silently inherited.

A bare string claim (as above) takes the best route: a symbolic proof is attempted first, and a claim the proof cannot decide falls through to probing, so the returned entry's route names the mechanism that settled it. To pin the route, build the claim with route="derive" or route="probe" and pass it in the same claims= list; mathema.check() accepts a pre-built claim object exactly as it accepts a string, so nothing else about the call changes:

r = mathema.check(my_function,
                  claims=[mathema.claims.claim("f(-x) == -f(x)", route="derive")])

A proven verdict routed derive means the proof decided it, never sampling. When the proof cannot decide, the claim still falls through to probing, and Probe.meta["mathema.derive_status"] on the returned entry ("unliftable" vs. "undecided") records why the proof stopped; see authoring.md's own claim-grammar section for the full grammar (d(...)/lim(...)/integrate(...)/Sum(...), domain quantifiers, raises(...)) route="derive" understands. mathema.claims is this same claim()/check_conjectures() pair exposed directly, for calling the derive route standalone without check()'s own built-in-law probing:

results = mathema.claims.check_conjectures(
    my_function, [mathema.claims.claim("f(-x) == -f(x)", route="derive")])

This package implements the Claim-Driven Development spec: see the sibling claim-driven-development repo's v0.2.0/ for the workflow definition and the record schema this package reads and writes (SPEC_VERSION below states which version).

Record dataclass

The result of checking a function's claims: the facts read off it, and one Probe per claim adjudicated (built-in laws plus any claims passed in). See the claim-driven-development repo's v0.2.0/record-schema.md for the YAML shape this turns into via to_spec()/save_spec().

Source code in mathema/__init__.py

@dataclass
class Record:
    """The result of checking a function's claims: the facts read off it,
    and one Probe per claim adjudicated (built-in laws plus any claims
    passed in). See the claim-driven-development repo's
    v0.2.0/record-schema.md for the YAML shape this turns into via
    to_spec()/save_spec()."""
    facts: Facts
    probes: list[Probe]
    spec_path: str | None = None
    # `lifted` holds the derive route's own symbolic-lift result
    # (symbolic.Lifted) when the body lifts to a closed form, None
    # otherwise; every reader treats None as a valid value. `concepts`
    # is reserved for a future understanding/Mathemata layer and is
    # always empty.
    lifted: object | None = field(default=None, repr=False)
    concepts: list = field(default_factory=list, repr=False)
    dependencies: list = field(default_factory=list, repr=False)
    # one-deep callee records (inventory.function_dependencies): every
    # sibling function/class/module this function references, with key,
    # file, line, and (for functions) the form hash freshness checks
    # compare against, written into the verified spec as its own
    # section, annotated with per-dependency freshness at record time.
    # namespaced extension data, the same role Probe.meta already plays
    # for one claim; this is the function-level counterpart, for data
    # that isn't a stable, always-computed field (diagnostics.
    # diagnostic_report(), opted into per function, is one user:
    # "mathema.diagnostic_report" -> its own dict). check() fills
    # "mathema.effects" (what examining the source finds the function
    # does, stated under it) and "mathema.not_run" (a check of its own
    # battery mathema could not make: the call, the reason, the gap);
    # anything else a caller sets explicitly
    # when it wants the extra work done.
    meta: dict = field(default_factory=dict, repr=False)
    # the dotted key the function's claims are filed under, which the
    # printed record's commands name; the function's name when unset
    key: str | None = field(default=None, repr=False)

    def __repr__(self) -> str:
        return self.render()

    def render(self, families: bool = False) -> str:
        """Intent:
            The record as it prints. Where the function states claims of
            its own (a docstring `Claims:` block, a decorator, `declared=`,
            `claims=`), those come first and the rows mathema volunteered
            (the built-in families a bare `check(fn)` runs, row source
            `suggested` or `builtin`) fold under one count line;
            `families=True` prints every row in the order adjudicated,
            the folded rows included. A record with no stated claim
            prints every row.
        """
        from .analysis import tier_word
        from ._layout import blocks
        from ._missing_words import count_words as _count_words
        lines = [f"mathema.Record({self.facts.name}) · "
                 f"{tier_word(self.facts.tier, self.probes, (self.meta or {}).get('mathema.effects'))} "
                f"· form {self.facts.form}"]
        effects = (self.meta or {}).get("mathema.effects")
        if effects and effects.get("line") \
                and effects["line"] != "no side effects":
            # the header already says a function has no side effects;
            # anything more is stated under it
            lines.append(f"  effects: {effects['line']}")
        not_read = (self.meta or {}).get("mathema.compendium_not_read")
        if not_read:
            lines.append(f"  note: {not_read}")
        # a claim with lines under it prints as a block (see _layout)
        grouped = blocks(self.probes, list(self.facts.params),
                         dict(self.facts.param_kinds), self.key or self.facts.name,
                         _count_words)
        starts: list = []
        for p in self.probes:
            starts.append((p, len(lines)))
            if id(p) in grouped:
                lines.extend(grouped[id(p)])
                continue
            if id(p) in grouped["used"]:
                continue
            mark = {"holds": "holds    ", "falsified": "falsified", "proven": "proven   ",
                    "skipped": "unknown  ", "unknown": "unknown  ",
                    "invalidated": "invalidated"}.get(p.verdict.split(":", 1)[0], p.verdict)
            if p.verdict == "skipped:misspecified":
                mark = "misspecified"
            missing = (p.meta or {}).get("mathema.missing") or {}
            pol = (p.meta or {}).get("mathema.policy")
            if pol:
                # a policy row: its name and claim, where it came from, and
                # the next step when it does not hold; a row with no single
                # behaviour to state reads as a sentence
                if pol.get("sentence"):
                    line = f"  {mark} {p.name}: {pol['sentence']}"
                elif p.verdict.startswith(("unknown", "skipped")):
                    line = f"  {mark} {p.name}: {p.statement}"
                    if pol.get("reason") or p.note:
                        line += "\n           " + _pad(str(pol.get('reason') or p.note))
                else:
                    line = f"  {mark} {p.name}: {p.statement}"
                    if pol.get("reason"):
                        line += f"   [{pol['reason']}]"
                for extra in (pol.get("said"), pol.get("next")):
                    if extra and p.verdict not in ("holds", "proven"):
                        line += "\n           " + _pad(str(extra))
                lines.append(line)
                continue
            gate = (p.meta or {}).get("mathema.gate")
            if gate and p.sketch:
                # a gate names what each parameter's members do and whose
                # word it is; a falsified one its witness and next step
                line = f"  {mark} {p.name}: {p.statement}"
                line += "\n           " + _pad(str(p.sketch))
                if p.counterexample:
                    line += f"\n           counterexample {_pad(str(p.counterexample))}"
                if gate.get("next") and p.verdict not in ("holds", "proven"):
                    line += "\n           " + _pad(str(gate['next']))
                lines.append(line)
                continue
            if p.verdict == "proven":
                # a proof has no trial count the way a probe does: the
                # quantifier (who it holds for) stands in place of
                # "(n=...)", on its own line since it's often longer than
                # the statement it qualifies, with what a missing value
                # of each parameter means
                line = f"  {mark} {p.name}: {p.statement}"
                if (p.route or "").endswith(":within_float64"):
                    # every point run in float64: the count and the
                    # largest delta beside the statement
                    from .records import within_float64_words
                    said = within_float64_words(p.meta)
                    if said:
                        line += f"  ({said})"
                detail = "; ".join(t for t in (p.condition, missing.get("means")) if t)
                if detail:
                    line += f"\n           {detail}"
            else:
                shown = p.statement
                if (p.condition or "").startswith("let |inf| be ") \
                        and "|inf|" not in (shown or ""):
                    # the pseudo-infinity that bounded the computation
                    shown = f"{p.condition.split(', ', 1)[0]}, {shown}"
                line = f"  {mark} {p.name}: {shown}"
                if p.verdict == "holds" and p.n:
                    from ._missing_words import count_words
                    line += f" ({count_words(p.n, (p.meta or {}).get('mathema.drawn'))})"
            if p.verdict != "proven" and p.note and (
                    p.verdict.split(":", 1)[0] in ("unknown", "skipped")
                    or missing.get("said") or missing.get("returned")):
                # what happened at a missing input, or why the row is
                # open, said once under the row
                line += "\n           " + _pad(str(p.note))
            elif p.verdict == "proven" and (missing.get("said") or missing.get("returned")) \
                    and p.note:
                line += "\n           " + _pad(str(p.note))
            if p.counterexample:
                line += f"\n           counterexample {_pad(str(p.counterexample))}"
            if (p.meta or {}).get("mathema.correction"):
                line += "\n           " + _pad(str(p.meta["mathema.correction"]))
            for said in (p.meta or {}).get("mathema.let_warning") or ():
                line += f"\n           warning: {said}"
            stratum = getattr(p, "stratum", None)
            if stratum:
                # which stratum the falsification indicts, one line:
                # the verdict above is unchanged, this only classifies
                parts = []
                if stratum.get("mathematics"):
                    parts.append(f"mathematics {stratum['mathematics']}")
                if stratum.get("cause"):
                    parts.append(stratum["cause"])
                elif stratum.get("blame"):
                    parts.append(f"blame {stratum['blame']}")
                if parts:
                    line += f"\n           [{', '.join(parts)}]"
            lines.append(line)
        if not families:
            lines = _ranked_lines(self.probes, lines, starts)
        return "\n".join(lines)

    def to_spec(self) -> dict:
        from .spec import to_spec
        return to_spec(self)

    def save_spec(self, path: str) -> str:
        """Write the decoupled spec: intent, identity, claims, references,
        and the reasoning chain, as standalone YAML bound to the identity
        hashes."""
        from .spec import save_spec
        return save_spec(self, path)

render(families=False)

Intent: The record as it prints. Where the function states claims of its own (a docstring Claims: block, a decorator, declared=, claims=), those come first and the rows mathema volunteered (the built-in families a bare check(fn) runs, row source suggested or builtin) fold under one count line; families=True prints every row in the order adjudicated, the folded rows included. A record with no stated claim prints every row.

Source code in mathema/__init__.py

def render(self, families: bool = False) -> str:
    """Intent:
        The record as it prints. Where the function states claims of
        its own (a docstring `Claims:` block, a decorator, `declared=`,
        `claims=`), those come first and the rows mathema volunteered
        (the built-in families a bare `check(fn)` runs, row source
        `suggested` or `builtin`) fold under one count line;
        `families=True` prints every row in the order adjudicated,
        the folded rows included. A record with no stated claim
        prints every row.
    """
    from .analysis import tier_word
    from ._layout import blocks
    from ._missing_words import count_words as _count_words
    lines = [f"mathema.Record({self.facts.name}) · "
             f"{tier_word(self.facts.tier, self.probes, (self.meta or {}).get('mathema.effects'))} "
            f"· form {self.facts.form}"]
    effects = (self.meta or {}).get("mathema.effects")
    if effects and effects.get("line") \
            and effects["line"] != "no side effects":
        # the header already says a function has no side effects;
        # anything more is stated under it
        lines.append(f"  effects: {effects['line']}")
    not_read = (self.meta or {}).get("mathema.compendium_not_read")
    if not_read:
        lines.append(f"  note: {not_read}")
    # a claim with lines under it prints as a block (see _layout)
    grouped = blocks(self.probes, list(self.facts.params),
                     dict(self.facts.param_kinds), self.key or self.facts.name,
                     _count_words)
    starts: list = []
    for p in self.probes:
        starts.append((p, len(lines)))
        if id(p) in grouped:
            lines.extend(grouped[id(p)])
            continue
        if id(p) in grouped["used"]:
            continue
        mark = {"holds": "holds    ", "falsified": "falsified", "proven": "proven   ",
                "skipped": "unknown  ", "unknown": "unknown  ",
                "invalidated": "invalidated"}.get(p.verdict.split(":", 1)[0], p.verdict)
        if p.verdict == "skipped:misspecified":
            mark = "misspecified"
        missing = (p.meta or {}).get("mathema.missing") or {}
        pol = (p.meta or {}).get("mathema.policy")
        if pol:
            # a policy row: its name and claim, where it came from, and
            # the next step when it does not hold; a row with no single
            # behaviour to state reads as a sentence
            if pol.get("sentence"):
                line = f"  {mark} {p.name}: {pol['sentence']}"
            elif p.verdict.startswith(("unknown", "skipped")):
                line = f"  {mark} {p.name}: {p.statement}"
                if pol.get("reason") or p.note:
                    line += "\n           " + _pad(str(pol.get('reason') or p.note))
            else:
                line = f"  {mark} {p.name}: {p.statement}"
                if pol.get("reason"):
                    line += f"   [{pol['reason']}]"
            for extra in (pol.get("said"), pol.get("next")):
                if extra and p.verdict not in ("holds", "proven"):
                    line += "\n           " + _pad(str(extra))
            lines.append(line)
            continue
        gate = (p.meta or {}).get("mathema.gate")
        if gate and p.sketch:
            # a gate names what each parameter's members do and whose
            # word it is; a falsified one its witness and next step
            line = f"  {mark} {p.name}: {p.statement}"
            line += "\n           " + _pad(str(p.sketch))
            if p.counterexample:
                line += f"\n           counterexample {_pad(str(p.counterexample))}"
            if gate.get("next") and p.verdict not in ("holds", "proven"):
                line += "\n           " + _pad(str(gate['next']))
            lines.append(line)
            continue
        if p.verdict == "proven":
            # a proof has no trial count the way a probe does: the
            # quantifier (who it holds for) stands in place of
            # "(n=...)", on its own line since it's often longer than
            # the statement it qualifies, with what a missing value
            # of each parameter means
            line = f"  {mark} {p.name}: {p.statement}"
            if (p.route or "").endswith(":within_float64"):
                # every point run in float64: the count and the
                # largest delta beside the statement
                from .records import within_float64_words
                said = within_float64_words(p.meta)
                if said:
                    line += f"  ({said})"
            detail = "; ".join(t for t in (p.condition, missing.get("means")) if t)
            if detail:
                line += f"\n           {detail}"
        else:
            shown = p.statement
            if (p.condition or "").startswith("let |inf| be ") \
                    and "|inf|" not in (shown or ""):
                # the pseudo-infinity that bounded the computation
                shown = f"{p.condition.split(', ', 1)[0]}, {shown}"
            line = f"  {mark} {p.name}: {shown}"
            if p.verdict == "holds" and p.n:
                from ._missing_words import count_words
                line += f" ({count_words(p.n, (p.meta or {}).get('mathema.drawn'))})"
        if p.verdict != "proven" and p.note and (
                p.verdict.split(":", 1)[0] in ("unknown", "skipped")
                or missing.get("said") or missing.get("returned")):
            # what happened at a missing input, or why the row is
            # open, said once under the row
            line += "\n           " + _pad(str(p.note))
        elif p.verdict == "proven" and (missing.get("said") or missing.get("returned")) \
                and p.note:
            line += "\n           " + _pad(str(p.note))
        if p.counterexample:
            line += f"\n           counterexample {_pad(str(p.counterexample))}"
        if (p.meta or {}).get("mathema.correction"):
            line += "\n           " + _pad(str(p.meta["mathema.correction"]))
        for said in (p.meta or {}).get("mathema.let_warning") or ():
            line += f"\n           warning: {said}"
        stratum = getattr(p, "stratum", None)
        if stratum:
            # which stratum the falsification indicts, one line:
            # the verdict above is unchanged, this only classifies
            parts = []
            if stratum.get("mathematics"):
                parts.append(f"mathematics {stratum['mathematics']}")
            if stratum.get("cause"):
                parts.append(stratum["cause"])
            elif stratum.get("blame"):
                parts.append(f"blame {stratum['blame']}")
            if parts:
                line += f"\n           [{', '.join(parts)}]"
        lines.append(line)
    if not families:
        lines = _ranked_lines(self.probes, lines, starts)
    return "\n".join(lines)

save_spec(path)

Write the decoupled spec: intent, identity, claims, references, and the reasoning chain, as standalone YAML bound to the identity hashes.

Source code in mathema/__init__.py

def save_spec(self, path: str) -> str:
    """Write the decoupled spec: intent, identity, claims, references,
    and the reasoning chain, as standalone YAML bound to the identity
    hashes."""
    from .spec import save_spec
    return save_spec(self, path)

check(fn, claims=None, domain=None, trials=None, trials_downscale=None, extensive=False, declared=None, known_premises=None, pseudo_infinity=None, runtime_types=None, trials_scale=None)

Verify a function's claims, each adjudicated against the real function.

mathema.check(ema)                                    # + suggested claims
mathema.check(ema, claims=["f(x, 1.0) == x[-1]"])      # add a claim
mathema.check(ema, claims=[])                          # declared surfaces only
mathema.check(ema, domain={"alpha": (0, 1)})
mathema.check(ema, declared=mathema.retrieve(ema))     # + file claims

check is IO-free: it reads only what travels with the function object (decorator, docstring, type markers) and never touches the project's files. What mathema itself ships about libraries (the bundled compendium: numpy's sqrt has no value below zero, ...) applies to every call, as the engine's own knowledge; a project's own compendium files apply once compendium.install(root) ran: in a project with compendium files of its own, call mathema.compendium.install(root) first so check() reads the rows mathema verify reads; otherwise the record's meta["mathema.compendium_not_read"] says the files were not read. The file-declared layer, the highest-precedence authoring surface, therefore reaches it only through declared=, a retrieved entry from mathema.retrieve(fn, root). Call-site claims= still wins per claim name over everything retrieved. write_spec(), the CLI, and the MCP tools do this join for you; a bare check(fn) adjudicates the function-attached surfaces only.

claims omitted (None) defaults to suggest_claims(fn)'s own proposals, monotonicity/affine-ness/convexity, symmetry, idempotence, commutativity/associativity, raises(...) guards, each adjudicated at the best evidence level actually available (a proof when the function lifts, probing otherwise, see suggest_claims()'s own docstring). claims=[] (an explicit empty list, not merely omitted) means declared surfaces only: no suggested claims are added, while the built-in structural probes and the function's own decorator/docstring/type-marker claims still run, and so does a declared= entry when one is passed. Any other explicit claims=[...] is checked as given, unioned with whatever the function's own decorator or docstring declares.

domain declares parameter limits: algebraic probes sample inside the declared domain. Whether the code REJECTS out-of-domain input is its own declared claim, excluded_outside_domain(p), state it explicitly, opt in with the excluding keyword, or get it auto-declared by @enforce_domain (the decorator that makes it true). There is no adjudication mode: a declared exclusion that trials find unenforced is falsified with the accepted value as witness; an undeclared one reports nothing. See claim-driven-development's v0.2.0/claim-anatomy.md, "Domain: declared vs enforced".

known_premises is caller-supplied context for assuming <name> holds references that resolve nowhere in the batch: a mapping of claim name to a human line (usually from compendium.external_premises) that the missing-prerequisite note then includes. Data only; it never satisfies a premise, and check() itself stays IO-free. An entry {"cycle": True} marks a reference the caller found in a premise cycle across functions: a claim naming it is skipped as a premise cycle.

runtime_types ({param: "pandas.Series"}, else a declared entry's runtime_types:) names the runtime type of a parameter whose signature names none, for code that cannot be annotated.

pseudo_infinity is the function level of the operational infinity: how far each claim's computation (the probe route and the [float] companion) runs along an unbounded direction, unless the claim states its own let |inf| be. Omitted, a declared= entry's pseudo_infinity: field applies, else the project's MATHEMA_PSEUDO_INFINITY, else the number representation's maximum (sys.float_info.max for float64). A proof never reads it. Where the value that applied bounds a direction of a claim's domain, the claim's computation rows show it as let |inf| be <value> (the displayed claim, condition and the notes) and record its level in meta["mathema.pseudo_infinity"]; a value let |inf| be would refuse raises InvalidDomain.

extensive reaches every route this call touches: probe()'s own critical-point sampling hints and domain_safe[...] probe, and a route="derive" claim's case-split fallback. Default False everywhere; real, opt-in cost when set.

A parameter or return type hinted with a mathema type marker (Annotated[float, Probability], Annotated[list, Shape("m", "n")], see types.py) contributes its own claims automatically: a domain marker merges into domain (an explicitly passed bound for the same parameter wins), and a Shape marker adds a structural probe. Purely additive, a function with no markers behaves exactly as before.

Domains are per claim. The signature markers and domain= together are the function-level parent domain; each claim is adjudicated over that parent with its own for bindings overriding it per parameter, and one claim's bindings never reach another claim. A claim's record states its own bindings in domain/condition and whatever the parent supplied in meta["mathema.parent_domain"].

A @claims_decorator(...)-tagged function, or a docstring Claims: block (see authoring.py), also contributes its claims automatically, same as the type markers above; claims= passed here is unioned with those, winning per claim name on a collision (an explicit call- site claim is the most deliberate of the three; see authoring.declared_from_function's own decorator-over-docstring rule for the same reasoning one layer in).

Source code in mathema/__init__.py

@_quiet_while_probing
def check(fn, claims: list | None = None, domain: dict | None = None,
         trials: int | None = None,
         trials_downscale: float | None = None, extensive: bool = False,
         declared: dict | None = None,
         known_premises: dict | None = None,
         pseudo_infinity=None, runtime_types: dict | None = None,
         trials_scale: float | None = None) -> Record:
    """Verify a function's claims, each adjudicated against the real
    function.

        mathema.check(ema)                                    # + suggested claims
        mathema.check(ema, claims=["f(x, 1.0) == x[-1]"])      # add a claim
        mathema.check(ema, claims=[])                          # declared surfaces only
        mathema.check(ema, domain={"alpha": (0, 1)})
        mathema.check(ema, declared=mathema.retrieve(ema))     # + file claims

    check is IO-free: it reads only what travels with the function
    object (decorator, docstring, type markers) and never touches the
    project's files. What mathema itself ships about libraries (the
    bundled compendium: numpy's sqrt has no value below zero, ...)
    applies to every call, as the engine's own knowledge; a project's
    own compendium files apply once `compendium.install(root)` ran:
    in a project with compendium files of its own, call
    `mathema.compendium.install(root)` first so check() reads the rows
    `mathema verify` reads; otherwise the record's
    `meta["mathema.compendium_not_read"]` says the files were not read. The file-declared layer, the highest-precedence
    authoring surface, therefore reaches it only through `declared=`,
    a retrieved entry from `mathema.retrieve(fn, root)`. Call-site
    `claims=` still wins per claim name over everything retrieved.
    `write_spec()`, the CLI, and the MCP tools do this join for you;
    a bare `check(fn)` adjudicates the function-attached surfaces only.

    `claims` omitted (`None`) defaults to `suggest_claims(fn)`'s
    own proposals, monotonicity/affine-ness/convexity, symmetry,
    idempotence, commutativity/associativity, raises(...) guards, each
    adjudicated at the best evidence level actually available (a proof
    when the function lifts, probing otherwise, see suggest_claims()'s
    own docstring). `claims=[]` (an explicit empty list, not merely
    omitted) means declared surfaces only: no suggested claims are
    added, while the built-in structural probes and the function's own
    decorator/docstring/type-marker claims still run, and so does a
    `declared=` entry when one is passed. Any other explicit `claims=[...]` is
    checked as given, unioned with whatever the function's own decorator
    or docstring declares.

    `domain` declares parameter limits: algebraic probes sample inside
    the declared domain. Whether the code REJECTS out-of-domain input
    is its own declared claim, `excluded_outside_domain(p)`, state it
    explicitly, opt in with the `excluding` keyword, or get it
    auto-declared by @enforce_domain (the decorator that makes it
    true). There is no adjudication mode: a declared exclusion that
    trials find unenforced is falsified with the accepted value as
    witness; an undeclared one reports nothing. See
    claim-driven-development's v0.2.0/claim-anatomy.md, "Domain:
    declared vs enforced".

    `known_premises` is caller-supplied context for `assuming <name>
    holds` references that resolve nowhere in the batch: a mapping of
    claim name to a human line (usually from
    `compendium.external_premises`) that the missing-prerequisite note
    then includes. Data only; it never satisfies a premise, and
    check() itself stays IO-free. An entry `{"cycle": True}` marks a
    reference the caller found in a premise cycle across functions: a
    claim naming it is skipped as a premise cycle.

    `runtime_types` (`{param: "pandas.Series"}`, else a `declared`
    entry's `runtime_types:`) names the runtime type of a parameter
    whose signature names none, for code that cannot be annotated.

    `pseudo_infinity` is the function level of the operational
    infinity: how far each claim's computation (the probe route and
    the `[float]` companion) runs along an unbounded direction, unless
    the claim states its own `let |inf| be`. Omitted, a `declared=`
    entry's `pseudo_infinity:` field applies, else the project's
    `MATHEMA_PSEUDO_INFINITY`, else the number representation's maximum
    (`sys.float_info.max` for float64). A
    proof never reads it. Where the value that applied bounds a
    direction of a claim's domain, the claim's computation rows show it
    as `let |inf| be <value>` (the displayed claim, `condition` and the
    notes) and record its level in `meta["mathema.pseudo_infinity"]`; a
    value
    `let |inf| be` would refuse raises `InvalidDomain`.

    `extensive` reaches every route this call touches: `probe()`'s own
    critical-point sampling hints and `domain_safe[...]` probe, and a
    `route="derive"` claim's case-split fallback. Default `False`
    everywhere; real, opt-in cost when set.

    A parameter or return type hinted with a mathema type marker
    (`Annotated[float, Probability]`, `Annotated[list, Shape("m", "n")]`,
    see types.py) contributes its own claims automatically: a domain
    marker merges into `domain` (an explicitly passed bound for the same
    parameter wins), and a `Shape` marker adds a structural probe. Purely
    additive, a function with no markers behaves exactly as before.

    Domains are per claim. The signature markers and `domain=` together
    are the function-level parent domain; each claim is adjudicated over
    that parent with its own `for` bindings overriding it per parameter,
    and one claim's bindings never reach another claim. A claim's record
    states its own bindings in `domain`/`condition` and whatever the
    parent supplied in `meta["mathema.parent_domain"]`.

    A `@claims_decorator(...)`-tagged function, or a docstring `Claims:`
    block (see authoring.py), also contributes its claims automatically,
    same as the type markers above; `claims=` passed here is unioned
    with those, winning per claim name on a collision (an explicit call-
    site claim is the most deliberate of the three; see
    authoring.declared_from_function's own decorator-over-docstring rule
    for the same reasoning one layer in).
    """
    from .probing import resolve_trials_downscale
    trials_scale = resolve_trials_downscale(trials_downscale, trials_scale)
    from .compendium import ensure_bundled
    from .probing import _RISK, _SPECIALS
    from .spec import declare, entry_claims
    from .types import _TYPE_PROBE_TRIALS, domain_from_signature, type_probes

    ensure_bundled()
    facts = analyze(fn)
    if runtime_types is None and declared is not None:
        runtime_types = declared.get("runtime_types")
    if runtime_types:
        # a claims-file entry names the runtime types of code its
        # signature cannot state
        from .analysis import with_declared_runtime_types
        facts = with_declared_runtime_types(facts, fn, runtime_types)
    # the function-level parent domain: signature markers, then an
    # explicit domain= winning per parameter. Each claim is adjudicated
    # over this parent with its own `for` bindings overriding it per
    # parameter; one claim's bindings never reach another claim.
    parent_domain = {**domain_from_signature(fn), **(domain or {})}
    # the built-in battery only needs somewhere the function can be
    # called: a parameter the parent leaves open is synthesised inside
    # a region some claim declared for it, so the battery never reports
    # a raise outside every region the author stated
    battery_domain = {**_domains_from_claims(claims), **parent_domain}

    from .inventory import function_dependencies
    deps = function_dependencies(fn, facts)

    def _stamp_surface(ps, surface):
        # the authoring-surface provenance output rows fold into their
        # `source` field (records.row_source); claim-route probes carry
        # theirs from the conjecture instead
        for p in ps:
            meta = dict(p.meta or {})
            meta.setdefault("mathema.surface", surface)
            p.meta = meta
        return ps

    battery = probe(fn, facts, domain=battery_domain or None,
                    trials=trials, trials_scale=trials_scale, extensive=extensive)
    # a battery call mathema could not build is a check not run: it
    # leaves no row, and what it tried and why stays in the record meta
    not_run = [{"check": p.name, "statement": p.statement, "reason": p.note or "",
                "gap": (p.meta or {}).get("mathema.probe_gap")}
               for p in battery if p.name == "callable" and p.verdict == "skipped"]
    probes = _stamp_surface(
        [p for p in battery if not (p.name == "callable" and p.verdict == "skipped")],
        "builtin")

    type_trials = trials or _TYPE_PROBE_TRIALS
    scale = min(1.0, trials_scale)
    if scale < 1.0:
        type_trials = max(_RISK.min_trials_floor_when_scaled, len(_SPECIALS),
                          round(type_trials * scale))
    probes = probes + _stamp_surface(
        type_probes(fn, trials=type_trials, domain=battery_domain or None),
        "types")

    # whether this list is the caller's or mathema's own matters for
    # precedence below: a call-site claim is the MOST deliberate
    # surface, a suggestion the least
    suggested = claims is None
    if suggested:
        claims = suggest_claims(fn, facts=facts, extensive=extensive)
    claims = _expand_claim_keywords(claims, fn, facts, parent_domain,
                                    extensive)
    mats = _matrix_names_of(fn)
    built = [claim(c, matrix_names=mats) if isinstance(c, str) else c
             for c in claims]
    explicit = []
    for cj in built:
        entry = declare(cj)
        # declare()'s serialized form keeps only importable dotted
        # refs; the caller's actual callables ride beside it under an
        # in-memory-only key (never written to any store), re-attached
        # when the merged entry is rebuilt into claims
        live = {k: v for k, v in (getattr(cj, "funcs", None) or {}).items()
                if callable(v)}
        if live:
            entry["__live_funcs__"] = live
        entry["__written__"] = getattr(cj, "written", "") or getattr(cj, "raw", "")
        explicit.append(entry)
    # distinct claims that name alike (four domain variants of one law)
    # cannot share the name-keyed merge below
    explicit = _refuse_name_collisions(explicit)
    from .spec import merge_entries
    # a retrieved entry already carries the function surfaces merged
    # with the file store at the documented precedence; without one,
    # the function's own surfaces stand in (read off the object, so
    # check() stays IO-free)
    authored = (dict(declared) if declared is not None
                else {"claims": declared_from_function(fn)})
    if suggested:
        # a suggestion must never outrank a same-named authored claim.
        # It used to: the suggestion won the merge, so a human's
        # declared claim came back source "suggested", gates false,
        # and its verdict silently stopped counting toward the gate.
        merged_entry = merge_entries({"claims": explicit}, authored,
                                     on_conflict="silent")
    else:
        # a call-site claim overlays, winning per name: documented
        # precedence, the caller is expressing intent now
        merged_entry = merge_entries(authored, {"claims": explicit},
                                     on_conflict="silent")
    all_claims = entry_claims(merged_entry)
    if pseudo_infinity is None and declared is not None:
        pseudo_infinity = declared.get("pseudo_infinity")
    from . import policy as _policy
    with _policy.batch():
        adjudicated: list = []
        if all_claims:
            adjudicated = check_conjectures(fn, all_claims, domain=parent_domain or None,
                                            trials=trials, trials_downscale=trials_scale,
                                            facts=facts, extensive=extensive,
                                            known_premises=known_premises,
                                            float_companions=True,
                                            pseudo_infinity=pseudo_infinity)
            probes = probes + adjudicated
        # what f does with a value that is not there, for every parameter
        # that admits one and no stated policy row covers; a bare check
        # (no claim written, only suggestions) judges only the absence an
        # Optional annotation admits
        written = not suggested or bool(entry_claims(authored))
        covered = {(pol["kind"], pol.get("parameter"), pol.get("member"),
                    pol.get("premise") or "") for pol in
                   ((p.meta or {}).get("mathema.policy") for p in probes)
                   if pol and pol.get("source") == "stated"}
        # a record whose claims all report the mathematics line alone
        # (derive:math_only) carries no policy row: what the computation
        # does with a value that is not there is outside their remit
        from .gates import MATH_ONLY_ROUTE
        mathematics_only = bool(all_claims) and all(
            getattr(c, "route", None) == MATH_ONLY_ROUTE for c in all_claims)
        # a record whose value claims are all misspecified carries none
        # either: the domain they state has no points to draw from
        value_rows = [p for p in adjudicated
                      if not (p.meta or {}).get("mathema.policy")]
        misspecified_only = bool(value_rows) and all(
            p.verdict == "skipped:misspecified" for p in value_rows)
        if not mathematics_only and not misspecified_only:
            probes = probes + _policy.default_rows(
                fn, facts, parent_domain or {}, covered, _policy.row_name,
                optional_only=not written)
    if all_claims:
        # the split offer's own runs are not the record's claims: they
        # stay out of the calls the policy rows read
        _offer_splits(fn, facts, all_claims, probes,
                      [c for c in (claims or ()) if isinstance(c, str)])
    if not all_claims:
        # a bad function-level or project value refuses even with
        # nothing to adjudicate
        from .records import resolve_pseudo_infinity
        resolve_pseudo_infinity(None, pseudo_infinity)
    from .concepts import Concept, concepts_for, flat_union
    sources = concepts_for(facts, probes)
    dismissed = set(((declared or {}).get("meta") or {}).get(
        "mathema.concepts_dismissed") or [])
    if dismissed:
        # a curated dismissal silences the suggestion, permanently;
        # keyword hints are inferences and never re-offer a tag a
        # person has already said no to
        sources = {k: [c for c in v if c not in dismissed]
                   for k, v in sources.items()}
    # keyword hints are inferences, not assertions: they ride the
    # provenance split, clearly labeled, but never the interop union
    # or the record's own concepts field
    asserted = {k: v for k, v in sources.items()
                if k in ("declared", "mechanism") and v}
    concept_objs = [Concept(name, src)
                    for src, names in asserted.items() for name in names]
    meta: dict = {}
    if asserted or sources.get("keyword"):
        # the spec's own interop shape (a flat list under
        # meta.concepts) plus the un-flattened provenance beside it
        meta = {"mathema.concept_sources": {k: v for k, v in sources.items()
                                            if v}}
        if asserted:
            meta["concepts"] = flat_union(asserted)
    # the derive route's closed form, kept on the record so the math
    # section can state it (a proof's subject, rendered and exact).
    # Guarded: an unliftable body simply leaves the field None, which
    # every reader already treats as a valid value.
    try:
        lifted = lift_symbolic(fn, facts)
    except Exception:
        lifted = None
    from .authoring import _fn_key
    if not_run:
        meta = {**meta, "mathema.not_run": not_run}
    if facts.tree is not None:
        # what examining the source finds the function does beyond
        # returning a value, stated under the function
        from ._examine import effects_line
        effects = effects_line(fn)
        if effects is not None:
            meta = {**meta, "mathema.effects": effects}
    from .compendium import uninstalled_project_note
    try:
        not_read = uninstalled_project_note(fn)
    except Exception:
        not_read = None
    if not_read:
        meta = {**meta, "mathema.compendium_not_read": not_read}
    return Record(facts=facts, probes=probes, dependencies=deps,
                  concepts=concept_objs, meta=meta, lifted=lifted, key=_fn_key(fn))

analyze(fn)

Machine-derived facts about a function: parameters, purity, guards, structural shape. Pure ast, no probing, no claim verification.

Falls back to a documentation-only record (tier 0) for callables with no retrievable Python source (builtins, C extensions): the docstring states the intent, and probing still runs against the live callable.

Source code in mathema/__init__.py

def analyze(fn) -> Facts:
    """Machine-derived facts about a function: parameters, purity, guards,
    structural shape. Pure `ast`, no probing, no claim verification.

    Falls back to a documentation-only record (tier 0) for callables with no
    retrievable Python source (builtins, C extensions): the docstring states
    the intent, and probing still runs against the live callable."""
    injected = getattr(fn, "__mathema_facts__", None)
    if isinstance(injected, Facts):
        # a resolver-built proxy carries the facts its frontend could
        # honestly state (a namespaced form hash, real param kinds,
        # tree=None); they are richer than the doc-only fallback the
        # source-less path below would produce, so they win outright
        return effective_facts(fn)
    try:
        facts = effective_facts(fn)
    except SourceUnavailable:
        return _doc_only_facts(fn)
    facts.tier = 3 if not facts.is_pure else 2
    return facts

track_claims(fn)

Optional bare tag: track this function's claims over time.

Entirely optional. Without it, everything still works: check, write_spec, claims.check, and the CLI operate on any function. What an untracked function loses is visibility in mathema.status(), the fresh-versus-stale sweep, because status can only report on functions it knows exist. Tag the functions whose claims you want watched; leave the rest alone.

Mechanics, precisely: - runs once, at decoration time; the function object is returned unchanged (no wrapper, zero call overhead, stack traces untouched) - stamps fn.__mathema__ = {"key": ...} so tools and readers can see the tag by introspection - registers the function under its dotted key (module.qualname) in a weak registry, so mathema.tagged() and mathema.status() can find it; redefining the function in a notebook simply re-registers the key The tag carries no spec content: intent and claims live in the sidecar spec store (see mathema.spec), keeping code untouched by design.

Source code in mathema/__init__.py

def track_claims(fn):
    """Optional bare tag: track this function's claims over time.

    Entirely optional. Without it, everything still works: check, write_spec,
    claims.check, and the CLI operate on any function. What an untracked
    function loses is visibility in mathema.status(), the fresh-versus-stale
    sweep, because status can only report on functions it knows exist. Tag
    the functions whose claims you want watched; leave the rest alone.

    Mechanics, precisely:
      - runs once, at decoration time; the function object is returned
        unchanged (no wrapper, zero call overhead, stack traces untouched)
      - stamps ``fn.__mathema__ = {"key": ...}`` so tools and readers can see
        the tag by introspection
      - registers the function under its dotted key (module.qualname) in a
        weak registry, so `mathema.tagged()` and `mathema.status()` can find
        it; redefining the function in a notebook simply re-registers the key
    The tag carries no spec content: intent and claims live in the sidecar
    spec store (see `mathema.spec`), keeping code untouched by design.
    """
    import weakref

    from .authoring import _fn_key
    key = _fn_key(fn)
    fn.__mathema__ = {"key": key}
    _REGISTRY[key] = weakref.ref(fn)
    return fn

resolve(target, root='.', *, skipped=None)

Resolve a target spelling to its functions, keyed by canonical dotted name. See the module docstring for the accepted spellings. skipped, when given, collects (submodule, error) pairs for package submodules that failed to import (also carried on the returned Target).

Raises:

Type	Description
TargetError	nothing resolvable at this spelling; the message is printable as-is.

Source code in mathema/targets.py

def resolve(target: str, root: str = ".", *,
            skipped: list | None = None) -> Target:
    """Resolve a target spelling to its functions, keyed by canonical
    dotted name. See the module docstring for the accepted spellings.
    `skipped`, when given, collects `(submodule, error)` pairs for
    package submodules that failed to import (also carried on the
    returned Target).

    Raises:
        TargetError: nothing resolvable at this spelling; the message
            is printable as-is.
    """
    from .audit import DiscoveryError, discover

    skipped = skipped if skipped is not None else []
    mod_part, _, qual_part = target.partition(":")

    if ":" in target and not _is_pathlike(mod_part):
        # a tagged key (`<tag>:src/ema#ema`): a registered
        # resolver turns it into a Target of callable proxies; None
        # means "not mine" and resolution falls through to the
        # ordinary import path unchanged
        from ._target_resolvers import get_resolver
        resolver = get_resolver(mod_part)
        if resolver is not None:
            resolved = resolver(target, root)
            if resolved is not None:
                return resolved

    if _is_pathlike(mod_part):
        dotted, root = _dotted_name_for_file(mod_part)
        # a cached module under this dotted name that came from a
        # DIFFERENT file (two scratch scripts both named m.py, say)
        # would be returned instead of importing the requested one,
        # evict it, and its submodules, so the import is really this
        # file
        full = os.path.abspath(os.path.expanduser(mod_part))
        cached = sys.modules.get(dotted)
        if cached is not None and os.path.abspath(
                getattr(cached, "__file__", "") or "") != full:
            for name in [dotted] + [k for k in list(sys.modules)
                                    if k.startswith(dotted + ".")]:
                sys.modules.pop(name, None)
        _import_module(dotted, root)
        target = f"{dotted}:{qual_part}" if qual_part else dotted
        mod_part = dotted

    colon = ":" in target
    with _root_on_path(root):
        try:
            found = discover([target], skipped=skipped)
        except DiscoveryError as e:
            if not colon:
                walked = _prefix_walk(mod_part, root)
                if walked is not None:
                    return _walked_target(walked, target, root, skipped)
            if "#" in qual_part and "." not in mod_part:
                # the tagged-key shape with nothing registered to serve
                # it: name the remedy, not the bogus module import
                raise TargetError(
                    f"no target resolver is registered for "
                    f"{mod_part + ':'!r}; install the adaptor package "
                    f"providing it, or check the tag spelling "
                    f"(registered resolvers come from the "
                    f"{'mathema.target_resolvers'!r} entry-point "
                    f"group)") from e
            raise TargetError(str(e)) from e
        if colon and found:
            return Target("function", found, mod_part, root, skipped)
        if not colon:
            # a module or package resolves even with zero functions;
            # the caller decides whether an empty population is an error
            mod = sys.modules.get(target)
            kind = ("package" if mod is not None and hasattr(mod, "__path__")
                    else "module")
            return Target(kind, found, target if kind == "module" else None,
                          root, skipped)
        walked = _prefix_walk(f"{mod_part}.{qual_part}", root)
        if (walked is not None and callable(walked[2])
                and not inspect.isclass(walked[2])
                and not inspect.isfunction(walked[2])):
            # a callable discovery never lists (a C builtin, a ufunc,
            # a library's dispatcher object) found at the named
            # attribute: the same function the dotted spelling names
            return _walked_target(walked, target, root, skipped)
        if not _inside_root(mod_part, root):
            # a library installed outside the project: the name is read
            # as an attribute only, never searched for by importing
            # every submodule (some run a program when imported)
            if walked is not None:
                return _walked_target(walked, target, root, skipped)
            raise TargetError(_no_such_attribute(mod_part, qual_part))
        if "." not in qual_part:
            # bare-suffix search: `pkg:name` matches `name` anywhere
            # under the package when that suffix is unique
            wider = discover([mod_part], skipped=skipped)
            hits = {k: v for k, v in wider.items()
                    if k.rsplit(".", 1)[-1] == qual_part}
            if len(hits) == 1:
                return Target("function", hits, None, root, skipped)
            if len(hits) > 1:
                names = ", ".join(sorted(hits)[:10])
                raise TargetError(
                    f"{qual_part!r} is ambiguous under {mod_part!r}: {names}")
        what = qual_part or target
        hint = ""
        try:
            pool = discover([mod_part], skipped=list(skipped))
        except Exception:
            pool = {}
        if pool:
            import difflib
            leaf = what.rsplit(".", 1)[-1]
            close = set(difflib.get_close_matches(
                leaf, {k.rsplit(".", 1)[-1] for k in pool}, n=3, cutoff=0.6))
            matches = [k for k in sorted(pool)
                       if k.rsplit(".", 1)[-1] in close]
            if matches:
                hint = "; did you mean: " + ", ".join(matches[:3]) + "?"
        raise TargetError(
            f"no function named {what!r} found under {mod_part!r}{hint}")

resolve_function(target, root='.')

Resolve a target that must name exactly one function, returning (key, fn).

Raises:

Type	Description
TargetError	the target resolves to nothing, or to more than one function (the message lists candidates).

Source code in mathema/targets.py

def resolve_function(target: str, root: str = ".") -> tuple[str, Callable]:
    """Resolve a target that must name exactly one function, returning
    `(key, fn)`.

    Raises:
        TargetError: the target resolves to nothing, or to more than
            one function (the message lists candidates).
    """
    t = resolve(target, root)
    if len(t.functions) == 1:
        return next(iter(t.functions.items()))
    names = ", ".join(sorted(t.functions)[:10])
    more = "" if len(t.functions) <= 10 else f" (+{len(t.functions) - 10} more)"
    raise TargetError(
        f"{target!r} names {len(t.functions)} functions, not one: "
        f"{names}{more}. Narrow it with `module:function`.")

gate(claims, *, strict, accepted_risk=frozenset(), unresolved=(), key=None)

Apply the one gate policy to a set of adjudicated claims (live Probes or stored claim dicts, mixed freely).

Rules: a falsified or invalidated claim fails in every mode; an unknown claim fails unless its name is in accepted_risk (then it is owned, and only strict refuses it); strict additionally fails skipped claims; an unresolved global name fails in every mode. Suggestions mathema volunteered and foreign-grammar claims never gate (foreign ones are collected on the report for the caller to surface).

Source code in mathema/verify.py

def gate(claims, *, strict: bool,
         accepted_risk: frozenset = frozenset(),
         unresolved=(), key: "str | None" = None) -> GateReport:
    """Apply the one gate policy to a set of adjudicated claims (live
    Probes or stored claim dicts, mixed freely).

    Rules: a falsified or invalidated claim fails in every mode; an
    unknown claim fails unless its name is in `accepted_risk` (then it
    is `owned`, and only strict refuses it); strict additionally fails
    skipped claims; an unresolved global name fails in every mode.
    Suggestions mathema volunteered and foreign-grammar claims never
    gate (foreign ones are collected on the report for the caller to
    surface).
    """
    r = GateReport()
    gate_fails: list = []
    claims = list(claims)
    # a line under a claim mathema suggested is part of the suggestion
    suggested = {_claim_fields(c)[0] for c in claims
                 if _volunteered(_claim_fields(c)[2], _claim_fields(c)[3])}
    for c in claims:
        name, verdict, meta, note = _claim_fields(c)
        if "mathema.foreign_grammar" in meta:
            r.foreign.append(c)
            continue
        statement = _claim_statement(c)
        label = next((lab for rel, lab in _GATE_LABELS.items()
                      if statement.startswith(rel + "(")), None)
        parent = meta.get("mathema.companion_of")
        if parent is not None and parent in suggested:
            continue
        if label and classify_verdict(verdict) == "falsified":
            reason = ((meta.get("mathema.gate") or {}).get("reason")
                      or (c.get("counterexample") if isinstance(c, dict)
                          else getattr(c, "counterexample", None)) or "")
            under = f" under {parent}" if parent else ""
            line = (f"{label} ({statement}{under}) falsified: {reason}"
                    + (f"; mathema claims {key} prints the rows to state"
                       if key and label == "gate" else ""))
            if line not in gate_fails:
                gate_fails.append(line)
        pol = meta.get("mathema.policy")
        if pol and classify_verdict(verdict) == "falsified":
            clause = _policy_clause(name, _claim_statement(c), pol)
            if clause and _volunteered(meta, note) and not POLICY_ROWS_GATE:
                if clause not in r.unaccounted:
                    r.unaccounted.append(clause)
            elif clause:
                r.policy_problems.append(clause)
        if _volunteered(meta, note) and not (pol and POLICY_ROWS_GATE):
            continue
        kind = classify_verdict(verdict)
        if verdict == "skipped:unknown_but_accepted":
            # the stored form of an unknown a person accepted as risk
            r.owned += 1
            continue
        if kind == "proven":
            r.proven += 1
            if meta.get("mathema.surface") == "builtin":
                r.builtin_proven += 1
        elif kind == "holds":
            r.holds += 1
        elif kind == "falsified":
            r.falsified += 1
        elif kind == "invalidated":
            r.invalidated += 1
        elif kind == "unknown":
            if name in accepted_risk:
                r.owned += 1
            else:
                r.unknown += 1
                r.unknown_reasons.append((name, _first_sentence(note)))
        elif kind == "skipped":
            r.skipped += 1
            r.misspecified += verdict == "skipped:misspecified"
            word = ("misspecified" if verdict == "skipped:misspecified"
                    else "unknown")
            r.skipped_reasons.append((name, word, _first_sentence(note)))
    # a falsified or invalidated claim is a failing check, in every
    # mode; strictness only governs structurally-skipped claims, never
    # wrong or undecided ones
    if r.falsified:
        # a falsified gate names itself and its reason, and the policy
        # rows under it are the same fact; else the policy rows name
        # themselves and the one-word edit; any other falsified claim is
        # counted
        r.problems.extend(gate_fails)
        if r.policy_problems and not gate_fails:
            n = len(r.policy_problems)
            r.problems.append(f"{n} policy row{'s' if n != 1 else ''} to settle: "
                              + "\n".join(r.policy_problems)
                              + (f"\nto list them, run: mathema claims {key}" if key
                                 else ""))
        others = r.falsified - len(r.policy_problems) - len(gate_fails)
        if others > 0:
            r.problems.append(f"{others} falsified claim(s)")
    if r.invalidated:
        r.problems.append(f"{r.invalidated} invalidated claim(s)")
    if r.unknown:
        # an unaccepted unknown is an open epistemic gap: it fails in
        # every mode until it is resolved or a human owns the risk
        # (mathema accept --as risk)
        named = [f"{n} unknown: {why}" if why else f"{n} unknown"
                 for n, why in r.unknown_reasons]
        r.problems.append("; ".join(named) if named else
                          f"{r.unknown} unknown claim(s)")
    if strict and (r.skipped or r.owned):
        # accepted risk is visible relaxation, not laundering: lenient
        # proceeds past it, strict still refuses it
        if r.skipped:
            # a claim mathema could not run is unknown, with its reason,
            # and one misspecified as stated says so
            named = [f"{n} {word}: {why}" if why else f"{n} {word}"
                     for n, word, why in r.skipped_reasons]
            r.problems.append("; ".join(named) if named else
                              f"{r.skipped} unknown claim(s)")
        if r.owned:
            r.problems.append(f"{r.owned} accepted-risk claim(s)")
    if unresolved:
        r.problems.append(f"unresolved names: {', '.join(unresolved)}")
    return r

verify_project(root='.', *, all=False, strict=True, trials_downscale=None, only=None, files=None, trials_scale=None)

The test-runner sweep as a library call: for every key the declared/verified stores know, re-adjudicate if the function's form hash, claims fingerprint, or a dependency changed (all=True forces everything), rewrite the record, and gate each key's adjudicated claims through gate. only restricts the sweep to the given dotted keys (the single-key re-verify the reconcile workflow points at); None sweeps the whole population. files names claims files whose every entry is adjudicated up front, whether or not the project calls it (claims_file_entries); with files the sweep is restricted to their entries plus any only keys.

Notes

dependencies_current claims are settled AFTER the whole sweep has written its records, so a caller adjudicated before its callee in the same run still reads the callee's fresh record; the sweep's outcome does not depend on key order.

Source code in mathema/verify.py

def verify_project(root: str = ".", *, all: bool = False,
                   strict: bool = True,
                   trials_downscale: float | None = None,
                   only: "list | None" = None,
                   files: "list | None" = None,
                   trials_scale: float | None = None) -> VerifyResult:
    """The test-runner sweep as a library call: for every key the
    declared/verified stores know, re-adjudicate if the function's form
    hash, claims fingerprint, or a dependency changed (`all=True`
    forces everything), rewrite the record, and gate each key's
    adjudicated claims through `gate`. `only` restricts the sweep to the
    given dotted keys (the single-key re-verify the reconcile workflow
    points at); None sweeps the whole population. `files` names claims
    files whose every entry is adjudicated up front, whether or not the
    project calls it (`claims_file_entries`); with `files` the sweep is
    restricted to their entries plus any `only` keys.

    Notes:
        `dependencies_current` claims are settled AFTER the whole sweep
        has written its records, so a caller adjudicated before its
        callee in the same run still reads the callee's fresh record;
        the sweep's outcome does not depend on key order.
    """
    from .probing import resolve_trials_downscale
    trials_scale = resolve_trials_downscale(trials_downscale, trials_scale)
    import warnings

    from .analysis import StateDependenceWarning
    with warnings.catch_warnings():
        # analyze()'s state-outside warning is real, useful signal on a
        # single function, but a sweep would print it per stateful key
        # (twice: the freshness analyze and the battery's own) and
        # drown the report, whose rows and gate lines already carry the
        # same fact. Same reasoning, same fix, as audit's and
        # inventory's own analyze shields; only this category is
        # silenced, every other warning still surfaces.
        warnings.simplefilter("ignore", StateDependenceWarning)
        from ._run_scope import run_scope
        with run_scope():
            return _verify_sweep(root, all=all, strict=strict,
                                 trials_scale=trials_scale, only=only,
                                 files=files)

mathema.reason_codes

mathema.reason_codes

The public reason-code registry: a stable, versioned vocabulary for why a function didn't lift (ReasonCode/Category) and for why one claim's own adjudication was skipped (ClaimReasonCode), plus build_issue_record()/issue(), which build a real CDD spec record (spec.to_spec()) around whichever of those applies and attach the rest of the diagnostic depth under the record's own meta field.

This does not introduce a new vocabulary for either registry. inventory.derivability_report() already computes exactly ReasonCode's eight blocker values, symbolic.NotSymbolic already tags Category's finer-grained values, and conjecture.check_conjectures() already has its own closed set of skip sites, two of them already tagged in Probe.meta (mathema.foreign_grammar, mathema.derive_status), the rest identifiable from the exact note text it already writes. ClaimReasonCode names what's already there.

Once released, these names are public interface: never renamed, and never repointed at a different meaning. A new value is added as a new name; an existing one is never redefined underneath code that already depends on it.

ReasonCode

The eight values inventory.derivability_report()'s own blocker field can take, exactly as it already writes them, named here, not reinvented.

Source code in mathema/reason_codes.py

class ReasonCode:
    """The eight values `inventory.derivability_report()`'s own
    `blocker` field can take, exactly as it already writes them,
    named here, not reinvented."""
    STATEFUL = "stateful"
    LOOP = "loop"
    BRANCH = "branch"
    RECURSION = "recursion"
    NO_PARAMETERS = "no-parameters"
    NON_SCALAR_PARAMETERS = "non-scalar-parameters"
    INTERNAL_ERROR = "internal-error"
    UNSUPPORTED_CONSTRUCT = "unsupported-construct"

    ALL = (STATEFUL, LOOP, BRANCH, RECURSION, NO_PARAMETERS,
          NON_SCALAR_PARAMETERS, INTERNAL_ERROR, UNSUPPORTED_CONSTRUCT)

Category

symbolic.NotSymbolic.category's own vocabulary, only meaningful alongside ReasonCode.UNSUPPORTED_CONSTRUCT, naming which specific unsupported-syntax shape was hit. UNSUPPORTED_SYNTAX is NotSymbolic's own default when no more specific category is given; the rest are the specific categories currently raised anywhere in the derive-route lifting code.

Source code in mathema/reason_codes.py

class Category:
    """`symbolic.NotSymbolic.category`'s own vocabulary, only
    meaningful alongside `ReasonCode.UNSUPPORTED_CONSTRUCT`, naming
    which specific unsupported-syntax shape was hit. `UNSUPPORTED_SYNTAX`
    is `NotSymbolic`'s own default when no more specific category is
    given; the rest are the specific categories currently raised
    anywhere in the derive-route lifting code."""
    UNSUPPORTED_SYNTAX = "unsupported-syntax"
    UNSUPPORTED_CALL = "unsupported-call"
    UNSUPPORTED_ATTRIBUTE = "unsupported-attribute"
    UNBOUND_NAME = "unbound-name"
    TERNARY = "ternary"
    TUPLE_IN_EXPRESSION = "tuple-in-expression"
    INVALID_TUPLE_INDEX = "invalid-tuple-index"
    ARRAY_INDEX_MISMATCH = "array-index-mismatch"
    NON_NUMERIC_CONSTANT = "non-numeric-constant"

    ALL = (UNSUPPORTED_SYNTAX, UNSUPPORTED_CALL, UNSUPPORTED_ATTRIBUTE,
          UNBOUND_NAME, TERNARY, TUPLE_IN_EXPRESSION, INVALID_TUPLE_INDEX,
          ARRAY_INDEX_MISMATCH, NON_NUMERIC_CONSTANT)

ClaimReasonCode

Why one claim's own adjudication came back skipped (blocked, with reason) or stayed unknown (attempted, undecided), formalizes conjecture.check_conjectures()'s own existing skip sites, not a new taxonomy. Meaningful mainly alongside verdict skipped. An ordinary falsified claim's sketch/counterexample is the full story and carries no code; the one exception is a falsification whose stratum pins the failure on the implementation (meta["mathema.stratum"]), which carries its implementation: cause so tooling can separate a broken number representation from broken mathematics without parsing prose.

DERIVE_TIMEOUT is the one real code change behind this registry, not just a name: a derive-route wall-clock cutoff (symbolic._proof_support._prove_relation's own _with_timeout) used to come back indistinguishable from sympy simply failing to decide on its own; both were a bare undecided. It now carries meta["mathema.timeout"] ("fast" or "extensive", the tier that was in effect), propagated through to the claim's own Probe.meta alongside the existing mathema.derive_status.

NO_EVALUABLE_INPUTS is the one code here that's genuinely probe-route-specific (every synthesized trial raised before a comparison was ever made); everything else is checked before, or independent of, the route split.

Source code in mathema/reason_codes.py

class ClaimReasonCode:
    """Why one claim's own adjudication came back `skipped` (blocked,
    with reason) or stayed `unknown` (attempted, undecided),
    formalizes `conjecture.check_conjectures()`'s own existing skip
    sites, not a new taxonomy. Meaningful mainly alongside verdict
    `skipped`. An ordinary `falsified` claim's sketch/counterexample is
    the full story and carries no code; the one exception is a
    falsification whose stratum pins the failure on the implementation
    (`meta["mathema.stratum"]`), which carries its `implementation:`
    cause so tooling can separate a broken number representation from broken
    mathematics without parsing prose.

    `DERIVE_TIMEOUT` is the one real code change behind this registry,
    not just a name: a derive-route wall-clock cutoff
    (`symbolic._proof_support._prove_relation`'s own `_with_timeout`)
    used to come back indistinguishable from sympy simply failing to
    decide on its own; both were a bare `undecided`. It now carries
    `meta["mathema.timeout"]` (`"fast"` or `"extensive"`, the tier that
    was in effect), propagated through to the claim's own `Probe.meta`
    alongside the existing `mathema.derive_status`.

    `NO_EVALUABLE_INPUTS` is the one code here that's genuinely
    probe-route-specific (every synthesized trial raised before a
    comparison was ever made); everything else is checked before, or
    independent of, the route split."""
    FOREIGN_GRAMMAR = "foreign-grammar"
    UNSUPPORTED_MULTI_FUNCTION = "unsupported-multi-function"
    DERIVE_UNDECIDED = "derive-undecided"
    DERIVE_UNLIFTABLE = "derive-unliftable"
    DERIVE_TIMEOUT = "derive-timeout"
    UNKNOWN_ROUTE = "unknown-route"
    UNKNOWN_RELATION = "unknown-relation"
    UNKNOWN_EXCEPTION_TYPE = "unknown-exception-type"
    INVALID_CONJECTURE = "invalid-conjecture"
    NO_EVALUABLE_INPUTS = "no-evaluable-inputs"
    # a HOLDS verdict that rests on the empirical fallback because the
    # derive route could not settle the claim: the record is evidence,
    # not proof, and a caller measuring derive-route coverage needs the
    # gap machine-readable (previously only skipped/unknown verdicts
    # ever carried a code, so holds-rescued gaps, the bulk of a
    # corpus's open-proof population, were invisible to tooling)
    DERIVE_GAP_EMPIRICAL = "derive-gap-empirical"
    # a conditional claim (`assuming X holds, ...`) whose premise could
    # not be discharged. The claim itself was never attempted; there
    # is nothing wrong with it, only with what it rests on, so these
    # sit alongside the undecided codes rather than the blocked ones.
    MISSING_PREREQUISITE = "missing-prerequisite"
    UNMET_PREREQUISITE = "unmet-prerequisite"
    AMBIGUOUS_PREREQUISITE = "ambiguous-reference"
    DEPENDENCY_CYCLE = "dependency-cycle"

    ALL = (FOREIGN_GRAMMAR, UNSUPPORTED_MULTI_FUNCTION, DERIVE_UNDECIDED,
          DERIVE_UNLIFTABLE, DERIVE_TIMEOUT, UNKNOWN_ROUTE, UNKNOWN_RELATION,
          UNKNOWN_EXCEPTION_TYPE, INVALID_CONJECTURE, NO_EVALUABLE_INPUTS,
          DERIVE_GAP_EMPIRICAL, MISSING_PREREQUISITE, UNMET_PREREQUISITE,
          AMBIGUOUS_PREREQUISITE, DEPENDENCY_CYCLE)

LoopReason

The fold recognizer's own decline slugs (symbolic.diagnose_fold and _lift_fold_impl's reason field), exactly as they are already written, named here, not reinvented. Rendered composed as loop:<value> by blocked_code(). A loop decline can also carry a Category value when one of the loop's own pieces hit an unsupported construct.

Source code in mathema/reason_codes.py

class LoopReason:
    """The fold recognizer's own decline slugs (`symbolic.diagnose_fold`
    and `_lift_fold_impl`'s `reason` field), exactly as they are
    already written, named here, not reinvented. Rendered composed as
    `loop:<value>` by `blocked_code()`. A loop decline can also carry a
    `Category` value when one of the loop's own pieces hit an
    unsupported construct."""
    NO_LOOP = "no-loop"
    MULTIPLE_LOOPS = "multiple-loops"
    NOT_A_FOLD = "not-a-fold"
    GUARDED_FOLD = "guarded-fold"
    BRANCH_ELSEWHERE = "branch-elsewhere"
    RECURSION = "recursion"
    WRONG_SEQUENCE_PARAM_COUNT = "wrong-sequence-param-count"
    EXTRA_STATEMENTS = "extra-statements"
    NON_SIMPLE_INIT = "non-simple-init"
    NON_SIMPLE_LOOP_HEADER = "non-simple-loop-header"
    FIRST_ELEMENT_INIT_WRONG_ITERATION = "first-element-init-wrong-iteration"
    PARTIAL_SEQ_INIT = "partial-seq-init"
    EXTERNAL_INIT_WRONG_ITERATION = "external-init-wrong-iteration"
    UNRECOGNIZED_LOOP_HEADER = "unrecognized-loop-header"
    MULTI_STATEMENT_LOOP_BODY = "multi-statement-loop-body"
    NON_SIMPLE_UPDATE = "non-simple-update"
    NO_RETURN_VALUE = "no-return-value"
    NON_AFFINE_UPDATE = "non-affine-update"
    ADDITIVE_CONSTANT_UPDATE = "additive-constant-update"
    TUPLE_IN_EXPRESSION = "tuple-in-expression"
    UNCLASSIFIED = "unclassified"

    ALL = (NO_LOOP, MULTIPLE_LOOPS, NOT_A_FOLD, GUARDED_FOLD,
          BRANCH_ELSEWHERE, RECURSION, WRONG_SEQUENCE_PARAM_COUNT,
          EXTRA_STATEMENTS, NON_SIMPLE_INIT, NON_SIMPLE_LOOP_HEADER,
          FIRST_ELEMENT_INIT_WRONG_ITERATION, PARTIAL_SEQ_INIT,
          EXTERNAL_INIT_WRONG_ITERATION, UNRECOGNIZED_LOOP_HEADER,
          MULTI_STATEMENT_LOOP_BODY, NON_SIMPLE_UPDATE, NO_RETURN_VALUE,
          NON_AFFINE_UPDATE, ADDITIVE_CONSTANT_UPDATE, TUPLE_IN_EXPRESSION,
          UNCLASSIFIED)

BranchReason

Why one branch condition can or cannot be pruned (symbolic._explain_branch's code field). NEEDS_DOMAIN is the resolvable kind, pruning settles the branch once a claim declares a specific-enough domain for the named parameters; the rest are the structurally blocked kinds. Rendered composed as branch:<value> (branch:needs-domain(scale) names the parameters) by blocked_code().

Source code in mathema/reason_codes.py

class BranchReason:
    """Why one branch condition can or cannot be pruned
    (`symbolic._explain_branch`'s `code` field). `NEEDS_DOMAIN` is the
    resolvable kind, pruning settles the branch once a claim declares
    a specific-enough domain for the named parameters; the rest are the
    structurally blocked kinds. Rendered composed as `branch:<value>`
    (`branch:needs-domain(scale)` names the parameters) by
    `blocked_code()`."""
    NEEDS_DOMAIN = "needs-domain"
    BARE_LOCAL_NAME = "bare-local-name"
    TWO_NAMES_COMPARE = "two-names-compare"
    NON_LITERAL_COMPARE = "non-literal-compare"
    UNTRACEABLE_LOCAL = "untraceable-local"
    OPAQUE_EXPRESSION = "opaque-expression"
    NO_PARAMETER_DEPENDENCE = "no-parameter-dependence"
    NON_AFFINE_ESSENTIAL = "non-affine-essential"
    NON_AFFINE_REFINABLE = "non-affine-refinable"
    UNRECOGNIZED_SHAPE = "unrecognized-shape"
    COMPOSITE = "composite"

    ALL = (NEEDS_DOMAIN, BARE_LOCAL_NAME, TWO_NAMES_COMPARE,
          NON_LITERAL_COMPARE, UNTRACEABLE_LOCAL, OPAQUE_EXPRESSION,
          NO_PARAMETER_DEPENDENCE, NON_AFFINE_ESSENTIAL,
          NON_AFFINE_REFINABLE, UNRECOGNIZED_SHAPE, COMPOSITE)

blocked_code(report)

The compact underivability code for one inventory.derivability_report() dict: stateful, recursion, no-parameters, non-scalar-parameters, internal-error, loop:<LoopReason>, branch:<BranchReason> (with (param, ...) naming the domains to declare for the resolvable kind, and a +N suffix when several distinct blocked kinds occur), or unsupported:<Category>. None for a derivable function or a missing report. The lookup for every code is describe_code().

Source code in mathema/reason_codes.py

def blocked_code(report: dict | None) -> str | None:
    """The compact underivability code for one
    `inventory.derivability_report()` dict: `stateful`, `recursion`,
    `no-parameters`, `non-scalar-parameters`, `internal-error`,
    `loop:<LoopReason>`, `branch:<BranchReason>` (with
    `(param, ...)` naming the domains to declare for the resolvable
    kind, and a `+N` suffix when several distinct blocked kinds occur),
    or `unsupported:<Category>`. `None` for a derivable function or a
    missing report. The lookup for every code is `describe_code()`."""
    if not report or report.get("liftable"):
        return None
    blocker = report.get("blocker")
    if blocker == "loop":
        return f"loop:{report.get('reason') or LoopReason.UNCLASSIFIED}"
    if blocker == "branch":
        branches = report.get("branches") or []
        blocked = [b for b in branches if b.get("kind") == "blocked"]
        if not blocked:
            needs = sorted({p for b in branches
                            for p in b.get("needs_domain_for") or []})
            suffix = f"({', '.join(needs)})" if needs else ""
            return f"branch:{BranchReason.NEEDS_DOMAIN}{suffix}"
        codes: list[str] = []
        for b in blocked:
            c = b.get("code") or BranchReason.UNRECOGNIZED_SHAPE
            if c not in codes:
                codes.append(c)
        extra = f"+{len(codes) - 1}" if len(codes) > 1 else ""
        return f"branch:{codes[0]}{extra}"
    if blocker == "unsupported-construct":
        return (f"unsupported:"
                f"{report.get('category') or Category.UNSUPPORTED_SYNTAX}")
    return blocker

describe_code(code)

The CODE_TABLE entry for one compact code, tolerant of the composed decorations blocked_code() adds: a parameter list (branch:needs-domain(scale)) and a +N multiplicity suffix are stripped before lookup. A loop:<Category> code (a loop whose own pieces hit an unsupported construct) falls back to the matching unsupported:<Category> entry. None for an unknown code.

Source code in mathema/reason_codes.py

def describe_code(code: str) -> dict | None:
    """The `CODE_TABLE` entry for one compact code, tolerant of the
    composed decorations `blocked_code()` adds: a parameter list
    (`branch:needs-domain(scale)`) and a `+N` multiplicity suffix are
    stripped before lookup. A `loop:<Category>` code (a loop whose own
    pieces hit an unsupported construct) falls back to the matching
    `unsupported:<Category>` entry. `None` for an unknown code."""
    base = code.split("(", 1)[0]
    if "+" in base:
        base = base.split("+", 1)[0]
    entry = CODE_TABLE.get(base)
    if entry is not None:
        return {"id": CODE_IDS.get(base), **entry}
    if base.startswith("loop:"):
        fallback = CODE_TABLE.get("unsupported:" + base[len("loop:"):])
        if fallback is not None:
            return {"id": CODE_IDS.get("unsupported:" + base[len("loop:"):]),
                    **fallback}
    return None

claim_reason_code(probe)

ClaimReasonCode for a skipped or unknown Probe, read off whatever check_conjectures() already recorded for it, meta tags where they exist, the note text otherwise (not every skip site is meta-tagged today). None for any other verdict, or a skip this function doesn't recognize.

Source code in mathema/reason_codes.py

def claim_reason_code(probe) -> str | None:
    """`ClaimReasonCode` for a skipped or unknown `Probe`, read off whatever
    `check_conjectures()` already recorded for it, `meta` tags where
    they exist, the note text otherwise (not every skip site is
    meta-tagged today). `None` for any other verdict, or a skip this
    function doesn't recognize."""
    verdict_class = classify_verdict(probe.verdict)
    meta = probe.meta or {}
    if verdict_class == "holds" and meta.get("mathema.derive_status") in (
            "undecided", "unliftable"):
        # empirical evidence rescued a derive gap: real, but not proof;
        # the one non-skip verdict that carries a code, so coverage
        # tooling can count open proof gaps without parsing notes
        return ClaimReasonCode.DERIVE_GAP_EMPIRICAL
    if verdict_class == "falsified":
        # a falsification is not an ambiguous gap and normally carries
        # no code; a stratum that pins the failure on the
        # implementation is the exception, and its cause is the code
        stratum = meta.get("mathema.stratum") or {}
        cause = stratum.get("cause")
        if cause in CODE_TABLE:
            return cause
        return None
    if verdict_class not in ("skipped", "unknown"):
        return None
    premise = meta.get("mathema.premise")
    if premise in (ClaimReasonCode.MISSING_PREREQUISITE,
                   ClaimReasonCode.UNMET_PREREQUISITE,
                   ClaimReasonCode.AMBIGUOUS_PREREQUISITE,
                   ClaimReasonCode.DEPENDENCY_CYCLE):
        # the premise, not the claim, is what could not be settled
        return premise
    if "mathema.foreign_grammar" in meta:
        return ClaimReasonCode.FOREIGN_GRAMMAR
    if meta.get("mathema.probe_gap"):
        # the probe route could not evaluate the function at all,
        # input synthesis failed, or a parameter (a string, say) has no
        # domain to sample from
        return ClaimReasonCode.NO_EVALUABLE_INPUTS
    if meta.get("mathema.timeout"):
        return ClaimReasonCode.DERIVE_TIMEOUT
    if meta.get("mathema.derive_status") == "undecided":
        return ClaimReasonCode.DERIVE_UNDECIDED
    if meta.get("mathema.derive_status") == "unliftable":
        return ClaimReasonCode.DERIVE_UNLIFTABLE
    note = probe.note or ""
    # the current wording, and the one older records carry
    if ("cannot yet read a raises claim over several functions" in note
            or "does not yet lift multi-function" in note):
        return ClaimReasonCode.UNSUPPORTED_MULTI_FUNCTION
    if "unknown route" in note:
        return ClaimReasonCode.UNKNOWN_ROUTE
    if "unknown relation" in note:
        return ClaimReasonCode.UNKNOWN_RELATION
    if "unknown exception type" in note:
        return ClaimReasonCode.UNKNOWN_EXCEPTION_TYPE
    if "no evaluable inputs" in note:
        return ClaimReasonCode.NO_EVALUABLE_INPUTS
    if meta.get("mathema.invalid_conjecture"):
        # the statement never parsed/validated far enough to be
        # adjudicated at all, stamped in meta at the catch site, so
        # this never guesses from note prose (a record predating the
        # stamp simply reports no code here)
        return ClaimReasonCode.INVALID_CONJECTURE
    return None

mathema.conjecture

mathema.conjecture

The conjecture pipeline: externally proposed claims, machine-adjudicated.

A conjecture is a claim stated by someone other than the analyzer: a human in a review, or a model acting as a hypothesis generator. It enters as conjectured, and the verifier decides what it becomes: holds (n=…) with seeded probing, or falsified with the counterexample kept. The proposer never adjudicates its own claims.

Laws are written over the function name f and its parameter names, with any extra free names treated as auxiliary real variables (sampled alongside the inputs):

Conjecture("odd", lhs="f(-x)", rhs="-f(x)", relation="==")
Conjecture("bounded", lhs="min(x)", rhs="f(x, alpha)", relation="<=")
Conjecture("shift", lhs="f(x + c)", rhs="f(x) + c", relation="==")

Expressions are validated against an AST whitelist before evaluation: arithmetic, the comparisons the relation handles, the grammar's own functions, and calls to the functions the claim names. A dotted name in a claim (let g = numpy.mean) resolves to that function, which runs in the same way as importing it and calling it directly would, except that a name reaching a refused module (os, subprocess, builtins and the others _claim_reach lists) is refused. A binding into third-party code whose effects mathema cannot establish runs and carries a warning naming it.

Conjecture dataclass

One parsed claim, ready to be adjudicated: a relation between lhs and rhs over the function under test (f), the evidence route it's checked on, and everything a proof/probe attempt needs (declared domain, tolerance, prior counterexamples to replay, extra functions a multi-function law refers to). Built by claim(), which parses a claim's law text into these fields.

Source code in mathema/conjecture.py

@dataclass
class Conjecture:
    """One parsed claim, ready to be adjudicated: a relation between
    `lhs` and `rhs` over the function under test (`f`), the evidence
    route it's checked on, and everything a proof/probe attempt needs
    (declared domain, tolerance, prior counterexamples to replay, extra
    functions a multi-function law refers to). Built by `claim()`, which
    parses a claim's law text into these fields."""
    name: str
    lhs: str
    rhs: str
    relation: str = "=="        # "==" | "<=" | ">=" | ... | "in" | "not in"
    rhs_bound: object = None    # the domain a membership relation's rhs names, else None
    source: str = "user"
    route: str = "best"         # "best" (default cascade) | "probe" | "derive" | "examine" (see claim-driven-
                                 # development/0.1.0/claim-anatomy.md). "best" is
                                 # input-only: the cascade derive -> derive:extensive
                                 # -> probe, with the output record naming whichever
                                 # mechanism actually settled it ("auto" is retired,
                                 # an unknown route now, skipped loudly).
                                 # "derive:math_only" adjudicates as "derive" and
                                 # spawns no `[float]` companion.
    grammar: str = GRAMMAR      # statement dialect (record-schema.md's `grammar` field).
                                 # this module implements exactly one: the
                                 # `f`-and-parameter-names law language it and
                                 # symbolic.py parse. A claim declared under a
                                 # different one (mathema.data's, say) is
                                 # recognized and excluded by check_conjectures,
                                 # not misadjudicated as this one.
    funcs: dict = field(default_factory=dict)
    # extra function letters the law may apply, mapped to their callables:
    # {"g": other_fn} lets a law relate two implementations, f(x) == g(x).
    # `f` is always implicitly bound to the function under adjudication.
    # In a record this map is carried as meta["mathema.funcs"] (spec keys,
    # not callables), since the declared-claim field set is fixed.
    domain: dict = field(default_factory=dict)
    # per-parameter bounds this claim is asserted over (declared-schema.md's
    # `domain` field), usually lifted from an inline quantifier by claim().
    free_vars: frozenset = field(default_factory=frozenset)
    # domain keys with no real parameter to match; a claim-text `let
    # name in bounds` binding (grammar.extract_let_bindings), e.g. a
    # gauge-invariance claim's arbitrary shift constant. check_conjectures()
    # exempts these from its real-parameter-only domain-key check, but a
    # free variable's own declared bound is otherwise inert on the derive
    # route: only real parameters reach _domain_assumptions/the corner-
    # evaluation sign machinery, so this only helps a claim whose truth
    # doesn't depend on the free variable's exact range (unlike `let`'s
    # alias form, which substitutes an existing real parameter's own
    # already-bounded symbol and so has no such gap).
    # Empty means asserted without restriction.
    ambiguous_diff_vars: frozenset = field(default_factory=frozenset)
    # literal denominator names (grammar.extract_diff_fraction_sugar's
    # `d(<expr>/d<var>)` fraction sugar guessed at differentiation,
    # `dh`, not the stripped `h`. check_conjectures() checks these
    # against fn's own real parameter names once known: a real
    # collision (the literal name IS a parameter, e.g. a
    # gibbs_free_energy(dh, t, ds)-shaped function) means the guess was
    # never safe to make, and the claim is skipped:misspecified rather
    # than silently guessing wrong. Empty means the claim's `d(...)`
    # calls (if any) never used the fraction spelling at all.
    pins: list = field(default_factory=list)
    param_pins: dict = field(default_factory=dict)
    # `let <parameter> be None|True|False` bindings (grammar.
    # ParameterPin): the value each named parameter is passed at on
    # every call the claim makes. A number spelled the same way is a
    # single-point `let` bound in `domain`/`free_vars`, which reads as a
    # pin too when the name is a real parameter of a library function.
    meta: dict = field(default_factory=dict)   # declared extension data
                                 # (the spec's own meta object, e.g.
                                 # {"concepts": [...]}), carried onto
                                 # the claim's probe unchanged, per the
                                 # spec's pass-through rule
    # counterexamples already on record, replayed before any sampling so a
    # past falsification stays caught forever (cdd.md step 6: re-verification
    # is also a regression check). Each pin: {"args": [...], "aux": {...}}
    # with exact values, not display strings.
    tolerance: float | ToleranceKind | None = None
    # how close counts as equal (declared-schema.md's `tolerance` field;
    # an equivalence's or a single `~=`'s may name its kind,
    # `_tolerance.ToleranceKind`;
    # no spec-level default). Also what `ε`/`eps`/`epsilon` resolves to
    # inside a law's own text (grammar.py/symbolic.py), so
    # `abs(f(x) - g(x)) <= ε` reads exactly like the mathematical
    # convention it's borrowed from.
    negated: bool = False
    # a domain-safety predicate claim stated in its grammar not-form
    # (`not is_pole_safe(x)`): the relation stays the positive
    # predicate every dispatch site matches on, and adjudication
    # inverts the family's decision, the evidence that falsifies the
    # positive claim is exactly what proves the negation.
    assuming: str = ""
    # raw text of a claim's own `assuming <...>,` prefix (grammar.
    # extract_assuming_clause), keyword included; empty string means
    # the claim had no such section. Held verbatim here and interpreted
    # at adjudication time by `_interpret_assumption`, which needs the
    # sibling claims and the function's facts: a relation (or `and`-
    # joined conjunction) constrains the region both routes work over,
    # `is_defined(f)`/`f is defined` resolves to the function's own
    # definedness region and is pinned into the statement, a bare
    # sibling name borrows that claim's relation, and `<name> holds` /
    # `<name> is proven` consults the referenced claim's verdict and
    # caps this claim's own.
    outcome: str = ""
    # raw text of a claim's own trailing `=> <...>` suffix (grammar.
    # extract_outcome_clause), captured verbatim. Unlike `assuming`,
    # nothing reads this yet, the parser round-trips it and no
    # adjudication consults it. Empty string means no such section.
    pseudo_infinity: float | None = None
    # the authored `let |inf| be v`, the claim level of the operational
    # infinity (P6): how far the computation (the probe route and the
    # float companion) runs along an unbounded direction, applied
    # symmetrically (records.pseudo_infinity_range). The derive route
    # never reads it (P1). Part of the claim's text, and so of its
    # identity, only where it bounds an unbounded direction (P8).
    resolved_pseudo_infinity: "PseudoInfinity | None" = field(
        default=None, compare=False)
    # the operational infinity that applies after resolution, claim >
    # function > MATHEMA_PSEUDO_INFINITY (records.resolve_pseudo_infinity),
    # with its source; set only on check_conjectures' working copy and
    # read through records.operational_range. Output, never identity
    # (P7): no renderer or fingerprint reads it.
    overflow_safe: tuple = field(default=(), compare=False)
    # the `(lhs, relation, rhs)` links of the function's own recorded
    # `is_overflow_safe` region, from the claims adjudicated beside
    # this one; set only on check_conjectures' working copy, read by
    # the `is_defined` probe to keep its points inside that region
    links: list = field(default_factory=list)
    # a chained comparison's pairwise links, each an (lhs, rel, rhs)
    # triple (grammar.split_relation_chain); empty for an ordinary
    # single-relation claim. When present, the claim is the CONJUNCTION
    # of its links; proven iff every link is, falsified if any link
    # is, and lhs/rel/rhs hold the first link so every single-link
    # consumer keeps working unchanged.
    written: str = ""
    # the claim as its author wrote it, domain included, where `raw` holds
    # only the law a stored row keeps beside its domain
    raw: str = ""
    # the claim's original law text, before parsing (provenance, and the
    # source `check_conjectures` re-resolves the matrix sugar from when
    # the function's signature reveals a matrix the claim text alone did
    # not). Empty for a Conjecture built directly rather than via claim().
    scope_bound: frozenset = field(default_factory=frozenset)
    # the call names that are the function under test itself
    # (`midpoint(a, b)` for f = midpoint): no `let` renders for them
    under_test: frozenset = field(default_factory=frozenset)
    # the `funcs` names check_conjectures resolved from f's module or the
    # calling scope rather than from an explicit `funcs=`/`let` binding.
    # Their text stays the bare call name, which resolves the same way
    # when the claim is rebuilt, so rendering adds no `let` for them.
    trials: "int | None" = None

claim(law, name=None, source='user', route='best', grammar=GRAMMAR, funcs=None, tolerance=None, pseudo_infinity=None, meta=None, matrix_names=frozenset(), trials=None)

The simple way to state a claim: one string, relation included.

claim("f(-x) = -f(x)")
claim("f(x)^2 ≥ 0")
claim("min(x) <= f(x, alpha)", name="lower_bound")
claim("f(x) == g(x) / log(2)", funcs={"g": nats_version})
claim("raises(f(x), ValueError)")
claim("let m = m1, for m1 in [0.1,1000], x1 in [-100,100], x2 in [-100,100],"
      " f(m,x1,m,x2) == (x1+x2)/2")
claim("let g = pkg.mod.func1, for x in (0,100], g(x) >= 0")
claim("let c be [-1e6,1e6], for dh in [-1e6,1e6], t in [0,1000], ds in [-1e6,1e6],"
      " d(f(dh+c,t,ds), t) == d(f(dh,t,ds), t)")

Spellings are normalized by grammar.py (^ is power, = reads as ==, Unicode ≤ ≥ − · × π accepted), so equivalent spellings are the same statement. Accepted relations: ==, <=, >=, plus the raises(...) predicate and the family-derive-only is_pole_safe(param)/is_number_set_safe(param) predicates (no f(...) wrapper; these are facts about param's own declared domain, not fn's return value). route defaults to "best", which cascades: the fast proof attempt, then the extensive strategy ladder, then probing, and the output record names whichever route actually settled it. "derive" makes the fast proof attempt only; a claim it cannot decide still falls through to probing, with the derive attempt's status kept in meta["mathema.derive_status"]. "probe" samples only (seeded, verdict holds/falsified) ("auto" is retired, not a legacy spelling of "best"). A derive proof is the mathematics in exact arithmetic; mathema.check pairs it with a <name>[float] companion claim about the computation, and "derive:math_only" reports the mathematics line only: the computation and its policy rows are outside its remit. the safety predicates always adjudicate on the examine route regardless of the route passed in. A leading let name = expr, ... (see grammar.extract_let_bindings) substitutes each name for (expr) everywhere later in the law, e.g. binding one fresh name to two real parameters, forcing them equal, or, when expr is a bare dotted path, binds a callable letter (like g above) the same way an explicit funcs= entry would, without needing one; let name be bounds instead declares a genuinely free variable (no real parameter to alias, e.g. a gauge- invariance claim's arbitrary shift constant), be, not in, so it never reads like a for binding, exempted from the usual real-parameter-only domain-key check. If name also turns out to be a real parameter of whichever function is checked, with no separate for name in ... of its own in this same claim, that's harmless (there's still only one declared bound) and adjudicates like an ordinary for, noted in the result rather than treated as an error; declaring the same name via both let ... be ... and for ... in ... in one claim, though, raises ConflictingDomainBinding immediately; two different bounds for one name has no principled default to pick silently. trials is the claim's own trial budget, a positive whole number, which may exceed the usual limit.

Inside a run scope (_run_scope.run_scope) a claim stated again with the same text and arguments is parsed once for the run; each call gets its own copy of the parse.

Source code in mathema/conjecture.py

def claim(law: str, name: str | None = None, source: str = "user",
         route: str = "best", grammar: str = GRAMMAR,
         funcs: dict | None = None, tolerance: float | None = None,
         pseudo_infinity: float | None = None,
         meta: dict | None = None,
         matrix_names: frozenset = frozenset(),
         trials: "int | None" = None) -> Conjecture:
    """The simple way to state a claim: one string, relation included.

        claim("f(-x) = -f(x)")
        claim("f(x)^2 ≥ 0")
        claim("min(x) <= f(x, alpha)", name="lower_bound")
        claim("f(x) == g(x) / log(2)", funcs={"g": nats_version})
        claim("raises(f(x), ValueError)")
        claim("let m = m1, for m1 in [0.1,1000], x1 in [-100,100], x2 in [-100,100],"
              " f(m,x1,m,x2) == (x1+x2)/2")
        claim("let g = pkg.mod.func1, for x in (0,100], g(x) >= 0")
        claim("let c be [-1e6,1e6], for dh in [-1e6,1e6], t in [0,1000], ds in [-1e6,1e6],"
              " d(f(dh+c,t,ds), t) == d(f(dh,t,ds), t)")

    Spellings are normalized by grammar.py (^ is power, = reads as ==,
    Unicode ≤ ≥ − · × π accepted), so equivalent spellings are the same
    statement. Accepted relations: ==, <=, >=, plus the raises(...)
    predicate and the family-derive-only `is_pole_safe(param)`/`is_number_set_safe(param)`
    predicates (no `f(...)` wrapper; these are facts about param's own
    declared domain, not fn's return value). `route` defaults to "best",
    which cascades: the fast proof attempt, then the extensive strategy
    ladder, then probing, and the output record names whichever route
    actually settled it. "derive" makes the fast proof attempt only; a
    claim it cannot decide still falls through to probing, with the
    derive attempt's status kept in `meta["mathema.derive_status"]`.
    "probe" samples only (seeded, verdict `holds`/`falsified`) ("auto" is retired, not a
    legacy spelling of "best"). A derive proof is the mathematics in
    exact arithmetic; `mathema.check` pairs it with a `<name>[float]`
    companion claim about the computation, and "derive:math_only"
    reports the mathematics line only: the computation and its policy
    rows are outside its remit. the safety predicates always adjudicate on the examine route
    regardless of the route passed in. A
    leading `let name = expr, ...` (see grammar.extract_let_bindings)
    substitutes each name for `(expr)` everywhere later in the law,
    e.g. binding one fresh name to two real parameters, forcing them
    equal, or, when `expr` is a bare dotted path, binds a callable
    letter (like `g` above) the same way an explicit `funcs=` entry
    would, without needing one; `let name be bounds` instead declares a
    genuinely free variable (no real parameter to alias, e.g. a gauge-
    invariance claim's arbitrary shift constant), `be`, not `in`, so
    it never reads like a `for` binding, exempted from the usual
    real-parameter-only domain-key check. If `name` also turns out to be
    a real parameter of whichever function is checked, with no separate
    `for name in ...` of its own in this same claim, that's harmless
    (there's still only one declared bound) and adjudicates like an
    ordinary `for`, noted in the result rather than treated as an error;
    declaring the *same* name via both `let ... be ...` and
    `for ... in ...` in one claim, though, raises `ConflictingDomainBinding`
    immediately; two different bounds for one name has no principled
    default to pick silently. `trials` is the claim's own trial
    budget, a positive whole number, which may exceed the usual limit.

    Inside a run scope (`_run_scope.run_scope`) a claim stated again with
    the same text and arguments is parsed once for the run; each call
    gets its own copy of the parse."""
    from . import _run_scope
    kept = _run_scope.kept("claims")
    if kept is not None:
        key = _claim_cache_key(law, name, source, route, grammar, funcs,
                               tolerance, pseudo_infinity, meta,
                               matrix_names, trials)
        if key is not None:
            hit = kept.get(key)
            if hit is None:
                hit = kept[key] = _claim_parse(
                    law, name, source, route, grammar, funcs, tolerance,
                    pseudo_infinity, meta, matrix_names, trials)
            return _claim_copy(hit)
    return _claim_parse(law, name, source, route, grammar, funcs, tolerance,
                        pseudo_infinity, meta, matrix_names, trials)

check_conjectures(fn, conjectures, domain=None, trials=None, trials_downscale=None, facts=None, extensive=False, known_premises=None, float_companions=False, pseudo_infinity=None, trials_scale=None)

Adjudicate proposed claims against the live function.

Throughout, bars around one of the matrices fn's signature declares read as its determinant, and the abs of such a matrix renders with its call spelling (grammar.bars_over_matrices).

trials omitted (None) uses the same structural-risk-based adaptive budget probe()'s own laws always have (probing._starting_budget), a claim about a structurally riskier function gets more trials, the same signal either way, since a claim is adjudicated by the exact same shared sampling setup (probing._prepare_sampling) probe()'s remaining structural checks use, computed lazily, at most once per call, the first time some claim actually reaches a probe-needing attempt. A batch of route="derive" claims whose proofs all decide never triggers it at all (an UNDECIDED derive claim now falls back to probing, empirical evidence supersedes an unknown, and pays for the setup like any probe claim). An explicit trials= always wins.

trials_scale is the same dev-loop knob probe() takes, clamped to (0, 1] (shrinks only) and floored the same way (never below _RiskPolicy.min_trials_floor_when_scaled or len(_SPECIALS), see probe()'s own docstring for why), so a single --trials-scale flag turns down every probe-route check in one call's worth of claims at once, built-in laws and author-stated conjectures alike.

extensive reaches a route="derive" claim's own case-split fallback (symbolic._prove.try_prove), widening its wall-clock cap when an ordinary proof attempt comes back undecided, and also widens the critical-point analysis behind a probe-route claim's own sampling the same way it does for probe() (see probing._prepare_sampling). Default False, same as probe()'s own extensive.

float_companions=True makes every claim the derive route proves (route "derive" or "best") spawn its computation claim, <name>[float], emitted directly after it: a derive proven is the mathematics in exact arithmetic, and the companion is the same relation executed against the real code in float (see gates._float_companion). A claim authored with route derive:math_only adjudicates as a derive claim and reports the mathematics line only: no companion (which its proof's meta states) and no policy row, the computation being outside its remit. check(), and so every CLI and store path, asks for companions; the default here keeps the adjudicator at one probe per claim.

Returns one Probe per conjecture (plus any float companions): holds (n=…) / falsified (with the counterexample) / skipped (invalid law, nothing evaluable, or a different grammar entirely, see the grammar check below, tagged in meta["mathema.foreign_grammar"] so a caller can tell the two kinds of skip apart), each noting who proposed it.

pseudo_infinity is the function level of the operational infinity (a claims-file entry's pseudo_infinity:, or check(fn, pseudo_infinity=)). Each claim's computation runs to the value resolved claim > function > MATHEMA_PSEUDO_INFINITY (records.resolve_pseudo_infinity, read once per call), else to the number representation's maximum; the derive route never reads it. Where the resolved value bounds an unbounded direction of a claim's effective domain, the claim's rows carry it with its level in meta["mathema.pseudo_infinity"], and its computation rows show it as a let in front of their condition (P8).

The bundled library claims (compendium.ensure_bundled) are applied before anything is adjudicated, unless a project layer is already installed.

Raises:

Type	Description
InvalidDomain	a function-level or MATHEMA_PSEUDO_INFINITY value that let |inf| be would refuse.

Source code in mathema/conjecture.py

@quiet_while_probing
def check_conjectures(fn, conjectures: list[Conjecture],
                      domain: dict | None = None, trials: int | None = None,
                      trials_downscale: float | None = None, facts=None,
                      extensive: bool = False,
                      known_premises: dict | None = None,
                      float_companions: bool = False,
                      pseudo_infinity=None,
                      trials_scale: float | None = None) -> list[Probe]:
    """Adjudicate proposed claims against the live function.

    Throughout, bars around one of the matrices `fn`'s signature
    declares read as its determinant, and the `abs` of such a matrix
    renders with its call spelling (`grammar.bars_over_matrices`).

    `trials` omitted (`None`) uses the same structural-risk-based
    adaptive budget `probe()`'s own laws always have
    (`probing._starting_budget`), a claim about a structurally
    riskier function gets more trials, the same signal either way,
    since a claim is adjudicated by the exact same shared sampling
    setup (`probing._prepare_sampling`) `probe()`'s remaining
    structural checks use, computed lazily, at most once per call,
    the first time some claim actually reaches a probe-needing
    attempt. A batch of route="derive" claims whose proofs all decide
    never triggers it at all (an UNDECIDED derive claim now falls back
    to probing, empirical evidence supersedes an unknown, and pays
    for the setup like any probe claim). An explicit `trials=` always
    wins.

    `trials_scale` is the same dev-loop knob probe() takes, clamped to
    (0, 1] (shrinks only) and floored the same way (never below
    `_RiskPolicy.min_trials_floor_when_scaled` or `len(_SPECIALS)`, see
    probe()'s own docstring for why), so a single `--trials-scale` flag
    turns down every probe-route check in one call's worth of claims at
    once, built-in laws and author-stated conjectures alike.

    `extensive` reaches a route="derive" claim's own case-split
    fallback (`symbolic._prove.try_prove`), widening its wall-clock cap
    when an ordinary proof attempt comes back undecided, and also
    widens the critical-point analysis behind a probe-route claim's own
    sampling the same way it does for `probe()` (see
    `probing._prepare_sampling`). Default `False`, same as `probe()`'s
    own `extensive`.

    `float_companions=True` makes every claim the derive route proves
    (route "derive" or "best") spawn its computation claim,
    `<name>[float]`, emitted directly after it: a derive `proven` is
    the mathematics in exact arithmetic, and the companion is the same
    relation executed against the real code in float (see
    `gates._float_companion`). A claim authored with route
    `derive:math_only` adjudicates as a derive claim and reports the
    mathematics line only: no companion (which its proof's meta states)
    and no policy row, the computation being outside its remit. `check()`, and so every CLI and
    store path, asks for companions; the default here keeps the
    adjudicator at one probe per claim.

    Returns one Probe per conjecture (plus any float companions): holds
    (n=…) / falsified (with the counterexample) / skipped (invalid law,
    nothing evaluable, or a different grammar entirely, see the
    `grammar` check below, tagged in `meta["mathema.foreign_grammar"]`
    so a caller can tell the two kinds of skip apart), each noting who
    proposed it.

    `pseudo_infinity` is the function level of the operational
    infinity (a claims-file entry's `pseudo_infinity:`, or
    `check(fn, pseudo_infinity=)`). Each claim's computation runs to
    the value resolved claim > function > `MATHEMA_PSEUDO_INFINITY`
    (`records.resolve_pseudo_infinity`, read once per call), else to the
    number representation's maximum; the derive route never reads it.
    Where the resolved value bounds an unbounded direction of a claim's
    effective domain, the claim's rows carry it with its level in
    `meta["mathema.pseudo_infinity"]`, and its computation rows show it
    as a `let` in front of their `condition` (P8).

    The bundled library claims (`compendium.ensure_bundled`) are
    applied before anything is adjudicated, unless a project layer is
    already installed.

    Raises:
        InvalidDomain: a function-level or `MATHEMA_PSEUDO_INFINITY`
            value that `let |inf| be` would refuse.
    """
    from .probing import resolve_trials_downscale
    trials_scale = resolve_trials_downscale(trials_downscale, trials_scale)
    from .types import matrix_param_names
    try:
        fn_mats = matrix_param_names(fn)
    except Exception:
        fn_mats = frozenset()
    try:
        facts = _effective_facts(fn, facts)
        runtime_mats = frozenset(p for p, k in facts.param_kinds.items()
                                 if k == "mat")
    except Exception:
        runtime_mats = frozenset()
    # the signature's matrices read the bars as determinants; those and
    # the matrix runtime types also render as matrices, their products
    # in written order
    # a policy claim is decided on the calls the other claims make, so
    # it is adjudicated after them
    built = [claim(c) if isinstance(c, str) else c for c in conjectures]
    for c in built:
        # a name bound to the function under test is f: nothing to `let`
        funcs = getattr(c, "funcs", None) or {}
        mine = {n for n, v in funcs.items() if v != n and _is_under_test(v, fn)}
        if mine:
            c.under_test = c.under_test | mine
    stated = [c for c in built if getattr(c, "relation", None) == "policy"]
    # the function's gates read every policy row, so they come last
    gates = [c for c in built if _policy_gate(c, fn, facts)]
    scalar_empty = [c for c in built if _empty_on_a_scalar(c, fn, facts)]
    values = [c for c in built if getattr(c, "relation", None) != "policy"
              and c not in gates and c not in scalar_empty]
    from ._empty_input import STATED
    # the claims checked here state the empty policy their value claims
    # read; a nested check (a chain's links) keeps the outer ones too
    stated_token = STATED.set((*STATED.get(), *built))
    try:
        return _check_built(fn, built, values, stated, gates, scalar_empty,
                            fn_mats, runtime_mats, domain, trials,
                            trials_scale, facts, extensive, known_premises,
                            float_companions, pseudo_infinity)
    finally:
        STATED.reset(stated_token)

mathema.symbolic

mathema.symbolic

Symbolic proof: the derive evidence route. Public re-export surface for the package, import from here (from mathema.symbolic import lift, try_prove), never from a private mathema.symbolic._xxx submodule directly; those are implementation detail and may be reorganized without notice.

The underscore-prefixed names here are deliberately exported: they are the package-internal analysis surface inventory/analysis/tiers/ _tier_text consume (lift context walking, expression conversion, loop-header classification, branch explanation), internal to mathema, stable enough for its own sibling modules, not for third parties. The per-shape lift record classes (FoldLift and friends) are not exported: nothing outside this package constructs or annotates one.

Lifted dataclass

A function body lifted to a sympy expression: the symbolic form the derive route reasons over. expr is an ordinary sympy.Expr for a function with a single return value; for a function whose return statement is a tuple (return x, y), it's a plain Python tuple of sympy.Expr, one per element; there is no vector/matrix type here, just a fixed-length group of otherwise-independent scalar results.

params maps every liftable quantity to its symbol, ordinarily one entry per signature parameter, but a parameter that bundles many scalars (a flat dataclass, or a dict accessed by literal string keys, see _bind_params) expands into several composite-keyed entries ("cfg.a", "cfg.b") instead of one. sig_params/aggregate are what let f(...) call substitution still work in terms of the real signature: sig_params is the actual positional parameter order, and aggregate[p] is the list of composite keys p expanded into (or None for an ordinary, single-symbol parameter). opaque, when this lift encountered any non-numeric value (a string, None, an Enum member, see finitesetspy), is the registry those values were registered through, carried here so a claim's own law text can register its own literals into the same registry (f(x) == "positive" needs "positive" to resolve to the identical symbol the body itself produced, not an unrelated fresh one).

Source code in mathema/symbolic/_base.py

@dataclass
class Lifted:
    """A function body lifted to a sympy expression: the symbolic form the
    derive route reasons over. `expr` is an ordinary sympy.Expr for a
    function with a single return value; for a function whose `return`
    statement is a tuple (`return x, y`), it's a plain Python tuple of
    sympy.Expr, one per element; there is no vector/matrix type here,
    just a fixed-length group of otherwise-independent scalar results.

    `params` maps every liftable *quantity* to its symbol, ordinarily
    one entry per signature parameter, but a parameter that bundles many
    scalars (a flat dataclass, or a dict accessed by literal string keys,
    see _bind_params) expands into several composite-keyed entries
    ("cfg.a", "cfg.b") instead of one. `sig_params`/`aggregate` are what
    let `f(...)` call substitution still work in terms of the *real*
    signature: `sig_params` is the actual positional parameter order,
    and `aggregate[p]` is the list of composite keys `p` expanded into
    (or `None` for an ordinary, single-symbol parameter). `opaque`, when
    this lift encountered any non-numeric value (a string, `None`, an
    Enum member, see finite_sets.py), is the registry those values
    were registered through, carried here so a claim's own law text
    can register its own literals into the *same* registry (`f(x) ==
    "positive"` needs `"positive"` to resolve to the identical symbol
    the body itself produced, not an unrelated fresh one)."""
    expr: "sympy.Expr | tuple"
    params: dict            # possibly composite-keyed name -> sympy.Symbol
    sig_params: list = field(default_factory=list)
    aggregate: dict = field(default_factory=dict)
    unicode: str = ""
    latex: str = ""
    derived: list = field(default_factory=list)
    opaque: "OpaqueRegistry | None" = None
    branch_complete: bool = False

ProofResult dataclass

The outcome of a single derive-route decision: try_prove()/ try_prove_raises()'s return type. sketch is a short, human- readable explanation of how the status was reached (which expressions simplified to what, or why a sign/equality couldn't be settled), always present except when status is "unliftable" for a reason obvious from context. quantifier is only ever set alongside status == "proven": a closed-form '∀ x ∈ ℝ, ...' clause naming exactly the variables the proof actually holds over (see _quantifier_clause); a proof has no trial count the way a probe does, so this is what stands in its place.

Source code in mathema/symbolic/_proof_support.py

@dataclass
class ProofResult:
    """The outcome of a single derive-route decision: `try_prove()`/
    `try_prove_raises()`'s return type. `sketch` is a short, human-
    readable explanation of how the status was reached (which
    expressions simplified to what, or why a sign/equality couldn't be
    settled), always present except when `status` is `"unliftable"`
    for a reason obvious from context. `quantifier` is only ever set
    alongside `status == "proven"`: a closed-form '∀ x ∈ ℝ, ...' clause
    naming exactly the variables the proof actually holds over (see
    _quantifier_clause); a proof has no trial count the way a probe
    does, so this is what stands in its place."""
    status: str   # "proven" | "disproven" | "undecided" | "unliftable"
    sketch: str | None = None
    counterexample: str | None = None
    quantifier: str | None = None
    meta: dict = field(default_factory=dict)
    witness: dict | None = None
    # a concrete counterexample point behind a "disproven" (free-var
    # name -> sympy/number value), seeding the corroboration engine so
    # it re-checks the disproof against the ORIGINAL function, not the
    # internal (possibly corrupted) residual. `None` when the decider
    # had no point (the engine then searches).
    disproof_hint: "sympy.Expr | None" = None
    # the offending expression whose sign/value flipped, machine-
    # readable "where/why", so corroboration can perturb around its own
    # critical points rather than sampling blind.
    intermediates: "tuple | None" = None

lift(fn, facts, max_callee_depth=3, domain=None, _ctx=None, _opaque=None)

Translate a function body to a sympy expression. Only a loop-free, branch-free, non-recursive, all-scalar body is attempted; everything else returns None rather than guessing at a closed form; this gate is unaffected by domain, which never lets this function's own branches through (that's lift_conditioned()'s job); it only ever widens what a callee can resolve, below.

A call this body makes to a name that isn't a known math function (_SYMPY_FUNCS) but does resolve to a real, plain Python function; _display(np.minimum(r, R_CLIP))'s _display, say, isn't refused outright: _try_inline_callee recursively lifts the callee (this same function, one step further down) and substitutes its own parameters with this call site's argument expressions, up to max_callee_depth levels deep (mirrors docstring.docstring_sync()'s own max_callee_depth, the same concept applied to code/docstring sync rather than proof). If the callee itself has a branch, domain, fn's own declared domain, over fn's own parameters; lets _try_inline_callee derive a domain for the callee's parameters too (only for a bare-parameter-passthrough call-site argument, see _derive_passthrough_domain) and try lift_conditioned() on it as a fallback. This doesn't weaken lift()'s own contract for fn: the proof's claimed validity was already scoped to domain by try_prove()'s own quantifier-clause wrapping regardless of whether lift() itself consulted it, so a callee resolved this way is no less sound than one resolved directly in fn's own body would be. _ctx is private, only _try_inline_callee passes it, to carry the shrinking depth budget and the set of already-inlined callees (cycle protection) down through a recursive lift() call; an external caller only ever sets max_callee_depth/domain. _opaque is likewise private, _try_inline_callee forwards the caller's own registry so an opaque value means the same thing throughout a callee-inlining chain; an external caller never sets it (a fresh registry is built automatically).

Source code in mathema/symbolic/_base.py

def lift(fn, facts, max_callee_depth: int = 3, domain: dict | None = None,
        _ctx: "_LiftCtx | None" = None, _opaque: "OpaqueRegistry | None" = None) -> "Lifted | None":
    """Translate a function body to a sympy expression. Only a loop-free,
    branch-free, non-recursive, all-scalar body is attempted; everything
    else returns None rather than guessing at a closed form; this gate
    is unaffected by `domain`, which never lets *this* function's own
    branches through (that's lift_conditioned()'s job); it only ever
    widens what a *callee* can resolve, below.

    A call this body makes to a name that isn't a known math function
    (_SYMPY_FUNCS) but does resolve to a real, plain Python function;
    `_display(np.minimum(r, R_CLIP))`'s `_display`, say, isn't refused
    outright: `_try_inline_callee` recursively lifts the callee (this
    same function, one step further down) and substitutes its own
    parameters with this call site's argument expressions, up to
    `max_callee_depth` levels deep (mirrors docstring.docstring_sync()'s
    own `max_callee_depth`, the same concept applied to code/docstring
    sync rather than proof). If the callee itself has a branch, `domain`,
    `fn`'s own declared domain, over `fn`'s own parameters; lets
    `_try_inline_callee` derive a domain for the callee's parameters too
    (only for a bare-parameter-passthrough call-site argument, see
    _derive_passthrough_domain) and try lift_conditioned() on it as a
    fallback. This doesn't weaken lift()'s own contract for `fn`: the
    proof's claimed validity was already scoped to `domain` by
    try_prove()'s own quantifier-clause wrapping regardless of whether
    lift() itself consulted it, so a callee resolved this way is no less
    sound than one resolved directly in `fn`'s own body would be.
    `_ctx` is private, only `_try_inline_callee` passes it, to carry
    the shrinking depth budget and the set of already-inlined callees
    (cycle protection) down through a recursive lift() call; an external
    caller only ever sets `max_callee_depth`/`domain`. `_opaque` is
    likewise private, `_try_inline_callee` forwards the caller's own
    registry so an opaque value means the same thing throughout a
    callee-inlining chain; an external caller never sets it (a fresh
    registry is built automatically)."""
    if facts.tree is None or facts.loops or facts.branch_count or facts.recursion:
        return None
    if not facts.params or any(k in SEQUENCE_KINDS for k in facts.param_kinds.values()):
        return None

    _sp, _sc = _method_ctx_fields(fn, facts)
    ctx = _ctx or _LiftCtx(globals_ns=module_scope(fn),
                           depth=max_callee_depth, seen=frozenset({id(fn)}),
                           domain=domain or {},
                           unmodified=frozenset(_unmodified_params(facts.tree, set(facts.params))),
                           self_param=_sp, self_class=_sc)
    opaque = _opaque if _opaque is not None else OpaqueRegistry()
    params, aggregate = _bind_params(fn, facts)
    env = dict(params)
    from ._normalize import normalized_body
    body = normalized_body(fn, facts)

    kind, result, _failure = _walk_lift_body(body, env, ctx, allow_raise=False, opaque=opaque)
    if kind != "value":
        return None

    result = (tuple(_simplify_maybe_array(r) for r in result) if isinstance(result, tuple)
             else _simplify_maybe_array(result))
    # an inlined sibling method can introduce field symbols the caller
    # itself never read (present_value reads self.face, its inlined
    # discount reads self.rate): fold them into the symbol table so
    # claim text and domains can name them like any other field
    for _sym in (set() if isinstance(result, (tuple, _SymbolicArray))
                 else getattr(result, "free_symbols", set())):
        _name = str(_sym)
        _root = _name.split(".", 1)[0]
        if "." in _name and _root in facts.params and _name not in params:
            params[_name] = _sym
            aggregate[_root] = (aggregate.get(_root) or []) + [_name]
    display = _display_value(result)
    from ..grammar import render_canonical
    return Lifted(expr=result, params=params, sig_params=list(facts.params),
                  aggregate=aggregate, unicode=render_canonical(display)[0],
                  latex=sympy.latex(display), opaque=opaque)

lift_conditioned(fn, facts, domain, max_callee_depth=3, _ctx=None, _opaque=None)

Like lift(), but for a function whose branches resolve under the given domain (see _branch_condition_truth/_prune_body), still refuses loops/recursion/non-scalar parameters outright, unchanged from lift(); this only ever widens what counts as branch-free for this specific domain. None if there's nothing to prune (lift() already covers that), the domain doesn't settle enough branches, or the resolution budget (_MAX_PRUNED_BRANCHES) runs out. max_callee_depth is the same callee-inlining budget lift() itself takes, see there, applied here to the pruned body's own final walk, which also carries domain itself through so a callee this pruned body calls can attempt its own domain-derived conditioning in turn (see _try_inline_callee/_derive_passthrough_domain). _ctx/_opaque are private, same role as lift()'s own, only a recursive call from _try_inline_callee (inlining a callee that itself needs conditioning) passes them.

Source code in mathema/symbolic/_conditioned.py

def lift_conditioned(fn: Callable[..., Any], facts: Facts, domain: dict,
                     max_callee_depth: int = 3,
                     _ctx: "_LiftCtx | None" = None,
                     _opaque: "OpaqueRegistry | None" = None) -> "ConditionedLift | None":
    """Like lift(), but for a function whose branches resolve under the
    given domain (see _branch_condition_truth/_prune_body), still
    refuses loops/recursion/non-scalar parameters outright, unchanged
    from lift(); this only ever widens what counts as branch-free for
    *this specific domain*. `None` if there's nothing to prune (lift()
    already covers that), the domain doesn't settle enough branches, or
    the resolution budget (_MAX_PRUNED_BRANCHES) runs out. `max_callee_depth`
    is the same callee-inlining budget lift() itself takes, see there,
    applied here to the pruned body's own final walk, which also
    carries `domain` itself through so a callee this pruned body calls
    can attempt its own domain-derived conditioning in turn (see
    _try_inline_callee/_derive_passthrough_domain). `_ctx`/`_opaque` are
    private, same role as lift()'s own, only a recursive call from
    _try_inline_callee (inlining a callee that itself needs
    conditioning) passes them."""
    if facts.tree is None or facts.loops or facts.recursion:
        return None
    if not facts.branch_count:
        return None
    if not facts.params or any(k in SEQUENCE_KINDS for k in facts.param_kinds.values()):
        return None

    unmodified = _unmodified_params(facts.tree, set(facts.params))
    body = strip_docstring(facts.tree.body)

    # params/aggregate must exist before pruning, not just before the
    # final body-walk below: a branch condition over an *affine local*
    # (see _affine_locals) needs the unmodified parameters' own symbols
    # to lift that local's defining expression, which is exactly what
    # _prune_body -> _branch_condition_truth -> _compare_truth needs to
    # decide such a condition against the domain.
    params, aggregate = _bind_params(fn, facts)
    affine_locals = _affine_locals(facts.tree, unmodified, params)

    pruned = _prune_body(body, domain, unmodified, [_MAX_PRUNED_BRANCHES],
                         affine_locals, params)
    if pruned is None:
        return None

    from ._base import _method_ctx_fields
    _sp, _sc = _method_ctx_fields(fn, facts)
    ctx = _ctx or _LiftCtx(globals_ns=module_scope(fn),
                           depth=max_callee_depth, seen=frozenset({id(fn)}),
                           domain=domain, unmodified=frozenset(unmodified),
                           self_param=_sp, self_class=_sc)
    opaque = _opaque if _opaque is not None else OpaqueRegistry()
    env = dict(params)
    sig_params = list(facts.params)
    kind, result, _failure = _walk_lift_body(pruned, env, ctx, allow_raise=True, opaque=opaque)
    if kind == "value":
        result = (tuple(_simplify_maybe_array(r) for r in result)
                 if isinstance(result, tuple) else _simplify_maybe_array(result))
        return ConditionedLift(kind="value", expr=result, params=params,
                               sig_params=sig_params, aggregate=aggregate, opaque=opaque)
    if kind == "raises":
        return ConditionedLift(kind="raises", exc_type=result, params=params,
                               sig_params=sig_params, aggregate=aggregate, opaque=opaque)
    return None

try_prove(fn, facts, lhs_src, rhs_src, relation, domain=None, tolerance=None, max_callee_depth=3, extensive=False, _split_depth=0, funcs=None, assumption=None, assume_defined=False, exclude_own_guards=False)

See _try_prove. A proof is kept only when every raise region of the functions it reads was read too: a statement the raise-region pass stops at could hide a raise in the domain, and a value claim is false wherever the code raises. ~= is decided as abs(lhs - rhs) <= ε (see _try_prove_within_epsilon), or, under a tolerance kind, as the bound the kind states (_try_prove_within_kind).

Source code in mathema/symbolic/_prove.py

def try_prove(fn, facts, lhs_src: str, rhs_src: str, relation: str,
             domain: dict | None = None, tolerance: float | None = None,
             max_callee_depth: int = 3, extensive: bool = False,
             _split_depth: int = 0, funcs: dict | None = None,
             assumption: "list | None" = None,
             assume_defined: bool = False,
             exclude_own_guards: bool = False) -> ProofResult:
    """See `_try_prove`. A proof is kept only when every raise region
    of the functions it reads was read too: a statement the raise-region
    pass stops at could hide a raise in the domain, and a value claim is
    false wherever the code raises. `~=` is decided as `abs(lhs - rhs)
    <= ε` (see `_try_prove_within_epsilon`), or, under a tolerance kind,
    as the bound the kind states (`_try_prove_within_kind`)."""
    from .._tolerance import ToleranceKind, bare
    if isinstance(tolerance, ToleranceKind):
        if relation != "~=":
            bare(tolerance, f"a {relation} proof")
        return _try_prove_within_kind(
            fn, facts, lhs_src, rhs_src, tolerance, domain=domain,
            max_callee_depth=max_callee_depth, extensive=extensive,
            _split_depth=_split_depth, funcs=funcs, assumption=assumption,
            assume_defined=assume_defined,
            exclude_own_guards=exclude_own_guards)
    if relation == "~=":
        return _try_prove_within_epsilon(
            fn, facts, lhs_src, rhs_src, domain=domain, tolerance=tolerance,
            max_callee_depth=max_callee_depth, extensive=extensive,
            _split_depth=_split_depth, funcs=funcs, assumption=assumption,
            assume_defined=assume_defined,
            exclude_own_guards=exclude_own_guards)
    notes: dict = {}
    result = _try_prove(fn, facts, lhs_src, rhs_src, relation, domain,
                        tolerance, max_callee_depth, extensive, _split_depth,
                        funcs, assumption, assume_defined, _walk_notes=notes,
                        exclude_own_guards=exclude_own_guards)
    if result.status == "proven" and notes.get("claim_side"):
        return ProofResult(
            "undecided",
            sketch=(f"{result.sketch}; not kept as a proof: "
                    f"{notes['claim_side']}"),
            meta=dict(result.meta))
    if result.status == "proven" and notes.get("unread") and not assume_defined:
        return ProofResult(
            "undecided",
            sketch=(f"{result.sketch}; not kept as a proof: the raise-region "
                    f"pass stops at {notes['unread']}, so a raise inside the "
                    "domain is not ruled out"),
            meta=dict(result.meta))
    empty = _empty_sequence_raise(fn, facts, lhs_src, rhs_src, domain,
                                  assumption)
    if empty is not None:
        return empty
    if result.status == "proven":
        region = _complex_value_region(fn, facts, lhs_src, rhs_src, domain)
        if region is not None:
            return ProofResult(
                "undecided",
                sketch=(f"{result.sketch}; not kept as a proof: f returns a "
                        f"complex number where {region} (a fractional power "
                        f"of a negative base), which the declared domain "
                        f"does not exclude, and the proof reads f as real"),
                meta=dict(result.meta))
        kink = _derivative_kink(fn, facts, lhs_src, rhs_src, domain)
        if kink is not None:
            return ProofResult(
                "undecided",
                sketch=(f"{result.sketch}; not kept as a proof: f is not "
                        f"differentiable where {kink}, which the declared "
                        f"domain does not exclude"),
                meta=dict(result.meta))
    return result

try_prove_raises(fn, facts, call_src, exc_name, domain=None, max_callee_depth=3)

A raises(...) claim on the derive route, only ever reachable via domain-conditioned branch pruning: a raises claim with no declared domain specific enough to determine which branch runs stays unliftable, the same as any other derive claim would with an unresolvable branch. call_src must be a bare f(...) call (no multi-function claims here, same restriction check_conjectures() already applies before this is ever called). max_callee_depth is forwarded to lift_conditioned(), see lift()'s own docstring.

Source code in mathema/symbolic/_prove.py

def try_prove_raises(fn, facts, call_src: str, exc_name: str | None,
                     domain: dict | None = None, max_callee_depth: int = 3) -> ProofResult:
    """A raises(...) claim on the derive route, only ever reachable via
    domain-conditioned branch pruning: a raises claim with no declared
    domain specific enough to determine which branch runs stays
    unliftable, the same as any other derive claim would with an
    unresolvable branch. `call_src` must be a bare `f(...)` call (no
    multi-function claims here, same restriction check_conjectures()
    already applies before this is ever called). `max_callee_depth` is
    forwarded to lift_conditioned(), see lift()'s own docstring."""
    try:
        tree = ast.parse(call_src, mode="eval")
    except SyntaxError as e:
        return ProofResult("unliftable", sketch=f"unparseable call: {e}")
    if not (isinstance(tree.body, ast.Call) and isinstance(tree.body.func, ast.Name)
            and tree.body.func.id == "f"):
        return ProofResult("unliftable", sketch="raises(...) needs a bare f(...) call")

    if facts.tree is not None and not any(isinstance(n, ast.Raise) for n in ast.walk(facts.tree)):
        return ProofResult("unliftable", sketch="no explicit raise statement "
                           "anywhere in this function, an exception implicit "
                           "in an arithmetic operation (division, sqrt of a "
                           "negative, ...) can't be proven this way; only an "
                           "explicit `if cond: raise ...` guard can")

    conditioned = lift_conditioned(fn, facts, domain or {}, max_callee_depth=max_callee_depth)
    if conditioned is None:
        branch_sketch = _branch_pruning_sketch(fn, facts)
        if branch_sketch is not None:
            return ProofResult("unliftable", sketch=f"branch pruning couldn't "
                               f"settle which side runs under this domain: "
                               f"{branch_sketch}")
        return ProofResult("unliftable", sketch="function body is not derivable "
                           "in v1 even with branch pruning: contains a loop, "
                           "recursion, a non-scalar parameter, or the declared "
                           "domain doesn't settle which branch runs")
    if conditioned.kind == "value":
        return ProofResult("disproven", sketch="the function returns a value "
                           "under this domain rather than raising")
    if exc_name is None or conditioned.exc_type == exc_name:
        return ProofResult("proven", sketch=f"raises {conditioned.exc_type or '(unknown type)'} "
                           "under this domain")
    if conditioned.exc_type is None:
        return ProofResult("undecided", sketch="raises under this domain, but the "
                           "exception type couldn't be determined")
    return ProofResult("disproven", sketch=f"raises {conditioned.exc_type}, "
                       f"not the claimed {exc_name}")

mathema.inventory

mathema.inventory

Facts about one function: is it pure enough that a claim is realistically expected, does its docstring pass a checklist, is it liftable for a derive-route proof, does it depend on state outside its own parameters, is it exercised by the target's own tests (best-effort, only if a coverage report already exists). Everything here answers a question about a single function, standalone, e.g. mathema. docstring_report() calls straight into docstring_quality() for just one function, no sweep involved.

Distinct from audit.py, which sweeps a whole population by calling these primitives across it and shapes the results into audit rows/ rollups; that's "found N functions, called is_pure_enough() on each, built a table"; this module is what it's calling. Distinct too from cli.py's per-function "claims X/Y adjudicated": that's the completeness of ONE already-declared claim set, whereas this module (via audit.py) surfaces functions with zero claims, which the declared/verified store alone can never show.

is_pure_enough(fn)

A purity proxy, not a judgment about claim-worthiness on its own: reuses symbolic.py's own derive-route liftability check (loop-free, branch-free, non-recursive, scalar parameters, and; for a method; read-only over self: field reads and sibling calls derive; writes or escapes of self do not). None means mathema couldn't even retrieve the source, not a verdict either way, e.g. a function from a C extension or built dynamically.

Source code in mathema/inventory.py

def is_pure_enough(fn) -> bool | None:
    """A purity proxy, not a judgment about claim-worthiness on its
    own: reuses symbolic.py's own derive-route liftability check
    (loop-free, branch-free, non-recursive, scalar parameters, and;
    for a method; read-only over `self`: field reads and sibling
    calls derive; writes or escapes of `self` do not). `None` means mathema couldn't even retrieve the
    source, not a verdict either way, e.g. a function from a C
    extension or built dynamically."""
    from .symbolic import lift, lift_dot, lift_fold, lift_sum

    facts = quiet_facts(fn)
    if facts is None or facts.tree is None:
        return None
    if facts.params and facts.params[0] in ("self", "cls") \
            and _self_use_blocks(facts.tree, facts.params[0]):
        return False
    try:
        # lift_fold()/lift_dot()/lift_sum(), not just lift(): a
        # recognized linear-fold loop, dot-product, or general-sum
        # loop shape is liftable standalone, the same way lift() is,
        # unlike lift_conditioned()'s branch pruning, none of
        # them need a per-claim domain, so all belong in this
        # domain-free summary too.
        return (lift(fn, facts) is not None or lift_fold(fn, facts) is not None
               or lift_dot(fn, facts) is not None or lift_sum(fn, facts) is not None)
    except Exception:
        return None

purity_reason(fn)

Why is_pure_enough() said no; None means it's liftable (or source wasn't available, same as is_pure_enough()'s own None). Mirrors lift()'s own gate conditions exactly (same facts fields, same order), so the reason reported here is always consistent with what lift() actually did, not a separate guess at why.

Purity here is specifically "liftable for a derive-route proof"; it says nothing about whether a probe-route claim is viable. Probe doesn't lift anything; it calls the real function on sampled inputs, so branches, loops, and non-numeric parameters are no obstacle to it at all. A function reported not-pure here can still be claimed about perfectly well on the probe route; this only ever narrows which functions can additionally get proof-strength (derive-route) evidence, not which functions can be claimed about at all.

Source code in mathema/inventory.py

def purity_reason(fn) -> str | None:
    """Why is_pure_enough() said no; `None` means it's liftable (or
    source wasn't available, same as is_pure_enough()'s own `None`).
    Mirrors lift()'s own gate conditions exactly (same `facts` fields,
    same order), so the reason reported here is always consistent with
    what lift() actually did, not a separate guess at why.

    Purity here is specifically "liftable for a *derive-route* proof";
    it says nothing about whether a *probe-route* claim is viable. Probe
    doesn't lift anything; it calls the real function on sampled inputs,
    so branches, loops, and non-numeric parameters are no obstacle to it
    at all. A function reported not-pure here can still be claimed about
    perfectly well on the probe route; this only ever narrows which
    functions can additionally get proof-strength (derive-route)
    evidence, not which functions can be claimed about at all."""
    from .symbolic import lift, lift_dot, lift_fold, lift_sum

    facts = quiet_facts(fn)
    if facts is None:
        return None
    if facts.tree is None:
        return None
    if facts.params and facts.params[0] in ("self", "cls") \
            and _self_use_blocks(facts.tree, facts.params[0]):
        return f"stateful: updates {facts.params[0]} internally"
    if facts.loops and not facts.branch_count \
            and (lift_fold(fn, facts) is not None or lift_sum(fn, facts) is not None):
        return None
    if facts.loops or facts.branch_count:
        complexity = structural_complexity(fn)
        parts = []
        if complexity["branches"]:
            parts.append(f"{complexity['branches']} branch"
                         + ("es" if complexity['branches'] > 1 else ""))
        if complexity["loops"]:
            loop_part = (f"{complexity['loops']} loop"
                         + ("s" if complexity['loops'] > 1 else ""))
            if complexity["nested_loops"]:
                loop_part += f" ({complexity['nested_loops']} nested)"
            parts.append(loop_part)
        return ", ".join(parts)
    if facts.recursion:
        n = structural_complexity(fn)["recursive_calls"]
        return f"recursive ({n} call site{'s' if n != 1 else ''})"
    if not facts.params:
        return "no parameters"
    non_scalar = [p for p, k in facts.param_kinds.items() if k in SEQUENCE_KINDS]
    if non_scalar:
        if lift_dot(fn, facts) is not None:
            return None
        return f"non-scalar parameter(s): {', '.join(non_scalar)}"
    try:
        lifted = lift(fn, facts)
    except Exception:
        return "uses unsupported expression syntax"
    if lifted is None:
        return "uses unsupported expression syntax"
    return None

claim_floor(fn, facts=None)

Intent

The least this function's shape gives you to state: one claim per relevant claim family, per target. {"floor": int, "aspects": [[aspect, target], ...]}, or None when the source cannot be retrieved.

Notes

A floor, never a ceiling, a function carrying more claims than this is not over its budget, and nothing here divides by it. How many claims a function of this shape typically carries is a different question, answered by a corpus, not by structure.

Claims answering the same question about the same target count once (convex[x]/concave[x]/affine[x] are one aspect, see families.CLAIM_ASPECTS), while every member of a keyword group counts separately, since stateless expanding to three claims is three separate things to say.

Deliberately independent of whether the function lifts. Most families offer a probe route, so an unliftable function still has a floor, a smaller one, because the derive-only families drop out on their own structural gates.

Source code in mathema/inventory.py

def claim_floor(fn, facts=None) -> dict | None:
    """Intent:
        The least this function's shape gives you to state: one claim
        per relevant claim family, per target. `{"floor": int,
        "aspects": [[aspect, target], ...]}`, or None when the source
        cannot be retrieved.

    Notes:
        A floor, never a ceiling, a function carrying more claims
        than this is not over its budget, and nothing here divides by
        it. How many claims a function of this shape typically carries
        is a different question, answered by a corpus, not by
        structure.

        Claims answering the same question about the same target count
        once (`convex[x]`/`concave[x]`/`affine[x]` are one aspect,
        see `families.CLAIM_ASPECTS`), while every member of a keyword
        group counts separately, since `stateless` expanding to three
        claims is three separate things to say.

        Deliberately independent of whether the function lifts. Most
        families offer a probe route, so an unliftable function still
        has a floor, a smaller one, because the derive-only families
        drop out on their own structural gates.
    """
    from .families import claim_aspect
    from .suggest import suggest_claims

    if facts is None:
        facts = quiet_facts(fn)
    if facts is None or facts.tree is None:
        return None
    aspects = sorted({claim_aspect(cj.name)
                      for cj in suggest_claims(fn, facts)})
    return {"floor": len(aspects),
            "aspects": [list(pair) for pair in aspects]}

derivability_report(fn)

Deep-dive diagnosis of why a function isn't derivable (mathema audit --deriv-report), unlike purity_reason()'s single summary string, this locates the exact blocking construct (source line and a stable, versioned "category" code) for an unsupported-syntax failure, and for a branch, classifies each branch's condition individually as either resolvable (naming which parameters a claim would need to declare a domain for) or structurally blocked (naming why), see _explain_branch().

purity_reason()'s single generic "uses unsupported expression syntax" bucket only reports that lifting failed, not where: it swallows the actual NotSymbolic message and source location. A function can fail to lift for a reason several statements away from where the failure is easiest to guess at (a tuple return further down the body, say, when the real blocker is an earlier ternary); this function surfaces the precise statement and category instead of requiring that tracing to be done by hand.

Deliberately raw: every field here is a mechanical fact about the function's own source (which construct, which line, which stable category name from symbolic.NotSymbolic's fixed vocabulary), never an editorial verdict about whether it's worth fixing. A caller wanting that judgment call layers it on top of this report, not the other way around.

None if the source isn't available at all (same convention as purity_reason()/is_pure_enough()). Otherwise a dict with at least "liftable" (True means this function shouldn't have been asked about at all; callers should only reach for this on rows where pure is False) and, when not liftable, a stable "blocker" name plus blocker-specific raw detail; "branches" (a list of {"line", "condition", "kind", ...}, one per ast.If anywhere in the body) for the branch case specifically, since a function can have several independent branches with different fates.

Source code in mathema/inventory.py

def derivability_report(fn) -> dict | None:
    """Deep-dive diagnosis of *why* a function isn't derivable
    (`mathema audit --deriv-report`), unlike purity_reason()'s single
    summary string, this locates the exact blocking construct (source
    line and a stable, versioned `"category"` code) for an
    unsupported-syntax failure, and for a branch, classifies *each*
    branch's condition individually as either resolvable (naming which
    parameters a claim would need to declare a domain for) or
    structurally blocked (naming why), see _explain_branch().

    purity_reason()'s single generic "uses unsupported expression
    syntax" bucket only reports *that* lifting failed, not *where*:
    it swallows the actual NotSymbolic message and source location. A
    function can fail to lift for a reason several statements away from
    where the failure is easiest to guess at (a tuple return further
    down the body, say, when the real blocker is an earlier ternary);
    this function surfaces the precise statement and category instead
    of requiring that tracing to be done by hand.

    Deliberately raw: every field here is a mechanical fact about the
    function's own source (which construct, which line, which stable
    category name from `symbolic.NotSymbolic`'s fixed vocabulary),
    never an editorial verdict about whether it's worth fixing. A
    caller wanting that judgment call layers it on top of this report,
    not the other way around.

    `None` if the source isn't available at all (same convention as
    purity_reason()/is_pure_enough()). Otherwise a dict with at least
    `"liftable"` (`True` means this function shouldn't have been asked
    about at all; callers should only reach for this on rows where
    `pure is False`) and, when not liftable, a stable `"blocker"` name
    plus blocker-specific raw detail; `"branches"` (a list of
    `{"line", "condition", "kind", ...}`, one per `ast.If` anywhere in
    the body) for the branch case specifically, since a function can
    have several independent branches with different fates."""
    from .symbolic import (_LiftCtx, _affine_locals, _bind_params, _explain_branch,
                           strip_docstring, _unmodified_params, _walk_lift_body,
                           diagnose_fold, lift_dot, lift_fold, lift_sum)
    from .finite_sets import OpaqueRegistry

    facts = quiet_facts(fn)
    if facts is None:
        return None
    if facts.tree is None:
        return None

    if facts.params and facts.params[0] in ("self", "cls") \
            and _self_use_blocks(facts.tree, facts.params[0]):
        return {"liftable": False, "blocker": "stateful", "param": facts.params[0],
               "line": facts.tree.lineno}
    if facts.loops:
        if lift_fold(fn, facts) is not None or lift_sum(fn, facts) is not None:
            return {"liftable": True}
        diagnosis = diagnose_fold(fn, facts)
        first_loop = next((node for node in ast.walk(facts.tree)
                          if isinstance(node, (ast.For, ast.While))), facts.tree)
        if diagnosis is None:
            # every structural check in diagnose_fold passed but
            # lift_fold() still declined, shouldn't happen if the two
            # are kept in sync; report honestly rather than claim a
            # specific reason that isn't real.
            return {"liftable": False, "blocker": "loop", "reason": "unclassified",
                   "line": first_loop.lineno}
        return {"liftable": False, "blocker": "loop", "reason": diagnosis["reason"],
               "hint": diagnosis.get("hint"), "derive_unlock": diagnosis.get("derive_unlock"),
               "line": first_loop.lineno}
    if facts.branch_count:
        body = strip_docstring(facts.tree.body)
        unmodified = _unmodified_params(facts.tree, set(facts.params))
        bound_params, _aggregate = _bind_params(fn, facts)
        affine_locals = _affine_locals(facts.tree, unmodified, bound_params)
        branches = [
            {"line": node.lineno, "condition": ast.unparse(node.test),
             **_explain_branch(node.test, unmodified, affine_locals, bound_params)}
            for node in ast.walk(facts.tree) if isinstance(node, ast.If)
        ]
        return {"liftable": False, "blocker": "branch", "branches": branches,
               "line": branches[0]["line"]}
    if facts.recursion:
        n = structural_complexity(fn)["recursive_calls"]
        first_call = next(node for node in ast.walk(facts.tree)
                         if isinstance(node, ast.Call) and isinstance(node.func, ast.Name)
                         and node.func.id == facts.name)
        return {"liftable": False, "blocker": "recursion", "recursive_calls": n,
               "line": first_call.lineno}
    if not facts.params:
        return {"liftable": False, "blocker": "no-parameters", "line": facts.tree.lineno}
    non_scalar = [p for p, k in facts.param_kinds.items() if k in SEQUENCE_KINDS]
    if non_scalar:
        if lift_dot(fn, facts) is not None:
            return {"liftable": True}
        return {"liftable": False, "blocker": "non-scalar-parameters",
               "params": non_scalar, "line": facts.tree.lineno}

    params, _aggregate2 = _bind_params(fn, facts)
    env = dict(params)
    from .symbolic._normalize import normalized_body
    body = normalized_body(fn, facts)
    # a real ctx/opaque, not the bare `_walk_lift_body(body, env)`
    # this used before, so this retrace recognizes exactly what
    # lift() itself would (callee inlining, opaque values, local
    # symbolic arrays from np.linspace/np.arange): otherwise a
    # function lift() already handles could still be diagnosed here
    # against a *stricter* retrace than what actually ran, reporting
    # a blocker that isn't real. Only reached for a row already
    # known not to lift (see this function's own docstring), so
    # this never contradicts is_pure_enough()/purity_reason().
    from .symbolic._base import _method_ctx_fields
    _sp, _sc = _method_ctx_fields(fn, facts)
    ctx = _LiftCtx(globals_ns=module_scope(fn), depth=3,
                   seen=frozenset({id(fn)}), domain={},
                   unmodified=frozenset(_unmodified_params(facts.tree, set(facts.params))),
                   self_param=_sp, self_class=_sc)
    try:
        kind, _result, failure = _walk_lift_body(body, env, ctx, allow_raise=False,
                                                  opaque=OpaqueRegistry())
    except Exception as e:
        return {"liftable": False, "blocker": "internal-error", "message": str(e),
               "line": facts.tree.lineno}
    if kind == "value":
        return {"liftable": True}
    return {"liftable": False, "blocker": "unsupported-construct",
           "line": failure["line"], "statement": failure["statement"],
           "message": failure["message"], "category": failure["category"]}

structural_complexity(fn)

Loop/branch/recursive-call counts, plus a complexity number in the spirit of cyclomatic complexity (decision points + 1: one per branch, one per loop) but with a heavier, depth-scaled charge for nested loops, the standard McCabe formula charges a flat point per loop regardless of nesting, which understates the real cost: a loop two levels deep is harder to reason about than one four levels wide and flat, and a loop three or four levels deep is a different order of difficulty again, not just "one more of the same thing." Each loop pays _NESTED_LOOP_PENALTY points per level of nesting it sits at (LoopFact.depth), so depth 1 costs 2 extra, depth 2 costs 4 extra, depth 3 costs 6 extra, and so on; deeper nesting is charged more, not the same, each additional level down. loops is the total loop count including nested ones; nested_loops is the subset of loops that sit inside another loop's body (depth > 0). recursive_calls counts self-call sites in the function's own body, not recursion depth or mutual recursion across multiple functions; true call-graph cycle detection across a codebase is a different, bigger feature, not attempted here. None if source wasn't available.

Source code in mathema/inventory.py

def structural_complexity(fn) -> dict | None:
    """Loop/branch/recursive-call counts, plus a complexity number in the
    spirit of cyclomatic complexity (decision points + 1: one per
    branch, one per loop) but with a heavier, depth-scaled charge for
    *nested* loops, the standard McCabe formula charges a flat point
    per loop regardless of nesting, which understates the real cost: a
    loop two levels deep is harder to reason about than one four levels
    wide and flat, and a loop three or four levels deep is a different
    order of difficulty again, not just "one more of the same thing."
    Each loop pays `_NESTED_LOOP_PENALTY` points per level of nesting it
    sits at (`LoopFact.depth`), so depth 1 costs 2 extra, depth 2 costs
    4 extra, depth 3 costs 6 extra, and so on; deeper nesting is
    charged more, not the same, each additional level down. `loops` is
    the total loop count including nested ones; `nested_loops` is the
    subset of `loops` that sit inside another loop's body (depth > 0).
    `recursive_calls` counts self-call *sites* in the function's own
    body, not recursion depth or mutual recursion across multiple
    functions; true call-graph cycle detection across a codebase is a
    different, bigger feature, not attempted here. `None` if source
    wasn't available."""
    import ast


    facts = quiet_facts(fn)
    if facts is None:
        return None
    if facts.tree is None:
        return None
    recursive_calls = sum(
        1 for node in ast.walk(facts.tree)
        if isinstance(node, ast.Call) and isinstance(node.func, ast.Name)
        and node.func.id == facts.name)
    branches, loops = facts.branch_count, len(facts.loops)
    nested_loops = sum(1 for loop in facts.loops if loop.depth > 0)
    nesting_penalty = _NESTED_LOOP_PENALTY * sum(loop.depth for loop in facts.loops)
    return {
        "branches": branches, "loops": loops, "nested_loops": nested_loops,
        "recursive_calls": recursive_calls,
        "cyclomatic": 1 + branches + loops + nesting_penalty,
    }

scope_dependencies(fn)

(global_vars, global_funcs, unresolved), names a function reads that aren't its own parameters/locals, split by what kind of dependency they actually are: global_vars are a genuine global variable dependency (real, if hidden, state, a claim about this function is only as reliable as that global's current value); global_funcs are an ordinary reference to a sibling function/ class/module (normal code structure, not a state dependency at all, a different error surface from global_vars, not the same one); unresolved have no binding mathema can find at all (likely a real bug, or a name only defined at call time). None if source wasn't retrievable. This is exactly what analyze_source() already warns about on every call, surfaced here as data instead of text, since a population sweep wants one row per function, not one interleaved warning per function.

Source code in mathema/inventory.py

def scope_dependencies(fn) -> tuple[list[str], list[str], list[str]] | None:
    """`(global_vars, global_funcs, unresolved)`, names a function
    reads that aren't its own parameters/locals, split by what kind of
    dependency they actually are: `global_vars` are a genuine global
    *variable* dependency (real, if hidden, state, a claim about this
    function is only as reliable as that global's current value);
    `global_funcs` are an ordinary reference to a sibling function/
    class/module (normal code structure, not a state dependency at all,
    a different error surface from `global_vars`, not the same one);
    `unresolved` have no binding mathema can find at all (likely a real
    bug, or a name only defined at call time). `None` if source wasn't
    retrievable. This is exactly what analyze_source() already warns
    about on every call, surfaced here as data instead of text, since
    a population sweep wants one row per function, not one interleaved
    warning per function."""


    facts = quiet_facts(fn)
    if facts is None:
        return None
    return facts.global_vars, facts.global_funcs, facts.unresolved

mutated_globals(fn)

Intent

Module-level names this function writes through, CACHE[k] = v, CONFIG.field = x, rather than merely reads. None if the source wasn't retrievable.

Notes

Deliberately separate from scope_dependencies' global_vars, which reports names a function depends on. Writing is the stronger relationship: it makes this function the reason some other caller's answer changed. A name appears here and not in global_vars when the function only ever writes it.

Source code in mathema/inventory.py

def mutated_globals(fn) -> list[str] | None:
    """Intent:
        Module-level names this function *writes through*, `CACHE[k] = v`,
        `CONFIG.field = x`, rather than merely reads. `None` if the
        source wasn't retrievable.

    Notes:
        Deliberately separate from `scope_dependencies`' `global_vars`,
        which reports names a function *depends on*. Writing is the
        stronger relationship: it makes this function the reason some
        other caller's answer changed. A name appears here and not in
        `global_vars` when the function only ever writes it.
    """
    facts = quiet_facts(fn)
    if facts is None:
        return None
    return facts.mutated_globals

typing_info(fn)

How much of the signature actually carries type hints, params annotated vs total, and whether the return type is. A cheap signal on its own (an untyped parameter is exactly where mathema has least to go on inferring anything), and the prerequisite for a richer one: a bare str parameter carries none of a proper Literal[...]/ Enum hint's finite-value information. finite_domains is populated whenever a parameter's own type hint already states its entire meaningful value set, exactly the shape lift_conditioned()'s branch pruning needs, read directly from the signature rather than requiring a claim to redeclare it.

Source code in mathema/inventory.py

def typing_info(fn) -> dict:
    """How much of the signature actually carries type hints, params
    annotated vs total, and whether the return type is. A cheap signal
    on its own (an untyped parameter is exactly where mathema has least
    to go on inferring anything), and the prerequisite for a richer one:
    a bare `str` parameter carries none of a proper `Literal[...]`/
    `Enum` hint's finite-value information. `finite_domains` is
    populated whenever a parameter's own type hint already states its
    entire meaningful value set, exactly the shape `lift_conditioned()`'s
    branch pruning needs, read directly from the signature rather than
    requiring a claim to redeclare it."""
    import inspect

    from .analysis import finite_annotation_domains

    try:
        sig = callable_signature(fn)
    except (TypeError, ValueError):
        return {"params_typed": 0, "params_total": 0, "return_typed": None,
                "finite_domains": {}}
    params = list(sig.parameters.values())
    typed = sum(1 for p in params
                if p.annotation is not inspect.Parameter.empty)
    finite_domains = finite_annotation_domains(fn)
    return_typed = sig.return_annotation is not inspect.Signature.empty
    return {"params_typed": typed, "params_total": len(params),
            "return_typed": return_typed, "finite_domains": finite_domains}

wrapped_target(fn)

Is this function's body exactly one statement; return <call>(...), a thin pass-through with no real computation of its own (a docstring beforehand doesn't disqualify it, same convention lift() already uses)? If so, a best-effort name for what it calls: module.qualname when the callable can be resolved (a bare-name call resolved against fn's own globals, or an attribute call resolved against whatever object its root name is bound to, np.sqrt resolves through the real np module object, not by guessing), else just the name as written (self.helper, foo) when it can't be. None if the body isn't exactly this shape.

Source code in mathema/inventory.py

def wrapped_target(fn) -> str | None:
    """Is this function's body exactly one statement; `return
    <call>(...)`, a thin pass-through with no real computation of its
    own (a docstring beforehand doesn't disqualify it, same convention
    lift() already uses)? If so, a best-effort name for what it calls:
    `module.qualname` when the callable can be resolved (a bare-name
    call resolved against fn's own globals, or an attribute call
    resolved against whatever object its root name is bound to,
    `np.sqrt` resolves through the real `np` module object, not by
    guessing), else just the name as written (`self.helper`, `foo`)
    when it can't be. `None` if the body isn't exactly this shape."""


    facts = quiet_facts(fn)
    if facts is None:
        return None
    if facts.tree is None:
        return None
    body = facts.tree.body
    if body and isinstance(body[0], ast.Expr) and isinstance(body[0].value, ast.Constant) \
            and isinstance(body[0].value.value, str):
        body = body[1:]
    if len(body) != 1 or not isinstance(body[0], ast.Return) or body[0].value is None:
        return None
    call = body[0].value
    if not isinstance(call, ast.Call):
        return None

    g = module_scope(fn)

    def resolved_name(obj, fallback: str) -> str:
        mod = getattr(obj, "__module__", None)
        qn = getattr(obj, "__qualname__", None)
        return f"{mod}.{qn}" if mod and qn else fallback

    if isinstance(call.func, ast.Name):
        name = call.func.id
        return resolved_name(g[name], name) if name in g else name
    if isinstance(call.func, ast.Attribute):
        attr, base = call.func.attr, call.func.value
        if isinstance(base, ast.Name) and base.id in ("self", "cls"):
            return f"{base.id}.{attr}"   # not resolvable without an instance/class
        if isinstance(base, ast.Name) and base.id in g:
            target = getattr(g[base.id], attr, None)
            if target is not None:
                return resolved_name(target, attr)
        return attr
    return None

docstring_quality(fn)

A best-practice checklist, not a style grade, has a docstring at all, has a real summary (non-empty text before the first recognized section header, either convention), documents its parameters (each real parameter's name found literally somewhere in the docstring, a presence heuristic, not true cross-referencing), documents what it returns (only applicable if it actually returns something, analyze_source()'s own returns_kind, so a function returning None is never penalized for not documenting a return value it doesn't have), documents raising (only applicable if the body actually raises at least one exception with a resolvable type name; see _raised_exception_names(); passing requires both a Raises/ Exceptions section AND every one of those exception names mentioned in it by name, not just the section existing). score/applicable let a caller compute "N/M" without redefining what counts, applicable shrinks when a criterion genuinely doesn't apply (no params, no raise, no return value), rather than counting it as a failure.

Source code in mathema/inventory.py

def docstring_quality(fn) -> dict:
    """A best-practice checklist, not a style grade, has a docstring at
    all, has a real summary (non-empty text before the first recognized
    section header, either convention), documents its parameters (each
    real parameter's name found literally somewhere in the docstring,
    a presence heuristic, not true cross-referencing), documents what it
    returns (only applicable if it actually returns something,
    analyze_source()'s own returns_kind, so a function returning None is
    never penalized for not documenting a return value it doesn't have),
    documents raising (only applicable if the body actually raises at
    least one exception with a resolvable type name; see
    `_raised_exception_names()`; passing requires both a Raises/
    Exceptions section AND every one of those exception names mentioned
    in it by name, not just the section existing). `score`/`applicable`
    let a caller compute "N/M" without redefining what counts,
    `applicable` shrinks when a criterion genuinely doesn't apply (no
    params, no raise, no return value), rather than counting it as a
    failure."""


    facts = quiet_facts(fn)
    if facts is None:
        # no facts.docstring to fall back on, best-effort raw
        # __doc__, which is unindented for a top-level function
        # anyway (indentation only matters for a method/nested
        # function's docstring, exactly the case source access just
        # failed for)
        doc = getattr(fn, "__doc__", None) or ""
        has_doc = bool(doc.strip())
        has_summary = has_doc and bool(_DOC_HEADER_GOOGLE.split(doc)[0].strip())
        return {"has_docstring": has_doc, "has_summary": has_summary,
                "params_documented": None, "params_total": None,
                "documents_return": None, "documents_raises": None,
                "raises_documented": None, "raises_total": None,
                "score": int(has_doc) + int(has_summary),
                "applicable": 1 + int(has_doc)}

    # facts.docstring is ast.get_docstring()'s output, dedented
    # consistently regardless of the function's own source indentation,
    # unlike raw fn.__doc__. _sections()'s numpydoc header regex requires
    # exactly that (`^Parameters` at column 0), so raw __doc__ on an
    # indented method's docstring would silently never match a single
    # section, even a real one.
    doc = facts.docstring or ""
    has_doc = bool(doc.strip())
    lead_text = _DOC_HEADER_GOOGLE.split(doc)[0]
    numpy_sections = set(_sections(doc))
    if numpy_sections:
        # _sections() already strips everything from the first numpydoc
        # header onward out of its own accounting; mirror that here too
        first_numpy_header = re.search(r"^(\w[\w ]*)\n\s*-{3,}\s*$", doc, re.M)
        if first_numpy_header and first_numpy_header.start() < len(lead_text):
            lead_text = doc[:first_numpy_header.start()]
    has_summary = has_doc and bool(lead_text.strip())

    google_headers = {m.group(1) for m in _DOC_HEADER_GOOGLE.finditer(doc)}

    def has_section(*names):
        return (any(n.lower() in numpy_sections for n in names)
               or any(n in google_headers for n in names))

    result: dict[str, object] = {
        "has_docstring": has_doc, "has_summary": has_summary,
        "params_documented": None, "params_total": None,
        "documents_return": None, "documents_raises": None,
        "raises_documented": None, "raises_total": None,
    }
    score, applicable = int(has_doc), 1
    if has_doc:
        score += int(has_summary)
        applicable += 1

    # Scored per parameter/exception, not as one all-or-nothing point,
    # a function with 3 params and 2 documented is 2/3 of the way there,
    # not the same 0/1 as a function with none documented at all; the
    # overall score/applicable should reflect that granularity, the same
    # granularity params_documented/params_total and raises_documented/
    # raises_total already report individually.
    real_params = [p for p in facts.params if p not in ("self", "cls")]
    documented = sum(1 for p in real_params if re.search(rf"\b{re.escape(p)}\b", doc))
    result["params_documented"], result["params_total"] = documented, len(real_params)
    if real_params:
        score += documented
        applicable += len(real_params)

    raised = _raised_exception_names(facts.tree) if facts.tree is not None else []
    if raised:
        raises_doc = has_section("Raises", "Exceptions")
        mentioned = sum(1 for name in raised if re.search(rf"\b{re.escape(name)}\b", doc))
        result["raises_documented"], result["raises_total"] = mentioned, len(raised)
        result["documents_raises"] = raises_doc and mentioned == len(raised)
        score += mentioned
        applicable += len(raised)

    returns_something = facts.returns_kind not in ("none", "unknown")
    if returns_something:
        documents_return = has_section("Returns", "Yields")
        result["documents_return"] = documents_return
        score += int(documents_return)
        applicable += 1

    # Not scored alongside the prose checks above; this is mathema's
    # own claim-authoring surface (authoring.py's "Claims:" docstring
    # block), checked with its own real parser rather than a presence
    # regex, so it can catch a real, easy-to-hit authoring mistake: a
    # claim line missing its `name:` prefix parses to zero claims
    # silently, so a Claims: header can be present with nothing valid
    # actually parsed out of it; a prose-based heuristic could never
    # see that gap.
    from .authoring import parse_docstring_claims

    has_claims_header = bool(re.search(r"^\s*claims:\s*$", doc, re.I | re.M))
    claims_parsed = len(parse_docstring_claims(doc)) if has_claims_header else 0
    result["has_claims_block"] = has_claims_header
    result["claims_parsed"] = claims_parsed if has_claims_header else None

    result.update(score=score, applicable=applicable)
    return result

docs_checklist(q)

docstring_quality()'s result as checkbox-style lines (✓/✗, · for informational-only); one shared renderer so mathema.DocstringReport.__repr__ and mathema audit --docs-only can't drift apart on what a checkmark means. No leading indentation; callers indent as their own context needs.

Source code in mathema/inventory.py

def docs_checklist(q: dict) -> list[str]:
    """`docstring_quality()`'s result as checkbox-style lines (✓/✗, `·`
    for informational-only); one shared renderer so
    `mathema.DocstringReport.__repr__` and `mathema audit --docs-only`
    can't drift apart on what a checkmark means. No leading indentation;
    callers indent as their own context needs."""
    def mark(ok):
        return "✓" if ok else ("·" if ok is None else "✗")

    lines = [f"{mark(q['has_docstring'])} has a docstring"]
    if q["has_docstring"]:
        lines.append(f"{mark(q['has_summary'])} has a summary")
    if q["params_total"]:
        lines.append(f"{mark(q['params_documented'] == q['params_total'])} "
                     f"params documented ({q['params_documented']}/{q['params_total']})")
    if q["documents_return"] is not None:
        lines.append(f"{mark(q['documents_return'])} documents its return value")
    if q["raises_total"]:
        lines.append(f"{mark(q['documents_raises'])} exceptions documented "
                     f"({q['raises_documented']}/{q['raises_total']})")
    if q.get("has_claims_block"):
        lines.append(f"· Claims: block present ({q['claims_parsed']} parsed)")
    return lines

is_test_covered(fn, coverage_data)

None means unknown (no coverage report found, this function's file wasn't in it, or fn stands for a function another frontend read, whose coverage is not in a Python report), never conflate that with False.

Source code in mathema/inventory.py

def is_test_covered(fn, coverage_data: dict[str, set[int]] | None) -> bool | None:
    """`None` means unknown (no coverage report found, this function's
    file wasn't in it, or `fn` stands for a function another frontend
    read, whose coverage is not in a Python report), never conflate that
    with False."""
    from .analysis import foreign_body
    if coverage_data is None or foreign_body(fn):
        return None
    try:
        src_file = inspect.getsourcefile(fn)
        lines, start = inspect.getsourcelines(fn)
    except (TypeError, OSError):
        return None
    if src_file is None:
        return None
    executed = coverage_data.get(os.path.abspath(src_file))
    if executed is None:
        return None
    end = start + len(lines) - 1
    return any(start <= ln <= end for ln in executed)

read_test_coverage(root='.')

Best-effort executed-line-numbers-per-file, from an existing coverage.py report; this never runs the target's tests itself. Tries coverage.json (coverage.py's own coverage json export) first, since that needs no import of the coverage package at all; falls back to a native .coverage data file if coverage happens to be importable. None (not {}) if neither is available or readable; callers must treat that as "unknown", not "nothing was covered".

Source code in mathema/inventory.py

def read_test_coverage(root: str = ".") -> dict[str, set[int]] | None:
    """Best-effort executed-line-numbers-per-file, from an *existing*
    coverage.py report; this never runs the target's tests itself.
    Tries `coverage.json` (coverage.py's own `coverage json` export)
    first, since that needs no import of the `coverage` package at all;
    falls back to a native `.coverage` data file if `coverage` happens
    to be importable. `None` (not `{}`) if neither is available or
    readable; callers must treat that as "unknown", not "nothing was
    covered"."""
    json_path = os.path.join(root, "coverage.json")
    if os.path.exists(json_path):
        import json
        with open(json_path) as fh:
            data = json.load(fh)
        return {os.path.abspath(os.path.join(root, f)): set(info.get("executed_lines", []))
                for f, info in data.get("files", {}).items()}
    cov_path = os.path.join(root, ".coverage")
    if os.path.exists(cov_path):
        try:
            import coverage
        except ImportError:
            return None
        cov = coverage.Coverage(data_file=cov_path)
        try:
            cov.load()
        except Exception:
            return None
        out = {}
        for f in cov.get_data().measured_files():
            try:
                # analysis2() is a 5-tuple (file, statements, excluded,
                # missing, readable); the lines actually RUN are the
                # statements minus the ones missing from execution, the
                # same `executed_lines` sense the JSON path above reads.
                _, statements, _, missing, _ = cov.analysis2(f)
            except Exception:
                continue
            out[os.path.abspath(f)] = set(statements) - set(missing)
        return out
    return None

suggest_coverage_command(root='.')

Best-effort: does this project look like it uses pytest? If so, the command that would produce the coverage.json report read_test_coverage() already knows how to read, never runs it, only detects whether suggesting it makes sense. None if nothing pytest-shaped is found, no guess is better than a wrong one for a project that uses something else entirely. The export runs whatever the test run's exit status: a failing test still leaves the lines every other test executed.

Uses python -m coverage/python -m pytest, not the bare coverage/ pytest console scripts; those aren't guaranteed to be on PATH even when the packages themselves are installed. Checks whether coverage is actually importable in this process first (mathema is expected to run in the same venv as the target project, per the walkthrough) and prepends an install step if not, a suggested command that fails with "command not found" is worse than no suggestion.

Source code in mathema/inventory.py

def suggest_coverage_command(root: str = ".") -> str | None:
    """Best-effort: does this project look like it uses pytest? If so,
    the command that would produce the coverage.json report
    read_test_coverage() already knows how to read, never runs it,
    only detects whether suggesting it makes sense. `None` if nothing
    pytest-shaped is found, no guess is better than a wrong one for a
    project that uses something else entirely. The export runs whatever
    the test run's exit status: a failing test still leaves the lines
    every other test executed.

    Uses `python -m coverage`/`python -m pytest`, not the bare `coverage`/
    `pytest` console scripts; those aren't guaranteed to be on PATH even
    when the packages themselves are installed. Checks whether `coverage`
    is actually importable in *this* process first (mathema is expected
    to run in the same venv as the target project, per the walkthrough)
    and prepends an install step if not, a suggested command that
    fails with "command not found" is worse than no suggestion."""
    import importlib.util

    pytest_shaped = (
        os.path.isdir(os.path.join(root, "tests"))
        or os.path.isdir(os.path.join(root, "test")))
    if not pytest_shaped:
        for cfg in ("pyproject.toml", "setup.cfg", "pytest.ini", "tox.ini"):
            path = os.path.join(root, cfg)
            if not os.path.exists(path):
                continue
            try:
                content = open(path).read()
            except OSError:
                continue
            if "pytest" in content:
                pytest_shaped = True
                break
    if not pytest_shaped:
        return None
    cmd = "python -m coverage run -m pytest; python -m coverage json"
    if importlib.util.find_spec("coverage") is None:
        cmd = "pip install coverage && " + cmd
    return cmd

mathema.types

mathema.types

Semantic type markers: attach a typing.Annotated marker to a parameter or return type, and mathema infers a standard claim automatically, a fourth claim-authoring surface, alongside the file/ decorator/docstring ones in authoring.py, except inferred rather than explicitly stated.

from typing import Annotated
from mathema.types import Probability, Shape

def bayes_update(prior: Annotated[float, Probability],
                 likelihood: Annotated[float, Probability]) -> Annotated[float, Probability]:
    ...

def matmul(a: Annotated[list, Shape("m", "n")],
          b: Annotated[list, Shape("n", "p")]) -> Annotated[list, Shape("m", "p")]:
    ...

Markers are deliberately general mathematics only, matching the domain-specific-goes-outside boundary drawn in 05-pushing-derive-further.md: Probability/Positive/Shape are math, not a business vertical (a StockPrice marker would not belong here).

Domain markers (Probability/Positive/Nonnegative) fold into an ordinary domain-scoped claim, reusing check()'s existing domain= mechanism. Shape is structural, not algebraic; it can't be expressed in the scalar claim-law grammar (there is no index quantifier over a variable- length structure), so it's checked the way probing.py already checks monotone/is_numerically_stable: a bespoke Python probe, not a parsed law string. Precedence-wise this surface is the lowest of the four: a human writing a decorator or docstring claim is a more deliberate statement than an incidentally-implied one from a type hint, so a same-named explicit claim from any other surface overrides an inferred one (see authoring.declared_from_function, which does not consult this module; type inference is folded in one level further out, in type_probes(), so it never competes with an ordinary claim name).

Probability dataclass

Value in [0, 1].

Source code in mathema/types.py

@dataclass(frozen=True)
class Probability:
    """Value in [0, 1]."""

Positive dataclass

Value > 0.

Source code in mathema/types.py

@dataclass(frozen=True)
class Positive:
    """Value > 0."""

Nonnegative dataclass

Value >= 0.

Source code in mathema/types.py

@dataclass(frozen=True)
class Nonnegative:
    """Value >= 0."""

Shape dataclass

Expected outer dimensions of a nested-list "matrix"/"vector" value: concrete ints or symbolic dimension-name strings shared across the signature (Shape("m", "n") on one parameter and Shape("n", "p") on another means both must agree on the size bound to "n" within a trial). 1-D: Shape("n"); 2-D: Shape("m", "n").

Source code in mathema/types.py

@dataclass(frozen=True)
class Shape:
    """Expected outer dimensions of a nested-list "matrix"/"vector"
    value: concrete ints or symbolic dimension-name strings shared across
    the signature (`Shape("m", "n")` on one parameter and `Shape("n",
    "p")` on another means both must agree on the size bound to "n"
    within a trial). 1-D: `Shape("n")`; 2-D: `Shape("m", "n")`."""
    dims: tuple = field(default_factory=tuple)

    def __init__(self, *dims):
        object.__setattr__(self, "dims", dims)

mathema.runtime_types

mathema.runtime_types

Runtime types: what a library hands a function as a vector, a matrix or a table (a list, a numpy.ndarray, a pandas.Series or DataFrame, a polars.Series or DataFrame), and the runtime type adapters that realise mathema's abstract values as them.

A claim's sampler draws an abstract value (today still spelled as a plain list or a list of lists); before each call of the function, the parameter's runtime type adapter realises it as the object the function expects, and what the function returns is observed back into a plain value before anything compares it. A parameter's runtime type is read from the function's signature only:

1. a marker, Vec("n", runtime="pandas.Series") or Mat(..., runtime=);
2. the live annotation (typing.get_type_hints): np.ndarray, npt.NDArray[...], pd.Series, pd.DataFrame, pl.Series, pl.DataFrame; a union gives one detection per member and the first is sampled;
3. the annotation's source text, when the hints do not resolve;
4. for code that cannot be annotated, a claims-file entry's runtime_types: {param: pandas.Series}.

A parameter no adapter claims is sampled as a list, exactly as before. Adapters beyond the built-ins register under the entry-point group mathema.runtime_types; a built-in wins a name clash, and an adapter that fails to load is skipped with a warning.

RuntimeTypeAdapter

Bases: Protocol

What a runtime type adapter provides.

name is the runtime type's dotted name ("pandas.Series"), kinds the abstract kinds it carries, requires the modules that must be importable for it to be used. detect(annotation) reads one annotation, a live type or its source text, and returns a Detection or None. realise(abstract, options) builds the object passed to the function from an abstract value. observe(obj) turns a returned object into an abstract value or a plain number, or returns NotMine for an object that is not its runtime type. An adapter may also state ALIASES, the module aliases its library is usually imported under ({"pd": "pandas"}), through which an annotation's source text is read, and USES, a BodyUses naming the uses of an unannotated parameter only its type supports, by which such a parameter is drawn as its type in a module that imports its library.

Source code in mathema/runtime_types/_adapters.py

@runtime_checkable
class RuntimeTypeAdapter(Protocol):
    """What a runtime type adapter provides.

    `name` is the runtime type's dotted name (`"pandas.Series"`),
    `kinds` the abstract kinds it carries, `requires` the modules that
    must be importable for it to be used. `detect(annotation)` reads
    one annotation, a live type or its source text, and returns a
    `Detection` or None. `realise(abstract, options)` builds the object
    passed to the function from an abstract value. `observe(obj)`
    turns a returned object into an abstract value or a plain number,
    or returns `NotMine` for an object that is not its runtime type.
    An adapter may also state `ALIASES`, the module aliases its
    library is usually imported under (`{"pd": "pandas"}`), through
    which an annotation's source text is read, and `USES`, a
    `BodyUses` naming the uses of an unannotated parameter only its
    type supports, by which such a parameter is drawn as its type in a
    module that imports its library.
    """
    name: str
    kinds: frozenset
    requires: tuple

    def detect(self, annotation) -> "Detection | None": ...

    def realise(self, abstract, options: dict) -> Any: ...

    def observe(self, obj) -> Any: ...

Detection dataclass

An adapter's claim on a parameter: the adapter's name, the kind of abstract value the parameter carries (vec, mat or table), and the evidence, stated as the record states it ("annotation: pandas.Series").

Source code in mathema/runtime_types/_adapters.py

@dataclass(frozen=True)
class Detection:
    """An adapter's claim on a parameter: the adapter's name, the kind
    of abstract value the parameter carries (`vec`, `mat` or `table`),
    and the evidence, stated as the record states it
    (`"annotation: pandas.Series"`)."""
    adapter: str
    kind: str
    evidence: str

AbstractVec dataclass

A vector of len(values) numbers, strings or booleans, with missing the positions that hold no value and spelling the member they are held as (nan, null, NA), None for the runtime type's own default; members the member each missing position holds, ((position, member), ...), when they are not all one. The value stored at a missing position is NaN and carries no meaning. labels names each position when the vector is indexed by name (a pandas Series labelled by column names, as a table's reduction answers), () when its positions carry no names. element is the type of its elements, one of ELEMENT_TYPES, when it was drawn or returned as that type; None when the values say it (element_type). A vector of strings or booleans holds them in values as they are.

Source code in mathema/runtime_types/_abstract.py

@dataclass(frozen=True)
class AbstractVec:
    """A vector of `len(values)` numbers, strings or booleans, with
    `missing` the positions that hold no value and `spelling` the
    member they are held as (`nan`, `null`, `NA`), None for the runtime
    type's own default; `members` the member each missing position
    holds, `((position, member), ...)`, when they are not all one. The
    value stored at a missing position is NaN and carries no meaning.
    `labels` names
    each position when the vector is indexed by name (a pandas Series
    labelled by column names, as a table's reduction answers), `()`
    when its positions carry no names. `element` is the type of its
    elements, one of `ELEMENT_TYPES`, when it was drawn or returned as
    that type; None when the values say it (`element_type`). A vector
    of strings or booleans holds them in `values` as they are."""
    values: tuple
    missing: frozenset = frozenset()
    spelling: "str | None" = None
    members: tuple = ()
    labels: tuple = ()
    element: "str | None" = None

    def __len__(self) -> int:
        return len(self.values)

    def non_missing(self) -> tuple:
        """The values at the positions that are not missing, in order."""
        return tuple(v for k, v in enumerate(self.values)
                     if k not in self.missing)

non_missing()

The values at the positions that are not missing, in order.

Source code in mathema/runtime_types/_abstract.py

def non_missing(self) -> tuple:
    """The values at the positions that are not missing, in order."""
    return tuple(v for k, v in enumerate(self.values)
                 if k not in self.missing)

AbstractMat dataclass

A matrix as a tuple of equal-length rows of numbers, with missing the (row, column) positions that hold no value (NaN in rows) and spelling the member they are held as, or members per position when they are not all one.

Source code in mathema/runtime_types/_abstract.py

@dataclass(frozen=True)
class AbstractMat:
    """A matrix as a tuple of equal-length rows of numbers, with
    `missing` the `(row, column)` positions that hold no value (NaN in
    `rows`) and `spelling` the member they are held as, or `members`
    per position when they are not all one."""
    rows: tuple
    missing: frozenset = frozenset()
    spelling: "str | None" = None
    members: tuple = ()

    @property
    def shape(self) -> tuple:
        return (len(self.rows), len(self.rows[0]) if self.rows else 0)

AbstractTable dataclass

Named columns of equal length, each an AbstractVec, in order. column_names, column_types, column and row_count read it whatever runtime type it was realised as or observed from.

Source code in mathema/runtime_types/_abstract.py

@dataclass(frozen=True)
class AbstractTable:
    """Named columns of equal length, each an `AbstractVec`, in order.
    `column_names`, `column_types`, `column` and `row_count` read it
    whatever runtime type it was realised as or observed from."""
    columns: dict = field(default_factory=dict)

    def __hash__(self) -> int:
        return hash(tuple(self.columns.items()))

    def column_names(self) -> tuple:
        """The column names, in order."""
        return tuple(self.columns)

    def column_types(self) -> dict:
        """`{name: type}`, each column's `element_type`, in order."""
        return {name: element_type(col) for name, col in self.columns.items()}

    def column(self, name: str) -> AbstractVec:
        """Intent:
            The column called `name`.

        Raises:
            KeyError: the table has no such column; the message names
                the columns it has.
        """
        try:
            return self.columns[name]
        except KeyError:
            raise KeyError(f"the table has no column {name!r} (columns: "
                           f"{', '.join(self.columns) or 'none'})") from None

    def row_count(self) -> int:
        """The number of rows: the length of its columns, 0 with none."""
        return len(next(iter(self.columns.values()))) if self.columns else 0

column(name)

Intent

The column called name.

Raises:

Type	Description
KeyError	the table has no such column; the message names the columns it has.

Source code in mathema/runtime_types/_abstract.py

def column(self, name: str) -> AbstractVec:
    """Intent:
        The column called `name`.

    Raises:
        KeyError: the table has no such column; the message names
            the columns it has.
    """
    try:
        return self.columns[name]
    except KeyError:
        raise KeyError(f"the table has no column {name!r} (columns: "
                       f"{', '.join(self.columns) or 'none'})") from None

column_names()

The column names, in order.

Source code in mathema/runtime_types/_abstract.py

def column_names(self) -> tuple:
    """The column names, in order."""
    return tuple(self.columns)

column_types()

{name: type}, each column's element_type, in order.

Source code in mathema/runtime_types/_abstract.py

def column_types(self) -> dict:
    """`{name: type}`, each column's `element_type`, in order."""
    return {name: element_type(col) for name, col in self.columns.items()}

row_count()

The number of rows: the length of its columns, 0 with none.

Source code in mathema/runtime_types/_abstract.py

def row_count(self) -> int:
    """The number of rows: the length of its columns, 0 with none."""
    return len(next(iter(self.columns.values()))) if self.columns else 0

RuntimeType dataclass

The marker Vec(..., runtime=...) and Mat(..., runtime=...) attach: the parameter's runtime type, by its dotted name ("pandas.Series").

Source code in mathema/runtime_types/__init__.py

@dataclass(frozen=True)
class RuntimeType:
    """The marker `Vec(..., runtime=...)` and `Mat(..., runtime=...)`
    attach: the parameter's runtime type, by its dotted name
    (`"pandas.Series"`)."""
    name: str

adapters()

Every runtime type adapter by name, in detection order: the built-ins (the list adapter last), then any registered under mathema.runtime_types whose name no built-in uses, placed before the list adapter.

Source code in mathema/runtime_types/__init__.py

def adapters() -> dict:
    """Every runtime type adapter by name, in detection order: the
    built-ins (the list adapter last), then any registered under
    `mathema.runtime_types` whose name no built-in uses, placed before
    the list adapter."""
    builtin = {a.name: a for a in BUILTIN_ADAPTERS}
    external: dict = {}
    for a in _discovered():
        name = getattr(a, "name", None)
        if not isinstance(name, str) or not isinstance(a, RuntimeTypeAdapter):
            warnings.warn(f"mathema: runtime type adapter {a!r} does not "
                          f"provide name, kinds, requires, detect, "
                          f"realise and observe, skipping it",
                          stacklevel=2)
            continue
        if name in builtin:
            warnings.warn(f"mathema: external runtime type adapter "
                          f"{name!r} ignored because a built-in adapter "
                          f"already uses that name", stacklevel=2)
            continue
        external.setdefault(name, a)
    ordered = {n: a for n, a in builtin.items() if n != ListAdapter.name}
    ordered.update(external)
    ordered[ListAdapter.name] = builtin[ListAdapter.name]
    return ordered

detect_parameters(fn, declared=None)

Intent: Each parameter's runtime type detections, from the signature only, as {param: (Detection, ...)}: a RuntimeType marker first, then the live annotation, then the annotation's source text when the hints do not resolve, and for a parameter the signature says nothing about, declared (a claims-file entry's runtime_types: {param: name}). A parameter nothing names is absent.

Source code in mathema/runtime_types/__init__.py

def detect_parameters(fn, declared: "dict | None" = None) -> dict:
    """Intent:
        Each parameter's runtime type detections, from the signature
        only, as `{param: (Detection, ...)}`: a `RuntimeType` marker
        first, then the live annotation, then the annotation's source
        text when the hints do not resolve, and for a parameter the
        signature says nothing about, `declared` (a claims-file entry's
        `runtime_types: {param: name}`). A parameter nothing names is
        absent.
    """
    sig = _signature(fn)
    if sig is None:
        return {}
    scope = module_scope(fn)
    try:
        hints = typing.get_type_hints(fn, include_extras=True)
    except Exception:
        hints = {}
    out: dict = {}
    owner = _owning_class(fn)
    for index, (p, param) in enumerate(sig.parameters.items()):
        found: list = []
        live = hints.get(p)
        raw = param.annotation
        if (index == 0 and p == "self" and owner is not None and live is None
                and raw is inspect.Parameter.empty):
            # an unbound method's self is an instance of its own class
            live = owner
        if live is None and isinstance(raw, str):
            try:
                live = eval(raw, dict(scope))   # noqa: S307
            except Exception:
                live = None
        if live is None and raw is not inspect.Parameter.empty \
                and not isinstance(raw, str):
            live = raw
        marker = _marker_of(live) if live is not None else None
        if marker is not None:
            named = adapter(marker.name)
            if named is not None and installed(named):
                found = [Detection(named.name, _marker_kind(live, named),
                                   f"marker: {named.name}")]
        elif live is not None:
            found = detect_annotation(live, scope)
        elif isinstance(raw, str):
            found = detect_annotation(raw, scope)
        if not found and (declared or {}).get(p):
            named = adapter(str(declared[p]))
            if named is not None and installed(named):
                kind = "table" if named.kinds == frozenset({"table"}) \
                    else "vec"
                found = [Detection(named.name, kind,
                                   f"claims file: {named.name}")]
        if found:
            out[p] = tuple(found)
    return out

realise(value, detection, options=None, declared=None)

Intent: value (a drawn plain value) as the object the detection's runtime type carries, or value unchanged when it is not a vector, matrix or table the adapter carries (a scalar, a value already of the runtime type). declared states the element type the claim binds where the values may not show it: {"element": "str"} for a vector, {"columns": {"k": "str"}} for a table's columns; a vector or column whose own values state no type (holes only, or no rows) takes it.

Source code in mathema/runtime_types/__init__.py

def realise(value, detection: Detection, options: "dict | None" = None,
            declared: "dict | None" = None):
    """Intent:
        `value` (a drawn plain value) as the object the detection's
        runtime type carries, or `value` unchanged when it is not a
        vector, matrix or table the adapter carries (a scalar, a value
        already of the runtime type). `declared` states the element
        type the claim binds where the values may not show it:
        `{"element": "str"}` for a vector, `{"columns": {"k": "str"}}`
        for a table's columns; a vector or column whose own values
        state no type (holes only, or no rows) takes it.
    """
    found = adapter(detection.adapter)
    if found is None:
        return value
    abstract = abstract_of(value)
    if abstract is None:
        return value
    abstract = _with_declared(abstract, declared or {})
    kind = ("mat" if isinstance(abstract, AbstractMat) else
            "table" if isinstance(abstract, AbstractTable) else "vec")
    if kind not in found.kinds:
        return value
    return found.realise(abstract, dict(options or {}))

observe(obj)

Intent: What a function returned, as an abstract value or a plain number: the first installed adapter whose observe recognises it answers, the list adapter last. An object no adapter recognises is returned unchanged.

Source code in mathema/runtime_types/__init__.py

def observe(obj):
    """Intent:
        What a function returned, as an abstract value or a plain
        number: the first installed adapter whose `observe` recognises
        it answers, the list adapter last. An object no adapter
        recognises is returned unchanged.
    """
    for found in adapters().values():
        if found.name == ListAdapter.name or not installed(found):
            continue
        if _root_module_of(obj) not in (*found.requires, "builtins") \
                and found.requires:
            continue
        try:
            seen = found.observe(obj)
        except Exception:
            continue
        if seen is not NotMine:
            return seen
    return obj

mathema.identity

mathema.identity

Identity: the two Mathema hashes.

form ; how it's written: rename/format-invariant structural hash (locals and parameters replaced by binding-order names). sig ; the coarsest facet of meaning: the typed shape of the transformation.

Line-anchored artifacts bind to form; everything else binds to meaning (signature + lifted normal form, when available).

form_hash(fdef)

The form identity, py:<sha>: the Python frontend's namespace and a 12-hex-char hash of the function's alpha-normalized AST (normalized(), locals/parameters replaced by binding-order names, so a pure rename doesn't change it, but any real structural change does), rendered by form_text so the hash is the same on every supported Python.

Source code in mathema/identity.py

def form_hash(fdef: ast.FunctionDef | ast.AsyncFunctionDef) -> str:
    """The `form` identity, `py:<sha>`: the Python frontend's namespace
    and a 12-hex-char hash of the function's alpha-normalized AST
    (`normalized()`, locals/parameters replaced by binding-order names,
    so a pure rename doesn't change it, but any real structural change
    does), rendered by `form_text` so the hash is the same on every
    supported Python."""
    digest = hashlib.sha256(form_text(normalized(fdef)).encode()).hexdigest()[:12]
    return f"{PYTHON_FORM_NAMESPACE}:{digest}"

mathema.compiled

mathema.compiled

Executable closed forms: a sympy expression compiled back into a runnable callable, with the provenance and domain-validity facts that make evidence from running it honest.

A compiled form is mathema's RECONSTRUCTION of some mathematics, a lifted function body, a rewrite-gallery form, the resolved intermediate of a stalled proof, never the user's own code. Numeric evidence from evaluating one is evidence about the symbolic form, and only transitively (through the lift) about any code it came from, so every consumer states that provenance: the numeric-fallback route is probe:lifted_numeric, its ceiling is holds, and the record names the form that was actually sampled.

A compiled form evaluates; it does not print. Nothing here emits source code.

CompiledForm dataclass

One executable closed form: the expression, the callable compiled from it, the ordered free-variable names the callable takes, where the form came from (provenance, e.g. the rewrites applied), the conditions under which it is a valid rendering of its origin (validity), and the numeric backend that runs it.

Source code in mathema/compiled.py

@dataclass(frozen=True)
class CompiledForm:
    """One executable closed form: the expression, the callable
    compiled from it, the ordered free-variable names the callable
    takes, where the form came from (`provenance`, e.g. the rewrites
    applied), the conditions under which it is a valid rendering of its
    origin (`validity`), and the numeric backend that runs it."""
    expr: "sympy.Expr"
    fn: "Callable"
    names: tuple
    provenance: tuple = ()
    validity: str = ""
    backend: str = "math"

compile_form(expr, names=None, provenance=(), validity='', backend='math', pseudo_infinity=None)

Intent

Lambdify expr over names (defaulting to its sorted free symbols) into a CompiledForm, or None when the expression contains something the backend cannot run (an unevaluated Integral under the plain math backend, an unmapped special function).

Notes

pseudo_infinity is the claim's resolved (lo, hi) operational infinity (records.pseudo_infinity_range). An unevaluated Integral with an infinite bound is read at that range, the same empirical reading of infinity every other consumer of a let |inf| be v binding uses, and the truncation is stated in the form's validity. Without a declared operational infinity there is no honest finite reading, so the form declines to compile.

Source code in mathema/compiled.py

def compile_form(expr, names=None, provenance=(), validity="",
                 backend="math",
                 pseudo_infinity=None) -> "CompiledForm | None":
    """Intent:
        Lambdify `expr` over `names` (defaulting to its sorted free
        symbols) into a CompiledForm, or None when the expression
        contains something the backend cannot run (an unevaluated
        Integral under the plain math backend, an unmapped special
        function).

    Notes:
        `pseudo_infinity` is the claim's resolved (lo, hi) operational
        infinity (records.pseudo_infinity_range). An unevaluated
        Integral with an infinite bound is read at that range, the
        same empirical reading of infinity every other consumer of a
        `let |inf| be v` binding uses, and the truncation is stated
        in the form's validity. Without a declared operational
        infinity there is no honest finite reading, so the form
        declines to compile.
    """
    free = sorted(expr.free_symbols, key=str)
    if names is None:
        names = [str(s) for s in free]
    by_name = {str(s): s for s in free}
    syms = [by_name.get(n, sympy.Symbol(n)) for n in names]
    if expr.has(sympy.Sum, sympy.Product, sympy.Limit, sympy.Derivative):
        return None   # unevaluated calculus needs its own treatment
    if expr.has(sympy.Integral):
        # a definite integral sympy couldn't close still evaluates
        # NUMERICALLY: substitute the point, then evalf, which routes
        # through mpmath's quadrature internally, no new dependency.
        # Each call is real numeric integration, so the "quad" backend
        # tag tells consumers to spend far fewer trials. FINITE ranges
        # only: quadrature over an infinite (often oscillatory) range
        # can be silently inaccurate, and a wrong value here would
        # manufacture a counterexample, a true residue-family
        # identity was once "falsified" exactly this way. An infinite
        # bound therefore compiles only when the claim binds an
        # operational infinity, and is read at that declared range.
        has_infinite = any(
            getattr(bound, "is_infinite", False)
            for integral in expr.atoms(sympy.Integral)
            for limits in integral.limits for bound in limits[1:])
        if has_infinite:
            if pseudo_infinity is None:
                return None
            lo, hi = pseudo_infinity
            expr = expr.subs({sympy.oo: sympy.Float(hi),
                              -sympy.oo: sympy.Float(lo)})
            reading = (f"infinite integration bounds read at the "
                       f"declared operational infinity [{lo:g}, {hi:g}]")
            validity = f"{validity}; {reading}" if validity else reading
        def quad_fn(*vals, _expr=expr, _syms=tuple(syms)):
            value = _expr.subs(dict(zip(_syms, vals))).evalf(15)
            if not getattr(value, "is_number", False):
                raise ValueError("integral did not resolve numerically")
            c = complex(value)
            if abs(c.imag) > 1e-9:
                raise ValueError("complex-valued integral")
            return float(c.real)
        return CompiledForm(expr=expr, fn=quad_fn, names=tuple(names),
                            provenance=tuple(provenance), validity=validity,
                            backend="quad")
    modules = "mpmath" if backend == "mpmath" else ["math"]
    try:
        raw = sympy.lambdify(syms, expr, modules=modules)
    except Exception:
        return None
    return CompiledForm(expr=expr, fn=raw, names=tuple(names),
                        provenance=tuple(provenance), validity=validity,
                        backend=backend)

numeric_check(lhs, rhs, relation, domain, tolerance=1e-09, admits=None, trials=_NUMERIC_TRIALS)

Intent

Sample the two compiled sides over the declared domain and adjudicate the relation numerically: the fallback evidence for a claim whose symbolic comparison stalled and whose original form the probe route cannot evaluate (a d()/integrate()/Sum() law). Returns (verdict, checked, counterexample_text) with verdict one of "holds" / "falsified" / None (not enough evaluable samples). The ceiling is holds; this is sampling, never proof, and it samples the RECONSTRUCTION, which the caller must say.

Notes

Strict relations get no tolerance credit and equality gets the claim's own tolerance, matching the probe loop's comparison rules exactly; a ~= claim's tolerance kind is its allowance at each pair, in float64. admits, when given, filters candidate points (an assuming surface).

Source code in mathema/compiled.py

def numeric_check(lhs: CompiledForm, rhs: CompiledForm, relation: str,
                  domain: dict, tolerance: "float | ToleranceKind" = 1e-9,
                  admits=None, trials: int = _NUMERIC_TRIALS):
    """Intent:
        Sample the two compiled sides over the declared domain and
        adjudicate the relation numerically: the fallback evidence for
        a claim whose symbolic comparison stalled and whose original
        form the probe route cannot evaluate (a d()/integrate()/Sum()
        law). Returns `(verdict, checked, counterexample_text)` with
        verdict one of "holds" / "falsified" / None (not enough
        evaluable samples). The ceiling is holds; this is sampling,
        never proof, and it samples the RECONSTRUCTION, which the
        caller must say.

    Notes:
        Strict relations get no tolerance credit and equality gets the
        claim's own tolerance, matching the probe loop's comparison
        rules exactly; a `~=` claim's tolerance kind is its allowance
        at each pair, in float64. `admits`, when given, filters candidate points
        (an `assuming` surface).
    """
    names = sorted(set(lhs.names) | set(rhs.names))
    rng = random.Random(_RNG_SEED)
    checked = 0
    for _ in range(trials):
        point = {}
        for n in names:
            bound = domain.get(n)
            b = None
            if isinstance(bound, tuple):
                try:
                    b = (float(bound[0]), float(bound[1]))
                except (TypeError, ValueError):
                    b = None
            point[n] = _synth_scalar(rng, b)
        if admits is not None and not admits(point):
            continue
        try:
            lv = lhs.fn(*[point[n] for n in lhs.names])
            rv = rhs.fn(*[point[n] for n in rhs.names])
        except Exception:
            continue
        if not all(isinstance(v, (int, float)) and not isinstance(v, bool)
                   and v == v and abs(v) != float("inf") for v in (lv, rv)):
            continue
        tol = tolerance
        if isinstance(tol, ToleranceKind):
            if relation != "~=":
                bare(tol, f"a sampled {relation} comparison")
            # a kind's allowance at this pair, in float64
            tol = tol.bound(lv, rv)
        if "quad" in (lhs.backend, rhs.backend):
            # numeric integration carries its own error: a quad-backed
            # comparison only counts a failure past a magnitude-scaled
            # margin, so quadrature noise never manufactures a witness
            tol = tolerance + 1e-6 * max(abs(lv), abs(rv), 1.0)
        ok = (abs(lv - rv) <= tol if relation in ("==", "~=") else
              abs(lv - rv) > tol if relation == "!=" else
              lv <= rv + tol if relation == "<=" else
              lv >= rv - tol if relation == ">=" else
              lv < rv if relation == "<" else
              lv > rv if relation == ">" else None)
        if ok is None:
            return None, checked, None
        checked += 1
        if not ok:
            from .probing import _fmt_coordinate
            coords = ", ".join(f"{n} = {_fmt_coordinate(point[n])}" for n in names)
            return "falsified", checked, f"{coords}: {lv!r} vs {rv!r}"
    if checked >= max(6, trials // 4):
        # the floor bends for expensive backends (a quad-backed check
        # runs 12 trials, each a real numeric integration): six
        # agreeing evaluations is still evidence, thin sampling below
        # that is not
        return "holds", checked, None
    return None, checked, None

mathema.forms

mathema.forms

Other closed forms of arbitrary code: the public face of the rewrite gallery and the substitution library.

closed_forms(fn) lifts a function's body to its symbolic closed form and returns every structurally distinct equivalent the gallery can produce (factored, expanded, trig-simplified, ...), each named by the rewrite that made it. substituted_forms(fn) lists the known changes of variable that apply to the body's shape, t = log(x) for a logarithmic body, the Weierstrass half-angle for a trigonometric one, with the transformed expression and the domain condition each one needs. register_substitution extends that library: a registered substitution is immediately available here and to the extensive proof ladder, so a domain-specific change of variable contributed once can start closing proofs.

These are the same registries extensive=True adjudication draws on, exposed directly because an alternative form of one's own code is useful beyond proving: reading it, simplifying it, or spotting that two implementations share a closed form.

register_substitution = _register_substitution module-attribute

Form dataclass

One closed form of a function's body: name is the rewrite that produced it ("as written" for the lift itself), expr the sympy expression, text its canonical rendering.

Source code in mathema/forms.py

@dataclass(frozen=True)
class Form:
    """One closed form of a function's body: `name` is the rewrite that
    produced it ("as written" for the lift itself), `expr` the sympy
    expression, `text` its canonical rendering."""
    name: str
    expr: object
    text: str

SubstitutedForm dataclass

A function's body carried through one known change of variable: name is the substitution ("t = log(x)"), param the parameter it replaced, expr/text the transformed body in the new variable var, and requires the domain condition under which the substitution is a monotone bijection (and the transformed form therefore takes exactly the original's values).

Source code in mathema/forms.py

@dataclass(frozen=True)
class SubstitutedForm:
    """A function's body carried through one known change of variable:
    `name` is the substitution ("t = log(x)"), `param` the parameter it
    replaced, `expr`/`text` the transformed body in the new variable
    `var`, and `requires` the domain condition under which the
    substitution is a monotone bijection (and the transformed form
    therefore takes exactly the original's values)."""
    name: str
    param: str
    var: object
    expr: object
    text: str
    requires: str = field(default="always")

Substitution dataclass

One classic change of variable, t = g(x).

name is the display form ("t = log(x)"); requires states, in plain text, the domain condition under which the substitution is a monotone bijection ("x > 0"); forward maps a value of x to the corresponding t (used on domain endpoints); inverse maps the new variable back (x = g⁻¹(t), substituted into the expression); detect says whether an expression contains the shape this substitution is known to help with; applicable checks the domain condition on exact interval endpoints; monotone is "increasing" or "decreasing" and controls whether the mapped endpoints swap.

A substitution transforms a sign or equality question without changing its answer: g is a bijection from the declared interval onto its image, so expr(x) and expr(g⁻¹(t)) take exactly the same set of values. That is what lets a proof found in t-space stand as a proof of the original claim.

Source code in mathema/symbolic/_forms.py

@dataclass(frozen=True)
class Substitution:
    """One classic change of variable, `t = g(x)`.

    `name` is the display form ("t = log(x)"); `requires` states, in
    plain text, the domain condition under which the substitution is a
    monotone bijection ("x > 0"); `forward` maps a value of x to the
    corresponding t (used on domain endpoints); `inverse` maps the new
    variable back (`x = g⁻¹(t)`, substituted into the expression);
    `detect` says whether an expression contains the shape this
    substitution is known to help with; `applicable` checks the domain
    condition on exact interval endpoints; `monotone` is "increasing"
    or "decreasing" and controls whether the mapped endpoints swap.

    A substitution transforms a sign or equality question without
    changing its answer: g is a bijection from the declared interval
    onto its image, so `expr(x)` and `expr(g⁻¹(t))` take exactly the
    same set of values. That is what lets a proof found in t-space
    stand as a proof of the original claim."""
    name: str
    requires: str
    forward: Callable[[sympy.Basic], sympy.Basic]
    inverse: Callable[[sympy.Basic], sympy.Basic]
    detect: Callable[[sympy.Basic, sympy.Symbol], bool]
    applicable: Callable[[sympy.Basic, sympy.Basic], bool]
    monotone: str = "increasing"

closed_forms(fn, facts=None)

Every structurally distinct closed form of fn's body the rewrite gallery produces, the as-written lift first.

>>> def parallel(a: float, b: float) -> float:
...     return 1.0 / (1.0 / a + 1.0 / b)
>>> [f.name for f in closed_forms(parallel)]  # doctest: +SKIP
['as written', 'cancel', 'together', ...]

Each Form carries the producing rewrite's name, the sympy expression, and its canonical text. Forms are deduplicated structurally, so two rewrites that land on the same expression yield one entry (the first name wins). Raises ValueError, with the blocking construct named, for a function that has no scalar closed form at all.

Source code in mathema/forms.py

def closed_forms(fn, facts=None) -> list[Form]:
    """Every structurally distinct closed form of `fn`'s body the
    rewrite gallery produces, the as-written lift first.

        >>> def parallel(a: float, b: float) -> float:
        ...     return 1.0 / (1.0 / a + 1.0 / b)
        >>> [f.name for f in closed_forms(parallel)]  # doctest: +SKIP
        ['as written', 'cancel', 'together', ...]

    Each `Form` carries the producing rewrite's name, the sympy
    expression, and its canonical text. Forms are deduplicated
    structurally, so two rewrites that land on the same expression
    yield one entry (the first name wins). Raises `ValueError`, with
    the blocking construct named, for a function that has no scalar
    closed form at all."""
    lifted = _lifted_expr(fn, facts)
    expr = lifted.expr
    forms = [Form("as written", expr, render_canonical(expr)[0])]
    seen = {sympy.srepr(expr)}
    for name, form_expr in rewrite_forms(expr):
        key = sympy.srepr(form_expr)
        if key in seen:
            continue
        seen.add(key)
        forms.append(Form(name, form_expr, render_canonical(form_expr)[0]))
    return forms

substituted_forms(fn, facts=None)

The known changes of variable that apply to fn's body, one SubstitutedForm per (substitution, parameter) pair whose shape the substitution recognizes.

>>> import math
>>> def loglaw(x: float) -> float:
...     return math.log(x) ** 2 - 2.0 * math.log(x) + 1.5
>>> [s.name for s in substituted_forms(loglaw)]  # doctest: +SKIP
['t = log(x)']

The transformed expression is simplified in the new variable, and requires states the domain condition ("x > 0") under which the substitution is a monotone bijection, on such a domain the transformed form takes exactly the values the original does, which is what makes it usable in a proof and not just a display. Raises ValueError for a function with no scalar closed form.

Source code in mathema/forms.py

def substituted_forms(fn, facts=None) -> list[SubstitutedForm]:
    """The known changes of variable that apply to `fn`'s body, one
    `SubstitutedForm` per (substitution, parameter) pair whose shape
    the substitution recognizes.

        >>> import math
        >>> def loglaw(x: float) -> float:
        ...     return math.log(x) ** 2 - 2.0 * math.log(x) + 1.5
        >>> [s.name for s in substituted_forms(loglaw)]  # doctest: +SKIP
        ['t = log(x)']

    The transformed expression is simplified in the new variable, and
    `requires` states the domain condition ("x > 0") under which the
    substitution is a monotone bijection, on such a domain the
    transformed form takes exactly the values the original does, which
    is what makes it usable in a proof and not just a display. Raises
    `ValueError` for a function with no scalar closed form."""
    lifted = _lifted_expr(fn, facts)
    expr = lifted.expr
    out = []
    for pname, sym in lifted.params.items():
        if sym not in expr.free_symbols:
            continue
        for sub in _substitutions():
            try:
                if not sub.detect(expr, sym):
                    continue
            except Exception:
                continue
            t = sympy.Symbol("t", real=True)
            try:
                from ._timeout import FAST_TIMEOUT_SECONDS, _with_timeout
                transformed = _with_timeout(
                    lambda: sympy.simplify(expr.subs(sym, sub.inverse(t))),
                    FAST_TIMEOUT_SECONDS)
            except Exception:
                continue
            requires = (sub.requires if sub.requires == "always"
                        else sub.requires.replace("x", pname))
            out.append(SubstitutedForm(
                name=sub.name.replace("(x)", f"({pname})").replace("/x", f"/{pname}")
                             .replace("(x/2)", f"({pname}/2)"),
                param=pname, var=t, expr=transformed,
                text=render_canonical(transformed)[0], requires=requires))
    return out

executable_forms(fn, facts=None, backend='math')

Intent

Every closed form of fn's body as a runnable CompiledForm: the as-written lift and each gallery rewrite, compiled through mathema.compiled.compile_form, carrying the provenance chain (which rewrite produced it) and, for a substituted form, the domain condition its equivalence needs. A compiled form is mathema's reconstruction, never the original code, evidence from running one is evidence about the symbolic form, which is exactly what makes it useful for cross-checking the original against its own mathematics.

import mathema.forms def parallel(a: float, b: float) -> float: ... return 1.0 / (1.0 / a + 1.0 / b) cfs = mathema.forms.executable_forms(parallel) # doctest: +SKIP cfs[0].fn(2.0, 2.0) # doctest: +SKIP 1.0

Notes

A form the backend cannot compile (an unevaluated calculus atom, an unmapped special function) is skipped, not an error; an unliftable function raises the same ValueError closed_forms does. Substituted forms carry their requires condition in validity; equivalence holds only where the change of variable is a monotone bijection.

Source code in mathema/forms.py

def executable_forms(fn, facts=None, backend: str = "math") -> list:
    """Intent:
        Every closed form of `fn`'s body as a runnable CompiledForm:
        the as-written lift and each gallery rewrite, compiled through
        `mathema.compiled.compile_form`, carrying the provenance chain
        (which rewrite produced it) and, for a substituted form, the
        domain condition its equivalence needs. A compiled form is
        mathema's reconstruction, never the original code, evidence
        from running one is evidence about the symbolic form, which is
        exactly what makes it useful for cross-checking the original
        against its own mathematics.

        >>> import mathema.forms
        >>> def parallel(a: float, b: float) -> float:
        ...     return 1.0 / (1.0 / a + 1.0 / b)
        >>> cfs = mathema.forms.executable_forms(parallel)  # doctest: +SKIP
        >>> cfs[0].fn(2.0, 2.0)  # doctest: +SKIP
        1.0

    Notes:
        A form the backend cannot compile (an unevaluated calculus
        atom, an unmapped special function) is skipped, not an error;
        an unliftable function raises the same `ValueError`
        `closed_forms` does. Substituted forms carry their `requires`
        condition in `validity`; equivalence holds only where the
        change of variable is a monotone bijection.
    """
    from .compiled import compile_form
    out = []
    for form in closed_forms(fn, facts):
        cf = compile_form(form.expr, provenance=("lift",) if form.name == "as written"
                          else ("lift", form.name),
                          validity="as lifted", backend=backend)
        if cf is not None:
            out.append(cf)
    for sub in substituted_forms(fn, facts):
        cf = compile_form(sub.expr,
                          provenance=("lift", sub.name),
                          validity=sub.requires, backend=backend)
        if cf is not None:
            out.append(cf)
    return out

mathema.targets

mathema.targets

The one target resolver: any spelling of "which function(s)" that a mathema command accepts resolves here, to live callables keyed by their canonical dotted name (module.qualname, the same shape the declared/verified stores use).

Accepted spellings:

• pkg / pkg.mod, an importable package or module; a package is walked into every submodule.
• pkg.mod.fn / pkg.mod.Class.method; one function or method, found by importing the longest importable prefix and walking attributes for the rest.
• pkg.mod:fn / pkg.mod:Class.method, the explicit one-function form; pkg:name also matches name anywhere under pkg when that suffix is unique.
• path/to/file.py / path/to/file.py:fn, a file, imported under its real dotted name with full package context (the package root is found by walking up through __init__.py directories), so relative imports inside the target work and the loaded functions key identically to normally-imported ones.

Every command and programmatic surface resolves through resolve / resolve_function; a target that cannot be resolved raises TargetError with a printable message (CLI exit 2).

Target dataclass

One resolved target: kind is "package", "module", or "function"; functions maps each canonical dotted key to its live callable; module_name is the dotted module actually imported (or None for a package walk); skipped lists (submodule, error) pairs for package submodules that failed to import.

Source code in mathema/targets.py

@dataclass
class Target:
    """One resolved target: `kind` is "package", "module", or
    "function"; `functions` maps each canonical dotted key to its live
    callable; `module_name` is the dotted module actually imported (or
    None for a package walk); `skipped` lists `(submodule, error)`
    pairs for package submodules that failed to import."""
    kind: str
    functions: dict[str, Callable]
    module_name: str | None
    root: str
    skipped: list = field(default_factory=list)

TargetError

Bases: Exception

A target string that cannot be resolved to any function. The message is written to be printed as-is to a CLI user.

Source code in mathema/targets.py

class TargetError(Exception):
    """A target string that cannot be resolved to any function. The
    message is written to be printed as-is to a CLI user."""

resolve(target, root='.', *, skipped=None)

Resolve a target spelling to its functions, keyed by canonical dotted name. See the module docstring for the accepted spellings. skipped, when given, collects (submodule, error) pairs for package submodules that failed to import (also carried on the returned Target).

Raises:

Type	Description
TargetError	nothing resolvable at this spelling; the message is printable as-is.

Source code in mathema/targets.py

def resolve(target: str, root: str = ".", *,
            skipped: list | None = None) -> Target:
    """Resolve a target spelling to its functions, keyed by canonical
    dotted name. See the module docstring for the accepted spellings.
    `skipped`, when given, collects `(submodule, error)` pairs for
    package submodules that failed to import (also carried on the
    returned Target).

    Raises:
        TargetError: nothing resolvable at this spelling; the message
            is printable as-is.
    """
    from .audit import DiscoveryError, discover

    skipped = skipped if skipped is not None else []
    mod_part, _, qual_part = target.partition(":")

    if ":" in target and not _is_pathlike(mod_part):
        # a tagged key (`<tag>:src/ema#ema`): a registered
        # resolver turns it into a Target of callable proxies; None
        # means "not mine" and resolution falls through to the
        # ordinary import path unchanged
        from ._target_resolvers import get_resolver
        resolver = get_resolver(mod_part)
        if resolver is not None:
            resolved = resolver(target, root)
            if resolved is not None:
                return resolved

    if _is_pathlike(mod_part):
        dotted, root = _dotted_name_for_file(mod_part)
        # a cached module under this dotted name that came from a
        # DIFFERENT file (two scratch scripts both named m.py, say)
        # would be returned instead of importing the requested one,
        # evict it, and its submodules, so the import is really this
        # file
        full = os.path.abspath(os.path.expanduser(mod_part))
        cached = sys.modules.get(dotted)
        if cached is not None and os.path.abspath(
                getattr(cached, "__file__", "") or "") != full:
            for name in [dotted] + [k for k in list(sys.modules)
                                    if k.startswith(dotted + ".")]:
                sys.modules.pop(name, None)
        _import_module(dotted, root)
        target = f"{dotted}:{qual_part}" if qual_part else dotted
        mod_part = dotted

    colon = ":" in target
    with _root_on_path(root):
        try:
            found = discover([target], skipped=skipped)
        except DiscoveryError as e:
            if not colon:
                walked = _prefix_walk(mod_part, root)
                if walked is not None:
                    return _walked_target(walked, target, root, skipped)
            if "#" in qual_part and "." not in mod_part:
                # the tagged-key shape with nothing registered to serve
                # it: name the remedy, not the bogus module import
                raise TargetError(
                    f"no target resolver is registered for "
                    f"{mod_part + ':'!r}; install the adaptor package "
                    f"providing it, or check the tag spelling "
                    f"(registered resolvers come from the "
                    f"{'mathema.target_resolvers'!r} entry-point "
                    f"group)") from e
            raise TargetError(str(e)) from e
        if colon and found:
            return Target("function", found, mod_part, root, skipped)
        if not colon:
            # a module or package resolves even with zero functions;
            # the caller decides whether an empty population is an error
            mod = sys.modules.get(target)
            kind = ("package" if mod is not None and hasattr(mod, "__path__")
                    else "module")
            return Target(kind, found, target if kind == "module" else None,
                          root, skipped)
        walked = _prefix_walk(f"{mod_part}.{qual_part}", root)
        if (walked is not None and callable(walked[2])
                and not inspect.isclass(walked[2])
                and not inspect.isfunction(walked[2])):
            # a callable discovery never lists (a C builtin, a ufunc,
            # a library's dispatcher object) found at the named
            # attribute: the same function the dotted spelling names
            return _walked_target(walked, target, root, skipped)
        if not _inside_root(mod_part, root):
            # a library installed outside the project: the name is read
            # as an attribute only, never searched for by importing
            # every submodule (some run a program when imported)
            if walked is not None:
                return _walked_target(walked, target, root, skipped)
            raise TargetError(_no_such_attribute(mod_part, qual_part))
        if "." not in qual_part:
            # bare-suffix search: `pkg:name` matches `name` anywhere
            # under the package when that suffix is unique
            wider = discover([mod_part], skipped=skipped)
            hits = {k: v for k, v in wider.items()
                    if k.rsplit(".", 1)[-1] == qual_part}
            if len(hits) == 1:
                return Target("function", hits, None, root, skipped)
            if len(hits) > 1:
                names = ", ".join(sorted(hits)[:10])
                raise TargetError(
                    f"{qual_part!r} is ambiguous under {mod_part!r}: {names}")
        what = qual_part or target
        hint = ""
        try:
            pool = discover([mod_part], skipped=list(skipped))
        except Exception:
            pool = {}
        if pool:
            import difflib
            leaf = what.rsplit(".", 1)[-1]
            close = set(difflib.get_close_matches(
                leaf, {k.rsplit(".", 1)[-1] for k in pool}, n=3, cutoff=0.6))
            matches = [k for k in sorted(pool)
                       if k.rsplit(".", 1)[-1] in close]
            if matches:
                hint = "; did you mean: " + ", ".join(matches[:3]) + "?"
        raise TargetError(
            f"no function named {what!r} found under {mod_part!r}{hint}")

resolve_function(target, root='.')

Resolve a target that must name exactly one function, returning (key, fn).

Raises:

Type	Description
TargetError	the target resolves to nothing, or to more than one function (the message lists candidates).

Source code in mathema/targets.py

def resolve_function(target: str, root: str = ".") -> tuple[str, Callable]:
    """Resolve a target that must name exactly one function, returning
    `(key, fn)`.

    Raises:
        TargetError: the target resolves to nothing, or to more than
            one function (the message lists candidates).
    """
    t = resolve(target, root)
    if len(t.functions) == 1:
        return next(iter(t.functions.items()))
    names = ", ".join(sorted(t.functions)[:10])
    more = "" if len(t.functions) <= 10 else f" (+{len(t.functions) - 10} more)"
    raise TargetError(
        f"{target!r} names {len(t.functions)} functions, not one: "
        f"{names}{more}. Narrow it with `module:function`.")