core.math — Mathematics
The largest module in the stdlib — a 10-layer mathematical stack plus a substantial pure-mathematics branch. libm-free: every function is implemented in Verum on top of CPU intrinsics.
This page is an index of every layer and sub-module. Deep APIs (hundreds of functions per layer) are listed here in summary form; follow the source links for complete signatures.
Layer overview
Layer 9 Agents & LLM agent/ (tokenizer, KV cache, ReAct, RAG)
Layer 8 State-space models + distributed ssm/ distributed/
Layer 7 Neural networks nn/
Layer 6 Automatic differentiation autodiff/
Layer 5 GPU / accelerator gpu/
Layer 4 Tensor system tensor/
Layer 3 Numerical analysis & random calculus/ random/
Layer 2 Linear algebra (BLAS-style) linalg/
Layer 1 Scalar math constants/ elementary/ hyperbolic/ special/
Layer 0 Foundation ieee754/ integers/ bits/ checked/ libm/
Pure mathematics (parallel branch): algebra/, category/,
topology/, analysis/, logic/, hott/, cubical/,
simplicial/, infinity_category/, infinity_topos/,
kan_extension/, fibration/, model_category/, operad/,
number_theory/.
∞-topos foundations: quantum_logic/, giry/, epistemic/,
cohesive/, day_convolution/, sdg/.
Others: complex/, category_finite/, bitvec/,
observational/, examples/, internal/, simple/, advanced/,
tactics/.
Layer 0 — Foundation
math.ieee754
type FpCategory is NaN | Infinite | Zero | Subnormal | Normal;
f64_decompose(f: Float64) -> (sign: Bool, exp: Int, mantissa: UInt64)
f32_decompose(f: Float32) -> (Bool, Int, UInt32)
f64_compose(sign, exp, mantissa) -> Float64
f32_compose(sign, exp, mantissa) -> Float32
classify(f: Float64) -> FpCategory classify_f32(f: Float32) -> FpCategory
is_nan / is_infinite / is_finite / is_normal / is_subnormal
copysign(x, y) signbit(x) -> Bool
math.ieee754_deterministic
core.math.ieee754_deterministic is re-exported from core/math/mod.vr,
so mount core.math.ieee754_deterministic.{sqrt} resolves and compiles.
Every one of its twenty-one functions then panics on its first call.
Checked:
mount core.math.ieee754_deterministic.{sqrt};
fn main() { print(f"sqrt={sqrt(4.0)}"); } // panics — that IS the point
Panic: @intrinsic("verum.libm_deterministic.sqrt") is not implemented
in this build (called from sqrt); it has no registry entry
The module declares 42 verum.libm_deterministic.* intrinsic keys and
the runtime implements none of them:
grep -c '@intrinsic' core/math/ieee754_deterministic.vr # 42
grep -rl 'verum.libm_deterministic' crates/ --include='*.rs' # nothing
(grep -rl, not -rc: the counting form prints one path:0 line for
each of the 2442 files it looked at, which buries the answer it gives.)
Use math.libm instead, above — it is pure Verum and it runs. This
module exists for a future bit-exact cross-platform mode; the note stops
being true the moment a verum.libm_deterministic.* key gets a runtime
implementation.
math.integers
type DivMode is Truncate | Floor | Ceiling | Euclidean;
div_floor(a, b) div_ceiling(a, b)
div_euclidean(a, b) mod_euclidean(a, b) mod_floor(a, b)
div(a, b, mode: DivMode) divmod(a, b) -> (q, r)
gcd(a, b) -> Int gcd_binary(a, b) -> Int lcm(a, b) -> Int
extended_gcd(a, b) -> (gcd, x, y) // ax + by = gcd
mod_inverse(a, m) -> Maybe<Int>
mod_pow(base, exp, m) -> Int
math.bits
clz(x) / clz32(x) ctz(x) / ctz32(x)
popcnt(x) / popcnt32(x)
ffs(x) / ffs32(x) fls(x) / fls32(x)
highest_bit(x) / lowest_bit(x)
rotl(x, n) / rotr(x, n) rotl32 / rotr32
bswap(x) / bswap32 / bswap16
bitreverse(x)
math.checked
Overflow-safe arithmetic wrappers (thin layer over intrinsics, but using refinement types to document invariants).
math.libm
Pure-Verum libm. sin, cos, exp, log, pow, etc. — all
implemented on top of the bit-level primitives above. No C library
dependency. See the callout at the top of Layer 1 — the same-named
functions one layer up are currently affected by a stdlib
name-resolution defect; this module is entangled in the same
collision (it declares some of the same bare names) and has not been
independently verified.
Layer 1 — Scalar math
The recorded core.math.elementary controls use nonzero inputs to
distinguish the selected function from a default-valued result:
sin(1) 0.8414709848078965 cos(1) 0.5403023058681397
exp(1) 2.71828182442294 log(e) 0.9999999998112601
sqrt(2) 1.4142135623730951 exp2(3) 8
log2(8) 2.9999999999999996 log10(1e3) 3
pow(2,0.5) 1.4142135623730951 hypot(3,4) 5
log1p(1) 0.6931471805599453 expm1(1) 1.7182818244229399
Every one is the right number. The remaining departures are ordinary
precision, not a wrong callee: exp, expm1 and log land around nine
significant digits, which is this stack's pure-Verum implementation
rather than the platform's libm.
atan uses range reduction to preserve its (−π/2, π/2) range and
avoid the slow convergence of a short Taylor series near |x| = 1.
Recorded comparisons give:
input elementary atan reference
-2.0 -1.1071487177940904 -1.1071487177940906
0.999 0.7848979134744296 0.784897913314115
1.0 0.785398163562613 0.7853981633974483
1.001 0.785897913320462 0.7858979134807815
The recorded maximum error over [−40, 40] is 1.65e-10; this is a
bounded numerical control, not a guarantee over all floating-point inputs.
atan2 uses the same implementation.
Two atans, and the bare name is not the exact one. core.math.libm
delegates to an @intrinsic("atan2"), so it answers exactly;
core.math.elementary is pure Verum and answers to about 1e-10. A bare
mount core.math.* resolves to the ELEMENTARY one. Name the module when
the last digits matter.
Still open. asin(0.5) answers 0.523596119295823 against
0.5235987755982988 and acos(0.5) 1.0472002074990736 against
1.0471975511965976 — both off from the sixth decimal by the same
2.66e-6, while asin(0.1) and asin(0.9) are accurate to 1e-16 and
1e-10. The loss peaks in the middle of the range: both the series and
the half-angle identity it falls back on are weakest at exactly 0.5, so
moving the split between them does not help.
math.constants
Refinement-based semantic aliases
const PI: Float | |
const E: Float | |
const TAU: Float | |
const PHI: Float | |
const SQRT2: Float | |
const EPSILON: Float | |
const INFINITY: Float | |
const NAN: Float | |
type NonNegative is Float { self >= 0.0 } | |
type Positive | |
is Float { self > 0.0 } | |
type UnitInterval is Float { 0.0 <= self && self <= 1.0 } | |
type Probability is UnitInterval | |
type Angle | radians |
is Float |
math.elementary
// Trigonometry
sin(x) / cos(x) / tan(x) asin(x) / acos(x) / atan(x) / atan2(y, x)
sincos(x) -> (Float, Float)
// Exponentials & logs
exp(x) / exp2(x) / expm1(x) log(x) / log2(x) / log10(x) / log1p(x)
// Powers & roots
pow(x, y) / powi(x, n: Int) sqrt(x) / cbrt(x) / hypot(x, y)
// Rounding
floor / ceil / round / rint / trunc / fract
// Min/max/clamp
min(a, b) / max(a, b) / clamp(x, lo, hi)
abs(x) / signum(x)
// Fused operations
fma(a, b, c) // (a*b + c) with single rounding
lerp(a, b, t) // linear interpolation
inverse_lerp(a, b, x) -> Float // where x sits in [a, b]
remap(x, lo1, hi1, lo2, hi2) -> Float // remap x from [lo1, hi1] to [lo2, hi2]
smoothstep(edge0, edge1, x) / smootherstep(edge0, edge1, x)
// Safe variants — return Maybe<T>
sqrt_safe(x) / log_safe(x) / asin_safe(x) / acos_safe(x)
math.hyperbolic
sinh / cosh / tanh asinh / acosh / atanh
Most of this module's general-case paths are currently broken — see the callout at the top of Layer 1.
math.special
gamma(x) / lgamma(x) / digamma(x)
beta(x, y) / lbeta(x, y)
erf(x) / erfc(x) / erfinv(x)
Every function here calls into log/exp/sqrt/sin/cos — see
the callout at the top of Layer 1; treat this module as unverified
until that lands.
Layer 2 — Linear algebra
math.linalg
BLAS-style API. Types: Vector<T>, Matrix<T>, StaticVector<T, const N>,
StaticMatrix<T, const R, const C>, and the Numeric protocol.
// Level 1 (vector ops)
dot(a, b) -> T nrm2(a) -> T asum(a) -> T
iamax(a) -> Int // index of max |element|
scal(alpha, a) axpy(alpha, x, y) // y := αx + y
copy(src, dst) swap(a, b)
rotg(a, b) -> (c, s) rot(x, y, c, s)
// Level 2 (matrix-vector)
gemv(alpha, A, x, beta, y) // y := α A x + β y
trsv(upper, A, x) // triangular solve
ger(alpha, x, y, A) // A := α x yᵀ + A
syr(alpha, x, A) // symmetric rank-1
// Level 3 (matrix-matrix)
gemm(alpha, A, B, beta, C) // C := α A B + β C
trsm(upper, alpha, A, B) // triangular solve
syrk(alpha, A, beta, C) // symmetric rank-k
// Decompositions
lu(A) -> LUDecomposition<T>
qr(A) -> QRDecomposition<T>
cholesky(A) -> CholeskyDecomposition<T>
svd(A) -> SvdDecomposition<T>
// Solvers
determinant(A) -> T
inverse(A) -> Maybe<Matrix<T>>
solve(A, b) -> Maybe<Vector<T>> // Ax = b
Layer 3 — Numerical analysis & random
math.calculus
// Differentiation
forward_diff(f, x, h) -> Float
backward_diff(f, x, h) -> Float
central_diff(f, x, h) -> Float
// Integration
trapezoid(f, a, b, n) -> Float
simpson(f, a, b, n) -> Float
romberg(f, a, b, tol) -> Float
gauss_legendre(f, a, b, n) -> Float
// ODE solvers
euler(f, t0, y0, h, n) -> List<Float>
heun(f, t0, y0, h, n) -> List<Float>
midpoint(f, t0, y0, h, n) -> List<Float>
rk4(f, t0, y0, h, n) -> List<Float>
rk45(f, t0, y0, h_init, tol) -> List<(Float, Float)> // adaptive
// Root finding
bisection(f, a, b, tol) -> Maybe<Float>
newton(f, df, x0, tol, max_iter) -> Maybe<Float>
secant(f, x0, x1, tol, max_iter) -> Maybe<Float>
brent(f, a, b, tol) -> Maybe<Float>
// Optimisation
gradient_descent(f, grad, x0, lr, max_iter) -> Vector<Float>
newton_optimize(f, grad, hess, x0, tol) -> Vector<Float>
bfgs(f, grad, x0, tol, max_iter) -> Vector<Float>
math.random
type RandomKey is UInt64;
// RAW GENERATORS — a stream of bits, nothing else.
type XorShift128 is { ... }; type PCG is { ... };
XorShift128.new(seed: UInt64) -> XorShift128
PCG.new(seed: UInt64, stream: UInt64) -> PCG // two words: seed and stream
gen.next_u64() -> UInt64 gen.next_bounded(bound) -> UInt64
gen.next_f64() -> Float gen.next_f32() -> Float32
gen.next_bool() -> Bool
// SAMPLING — `Rng` is a RECORD holding a key, and it owns the
// distributions. The raw generators above do NOT have these.
type Rng is { key: RandomKey };
Rng.new(seed: UInt64) -> Rng Rng.from_key(key) -> Rng
rng.uniform_01() -> Float // [0.0, 1.0)
rng.uniform(low, high) -> Float
rng.normal_01() -> Float
rng.normal(mean, std) -> Float
rng.exponential(rate) -> Float
rng.bernoulli(p) -> Bool
rng.uniform_int(bound) -> UInt64
rng.next_key() -> RandomKey
rng.permutation(n) -> List<USize>
rng.shuffle(&mut xs)
mount core.random.deterministic.{Rng};
mount core.collections.{List};
fn main() {
let mut r = Rng.new(7);
let a = r.uniform_01();
let b = r.uniform_01();
print(f"advances={a != b} in_range={a >= 0.0 && a < 1.0}");
let mut xs: List<Int> = List.from([1, 2, 3, 4, 5, 6, 7, 8]);
r.shuffle(&mut xs);
let mut sum = 0;
for i in 0..8 { sum = sum + xs[i]; }
print(f"shuffle len={xs.len()} sum={sum}");
}
advances=true in_range=true
shuffle len=8 sum=36
Rng is a record. Raw generators such as XorShift128 are separate
types. shuffle_vec, choice, truncated_normal, poisson, gamma,
beta, chi_squared, student_t and categorical are key-taking free
functions in core/random/deterministic.vr:
core.random.deterministic.choice(key, &xs) -> T
core.random.deterministic.shuffle_vec(key, &mut xs)
They are named here rather than listed with signatures, because none of
them has been run and a signature transcribed from a declaration is a
claim like any other. Rng.shuffle (above) is the method form and was
run.
Layer 4 — Tensor system
Defines Tensor<T, const S: Shape> (statically shaped) and DynTensor<T>
(dynamic), plus all the usual operations.
Tensor operations run under the interpreter. The AOT tier lowers some of them and announces the rest: of the 107 tensor runtime helpers the compiler references, 71 are panic stubs that name themselves when reached. Checked:
verum run shape ok
verum run --tier aot PANIC: verum_tensor_arange_i: no Tier-1 lowering
yet
This is deliberate. A helper declared without a body would either break the link or silently return zero; a stub that panics with its own name fails where you can see it, and names the epic that is landing the real lowerings per operation.
What is not yet measured is WHICH operations survive Tier 1 — every
tensor spec in the conformance suite runs at tier 0, so the boundary is
known to exist and not known in detail. If you are targeting AOT, run
your kernel under --tier aot before depending on it.
// Construction
zeros<Float, shape[3, 4]>() -> Tensor<Float, shape[3, 4]>
ones<Float, shape[3, 4]>()
full<Float, shape[2, 2]>(value: 3.14)
eye<Float, 5>() // identity
arange(start, stop, step) -> DynTensor<Float>
linspace(start, stop, n) -> Tensor<Float, shape[n]>
rand<Float, shape[3, 4]>() // uniform [0, 1)
randn<Float, shape[3, 4]>() // standard normal
// Shape — these ARE methods on the tensor
t.shape() t.rank() t.ndim() t.dim(i) t.numel()
t.reshape(...) t.squeeze() t.unsqueeze(axis) t.permute(axes)
t.slice(...) t.get(...) t.set(...) t.item() t.cast(...) t.to(device)
t.contiguous() t.is_contiguous() t.clone() t.device()
// Everything else is a FREE FUNCTION taking the tensor by reference
transpose(&t) flatten(&t) cumsum(&t, axis)
matmul(&a, &b) mm(&a, &b) bmm(&a, &b)
sum(&t) mean(&t) prod(&t) argmax(&t) argmin(&t) // whole tensor
sum_axis(&t, axis) mean_axis(&t, axis) max_axis(&t, axis)
min_axis(&t, axis) argmax_axis(&t, axis) all_axis / any_axis
softmax(&t) softmax_axis(&t, axis) log_softmax(&t, axis)
// Comparison — free, and they return a Bool tensor
eq(&a, &b) ne(&a, &b) lt(&a, &b) le(&a, &b) gt(&a, &b) ge(&a, &b)
// Selection
where_tensor(&mask, &a, &b) where_scalar(&mask, a, b)
masked_select(&t, &mask) masked_sum / masked_mean / masked_min / masked_max
// Composition
cat(&tensors, axis) / stack(&tensors, axis)
split(t, sizes, axis) / chunk(t, n, axis)
hstack / vstack / dstack
The tensor API is free functions over &DynTensor<T>, not methods.
t.matmul(other) does not compile; matmul(&t, &other) does. Only the
shape and storage operations in the first block are methods.
Normalisation is likewise not a tensor method: layer_norm(shape) and
rms_norm(dim) build a module (LayerNorm, RMSNorm) that you then
apply. There is no batch_norm, no masked_fill, no logical_and, and
a tensor does not report its own dtype.
Layer 5 — GPU
type GPUBackend, DeviceId, DeviceInfo, ComputeCapability | |
type DeviceSelector, DeviceRegistry | |
type MemorySpace, DevicePtr<T>, GPUBuffer<T>, PinnedBuffer<T> | |
type Stream, Event, LaunchConfig, CudaGraph | |
GPUBackend.default() -> GPUBackend | |
device.allocate<T>(count) -> GPUBuffer<T> | |
device.launch(config, kernel, args) | |
device.sync() |
See simd.gpu and
intrinsics → gpu for device-side
intrinsics.
Layer 6 — Automatic differentiation
type DiffMode is ReverseMode | ForwardMode | MixedMode { threshold: Float };
DiffMode.auto(input_dim, output_dim) -> DiffMode
// Picks ForwardMode when output_dim / input_dim > 1, else ReverseMode.
type Differentiable is protocol {
type Tangent; type Cotangent;
fn zero_tangent() -> Self.Tangent;
fn add_tangent(a: Self.Tangent, b: Self.Tangent) -> Self.Tangent;
fn scale_tangent(t: Self.Tangent, s: Float) -> Self.Tangent;
}
// Gradients
grad(f) -> fn(input) -> Cotangent
value_and_grad(f, x) -> (output, gradient)
grad_argnums(f, argnums) -> fn(*args) -> Tuple<Cotangent>
// Vector-Jacobian products
vjp(f, x) -> (output, vjp_fn: fn(cotangent) -> Cotangent)
jvp(f, x, tangent) -> (output, tangent_out)
// Higher-order
jacobian(f) -> fn(x) -> Tensor
hessian(f) -> fn(x) -> Tensor
hvp(f, x, v) -> Tensor // Hessian-vector product
// Control
stop_gradient(x) -> T
custom_vjp(primal, vjp_fn)
GradientScope { fn enter() / exit() }
with_no_grad(|| pure_inference())
// Memory
checkpoint(f, x) -> y // trade recompute for memory
recompute(values)
Scalar gradients in the interpreter
During scalar Float gradient recording, a selected numeric source method
contributes the arithmetic executed by its body. The receiver and explicit
arguments retain their gradient connections across the call, as does the
returned scalar. This covers direct values and local references passed to a
by-value self. Reference receivers whose gradient-tape origin cannot be
recovered produce an unsupported-gradient error.
A builtin derivative rule for a name such as sin applies when that builtin
operation executes. A source method with that name follows its own body.
This interpreter behavior does not establish tensor or native
differentiation, or validate the separate compiler transformation for
@differentiable functions. See autodiff compilation.
core/math/autodiff.vr declares four Differentiable
implementations — for Float, DynTensor<T: RealField>,
Vector<Float> and Matrix<Float>. There are none for Float32 or
Float64.
Two caveats, both measured on the current toolchain rather than read off the source:
-
A
<T: Differentiable>bound is satisfied byFloat(it was not when this page was first written). Measured with the control that makes the result mean something:probe result needs_diff(1.0)wheref: Floataccepted needs_diff(p)wherepimplements nothingerror<E405>: type \Plain` does not implement `Differentiable``The negative case is the point: a clean result on
Floatalone would equally mean "the bound is not checked at all".Float32andFloat64are still refused —core/math/autodiff.vrdeclaresimplement Differentiable for Floatand nothing for the sized spellings, so this is a missing implementation rather than a carrier defect. The underlying cause the page used to describe (a protocol impl is carried by its target type's descriptor, and built-in scalars have none) has since been repaired. -
@derive(Differentiable)on a user record does not generate an implementation. The compiler says so rather than pretending:warning<W0507>: `@derive(Differentiable)` on `Params` was not applied— no generator for this protocol yetWrite the implementation by hand until a generator lands.
Layer 7 — Neural networks
type Module is protocol { ... };
type Trainable is protocol { ... };
// Not generic, and it carries the autograd flag: a Parameter IS a
// float tensor plus its gradient plus whether one is wanted.
type Parameter is {
data: DynTensor<Float>,
grad: Maybe<DynTensor<Float>>,
requires_grad: Bool,
};
Parameter.new(shape: &[USize]) -> Parameter // zeros, requires_grad
// Layers
Linear.new(in_features, out_features, use_bias: Bool) -> Linear
Embedding.new(vocab, dim) -> Embedding
Conv2d.new(in_channels, out_channels, kernel_size: (USize, USize))
// no stride / padding parameters — both are fixed
LayerNorm.new(shape) RMSNorm.new(shape) BatchNorm.new(features)
// Activations
relu / gelu / silu / sigmoid / softmax / softplus / tanh
// Dropout
Dropout.new(p)
// Attention
MultiHeadAttention.new(embed_dim, num_heads, dropout)
FeedForward.new(dim, hidden_dim, dropout_p, activation: Activation)
TransformerBlock.new(embed_dim, num_heads, hidden_dim, dropout)
RoPE.new(dim, max_positions)
// Optimisers
type Optimizer is protocol {
fn step(&mut self, params: &mut List<&mut Parameter>);
fn zero_grad(&mut self, params: &mut List<&mut Parameter>);
fn lr(&self) -> Float;
fn set_lr(&mut self, lr: Float);
}
// The optimisers do NOT take the parameter list; they are handed it
// per step. SGD.simple(lr) fills momentum and weight_decay with 0.
SGD.new(lr, momentum, weight_decay)
AdamW.new(lr, weight_decay) // betas fixed at 0.9 / 0.999, eps 1e-8
// Schedulers — `LRScheduler` is a protocol (`get_lr(step) -> Float`),
// so you construct a concrete one, not a factory method on the protocol.
CosineScheduler.new(initial_lr, min_lr, warmup_steps, total_steps)
LinearWarmup { target_lr, warmup_steps }
// Loss
mse_loss(pred, target) / cross_entropy(pred, target) / bce_loss(pred, target)
// Utility
clip_grad_norm(params, max_norm)
Layer 8 — SSM & distributed
math.ssm — state-space models
S4.new(dim, state_dim, kernel) / Mamba.new(dim, state_dim, conv_dim)
BiMambaBlock.new(dim, state_dim) Jamba.new(...) // hybrid SSM + attention
MoELayer.new(num_experts, dim, routing: RoutingStrategy)
RoutingStrategy is TopK(k) | Hash(buckets) | Learned;
BalanceLoss.new(num_experts)
math.distributed
DataParallel.new(module, devices)
DistributedDataParallel.new(module, process_group)
FSDP.new(module, sharding_strategy) // fully-sharded data parallel
ActorMesh.new(layout) Supervision(...)
RdmaContext // remote direct memory access:
get_ref(actor_id, &tensor) / prefetch(&refs) / wait_all()
Layer 9 — Agents, RAG, guardrails
math.agent
type Tokenizer is protocol { fn encode(text) -> List<Int>; fn decode(ids) -> Text; }
type KVCache is { ... }; PagedKVCache.new(num_blocks, block_size, num_heads, head_dim)
type SpeculativeDecoder is { ... };
type ContinuousBatcher is { ... };
LLMAgent.new(model, tokenizer)
ReActAgent.new(llm, tool_registry, max_iterations)
MemoryStore.new(vector_store)
flash_attention(q, k, v, scale) / paged_attention(...)
sample_top_p(logits, p) / sample_temperature(logits, t) / sample_greedy(logits)
type ChatMessage is { role: AgentRole, content: MessageContent };
type FunctionSchema is { name: Text, parameters: JsonSchema };
type ExecutableTool is protocol {
fn schema(&self) -> FunctionSchema;
fn execute(&self, arguments: Text) -> Result<Value, Error>;
}
QuantizedLinear.new(in_dim, out_dim, bits: Int) // INT4/INT8
math.guardrails
ContentClassifier.new(categories, threshold) | |
Guardrail.new(&classifiers) | |
PIIFilter.new(patterns) | |
TopicGuardrail.new(allowed_topics) | |
GuardrailChain.new(&rails) | |
GuardedAgent.new(agent, chain) |
math.rag
Document { id, content, embedding, metadata }
VectorStore is protocol { ... };
HNSWIndex.new(dim, m, ef_construction)
TextChunker.new(chunk_size, overlap)
BM25Index.new()
HybridRetriever.new(dense_store, sparse_index) // dense_weight defaults to 0.5
RAGPipeline.new(retriever, llm, prompt_template)
Pure mathematics
Self-contained formalisations, used by the verification system
and by theory_interop. Depth varies per branch; most define
the usual algebraic structures and their universal
constructions.
algebra/— groups, rings, fields, lattices, modules.category/— categories, functors, natural transformations, adjunctions, monads, limits, colimits.topology/— point-set topology, manifolds, homology.analysis/— real, functional, measure theory.logic/— propositions-as-types, proof terms, decidability.hott/— cubical HoTT:I,Path,refl,transport,hcomp,Equiv,IsContr,IsProp,ua,funext,S1,Susp,Trunc,Quotient.cubical/— interval operations,Face,comp,Glue.simplicial/—SimplicialSet,KanComplex,InfinityGroupoid.infinity_category/—QuasiCategory,InfinityFunctor,MappingSpace.infinity_topos/—Sieve,GrothendieckTopology,InfPresheaf,InfSheaf,InfinityTopos,GeometricMorphism,DescentObstruction.kan_extension/—InfLeftKanExtension,InfRightKanExtension,PointwiseKanExtension.fibration/—GrothendieckFibration,CartesianMorphism.model_category/—QuillenModelStructure,WeakEquivalence.operad/— operads,E_noperads, ∞-operads.number_theory/— Peano naturals, primes, modular arithmetic.
∞-Topos foundations
quantum_logic/—OrthomodularLattice,EpistemicHilbertSpace, measure, commutator.giry/—MeasurableSpace,ProbabilityMeasure, Giry monad,LlmOracle.epistemic/—EpistemicStatus,Theory,EpistemicTopology, theory-site.cohesive/— cohesive structure: Π ⊣ Disc ⊣ Γ ⊣ coDisc.day_convolution/—SymmetricMonoidalCategory,DayConvolution,CognitiveExtension.sdg/— synthetic differential geometry:D,TangentBundle,DifferentialForm,Connection.
Miscellaneous
complex/— complex numbers.category_finite/— finite categories (decidable equality).bitvec/— bit-vectors for cryptography.observational/— observational type theory.examples/— worked examples covering the algebra and topology layers.internal/— library internals (@internalmarked).simple//advanced/— convenience API / fine-grained API.tactics/— tactic library for proof automation.
Cross-references
- simd — SIMD vectors that
math.tensoruses under the hood. - intrinsics — raw CPU/GPU primitives.
- theory_interop — theory registry + translation + coherence audit; consumes
math.infinity_topos+math.kan_extension. - proof — proof certificates that verify math-module obligations.
- Verification → cubical & HoTT — the path types that
math.hottencodes.