omnibias.core.verified.ftc
Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.
import omnibias.core.verified.ftcModule contract & mathematical conventions
Rigorous Fundamental Theorem of Calculus certificate (verified register).
This module seals the integral<->derivative link of the closed-form derivative tower as a tamper-evident v1 certificate. For any verified-tower activation it certifies
\int_a^b \sigma^{(k)}(z)\,dz \;=\; \sigma^{(k-1)}(b) - \sigma^{(k-1)}(a) \qquad (k \ge 1),
the default k = 1 being the textbook \int_a^b \sigma' = \sigma(b) -
\sigma(a). The two sides are computed **independently** -- the left by
integrating a rigorous ~omnibias.core.verified.taylor_model.TaylorModel
of \sigma^{(k)} over the cell, the right by evaluating the pointwise
~omnibias.core.verified.sigma.sigma_tower_interval at the two endpoints --
so the residual LHS - RHS enclosing 0 is a genuine cross-check, not a
tautology. Everything is interval arithmetic: honest, rigorous, and never a
open-problem claim.
Shared formulas do not imply universal floating-point identity. Verify dtype, shape, derivative-order support, and the stated numerical assumptions for the path you use.
certified_ftc_residual
omnibias.core.verified.certified_ftc_residualSource ↗certified_ftc_residual(name: str, a: float, b: float, *, k: int=1, order: int=_DEFAULT_ORDER) -> IntervalRigorous enclosure of \int_a^b sigma^(k) - (sigma^(k-1)(b) - sigma^(k-1)(a)).
A sound FTC identity forces the true residual to be exactly 0, so a correct
enclosure must satisfy residual.contains(0.0). Because the two terms are
computed by independent rigorous methods (Taylor-model integration vs pointwise
endpoint towers), a tight residual around 0 is a real cross-check of the
derivative tower.
Parameters
name A verified-tower activation (tanh/sigmoid/gaussian/sin/ cos/silu/gelu/softplus).
a, b Integration limits with a < b.
k Derivative order of the integrand sigma^(k) (default 1); must be >= 1 so the endpoints evaluate sigma^(k-1).
order Taylor-model degree used to enclose sigma^(k) over the cell.
Parameters
| Name | Type & default | Contract |
|---|---|---|
namepositional-or-keyword | strRequired | A verified-tower activation (tanh/sigmoid/gaussian/sin/ cos/silu/gelu/softplus). |
apositional-or-keyword | floatRequired | Integration limits with a < b. |
bpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
kkeyword-only | intDefault: 1 | Derivative order of the integrand sigma^(k) (default 1); must be >= 1 so the endpoints evaluate sigma^(k-1). |
orderkeyword-only | intDefault: _DEFAULT_ORDER | Taylor-model degree used to enclose sigma^(k) over the cell. |
IntervalExecuted regression · higher order gives tighter residual
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_higher_order_gives_tighter_residual() -> None:
a, b = -0.4, 0.4
w_lo = certified_ftc_residual("tanh", a, b, k=1, order=10).width
w_hi = certified_ftc_residual("tanh", a, b, k=1, order=4).width
assert w_lo < w_hi # the Taylor-model remainder shrinks with orderpython -m pytest "packages/omnibias-core/tests/verified/test_ftc.py::test_higher_order_gives_tighter_residual" -qRegression example · residual contains zero and is tight
This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_residual_contains_zero_and_is_tight(name: str, a: float, b: float, k: int) -> None:
residual = certified_ftc_residual(name, a, b, k=k, order=8)
assert residual.contains(0.0) # a sound tower forces the true residual to 0
assert residual.width < 1e-3 # rigorous + tight over a modest cellpython -m pytest packages/omnibias-core/tests/verified/test_ftc.py -k test_residual_contains_zero_and_is_tight -qRead the implementation
def certified_ftc_residual(
name: str, a: float, b: float, *, k: int = 1, order: int = _DEFAULT_ORDER
) -> Interval:
r"""Rigorous enclosure of ``\int_a^b sigma^(k) - (sigma^(k-1)(b) - sigma^(k-1)(a))``.
A sound FTC identity forces the true residual to be exactly ``0``, so a correct
enclosure must satisfy ``residual.contains(0.0)``. Because the two terms are
computed by independent rigorous methods (Taylor-model integration vs pointwise
endpoint towers), a tight residual around ``0`` is a real cross-check of the
derivative tower.
Parameters
----------
name
A verified-tower activation (``tanh``/``sigmoid``/``gaussian``/``sin``/
``cos``/``silu``/``gelu``/``softplus``).
a, b
Integration limits with ``a < b``.
k
Derivative order of the integrand ``sigma^(k)`` (default ``1``); must be
``>= 1`` so the endpoints evaluate ``sigma^(k-1)``.
order
Taylor-model degree used to enclose ``sigma^(k)`` over the cell.
"""
return _ftc_parts(name, a, b, k=k, order=order)[2]Other public import paths
omnibias.core.verified.certified_ftc_residualomnibias.core.verified.ftc.certified_ftc_residual
ftc_certificate
omnibias.core.verified.ftc_certificateSource ↗ftc_certificate(name: str, a: float, b: float, *, k: int=1, order: int=_DEFAULT_ORDER) -> CertSeal the FTC identity \int_a^b sigma^(k) = sigma^(k-1)(b) - sigma^(k-1)(a).
Returns a canonical, hash-sealed v1 certificate carrying the integral
enclosure (LHS), the endpoint difference (RHS), and their residual
(which contains 0 for a sound tower). The certificate makes no open-problem
claim; it is a rigorous, tamper-evident interval artifact.
Parameters
| Name | Type & default | Contract |
|---|---|---|
namepositional-or-keyword | strRequired | See the operation contract and implementation below. |
apositional-or-keyword | floatRequired | See the operation contract and implementation below. |
bpositional-or-keyword | floatRequired | See the operation contract and implementation below. |
kkeyword-only | intDefault: 1 | See the operation contract and implementation below. |
orderkeyword-only | intDefault: _DEFAULT_ORDER | See the operation contract and implementation below. |
CertExecuted regression · certificate verifies and flips on tampered bound
Recorded coverage confirms this test executed the API body. This example belongs to the pinned upstream test suite. It may use fixtures and imports from its full file. Run it from that checkout with its test dependencies installed.
def test_certificate_verifies_and_flips_on_tampered_bound() -> None:
cert = ftc_certificate("tanh", -0.3, 0.4, k=1, order=6)
assert verify_certificate_digest(cert)
assert cert["claim"].startswith("FTC:")
assert cert["honesty"]["unproven_claim"] is False
assert cert["honesty"]["rigorous_enclosure"] is True
assert cert["payload"]["residual_contains_zero"] is True
tampered = copy.deepcopy(cert)
hi = float.fromhex(tampered["payload"]["residual"]["hi"])
tampered["payload"]["residual"]["hi"] = (hi + 0.5).hex() # widen a sealed bound
assert not verify_certificate_digest(tampered)python -m pytest "packages/omnibias-core/tests/verified/test_ftc.py::test_certificate_verifies_and_flips_on_tampered_bound" -qRead the implementation
def ftc_certificate(
name: str, a: float, b: float, *, k: int = 1, order: int = _DEFAULT_ORDER
) -> Cert:
r"""Seal the FTC identity ``\int_a^b sigma^(k) = sigma^(k-1)(b) - sigma^(k-1)(a)``.
Returns a canonical, hash-sealed v1 certificate carrying the integral
enclosure (``LHS``), the endpoint difference (``RHS``), and their residual
(which contains ``0`` for a sound tower). The certificate makes no open-problem
claim; it is a rigorous, tamper-evident interval artifact.
"""
# Imported lazily: certificate.py imports verified.interval, so a top-level
# import here would create a proof<->verified initialisation cycle.
from omnibias.core.proof.certificate import encode_interval, make_certificate
lhs, rhs, residual = _ftc_parts(name, a, b, k=k, order=order)
payload = {
"type": "ftc_identity",
"activation": name,
"k": k,
"order": order,
"a": float(a),
"b": float(b),
"integral_of_kth_derivative": encode_interval(lhs),
"endpoint_difference": encode_interval(rhs),
"residual": encode_interval(residual),
"residual_contains_zero": residual.contains(0.0),
}
return make_certificate(
claim="FTC: integral of sigma^(k) = sigma^(k-1)(b) - sigma^(k-1)(a)",
payload=payload,
honesty={
"unproven_claim": False,
"closed_form_integrand": True,
"rigorous_enclosure": True,
},
)Other public import paths
omnibias.core.verified.ftc_certificateomnibias.core.verified.ftc.ftc_certificate