Glossary
Concise definitions of the terms used throughout these docs.
Activation spec
The metadata object (ActivationSpec) describing an activation: its name, fast
path, supported orders, operator role, and noise model. Backends share the
metadata and specialize only the tensor type.
Autodiff-exact
A quantity computed by automatic differentiation that is exact up to floating-point round-off, but not from a closed-form expression. Example: metric derivatives in the geometry package. Distinct from closed-form exact.
Bell polynomial / Faà di Bruno
The combinatorics of differentiating a composition. omnibias uses Bell
polynomials (in pure-Python omnibias-core) to propagate jets through composed
functions exactly.
Bias collapse
The founding omnibias limit — what the library is named for. A K-bias unit
f_K(z) = Σₖ sₖ·σ(z + bₖ) with its biases on a finite-difference stencil
(spread δ) collapses, as δ → 0, to the derivative σ^(K−1)(z + b̄). The
derivative tower evaluates this limit exactly — one σ call, no 1/δ^(K−1)
catastrophic cancellation — so the output is a smooth derivative, never a 0/1
step. At K = 2 the collapse output (σ') also realizes a classical operator
role (see the activation dictionary).
Sources: omnibias.torch.unit, omnibias.torch.stencil, and the
closed-form derivatives primer.
Distinct from the collapsed-bias penalty below.
Certificate
A canonical, hash-sealed JSON record of an enclosure: what was bounded, how, how tightly, and whether a theorem prover checked it. Tamper-evident.
Closed-form exact
A quantity computed directly from a known formula — e.g. σⁿ(z) from the
recurrence — with one σ evaluation regardless of order. The strongest of the
three exactness categories.
Collapsed-bias penalty
A different use of "collapse", in the omnibias-convex / -control /
-routing first-order solvers: a single constraint hyperplane aᵀx = b is
enforced by the tempered unit σ(β(aᵀx − b)) (or a relu hinge) whose β → ∞
limit is a 0/1 feasibility step — the sub-gradient of the hinge max(·, 0).
This is a constraint indicator, not a derivative; do not conflate it with
bias collapse.
Derivative tower
The sequence σ(z), σ'(z), σ''(z), …, σⁿ(z) produced in closed form from a
single σ evaluation.
Enclosure
An outward-rounded interval / affine / Taylor-model object that provably contains the true value of a quantity.
Field substrate
The foundational omnibias-fields layer: FieldState, attribute-DSL views,
SigmaCache, and the ops_registry that the PINN, geometry, and SDE packages
build on.
Jet
A truncated Taylor expansion (the tuple of derivatives up to some order) carried through a computation. See jets.
Multi-index
The bookkeeping (α₁, …, α_D) that labels a mixed partial in a multivariate
jet. See multivariate jets.
OMBU
Operator Multi-Bias Unit — a trainable K-bias operator that
drops in for an activation. See operator-typed layers.
OperatorBlock
A typed scalar operator that dispatches on an op tag:
identity | grad | laplacian | derivative | band | integral.
Poly-Laplacian
The iterated Laplacian Δᵏ. In omnibias it is one tower evaluation per order,
so its cost is flat in k.
Riccati family
The smooth activations whose derivatives satisfy a Riccati-type identity
(sigmoid' = s(1−s), tanh' = 1−t²), giving them a closed-form tower at every
order: tanh, sigmoid, softplus, gaussian.
theorem_prover_verified
A boolean on a verdict, set only by a genuine Mathlib-free Lean 4 kernel pass on the certificate's finite obligation. Never forgeable by the certificate.
ULP
Unit in the last place — the granularity of floating-point. "ULP-equal" means identical to the last representable bit.