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 the first real
    # user: "mathema.diagnostic_report" -> its own dict). Never
    # populated automatically by check()/write_spec(), a caller sets it
    # explicitly when it wants the extra work done.
    meta: dict = field(default_factory=dict, repr=False)

    def __repr__(self) -> str:
        from .analysis import tier_word
        lines = [f"mathema.Record({self.facts.name}) · {tier_word(self.facts.tier)} "
                f"· form {self.facts.form}"]
        for p in self.probes:
            mark = {"holds": "holds  ", "falsified": "FALSIFY", "proven": "proven ",
                    "skipped": "skip   ", "unknown": "unknown",
                    "invalidated": "INVALID"}.get(p.verdict.split(":", 1)[0], p.verdict)
            if p.verdict == "proven":
                # a proof has no trial count the way a probe does, the
                # statement itself gets prettified into ordinary math
                # notation, and 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.
                stmt = p.statement.replace("==", "=").replace("<=", "≤").replace(">=", "≥")
                line = f"  {mark} {p.name}: {stmt}"
                if p.condition:
                    line += f"\n           {p.condition}"
            else:
                line = f"  {mark} {p.name}: {p.statement}"
                if p.verdict == "holds" and p.n:
                    line += f" (n={p.n})"
            if p.counterexample:
                line += f"\n           counterexample {p.counterexample}"
            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)
        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)

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_scale=1.0, extensive=False, declared=None, known_premises=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 filesystem. 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.

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

def check(fn, claims: list | None = None, domain: dict | None = None,
         trials: int | None = None,
         trials_scale: float = 1.0, extensive: bool = False,
         declared: dict | None = None,
         known_premises: dict | 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
    filesystem. 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.

    `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 _RISK, _SPECIALS
    from .spec import declare, entry_claims
    from .types import _TYPE_PROBE_TRIALS, domain_from_signature, type_probes

    facts = analyze(fn)
    # 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

    probes = _stamp_surface(
        probe(fn, facts, domain=battery_domain or None,
              trials=trials, trials_scale=trials_scale, extensive=extensive),
        "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),
                                     "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)
    built = [claim(c) 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
        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 all_claims:
        probes = probes + check_conjectures(fn, all_claims, domain=parent_domain or None,
                                            trials=trials, trials_scale=trials_scale,
                                            facts=facts, extensive=extensive,
                                            known_premises=known_premises,
                                            float_companions=True)
    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 = {}
    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
    return Record(facts=facts, probes=probes, dependencies=deps,
                  concepts=concept_objs, meta=meta, lifted=lifted)

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 injected
    try:
        facts = analyze_source(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 language-tagged key (`ts:src/ema.ts#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)
        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=())

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=()) -> 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()
    for c in claims:
        name, verdict, meta, note = _claim_fields(c)
        if "mathema.foreign_grammar" in meta:
            r.foreign.append(c)
            continue
        if _volunteered(meta, note):
            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
        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
        elif kind == "skipped":
            r.skipped += 1
    # 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:
        r.problems.append(f"{r.falsified} 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)
        r.problems.append(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:
            r.problems.append(f"{r.skipped} skipped 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_scale=1.0, only=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.

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_scale: float = 1.0,
                   only: "list | 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.

    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.
    """
    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)
        return _verify_sweep(root, all=all, strict=strict,
                             trials_scale=trials_scale, only=only)

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 carrier 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 carrier 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 ""
    if "does not yet lift multi-function or != claims" 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 a strict AST whitelist before evaluation: this pipeline accepts untrusted proposals, so nothing outside arithmetic, comparisons handled by the relation, and a fixed set of safe calls can run.

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 = "=="        # "==" | "<=" | ">="
    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)
    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 | None = None
    # how close counts as equal (declared-schema.md's `tolerance` field;
    # 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 domain approximation for infinity, parallel to tolerance: an
    # unbounded (+-inf) direction stops at this magnitude on both
    # routes, and the float companion runs to it, applied symmetrically
    # (records.pseudo_infinity_range resolves it to the (-v, v) range
    # consumers read). None means real infinity: no default, and the
    # float companion then runs to a large sampled magnitude. Rendered
    # in the claim text only when set (an ordinary bounded-domain claim
    # never states it).
    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.
    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)

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

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_builtin_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 implementation, and "derive:math_only" asks for the proof alone, with no companion. 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.

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()) -> 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_builtin_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 implementation, and "derive:math_only"
    asks for the proof alone, with no companion. 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."""
    # "auto" is fully retired (the word stays free for automatic
    # differentiation): it is NOT a legacy alias, an "auto" route
    # reaches adjudication as an unknown route and skips loudly.
    # A safety predicate is an implementation fact: whatever route the
    # author passed, it is examined through the full structural +
    # empirical cascade, and the record reports which mechanism
    # decided (the examine route). That normalization happens after
    # parsing, once the relation is known, see below.
    if "#" in blank_strings(law):
        raise InvalidConjecture(
            f"`#` has no meaning in a claim and would silently cut off "
            f"everything after it; remove it (a comment belongs outside "
            f"the claim text): {law.strip()!r}")
    try:
        text, ambiguous_diff_vars = extract_diff_fraction_sugar(law.strip())
    except UnreadableSpelling as e:
        raise InvalidConjecture(str(e)) from e
    # outcome section: stripped first, on raw text, extract_outcome_
    # clause recognizes any accepted "implies" spelling directly rather
    # than relying on normalize() to have unified them, so it never has
    # to wait its turn in the retry loop below. Stub only: captured
    # verbatim, no semantics read it yet.
    outcome, text = extract_outcome_clause(text)
    # let/for/assuming section order: extract_let_bindings and
    # extract_assuming_clause only ever fire on text literally starting
    # with "let"/"assuming" (never misreading a bare trailing "name =
    # expr" statement as a let-continuation, since that shape is only
    # ever a continuation of an *already-found* let run), and
    # split_quantifier only fires on text literally starting with "for",
    # so retrying all three, each on whatever's left after the
    # others last ran, correctly finds any relative ordering of them
    # (`for ..., let ..., statement`, `assuming ..., for ..., let ...,
    # statement`, ...) exactly as readily as today's fixed `let ...,
    # for ..., statement` one, with no change to any of their own entry
    # conditions or internal logic. Loop terminates by construction:
    # each iteration either makes progress (text changes) or breaks
    # immediately.
    let_funcs: dict = {}
    let_domain: dict = {}
    dom: dict = {}
    aliases: dict = {}
    assuming = ""
    let_pseudo_inf: float | None = None
    while True:
        prev = text
        new_assuming, text = extract_assuming_clause(text)
        if new_assuming is not None:
            if not new_assuming.strip()[len("assuming"):].strip():
                raise InvalidConjecture(
                    f"`assuming` has no premise before its comma: state "
                    f"one (`assuming x > 0, ...`) or drop the keyword: "
                    f"{law.strip()!r}")
            assuming = (_conjoin_assuming(assuming, new_assuming, law)
                        if assuming else new_assuming)
        try:
            (new_funcs, new_free_domain, text, new_aliases,
             new_pseudo_inf) = extract_let_bindings(text)
        except InvalidDomain as e:
            raise InvalidConjecture(str(e)) from e
        let_funcs.update(new_funcs)
        let_domain.update(new_free_domain)
        aliases.update(new_aliases)
        if new_pseudo_inf is not None:
            if (let_pseudo_inf is not None
                    and let_pseudo_inf != new_pseudo_inf):
                raise InvalidConjecture(
                    "the operational infinity is bound twice with "
                    "different ranges")
            let_pseudo_inf = new_pseudo_inf
        text = normalize(text)
        try:
            new_dom, text = split_quantifier(text)
        except DuplicateBinding as e:
            raise ConflictingDomainBinding(str(e)) from e
        except InvalidDomain as e:
            raise InvalidConjecture(str(e)) from e
        rebound = sorted(set(new_dom) & set(dom) - {"n"})
        if rebound:
            raise ConflictingDomainBinding(
                f"{rebound} bound by two quantifiers in the same claim; "
                f"give each name one domain")
        dom.update(new_dom)
        if text == prev:
            break
    double_bound = sorted(set(let_domain) & set(dom))
    if double_bound:
        raise ConflictingDomainBinding(
            f"{double_bound} declared with both 'let ... be ...' and "
            f"'for ... in ...' in the same claim, pick one")
    # a `for` clause processed in an earlier retry-loop iteration, before
    # this claim's `let <alias> = <real name>` was even found, can commit
    # a domain key literally spelled the same as that alias
    # (`for m in [...], let m = m1, ...`), silently binding the
    # declared domain to the alias, not the real parameter it resolves
    # to, since the domain key is already committed by the time the
    # alias is known. Only reachable now that `for` can precede
    # `let`, caught here
    # rather than left to silently produce a domain key that can never
    # match a real parameter.
    aliased_domain_keys = sorted(set(aliases) & set(dom))
    if aliased_domain_keys:
        raise ConflictingDomainBinding(
            f"{aliased_domain_keys} used as a 'for ... in ...' binding name "
            f"before its own 'let {aliased_domain_keys[0]} = "
            f"{aliases[aliased_domain_keys[0]]}' alias was resolved, "
            f"write the real name ({aliases[aliased_domain_keys[0]]!r}) in "
            f"the 'for' clause instead, or move the 'let' earlier")
    dom = {**let_domain, **dom}
    prime_problem = unexpanded_prime_message(text)
    if prime_problem is not None:
        raise InvalidConjecture(prime_problem)
    r = parse_raises(text)
    ds = None if r is not None else parse_domain_safety(text)
    negated = False
    links: list = []
    if r is not None:
        lhs, exc = r
        rel, rhs = "raises", (exc or "")
    elif ds is not None:
        rel, lhs, rhs = ds[0], ds[1], ""
        if rel.startswith("not "):
            rel, negated = rel[4:], True
    else:
        section = _MISCASED_SECTION.match(text)
        if section is not None:
            raise InvalidConjecture(
                f"section keywords are lowercase: write "
                f"`{section.group(1).lower()}`, not `{section.group(1)}`, "
                f"in {law.strip()!r}")
        # a residual top-level comma is a comma-joined relation pair
        # (`f >= 1, f <= 4`), ambiguous with the section-separator comma
        # (and parsing as a bare tuple, which no relation split would
        # flag), refuse with the actionable spelling up front
        if len(_split_commas(text)) > 1:
            raise InvalidConjecture(
                "a claim carries one relation: state each as its own "
                "claim, or use a chained comparison (a <= b <= c)")
        # a top-level implication arrow that survived to here is not
        # outcome grammar (that shape is `=> self.<claim>`, stripped
        # off raw text up front) and not an assuming pin (those live in
        # the assuming section, already extracted), left in place it
        # would silently become part of one side's expression text, a
        # different claim than the author wrote
        if _split_top_level(text, ("=>",)) is not None:
            raise InvalidConjecture(
                "'=>' reads as an outcome clause and takes a claim "
                "reference (`=> self.<claim_name>`); to make one "
                "relation conditional on another, state the premise "
                "as `assuming <relation>, <statement>`")
        try:
            links = split_relation_chain(text)
        except NoRelation as e:
            raise InvalidConjecture(str(e)) from e
        lhs, rel, rhs = links[0]
        if len(links) == 1:
            links = []
    # a residual `|` is a bar the grammar could not pair with another,
    # and left in place it reaches rendering as unparseable text
    for _side in (lhs, rhs):
        if _side and "|" in blank_strings(_side):
            raise InvalidConjecture(
                f"the bars in {_side!r} do not pair up. Each opening bar "
                f"needs a closing one; abs(...), norm(...) and det(...) "
                f"are the call spellings of the same quantities.")
    # type-aware matrix sugar: `A^T` -> `A.T`, `|A|` -> `det(A)`,
    # `A^-1` -> `inv(A)`, but only for names known to be matrices, from
    # this claim's own domain or supplied by a caller holding the
    # function's signature. A scalar operand keeps power / abs /
    # reciprocal, so the reading is decided by the type, never guessed.
    mat_names = frozenset(matrix_names) | linalg.declared_matrix_names(dom)
    if mat_names:
        lhs = linalg.apply_matrix_sugar(lhs, mat_names)
        if rhs:
            rhs = linalg.apply_matrix_sugar(rhs, mat_names)
    # every side of a relation is an expression: text left over from a
    # malformed relation (`1 +`, `(`, the `= 1` that `===` splits into)
    # is refused here with the claim named, not left to surface as a
    # SyntaxError wherever the side is next parsed
    if r is None and ds is None:
        for _lhs, _rel, _rhs in (links or [(lhs, rel, rhs)]):
            for _side in (_lhs, _rhs):
                try:
                    ast.parse(_side, mode="eval")
                except SyntaxError:
                    command = _LATEX_COMMAND.search(blank_strings(_side))
                    if command is not None:
                        raise InvalidConjecture(
                            f"the LaTeX command `{command.group(0)}` has no "
                            f"meaning in the claim grammar (in the claim "
                            f"{law.strip()!r})") from None
                    raise InvalidConjecture(
                        f"cannot read {_side.strip()!r} as an expression "
                        f"in the claim {law.strip()!r}") from None
                problem = _unreadable_side(_side)
                if problem is not None:
                    where = ("" if _D_AT_SENTINEL in _side
                             else f"in {_side.strip()!r}, ")
                    raise InvalidConjecture(
                        f"{problem} ({where}claim {law.strip()!r})")
    # the record's grammar names the linear-algebra dialect when the
    # claim uses the matrix vocabulary: informative only (a reader sees
    # the parsing was matrix-aware), never required to round-trip, the
    # canonical statement re-parses under base `mathema` on its own.
    if grammar == GRAMMAR and linalg.mentions_matrix_ops(lhs, rhs):
        grammar = f"{GRAMMAR}/linalg"
    if let_pseudo_inf is not None:
        from .records import pseudo_infinity_range
        if (pseudo_infinity is not None
                and pseudo_infinity_range(pseudo_infinity)
                != pseudo_infinity_range(let_pseudo_inf)):
            raise InvalidConjecture(
                "pseudo_infinity stated twice: the let binding and the "
                "keyword argument disagree")
        pseudo_infinity = let_pseudo_inf
    if rel in routes.examine_predicates():
        # the examine normalization promised above: implementation
        # facts always run the full cascade; a declared derive/probe/
        # best on a safety predicate is advisory and folds here
        route = "examine"
    if name is None and rel in routes.examine_predicates():
        # a bare predicate claim gets the canonical bracketed name the
        # rest of the system keys on (`is_pole_safe[x]`), the name a
        # suggestion would have carried, so family dispatch and the
        # call-form rebuilders read hand-written and suggested claims
        # identically; a negated predicate is a different claim and
        # gets its own name, never the positive row's
        name = f"{'not_' if negated else ''}{rel}[{lhs}]"
    if name is None:
        name = auto_claim_name(text)
    bound_funcs = {**let_funcs, **(funcs or {})}
    for unbound in _unbound_call_names(lhs, rhs, set(bound_funcs)):
        # a bare call name (`budget_line(...)`) is a function reference
        # awaiting scope resolution at check time; recording it now;
        # the name as its own placeholder value; lets the renderer
        # treat it as the function it is rather than refusing
        bound_funcs[unbound] = unbound
    return Conjecture(name=name, lhs=lhs, rhs=rhs, relation=rel,
                      source=source, route=route, grammar=grammar,
                      funcs=bound_funcs, domain=dom,
                      free_vars=frozenset(let_domain),
                      ambiguous_diff_vars=ambiguous_diff_vars, tolerance=tolerance,
                      negated=negated, assuming=assuming, outcome=outcome or "",
                      links=links, pseudo_infinity=pseudo_infinity,
                      meta=dict(meta or {}), raw=law)

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

Adjudicate proposed claims against the live function.

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 implementation 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 spawns none, which its proof's meta states. 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.

Source code in mathema/conjecture.py

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

    `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 implementation 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 spawns none,
    which its proof's meta states. `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.
    """
    facts = _effective_facts(fn, facts)
    kinds = {p: facts.param_kinds.get(p, "unknown") for p in facts.params}
    domain = domain or {}
    # the exact same sampling setup probe()'s own remaining structural
    # checks use (seeded RNG, adaptive budget, critical-point hints),
    # computed at most once per call, from the function-level domain,
    # not re-derived per claim, matching probe()'s own established
    # precedent of one sampling decision for the whole call. Lazy,
    # behind _sampling(): a route="derive" claim never reaches the
    # generic probe loop or a family's probe:algorithmic route, so a
    # batch made entirely of those never pays for the critical-point
    # search (_points_for_probe, wall-clock capped but not free) on
    # behalf of a probe attempt that's never made.
    _sampling_cache: list = []

    def _sampling():
        if not _sampling_cache:
            _sampling_cache.append(
                _prepare_sampling(fn, facts, domain, trials, trials_scale, extensive))
        return _sampling_cache[0]

    out: list[Probe] = []

    def _stamped(probe, cj, canonical=True):
        # one statement, every surface: the row, the display, and the
        # store all carry the canonical ascii text, which re-parses to
        # this claim (sections, quantifier, premise and all). The
        # structured fields beside it are the same claim for machines.
        from .grammar import domain_bound_to_json
        from .spec import canonical_claim_text
        if canonical:
            # the renderer is total over everything claim() accepts, so
            # a failure here is a renderer bug worth a loud crash, never
            # a claim to quietly record under a different spelling
            probe.statement = canonical_claim_text(cj)
        if cj.domain:
            probe.domain = {p2: domain_bound_to_json(b)
                            for p2, b in cj.domain.items()}
        probe.grammar = cj.grammar
        probe.tolerance = cj.tolerance
        if cj.domain and not probe.condition:
            # every quantified row carries its region as the ONE
            # canonical rendered condition, real parameter names,
            # grammar-roundtrip guaranteed, human-readable. This is
            # what lets the verified layer repopulate a claim whose
            # declared entry was deleted, region intact (derive rows
            # already carry the proof's own quantifier clause).
            from .domain import render_domain
            # pinned ascii: a record's bytes must not depend on the
            # writer's global unicode preference, display re-renders
            probe.condition = "for " + ", ".join(
                f"{p2} in {render_domain(b, ascii_mode=True)}"
                for p2, b in cj.domain.items())
        inherited = {p2: b for p2, b in domain.items()
                     if p2 not in (cj.domain or {})}
        if inherited:
            # the parent domain's share of the region this claim was
            # adjudicated over, stated beside the claim's own bindings
            from .domain import render_domain
            meta = dict(probe.meta or {})
            meta["mathema.parent_domain"] = "for " + ", ".join(
                f"{p2} in {render_domain(b, ascii_mode=True)}"
                for p2, b in sorted(inherited.items()))
            probe.meta = meta
        if cj.meta:
            # declared meta (the spec's own extension object, e.g.
            # concepts) passes through under the probe's meta, the
            # probe's own keys winning
            probe.meta = {**cj.meta, **(probe.meta or {})}
        if cj.source:
            # always stamped, "user" included: with no provenance
            # prose in the note, meta is the one source channel
            meta = dict(probe.meta or {})
            meta.setdefault("mathema.surface", cj.source)
            probe.meta = meta
        _stamp_examine_route(probe, cj, fn, facts)
        return probe

    from .types import matrix_param_names
    _fn_mats = matrix_param_names(fn)
    conjectures = [claim(c) if isinstance(c, str) else c for c in conjectures]
    conjectures = [_resolve_matrix_sugar(c, _fn_mats) for c in conjectures]
    # prerequisites first, whatever order they were written in; the
    # returned list is put back in declaration order at the end, so
    # ordering is an adjudication concern and never a visible one
    declared_order = {id(cj): i for i, cj in enumerate(conjectures)}
    ordered, premise_cycles = _adjudication_order(conjectures)
    duplicate_names = {name for name in
                       (cj.name for cj in conjectures)
                       if [c.name for c in conjectures].count(name) > 1}
    for cj in ordered:
        math_only = cj.route == MATH_ONLY_ROUTE
        if math_only:
            # the opt-out adjudicates exactly as a derive claim; only the
            # companion it would spawn is withheld
            cj = _dc_replace(cj, route="derive")
        if cj.links:
            # a chained comparison is the conjunction of its links: run
            # each link through the full ordinary adjudication (same
            # domain/funcs/assuming/route) and fold, so no proof path is
            # duplicated; the exact combination rule tuple claims use
            chained, companion = _adjudicate_chain(
                cj, fn, facts, domain, trials, trials_scale, extensive,
                float_companions=(float_companions and not math_only
                                  and cj.route in ("derive", "best")))
            if math_only and chained.verdict == "proven":
                chained.meta = {**(chained.meta or {}),
                                "mathema.float_companion":
                                    "none (derive:math_only)"}
            out.append(_stamped(chained, cj))
            if companion is not None:
                _emit_companion(out, _stamped(companion, cj), cj.name)
            continue
        if (cj.relation in routes.safety_predicates() and cj.lhs == "f"
                and "f" not in facts.params):
            # the function-wide spelling: the predicate over f is the
            # conjunction of the predicate over every numeric parameter
            out.append(_stamped(_adjudicate_function_wide_safety(
                cj, fn, facts, domain, trials, trials_scale, extensive), cj))
            continue
        statement = statement_text(cj.relation, cj.lhs, cj.rhs)
        if cj.negated:
            statement = f"not {statement.strip()}"
        # no provenance prose: the source rides
        # meta["mathema.surface"] (and the compact rows' own
        # source field), and verdicts are always mathema's own, the
        # note carries only claim-specific substance
        note = _bind_scope_functions(cj, fn).lstrip("; ")
        # an explicit route that can't evaluate this claim's forms
        # (probe asked to differentiate/integrate, ...) skips up front,
        # with the reason in the sketch, never mis-adjudicated or
        # reported as an "unresolved bound function"
        unsupported = routes.unsupported_forms(cj.route, cj)
        if unsupported:
            out.append(_stamped(Probe(
                cj.name, statement, "skipped", route=None, note=note,
                sketch=f"not implemented on the {cj.route} route: "
                       f"{', '.join(unsupported)}, the {cj.route} route's "
                       f"vocabulary does not evaluate these forms"), cj))
            continue
        shadowed = _shadowed_constants(cj.lhs, cj.rhs, set(facts.params))
        if shadowed:
            note += (f"; {', '.join(shadowed)} read as the parameter"
                     f"{'s' if len(shadowed) > 1 else ''}, not the math "
                     f"constant, "
                     + ", ".join(_CONSTANT_SPELLINGS[c] for c in shadowed))
        assumption = _interpret_assumption(cj, conjectures)
        if isinstance(assumption, Probe):
            out.append(_stamped(assumption, cj))
            continue
        verdict_cap = None
        defined_mode = False
        discharged: list = []
        premise_structures: dict = {}
        if assumption is not None and assumption[0] == "structure":
            # a matrix-structure premise narrows synthesis (and, on the
            # derive route, becomes a sympy assumption); it is not a
            # region, so it does not touch the domain box
            _kind, display, premise_structures = assumption
            statement = f"assuming {display}, {statement}"
            cj = _dc_replace(cj, assuming=f"assuming {display}")
            assumption = None
        if assumption is not None and assumption[0] in ("defined",
                                                         "defined-pinned"):
            expansion = _defined_expansion(fn, facts, cj)
            if assumption[0] == "defined-pinned":
                pinned = assumption[2]
                if _region_texts_agree(pinned, expansion):
                    # the pin still describes the code: keep its exact
                    # spelling, so the record stays byte-stable
                    expansion = pinned
                else:
                    note += (f"; the pinned definedness region "
                             f"({pinned}) no longer matches the code; "
                             f"recomputed as "
                             f"({expansion or 'no raise regions'})")
            premise = (f"assuming f is defined --> {expansion}"
                       if expansion else "assuming f is defined")
            statement = f"{premise}, {statement}"
            cj = _dc_replace(cj, assuming=premise)
            assumption = None
            defined_mode = True
        elif assumption is not None and assumption[0] == "verdict":
            _kind, display, refs, lemmas = assumption
            statement = f"assuming {display}, {statement}"
            cj = _dc_replace(cj, assuming=f"assuming {display}")
            ref_name = refs[0][0]
            if cj.name in premise_cycles:
                out.append(_stamped(Probe(
                    cj.name, statement, "skipped", route=None,
                    note=f"{note}; premise cycle: {cj.name} and "
                         f"{ref_name} rest on each other, so neither can "
                         f"be established first",
                    meta={"mathema.premise": "dependency-cycle"}), cj))
                continue
            if ref_name in duplicate_names:
                out.append(_stamped(Probe(
                    cj.name, statement, "unknown", route=None,
                    note=f"{note}; prerequisite {ref_name!r} names more "
                         f"than one claim in this batch, so there is no "
                         f"one verdict to rest on; give them distinct "
                         f"names",
                    meta={"mathema.premise": "ambiguous-reference"}), cj))
                continue
            in_batch = {name for name, _ in refs
                        if any(p.name == name for p in out)}
            external: dict = {}
            hints: list = []
            ambiguous: list = []
            for name, _wanted in refs:
                if name in in_batch:
                    continue
                info = (known_premises or {}).get(name)
                if isinstance(info, str):
                    hints.append(info)
                elif isinstance(info, dict) and info.get("verdict"):
                    # resolved outside the batch (a verified row under
                    # another key, or an accepted library-stub row):
                    # the premise is satisfied at that evidence level
                    external[name] = info
                elif isinstance(info, dict) and info.get("ambiguous"):
                    ambiguous.append((name, info["ambiguous"]))
                elif isinstance(info, dict) and info.get("hint"):
                    hints.append(info["hint"])
            if ambiguous:
                name, keys = ambiguous[0]
                out.append(_stamped(Probe(
                    cj.name, statement, "unknown", route=None,
                    note=f"{note}; prerequisite {name!r} matches claims "
                         f"under {', '.join(keys)}; qualify it "
                         f"({keys[0]}.{name})",
                    meta={"mathema.premise": "ambiguous-reference"}), cj))
                continue
            missing = [name for name, _ in refs
                       if name not in in_batch and name not in external]
            if missing:
                named = ", ".join(repr(m) for m in missing)
                hint = ("; " + "; ".join(hints)) if hints else ""
                out.append(_stamped(Probe(
                    cj.name, statement, "unknown", route=None,
                    note=f"{note}; prerequisite {named} is not a claim "
                         f"in this batch, nothing to rest this claim on"
                         f"{hint}",
                    meta={"mathema.premise": "missing-prerequisite"}), cj))
                continue
            resolved = [(name, wanted,
                         next(p for p in out if p.name == name))
                        for name, wanted in refs if name in in_batch]
            resolved += [
                (name, wanted,
                 Probe(name, name, external[name]["verdict"],
                       note=external[name].get("provenance", "")))
                for name, wanted in refs if name in external]
            unmet = [(name, wanted, ref) for name, wanted, ref in resolved
                     if not (ref.verdict == "proven" if wanted == "proven"
                             else ref.verdict in ("proven", "holds"))]
            if unmet:
                name, wanted, ref = unmet[0]
                out.append(_stamped(Probe(
                    cj.name, statement, "unknown", route=None,
                    note=f"{note}; prerequisite {name} is "
                         f"{ref.verdict}, not {wanted}, nothing to rest "
                         f"this claim on",
                    meta={"mathema.premise": "unmet-prerequisite"}), cj))
                continue
            # the weakest lemma bounds the conclusion; an external
            # premise is named by its provenance so the cap says whose
            # word it rests on
            empirical = [
                (external[name].get("provenance", name)
                 if name in external else name)
                for name, _, ref in resolved if ref.verdict == "holds"]
            if empirical:
                verdict_cap = ("holds", ", ".join(empirical))
            discharged = lemmas
            assumption = None
        elif assumption is not None:
            statement = f"assuming {assumption[1]}, {statement}"
            cj = _dc_replace(cj, assuming=f"assuming {assumption[1]}")
        validated = _validate_claim(cj, statement, note, facts, domain, fn=fn)
        if isinstance(validated, Probe):
            # a rejected claim has no canonical form (it was never a
            # claim), so its record keeps what was written, verbatim
            out.append(_stamped(validated, cj, canonical=False))
            continue
        ctx = validated
        if assumption is not None:
            ctx.assumption = assumption[2]
            ctx.assumption_display = assumption[1]
        elif discharged:
            # what the lemmas establish is available to this proof, not
            # just the fact that they were established
            lent = _lemma_conjuncts(discharged, cj, ctx.cj_domain)
            if lent:
                ctx.assumption = lent
                ctx.assumption_display = ", ".join(
                    f"{r.lhs} {r.relation} {r.rhs}" for r in lent)
        ctx.assume_defined = defined_mode
        ctx.premise_structures = premise_structures
        ctx.companion_mode = (
            "math_only" if math_only else
            "spawn" if float_companions and cj.route in ("derive", "best")
            else None)
        ctx.companion_budget = trials
        def stamp(probe, _cap=None):
            # `condition` is rendered text that gets read back,
            # docsync compares a verified row by feeding
            # f"{condition}, {statement}" through the claim grammar,
            # so it may only ever hold what the grammar accepts. An
            # assumed region reaches it the way a declared one does:
            # the premise narrows the quantified interval itself
            # (symbolic._prove._tighten_domain_by_assumption), and the
            # premise text rides in the statement.
            probe = _stamped(probe, cj)
            if _cap and classify_verdict(probe.verdict) == "proven":
                # a claim can be no better established than what it
                # rests on: resting a proof on a lemma that is itself
                # only empirically supported makes this evidence too,
                # whichever route reached it. Stated in the note and in
                # meta, never applied silently.
                capped_to, ref_name = _cap
                probe.verdict = capped_to
                probe.note = (f"{probe.note}; rests on {ref_name}, whose own "
                              f"evidence is empirical (holds), capped to "
                              f"{capped_to}").lstrip("; ")
                probe.meta = {**(probe.meta or {}),
                              "mathema.capped_by": ref_name}
            return probe
        if cj.route not in ("derive", "best", "probe", "examine"):
            out.append(_stamped(Probe(
                cj.name, statement, "skipped", route=None,
                note=f"unknown route {cj.route!r}"), cj))
            continue
        # the family is resolved for every concrete route: the derive
        # stage reads its derive half, and the probe stage reads its
        # probe:algorithmic half, a plain route="probe" claim on a
        # family-owned name reaches the family's own empirical
        # technique rather than the generic sampling loop
        ctx.family = _claim_family(cj, fn, facts)
        emptied = _empty_premise_parameter(ctx, facts)
        if emptied is not None:
            out.append(stamp(Probe(
                cj.name, statement, "skipped", route=None,
                note=f"{ctx.note}; the premise ({ctx.assumption_display}) "
                     f"admits no value of {emptied} in its declared "
                     f"domain, so the claim quantifies over nothing and "
                     f"is vacuous; state a premise the domain can "
                     f"satisfy",
                meta={"mathema.empty_premise": emptied})))
            continue
        if cj.relation == "=:=":
            # function equivalence has its own ladder (form hash ->
            # symbolic difference -> code-vs-code sampling); neither
            # generic stage applies
            out.append(stamp(_adjudicate_equivalence(ctx, fn, facts)))
            continue
        if cj.route in ("derive", "best", "examine"):
            # route="best" IS the cascade: its derive attempt engages
            # the extensive ladder inside the same try_prove call (the
            # fast attempt runs once; the ladder only starts where it
            # left off), so nothing is ever re-derived on the way down.
            # "examine" cascades the same way: structural half first,
            # empirical half when structure can't establish the fact.
            derived = _adjudicate_derive(
                ctx, fn, facts,
                extensive or cj.route in ("best", "examine"))
            if derived is not None:
                out.append(stamp(derived, _cap=verdict_cap))
                if ctx.companion is not None:
                    _emit_companion(out, _stamped(ctx.companion, cj),
                                    derived.name)
                continue
            # route == "best" and the derive stage couldn't settle it:
            # fall through to the probe stage, same as an ordinary
            # probe claim.
        probed = _arbitrate_empirical_fallback(
            _adjudicate_probe(ctx, fn, facts, kinds, _sampling), ctx)
        out.append(stamp(probed, _cap=verdict_cap))
    out.sort(key=lambda p: _emit_position(p, conjectures, declared_order))
    return out

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 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).

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 == "sequence" for k in facts.param_kinds.values()):
        return None

    _sp, _sc = _method_ctx_fields(fn, facts)
    ctx = _ctx or _LiftCtx(globals_ns=getattr(fn, "__globals__", {}),
                           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, 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 == "sequence" 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=getattr(fn, "__globals__", {}),
                           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)

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.

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) -> 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."""
    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)
    if (result.status == "disproven" and tolerance is not None
            and result.meta.get("mathema.exact_disproof")):
        # a declared tolerance is part of the claim: a difference below
        # it disproves nothing
        return ProofResult(
            "undecided",
            sketch=(f"{result.sketch}; within the declared tolerance "
                    f"({tolerance:g}), so not a disproof of this claim"))
    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:
        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 == "sequence"]
    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 == "sequence"]
    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=getattr(fn, "__globals__", {}), 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 = inspect.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 = getattr(fn, "__globals__", {})

    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, or this function's file wasn't in it), 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, or this
    function's file wasn't in it), never conflate that with False."""
    if coverage_data is None:
        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.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: 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: 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."""
    return hashlib.sha256(form_text(normalized(fdef)).encode()).hexdigest()[:12]

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. Turning one into compilable source in another language is not part of this module, and nothing here emits foreign 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. 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 = 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. `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 "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:
            coords = ", ".join(f"{n}={point[n]:.6g}" 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 language-tagged key (`ts:src/ema.ts#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)
        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`.")