`mathema describe`¶

The read-only look at what mathema sees in your code. Nothing is adjudicated, nothing is written, and no claim is checked: describe answers "what is here, and what does mathema make of it" before you commit to the cost of check or verify.

mathema describe TARGET... [--root .] [--tier NAME|1-5] [--depth 3]
mathema describe TARGET --issue [--include-source] [--include-falsified]

Two modes, chosen by the target¶

A target that resolves to exactly one function (a full dotted key like funcs.midpoint, or the module:name shorthand) prints that function's detail view. Anything else, a package, a module, several targets, lists every function found, one per line, with its rendered signature. With the tutorial project's funcs.py:

def settle(x: float) -> float:
    """Settlement amount for a signed exposure x."""
    return x


def midpoint(a: float, b: float) -> float:
    """The midpoint of two values."""
    return (a + b) / 2.0

mathema describe funcs

funcs.midpoint(a: float, b: float) -> float
funcs.settle(x: float) -> float

2 functions found

That list is deliberately lighter than mathema audit: no declared-claims lookup, no coverage report, no docstring scoring, no derivability analysis. It is discovery plus a signature, which makes it the cheap way to check that a target string resolves to the functions you meant before pointing an expensive verb at it.

The detail view¶

Here the tutorial's claims/demo.claims.yaml also gives midpoint a mean_bound claim:

funcs.settle:
  claims:
    - name: nonneg
      statement: "for x in [-5, 5], f(x) >= 0"
      route: probe
    - name: symmetric_in_sign
      statement: "for x in [-5, 5], f(x) == f(-x)"
      route: probe
    - name: negative_exposure_negative
      statement: "for x in [-5, -1], f(x) <= 0"
      route: probe
funcs.midpoint:
  claims:
    - name: commutative
      statement: "f(a, b) == f(b, a)"
      route: derive
    - name: mean_bound
      statement: "for a in [0, 1], b in [0, 1], f(a, b) <= 1"

and after one sweep:

mathema verify --root .

$ mathema describe funcs:midpoint
funcs.midpoint(a: float, b: float) -> float
  sig_hash:  6e64b8a7a1f0
  form_hash: py:54265556347f

Domains:
  (none inferred)

Claims:
  commutative: f(a, b) == f(b, a)  [proven]
    latex: f{\left(a,b \right)} = f{\left(b,a \right)}
  mean_bound: for a in [0, 1], b in [0, 1], f(a, b) <= 1  [proven]
    latex: \forall a \in \left[0, 1\right],\ b \in \left[0, 1\right]:\ f{\left(a,b \right)} \leq 1

Concepts: symmetry

The two hashes are the identity a record binds to: form_hash over the function's structure (a rename or a reformat leaves it alone, a behavior change does not) and sig_hash over its parameter shape. Domains are listed with the source each was inferred from, so a domain that came from a claim is distinguishable from one read off a guard in the code. Claims come from the declared and verified layers together, each showing its verified verdict when a record exists for it.

Below the claims, the detail view may print careful: lines: edges mathema knows about that lie just outside a domain the function declares, where a claim over that domain passes but a slightly wider one would not. A function calling np.exp(x) with a claim over [0, 700] gets careful: numpy.exp overflows past x = 709.78 (the domain stops at 700). The edges are a covered library call's overflow-safe region (from its compendium), a restricted builtin's range (sqrt needs x >= 0), and a pole of the lifted body, and an edge is shown only when it lies within a factor of 10 of the nearest bound, or within 1 of a bound near zero. A claim whose recorded verdict is falsified contributes no line, since its domain does not pass. The lines are information only: they are never a verdict, never gate anything, and appear nowhere but describe, not in check, verify or the record.

The tier ladder¶

The detail view then prints the same function at each of five tiers, which is the derive route's own pipeline made visible:

Tier	Name	What it shows
1	`source`	the function body as written
2	`normalized`	parameters renamed to positional `v0`, `v1`, ...
3	`structural`	the statement skeleton with expressions dropped
4	`lifted`	the sympy expression tree the body lifted to
5	`canonical`	that tree simplified

With --tier, the header above is followed by that one tier alone (shown here without the header):

$ mathema describe funcs:midpoint --tier lifted
--- lifted ---
Add
    Mul
        Half(1/2)
        Symbol(a)
    Mul
        Half(1/2)
        Symbol(b)

--tier takes either the name or the ladder position (--tier 4 is --tier lifted), and without it all five print in order. A tier that is unavailable prints its own real reason rather than a silent gap, which is usually the fastest way to see where in the pipeline a function stops being derivable, if lifted reports a blocker, the matching reason code explains it and says whether it is actionable. --depth controls how far callees are inlined while building the ladder (default 3).

`--issue`¶

A structured failure report for exactly one function, printed and then offered for writing under .mathema/issues/:

mathema describe funcs:settle --issue

It collects the reason codes, the blocked constructs, and the claim state into one payload you can paste into a bug report. --include-source adds the function's source to that one payload and is never remembered between runs; --include-falsified widens the report to an undiagnosed falsified claim, where the default covers only skipped ones. Declining the write, or running it on a function that turns out to be perfectly derivable, is a normal outcome and exits 0. It never makes a network request: the payload is yours to send, or not.

Arguments¶

Flag	Meaning
`target`	importable module, package, or `module:function` name(s), the same convention as `audit`
`--root`	project root to import targets relative to (default: the nearest ancestor holding `.mathema/` within the enclosing git repository, else that repository, else `.`; never the home directory)
`--tier`	narrow the ladder to one tier, by name or by position 1-5 (single-function mode only)
`--depth`	callee-inlining depth for the ladder (default 3, single-function mode only)
`--issue`	build the structured failure report for one function
`--include-source`	with `--issue`: include the source in this one payload
`--include-falsified`	with `--issue`: also report an undiagnosed falsified claim

Exit codes¶

describe reports rather than gates, so a successful run is always 0, including the run that finds no functions at all. A target that does not resolve exits 2, like every other verb (see exit codes).

mathema describe¶