API REFERENCE/omnibias-core

omnibias.core.verified.clamped_biharmonic

0.5.0rc1Release candidatePython >=3.10Apache-2.0

Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.

import omnibias.core.verified.clamped_biharmonic

Module contract & mathematical conventions

Exact Green bounds and a conditional gate for a clamped cubic beam.

On [0,L], the inverse K of the fourth derivative with u=u'=0 at both endpoints has exact C -> C norm L**4/384. On [0,1] its symmetric kernel, for x <= t, is

G(x,t) = x**2 * (1-t)**2 * (3*t - (1+2*t)*x) / 6.

Each branch is cubic in x, its first two derivatives are continuous at x=t, and its third derivative has jump one. The kernel and its first derivative vanish at both endpoints. Thus K h is the unique clamped C4 solution of v''''=h for every continuous h. The kernel is nonnegative because its last factor is at least 2*t*(1-t) when x<=t. Since K 1=x**2*(1-x)**2/24, positivity gives the exact sup norm 1/384; equality is attained for h=1 at x=1/2. Scaling gives the stated L**4 law. Symmetry and the same row integral give ||K||_L2 <= L**4/384 by the Schur estimate. The clamped self-adjoint fourth derivative therefore has quadratic-form lower bound 384/L**4. Adding 3*lambda*v**2 for real bounded v and lambda>=0 preserves this lower bound.

For u''''+lambda*u**3=f and a clamped C4 candidate q, suppose the CALLER PROVES ||q|| <= U and ||q''''+lambda*q**3-f|| <= R uniformly over the whole interval and 0<=lambda<=lambda_max. On the complete C-space ball B_r(q), the full operator T(v)=K(f-lambda*v**3) has defect at most Y=norm(K)*R and Lipschitz constant at most Z=3*lambda_max*norm(K)*(U+r)**2. The finite gate Z<1, Y+Z*r<=r implies a self-map contraction PROVIDED those candidate/residual/boundary hypotheses are established. A fixed point is C4 and solves the original BVP by the Green identity. Global classical uniqueness follows by integrating (u-v)*(u''''-v'''') + lambda*(u-v)*(u**3-v**3)=0 twice by parts.

This module computes the exact scalar gate; it DOES NOT verify the supplied whole-domain bounds or boundary conditions. Its result never independently asserts PDE existence, a quantum continuum theorem, or a Lean tier. There are no finite-mode tails in K. No differentiation backend is imported.

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.

Module source ↗Source revision 9a2d73df0573Running reference examples →

CLASS

ClampedCubicContraction

omnibias.core.verified.ClampedCubicContractionSource ↗

class ClampedCubicContraction

Dataclass constructor fields; inherited fields, if any, are declared by the base class. A field(...) expression describes a default factory or field options, not a literal argument default.

Exact scalar conditions, with candidate proof obligations still external.

Parameters

Name	Type & default	Contract
candidate_sup_upperdataclass field	FractionRequired	See the operation contract and implementation below.
residual_sup_upperdataclass field	FractionRequired	See the operation contract and implementation below.
coupling_upperdataclass field	FractionRequired	See the operation contract and implementation below.
radiusdataclass field	FractionRequired	See the operation contract and implementation below.
lengthdataclass field	FractionRequired	See the operation contract and implementation below.
inverse_normdataclass field	FractionRequired	See the operation contract and implementation below.
defectdataclass field	FractionRequired	See the operation contract and implementation below.
contractiondataclass field	FractionRequired	See the operation contract and implementation below.
self_map_margindataclass field	FractionRequired	See the operation contract and implementation below.

Executed regression · failed contraction or self map refuses

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.

Full file, imports & fixtures ↗

def test_failed_contraction_or_self_map_refuses():
    assert not clamped_cubic_contraction(1, 32, 32, Q(1, 1000000)).passed
    assert not clamped_cubic_contraction(1, 0, 1000, Q(1, 8)).passed

python -m pytest "packages/omnibias-core/tests/verified/test_clamped_biharmonic.py::test_failed_contraction_or_self_map_refuses" -q

Fields & methods

candidate_sup_upperfield

candidate_sup_upper: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

residual_sup_upperfield

residual_sup_upper: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

coupling_upperfield

coupling_upper: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

radiusfield

radius: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

lengthfield

length: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

inverse_normfield

inverse_norm: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

defectfield

defect: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

contractionfield

contraction: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

self_map_marginfield

self_map_margin: Fraction

Declared Fraction field on ClampedCubicContraction. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.

View source ↗

passedproperty

passed(self) -> bool

Whether the finite contraction inequalities pass, not a PDE claim.

Returns: bool

Executed regression · failed contraction or self map refuses

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.

Full file, imports & fixtures ↗

def test_failed_contraction_or_self_map_refuses():
    assert not clamped_cubic_contraction(1, 32, 32, Q(1, 1000000)).passed
    assert not clamped_cubic_contraction(1, 0, 1000, Q(1, 8)).passed

python -m pytest "packages/omnibias-core/tests/verified/test_clamped_biharmonic.py::test_failed_contraction_or_self_map_refuses" -q

Method implementation

    def passed(self) -> bool:
        """Whether the finite contraction inequalities pass, not a PDE claim."""
        return self.contraction < 1 and self.self_map_margin >= 0

View source ↗

to_payloadmethod

to_payload(self) -> dict[str, Any]

Record the remaining analytic input obligations explicitly.

Returns: dict[str, Any]

Executed regression · false residual bound is only a conditional gate

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.

Full file, imports & fixtures ↗

def test_false_residual_bound_is_only_a_conditional_gate():
    gate = clamped_cubic_contraction(0, 0, 0, Q(1, 1000000))
    assert gate.passed
    assert not gate.to_payload()["pde_existence_claim"]

python -m pytest "packages/omnibias-core/tests/verified/test_clamped_biharmonic.py::test_false_residual_bound_is_only_a_conditional_gate" -q

Method implementation

    def to_payload(self) -> dict[str, Any]:
        """Record the remaining analytic input obligations explicitly."""
        return {
            "status": "PASS" if self.passed else "INCONCLUSIVE",
            "candidate_sup_upper": str(self.candidate_sup_upper),
            "residual_sup_upper": str(self.residual_sup_upper),
            "coupling_upper": str(self.coupling_upper),
            "radius": str(self.radius),
            "length": str(self.length),
            "green_operator_norm": str(self.inverse_norm),
            "defect_Y": str(self.defect),
            "contraction_Z": str(self.contraction),
            "self_map_margin": str(self.self_map_margin),
            "verification_kind": "EXACT_RATIONAL_FINITE_GATE",
            "external_premises": {
                "forcing_is_real_continuous": "UNVERIFIED",
                "actual_coupling_in_closed_interval_0_to_coupling_upper": "UNVERIFIED",
                "candidate_is_real_C4_and_clamped": "UNVERIFIED",
                "candidate_bound_on_whole_interval": "UNVERIFIED",
                "residual_bound_on_whole_interval_and_parameter_family": "UNVERIFIED",
            },
            "pde_existence_claim": False,
            "continuum_claim": False,
            "theorem_prover_verified": False,
            "mathlib_verified": False,
        }

View source ↗

Read the implementation

class ClampedCubicContraction:
    """Exact scalar conditions, with candidate proof obligations still external."""

    candidate_sup_upper: Fraction
    residual_sup_upper: Fraction
    coupling_upper: Fraction
    radius: Fraction
    length: Fraction
    inverse_norm: Fraction
    defect: Fraction
    contraction: Fraction
    self_map_margin: Fraction

    @property
    def passed(self) -> bool:
        """Whether the finite contraction inequalities pass, not a PDE claim."""
        return self.contraction < 1 and self.self_map_margin >= 0

    def to_payload(self) -> dict[str, Any]:
        """Record the remaining analytic input obligations explicitly."""
        return {
            "status": "PASS" if self.passed else "INCONCLUSIVE",
            "candidate_sup_upper": str(self.candidate_sup_upper),
            "residual_sup_upper": str(self.residual_sup_upper),
            "coupling_upper": str(self.coupling_upper),
            "radius": str(self.radius),
            "length": str(self.length),
            "green_operator_norm": str(self.inverse_norm),
            "defect_Y": str(self.defect),
            "contraction_Z": str(self.contraction),
            "self_map_margin": str(self.self_map_margin),
            "verification_kind": "EXACT_RATIONAL_FINITE_GATE",
            "external_premises": {
                "forcing_is_real_continuous": "UNVERIFIED",
                "actual_coupling_in_closed_interval_0_to_coupling_upper": "UNVERIFIED",
                "candidate_is_real_C4_and_clamped": "UNVERIFIED",
                "candidate_bound_on_whole_interval": "UNVERIFIED",
                "residual_bound_on_whole_interval_and_parameter_family": "UNVERIFIED",
            },
            "pde_existence_claim": False,
            "continuum_claim": False,
            "theorem_prover_verified": False,
            "mathlib_verified": False,
        }

Other public import paths

• omnibias.core.verified.ClampedCubicContraction
• omnibias.core.verified.clamped_biharmonic.ClampedCubicContraction

FUNCTION

clamped_biharmonic_green_kernel

omnibias.core.verified.clamped_biharmonic_green_kernelSource ↗

clamped_biharmonic_green_kernel(x: int | Fraction, t: int | Fraction, *, length: int | Fraction=1) -> Fraction

Evaluate the exact nonnegative symmetric Green kernel at rational points.

Parameters

Name	Type & default	Contract
xpositional-or-keyword	int | FractionRequired	See the operation contract and implementation below.
tpositional-or-keyword	int | FractionRequired	See the operation contract and implementation below.
lengthkeyword-only	int | FractionDefault: 1	See the operation contract and implementation below.

ReturnsFraction

Explicit validation & failure cases

• When length <= 0 or not 0 <= x <= length or (not 0 <= t <= length), raises ValueError('require positive length and x,t in [0,length]').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · domain refusals

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.

Full file, imports & fixtures ↗

def test_domain_refusals():
    with pytest.raises(ValueError):
        clamped_biharmonic_inverse_norm(0)
    with pytest.raises(ValueError):
        clamped_biharmonic_green_kernel(-1, 0)
    with pytest.raises(ValueError):
        clamped_biharmonic_green_kernel(1, 0, length=Q(1, 2))

python -m pytest "packages/omnibias-core/tests/verified/test_clamped_biharmonic.py::test_domain_refusals" -q

Regression example · exact full inverse norm and length scaling

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.

Full file, imports & fixtures ↗

def test_exact_full_inverse_norm_and_length_scaling():
    assert clamped_biharmonic_inverse_norm() == Q(1, 384)
    assert clamped_biharmonic_inverse_norm(2) == Q(1, 24)
    assert clamped_biharmonic_inverse_norm(Q(1, 2)) == Q(1, 6144)
    for x in (Q(0), Q(1, 4), Q(1, 2), Q(1)):
        for t in (Q(0), Q(1, 3), Q(1)):
            assert clamped_biharmonic_green_kernel(2 * x, 2 * t, length=2) == (
                8 * clamped_biharmonic_green_kernel(x, t)
            )

python -m pytest packages/omnibias-core/tests/verified/test_clamped_biharmonic.py -k test_exact_full_inverse_norm_and_length_scaling -q

Read the implementation

def clamped_biharmonic_green_kernel(
    x: int | Fraction,
    t: int | Fraction,
    *,
    length: int | Fraction = 1,
) -> Fraction:
    """Evaluate the exact nonnegative symmetric Green kernel at rational points."""
    x, t, length = (_rational(v) for v in (x, t, length))
    if length <= 0 or not 0 <= x <= length or not 0 <= t <= length:
        raise ValueError("require positive length and x,t in [0,length]")
    x, t = x / length, t / length
    if x > t:
        x, t = t, x
    return length**3 * x**2 * (1 - t) ** 2 * (3 * t - (1 + 2 * t) * x) / 6

Other public import paths

• omnibias.core.verified.clamped_biharmonic_green_kernel
• omnibias.core.verified.clamped_biharmonic.clamped_biharmonic_green_kernel

FUNCTION

clamped_biharmonic_inverse_norm

omnibias.core.verified.clamped_biharmonic_inverse_normSource ↗

clamped_biharmonic_inverse_norm(length: int | Fraction=1) -> Fraction

Exact sup-norm inverse constant L**4/384 on the clamped interval.

Parameters

Name	Type & default	Contract
lengthpositional-or-keyword	int | FractionDefault: 1	See the operation contract and implementation below.

ReturnsFraction

Explicit validation & failure cases

• When length <= 0, raises ValueError('interval length must be positive').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · failed contraction or self map refuses

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.

Full file, imports & fixtures ↗

def test_failed_contraction_or_self_map_refuses():
    assert not clamped_cubic_contraction(1, 32, 32, Q(1, 1000000)).passed
    assert not clamped_cubic_contraction(1, 0, 1000, Q(1, 8)).passed

python -m pytest "packages/omnibias-core/tests/verified/test_clamped_biharmonic.py::test_failed_contraction_or_self_map_refuses" -q

Regression example · domain refusals

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.

Full file, imports & fixtures ↗

def test_domain_refusals():
    with pytest.raises(ValueError):
        clamped_biharmonic_inverse_norm(0)
    with pytest.raises(ValueError):
        clamped_biharmonic_green_kernel(-1, 0)
    with pytest.raises(ValueError):
        clamped_biharmonic_green_kernel(1, 0, length=Q(1, 2))

python -m pytest packages/omnibias-core/tests/verified/test_clamped_biharmonic.py -k test_domain_refusals -q

Read the implementation

def clamped_biharmonic_inverse_norm(length: int | Fraction = 1) -> Fraction:
    """Exact sup-norm inverse constant L**4/384 on the clamped interval."""
    length = _rational(length)
    if length <= 0:
        raise ValueError("interval length must be positive")
    return length**4 / 384

Other public import paths

• omnibias.core.verified.clamped_biharmonic_inverse_norm
• omnibias.core.verified.clamped_biharmonic.clamped_biharmonic_inverse_norm

FUNCTION

clamped_cubic_contraction

omnibias.core.verified.clamped_cubic_contractionSource ↗

clamped_cubic_contraction(candidate_sup_upper: int | Fraction, residual_sup_upper: int | Fraction, coupling_upper: int | Fraction, radius: int | Fraction, *, length: int | Fraction=1) -> ClampedCubicContraction

Check a full-Green contraction gate from supplied, unverified U and R.

Parameters

Name	Type & default	Contract
candidate_sup_upperpositional-or-keyword	int | FractionRequired	See the operation contract and implementation below.
residual_sup_upperpositional-or-keyword	int | FractionRequired	See the operation contract and implementation below.
coupling_upperpositional-or-keyword	int | FractionRequired	See the operation contract and implementation below.
radiuspositional-or-keyword	int | FractionRequired	See the operation contract and implementation below.
lengthkeyword-only	int | FractionDefault: 1	See the operation contract and implementation below.

ReturnsClampedCubicContraction

Explicit validation & failure cases

• When min(u, residual, coupling) < 0 or radius <= 0, raises ValueError('require nonnegative U, R, coupling and positive radius').

These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.

Executed regression · nonrational inputs refused

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.

Full file, imports & fixtures ↗

def test_nonrational_inputs_refused(args):
    with pytest.raises(TypeError):
        clamped_cubic_contraction(*args)

python -m pytest "packages/omnibias-core/tests/verified/test_clamped_biharmonic.py::test_nonrational_inputs_refused[args0]" -q

Regression example · wrong sign inputs refused

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.

Full file, imports & fixtures ↗

def test_wrong_sign_inputs_refused(args):
    with pytest.raises(ValueError):
        clamped_cubic_contraction(*args)

python -m pytest packages/omnibias-core/tests/verified/test_clamped_biharmonic.py -k test_wrong_sign_inputs_refused -q

Read the implementation

def clamped_cubic_contraction(
    candidate_sup_upper: int | Fraction,
    residual_sup_upper: int | Fraction,
    coupling_upper: int | Fraction,
    radius: int | Fraction,
    *,
    length: int | Fraction = 1,
) -> ClampedCubicContraction:
    """Check a full-Green contraction gate from supplied, unverified U and R."""
    u, residual, coupling, radius, length = (
        _rational(value)
        for value in (candidate_sup_upper, residual_sup_upper, coupling_upper, radius, length)
    )
    if min(u, residual, coupling) < 0 or radius <= 0:
        raise ValueError("require nonnegative U, R, coupling and positive radius")
    norm = clamped_biharmonic_inverse_norm(length)
    defect = norm * residual
    contraction = 3 * coupling * norm * (u + radius) ** 2
    margin = radius - defect - contraction * radius
    return ClampedCubicContraction(
        u, residual, coupling, radius, length, norm, defect, contraction, margin
    )

Related APIsomnibias.core.verified.ClampedCubicContraction↗omnibias.core.verified.clamped_biharmonic_inverse_norm↗

Other public import paths

• omnibias.core.verified.clamped_cubic_contraction
• omnibias.core.verified.clamped_biharmonic.clamped_cubic_contraction

← Package overviewRunnable learning examples →