omnibias.core.verified.invariant_subspace
Coefficient recurrences, activation contracts, jet algebra, and verified arithmetic shared by the numerical backends.
import omnibias.core.verified.invariant_subspaceModule contract & mathematical conventions
Certified **invariant-subspace** (Davis-Kahan sin Theta) enclosures.
omnibias.core.verified.eig_operator and omnibias.core.verified.eig
certify *scalar* facts about a symmetric operator's spectrum: a lower bound on
one eigenvalue, an exact eigenvalue *count* (with multiplicity) below a
threshold, or a spectral gap between two named eigenvalues. None of them
certify that a whole **cluster** of eigenvalues (a genuinely degenerate ground
state, or a near-degenerate representation multiplet) has been resolved as a
*subspace* -- i.e. that a candidate k-dimensional span(V) is close to
some true k-dimensional invariant subspace of A, without requiring the
k eigenvalues inside the cluster to be individually separated from *each
other*. This module closes that gap with a single certificate,
certified_invariant_subspace, implementing the classical **Davis-Kahan
sin Theta theorem** via its residual/Sylvester-equation proof, entirely in
outward-rounded interval arithmetic and entirely on top of the *existing*
eigenvalue machinery (no new eigenvalue solver):
1. **Ritz-value cluster bracket.** With H = V^T A V and Gram G = V^T V (V's columns need not be orthonormal), the generalized eigenvalues of the pencil (H, G) are exactly the Ritz values of the candidate subspace. ~omnibias.core.verified.eig_operator.generalized_eigenvalue_enclosure brackets the smallest (index 1) and largest (index k) of them, giving a certified cluster interval [ritz_lower, ritz_upper] -- unchanged whether the k Ritz values are distinct or exactly repeated.
2. **Separation gap of the true operator.** Rather than construct an explicit (n-k)-dimensional orthogonal-complement basis (which would need its own soundness argument, e.g. a Gershgorin bound on a deflated A - V H V^T), this module reuses ~omnibias.core.verified.eig_operator.count_eigenvalues_below and ~omnibias.core.verified.eig_operator.generalized_eigenvalue_enclosure directly on the pencil (A, I) -- i.e. on A itself. Let p be the certified number of eigenvalues of A strictly below ritz_lower (inertia bisection, exact for a genuinely repeated eigenvalue). Assign the cluster to eigenvalue indices p+1 .. p+k and certify the gap to *everything else*: a lower bound on ritz_lower - lambda_p (if p>=1) and on lambda_{p+k+1} - ritz_upper (if p+k<n); their minimum is gap. This is *sound for any choice of the p+1..p+k block* (see the Sylvester-equation argument below) and directly bounds the true spectral gap of A -- tighter, and requiring strictly less new machinery, than a Gershgorin estimate on a deflated matrix. It is also exact for an exactly-degenerate cluster: the inertia bisection that produces p never confuses a repeated eigenvalue with two nearby distinct ones.
3. **Residual.** V is first turned into a basis Vtilde that is *exactly* orthonormal (to interval precision) but spans the same subspace, via the certified interval LDL^T factor G = L D L^T (Vtilde = V L^{-T} D^{-1/2}, using ~omnibias.core.verified.eig_operator.interval_ldlt_factor and ~omnibias.core.verified.linalg.interval_triangular_solve -- no new factorization). The residual R = A Vtilde - Vtilde Htilde (Htilde = Vtilde^T A Vtilde) is then formed in interval arithmetic and its **Frobenius norm** ||R||_F bounded (.hi of the enclosed sum R_ij^2, then sqrt). Frobenius is the norm convention used throughout this module: it is the simplest to bound rigorously without further (operator-norm) machinery, and it is exactly the norm for which the classical proof below is cleanest.
**The theorem** (finite-dimensional Davis-Kahan via the Sylvester equation):
let S be the true invariant subspace of A spanned by the eigenvectors
with eigenvalues lambda_{p+1..p+k} and let S_perp be its orthogonal
complement (spanned by every *other* eigenvector, i.e.
lambda_1..lambda_p, lambda_{p+k+1..n}). Writing Y = P_{S_perp} Vtilde,
the residual identity A Vtilde = Vtilde Htilde + R gives the Sylvester
equation A_2 Y - Y Htilde = P_{S_perp} R on S_perp (where
A_2 = A|_{S_perp}, spectrum spec(A) \ {lambda_{p+1..p+k}}). Because
spec(Htilde) lies inside [ritz_lower, ritz_upper] and every point of
spec(A_2) is at distance >= gap from that interval (step 2), the
Sylvester operator is invertible with ||.^{-1}|| <= 1/gap, hence
||Y||_F <= ||R||_F / gap. Y is exactly the matrix whose singular
values are the sines of the principal angles between span(V) and S, so
The certificate reports min(||R||_F / gap, sqrt(k)). The sqrt(k)
clamp is itself always sound: Y's k columns each have norm <= 1
(each is the projection P_{S_perp} -- a contraction -- applied to a unit
column of the exactly orthonormal Vtilde), so ||Y||_F <= sqrt(k)
regardless of the residual/gap estimate (for k = 1 this is the familiar
sin Theta <= 1). When G cannot
be certified positive definite (V's columns are not certified
independent), or the separation gap cannot be certified positive, the
certificate honestly reports certified=False with the unresolved fields
left None -- matching the
~omnibias.core.verified.eig_operator.count_eigenvalues_below
returns-None-on-failure idiom used throughout this file -- rather than
fabricating a bound.
This module lives apart from eig_operator (rather than being folded
into it) because it is a genuinely different *object*: a subspace/projector
statement built by composing the scalar eigenvalue machinery, not another
scalar eigenvalue bound in the same Temple/Lehmann-Maehly-Goerisch ladder.
Every statement here is a **fixed-operator** result; nothing makes a
continuum or limit 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.
InvariantSubspaceCertificate
omnibias.core.verified.InvariantSubspaceCertificateSource ↗class InvariantSubspaceCertificateDataclass 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.
Certified Davis-Kahan sin Theta bound for a candidate invariant subspace.
certified is True only when a positive separation gap was
actually established; otherwise every downstream field
(residual_norm_upper, gap_lower, sin_theta_upper) is None
-- an honest refusal, never a fabricated bound.
Parameters
| Name | Type & default | Contract |
|---|---|---|
dimensiondataclass field | intRequired | See the operation contract and implementation below. |
cluster_sizedataclass field | intRequired | See the operation contract and implementation below. |
gram_positive_definitedataclass field | boolRequired | See the operation contract and implementation below. |
ritz_lowerdataclass field | float | NoneRequired | See the operation contract and implementation below. |
ritz_upperdataclass field | float | NoneRequired | See the operation contract and implementation below. |
cluster_start_indexdataclass field | int | NoneRequired | See the operation contract and implementation below. |
gap_lowerdataclass field | float | NoneRequired | See the operation contract and implementation below. |
residual_norm_upperdataclass field | float | NoneRequired | See the operation contract and implementation below. |
sin_theta_upperdataclass field | float | NoneRequired | See the operation contract and implementation below. |
certifieddataclass field | boolRequired | See the operation contract and implementation below. |
Regression example · result is the dataclass type
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_result_is_the_dataclass_type() -> None:
cert = certified_invariant_subspace(A_DEGENERATE, [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0]])
assert isinstance(cert, InvariantSubspaceCertificate)
assert cert.dimension == 3
assert cert.cluster_size == 2python -m pytest packages/omnibias-core/tests/verified/test_invariant_subspace.py -k test_result_is_the_dataclass_type -qFields & methods
dimensionfield
dimension: intDeclared int field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗cluster_sizefield
cluster_size: intDeclared int field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗gram_positive_definitefield
gram_positive_definite: boolDeclared bool field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗ritz_lowerfield
ritz_lower: float | NoneDeclared float | None field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗ritz_upperfield
ritz_upper: float | NoneDeclared float | None field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗cluster_start_indexfield
cluster_start_index: int | NoneDeclared int | None field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗gap_lowerfield
gap_lower: float | NoneDeclared float | None field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗residual_norm_upperfield
residual_norm_upper: float | NoneDeclared float | None field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗sin_theta_upperfield
sin_theta_upper: float | NoneDeclared float | None field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗certifiedfield
certified: boolDeclared bool field on InvariantSubspaceCertificate. A value must be provided when constructing the configuration, unless an inherited constructor supplies it.
View source ↗Read the implementation
class InvariantSubspaceCertificate:
"""Certified Davis-Kahan ``sin Theta`` bound for a candidate invariant subspace.
``certified`` is ``True`` only when a positive separation ``gap`` was
actually established; otherwise every downstream field
(``residual_norm_upper``, ``gap_lower``, ``sin_theta_upper``) is ``None``
-- an honest refusal, never a fabricated bound.
"""
dimension: int
cluster_size: int
gram_positive_definite: bool
ritz_lower: float | None
ritz_upper: float | None
cluster_start_index: int | None
gap_lower: float | None
residual_norm_upper: float | None
sin_theta_upper: float | None
certified: boolOther public import paths
omnibias.core.verified.InvariantSubspaceCertificateomnibias.core.verified.invariant_subspace.InvariantSubspaceCertificate
certified_invariant_subspace
omnibias.core.verified.certified_invariant_subspaceSource ↗certified_invariant_subspace(matrix: Matrix, basis: Sequence[Vector]) -> InvariantSubspaceCertificateCertify a Davis-Kahan sin Theta bound for span(basis).
Parameters
matrix: The n x n (numerically) symmetric operator A, as an interval matrix (entries may themselves be non-degenerate intervals for an uncertain A).
basis: The k candidate basis vectors (the columns of V), each of length n. Columns need not be orthonormal or even orthogonal -- they are rescaled by a per-column float norm (mirroring omnibias.core.verified.eig._partner_eigenvalue_lower's diagonal-congruence trick, for Gershgorin-free conditioning only) and then rigorously re-orthonormalized inside interval arithmetic (see _orthonormal_basis); soundness never depends on basis being well-conditioned, only on k linearly independent columns (a certified positive-definite Gram matrix).
Returns
InvariantSubspaceCertificate Works correctly for an **exactly degenerate** cluster (the k Ritz values need not be separated from *each other*, only the cluster as a whole from the rest of A's spectrum) and for any k >= 1.
Parameters
| Name | Type & default | Contract |
|---|---|---|
matrixpositional-or-keyword | MatrixRequired | The n x n (numerically) symmetric operator A, as an interval matrix (entries may themselves be non-degenerate intervals for an uncertain A). |
basispositional-or-keyword | Sequence[Vector]Required | The k candidate basis vectors (the columns of V), each of length n. Columns need not be orthonormal or even orthogonal -- they are rescaled by a per-column float norm (mirroring omnibias.core.verified.eig._partner_eigenvalue_lower's diagonal-congruence trick, for Gershgorin-free conditioning only) and then rigorously re-orthonormalized inside interval arithmetic (see _orthonormal_basis); soundness never depends on basis being well-conditioned, only on k linearly independent columns (a certified positive-definite Gram matrix). |
InvariantSubspaceCertificateExplicit validation & failure cases
- When
k < 1, raisesValueError('basis must contain at least one vector'). - When
k > n, raisesValueError('basis dimension k must not exceed the matrix dimension n'). - When
len(v) != n, raisesValueError('basis vector length must match matrix dimension').
These are explicit source guards. Backend operations may also raise for invalid shapes, dtypes, or unsupported devices.
Executed regression · result is the dataclass type
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_result_is_the_dataclass_type() -> None:
cert = certified_invariant_subspace(A_DEGENERATE, [[1.0, 0.0, 0.0], [0.0, 1.0, 0.0]])
assert isinstance(cert, InvariantSubspaceCertificate)
assert cert.dimension == 3
assert cert.cluster_size == 2python -m pytest "packages/omnibias-core/tests/verified/test_invariant_subspace.py::test_result_is_the_dataclass_type" -qRegression example · linearly dependent basis is 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.
def test_linearly_dependent_basis_is_refused() -> None:
# Duplicate columns -> singular Gram matrix -> honestly uncertified.
cert = certified_invariant_subspace(A_DEGENERATE, [[1.0, 0.0, 0.0], [1.0, 0.0, 0.0]])
assert not cert.certified
assert not cert.gram_positive_definite
assert cert.ritz_lower is None
assert cert.sin_theta_upper is Nonepython -m pytest packages/omnibias-core/tests/verified/test_invariant_subspace.py -k test_linearly_dependent_basis_is_refused -qRead the implementation
def certified_invariant_subspace(
matrix: Matrix, basis: Sequence[Vector]
) -> InvariantSubspaceCertificate:
r"""Certify a Davis-Kahan ``sin Theta`` bound for ``span(basis)``.
Parameters
----------
matrix:
The ``n x n`` (numerically) symmetric operator ``A``, as an interval
matrix (entries may themselves be non-degenerate intervals for an
uncertain ``A``).
basis:
The ``k`` candidate basis vectors (the columns of ``V``), each of
length ``n``. Columns need not be orthonormal or even orthogonal --
they are rescaled by a per-column float norm (mirroring
:func:`omnibias.core.verified.eig._partner_eigenvalue_lower`'s
diagonal-congruence trick, for Gershgorin-free conditioning only) and
then rigorously re-orthonormalized inside interval arithmetic (see
:func:`_orthonormal_basis`); soundness never depends on ``basis``
being well-conditioned, only on ``k`` linearly independent columns
(a certified positive-definite Gram matrix).
Returns
-------
InvariantSubspaceCertificate
Works correctly for an **exactly degenerate** cluster (the ``k``
Ritz values need not be separated from *each other*, only the
cluster as a whole from the rest of ``A``'s spectrum) and for any
``k >= 1``.
"""
a = _to_sym_matrix(matrix)
n = len(a)
k = len(basis)
if k < 1:
raise ValueError("basis must contain at least one vector")
if k > n:
raise ValueError("basis dimension k must not exceed the matrix dimension n")
raw = [[Interval.from_value(x) for x in v] for v in basis]
for v in raw:
if len(v) != n:
raise ValueError("basis vector length must match matrix dimension")
# Per-column float rescaling: conditions the Gram/Ritz blocks (mirrors
# eig._partner_eigenvalue_lower) but never affects soundness, since every
# certified quantity below is recomputed in interval arithmetic from the
# rescaled vectors.
vs: list[list[Interval]] = []
for v in raw:
norm = sqrt(sum((0.5 * (x.lo + x.hi)) ** 2 for x in v))
scale = Interval.point(1.0 / norm) if norm > 0.0 else Interval.point(1.0)
vs.append([x * scale for x in v])
gram = [[_dot(vs[i], vs[j]) for j in range(k)] for i in range(k)]
if not is_positive_definite(gram):
return InvariantSubspaceCertificate(
dimension=n,
cluster_size=k,
gram_positive_definite=False,
ritz_lower=None,
ritz_upper=None,
cluster_start_index=None,
gap_lower=None,
residual_norm_upper=None,
sin_theta_upper=None,
certified=False,
)
h = _ritz_block(a, vs)
ritz_lo = generalized_eigenvalue_enclosure(h, gram, 1).lo
ritz_hi = generalized_eigenvalue_enclosure(h, gram, k).hi
ident = identity_matrix(n)
p = count_eigenvalues_below(a, ident, ritz_lo)
if p is None or p + k > n:
return InvariantSubspaceCertificate(
dimension=n,
cluster_size=k,
gram_positive_definite=True,
ritz_lower=ritz_lo,
ritz_upper=ritz_hi,
cluster_start_index=None,
gap_lower=None,
residual_norm_upper=None,
sin_theta_upper=None,
certified=False,
)
ritz_lo_iv = Interval.point(ritz_lo)
ritz_hi_iv = Interval.point(ritz_hi)
if p >= 1:
left = generalized_eigenvalue_enclosure(a, ident, p)
left_gap = (ritz_lo_iv - Interval.point(left.hi)).lo
else:
left_gap = inf
if p + k < n:
right = generalized_eigenvalue_enclosure(a, ident, p + k + 1)
right_gap = (Interval.point(right.lo) - ritz_hi_iv).lo
else:
right_gap = inf
gap = min(left_gap, right_gap)
if not gap > 0.0:
return InvariantSubspaceCertificate(
dimension=n,
cluster_size=k,
gram_positive_definite=True,
ritz_lower=ritz_lo,
ritz_upper=ritz_hi,
cluster_start_index=p + 1,
gap_lower=(gap if gap != inf else None),
residual_norm_upper=None,
sin_theta_upper=None,
certified=False,
)
vtilde = _orthonormal_basis(vs, gram)
assert vtilde is not None # gram already certified PD above
residual_norm = _residual_frobenius_upper(a, vtilde)
sin_theta = min(residual_norm / gap, sqrt(k))
return InvariantSubspaceCertificate(
dimension=n,
cluster_size=k,
gram_positive_definite=True,
ritz_lower=ritz_lo,
ritz_upper=ritz_hi,
cluster_start_index=p + 1,
gap_lower=gap,
residual_norm_upper=residual_norm,
sin_theta_upper=sin_theta,
certified=True,
)Other public import paths
omnibias.core.verified.certified_invariant_subspaceomnibias.core.verified.invariant_subspace.certified_invariant_subspace