Execute provably-correct mathematics with evidence trails

MathKernel

An evidence-aware multi-engine mathematics kernel - usable both as a Python library (mathkernel) and as an MCP server (mathkernel-mcp) - so applications and LLMs can do advanced mathematics while preserving assumptions, provenance, and claim-specific evidence.

The LLM interprets intent; the MathKernel establishes mathematical evidence.

Mathematical results carry an explicit trust level, an engine tag, and a derivation trail. Exact computation, checked certificates, symbolic results, certified enclosures, empirical evidence, and formal proofs are distinct claims. Exact arithmetic alone is not a formal proof; approximate-input ancestry must not silently disappear.

The current development line is Beta. Optional engines and Studio have
separate availability and validation boundaries; the package classification does
not certify every backend, platform, or mathematical claim.

Table of contents

• Why
• Architecture
• Feature matrix
• Installation
• Quickstart - MCP server
• Quickstart - Python library
• Trust model
• External formal-project audits
• Continuous symbolic mathematics
• Finite dynamics & PRNG analysis
• Engineering mathematics
• Geometry and topology
• Statistics and stochastic modeling
• PDEs and adaptive finite elements
• Relation and information-geometry inference
• Performance: numba · CUDA · parallelism
• Visualization & portable artifacts
• Shared multimodal projections
• Scientific sonification
• Unified multimodal artifacts
• MathKernel Studio
• MCP tool surface
• Configuration
• Repository layout
• Skill packages
• Testing
• Safety boundaries
• License

Why

LLMs are good at mathematical intent and bad at mathematical arithmetic. MathKernel inverts the division of labor: the model parses, plans, and interprets; the kernel computes and records claim-specific evidence. Some claims use independent certificates or cross-checks; others are exact computations in one engine. Engine agreement alone is not a proof, and a single trust label does not replace the evidence bundle.

Architecture

MathKernel is a typed orchestration layer rather than a single solver. The public
facade owns parsing, contexts, object identity, persistence, evidence composition,
resource policy and derivation tracking; domain adapters own the actual mathematics.
Presentation layers sit downstream and cannot silently change the claim being made.

Python / MCP
    |
    v
MathKernel facade
    |-- parser + contexts + typed objects
    |-- execution/evidence contract
    |-- persistence + derivation graph
    |
    +--> symbolic / exact / certified / formal / numerical engines
    |
    +--> MathResult and derived mathematical objects
             |
             +--> MultimodalProjection
                     |--> mathkernel-viz
                     |--> mathkernel-sonify
                     +--> unified portable artifacts

This separation is deliberate: a renderer may present evidence, but it does not create
stronger mathematical evidence merely by producing a polished plot or audio artifact.

Feature matrix

Typed functionality surface

The generic MCP tools math_object_create, math_object_get, and math_apply
expose the following compositional operations. This is the full typed-operation
inventory; math_capability_query is the live source of parameter schemas,
output types, limits, engines and verification methods.

Source objects use the same boundary: transform/complex/probability objects,
graphs and combinatorial structures, finite groups/rings/fields/modules,
signals/filters/control systems, optimization problems, and Manifold →
Chart → Metric/CoordinateMap/TensorField/DifferentialForm, plus
Point/PointSet/Polygon/Polytope/Triangulation, and finite
SimplicialComplex/CubicalComplex/integral ChainComplex, and typed
StatisticalSample observations, GeneralizedLinearModel specifications, and
SurvivalDataset/CoxProportionalHazardsModel survival sources, plus
TimeSeriesDataset/TimeSeriesModel ordered-time sources, and
PoissonProcess/WienerProcess/GaussianProcess/ContinuousTimeMarkovChain
process-law sources, StochasticDifferentialEquation Itô models, and structured
PDEProblem equations/domains/conditions.
NonparametricTestResult, ResamplingResult, KaplanMeierEstimate, GLMFit,
and CoxPHFit are derived-only, source-linked records with deterministic exact,
numerical, or seeded-stream replay. TimeSeriesAnalysis, TimeSeriesFit, and
TimeSeriesForecast, FiniteDimensionalDistribution,
GaussianProcessPosterior, and CTMCTransition follow the same output-only
replay boundary. PDEClassification, PDECompatibilityReport, and WeakForm
replay their principal-part, represented-trace, or complete weak-identity result
from the source problem. FEMMesh links that weak form and an optional verified
triangulation. ReferenceElement, BasisFunctionSet, QuadratureRule, and
FiniteElementSpace are output-only with replayable single- or multi-source
ancestry. AssembledSystem retains local and sparse global contributions plus
its space/quadrature sources; output-only FEMSolution retains the exact
assembled-system source and replayable solver diagnostics. G.5 output-only
FEMErrorEstimate, RefinementMarking, RefinedMesh, MeshTransfer, and
FEMConvergenceObservation records retain the complete solution-to-child-mesh
chain, marking policy, parent/child cells, interpolation weights and empirical
rate inputs.
SDESimulation and SDEConvergenceStudy additionally replay
their PCG64 streams and discretizations. Derived-only types cannot be forged through
public input.

Installation

pip install mathkernel           # Python mathematical core
pip install 'mathkernel[mcp]'    # add the optional MCP transport

From a source checkout:

python -m venv .venv
source .venv/bin/activate        # Windows: .venv\Scripts\activate
pip install -e .           # Python mathematical core
pip install -e '.[mcp]'  # add the optional MCP transport

Optional extras:

pip install -e '.[perf]'    # numba — JIT kernels (sieves, GF(2^m), FWHT, closure search)
pip install -e '.[cuda]'    # CuPy + all nvidia-*-cu12 runtime libraries (RTX-class GPU)
pip install -e '.[latex]'   # antlr4 runtime for math_parse_latex
pip install -e '.[dev]'     # pytest

Lean 4 + Mathlib is optional and requires explicit operator setup. MCP startup,
capability discovery and proof calls never download or repair a toolchain.
Without a healthy local installation, formal checks report unavailable.

mathkernel-lean-setup --check   # local version, runtime and Mathlib proof check
mathkernel-lean-setup           # explicitly download the pinned toolchain
mathkernel-lean-setup --repair  # stage and verify a fresh managed installation

Setup requires Git, allows one hour by default (--timeout), and checks for
8 GiB free in MATHKERNEL_LEAN_CACHE before downloading (--min-free-gib).
This is a preflight check, not a disk quota; installation uses several GiB.
Failed setup removes its partial generation, and interrupted setup is cleaned on
the next setup invocation. Repair preserves the active generation until the new
one passes a real Lean/Mathlib proof check. A failed binary-cache download stops
unless --build-from-source was explicitly selected. Custom Lean paths are
read-only to this installer; repair those with their own installation manager.
MATHKERNEL_LEAN_BINARY must point to a real installed Lean binary, not an elan
proxy. MATHKERNEL_SKIP_LEAN_INSTALL=1 additionally blocks explicit setup unless
--force/--repair is supplied; setting it to 0 does not enable automatic setup.

GPU note: CuPy wheels ship no CUDA libraries. The cuda extra installs the
matching nvidia-*-cu12 pip packages - without them, cuBLAS/NVRTC DLL loads fail
even though import cupy succeeds. GPU availability is probed at runtime with a
real matmul, so a broken stack degrades gracefully to CPU. Verify your stack with
python scripts/gpu_smoke.py.

Quickstart - MCP server

mathkernel-mcp

The server speaks MCP over stdio (FastMCP 3) and ships core instructions to the
client at initialize time: discover → parse → context → trust discipline → async jobs
→ provenance. 162 tools, all prefixed math_.

Typical agent session:

math_capabilities                                   # discover surface, limits, engines
math_parse("x^2 - 3*x + 2 = 0")                     # -> expr_id
math_context_create(domains={"x": "real"})          # -> context_id
math_reason(expr_id, context_id, formal=true)       # solve + independently verify
math_derivation_trace(step_id)                      # full provenance on demand

Long-running sweeps are async:

math_job_submit("collatz", {"n_max": 14})  ->  math_job_status(job_id)  ->  math_job_result(job_id)

Quickstart - Python library

The MCP server is a thin transport layer; everything is available in-process:

from mathkernel import MathKernel

kernel = MathKernel()

# symbolic
r = kernel.parse("x^2 - 2 = 0")
sol = kernel.solve(r.data["expr_id"], "x")
assert sol.ok and sol.trust.value == "symbolic"

# exact GF(2^m) field arithmetic
f = kernel.gf2m_create(8, "1b")  # AES polynomial x^8 + x^4 + x^3 + x + 1 (hex reduction part)
kernel.gf2m_compute(f.data["field_id"], "mul", ["53", "ca"])

# finite dynamics: an explicit eight-state cyclic permutation
transition = [1, 2, 3, 4, 5, 6, 7, 0]
fs = kernel.finite_system_create("uniform", transition)
km = kernel.koopman_matrix(fs.data["system_id"], {"kind": "walsh", "r": 3})
vis = kernel.koopman_visibility(fs.data["system_id"], {"kind": "walsh", "r": 3})
# Exact zeros certify the requested modes in this declared finite model.

# closure relations (njit meet-in-the-middle)
kernel.closure_search("cyclic", m="97", weight_bound=10, multipliers=["1", "5"])

Standalone modules (mathkernel.gf2m, mathkernel.koopman, mathkernel.relations,
mathkernel.cumulants, mathkernel.finite_fourier, mathkernel.transforms,
mathkernel.integral_transforms, mathkernel.complex_analysis,
mathkernel.continuous_probability, mathkernel.integers,
mathkernel.computational_geometry, mathkernel.algebraic_topology,
mathkernel.collatz, mathkernel.cuboid) are usable without the facade when
you don't need derivation tracking.

Trust model

formal                  Lean certificate accepted by the Lean kernel
exact                   exact computation / checked claim-specific certificate
symbolic                symbolic engine agreement (e.g. SymPy residual checks)
interval_certified      rigorous enclosure (mpmath interval)
numeric_high_precision  arbitrary-precision numeric
numeric                 float evidence (incl. GPU fast paths)
empirical / heuristic / unknown

Overall trust is limited by the weakest evidence required to establish the claimed
result. Required dependencies within a support path are conjunctive; independent
paths can establish the same conclusion at different strengths. Declined verifier
attempts remain diagnostics and cannot lower a successful independent result.
Unknown required dependencies still limit trust. Counterexamples take precedence
over successful proof attempts; the conflicting attempts remain visible.

Every MathResult also carries an evidence_bundle with separate computation,
proof, certificate, numerical, model and empirical evidence. claim_evidence
retains those bundles per conclusion instead of flattening unlike claims into one
score. The legacy trust field remains a conservative summary and is automatically
capped by the evidence required for the result. A producer-supplied
justified_trust is a ceiling, never an override; an unverified proof or certificate
supports only unknown.

prove_equivalence emits data.lean_certificate only after Lean accepts the script,
with a matching verified proof record. Unchecked scripts, when retained for an
unrefuted statement, appear only under data.lean_candidate with checked: false.
Already-refuted statements skip Lean and contain neither artifact.
Solution reasoning follows the same rule: candidate_certificates contains only
checked scripts; unchecked work is separated into candidate_attempts.

Semantic statuses distinguish proof or certification strength from mathematical
outcomes such as does_not_exist, undefined, infeasible and unsupported.
These distinctions survive MCP serialization, asynchronous job retrieval,
derivation replay, visualization and multimodal artifact assembly.

The capability registry separates advertised trust levels from verification
methods. Query it by domain, input/output type, operation, trust level,
verification method or engine; capability records also identify their execution
handler and meaningful cost dimensions. Expression plans record the resolved
capability route before the existing obligation executor runs it.

Exact and numeric paths are strictly separated: koopman/finite-dynamics tools default
to exact=true (proof-grade rational/cyclotomic values); exact=false selects the
vectorized numeric path (CuPy GPU when usable) and downgrades trust to numeric.

Decimal literals are approximate observations. A decimal (RealNode) anywhere in
an expression caps its trust at numeric from parse onward - 0.1 + x parses as
numeric, 1/2 + x as symbolic. Formal certificates (Lean) and exact SMT
proofs and counterexamples are refused for approximate inputs or assumptions, because the backends would encode
decimal syntax as exact rationals - silently proving a different statement. Use exact
rationals or interval certification when proof-grade evidence is needed.

External formal-project audits

mathkernel.formal_audit inspects external Lean projects without compiling them,
checks source/toolchain/dependency fingerprints, inventories lexical imports and
flags placeholders, unexpected axioms, native constructs and unsafe verification
configuration. Inspection results remain UNKNOWN: source-module reachability
is not proof-dependency reachability, and absence of sorry text is not proof.
The Python facade exposes formal_project_audit and formal_project_probe with
normal derivation/evidence tracking and output paging.

The mathkernel-formal-audit CLI provides inspect, fingerprint, probe and
operator-authorized replay. Replay requires a separate trusted reference,
pinned tools, a fresh Linux unprivileged sandbox and Comparator with nanoda. It
never pre-builds an untrusted submission. Successful checking supports only the
specified Lean statements and axiom policy; mathematical paper/definition
alignment remains a separate obligation. Live external-checker qualification
is still pending; mocked runner tests are not proof verification.

MCP exposes only read-only math_formal_project_audit and
math_formal_project_probe. Local project access is disabled unless the operator
sets MATHKERNEL_FORMAL_PROJECT_ROOTS before startup. Clients cannot enable replay
or change checker binaries through these tools.

certified_enclose evaluates coefficients and endpoint expressions directly in
an isolated mpmath.iv context, without point-rounding them first. Approximate
input or endpoint ancestry remains NUMERIC; unsupported domains return errors.
Closed exact rational inequalities can be refuted without optional SMT tools.

The formal-project audit guide
describes the trust boundary and deployment contract. The
Navier-Stokes audit example
contains pinned targets and reproducible local checks, not a claimed proof or
disproof of the full construction.

Continuous symbolic mathematics

Continuous domains use typed objects and the compositional
object_create → apply model rather than exposing a flat CAS surface.
Every operation records a four-obligation DAG: typed-input validation,
candidate computation, domain-invariant verification and conservative evidence
reconciliation.

• Integral transforms - Laplace, Fourier, Mellin and bilateral Z transforms
  with explicit conventions, assumptions and regions of convergence. Inverse Z
  uses annulus-aware Laurent/residue extraction when justified. Verification
  records round-trip, linearity, convolution, differentiation, value-theorem and
  ROC obligations separately; unresolved obligations remain unknown.
• Complex analysis - derivatives, analyticity candidates, zeros,
  singularities, Laurent series, residues, contour integration, winding numbers,
  argument-principle accounting, conservative identity continuation and
  domain-aware conformal maps. Branch conventions, cuts, excluded points,
  contour orientation and boundary incidents remain explicit.
• Continuous probability - typed univariate, random-variable, joint and
  conditional distributions; PDF/CDF/survival/quantile, moments, transforms,
  entropy, truncation, convolution, mixtures, divergence, marginals,
  conditioning/Bayes, covariance/correlation and order statistics. Support,
  parameter constraints, Jacobians and inverse branches are retained.

Symbolic availability is candidate evidence, not independent proof. Same-engine
identities are capped at symbolic; decimal ancestry remains capped at
numeric. does_not_exist (for example, a Cauchy mean) is distinct from an
unsupported method or an unresolved convergence question.

Conventions and assumptions are part of the object. Fourier sign and
normalization, transform source/target variables, complex branches/cuts,
probability supports and parameter constraints are never selected silently.
Contour orientation and singularity accounting are mandatory where the theorem
depends on them.

Verification is operation-specific. Transforms retain every checked or unresolved
identity and ROC obligation. Residues are compared with defining limit/derivative
or Laurent-coefficient formulas; contour claims retain enclosed singularities,
cuts and winding numbers. Probability verifies normalization, support-aware
nonnegativity, CDF boundaries/derivative/monotonicity when decidable, and
Jacobian branches. These are symbolic checks unless an exact certificate or
separate numerical record says otherwise.

Failures use semantic statuses: candidate, unknown, unsupported,
does_not_exist, and error are distinct. Known limitations include
non-product joint supports, continuation without an explicit overlapping source
domain, branch-sensitive argument-principle inputs, transforms whose ROC SymPy
cannot establish, and general multivariate changes of variables without supplied
inverse branches/Jacobians.

Continuous symbolic work is bounded by the global AST/output/solver-time limits
and dedicated contour, joint-dimension, mixture-component, series-order,
order-statistic and inverse-branch limits. Raise the corresponding
MATHKERNEL_MAX_* value explicitly when a larger request is intentional.

# PDF → Laplace transform, preserving support and evidence ancestry
d = kernel.object_create("Distribution", {
    "family": "exponential", "parameters": ["2"], "variable": "x",
})
r = kernel.apply(d.data["object_id"], "integral_transform", {
    "transform": "laplace",
    "transform_variable": "s",
    "convention": "laplace_standard",
})
assert r.data["value"] == "2/(s + 2)"

Finite dynamics & PRNG analysis

A distinctive capability: exact spectral analysis of finite dynamical systems
(X, μ, T, O) - built for (and validated on) PRNG structure analysis.

• Koopman suite - transport matrix Q, observation-transfer C, mode visibility
  ρ_O, lagged state tensors (raw/connected), observed statistics, IPR/entropy
  diagnostics. Walsh bases for GF(2)^r, character bases for Z_M.
• Stochastic observation transfer (library API) - exact
  FiniteJointLaw contractions for arbitrary finite latent joint laws; ordered
  Markov path moments/cumulants with the required multiplication operators;
  statewise multiplicativity-defect certificates; and exact finite-noise
  deterministic dilations for rational Markov kernels. The accompanying
  published primate quartet pilot deliberately records that the earlier K3ST
  split-zero diagnostic does not survive outside its group-based assumptions.
• Branching General Markov tensors (library API) - exact
  FiniteMarkovTree sum-product laws and cumulants on heterogeneous rooted
  trees; exact L M R edge-flattening certificates with the sharp transition-
  rank bound; local stochastic observation channels as Kronecker transforms;
  exact left-inverse recovery, collision witnesses, collective sensor fusion,
  and channel-conditioned singular-value bounds. The published primate pilot
  distinguishes algebraic identifiability from finite-sample stability.
• Statistical phylogenetic inference (library API) -
  probability-simplex projection; known-channel EM and constrained ridge
  recovery; held-out regularization selection; multinomial covariance and
  tangent-space Fisher information; nonnegative-rank multinomial likelihood;
  covariance-Wald rank diagnostics; and tie-safe quartet scoring. Controlled
  GM(4) experiments quantify the shared singular-value origin of visibility
  loss and inverse instability. Two fixed published-data pilots add site and
  moving-block bootstrap checks without claiming broad competitive accuracy.
• Frozen phylogenetic benchmarking (library API) -
  FASTA, relaxed PHYLIP, practical NEXUS and Newick ingestion; portable source
  SHA-256 manifests; canonical protocol and corpus locks; result-blind quartet
  sampling from reference-tree splits; complete-case site provenance; site,
  circular-block, partition-stratified and whole-partition resampling; rank-tail,
  p-distance and normalized log-det baselines; and tie-safe corpus summaries.
  The bundled execution evaluates 22 predeclared correlated units from two
  published source alignments and a 1,920-alignment known-truth stress grid. A
  separate lock fixes the first 20 eligible BenchmarkAlignments datasets before
  acquisition; that external corpus is explicitly pending rather than silently
  replaced.
• Observable connected-relation detection (library API) -
  exact and numerical pure-interaction laws; weighted conditional-expectation
  singular spectra; mode-specific stochastic visibility; exact local-channel
  transfer of connected amplitude; chi-square and null-Fisher information
  retention; exact invisibility certificates; finite necessary and constructive
  sufficient sample bounds; binary-parity scaling; and complementary sensor
  fusion. The controlled theorem shows that local visibility losses multiply
  in amplitude and square in information, yielding an s^(-2d) detection-cost
  law in the homogeneous binary specialization.
• Relation-subspace visibility and sensor design (library API) -
  finite multi-parameter local relation laws; latent and observed Fisher Gram
  matrices; generalized retained-information eigenvalues and principal
  visibility directions; exact observation-blind collision certificates;
  direction-level information and sample multipliers; rank, E-optimal, trace,
  D-optimal and pseudo-logdet sensor-subset selection; efficient empirical
  partition transfer; and score-mean long-run-covariance correction. A frozen
  SkewDB adapter adds source/schema auditing, discovery/validation/challenge
  splits by held-out taxonomy, discovery-only preprocessing, source hashing and
  a fail-closed raw-data runner. The bundled SkewDB fixture is explicitly
  synthetic because the current full payload was not acquired in this
  environment.
• Coordinate-invariant relation geometry (library API) -
  finite-simplex tangent vectors with the intrinsic Fisher metric; stochastic
  tangent pushforward; coordinate-invariant generalized retained-information
  eigenvalues; exact score/tangent equivalence; exact local chi-square transfer;
  worst-direction minimax necessary sample bounds; finite Bhattacharyya and
  retention-based pointwise sufficient counts; and iid, moving-block and
  cluster bootstrap intervals for ordered relation spectra. A SHA-256-locked
  local-resolution SkewDB adapter converts documented cumulative *_fit.csv
  tracks to window increments and explicitly separates genuine inputs from the
  bundled source-parameterized generated fixture.
• Finite Fourier - exact arithmetic in ℚ(ζ_L) via cyclotomic polynomials:
  DFT over Z_M, output-transfer transforms, two-point difference coefficients,
  measure Fourier transforms, orbit corrections.
• Closure search - short irreducible relations selected by the dynamics:
  cyclic (Σ k_j·a^j ≡ 0 mod m) and binary (⊕ (L^{jK})ᵀ w_j = 0),
  meet-in-the-middle with L1/Hamming weight bounds.
• GF(2^m) from transitions - reconstruct the field (dual-orbit cyclic basis,
  minimal/reduction polynomial, Rabin-verified) purely from a generator's
  GF(2)-linear transition columns.
• State-conditioned dynamics - exact per-state orbit access T^κ(x)(x):
  least-lag solving, symmetry-to-access conversion, cocycle composition,
  exhaustive additive closure proofs, symbolic affine access maps, GF(2)
  baby-step/giant-step orbit solving, sparse giant-lag predictive closures,
  and constrained symmetry discovery where numeric probing only ranks
  candidates - canonical-rewrite or exhaustive proofs decide.

The scripts/ tree contains uniform, end-to-end reproductions for 25+ generators
(xorshift/xoroshiro/xorwow families, MT19937, Melg19937, WELL19937a, MRG32k3a,
PCG32/64(+fast), LXM, SplitMix64, SFC64, JSF64, Romu, Philox, Threefry, RXS-M-XS),
each runnable from scratch with scripts/families/run_all.py and
scripts/companion/run_all.py. Reference data ships in scripts/data/ - no
external fixtures required.

Engineering mathematics

MathKernel provides typed engineering mathematics for signals, control systems and constrained optimization while preserving the same evidence and persistence contracts as the symbolic core.

Signals and spectra

Continuous and sampled signals carry explicit domains, sample grids and units. Spectral representations are typed rather than treated as anonymous arrays. FIR/IIR filters and filter designs retain coefficients, conventions and source signals, while immutable streaming state makes block-by-block processing replayable. Frequency-response and time-response operations record whether they used exact symbolic algebra or numerical evaluation.

Control systems

Typed SISO and MIMO models support state-space and transfer-function representations, continuous/discrete conversion, poles and zeros, stability checks, discretization, controller construction and observer construction. LQR, finite-horizon LQR, steady-state Kalman filtering, LQG composition and immutable Kalman prediction/update states retain plant/model ancestry and separate algebraic checks from modeling assumptions.

Constrained finite-horizon MPC keeps feasibility, optimality, terminal invariance, recursive-feasibility and stability claims separate. Frequency-domain analysis includes Bode, Nyquist and root-locus representations together with checked time responses.

Optimization and certificates

Linear and quadratic programs can return exact/checkable optimality witnesses where the supported fragment permits it. Infeasible LPs can expose Farkas certificates and unbounded problems can expose recession rays. MILP search results carry replayable proof trees rather than only an incumbent value. Conic and quadratic-constraint workflows support bounded SOCP/SDP product cones and Lagrangian-style certificates in their declared fragments.

External native candidate solvers are isolated in fresh processes with bounded requests and hard timeout termination. Candidate generation and certificate verification are distinct steps: a solver finding a point does not by itself establish a stronger claim than the verifier can check.

Geometry and topology

Differential geometry and tensor calculus

Immutable Manifold, Chart, and Metric objects feed typed GeometryTensor, Connection, and GeodesicSystem outputs. Metric operations compute inverse metrics, Christoffel symbols, Riemann/Ricci/scalar/Einstein curvature and affine geodesic equations. Exact symbolic checks cover inverse identities, torsion freedom, metric compatibility, Riemann symmetries, the first Bianchi identity and the contracted Bianchi identity. Chart domains and metric nondegeneracy conditions remain explicit.

Directional CoordinateMap objects carry explicit Jacobians and inverse-composition checks. Dense variance-aware TensorField objects and canonical sparse DifferentialForm objects support covariant and Lie derivatives, wedge products, exterior derivatives, interior products, pullbacks and Hodge stars. Checks include graded commutativity, d²=0, pullback commutation with d, metric compatibility, coordinate-map composition and the Hodge double-star sign when metric signature is supplied. Orientation and signature are never guessed.

Computational geometry

Point, PointSet, Polygon, half-space Polytope, Triangulation, and derived VoronoiDiagram objects provide exact orientation, incircle and segment-intersection predicates, monotone-chain convex hulls, winding containment, exact squared-distance nearest neighbors, certified ear clipping, convex polygon clipping, empty-circumcircle Delaunay triangulation and finite Voronoi duals with explicit unbounded rays. Decimal predicates use conservative floating-point error filters; when topology cannot be established, the result is explicitly ambiguous rather than promoted to an exact classification.

Algebraic topology

Exact finite SimplicialComplex, CubicalComplex, and integral ChainComplex objects expand cells to canonical face closures and derive oriented boundary matrices. Complexes verify boundary[k-1] * boundary[k] = 0 before homology is attempted. homology computes free ranks and integer torsion over Z through certified Smith-kernel/quotient reductions, and exact Betti numbers plus representative cycles over Q or GF(p). boundary_matrix, chain_complex, and euler_characteristic expose ordered bases and the Euler-Poincaré cross-check.

Verified exac...