Skip to content

linalg · MinimumRealization

7 accepted declarations. Python and Rust forms, contracts, evidence, failure boundaries, and checked usages are kept together below.

Worked example

The complete checked program Compute and verify a Bézout certificate over the integers uses this API directly.

# SPDX-License-Identifier: MIT
# Copyright (c) 2026 Benjamin Antieau and Deven Manam
"""Compute and verify a Bézout certificate over the integers."""

from noether import Z


def main() -> None:
    identity = Z.extended_gcd(987_654_321, 123_456_789)
    identity.verify(Z, 987_654_321, 123_456_789)
    assert (
        identity.coefficient_a * 987_654_321 + identity.coefficient_b * 123_456_789 == identity.gcd
    )
    print(identity)


if __name__ == "__main__":
    main()

Run it with .venv/bin/python examples/01_bezout_certificates.py.

linalg.MinimumRealization

Three-way certified result of minimum-vector realization.

class MinimumRealization

noether::linalg::MinimumRealization · Direct Rust declaration

pub struct MinimumRealization { /* private fields */ }
Contract Value
Guarantee checked deterministic result
Determinism deterministic
Availability default CPU build
Domain implementation crates noether, flint-core, m4rst, m4rst-distributed, m4rste, mzs, pwvla, spar-core, sparla, sparb, lattice-enum
GIL attached / bounded
Semantic ID noether/linalg/MinimumRealization@1

Executable usage: validation/unit/linalg/test_lattice_facade.py:20 · validation/unit/linalg/test_lattice_facade.py:202

linalg.MinimumRealization.certificate

Return the certificate recorded by this MinimumRealization.

Detailed contract

Rational negative evidence, when proved nonrealizable.

(self) -> MinimumNonrealizabilityCertificate | None

noether::linalg::MinimumRealization::certificate · Direct Rust declaration

pub fn certificate(&self) -> Option<&MinimumNonrealizabilityCertificate>
Contract Value
Guarantee checked deterministic result
Determinism deterministic
Availability default CPU build
Domain implementation crates noether, flint-core, m4rst, m4rst-distributed, m4rste, mzs, pwvla, spar-core, sparla, sparb, lattice-enum
GIL attached / bounded
Semantic ID noether/linalg/MinimumRealization@1

Executable usage: examples/01_bezout_certificates.py:3 · examples/18_finite_field_schemes.py:14 · examples/18_finite_field_schemes.py:15 · validation/unit/commalg/test_acceptance_workload.py:135 · validation/unit/commalg/test_acceptance_workload.py:137 · validation/unit/commalg/test_acceptance_workload.py:138

linalg.MinimumRealization.configuration

Return the configuration recorded by this MinimumRealization.

Detailed contract

Candidate configuration common to every outcome.

(self) -> IntegralLineConfiguration

noether::linalg::MinimumRealization::configuration · Direct Rust declaration

pub fn configuration(&self) -> &IntegralLineConfiguration
Contract Value
Guarantee checked deterministic result
Determinism deterministic
Availability default CPU build
Domain implementation crates noether, flint-core, m4rst, m4rst-distributed, m4rste, mzs, pwvla, spar-core, sparla, sparb, lattice-enum
GIL attached / bounded
Semantic ID noether/linalg/MinimumRealization@1

Executable usage: examples/29_integral_line_configurations.py:29 · validation/unit/linalg/test_lattice_facade.py:100 · validation/unit/linalg/test_lattice_facade.py:101 · validation/unit/linalg/test_lattice_facade.py:102 · validation/unit/linalg/test_lattice_facade.py:103 · validation/unit/linalg/test_lattice_facade.py:106

linalg.MinimumRealization.diagnostic

Return the diagnostic recorded by this MinimumRealization.

Detailed contract

Diagnostic information, when the computation is inconclusive.

(self) -> MinimumRealizationDiagnostic | None

noether::linalg::MinimumRealization::diagnostic · Direct Rust declaration

pub fn diagnostic(&self) -> Option<&MinimumRealizationDiagnostic>
Contract Value
Guarantee checked deterministic result
Determinism deterministic
Availability default CPU build
Domain implementation crates noether, flint-core, m4rst, m4rst-distributed, m4rste, mzs, pwvla, spar-core, sparla, sparb, lattice-enum
GIL attached / bounded
Semantic ID noether/linalg/MinimumRealization@1

Executable usage: validation/unit/infra/test_engine_gateway.py:82 · validation/unit/linalg/test_lattice_facade.py:140 · validation/unit/linalg/test_lattice_facade.py:216 · validation/unit/linalg/test_lattice_facade.py:217 · validation/bench/macaulay2_derived.py:856

linalg.MinimumRealization.realization

Return the realization recorded by this MinimumRealization.

Detailed contract

Positive Gram and complete-enumeration evidence, when realized.

(self) -> MinimumVectorConfiguration | None

noether::linalg::MinimumRealization::realization · Direct Rust declaration

pub fn realization(&self) -> Option<&MinimumVectorConfiguration>
Contract Value
Guarantee checked deterministic result
Determinism deterministic
Availability default CPU build
Domain implementation crates noether, flint-core, m4rst, m4rst-distributed, m4rste, mzs, pwvla, spar-core, sparla, sparb, lattice-enum
GIL attached / bounded
Semantic ID noether/linalg/MinimumRealization@1

Executable usage: examples/29_integral_line_configurations.py:15 · examples/29_integral_line_configurations.py:16 · examples/29_integral_line_configurations.py:17 · examples/29_integral_line_configurations.py:18 · examples/29_integral_line_configurations.py:23 · examples/29_integral_line_configurations.py:28

linalg.MinimumRealization.status

Return the status recorded by this MinimumRealization.

Detailed contract

Terminal state: realized, nonrealizable, or inconclusive.

(self) -> Literal['realized', 'nonrealizable', 'inconclusive']

noether::linalg::MinimumRealization::status · Direct Rust declaration

pub fn status(&self) -> &'static str
Contract Value
Guarantee checked deterministic result
Determinism deterministic
Availability default CPU build
Domain implementation crates noether, flint-core, m4rst, m4rst-distributed, m4rste, mzs, pwvla, spar-core, sparla, sparb, lattice-enum
GIL attached / bounded
Semantic ID noether/linalg/MinimumRealization@1

Executable usage: examples/29_integral_line_configurations.py:17 · examples/29_integral_line_configurations.py:22 · validation/unit/infra/test_macaulay2_benchmark_protocol.py:264 · validation/unit/infra/test_macaulay2_benchmark_protocol.py:282 · validation/unit/infra/test_macaulay2_benchmark_protocol.py:289 · validation/unit/infra/test_macaulay2_benchmark_protocol.py:343

linalg.MinimumRealization.verify

Replay and verify the mathematical evidence carried by this MinimumRealization.

Detailed contract

Verify the mathematical evidence appropriate to the outcome.

(self) -> None

noether::linalg::MinimumRealization::verify · Direct Rust declaration

pub fn verify(&self) -> Result<(), LineConfigurationError>
Contract Value
Guarantee checked deterministic result
Determinism deterministic
Availability default CPU build
Domain implementation crates noether, flint-core, m4rst, m4rst-distributed, m4rste, mzs, pwvla, spar-core, sparla, sparb, lattice-enum
GIL attached / bounded
Semantic ID noether/linalg/MinimumRealization@1

Executable usage: examples/01_bezout_certificates.py:10 · examples/01_bezout_certificates.py:3 · examples/03_exact_linear_systems.py:13 · examples/03_exact_linear_systems.py:3 · examples/04_smith_normal_form.py:12 · examples/06_shortest_lattice_vectors.py:12