mathema 0.6.1

• Documentation: https://mathema.tetrionlabs.com
• Install: pip install "mathema[all]" (recommended, with numpy, z3, MCP, coverage and mathema-language) or pip install mathema for the core alone; Python 3.10 to 3.14

What a record now shows

• Mathematics and computation are separate lines: derive proves a claim over the reals, and the [float] companion and the probe show what the code does in float64, where a raise, a NaN from non-missing inputs or an infinity from a finite input is no value and fails every relation; the computation's infinity resolves at the claim (let |inf| be), the function (pseudo_infinity: in a claims file, check(fn, pseudo_infinity=)) or the project (MATHEMA_PSEUDO_INFINITY), else the float maximum.
• A claim's headline is falsified when any line under it is falsified, mathematics or computation, and otherwise it is the weakest line; a falsification on the mathematics line carries an exact witness checked independently of the solver that found it, or one certified by interval arithmetic where the point cannot be written exactly (tan at pi/2).
• One allowance governs every comparison of a computed result against the exact one (the probe, the [float] companion, the exhaustive sweep, a witness re-run, the exact re-check and is_numerically_stable), and its input-rounding part never exceeds the relative part of the result, so a float result of 0.0 for an exact 1.0 at inputs of 1e16 is falsified on the computation line; at such a miss the record names the condition number and says whether the loss is inherent to the inputs or the code's, offering a narrower domain or accepting the discovery.
• Every sequence and table column meets its magnitude corners on both routes, the opposite-sign pair at the largest double included, and a decimal literal in a claim is its exact written value on the mathematics line, never rounded.
• A domain renders what it admits, [0.0, 1.0] : float|missing in ASCII and [0.0, 1.0] ⊂ ℝ ∪ {∅} in unicode: a value is absent (absent, Python's None) when the object is not there, and missing (missing, ∅) when one slot holds no computable value (nan, NA, null, NaT); a type clause states exactly what is admitted, and a binding without one is completed from the annotation.
• The record says in one sentence what the function did at each missing input (at x = nan f gave nan back, at x = None f raised TypeError), keeps in meta["mathema.missing"] the calls it made with the real value each word stands for (None, nan, pd.NA, each tried at least once, the degenerate containers first: empty, constant, length one, all-missing, a hole at the first and last position, a rank-deficient matrix), and counts draws as (43 draws) or (257 entries across 57 draws, sizes (1, 1) to (8, 1)).
• Every witness names its arguments (x = nan, alpha = 0.5), a large vector or matrix prints as its shape, first row and count, a string with invisible characters is followed by its escaped form, a record with a default repr shows its public fields, a witness too deep to print is summarised, and a recorded witness, one found by the exhaustive sweep included, is executed against the function and replays as the value that broke the claim.
• One effects: line under the function states what it writes or reads outside its arguments ("writes logs/app.log, reads os.environ", or "no side effects with default values"), and an automatic check mathema chose not to run leaves no row at all.
• Every remedy and "possible fixes" line puts its condition first and the claim or command last, after a colon ("(i) if nan for no data is intended, state: mean_ret([]) in {missing}").
• A lexicon row with an example function renders and round-trips as that function completes it (for n in N against n: int stays N), in lexicon.show, the golden snapshot and every lexicon_problems check; a row without one renders the unannotated default.

Soundness

• A policy claim states what a function does with a value that is not there, missing(f, x) propagates, absent(f, x) raises(TypeError), missing(f, xs, null) drops, with an optional premise (assuming count(xs) >= 1, ...); mathema writes one for every parameter that admits such a value and checks it, mathema claims KEY lists them, and --write puts them in claims/policies.claims.yaml.
• A value claim is judged wherever the function returns a value and never where it returns a missing value; a raise at a missing input that no claim accounts for, and a policy row the code contradicts, are falsified and fail verify and check, and mathema accept KEY missing[x] --as discovery --corrected "..." retires one with its witness.
• is_missing_safe(f) is about holes and is_absent_safe(f) about absence; a gate is proven only when every admitted member's policy comes from the code, a library's row, or a stated and confirmed claim, and an undeclared None return fails is_absent_safe(f).
• Along a path, where the None sits decides the kind: a field or key holding None is absent (null), a key left out or an index past the end is absent (unset), a list element holding None is a hole (null); \ {null} and \ {unset} narrow a path binding, and a path has its own policy row (absent(f, d.note, unset) drops).
• The empty input is judged strictly: a nan or None returned for [] is no value and falsifies the claim's empty-input line unless the author states the intent with an ordinary claim (f([]) in {missing}, raises(f([]), E), f([]) == 0) or guards it in the code, and a claim whose binding or premise excludes [] has no empty-input line.
• A value claim that binds no domain for a parameter is read over the working domain the function's own guards leave (a conditional raise, @enforce_domain(), @enforce_dimensions()), stated in the record's note, a literal passed in one call no longer pins that parameter for derive's domain, and a claim whose guards refuse every input is unknown (no valid domain), never a vacuous proven.
• is_representation_safe judges an excluded spelling (2.0 for n: int) on agreement with the in-domain value and with the declared return type, so a float returned where the function declares -> int falsifies it, with that as the stated reason.
• =:= says two functions are the same, so they agree where both give no value of one kind at the same input (nan and nan, None and None) and disagree where one gives a value and the other none; an absence agrees with an absence under == and ~= too, an undeclared None return is the absence line's own finding, and a value claim against a value still treats a nan from present inputs as agreeing with nothing.
• A raises(...) claim over a finite domain is proven by calling the function at every point, two results compare by their values whatever their leaves are (so a filter that drops a row falsifies f(xs) == xs with a witness), and a bare oo, inf, infinity or ∞ is infinity on the probe route as well, so f(x) < oo on a finite function holds instead of being falsified at a random value.
• A str parameter has the type fact : str (: str|absent when it is Optional), a non-string is outside its domain, a bare check carries an absent[p] row for every Optional parameter, and the numeric families (representation, pole, number set, overflow, numerical stability) never run on a string, a bool or a kind they do not understand; before, a string with no stated domain was falsified on numbers drawn for it.
• Literal[...], a str Enum and a guard to a set (if side not in {"buy", "sell"}: raise) read as the finite set {"buy", "sell"}, checked member by member and provable, a mixed function is split into one case per member, and an Enum parameter is called with its member and its spelling checked (f("buy") against f(Side.BUY)).
• Fixed: an integer result too large for a float is compared exactly (f(n) == 2**n over [0, 2000] is proven); a finite set with a missing value, a complex domain bound and a language with no member no longer raise out of a check; Optional[str] is read as a string parameter.

Claims and grammar

• a ~= b means abs(a - b) <= ε, with ε the claim's declared tolerance or else 1e-9, decided exactly on the mathematics line and in float64 on the computation line; the record says how it read the claim, and a premise assuming a ~= b reads the same way.
• A pin is written in the call: let alpha be 2, for x in R^n, f(x) == 2 * x[0] reads for x in R^n, f(x, alpha=2) == 2 * x[0], and the let form is still accepted as input.
• An int annotation completes a binding that states no type, so for n in [0, 10] on n: int is for n in [0, 10] : int on every route, and a type the claim states wins in either direction ([0, 10] ⊂ R widens, : int narrows).
• A dimension written as a number (for A in R^(30,15), for xs in [0, 1]^30, Mat(30, 15), Vec(30), or mixed as R^(n,15)) is drawn at that size on every route, a value of another shape is outside the domain, excluded_outside_domain(A) tries every shape just outside the space, and the rows shape and shape_enforced are now result_dimensions and dimensions_enforced, with size_enforced new.
• A norm is written with double bars, ||x||, ||x||_1, ||x||_2, ||x||_inf (also _oo, _∞), ||x||_p for a whole p >= 1 and ||x||^2, in unicode ‖x‖, ‖x‖₂, ‖x‖∞; a claim keeps its bars in the claims file, is the same claim as the norm(...) spelling, and derive proves vector norms, lengths, distances and normalisations for every length.
• sum, mean, std, var, min, max, prod, median, quantile, dot, cumsum, cumprod and count in a claim read a vector's values with missing left out: over no value sum is 0, prod 1, count 0, dot and norm 0, the rest are missing, and len counts every position.
• Two relations, in and not in (∈, ∉): `f(s) in ...

mathema 0.6.0

First public release.

mathema verifies claims about Python functions against the real code: a claim is proven where the mathematics permits, sampled where it does not, and the result is recorded as proof, evidence or an open question, bound to the exact code that earned it.

• Documentation: https://mathema.tetrionlabs.com
• Install: pip install mathema (Python 3.10 to 3.13); extras mcp, smt, numpy, symbology, coverage, or mathema[all]
• Licence: Business Source License 1.1, converting to AGPL-3.0-or-later four years after this release; see LICENSING.md for the plain-language version

0.6.0 is the first public version number rather than 0.1: the package is pre-1.0 and feature-complete for its current scope, the claim grammar and record format are settled by the claim-driven-development specification, and the Python API may still change before 1.0.