omnibias.core.proof.lift

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.proof.lift

Module contract & mathematical conventions

Exact-Q lift: residual identically zero, or None.

A float residual is not a certificate. residual_identically_zero and integer_null_space adjudicate over ~fractions.Fraction only. Applications use this module for exact rational residual checks.

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 →

FUNCTION

as_fraction

omnibias.core.proof.as_fractionSource ↗

as_fraction(value: Number | float, *, denom_bound: int | None=None) -> Fraction

Exact int / Fraction, or a bounded-denominator snap of a float.

Parameters

Name	Type & default	Contract
`value`positional-or-keyword	`Number \| float`Required	See the operation contract and implementation below.
`denom_bound`keyword-only	`int \| None`Default: None	See the operation contract and implementation below.

ReturnsFraction

Executed regression · integer null space rank deficient

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_integer_null_space_rank_deficient() -> None:
    null = integer_null_space([[1, 2], [2, 4]])
    assert len(null) == 1
    vector = null[0]
    assert vector[0] + 2 * vector[1] == 0

python -m pytest "packages/omnibias-core/tests/test_lift.py::test_integer_null_space_rank_deficient" -q

Read the implementation

def as_fraction(value: Number | float, *, denom_bound: int | None = None) -> Fraction:
    """Exact ``int`` / ``Fraction``, or a bounded-denominator snap of a float."""

    if isinstance(value, Fraction):
        return value
    if isinstance(value, int):
        return Fraction(value)
    snapped = Fraction(value).limit_denominator(denom_bound or 1_000_000)
    if denom_bound is not None:
        return snapped
    return Fraction(value)

Other public import paths

omnibias.core.proof.as_fraction
omnibias.core.proof.lift.as_fraction

FUNCTION

integer_null_space

omnibias.core.proof.integer_null_spaceSource ↗

integer_null_space(matrix: Sequence[Sequence[int]]) -> list[list[int]]

Exact primitive-integer basis of {p : matrix @ p = 0}.

Parameters

Name	Type & default	Contract
`matrix`positional-or-keyword	`Sequence[Sequence[int]]`Required	See the operation contract and implementation below.

Returnslist[list[int]]

Executed regression · integer null space rank deficient

Full file, imports & fixtures ↗

def test_integer_null_space_rank_deficient() -> None:
    null = integer_null_space([[1, 2], [2, 4]])
    assert len(null) == 1
    vector = null[0]
    assert vector[0] + 2 * vector[1] == 0

python -m pytest "packages/omnibias-core/tests/test_lift.py::test_integer_null_space_rank_deficient" -q

Read the implementation

def integer_null_space(matrix: Sequence[Sequence[int]]) -> list[list[int]]:
    """Exact primitive-integer basis of ``{p : matrix @ p = 0}``."""

    if not matrix:
        return []
    reduced, pivots = rref([[Fraction(int(v)) for v in row] for row in matrix])
    n_cols = len(matrix[0])
    pivot_set = set(pivots)
    free_cols = [c for c in range(n_cols) if c not in pivot_set]
    basis: list[list[int]] = []
    for free in free_cols:
        vec = [Fraction(0) for _ in range(n_cols)]
        vec[free] = Fraction(1)
        for row_idx, pivot_col in enumerate(pivots):
            vec[pivot_col] = -reduced[row_idx][free]
        basis.append(_primitive_integer(vec))
    return basis

Other public import paths

omnibias.core.proof.integer_null_space
omnibias.core.proof.lift.integer_null_space

FUNCTION

residual_identically_zero

omnibias.core.proof.residual_identically_zeroSource ↗

residual_identically_zero(design: Sequence[Sequence[Number | float]], coeffs: Sequence[Number | float], target: Sequence[Number | float], *, intercept: Number | float=0, denom_bound: int | None=None) -> bool

True iff intercept + design @ coeffs equals target in Q.

Parameters

Name	Type & default	Contract
`design`positional-or-keyword	`Sequence[Sequence[Number \| float]]`Required	See the operation contract and implementation below.
`coeffs`positional-or-keyword	`Sequence[Number \| float]`Required	See the operation contract and implementation below.
`target`positional-or-keyword	`Sequence[Number \| float]`Required	See the operation contract and implementation below.
`intercept`keyword-only	`Number \| float`Default: 0	See the operation contract and implementation below.
`denom_bound`keyword-only	`int \| None`Default: None	See the operation contract and implementation below.

Returnsbool

Explicit validation & failure cases

When len(design) != len(target), raises ValueError('design and target must have the same number of rows').
When len(row) != len(snapped), raises ValueError('design width must match coefficient count').

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

Executed regression · residual identically zero accepts planted

Full file, imports & fixtures ↗

def test_residual_identically_zero_accepts_planted() -> None:
    design = [[Fraction(1), Fraction(2)], [Fraction(3), Fraction(4)]]
    coeffs = [Fraction(1), Fraction(-1, 2)]
    target = [Fraction(0), Fraction(1)]
    assert residual_identically_zero(design, coeffs, target) is True

python -m pytest "packages/omnibias-core/tests/test_lift.py::test_residual_identically_zero_accepts_planted" -q

Regression example · residual identically zero rejects perturbation

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_residual_identically_zero_rejects_perturbation() -> None:
    design = [[Fraction(1), Fraction(2)], [Fraction(3), Fraction(4)]]
    coeffs = [Fraction(1), Fraction(-1, 2)]
    target = [Fraction(0), Fraction(1) + Fraction(1, 1000)]
    assert residual_identically_zero(design, coeffs, target) is False

python -m pytest packages/omnibias-core/tests/test_lift.py -k test_residual_identically_zero_rejects_perturbation -q

Read the implementation

def residual_identically_zero(
    design: Sequence[Sequence[Number | float]],
    coeffs: Sequence[Number | float],
    target: Sequence[Number | float],
    *,
    intercept: Number | float = 0,
    denom_bound: int | None = None,
) -> bool:
    """``True`` iff ``intercept + design @ coeffs`` equals ``target`` in ``Q``."""

    if len(design) != len(target):
        raise ValueError("design and target must have the same number of rows")
    snapped = [as_fraction(coef, denom_bound=denom_bound) for coef in coeffs]
    bias = as_fraction(intercept, denom_bound=denom_bound)
    for row, rhs in zip(design, target, strict=True):
        if len(row) != len(snapped):
            raise ValueError("design width must match coefficient count")
        acc = bias
        for coef, entry in zip(snapped, row, strict=True):
            acc += coef * as_fraction(entry, denom_bound=denom_bound)
        if acc != as_fraction(rhs, denom_bound=denom_bound):
            return False
    return True

Other public import paths

omnibias.core.proof.residual_identically_zero
omnibias.core.proof.lift.residual_identically_zero

FUNCTION

rref

omnibias.core.proof.lift.rrefSource ↗

rref(matrix: Sequence[Sequence[Number]]) -> tuple[list[list[Fraction]], list[int]]

Reduced row echelon form over the rationals; returns (rref, pivot_cols).

Parameters

Name	Type & default	Contract
`matrix`positional-or-keyword	`Sequence[Sequence[Number]]`Required	See the operation contract and implementation below.

Returnstuple[list[list[Fraction]], list[int]]

Executed regression · integer null space rank deficient

Full file, imports & fixtures ↗

def test_integer_null_space_rank_deficient() -> None:
    null = integer_null_space([[1, 2], [2, 4]])
    assert len(null) == 1
    vector = null[0]
    assert vector[0] + 2 * vector[1] == 0

python -m pytest "packages/omnibias-core/tests/test_lift.py::test_integer_null_space_rank_deficient" -q

Read the implementation

def rref(matrix: Sequence[Sequence[Number]]) -> tuple[list[list[Fraction]], list[int]]:
    """Reduced row echelon form over the rationals; returns ``(rref, pivot_cols)``."""

    rows = [[as_fraction(value) for value in row] for row in matrix]
    if not rows:
        return rows, []
    n_rows = len(rows)
    n_cols = len(rows[0])
    pivots: list[int] = []
    r = 0
    for c in range(n_cols):
        pivot = None
        for i in range(r, n_rows):
            if rows[i][c] != 0:
                pivot = i
                break
        if pivot is None:
            continue
        rows[r], rows[pivot] = rows[pivot], rows[r]
        head = rows[r][c]
        rows[r] = [val / head for val in rows[r]]
        for i in range(n_rows):
            if i != r and rows[i][c] != 0:
                factor = rows[i][c]
                rows[i] = [a - factor * b for a, b in zip(rows[i], rows[r], strict=True)]
        pivots.append(c)
        r += 1
        if r == n_rows:
            break
    return rows, pivots

← Package overview Runnable learning examples →

omnibias.core.proof.lift

as_fraction​

Parameters

integer_null_space​

Parameters

residual_identically_zero​

Parameters

rref​

Parameters

as_fraction

integer_null_space

residual_identically_zero

rref